Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb |
MD5SUM | 4df3e7eb358d27d446e34b975724a6c1 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -7772 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 60 |
Biggest coefficient in the objective function | 974 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 9460 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 6000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 26162 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01884 |
Number of variables | 60 |
Total number of constraints | 90 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 30 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 60 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-21 17:19:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17262 boxname=wulflinc7 idbench=1328 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4df3e7eb358d27d446e34b975724a6c1 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sentoy.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sentoy.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-sentoy.opb IDLAUNCH: 17262 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 767360 kB Buffers: 12100 kB Cached: 233756 kB SwapCached: 304 kB Active: 19472 kB Inactive: 228920 kB HighTotal: 131008 kB HighFree: 68684 kB LowTotal: 903652 kB LowFree: 698676 kB SwapTotal: 2097136 kB SwapFree: 2096520 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6448 kB Slab: 13272 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 17:39:04 (client local time) WITH STATUS 10 IN 1200.17 SECONDS stats: 17262 7 1200.17 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 30 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 29]---> Adder-cost: 448 maxlim: 11620 bits: 15/14 c ---[ 28]---> Adder-cost: 408 maxlim: 6087 bits: 14/13 c ---[ 27]---> Adder-cost: 432 maxlim: 9310 bits: 14/14 c ---[ 26]---> Adder-cost: 468 maxlim: 11096 bits: 15/14 c ---[ 25]---> Adder-cost: 444 maxlim: 10275 bits: 14/14 c ---[ 24]---> Adder-cost: 458 maxlim: 10302 bits: 14/14 c ---[ 23]---> Adder-cost: 436 maxlim: 13436 bits: 15/14 c ---[ 22]---> Adder-cost: 428 maxlim: 9755 bits: 14/14 c ---[ 21]---> Adder-cost: 412 maxlim: 6448 bits: 14/13 c ---[ 20]---> Adder-cost: 464 maxlim: 10002 bits: 14/14 c ---[ 19]---> Adder-cost: 426 maxlim: 9583 bits: 14/14 c ---[ 18]---> Adder-cost: 424 maxlim: 9848 bits: 14/14 c ---[ 17]---> Adder-cost: 364 maxlim: 5722 bits: 14/13 c ---[ 16]---> Adder-cost: 452 maxlim: 10594 bits: 15/14 c ---[ 15]---> Adder-cost: 434 maxlim: 10081 bits: 14/14 c ---[ 14]---> Adder-cost: 442 maxlim: 9196 bits: 14/14 c ---[ 13]---> Adder-cost: 456 maxlim: 12391 bits: 15/14 c ---[ 12]---> Adder-cost: 450 maxlim: 14161 bits: 15/14 c ---[ 11]---> Adder-cost: 418 maxlim: 12220 bits: 15/14 c ---[ 10]---> Adder-cost: 420 maxlim: 12782 bits: 15/14 c ---[ 9]---> Adder-cost: 460 maxlim: 11486 bits: 15/14 c ---[ 8]---> Adder-cost: 436 maxlim: 8903 bits: 14/14 c ---[ 7]---> Adder-cost: 456 maxlim: 10103 bits: 14/14 c ---[ 6]---> Adder-cost: 380 maxlim: 6238 bits: 14/13 c ---[ 5]---> Adder-cost: 430 maxlim: 10469 bits: 15/14 c ---[ 4]---> Adder-cost: 438 maxlim: 9149 bits: 14/14 c ---[ 3]---> Adder-cost: 420 maxlim: 13773 bits: 15/14 c ---[ 2]---> Adder-cost: 448 maxlim: 9436 bits: 14/14 c ---[ 1]---> Adder-cost: 456 maxlim: 8907 bits: 14/14 c ---[ 0]---> Adder-cost: 408 maxlim: 13608 bits: 15/14 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 89295 319020 | 26788 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/13035 c -- var.elim.: 2000/13035 c -- var.elim.: 3000/13035 c -- var.elim.: 4000/13035 c -- var.elim.: 5000/13035 c -- var.elim.: 6000/13035 c -- var.elim.: 7000/13035 c -- var.elim.: 8000/13035 c -- var.elim.: 9000/13035 c -- var.elim.: 10000/13035 c -- var.elim.: 11000/13035 c -- var.elim.: 12000/13035 c -- var.elim.: 13000/13035 c -- var.elim.: 13035/13035 c -- var.elim.: 929/929 c -- subsuming c -- var.elim.: 73/73 c -- var.elim.: 62/62 c | 0 | 88309 316345 | -- 0 -- -- | -- | -930/-2153 c | 0 | 88309 316345 | 35323 0 0 nan | 0.000 % | c | 100 | 88309 316345 | 38855 100 369 3.7 | 1.804 % | c | 251 | 88309 316345 | 42741 251 3460 13.8 | 1.804 % | c | 476 | 88309 316345 | 47015 476 10621 22.3 | 1.804 % | c | 814 | 88309 316345 | 51717 814 21788 26.8 | 1.804 % | c | 1324 | 88309 316345 | 56889 1324 36808 27.8 | 1.804 % | c ============================================================================== c (current CPU-time: 9.13361 s) c ============================================================================== c [1mFound solution: -2006[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6599 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1773 | 105307 356119 | 31592 1773 67382 38.0 | 1.804 % | c -- subsuming c -- var.elim.: 1000/5986 c -- var.elim.: 2000/5986 c -- var.elim.: 3000/5986 c -- var.elim.: 4000/5986 c -- var.elim.: 5000/5986 c -- var.elim.: 5986/5986 c -- var.elim.: 1000/3264 c -- var.elim.: 2000/3264 c -- var.elim.: 3000/3264 c -- var.elim.: 3264/3264 c -- var.elim.: 38/38 c -- subsuming c -- var.elim.: 348/348 c -- var.elim.: 49/49 c | 1773 | 103530 363482 | -- 1773 -- -- | -- | -1777/7364 c | 1773 | 103530 363482 | 41412 1773 67382 38.0 | 1.804 % | c | 1874 | 103530 363482 | 45553 1874 71653 38.2 | 1.452 % | c | 2024 | 103530 363482 | 50108 2024 73568 36.3 | 1.452 % | c | 2249 | 103530 363482 | 55119 2249 76069 33.8 | 1.452 % | c | 2587 | 103530 363482 | 60631 2587 83500 32.3 | 1.452 % | c | 3093 | 103530 363482 | 66694 3093 102146 33.0 | 1.452 % | c | 3853 | 103530 363482 | 73363 3853 128519 33.4 | 1.452 % | c | 4993 | 103530 363482 | 80700 4993 161353 32.3 | 1.452 % | c | 6702 | 103530 363482 | 88770 6702 198818 29.7 | 1.452 % | c ============================================================================== c (current CPU-time: 24.3253 s) c ============================================================================== c [1mFound solution: -2158[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6852 | 104283 365467 | 31284 6852 201770 29.4 | 1.452 % | c -- subsuming c -- var.elim.: 1000/1121 c -- var.elim.: 1121/1121 c -- var.elim.: 592/592 c -- subsuming c -- var.elim.: 250/250 c -- var.elim.: 10/10 c | 6852 | 103801 365032 | -- 6852 -- -- | -- | -482/-434 c | 6852 | 103801 365032 | 41520 6841 198475 29.0 | 1.452 % | c | 6952 | 103801 365032 | 45672 6941 199786 28.8 | 1.452 % | c | 7105 | 103801 365032 | 50239 7094 203436 28.7 | 1.452 % | c | 7330 | 103801 365032 | 55263 7319 209963 28.7 | 1.452 % | c | 7667 | 103801 365032 | 60790 7656 216113 28.2 | 1.452 % | c ============================================================================== c (current CPU-time: 27.3808 s) c ============================================================================== c [1mFound solution: -2583[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 7858 | 104137 366004 | 31241 7847 218517 27.8 | 1.452 % | c -- subsuming c -- var.elim.: 591/591 c -- var.elim.: 351/351 c -- subsuming c -- var.elim.: 114/114 c | 7858 | 103926 366384 | -- 7847 -- -- | -- | -211/381 c | 7858 | 103926 366384 | 41570 7847 218517 27.8 | 1.452 % | c | 7958 | 103926 366384 | 45727 7947 219607 27.6 | 1.455 % | c | 8108 | 103926 366384 | 50300 8097 220558 27.2 | 1.455 % | c | 8335 | 103926 366384 | 55330 8324 224027 26.9 | 1.455 % | c ============================================================================== c (current CPU-time: 29.3185 s) c ============================================================================== c [1mFound solution: -3152[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8487 | 104174 367172 | 31252 8476 231807 27.3 | 1.455 % | c -- subsuming c -- var.elim.: 502/502 c -- var.elim.: 303/303 c | 8487 | 103989 367513 | -- 8476 -- -- | -- | -185/342 c | 8487 | 103989 367513 | 41595 8476 231807 27.3 | 1.455 % | c | 8588 | 103989 367513 | 45755 8577 232969 27.2 | 1.460 % | c | 8738 | 103989 367513 | 50330 8727 234839 26.9 | 1.460 % | c | 8964 | 103989 367513 | 55363 8953 238681 26.7 | 1.460 % | c | 9304 | 103989 367513 | 60900 9293 298102 32.1 | 1.460 % | c | 9811 | 103989 367513 | 66990 9800 315134 32.2 | 1.460 % | c ============================================================================== c (current CPU-time: 37.0054 s) c ============================================================================== c [1mFound solution: -3229[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 10486 | 104110 367959 | 31232 10475 345237 33.0 | 1.460 % | c -- subsuming c -- var.elim.: 408/408 c -- var.elim.: 220/220 c | 10486 | 104017 368314 | -- 10475 -- -- | -- | -93/356 c | 10486 | 104017 368314 | 41606 10475 345237 33.0 | 1.460 % | c | 10587 | 104017 368314 | 45767 10576 347071 32.8 | 1.466 % | c | 10737 | 104017 368314 | 50344 10726 352783 32.9 | 1.466 % | c | 10964 | 104017 368314 | 55378 10953 356565 32.6 | 1.466 % | c | 11302 | 104017 368314 | 60916 11291 367369 32.5 | 1.466 % | c ============================================================================== c (current CPU-time: 41.6907 s) c ============================================================================== c [1mFound solution: -4106[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 11647 | 104338 369233 | 31301 11636 375565 32.3 | 1.466 % | c -- subsuming c -- var.elim.: 634/634 c -- var.elim.: 317/317 c | 11647 | 104136 369499 | -- 11636 -- -- | -- | -202/267 c | 11647 | 104136 369499 | 41654 11636 375565 32.3 | 1.466 % | c | 11748 | 104136 369499 | 45819 11737 377542 32.2 | 1.469 % | c | 11898 | 104136 369499 | 50401 11887 380367 32.0 | 1.469 % | c | 12123 | 104136 369499 | 55442 12112 392140 32.4 | 1.469 % | c | 12460 | 104136 369499 | 60986 12449 400637 32.2 | 1.469 % | c | 12966 | 104136 369499 | 67084 12955 417926 32.3 | 1.469 % | c | 13727 | 104136 369499 | 73793 13716 456875 33.3 | 1.469 % | c | 14866 | 104136 369499 | 81172 14855 511016 34.4 | 1.469 % | c | 16575 | 104136 369499 | 89289 16564 694292 41.9 | 1.469 % | c | 19139 | 104136 369499 | 98218 19128 830745 43.4 | 1.469 % | c ============================================================================== c (current CPU-time: 93.6608 s) c ============================================================================== c [1mFound solution: -4188[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 22231 | 104247 369922 | 31274 22220 1194376 53.8 | 1.469 % | c -- subsuming c -- var.elim.: 385/385 c -- var.elim.: 219/219 c | 22231 | 104166 370266 | -- 22220 -- -- | -- | -81/345 c | 22231 | 104166 370266 | 41666 22220 1194376 53.8 | 1.469 % | c | 22331 | 104166 370266 | 45833 22320 1197791 53.7 | 1.475 % | c | 22481 | 104166 370266 | 50416 22470 1203038 53.5 | 1.475 % | c | 22708 | 104166 370266 | 55457 22697 1210443 53.3 | 1.475 % | c | 23045 | 104166 370266 | 61003 23034 1220687 53.0 | 1.475 % | c | 23553 | 104166 370266 | 67104 23542 1250286 53.1 | 1.475 % | c ============================================================================== c (current CPU-time: 101.58 s) c ============================================================================== c [1mFound solution: -4422[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 23993 | 104254 370601 | 31276 23982 1290222 53.8 | 1.475 % | c -- subsuming c -- var.elim.: 289/289 c -- var.elim.: 178/178 c | 23993 | 104193 370882 | -- 23982 -- -- | -- | -61/282 c | 23993 | 104193 370882 | 41677 23941 1273306 53.2 | 1.475 % | c | 24094 | 104193 370882 | 45844 24042 1275192 53.0 | 1.481 % | c | 24244 | 104193 370882 | 50429 24192 1277041 52.8 | 1.481 % | c | 24469 | 104193 370882 | 55472 24417 1283698 52.6 | 1.481 % | c | 24808 | 104193 370882 | 61019 24756 1304176 52.7 | 1.481 % | c | 25314 | 104193 370882 | 67121 25262 1317879 52.2 | 1.481 % | c | 26074 | 104193 370882 | 73833 26022 1399828 53.8 | 1.481 % | c | 27214 | 104193 370882 | 81217 27162 1447698 53.3 | 1.481 % | c ============================================================================== c (current CPU-time: 124.658 s) c ============================================================================== c [1mFound solution: -4446[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 28661 | 104285 371251 | 31285 28609 1654001 57.8 | 1.481 % | c -- subsuming c -- var.elim.: 271/271 c -- var.elim.: 197/197 c | 28661 | 104219 371749 | -- 28609 -- -- | -- | -66/499 c | 28661 | 104219 371749 | 41687 28609 1654001 57.8 | 1.481 % | c | 28762 | 104219 371749 | 45856 28710 1656911 57.7 | 1.487 % | c | 28912 | 104219 371749 | 50441 28860 1659394 57.5 | 1.487 % | c | 29139 | 104219 371749 | 55486 29087 1677989 57.7 | 1.487 % | c | 29477 | 104219 371749 | 61034 29425 1692438 57.5 | 1.487 % | c | 29984 | 104219 371749 | 67138 29932 1742034 58.2 | 1.487 % | c | 30747 | 104219 371749 | 73852 30695 1805226 58.8 | 1.487 % | c | 31887 | 104219 371749 | 81237 31835 1844363 57.9 | 1.487 % | c | 33595 | 104219 371749 | 89361 33543 1918654 57.2 | 1.487 % | c | 36158 | 104219 371749 | 98297 36106 2103147 58.2 | 1.487 % | c | 40002 | 104219 371749 | 108126 39950 2596544 65.0 | 1.487 % | c | 45768 | 104219 371749 | 118939 45716 2991024 65.4 | 1.487 % | c ============================================================================== c (current CPU-time: 252.726 s) c ============================================================================== c [1mFound solution: -5328[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 47845 | 104430 372422 | 31328 47793 3141612 65.7 | 1.487 % | c -- subsuming c -- var.elim.: 483/483 c -- var.elim.: 266/266 c | 47845 | 104270 372587 | -- 47793 -- -- | -- | -160/166 c | 47845 | 104270 372587 | 41708 47793 3141612 65.7 | 1.487 % | c | 47945 | 104270 372587 | 45878 13966 1048197 75.1 | 1.492 % | c | 48095 | 104270 372587 | 50466 14116 1053015 74.6 | 1.492 % | c | 48320 | 104270 372587 | 55513 14341 1084860 75.6 | 1.492 % | c | 48658 | 104270 372587 | 61064 14679 1093240 74.5 | 1.492 % | c | 49164 | 104270 372587 | 67171 15185 1113745 73.3 | 1.492 % | c | 49923 | 104270 372587 | 73888 15944 1138904 71.4 | 1.492 % | c | 51062 | 104270 372587 | 81277 17083 1297848 76.0 | 1.492 % | c | 52771 | 104270 372587 | 89404 18792 1394231 74.2 | 1.492 % | c | 55333 | 104270 372587 | 98345 21354 1717863 80.4 | 1.492 % | c | 59177 | 104259 372550 | 108168 25197 1891459 75.1 | 1.498 % | c | 64945 | 104259 372550 | 118985 30965 2254232 72.8 | 1.498 % | c | 73595 | 104259 372550 | 130883 39615 3328663 84.0 | 1.498 % | c | 86569 | 104259 372550 | 143972 52589 4266909 81.1 | 1.498 % | c ============================================================================== c (current CPU-time: 437.482 s) c ============================================================================== c [1mFound solution: -6113[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 93979 | 104334 372811 | 31300 59999 5021871 83.7 | 1.498 % | c -- subsuming c -- var.elim.: 297/297 c -- var.elim.: 124/124 c | 93979 | 104286 372987 | -- 59999 -- -- | -- | -48/177 c | 93979 | 104286 372987 | 41714 59999 5021871 83.7 | 1.498 % | c | 94079 | 104286 372987 | 45885 15603 1161399 74.4 | 1.503 % | c | 94231 | 104286 372987 | 50474 15755 1168678 74.2 | 1.503 % | c | 94456 | 104286 372987 | 55521 15980 1170733 73.3 | 1.503 % | c | 94794 | 104286 372987 | 61074 16318 1199008 73.5 | 1.503 % | c | 95301 | 104286 372987 | 67181 16825 1213582 72.1 | 1.503 % | c | 96060 | 104286 372987 | 73899 17584 1269827 72.2 | 1.503 % | c ============================================================================== c (current CPU-time: 447.783 s) c ============================================================================== c [1mFound solution: -6408[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 96526 | 104334 373126 | 31300 18050 1310090 72.6 | 1.503 % | c -- subsuming c -- var.elim.: 145/145 c -- var.elim.: 53/53 c | 96526 | 104306 373117 | -- 18050 -- -- | -- | -28/-8 c | 96526 | 104306 373117 | 41722 18050 1310090 72.6 | 1.503 % | c | 96627 | 104306 373117 | 45894 18151 1313743 72.4 | 1.509 % | c | 96778 | 104306 373117 | 50484 18302 1327316 72.5 | 1.509 % | c | 97005 | 104306 373117 | 55532 18529 1331596 71.9 | 1.509 % | c | 97343 | 104306 373117 | 61085 18867 1338522 70.9 | 1.509 % | c | 97853 | 104306 373117 | 67194 19377 1379865 71.2 | 1.509 % | c | 98615 | 104306 373117 | 73913 20139 1411311 70.1 | 1.509 % | c | 99754 | 104306 373117 | 81305 21278 1553274 73.0 | 1.509 % | c | 101462 | 104306 373117 | 89435 22986 1653911 72.0 | 1.509 % | c | 104024 | 104306 373117 | 98379 25548 1885591 73.8 | 1.509 % | c | 107868 | 104306 373117 | 108217 29392 2222881 75.6 | 1.509 % | c | 113634 | 104306 373117 | 119038 35158 3170214 90.2 | 1.509 % | c | 122283 | 104306 373117 | 130942 43807 4917619 112.3 | 1.509 % | c | 135258 | 104306 373117 | 144037 56782 6944932 122.3 | 1.509 % | c | 154719 | 104306 373117 | 158440 76243 8919404 117.0 | 1.509 % | c | 183911 | 104306 373117 | 174284 105435 14215881 134.8 | 1.509 % | c c *** TERMINATE#### 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.77 0.91 0.90 2/54 12170 Raw data (stat): 12170 (runsolver) R 12169 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488608503 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.81 0.92 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 4978 0 0 0 982 15 0 0 25 0 1 0 488608503 20520960 4147 4294967295 134512640 134672761 3221224544 3221222992 134606665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5010 4147 603 41 0 4969 0 vsize: 20040 [startup+19.9998 s] Raw data (loadavg): 0.84 0.92 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 5242 0 0 0 1980 16 0 0 25 0 1 0 488608503 20758528 4202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5068 4202 603 41 0 5027 0 vsize: 20272 [startup+30.0055 s] Raw data (loadavg): 0.86 0.92 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 7556 0 0 0 2972 24 0 0 25 0 1 0 488608503 22962176 4765 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5606 4765 603 41 0 5565 0 vsize: 22424 [startup+40.0054 s] Raw data (loadavg): 0.88 0.92 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8151 0 0 0 3969 26 0 0 25 0 1 0 488608503 23891968 4939 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5833 4939 603 41 0 5792 0 vsize: 23332 [startup+50.0046 s] Raw data (loadavg): 0.90 0.92 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8810 0 0 0 4966 29 0 0 25 0 1 0 488608503 24162304 4992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5899 4992 603 41 0 5858 0 vsize: 23596 [startup+60.0046 s] Raw data (loadavg): 0.91 0.93 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8810 0 0 0 5966 29 0 0 25 0 1 0 488608503 24162304 4992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5899 4992 603 41 0 5858 0 vsize: 23596 [startup+70.0053 s] Raw data (loadavg): 0.93 0.93 0.90 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8845 0 0 0 6966 29 0 0 25 0 1 0 488608503 24162304 5027 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5899 5027 603 41 0 5858 0 vsize: 23596 [startup+80.0055 s] Raw data (loadavg): 0.94 0.93 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 9018 0 0 0 7966 30 0 0 25 0 1 0 488608503 24821760 5200 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6060 5200 603 41 0 6019 0 vsize: 24240 [startup+90.0055 s] Raw data (loadavg): 0.95 0.93 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 9251 0 0 0 8965 30 0 0 25 0 1 0 488608503 25751552 5433 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6287 5433 603 41 0 6246 0 vsize: 25148 [startup+100.005 s] Raw data (loadavg): 0.95 0.93 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10189 0 0 0 9960 34 0 0 25 0 1 0 488608503 27897856 5923 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6811 5923 603 41 0 6770 0 vsize: 27244 [startup+110.006 s] Raw data (loadavg): 0.96 0.93 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10793 0 0 0 10958 36 0 0 25 0 1 0 488608503 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6975 6100 603 41 0 6934 0 vsize: 27900 [startup+120.005 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10793 0 0 0 11957 36 0 0 25 0 1 0 488608503 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6975 6100 603 41 0 6934 0 vsize: 27900 [startup+130.006 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11620 0 0 0 12954 39 0 0 25 0 1 0 488608503 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7367 6462 603 41 0 7326 0 vsize: 29468 [startup+140.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11620 0 0 0 13954 39 0 0 25 0 1 0 488608503 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7367 6462 603 41 0 7326 0 vsize: 29468 [startup+150.006 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11701 0 0 0 14954 39 0 0 25 0 1 0 488608503 30306304 6543 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7399 6543 603 41 0 7358 0 vsize: 29596 [startup+160.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11903 0 0 0 15954 40 0 0 25 0 1 0 488608503 31100928 6745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7593 6745 603 41 0 7552 0 vsize: 30372 [startup+170.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12068 0 0 0 16953 41 0 0 25 0 1 0 488608503 31760384 6910 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7754 6910 603 41 0 7713 0 vsize: 31016 [startup+180.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12213 0 0 0 17953 41 0 0 25 0 1 0 488608503 32411648 7055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7913 7055 603 41 0 7872 0 vsize: 31652 [startup+190.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12361 0 0 0 18952 42 0 0 25 0 1 0 488608503 33071104 7203 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8074 7203 603 41 0 8033 0 vsize: 32296 [startup+200.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12486 0 0 0 19952 42 0 0 25 0 1 0 488608503 33472512 7328 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8172 7328 603 41 0 8131 0 vsize: 32688 [startup+210.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12582 0 0 0 20952 43 0 0 25 0 1 0 488608503 33873920 7424 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8270 7424 603 41 0 8229 0 vsize: 33080 [startup+220.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12673 0 0 0 21952 43 0 0 25 0 1 0 488608503 34271232 7515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8367 7515 603 41 0 8326 0 vsize: 33468 [startup+230.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12788 0 0 0 22952 43 0 0 25 0 1 0 488608503 34803712 7630 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8497 7630 603 41 0 8456 0 vsize: 33988 [startup+240.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12907 0 0 0 23952 43 0 0 25 0 1 0 488608503 35209216 7749 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8596 7749 603 41 0 8555 0 vsize: 34384 [startup+250.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12996 0 0 0 24952 44 0 0 25 0 1 0 488608503 35602432 7838 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8692 7838 603 41 0 8651 0 vsize: 34768 [startup+260.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 25949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223532 1075347104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+270.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 26949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+280.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 27949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223744 134610703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+290.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 28949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+300.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 29949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+310.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 30949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+320.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 31949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+330.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 32949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+340.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 33949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+350.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 34949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+360.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 35950 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8217 603 41 0 9062 0 vsize: 36412 [startup+370.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13890 0 0 0 36950 47 0 0 25 0 1 0 488608503 37416960 8282 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9135 8282 603 41 0 9094 0 vsize: 36540 [startup+380.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14049 0 0 0 37949 47 0 0 25 0 1 0 488608503 38072320 8441 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9295 8441 603 41 0 9254 0 vsize: 37180 [startup+390.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14405 0 0 0 38948 49 0 0 25 0 1 0 488608503 39542784 8797 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9654 8797 603 41 0 9613 0 vsize: 38616 [startup+400.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14651 0 0 0 39947 50 0 0 25 0 1 0 488608503 40464384 9043 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9879 9043 603 41 0 9838 0 vsize: 39516 [startup+410.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14830 0 0 0 40947 50 0 0 25 0 1 0 488608503 41254912 9222 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10072 9222 603 41 0 10031 0 vsize: 40288 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 15148 0 0 0 41946 51 0 0 25 0 1 0 488608503 42569728 9540 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10393 9540 603 41 0 10352 0 vsize: 41572 [startup+430.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 15478 0 0 0 42945 52 0 0 25 0 1 0 488608503 43896832 9870 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10717 9870 603 41 0 10676 0 vsize: 42868 [startup+440.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 16461 0 0 0 43942 55 0 0 25 0 1 0 488608503 46182400 10401 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11275 10401 603 41 0 11234 0 vsize: 45100 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 44940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+460.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 45940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+470.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 46940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+480.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 47940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+490.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 48940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+500.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 49940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+510.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 50941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 51941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 52941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+540.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 53941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+550.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 54941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+560.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 55942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 56942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+580.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 57942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+590.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 58942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+600.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 59942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+610.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 60943 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134612777 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+620.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 61943 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11131 10296 603 41 0 11090 0 vsize: 44524 [startup+630.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17177 0 0 0 62943 58 0 0 25 0 1 0 488608503 45858816 10338 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11196 10338 603 41 0 11155 0 vsize: 44784 [startup+640.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17431 0 0 0 63942 58 0 0 25 0 1 0 488608503 46776320 10592 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11420 10592 603 41 0 11379 0 vsize: 45680 [startup+650.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17730 0 0 0 64941 59 0 0 25 0 1 0 488608503 48099328 10891 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11743 10891 603 41 0 11702 0 vsize: 46972 [startup+660.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17916 0 0 0 65941 60 0 0 25 0 1 0 488608503 48885760 11077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11935 11077 603 41 0 11894 0 vsize: 47740 [startup+670.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18157 0 0 0 66941 60 0 0 25 0 1 0 488608503 49799168 11318 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12158 11318 603 41 0 12117 0 vsize: 48632 [startup+680.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18401 0 0 0 67940 61 0 0 25 0 1 0 488608503 50843648 11562 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12413 11562 603 41 0 12372 0 vsize: 49652 [startup+690.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18667 0 0 0 68940 62 0 0 25 0 1 0 488608503 51888128 11828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12668 11828 603 41 0 12627 0 vsize: 50672 [startup+700.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18940 0 0 0 69939 63 0 0 25 0 1 0 488608503 53075968 12101 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12958 12101 603 41 0 12917 0 vsize: 51832 [startup+710.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19170 0 0 0 70939 63 0 0 25 0 1 0 488608503 54001664 12331 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13184 12331 603 41 0 13143 0 vsize: 52736 [startup+720.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19356 0 0 0 71938 64 0 0 25 0 1 0 488608503 54665216 12517 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13346 12517 603 41 0 13305 0 vsize: 53384 [startup+730.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19553 0 0 0 72938 65 0 0 25 0 1 0 488608503 55590912 12714 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13572 12714 603 41 0 13531 0 vsize: 54288 [startup+740.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19812 0 0 0 73937 66 0 0 25 0 1 0 488608503 56901632 12973 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13892 12973 603 41 0 13851 0 vsize: 55568 [startup+750.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20068 0 0 0 74936 67 0 0 25 0 1 0 488608503 57946112 13229 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14147 13229 603 41 0 14106 0 vsize: 56588 [startup+760.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20247 0 0 0 75935 68 0 0 25 0 1 0 488608503 58609664 13408 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14309 13408 603 41 0 14268 0 vsize: 57236 [startup+770.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20467 0 0 0 76934 69 0 0 25 0 1 0 488608503 59527168 13628 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14533 13628 603 41 0 14492 0 vsize: 58132 [startup+780.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20701 0 0 0 77934 70 0 0 25 0 1 0 488608503 60444672 13862 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14757 13862 603 41 0 14716 0 vsize: 59028 [startup+790.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20922 0 0 0 78933 70 0 0 25 0 1 0 488608503 61374464 14083 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14984 14083 603 41 0 14943 0 vsize: 59936 [startup+800.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21115 0 0 0 79933 71 0 0 25 0 1 0 488608503 62173184 14276 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15179 14276 603 41 0 15138 0 vsize: 60716 [startup+810.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21355 0 0 0 80932 72 0 0 25 0 1 0 488608503 63107072 14516 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15407 14516 603 41 0 15366 0 vsize: 61628 [startup+820.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21541 0 0 0 81932 72 0 0 25 0 1 0 488608503 63897600 14702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15600 14702 603 41 0 15559 0 vsize: 62400 [startup+830.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21719 0 0 0 82932 72 0 0 25 0 1 0 488608503 64561152 14880 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15762 14880 603 41 0 15721 0 vsize: 63048 [startup+840.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21932 0 0 0 83932 73 0 0 25 0 1 0 488608503 65478656 15093 4294967295 134512640 134672761 3221224544 3221223584 134613025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15986 15093 603 41 0 15945 0 vsize: 63944 [startup+850.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22215 0 0 0 84931 74 0 0 25 0 1 0 488608503 66658304 15376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16274 15376 603 41 0 16233 0 vsize: 65096 [startup+860.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22417 0 0 0 85930 74 0 0 25 0 1 0 488608503 67461120 15578 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16470 15578 603 41 0 16429 0 vsize: 65880 [startup+870.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22669 0 0 0 86930 75 0 0 25 0 1 0 488608503 68509696 15830 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16726 15830 603 41 0 16685 0 vsize: 66904 [startup+880.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22863 0 0 0 87929 76 0 0 25 0 1 0 488608503 69296128 16024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16918 16024 603 41 0 16877 0 vsize: 67672 [startup+890.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23065 0 0 0 88929 77 0 0 25 0 1 0 488608503 70086656 16226 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17111 16226 603 41 0 17070 0 vsize: 68444 [startup+900.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23223 0 0 0 89928 77 0 0 25 0 1 0 488608503 70742016 16384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17271 16384 603 41 0 17230 0 vsize: 69084 [startup+910.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23523 0 0 0 90928 78 0 0 25 0 1 0 488608503 71925760 16684 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17560 16684 603 41 0 17519 0 vsize: 70240 [startup+920.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23754 0 0 0 91927 79 0 0 25 0 1 0 488608503 72855552 16915 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17787 16915 603 41 0 17746 0 vsize: 71148 [startup+930.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23953 0 0 0 92927 79 0 0 25 0 1 0 488608503 73781248 17114 4294967295 134512640 134672761 3221224544 3221223348 1075358820 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18013 17114 603 41 0 17972 0 vsize: 72052 [startup+940.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24113 0 0 0 93927 79 0 0 25 0 1 0 488608503 74305536 17274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18141 17274 603 41 0 18100 0 vsize: 72564 [startup+950.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24293 0 0 0 94927 80 0 0 25 0 1 0 488608503 75091968 17454 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18333 17454 603 41 0 18292 0 vsize: 73332 [startup+960.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24522 0 0 0 95926 80 0 0 25 0 1 0 488608503 76013568 17683 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18558 17683 603 41 0 18517 0 vsize: 74232 [startup+970.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24773 0 0 0 96926 81 0 0 25 0 1 0 488608503 77070336 17934 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18816 17934 603 41 0 18775 0 vsize: 75264 [startup+980.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25024 0 0 0 97926 81 0 0 25 0 1 0 488608503 78123008 18185 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19073 18185 603 41 0 19032 0 vsize: 76292 [startup+990.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25225 0 0 0 98926 82 0 0 25 0 1 0 488608503 78921728 18386 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19268 18386 603 41 0 19227 0 vsize: 77072 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25420 0 0 0 99925 82 0 0 25 0 1 0 488608503 79712256 18581 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19461 18581 603 41 0 19420 0 vsize: 77844 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25620 0 0 0 100924 83 0 0 25 0 1 0 488608503 80502784 18781 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19654 18781 603 41 0 19613 0 vsize: 78616 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25826 0 0 0 101924 84 0 0 25 0 1 0 488608503 81420288 18987 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19878 18987 603 41 0 19837 0 vsize: 79512 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26053 0 0 0 102923 85 0 0 25 0 1 0 488608503 82333696 19214 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20101 19214 603 41 0 20060 0 vsize: 80404 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26368 0 0 0 103922 86 0 0 25 0 1 0 488608503 83542016 19529 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20396 19529 603 41 0 20355 0 vsize: 81584 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26615 0 0 0 104922 86 0 0 25 0 1 0 488608503 84590592 19776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20652 19776 603 41 0 20611 0 vsize: 82608 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26782 0 0 0 105922 87 0 0 25 0 1 0 488608503 85254144 19943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20814 19943 603 41 0 20773 0 vsize: 83256 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27017 0 0 0 106921 88 0 0 25 0 1 0 488608503 86179840 20178 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21040 20178 603 41 0 20999 0 vsize: 84160 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27212 0 0 0 107921 88 0 0 25 0 1 0 488608503 86978560 20373 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21235 20373 603 41 0 21194 0 vsize: 84940 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27370 0 0 0 108920 89 0 0 25 0 1 0 488608503 87646208 20531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21398 20531 603 41 0 21357 0 vsize: 85592 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27513 0 0 0 109920 90 0 0 25 0 1 0 488608503 88301568 20674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21558 20674 603 41 0 21517 0 vsize: 86232 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27715 0 0 0 110920 90 0 0 25 0 1 0 488608503 89096192 20876 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21752 20876 603 41 0 21711 0 vsize: 87008 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27888 0 0 0 111919 91 0 0 25 0 1 0 488608503 89755648 21049 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21913 21049 603 41 0 21872 0 vsize: 87652 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28032 0 0 0 112919 91 0 0 25 0 1 0 488608503 90423296 21193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22076 21193 603 41 0 22035 0 vsize: 88304 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28158 0 0 0 113918 92 0 0 25 0 1 0 488608503 90816512 21319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22172 21319 603 41 0 22131 0 vsize: 88688 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28288 0 0 0 114918 93 0 0 25 0 1 0 488608503 91340800 21449 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22300 21449 603 41 0 22259 0 vsize: 89200 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28422 0 0 0 115918 93 0 0 25 0 1 0 488608503 92000256 21583 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22461 21583 603 41 0 22420 0 vsize: 89844 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28599 0 0 0 116918 93 0 0 25 0 1 0 488608503 92663808 21760 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22623 21760 603 41 0 22582 0 vsize: 90492 [startup+1180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28823 0 0 0 117917 94 0 0 25 0 1 0 488608503 94109696 21984 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22976 21984 603 41 0 22935 0 vsize: 91904 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 29025 0 0 0 118916 95 0 0 25 0 1 0 488608503 94924800 22186 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23175 22186 603 41 0 23134 0 vsize: 92700 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12170 Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 29191 0 0 0 119916 96 0 0 25 0 1 0 488608503 95584256 22352 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23336 22352 603 41 0 23295 0 vsize: 93344 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 12170 Raw data (stat): 12170 (minisat+) Z 12169 22932 22931 0 -1 12 29192 0 0 0 119916 100 0 0 25 0 1 0 488608503 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.06 CPU time (s): 1200.17 CPU user time (s): 1199.16 CPU system time (s): 1.00485 CPU usage (%): 100.009 Max. virtual memory (Kb): 93344 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####