Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02084 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-04-21 18:39:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17131 boxname=wulflinc3 idbench=1318 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0282.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0282.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-p0282.opb IDLAUNCH: 17131 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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.190 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: 696912 kB Buffers: 30500 kB Cached: 285020 kB SwapCached: 0 kB Active: 54980 kB Inactive: 263364 kB HighTotal: 131008 kB HighFree: 51380 kB LowTotal: 903652 kB LowFree: 645532 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6844 kB Slab: 13740 kB Committed_AS: 71788 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 18:59:13 (client local time) WITH STATUS 10 IN 1200.2 SECONDS stats: 17131 7 1200.2 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 221 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss................................................................................................................................................................................. c ---[ 223]---> Adder-cost: 124 maxlim: 245 bits: 9/8 c ---[ 222]---> Adder-cost: 104 maxlim: 265 bits: 10/9 c ---[ 221]---> Adder-cost: 126 maxlim: 182 bits: 9/8 c ---[ 220]---> Adder-cost: 98 maxlim: 202 bits: 9/8 c ---[ 219]---> Adder-cost: 114 maxlim: 168 bits: 9/8 c ---[ 218]---> Adder-cost: 100 maxlim: 188 bits: 9/8 c ---[ 217]---> Adder-cost: 98 maxlim: 192 bits: 9/8 c ---[ 216]---> Adder-cost: 98 maxlim: 212 bits: 9/8 c ---[ 215]---> Adder-cost: 106 maxlim: 178 bits: 9/8 c ---[ 214]---> Adder-cost: 98 maxlim: 198 bits: 9/8 c ---[ 213]---> Adder-cost: 127 maxlim: 321 bits: 10/9 c ---[ 211]---> Adder-cost: 115 maxlim: 341 bits: 10/9 c ---[ 209]---> Adder-cost: 112 maxlim: 529 bits: 10/10 c ---[ 208]---> Adder-cost: 98 maxlim: 249 bits: 9/8 c ---[ 207]---> Adder-cost: 108 maxlim: 198 bits: 9/8 c ---[ 206]---> Adder-cost: 104 maxlim: 218 bits: 9/8 c ---[ 205]---> Adder-cost: 100 maxlim: 155 bits: 9/8 c ---[ 204]---> Adder-cost: 98 maxlim: 175 bits: 9/8 c ---[ 203]---> Adder-cost: 104 maxlim: 118 bits: 8/7 c ---[ 202]---> Adder-cost: 98 maxlim: 138 bits: 9/8 c ---[ 201]---> Adder-cost: 104 maxlim: 267 bits: 10/9 c ---[ 199]---> Adder-cost: 98 maxlim: 204 bits: 9/8 c ---[ 198]---> Adder-cost: 98 maxlim: 224 bits: 9/8 c ---[ 197]---> Adder-cost: 96 maxlim: 167 bits: 9/8 c ---[ 196]---> Adder-cost: 102 maxlim: 187 bits: 9/8 c ---[ 195]---> Adder-cost: 106 maxlim: 234 bits: 9/8 c ---[ 194]---> Adder-cost: 100 maxlim: 254 bits: 9/8 c ---[ 193]---> Adder-cost: 100 maxlim: 442 bits: 10/9 c ---[ 192]---> Adder-cost: 110 maxlim: 182 bits: 9/8 c ---[ 191]---> Adder-cost: 119 maxlim: 401 bits: 10/9 c ---[ 190]---> Adder-cost: 117 maxlim: 141 bits: 9/8 c ---[ 189]---> Adder-cost: 115 maxlim: 421 bits: 10/9 c ---[ 188]---> Adder-cost: 117 maxlim: 161 bits: 9/8 c ---[ 187]---> Adder-cost: 112 maxlim: 55 bits: 7/6 c ---[ 186]---> Adder-cost: 20 maxlim: 9 bits: 5/4 c ---[ 185]---> Adder-cost: 112 maxlim: 55 bits: 7/6 c ---[ 184]---> Adder-cost: 112 maxlim: 55 bits: 7/6 c ---[ 183]---> Adder-cost: 31 maxlim: 15 bits: 5/4 c ---[ 182]---> Adder-cost: 52 maxlim: 25 bits: 6/5 c ---[ 181]---> Adder-cost: 15 maxlim: 7 bits: 4/3 c ---[ 180]---> Adder-cost: 7 maxlim: 3 bits: 3/2 c ---[ 2]---> Adder-cost: 83 maxlim: 61 bits: 7/6 c ---[ 1]---> Adder-cost: 81 maxlim: 81 bits: 8/7 c ---[ 0]---> Adder-cost: 21 maxlim: 7 bits: 4/3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 27042 96123 | 9014 0 0 nan | 0.000 % | c | 100 | 27042 96123 | 9915 100 368 3.7 | 4.011 % | c | 251 | 27042 96123 | 10906 251 2323 9.3 | 4.011 % | c | 477 | 27042 96123 | 11997 477 5125 10.7 | 4.011 % | c | 816 | 27042 96123 | 13197 816 9603 11.8 | 4.011 % | c | 1322 | 27042 96123 | 14517 1322 17051 12.9 | 4.011 % | c | 2082 | 27042 96123 | 15968 2082 27819 13.4 | 4.012 % | c ============================================================================== c [1mFound solution: 530574[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2436 maxlim: 772041 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2861 | 44003 156729 | 14667 2861 38547 13.5 | 4.012 % | c | 2963 | 44003 156729 | 16133 2963 39359 13.3 | 2.778 % | c | 3113 | 44003 156729 | 17747 3113 41738 13.4 | 2.778 % | c | 3338 | 44003 156729 | 19521 3338 44844 13.4 | 2.778 % | c | 3675 | 44003 156729 | 21473 3675 49558 13.5 | 2.778 % | c | 4182 | 44003 156729 | 23621 4182 57396 13.7 | 2.778 % | c ============================================================================== c [1mFound solution: 495924[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 806691 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4705 | 44018 156848 | 14672 4705 65230 13.9 | 2.778 % | c | 4805 | 44018 156848 | 16139 4805 66630 13.9 | 2.889 % | c | 4955 | 44018 156848 | 17753 4955 68220 13.8 | 2.889 % | c | 5181 | 44018 156848 | 19528 5181 71423 13.8 | 2.889 % | c | 5518 | 44018 156848 | 21481 5518 78404 14.2 | 2.889 % | c | 6024 | 44018 156848 | 23629 6024 83049 13.8 | 2.889 % | c | 6783 | 44018 156848 | 25992 6783 95959 14.1 | 2.889 % | c | 7923 | 44018 156848 | 28591 7923 111884 14.1 | 2.889 % | c | 9632 | 44018 156848 | 31450 9632 165118 17.1 | 2.889 % | c | 12197 | 44018 156848 | 34595 12197 226674 18.6 | 2.889 % | c | 16041 | 44018 156848 | 38055 16041 388131 24.2 | 2.889 % | c | 21808 | 44018 156848 | 41860 21808 728993 33.4 | 2.889 % | c ============================================================================== c [1mFound solution: 471827[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 830788 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23958 | 44040 157011 | 14680 23958 760593 31.7 | 2.889 % | c | 24058 | 44040 157011 | 16148 12079 471606 39.0 | 2.998 % | c | 24208 | 44040 157011 | 17762 12229 472810 38.7 | 2.998 % | c | 24433 | 44040 157011 | 19539 12454 475232 38.2 | 2.998 % | c | 24771 | 44040 157011 | 21492 12792 478852 37.4 | 2.998 % | c | 25277 | 44040 157011 | 23642 13298 487049 36.6 | 2.998 % | c | 26036 | 44040 157011 | 26006 14057 525090 37.4 | 2.998 % | c | 27175 | 44040 157011 | 28607 15196 557070 36.7 | 2.998 % | c | 28885 | 44040 157011 | 31467 16906 604692 35.8 | 2.998 % | c | 31447 | 44040 157011 | 34614 19468 657782 33.8 | 2.998 % | c | 35291 | 44040 157011 | 38076 23312 941858 40.4 | 2.998 % | c | 41059 | 44040 157011 | 41883 29080 1285083 44.2 | 2.998 % | c | 49709 | 44040 157011 | 46072 37730 1885618 50.0 | 2.998 % | c | 62683 | 44040 157011 | 50679 17242 857024 49.7 | 2.998 % | c | 82144 | 44040 157011 | 55747 36703 1910978 52.1 | 2.998 % | c | 111336 | 44040 157011 | 61322 24666 1025240 41.6 | 2.998 % | c ============================================================================== c [1mFound solution: 471639[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 830976 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 147661 | 44043 157048 | 14681 60991 4210897 69.0 | 2.998 % | c | 147761 | 44043 157048 | 16149 14692 1336667 91.0 | 3.026 % | c | 147911 | 44043 157048 | 17764 14842 1338047 90.2 | 3.026 % | c | 148136 | 44043 157048 | 19540 15067 1340176 88.9 | 3.026 % | c | 148475 | 44043 157048 | 21494 15406 1344108 87.2 | 3.026 % | c | 148981 | 44043 157048 | 23643 15912 1350334 84.9 | 3.026 % | c | 149740 | 44043 157048 | 26008 16671 1367099 82.0 | 3.026 % | c | 150879 | 44037 157031 | 28609 17809 1380340 77.5 | 3.040 % | c | 152587 | 44037 157031 | 31470 19517 1422609 72.9 | 3.040 % | c | 155150 | 44037 157031 | 34617 22080 1515797 68.7 | 3.040 % | c | 158994 | 44037 157031 | 38078 25924 1738296 67.1 | 3.040 % | c | 164762 | 44037 157031 | 41886 31692 1976844 62.4 | 3.040 % | c ============================================================================== c [1mFound solution: 464210[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 838405 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 167831 | 44045 157121 | 14681 34761 2081464 59.9 | 3.040 % | c | 167933 | 44045 157121 | 16149 13823 525799 38.0 | 3.122 % | c | 168083 | 44045 157121 | 17764 13973 527131 37.7 | 3.122 % | c | 168309 | 44045 157121 | 19540 14199 530316 37.3 | 3.122 % | c | 168646 | 44045 157121 | 21494 14536 539546 37.1 | 3.122 % | c | 169152 | 44045 157121 | 23643 15042 546548 36.3 | 3.122 % | c | 169911 | 44045 157121 | 26008 15801 564733 35.7 | 3.122 % | c | 171052 | 44045 157121 | 28609 16942 591764 34.9 | 3.122 % | c | 172760 | 44045 157121 | 31470 18650 675261 36.2 | 3.122 % | c | 175323 | 44045 157121 | 34617 21213 750053 35.4 | 3.122 % | c | 179167 | 44045 157121 | 38078 25057 899368 35.9 | 3.122 % | c ============================================================================== c [1mFound solution: 428395[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 874220 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 184012 | 44060 157289 | 14686 29902 1218066 40.7 | 3.122 % | c | 184112 | 44060 157289 | 16154 13979 555675 39.8 | 3.273 % | c | 184263 | 44060 157289 | 17770 14130 557655 39.5 | 3.273 % | c | 184489 | 44060 157289 | 19547 14356 562583 39.2 | 3.273 % | c | 184826 | 44060 157289 | 21501 14693 569455 38.8 | 3.273 % | c | 185332 | 44060 157289 | 23651 15199 581093 38.2 | 3.273 % | c | 186092 | 44060 157289 | 26017 15959 610267 38.2 | 3.273 % | c | 187232 | 44060 157289 | 28618 17099 641313 37.5 | 3.273 % | c | 188940 | 44060 157289 | 31480 18807 722381 38.4 | 3.273 % | c | 191502 | 44060 157289 | 34628 21369 836978 39.2 | 3.273 % | c | 195346 | 44060 157289 | 38091 25213 996388 39.5 | 3.273 % | c ============================================================================== c [1mFound solution: 423988[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 878627 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 200841 | 44067 157351 | 14689 30708 1247484 40.6 | 3.273 % | c | 200941 | 44067 157351 | 16157 14363 512857 35.7 | 3.326 % | c | 201092 | 44067 157351 | 17773 14514 514356 35.4 | 3.326 % | c | 201321 | 44067 157351 | 19551 14743 519060 35.2 | 3.326 % | c | 201659 | 44067 157351 | 21506 15081 529211 35.1 | 3.326 % | c | 202165 | 44067 157351 | 23656 15587 539280 34.6 | 3.326 % | c | 202924 | 44067 157351 | 26022 16346 561699 34.4 | 3.326 % | c | 204063 | 44067 157351 | 28624 17485 587857 33.6 | 3.326 % | c | 205771 | 44067 157351 | 31487 19193 640102 33.4 | 3.326 % | c | 208334 | 44067 157351 | 34635 21756 708768 32.6 | 3.326 % | c | 212178 | 44067 157351 | 38099 25600 904857 35.3 | 3.326 % | c | 217944 | 44067 157351 | 41909 31366 1130671 36.0 | 3.326 % | c | 226594 | 44067 157351 | 46100 40016 1847353 46.2 | 3.326 % | c | 239568 | 44067 157351 | 50710 19765 1007280 51.0 | 3.326 % | c ============================================================================== c [1mFound solution: 423588[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 879027 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 241573 | 44076 157451 | 14692 21770 1052056 48.3 | 3.326 % | c | 241673 | 44076 157451 | 16161 10985 450938 41.1 | 3.395 % | c | 241823 | 44076 157451 | 17777 11135 452162 40.6 | 3.395 % | c | 242048 | 44076 157451 | 19555 11360 454485 40.0 | 3.395 % | c | 242385 | 44076 157451 | 21510 11697 460353 39.4 | 3.395 % | c | 242891 | 44076 157451 | 23661 12203 472355 38.7 | 3.395 % | c | 243653 | 44076 157451 | 26027 12965 488582 37.7 | 3.395 % | c | 244793 | 44076 157451 | 28630 14105 531048 37.6 | 3.395 % | c | 246502 | 44076 157451 | 31493 15814 591619 37.4 | 3.395 % | c | 249064 | 44076 157451 | 34642 18376 691318 37.6 | 3.395 % | c | 252908 | 44076 157451 | 38107 22220 842012 37.9 | 3.395 % | c | 258674 | 44076 157451 | 41917 27986 1189161 42.5 | 3.395 % | c ============================================================================== c [1mFound solution: 420872[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 881743 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 266993 | 44081 157509 | 14693 36305 1679287 46.3 | 3.395 % | c | 267093 | 44081 157509 | 16162 14483 703373 48.6 | 3.449 % | c | 267243 | 44081 157509 | 17778 14633 706227 48.3 | 3.449 % | c | 267468 | 44081 157509 | 19556 14858 710085 47.8 | 3.449 % | c | 267806 | 44081 157509 | 21512 15196 719828 47.4 | 3.449 % | c | 268312 | 44081 157509 | 23663 15702 728727 46.4 | 3.449 % | c | 269071 | 44081 157509 | 26029 16461 742697 45.1 | 3.449 % | c | 270214 | 44081 157509 | 28632 17604 770239 43.8 | 3.449 % | c | 271923 | 44081 157509 | 31495 19313 837394 43.4 | 3.449 % | c | 274486 | 44081 157509 | 34645 21876 955364 43.7 | 3.449 % | c | 278330 | 44081 157509 | 38109 25720 1074152 41.8 | 3.449 % | c | 284096 | 44081 157509 | 41920 31486 1413971 44.9 | 3.449 % | c | 292747 | 44081 157509 | 46112 40137 2027122 50.5 | 3.449 % | c | 305721 | 44081 157509 | 50724 20385 1125855 55.2 | 3.449 % | c | 325184 | 44081 157509 | 55796 39848 1921718 48.2 | 3.449 % | c | 354376 | 44081 157509 | 61376 25261 1965083 77.8 | 3.449 % | c | 398166 | 44081 157509 | 67513 23312 949324 40.7 | 3.449 % | c | 463850 | 44081 157509 | 74265 35145 3672852 104.5 | 3.449 % | c ============================================================================== c [1mFound solution: 419359[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 883256 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 495971 | 44091 157616 | 14697 67266 6262844 93.1 | 3.449 % | c | 496071 | 44091 157616 | 16166 7789 286020 36.7 | 3.529 % | c | 496221 | 44091 157616 | 17783 7939 286976 36.1 | 3.529 % | c | 496446 | 44091 157616 | 19561 8164 289013 35.4 | 3.529 % | c | 496783 | 44091 157616 | 21517 8501 292292 34.4 | 3.529 % | c | 497289 | 44091 157616 | 23669 9007 299722 33.3 | 3.529 % | c | 498049 | 44091 157616 | 26036 9767 315837 32.3 | 3.529 % | c | 499193 | 44091 157616 | 28640 10911 342383 31.4 | 3.529 % | c | 500902 | 44091 157616 | 31504 12620 401810 31.8 | 3.529 % | c | 503466 | 44091 157616 | 34654 15184 535017 35.2 | 3.529 % | c | 507310 | 44091 157616 | 38120 19028 733279 38.5 | 3.529 % | c | 513076 | 44091 157616 | 41932 24794 1087774 43.9 | 3.529 % | c | 521726 | 44091 157616 | 46125 33444 1359557 40.7 | 3.529 % | c | 534700 | 44091 157616 | 50738 46418 2128951 45.9 | 3.529 % | c ============================================================================== c [1mFound solution: 400558[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 902057 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 551634 | 44105 157742 | 14701 26955 1310918 48.6 | 3.529 % | c | 551734 | 44105 157742 | 16171 12906 680313 52.7 | 3.636 % | c | 551884 | 44105 157742 | 17788 13056 681395 52.2 | 3.636 % | c | 552110 | 44105 157742 | 19567 13282 683676 51.5 | 3.636 % | c | 552448 | 44105 157742 | 21523 13620 688067 50.5 | 3.636 % | c | 552954 | 44105 157742 | 23676 14126 695245 49.2 | 3.636 % | c | 553713 | 44105 157742 | 26043 14885 708403 47.6 | 3.636 % | c | 554852 | 44105 157742 | 28648 16024 739185 46.1 | 3.636 % | c | 556560 | 44105 157742 | 31512 17732 810601 45.7 | 3.636 % | c | 559123 | 44105 157742 | 34664 20295 891067 43.9 | 3.636 % | c | 562969 | 44105 157742 | 38130 24141 1078799 44.7 | 3.636 % | c | 568736 | 44105 157742 | 41943 29908 1401672 46.9 | 3.636 % | c | 577385 | 44105 157742 | 46138 38557 1755814 45.5 | 3.636 % | c | 590359 | 44105 157742 | 50751 17722 1304581 73.6 | 3.636 % | c ============================================================================== c [1mFound solution: 400552[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 902063 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 596280 | 44107 157761 | 14702 23643 1639743 69.4 | 3.636 % | c | 596380 | 44107 157761 | 16172 11922 759686 63.7 | 3.649 % | c | 596530 | 44107 157761 | 17789 12072 761740 63.1 | 3.649 % | c | 596755 | 44107 157761 | 19568 12297 766189 62.3 | 3.649 % | c | 597093 | 44107 157761 | 21525 12635 769597 60.9 | 3.649 % | c | 597599 | 44107 157761 | 23677 13141 779266 59.3 | 3.649 % | c | 598358 | 44107 157761 | 26045 13900 798213 57.4 | 3.649 % | c | 599497 | 44107 157761 | 28650 15039 819921 54.5 | 3.649 % | c | 601205 | 44107 157761 | 31515 16747 861156 51.4 | 3.649 % | c | 603767 | 44107 157761 | 34666 19309 1006094 52.1 | 3.649 % | c | 607614 | 44107 157761 | 38133 23156 1229444 53.1 | 3.649 % | c | 613380 | 44107 157761 | 41946 28922 1467188 50.7 | 3.649 % | c | 622029 | 44107 157761 | 46141 37571 1745722 46.5 | 3.649 % | c | 635005 | 44107 157761 | 50755 15986 842613 52.7 | 3.649 % | c | 654469 | 44107 157761 | 55830 35450 1990931 56.2 | 3.649 % | c | 683661 | 44107 157761 | 61413 21176 1289814 60.9 | 3.649 % | c | 727450 | 44107 157761 | 67555 17370 812244 46.8 | 3.649 % | c ============================================================================== c [1mFound solution: 400545[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 902070 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 758106 | 44116 157844 | 14705 48026 3409727 71.0 | 3.649 % | c | 758207 | 44116 157844 | 16175 14788 1211145 81.9 | 3.689 % | c | 758357 | 44116 157844 | 17793 14938 1212847 81.2 | 3.689 % | c | 758582 | 44116 157844 | 19572 15163 1215427 80.2 | 3.689 % | c | 758919 | 44116 157844 | 21529 15500 1219018 78.6 | 3.689 % | c | 759426 | 44116 157844 | 23682 16007 1225623 76.6 | 3.689 % | c | 760185 | 44116 157844 | 26050 16766 1238051 73.8 | 3.689 % | c | 761327 | 44116 157844 | 28655 17908 1276581 71.3 | 3.689 % | c | 763040 | 44116 157844 | 31521 19621 1334077 68.0 | 3.689 % | c | 765602 | 44116 157844 | 34673 22183 1427366 64.3 | 3.689 % | c | 769446 | 44116 157844 | 38140 26027 1568726 60.3 | 3.689 % | c | 775212 | 44116 157844 | 41955 31793 2017974 63.5 | 3.689 % | c | 783861 | 44116 157844 | 46150 40442 2388298 59.1 | 3.689 % | c | 796836 | 44116 157844 | 50765 21038 923926 43.9 | 3.689 % | c | 816297 | 44116 157844 | 55842 40499 2224951 54.9 | 3.689 % | c | 845489 | 44116 157844 | 61426 26709 1524041 57.1 | 3.689 % | c | 889278 | 44116 157844 | 67569 20958 1209785 57.7 | 3.689 % | c | 954965 | 44116 157844 | 74325 33870 2294974 67.8 | 3.689 % | c ============================================================================== c [1mFound solution: 400544[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 902071 bits: 21/20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 958755 | 44118 157865 | 14706 37660 2484804 66.0 | 3.689 % | c | 958855 | 44118 157865 | 16176 8107 304431 37.6 | 3.702 % | c | 959005 | 44118 157865 | 17794 8257 305937 37.1 | 3.702 % | c | 959230 | 44118 157865 | 19573 8482 307906 36.3 | 3.702 % | c | 959567 | 44118 157865 | 21531 8819 312077 35.4 | 3.702 % | c | 960074 | 44118 157865 | 23684 9326 326001 35.0 | 3.702 % | c | 960833 | 44118 157865 | 26052 10085 339354 33.6 | 3.702 % | c | 961972 | 44118 157865 | 28657 11224 381255 34.0 | 3.702 % | c | 963680 | 44118 157865 | 31523 12932 495253 38.3 | 3.702 % | c | 966243 | 44118 157865 | 34675 15495 610073 39.4 | 3.702 % | c | 970087 | 44118 157865 | 38143 19339 855510 44.2 | 3.702 % | c | 975854 | 44118 157865 | 41957 25106 1134303 45.2 | 3.702 % | c | 984503 | 44118 157865 | 46153 33755 1532699 45.4 | 3.702 % | c | 997478 | 44118 157865 | 50769 46730 2208226 47.3 | 3.702 % | c | 1016942 | 44118 157865 | 55846 29853 1326820 44.4 | 3.702 % | c | 1046137 | 44118 157865 | 61430 14560 911721 62.6 | 3.702 % | c | 1089927 | 44118 157865 | 67573 58350 4936560 84.6 | 3.702 % | #### 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.84 0.95 0.90 2/54 16373 Raw data (stat): 16373 (runsolver) R 16372 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489079931 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.001 s] Raw data (loadavg): 0.87 0.95 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 2049 0 0 0 994 5 0 0 25 0 1 0 489079931 10227712 2026 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2497 2026 603 41 0 2456 0 vsize: 9988 [startup+20.0018 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 2590 0 0 0 1992 7 0 0 25 0 1 0 489079931 12349440 2567 4294967295 134512640 134672761 3221224544 3221223624 134541793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3015 2567 603 41 0 2974 0 vsize: 12060 [startup+30.0021 s] Raw data (loadavg): 0.90 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 3497 0 0 0 2989 9 0 0 25 0 1 0 489079931 16236544 3474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3964 3474 603 41 0 3923 0 vsize: 15856 [startup+40.0025 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 3995 0 0 0 3988 11 0 0 25 0 1 0 489079931 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4455 3972 603 41 0 4414 0 vsize: 17820 [startup+50.0033 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 3995 0 0 0 4988 11 0 0 25 0 1 0 489079931 18247680 3972 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4455 3972 603 41 0 4414 0 vsize: 17820 [startup+60.0037 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 3995 0 0 0 5988 11 0 0 25 0 1 0 489079931 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4455 3972 603 41 0 4414 0 vsize: 17820 [startup+70.004 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 4327 0 0 0 6987 12 0 0 25 0 1 0 489079931 19582976 4304 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4781 4304 603 41 0 4740 0 vsize: 19124 [startup+80.0048 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 4693 0 0 0 7985 14 0 0 25 0 1 0 489079931 21061632 4670 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5142 4670 603 41 0 5101 0 vsize: 20568 [startup+90.0042 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 4693 0 0 0 8985 14 0 0 25 0 1 0 489079931 21061632 4670 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5142 4670 603 41 0 5101 0 vsize: 20568 [startup+100.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 4693 0 0 0 9985 14 0 0 25 0 1 0 489079931 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5142 4670 603 41 0 5101 0 vsize: 20568 [startup+110.006 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 5201 0 0 0 10983 17 0 0 25 0 1 0 489079931 23072768 5178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5633 5178 603 41 0 5592 0 vsize: 22532 [startup+120.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 5963 0 0 0 11980 19 0 0 25 0 1 0 489079931 26173440 5940 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6390 5940 603 41 0 6349 0 vsize: 25560 [startup+130.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6176 0 0 0 12979 20 0 0 25 0 1 0 489079931 27111424 6153 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6153 603 41 0 6578 0 vsize: 26476 [startup+140.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6176 0 0 0 13979 21 0 0 25 0 1 0 489079931 27111424 6153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6153 603 41 0 6578 0 vsize: 26476 [startup+150.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6177 0 0 0 14979 21 0 0 25 0 1 0 489079931 27111424 6154 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6154 603 41 0 6578 0 vsize: 26476 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6178 0 0 0 15979 21 0 0 25 0 1 0 489079931 27111424 6155 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6178 0 0 0 16979 21 0 0 25 0 1 0 489079931 27111424 6155 4294967295 134512640 134672761 3221224544 3221223464 1075351154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6178 0 0 0 17978 21 0 0 25 0 1 0 489079931 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6178 0 0 0 18979 21 0 0 25 0 1 0 489079931 27111424 6155 4294967295 134512640 134672761 3221224544 3221223720 134559124 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6178 0 0 0 19979 21 0 0 25 0 1 0 489079931 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 20979 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 21979 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 22979 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+240.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 23979 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 24980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+260.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 25980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 26980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+280.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 27980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+290.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 28980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+300.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 29980 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 30981 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+320.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6179 0 0 0 31981 21 0 0 25 0 1 0 489079931 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+330.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6180 0 0 0 32981 21 0 0 25 0 1 0 489079931 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+340.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6180 0 0 0 33981 21 0 0 25 0 1 0 489079931 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6180 0 0 0 34981 21 0 0 25 0 1 0 489079931 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6180 0 0 0 35982 21 0 0 25 0 1 0 489079931 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6180 0 0 0 36982 21 0 0 25 0 1 0 489079931 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+380.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6447 0 0 0 37981 22 0 0 25 0 1 0 489079931 28188672 6424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6882 6424 603 41 0 6841 0 vsize: 27528 [startup+390.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 6952 0 0 0 38979 24 0 0 25 0 1 0 489079931 30216192 6929 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7377 6929 603 41 0 7336 0 vsize: 29508 [startup+400.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7480 0 0 0 39979 25 0 0 25 0 1 0 489079931 32624640 7457 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7965 7458 603 41 0 7924 0 vsize: 31860 [startup+410.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 40977 26 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+420.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 41978 26 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+430.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 42978 26 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+440.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 43978 26 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+450.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 44978 27 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7848 0 0 0 45977 27 0 0 25 0 1 0 489079931 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 7965 0 0 0 46977 27 0 0 25 0 1 0 489079931 34652160 7942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8460 7942 603 41 0 8419 0 vsize: 33840 [startup+480.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 8625 0 0 0 47975 29 0 0 25 0 1 0 489079931 37335040 8602 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9115 8602 603 41 0 9074 0 vsize: 36460 [startup+490.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9096 0 0 0 48973 31 0 0 25 0 1 0 489079931 39350272 9073 4294967295 134512640 134672761 3221224544 3221223536 134565829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+500.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9096 0 0 0 49973 32 0 0 25 0 1 0 489079931 39350272 9073 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+510.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9096 0 0 0 50973 32 0 0 25 0 1 0 489079931 39350272 9073 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+520.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9096 0 0 0 51973 32 0 0 25 0 1 0 489079931 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+530.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9096 0 0 0 52974 32 0 0 25 0 1 0 489079931 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+540.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 53974 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+550.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 54974 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+560.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 55974 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+570.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 56974 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+580.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 57974 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+590.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 58975 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+600.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 59975 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+610.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 60975 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+620.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 61975 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+630.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 62975 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+640.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 63976 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+650.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 64976 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221222848 134565768 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+660.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 65976 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+670.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 66976 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+680.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9097 0 0 0 67976 32 0 0 25 0 1 0 489079931 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+690.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 68976 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+700.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 69977 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+710.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 70977 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+720.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 71977 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+730.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 72977 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+740.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 73977 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+750.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 74978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+760.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 75978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+770.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 76978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+780.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 77978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+790.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 78978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+800.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 79978 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+810.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 80979 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+820.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 81979 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+830.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 82979 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+840.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 83979 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+850.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 84979 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+860.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 85980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+870.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 86980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+880.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 87980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+890.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 88980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+900.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 89980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 90980 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+920.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 91981 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+930.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 92981 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+940.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 93981 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+950.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 94981 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+960.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 95981 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+970.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 96982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+980.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 97982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+990.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 98982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 99982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 100982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 101982 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 102983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134565140 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 103983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 104983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 105983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 106983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 107983 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 108984 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 109984 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 110984 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 111984 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 112985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 113985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 114985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 115985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 116985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 117985 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 118986 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 16373 Raw data (stat): 16373 (minisat+) R 16372 10720 10719 0 -1 0 9098 0 0 0 119986 32 0 0 25 0 1 0 489079931 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 16373 Raw data (stat): 16373 (minisat+) Z 16372 10720 10719 0 -1 12 9101 0 0 0 119986 34 0 0 25 0 1 0 489079931 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.05 CPU time (s): 1200.2 CPU user time (s): 1199.86 CPU system time (s): 0.340948 CPU usage (%): 100.013 Max. virtual memory (Kb): 38428 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####