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 wulflinc10 THE 2005-04-21 08:23:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12647 boxname=wulflinc10 idbench=973 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 10386fd19d9976c249ce2be861b38a70 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 12647 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 445668 kB Buffers: 33804 kB Cached: 532976 kB SwapCached: 0 kB Active: 159224 kB Inactive: 410052 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 445416 kB SwapTotal: 2097136 kB SwapFree: 2096784 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6412 kB Slab: 14088 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 08:43:32 (client local time) WITH STATUS 10 IN 1200.13 SECONDS stats: 12647 7 1200.13 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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 13152 47982 | 3945 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/1948 c -- var.elim.: 1948/1948 c -- var.elim.: 255/255 c -- subsuming c -- var.elim.: 89/89 c | 0 | 12429 44143 | -- 0 -- -- | -- | -364/-1112 c | 0 | 12429 44143 | 4971 0 0 nan | 0.000 % | c | 100 | 12429 44143 | 5468 100 688 6.9 | 15.718 % | c ============================================================================== c (current CPU-time: 0.45793 s) c ============================================================================== c [1mFound solution: 3053568[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 211 | 14544 49081 | 4363 211 2671 12.7 | 15.718 % | c -- subsuming c -- var.elim.: 810/810 c -- var.elim.: 443/443 c -- var.elim.: 10/10 c -- subsuming c -- var.elim.: 124/124 c -- var.elim.: 30/30 c | 211 | 14219 49850 | -- 211 -- -- | -- | -325/770 c | 211 | 14219 49850 | 5687 211 2671 12.7 | 15.718 % | c | 312 | 14219 49850 | 6256 312 17988 57.7 | 13.453 % | c | 463 | 14219 49850 | 6881 463 31703 68.5 | 13.453 % | c | 689 | 14219 49850 | 7570 689 70289 102.0 | 13.453 % | c | 1026 | 14219 49850 | 8327 1026 101311 98.7 | 13.453 % | c | 1532 | 14219 49850 | 9159 1532 160501 104.8 | 13.453 % | c | 2292 | 14219 49850 | 10075 2292 235028 102.5 | 13.453 % | c | 3431 | 14219 49850 | 11083 3431 388676 113.3 | 13.453 % | c | 5140 | 14219 49850 | 12191 5140 555823 108.1 | 13.453 % | c | 7702 | 14219 49850 | 13411 7702 935323 121.4 | 13.453 % | c | 11546 | 14219 49850 | 14752 11546 1409850 122.1 | 13.453 % | c ============================================================================== c (current CPU-time: 22.6876 s) c ============================================================================== c [1mFound solution: 2376704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 11669 | 14355 50226 | 4306 11669 1423863 122.0 | 13.453 % | c -- subsuming c -- var.elim.: 267/267 c -- var.elim.: 132/132 c | 11669 | 14271 50239 | -- 11669 -- -- | -- | -84/14 c | 11669 | 14271 50239 | 5708 11669 1423863 122.0 | 13.453 % | c | 11769 | 14271 50239 | 6279 5287 574571 108.7 | 13.450 % | c | 11920 | 14271 50239 | 6907 5438 598192 110.0 | 13.450 % | c | 12145 | 14271 50239 | 7597 5663 619865 109.5 | 13.450 % | c | 12483 | 14271 50239 | 8357 6001 661431 110.2 | 13.450 % | c | 12989 | 14271 50239 | 9193 6507 706989 108.7 | 13.450 % | c | 13748 | 14271 50239 | 10112 7266 782822 107.7 | 13.450 % | c | 14887 | 14271 50239 | 11124 8405 830794 98.8 | 13.450 % | c | 16596 | 14271 50239 | 12236 10114 1025259 101.4 | 13.450 % | c ============================================================================== c (current CPU-time: 30.9193 s) c ============================================================================== c [1mFound solution: 1439744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17069 | 14329 50398 | 4298 10587 1041987 98.4 | 13.450 % | c -- subsuming c -- var.elim.: 124/124 c -- var.elim.: 66/66 c | 17069 | 14305 50596 | -- 10587 -- -- | -- | -24/199 c | 17069 | 14305 50596 | 5722 10587 1041987 98.4 | 13.450 % | c | 17169 | 14305 50596 | 6294 4806 323309 67.3 | 13.473 % | c | 17319 | 14305 50596 | 6923 4956 332289 67.0 | 13.473 % | c | 17545 | 14305 50596 | 7615 5182 352745 68.1 | 13.473 % | c | 17883 | 14305 50596 | 8377 5520 392849 71.2 | 13.473 % | c | 18389 | 14305 50596 | 9215 6026 410638 68.1 | 13.473 % | c | 19149 | 14305 50596 | 10136 6786 470178 69.3 | 13.473 % | c | 20289 | 14305 50596 | 11150 7926 530131 66.9 | 13.473 % | c | 21998 | 14305 50596 | 12265 9635 624905 64.9 | 13.473 % | c | 24562 | 14259 50082 | 13448 12198 722708 59.2 | 13.511 % | c | 28406 | 14259 50082 | 14793 11293 522489 46.3 | 13.511 % | c | 34172 | 14259 50082 | 16273 11914 528669 44.4 | 13.511 % | c | 42821 | 14211 49880 | 17840 14909 671994 45.1 | 13.744 % | c ============================================================================== c (current CPU-time: 63.3104 s) c ============================================================================== c [1mFound solution: 1349632[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 50297 | 14234 49943 | 4270 16186 690852 42.7 | 13.744 % | c -- subsuming c -- var.elim.: 123/123 c -- var.elim.: 62/62 c -- var.elim.: 3/3 c | 50297 | 14208 49930 | -- 16186 -- -- | -- | -24/-8 c | 50297 | 14208 49930 | 5683 16184 690790 42.7 | 13.744 % | c | 50397 | 14208 49930 | 6251 4896 203529 41.6 | 13.965 % | c | 50547 | 14208 49930 | 6876 5046 207369 41.1 | 13.965 % | c | 50772 | 14208 49930 | 7564 5271 217531 41.3 | 13.965 % | c | 51110 | 14208 49930 | 8320 5609 225153 40.1 | 13.965 % | c | 51617 | 14208 49930 | 9152 6116 238619 39.0 | 13.965 % | c | 52376 | 14208 49930 | 10068 6875 324522 47.2 | 13.965 % | c | 53515 | 14208 49930 | 11074 8014 380370 47.5 | 13.965 % | c | 55223 | 14208 49930 | 12182 9722 462064 47.5 | 13.965 % | c ============================================================================== c (current CPU-time: 68.3606 s) c ============================================================================== c [1mFound solution: 1114112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 55358 | 14264 50091 | 4279 9857 469189 47.6 | 13.965 % | c -- subsuming c -- var.elim.: 124/124 c -- var.elim.: 81/81 c | 55358 | 14232 50101 | -- 9857 -- -- | -- | -32/11 c | 55358 | 14232 50101 | 5692 9857 469189 47.6 | 13.965 % | c | 55459 | 14232 50101 | 6262 4483 214310 47.8 | 13.993 % | c | 55609 | 14232 50101 | 6888 4633 219009 47.3 | 13.993 % | c | 55834 | 14232 50101 | 7577 4858 229275 47.2 | 13.993 % | c | 56171 | 14232 50101 | 8334 5195 237118 45.6 | 13.993 % | c | 56677 | 14232 50101 | 9168 5701 255178 44.8 | 13.993 % | c | 57437 | 14232 50101 | 10085 6461 282231 43.7 | 13.993 % | c | 58577 | 14232 50101 | 11093 7601 327547 43.1 | 13.993 % | c | 60285 | 14232 50101 | 12203 9309 383224 41.2 | 13.993 % | c ============================================================================== c (current CPU-time: 72.8969 s) c ============================================================================== c [1mFound solution: 1091584[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 62479 | 14286 50260 | 4285 11503 484638 42.1 | 13.993 % | c -- subsuming c -- var.elim.: 104/104 c -- var.elim.: 72/72 c | 62479 | 14256 50270 | -- 11503 -- -- | -- | -30/11 c | 62479 | 14256 50270 | 5702 11503 484638 42.1 | 13.993 % | c | 62579 | 14256 50270 | 6272 5213 177154 34.0 | 14.005 % | c | 62730 | 14256 50270 | 6899 5364 183255 34.2 | 14.005 % | c | 62955 | 14256 50270 | 7589 5589 196304 35.1 | 14.005 % | c | 63293 | 14256 50270 | 8348 5927 208156 35.1 | 14.005 % | c | 63800 | 14256 50270 | 9183 6434 230618 35.8 | 14.005 % | c | 64561 | 14256 50270 | 10102 7195 260804 36.2 | 14.005 % | c | 65700 | 14256 50270 | 11112 8334 309868 37.2 | 14.005 % | c | 67408 | 14256 50270 | 12223 10042 379759 37.8 | 14.005 % | c | 69970 | 14256 50270 | 13445 12604 504441 40.0 | 14.005 % | c | 73815 | 14256 50270 | 14790 11664 562095 48.2 | 14.005 % | c | 79581 | 14256 50270 | 16269 12228 646047 52.8 | 14.005 % | c | 88230 | 14256 50270 | 17896 15226 702493 46.1 | 14.005 % | c | 101205 | 14256 50270 | 19686 14889 944249 63.4 | 14.005 % | c ============================================================================== c (current CPU-time: 132.394 s) c ============================================================================== c [1mFound solution: 1085440[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 112900 | 14304 50412 | 4291 19617 1175865 59.9 | 14.005 % | c -- subsuming c -- var.elim.: 93/93 c -- var.elim.: 67/67 c | 112900 | 14278 50406 | -- 19617 -- -- | -- | -26/-5 c | 112900 | 14278 50406 | 5711 19617 1175865 59.9 | 14.005 % | c | 113000 | 14278 50406 | 6282 5564 248740 44.7 | 14.022 % | c | 113150 | 14278 50406 | 6910 5714 250272 43.8 | 14.022 % | c | 113376 | 14278 50406 | 7601 5940 260805 43.9 | 14.022 % | c | 113714 | 14278 50406 | 8361 6278 283190 45.1 | 14.022 % | c | 114221 | 14278 50406 | 9197 6785 303247 44.7 | 14.022 % | c | 114980 | 14278 50406 | 10117 7544 336091 44.6 | 14.022 % | c ============================================================================== c (current CPU-time: 135.431 s) c ============================================================================== c [1mFound solution: 934912[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 115741 | 14306 50490 | 4291 8305 377260 45.4 | 14.022 % | c -- subsuming c -- var.elim.: 88/88 c -- var.elim.: 82/82 c -- var.elim.: 19/19 c -- var.elim.: 11/11 c -- var.elim.: 20/20 c | 115741 | 14199 50247 | -- 8305 -- -- | -- | -70/-96 c | 115741 | 14199 50247 | 5679 7408 281886 38.1 | 14.022 % | c | 115841 | 14199 50247 | 6247 5039 170645 33.9 | 14.380 % | c | 115995 | 14199 50247 | 6872 5193 179758 34.6 | 14.380 % | c | 116220 | 14199 50247 | 7559 5418 190968 35.2 | 14.380 % | c | 116559 | 14199 50247 | 8315 5757 199420 34.6 | 14.380 % | c | 117065 | 14199 50247 | 9147 6263 221541 35.4 | 14.380 % | c | 117824 | 14199 50247 | 10061 7022 247473 35.2 | 14.380 % | c | 118963 | 14199 50247 | 11067 8161 290223 35.6 | 14.380 % | c | 120672 | 14182 50154 | 12160 9869 350255 35.5 | 14.457 % | c | 123236 | 14182 50154 | 13376 12433 484969 39.0 | 14.457 % | c ============================================================================== c (current CPU-time: 142.332 s) c ============================================================================== c [1mFound solution: 730112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 123658 | 14219 50270 | 4265 12855 499657 38.9 | 14.457 % | c -- subsuming c -- var.elim.: 125/125 c -- var.elim.: 97/97 c -- var.elim.: 15/15 c | 123658 | 14170 50324 | -- 12855 -- -- | -- | -49/55 c | 123658 | 14170 50324 | 5668 12840 499456 38.9 | 14.457 % | c | 123759 | 14170 50324 | 6234 5808 209474 36.1 | 14.652 % | c | 123909 | 14170 50324 | 6858 5958 215622 36.2 | 14.652 % | c | 124134 | 14170 50324 | 7544 6183 221644 35.8 | 14.652 % | c | 124474 | 14170 50324 | 8298 6523 233055 35.7 | 14.652 % | c | 124980 | 14170 50324 | 9128 7029 252621 35.9 | 14.652 % | c | 125739 | 14170 50324 | 10041 7788 281064 36.1 | 14.652 % | c | 126879 | 14170 50324 | 11045 8928 323902 36.3 | 14.652 % | c | 128588 | 14170 50324 | 12149 10637 397003 37.3 | 14.652 % | c | 131150 | 14170 50324 | 13364 8973 283352 31.6 | 14.652 % | c | 134995 | 14170 50324 | 14701 12818 457391 35.7 | 14.652 % | c | 140762 | 14170 50324 | 16171 13470 576250 42.8 | 14.652 % | c | 149412 | 14170 50324 | 17788 16420 871988 53.1 | 14.652 % | c | 162387 | 14170 50324 | 19567 17148 901121 52.5 | 14.652 % | c | 181848 | 14143 50187 | 21483 13229 809485 61.2 | 14.769 % | c | 211040 | 14134 50152 | 23616 14463 731577 50.6 | 14.808 % | c | 254831 | 14079 49782 | 25877 13599 732388 53.9 | 15.002 % | c | 320517 | 14079 49782 | 28464 17581 889976 50.6 | 15.002 % | c ============================================================================== c (current CPU-time: 419.67 s) c ============================================================================== c [1mFound solution: 719872[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 323037 | 14113 49883 | 4233 20101 1076867 53.6 | 15.002 % | c -- subsuming c -- var.elim.: 145/145 c -- var.elim.: 116/116 c -- var.elim.: 71/71 c -- var.elim.: 16/16 c -- var.elim.: 9/9 c | 323037 | 13931 48823 | -- 20101 -- -- | -- | -182/-1059 c | 323037 | 13931 48823 | 5572 20076 1073529 53.5 | 15.002 % | c | 323138 | 13931 48823 | 6129 6050 292049 48.3 | 15.300 % | c | 323289 | 13931 48823 | 6742 6201 296848 47.9 | 15.300 % | c | 323515 | 13931 48823 | 7416 6427 304476 47.4 | 15.300 % | c | 323852 | 13931 48823 | 8158 6764 313830 46.4 | 15.300 % | c | 324358 | 13931 48823 | 8974 7270 327645 45.1 | 15.300 % | c | 325118 | 13931 48823 | 9871 8030 356159 44.4 | 15.300 % | c | 326261 | 13931 48823 | 10859 9173 409371 44.6 | 15.300 % | c | 327969 | 13931 48823 | 11944 10881 484079 44.5 | 15.300 % | c | 330532 | 13931 48823 | 13139 9189 340366 37.0 | 15.300 % | c | 334380 | 13931 48823 | 14453 13037 519853 39.9 | 15.300 % | c | 340146 | 13931 48823 | 15898 13753 606012 44.1 | 15.300 % | c | 348795 | 13931 48823 | 17488 11344 503259 44.4 | 15.300 % | c ============================================================================== c (current CPU-time: 450.215 s) c ============================================================================== c [1mFound solution: 645120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 353355 | 13987 48984 | 4196 15904 692192 43.5 | 15.300 % | c -- subsuming c -- var.elim.: 118/118 c -- var.elim.: 72/72 c | 353355 | 13956 48966 | -- 15904 -- -- | -- | -31/-17 c | 353355 | 13956 48966 | 5582 15904 692192 43.5 | 15.300 % | c | 353455 | 13956 48966 | 6140 4813 160374 33.3 | 15.297 % | c | 353605 | 13956 48966 | 6754 4963 163510 32.9 | 15.297 % | c | 353830 | 13956 48966 | 7430 5188 168204 32.4 | 15.297 % | c | 354167 | 13956 48966 | 8173 5525 181010 32.8 | 15.297 % | c | 354674 | 13956 48966 | 8990 6032 197528 32.7 | 15.297 % | c | 355433 | 13956 48966 | 9889 6791 219084 32.3 | 15.297 % | c ============================================================================== c (current CPU-time: 452.178 s) c ============================================================================== c [1mFound solution: 586752[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 355662 | 13981 49052 | 4194 7020 233699 33.3 | 15.297 % | c -- subsuming c -- var.elim.: 66/66 c -- var.elim.: 48/48 c | 355662 | 13967 49030 | -- 7020 -- -- | -- | -14/-21 c | 355662 | 13967 49030 | 5586 7020 233699 33.3 | 15.297 % | c | 355763 | 13967 49030 | 6145 4781 137434 28.7 | 15.318 % | c | 355913 | 13967 49030 | 6760 4931 140243 28.4 | 15.318 % | c | 356138 | 13967 49030 | 7436 5156 147634 28.6 | 15.318 % | c | 356477 | 13967 49030 | 8179 5495 163158 29.7 | 15.318 % | c | 356983 | 13967 49030 | 8997 6001 179260 29.9 | 15.318 % | c | 357744 | 13967 49030 | 9897 6762 202408 29.9 | 15.318 % | c | 358883 | 13967 49030 | 10887 7901 239683 30.3 | 15.318 % | c | 360591 | 13967 49030 | 11975 9609 312804 32.6 | 15.318 % | c | 363153 | 13967 49030 | 13173 12171 422696 34.7 | 15.318 % | c | 366997 | 13967 49030 | 14490 11361 391573 34.5 | 15.318 % | c | 372764 | 13967 49030 | 15939 12116 436879 36.1 | 15.318 % | c | 381413 | 13967 49030 | 17533 15184 720989 47.5 | 15.318 % | c ============================================================================== c (current CPU-time: 488.13 s) c ============================================================================== c [1mFound solution: 505856[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 389055 | 13982 49089 | 4194 16738 874844 52.3 | 15.318 % | c -- subsuming c -- var.elim.: 78/78 c -- var.elim.: 53/53 c -- var.elim.: 44/44 c -- var.elim.: 22/22 c | 389055 | 13827 48417 | -- 16738 -- -- | -- | -65/-349 c | 389055 | 13827 48417 | 5530 15691 757889 48.3 | 15.318 % | c | 389155 | 13827 48417 | 6083 4750 179439 37.8 | 15.920 % | c | 389306 | 13827 48417 | 6692 4901 181811 37.1 | 15.920 % | c | 389531 | 13827 48417 | 7361 5126 194835 38.0 | 15.920 % | c | 389869 | 13827 48417 | 8097 5464 203761 37.3 | 15.920 % | c | 390375 | 13827 48417 | 8907 5970 220801 37.0 | 15.920 % | c | 391135 | 13827 48417 | 9798 6730 253043 37.6 | 15.920 % | c | 392274 | 13827 48417 | 10777 7869 297313 37.8 | 15.920 % | c | 393982 | 13827 48417 | 11855 9577 351251 36.7 | 15.920 % | c | 396547 | 13816 48368 | 13030 12141 451466 37.2 | 15.959 % | c | 400391 | 13750 48127 | 14265 11415 400124 35.1 | 16.392 % | c | 406158 | 13750 48127 | 15692 12097 503090 41.6 | 16.392 % | c ============================================================================== c (current CPU-time: 504.044 s) c ============================================================================== c [1mFound solution: 416768[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 406504 | 13772 48206 | 4131 12443 522414 42.0 | 16.392 % | c -- subsuming c -- var.elim.: 76/76 c -- var.elim.: 63/63 c -- var.elim.: 49/49 c -- var.elim.: 59/59 c -- var.elim.: 11/11 c | 406504 | 13682 47895 | -- 12443 -- -- | -- | -90/-310 c | 406504 | 13682 47895 | 5472 10753 372574 34.6 | 16.392 % | c | 406606 | 13682 47895 | 6020 4882 149374 30.6 | 16.680 % | c | 406756 | 13682 47895 | 6622 5032 153741 30.6 | 16.680 % | c | 406981 | 13682 47895 | 7284 5257 157122 29.9 | 16.680 % | c | 407318 | 13682 47895 | 8012 5594 170896 30.5 | 16.680 % | c | 407825 | 13682 47895 | 8813 6101 186688 30.6 | 16.680 % | c | 408585 | 13682 47895 | 9695 6861 214871 31.3 | 16.680 % | c | 409724 | 13668 47847 | 10654 7998 253597 31.7 | 16.759 % | c | 411432 | 13668 47847 | 11719 9706 329529 34.0 | 16.759 % | c | 413995 | 13655 47801 | 12879 12266 427958 34.9 | 16.838 % | c | 417840 | 13655 47801 | 14167 11623 425850 36.6 | 16.838 % | c | 423606 | 13655 47801 | 15583 12378 446213 36.0 | 16.838 % | c | 432255 | 13655 47801 | 17142 15557 608027 39.1 | 16.838 % | c ============================================================================== c (current CPU-time: 542.168 s) c ============================================================================== c [1mFound solution: 395264[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 444125 | 13741 48016 | 4122 15436 674235 43.7 | 16.838 % | c -- subsuming c -- var.elim.: 169/169 c -- var.elim.: 108/108 c -- var.elim.: 15/15 c | 444125 | 13670 47900 | -- 15436 -- -- | -- | -71/-115 c | 444125 | 13670 47900 | 5468 14790 625455 42.3 | 16.838 % | c | 444225 | 13670 47900 | 6014 4483 153449 34.2 | 16.930 % | c | 444375 | 13670 47900 | 6616 4633 158140 34.1 | 16.930 % | c | 444601 | 13670 47900 | 7277 4859 161964 33.3 | 16.930 % | c | 444938 | 13670 47900 | 8005 5196 167443 32.2 | 16.930 % | c | 445444 | 13670 47900 | 8806 5702 187479 32.9 | 16.930 % | c | 446203 | 13670 47900 | 9686 6461 216905 33.6 | 16.930 % | c | 447343 | 13670 47900 | 10655 7601 258812 34.0 | 16.930 % | c | 449052 | 13670 47900 | 11721 9310 319083 34.3 | 16.930 % | c | 451614 | 13670 47900 | 12893 11872 462516 39.0 | 16.930 % | c ============================================================================== c (current CPU-time: 549.248 s) c ============================================================================== c [1mFound solution: 392192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 451852 | 13716 48034 | 4114 12110 483502 39.9 | 16.930 % | c -- subsuming c -- var.elim.: 88/88 c -- var.elim.: 67/67 c -- var.elim.: 31/31 c | 451852 | 13641 47770 | -- 12110 -- -- | -- | -75/-263 c | 451852 | 13641 47770 | 5456 12051 478275 39.7 | 16.930 % | c | 451952 | 13641 47770 | 6002 5456 215790 39.6 | 17.010 % | c | 452103 | 13641 47770 | 6602 5607 219280 39.1 | 17.010 % | c | 452328 | 13641 47770 | 7262 5832 225041 38.6 | 17.010 % | c | 452665 | 13641 47770 | 7988 6169 236550 38.3 | 17.010 % | c | 453173 | 13641 47770 | 8787 6677 251716 37.7 | 17.010 % | c | 453934 | 13641 47770 | 9666 7438 280924 37.8 | 17.010 % | c | 455075 | 13641 47770 | 10632 8579 326590 38.1 | 17.010 % | c | 456783 | 13641 47770 | 11696 10287 392700 38.2 | 17.010 % | c | 459345 | 13641 47770 | 12865 8761 290098 33.1 | 17.010 % | c | 463189 | 13641 47770 | 14152 12605 575879 45.7 | 17.010 % | c | 468956 | 13641 47770 | 15567 13338 715647 53.7 | 17.010 % | c | 477605 | 13641 47770 | 17124 11195 530477 47.4 | 17.010 % | c | 490581 | 13641 47770 | 18836 12239 606057 49.5 | 17.010 % | c | 5#### 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.55 0.86 0.88 2/54 27998 Raw data (stat): 27998 (runsolver) R 27997 25347 25346 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 485397835 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 97 215 215 0 42 0 vsize: 1028 [startup+9.99933 s] Raw data (loadavg): 0.62 0.87 0.88 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 1794 0 0 0 994 4 0 0 25 0 1 0 485397835 8327168 1655 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2033 1655 603 41 0 1992 0 vsize: 8132 [startup+19.9989 s] Raw data (loadavg): 0.68 0.87 0.88 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2434 0 0 0 1992 6 0 0 25 0 1 0 485397835 10960896 2295 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2676 2295 603 41 0 2635 0 vsize: 10704 [startup+29.9996 s] Raw data (loadavg): 0.72 0.87 0.88 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2717 0 0 0 2991 8 0 0 25 0 1 0 485397835 11923456 2543 4294967295 134512640 134672761 3221224528 3221223568 134612783 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2911 2543 603 41 0 2870 0 vsize: 11644 [startup+39.9991 s] Raw data (loadavg): 0.77 0.88 0.88 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2742 0 0 0 3991 8 0 0 25 0 1 0 485397835 11747328 2502 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2868 2502 603 41 0 2827 0 vsize: 11472 [startup+49.9997 s] Raw data (loadavg): 0.80 0.88 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2744 0 0 0 4991 8 0 0 25 0 1 0 485397835 11747328 2504 4294967295 134512640 134672761 3221224528 3221223568 134613809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2868 2504 603 41 0 2827 0 vsize: 11472 [startup+59.9993 s] Raw data (loadavg): 0.83 0.88 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2763 0 0 0 5990 9 0 0 25 0 1 0 485397835 11878400 2523 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2900 2523 603 41 0 2859 0 vsize: 11600 [startup+69.9988 s] Raw data (loadavg): 0.86 0.89 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2844 0 0 0 6989 10 0 0 25 0 1 0 485397835 11943936 2552 4294967295 134512640 134672761 3221224528 3221223712 134616017 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2552 603 41 0 2875 0 vsize: 11664 [startup+79.9994 s] Raw data (loadavg): 0.88 0.89 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 7989 10 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223568 134612832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2554 603 41 0 2875 0 vsize: 11664 [startup+89.999 s] Raw data (loadavg): 0.90 0.89 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 8989 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2554 603 41 0 2875 0 vsize: 11664 [startup+99.9995 s] Raw data (loadavg): 0.91 0.90 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 9988 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223568 134614239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2554 603 41 0 2875 0 vsize: 11664 [startup+110 s] Raw data (loadavg): 0.93 0.90 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 10988 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2554 603 41 0 2875 0 vsize: 11664 [startup+120 s] Raw data (loadavg): 0.94 0.90 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2933 0 0 0 11988 12 0 0 25 0 1 0 485397835 12206080 2604 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2980 2604 603 41 0 2939 0 vsize: 11920 [startup+129.999 s] Raw data (loadavg): 0.95 0.91 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3089 0 0 0 12987 13 0 0 25 0 1 0 485397835 12828672 2760 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2760 603 41 0 3091 0 vsize: 12528 [startup+139.999 s] Raw data (loadavg): 0.95 0.91 0.89 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3193 0 0 0 13987 13 0 0 25 0 1 0 485397835 12820480 2768 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3130 2768 603 41 0 3089 0 vsize: 12520 [startup+150 s] Raw data (loadavg): 0.96 0.91 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 14986 14 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+160 s] Raw data (loadavg): 0.97 0.91 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 15986 14 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+169.999 s] Raw data (loadavg): 0.97 0.92 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 16986 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+179.999 s] Raw data (loadavg): 0.97 0.92 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 17985 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+190 s] Raw data (loadavg): 0.98 0.92 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 18985 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+200 s] Raw data (loadavg): 0.98 0.92 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 19985 16 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+210 s] Raw data (loadavg): 0.98 0.92 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 20985 16 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223664 134614513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3128 2766 603 41 0 3087 0 vsize: 12512 [startup+220 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3293 0 0 0 21985 16 0 0 25 0 1 0 485397835 13041664 2811 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3184 2811 603 41 0 3143 0 vsize: 12736 [startup+230 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3513 0 0 0 22985 17 0 0 25 0 1 0 485397835 13930496 3031 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3401 3031 603 41 0 3360 0 vsize: 13604 [startup+239.999 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3513 0 0 0 23984 17 0 0 25 0 1 0 485397835 13930496 3031 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3401 3031 603 41 0 3360 0 vsize: 13604 [startup+250 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 24984 17 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223728 134610705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3416 3044 603 41 0 3375 0 vsize: 13664 [startup+260.001 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 25984 18 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223712 134615752 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3416 3044 603 41 0 3375 0 vsize: 13664 [startup+270.001 s] Raw data (loadavg): 0.99 0.93 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 26984 18 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3416 3044 603 41 0 3375 0 vsize: 13664 [startup+280.001 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3529 0 0 0 27984 18 0 0 25 0 1 0 485397835 13983744 3045 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3414 3045 603 41 0 3373 0 vsize: 13656 [startup+290 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 28984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3414 3046 603 41 0 3373 0 vsize: 13656 [startup+300 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 29984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223672 134616132 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3414 3046 603 41 0 3373 0 vsize: 13656 [startup+309.999 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 30984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3414 3046 603 41 0 3373 0 vsize: 13656 [startup+319.999 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3564 0 0 0 31985 18 0 0 25 0 1 0 485397835 14127104 3079 4294967295 134512640 134672761 3221224528 3221223712 134615681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3449 3079 603 41 0 3408 0 vsize: 13796 [startup+330 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3564 0 0 0 32985 18 0 0 25 0 1 0 485397835 14127104 3079 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3449 3079 603 41 0 3408 0 vsize: 13796 [startup+339.999 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3751 0 0 0 33985 18 0 0 25 0 1 0 485397835 14880768 3266 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3633 3266 603 41 0 3592 0 vsize: 14532 [startup+349.998 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3758 0 0 0 34985 18 0 0 25 0 1 0 485397835 15015936 3273 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3273 603 41 0 3625 0 vsize: 14664 [startup+359.998 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 35985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3325 603 41 0 3651 0 vsize: 14768 [startup+369.998 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 36985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3325 603 41 0 3651 0 vsize: 14768 [startup+379.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 37985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3325 603 41 0 3651 0 vsize: 14768 [startup+389.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 38985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3692 3325 603 41 0 3651 0 vsize: 14768 [startup+399.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3875 0 0 0 39985 19 0 0 25 0 1 0 485397835 15388672 3390 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3757 3390 603 41 0 3716 0 vsize: 15028 [startup+409.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3875 0 0 0 40985 19 0 0 25 0 1 0 485397835 15388672 3390 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3757 3390 603 41 0 3716 0 vsize: 15028 [startup+419.996 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4013 0 0 0 41985 19 0 0 25 0 1 0 485397835 15544320 3433 4294967295 134512640 134672761 3221224528 3221223784 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3795 3433 603 41 0 3754 0 vsize: 15180 [startup+429.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4019 0 0 0 42984 19 0 0 25 0 1 0 485397835 15740928 3439 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3439 603 41 0 3802 0 vsize: 15372 [startup+439.997 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4037 0 0 0 43985 19 0 0 25 0 1 0 485397835 15740928 3457 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3457 603 41 0 3802 0 vsize: 15372 [startup+449.996 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4037 0 0 0 44985 19 0 0 25 0 1 0 485397835 15740928 3457 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3457 603 41 0 3802 0 vsize: 15372 [startup+459.997 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 45984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3470 603 41 0 3802 0 vsize: 15372 [startup+469.996 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 46984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223664 134614524 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3470 603 41 0 3802 0 vsize: 15372 [startup+479.996 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 47984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223712 134615755 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3470 603 41 0 3802 0 vsize: 15372 [startup+489.995 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 48984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+499.998 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 49984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+509.999 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 50983 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+519.998 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 51984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223728 134610622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+529.999 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 52984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+539.998 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 53984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3471 603 41 0 3802 0 vsize: 15372 [startup+549.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 54982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+559.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 55981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+569.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 56981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+579.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 57981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+589.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 58981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+599.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 59981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+609.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 60982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+619.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 61982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3472 603 41 0 3802 0 vsize: 15372 [startup+630.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 62981 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615591 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3474 603 41 0 3802 0 vsize: 15372 [startup+640.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 63981 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615571 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3474 603 41 0 3802 0 vsize: 15372 [startup+650.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 64980 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3474 603 41 0 3802 0 vsize: 15372 [startup+660.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 65980 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3474 603 41 0 3802 0 vsize: 15372 [startup+670.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 66979 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223568 134603510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3474 603 41 0 3802 0 vsize: 15372 [startup+680.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 67979 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+690.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 68980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+700.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 69980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+710.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 70980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615505 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+720.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 71980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+730.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 72980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3843 3475 603 41 0 3802 0 vsize: 15372 [startup+740.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4078 0 0 0 73980 22 0 0 25 0 1 0 485397835 15810560 3485 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3860 3485 603 41 0 3819 0 vsize: 15440 [startup+750.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4148 0 0 0 74980 23 0 0 25 0 1 0 485397835 16093184 3554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3929 3554 603 41 0 3888 0 vsize: 15716 [startup+760.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4148 0 0 0 75981 23 0 0 25 0 1 0 485397835 16093184 3554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3929 3554 603 41 0 3888 0 vsize: 15716 [startup+770.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 76981 23 0 0 25 0 1 0 485397835 16306176 3606 4294967295 134512640 134672761 3221224528 3221223560 134612937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3981 3606 603 41 0 3940 0 vsize: 15924 [startup+780.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 77981 23 0 0 25 0 1 0 485397835 16306176 3606 4294967295 134512640 134672761 3221224528 3221223712 134615638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3981 3606 603 41 0 3940 0 vsize: 15924 [startup+790.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 78981 23 0 0 25 0 1 0 485397835 16302080 3605 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3980 3605 603 41 0 3939 0 vsize: 15920 [startup+800.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 79981 23 0 0 25 0 1 0 485397835 16302080 3605 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3980 3605 603 41 0 3939 0 vsize: 15920 [startup+810.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4223 0 0 0 80981 23 0 0 25 0 1 0 485397835 16396288 3628 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4003 3628 603 41 0 3962 0 vsize: 16012 [startup+820.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4223 0 0 0 81982 23 0 0 25 0 1 0 485397835 16396288 3628 4294967295 134512640 134672761 3221224528 3221223712 134615551 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4003 3628 603 41 0 3962 0 vsize: 16012 [startup+830.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4278 0 0 0 82981 23 0 0 25 0 1 0 485397835 16666624 3683 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4069 3683 603 41 0 4028 0 vsize: 16276 [startup+840.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4358 0 0 0 83981 23 0 0 25 0 1 0 485397835 16945152 3762 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4137 3762 603 41 0 4096 0 vsize: 16548 [startup+850.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4358 0 0 0 84982 23 0 0 25 0 1 0 485397835 16945152 3762 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4137 3762 603 41 0 4096 0 vsize: 16548 [startup+860.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4376 0 0 0 85982 23 0 0 25 0 1 0 485397835 17018880 3780 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4155 3780 603 41 0 4114 0 vsize: 16620 [startup+870.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4376 0 0 0 86982 23 0 0 25 0 1 0 485397835 17018880 3780 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4155 3780 603 41 0 4114 0 vsize: 16620 [startup+880.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4405 0 0 0 87982 23 0 0 25 0 1 0 485397835 17125376 3809 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4181 3809 603 41 0 4140 0 vsize: 16724 [startup+890.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4405 0 0 0 88982 23 0 0 25 0 1 0 485397835 17125376 3809 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4181 3809 603 41 0 4140 0 vsize: 16724 [startup+900.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 89982 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4279 3907 603 41 0 4238 0 vsize: 17116 [startup+910.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 90982 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4279 3907 603 41 0 4238 0 vsize: 17116 [startup+920.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 91983 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4279 3907 603 41 0 4238 0 vsize: 17116 [startup+930.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4761 0 0 0 92982 25 0 0 25 0 1 0 485397835 18579456 4164 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4536 4164 603 41 0 4495 0 vsize: 18144 [startup+940.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4793 0 0 0 93982 25 0 0 25 0 1 0 485397835 18710528 4196 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4568 4196 603 41 0 4527 0 vsize: 18272 [startup+950.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4793 0 0 0 94982 25 0 0 25 0 1 0 485397835 18710528 4196 4294967295 134512640 134672761 3221224528 3221223728 134610630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4568 4196 603 41 0 4527 0 vsize: 18272 [startup+960.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 95982 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4580 4208 603 41 0 4539 0 vsize: 18320 [startup+970.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 96982 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4580 4208 603 41 0 4539 0 vsize: 18320 [startup+980.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 97983 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134616017 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4580 4208 603 41 0 4539 0 vsize: 18320 [startup+990.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 98983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4588 4216 603 41 0 4547 0 vsize: 18352 [startup+1000 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 99983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4588 4216 603 41 0 4547 0 vsize: 18352 [startup+1010 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 100983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4588 4216 603 41 0 4547 0 vsize: 18352 [startup+1020 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4824 0 0 0 101983 25 0 0 25 0 1 0 485397835 18825216 4224 4294967295 134512640 134672761 3221224528 3221223712 134615945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4596 4224 603 41 0 4555 0 vsize: 18384 [startup+1030 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4824 0 0 0 102984 25 0 0 25 0 1 0 485397835 18825216 4224 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4596 4224 603 41 0 4555 0 vsize: 18384 [startup+1040 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4832 0 0 0 103984 25 0 0 25 0 1 0 485397835 18956288 4232 4294967295 134512640 134672761 3221224528 3221223568 134612478 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4628 4232 603 41 0 4587 0 vsize: 18512 [startup+1050 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4872 0 0 0 104984 25 0 0 25 0 1 0 485397835 19017728 4271 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4643 4271 603 41 0 4602 0 vsize: 18572 [startup+1060 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4872 0 0 0 105984 25 0 0 25 0 1 0 485397835 19017728 4271 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4643 4271 603 41 0 4602 0 vsize: 18572 [startup+1070 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 106984 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223712 134616023 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4647 4278 603 41 0 4606 0 vsize: 18588 [startup+1080 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 107984 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223568 134614268 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4647 4278 603 41 0 4606 0 vsize: 18588 [startup+1090 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 108985 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4647 4278 603 41 0 4606 0 vsize: 18588 [startup+1100 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 109985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4698 4328 603 41 0 4657 0 vsize: 18792 [startup+1110 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 110985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223568 134612966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4698 4328 603 41 0 4657 0 vsize: 18792 [startup+1120 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 111985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4698 4328 603 41 0 4657 0 vsize: 18792 [startup+1130 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 112985 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4706 4336 603 41 0 4665 0 vsize: 18824 [startup+1140 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 113985 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4706 4336 603 41 0 4665 0 vsize: 18824 [startup+1150 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 114986 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223664 134614756 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4706 4336 603 41 0 4665 0 vsize: 18824 [startup+1160 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5035 0 0 0 115985 25 0 0 25 0 1 0 485397835 19668992 4432 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4802 4432 603 41 0 4761 0 vsize: 19208 [startup+1170 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 116986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4843 4474 603 41 0 4802 0 vsize: 19372 [startup+1180 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 117986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4843 4474 603 41 0 4802 0 vsize: 19372 [startup+1190 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 118986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4843 4474 603 41 0 4802 0 vsize: 19372 [startup+1200 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27998 Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5125 0 0 0 119986 25 0 0 25 0 1 0 485397835 20029440 4520 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4890 4520 603 41 0 4849 0 vsize: 19560 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.02 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 27998 Raw data (stat): 27998 (minisat+) Z 27997 25347 25346 0 -1 12 5126 0 0 0 119986 26 0 0 25 0 1 0 485397835 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.02 CPU time (s): 1200.13 CPU user time (s): 1199.87 CPU system time (s): 0.268959 CPU usage (%): 100.01 Max. virtual memory (Kb): 19560 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####