Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0282.opb |
MD5SUM | 1a8deb577df7e72871b7e1004c098336 |
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.01984 |
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 wulflinc26 THE 2005-04-21 22:51:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13725 boxname=wulflinc26 idbench=1056 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1a8deb577df7e72871b7e1004c098336 /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0282.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 13725 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 363568 kB Buffers: 34492 kB Cached: 609332 kB SwapCached: 68 kB Active: 193176 kB Inactive: 453436 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 363316 kB SwapTotal: 2097892 kB SwapFree: 2097800 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6880 kB Slab: 18864 kB Committed_AS: 63728 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 23:11:54 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 13725 7 1200.22 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.85 0.95 0.91 2/54 11446 Raw data (stat): 11446 (runsolver) R 11445 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548827132 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.87 0.95 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 2043 0 0 0 993 5 0 0 25 0 1 0 548827132 10227712 2020 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2497 2020 603 41 0 2456 0 vsize: 9988 [startup+20.0008 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 2581 0 0 0 1991 7 0 0 25 0 1 0 548827132 12349440 2558 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3015 2558 603 41 0 2974 0 vsize: 12060 [startup+30.0012 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 3492 0 0 0 2988 10 0 0 25 0 1 0 548827132 16236544 3469 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3964 3469 603 41 0 3923 0 vsize: 15856 [startup+40.0012 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 3995 0 0 0 3986 12 0 0 25 0 1 0 548827132 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.0018 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 3995 0 0 0 4986 12 0 0 25 0 1 0 548827132 18247680 3972 4294967295 134512640 134672761 3221224544 3221223648 134560005 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.0012 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 3995 0 0 0 5986 12 0 0 25 0 1 0 548827132 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0012 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 4333 0 0 0 6986 13 0 0 25 0 1 0 548827132 19582976 4310 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4781 4310 603 41 0 4740 0 vsize: 19124 [startup+80.0019 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 4693 0 0 0 7985 13 0 0 25 0 1 0 548827132 21061632 4670 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.0013 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 4693 0 0 0 8985 14 0 0 25 0 1 0 548827132 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.001 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 4693 0 0 0 9985 14 0 0 25 0 1 0 548827132 21061632 4670 4294967295 134512640 134672761 3221224544 3221223648 134559872 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.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 5239 0 0 0 10985 14 0 0 25 0 1 0 548827132 23216128 5216 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5668 5216 603 41 0 5627 0 vsize: 22672 [startup+120.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6008 0 0 0 11983 16 0 0 25 0 1 0 548827132 26439680 5985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6455 5985 603 41 0 6414 0 vsize: 25820 [startup+130.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6176 0 0 0 12983 17 0 0 25 0 1 0 548827132 27111424 6153 4294967295 134512640 134672761 3221224544 3221223728 134559324 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.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6176 0 0 0 13983 17 0 0 25 0 1 0 548827132 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.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6177 0 0 0 14983 17 0 0 25 0 1 0 548827132 27111424 6154 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6154 603 41 0 6578 0 vsize: 26476 [startup+160.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6178 0 0 0 15983 17 0 0 25 0 1 0 548827132 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6178 0 0 0 16983 17 0 0 25 0 1 0 548827132 27111424 6155 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6178 0 0 0 17982 17 0 0 25 0 1 0 548827132 27111424 6155 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+190.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6178 0 0 0 18982 17 0 0 25 0 1 0 548827132 27111424 6155 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+200.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6178 0 0 0 19983 17 0 0 25 0 1 0 548827132 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6155 603 41 0 6578 0 vsize: 26476 [startup+210.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 20983 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+220.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 21983 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+230.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 22983 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+240.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 23983 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+250.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 24983 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+260.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 25984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+270.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 26984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+280.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 27984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+290.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 28984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+300.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 29984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+310.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6179 0 0 0 30984 17 0 0 25 0 1 0 548827132 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6156 603 41 0 6578 0 vsize: 26476 [startup+320.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6180 0 0 0 31985 17 0 0 25 0 1 0 548827132 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+330.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6180 0 0 0 32985 17 0 0 25 0 1 0 548827132 27111424 6157 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+340.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6180 0 0 0 33985 17 0 0 25 0 1 0 548827132 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+350.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6180 0 0 0 34985 17 0 0 25 0 1 0 548827132 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+360.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6180 0 0 0 35985 17 0 0 25 0 1 0 548827132 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6157 603 41 0 6578 0 vsize: 26476 [startup+370.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6186 0 0 0 36985 17 0 0 25 0 1 0 548827132 27111424 6163 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 6163 603 41 0 6578 0 vsize: 26476 [startup+380.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 6731 0 0 0 37985 19 0 0 25 0 1 0 548827132 29401088 6708 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7178 6708 603 41 0 7137 0 vsize: 28712 [startup+390.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7198 0 0 0 38983 20 0 0 25 0 1 0 548827132 31551488 7175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7703 7175 603 41 0 7662 0 vsize: 30812 [startup+400.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7762 0 0 0 39982 21 0 0 25 0 1 0 548827132 33845248 7739 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8263 7739 603 41 0 8222 0 vsize: 33052 [startup+410.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 40982 21 0 0 25 0 1 0 548827132 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+420.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 41983 21 0 0 25 0 1 0 548827132 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+430.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 42983 21 0 0 25 0 1 0 548827132 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+440.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 43983 21 0 0 25 0 1 0 548827132 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.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 44982 22 0 0 25 0 1 0 548827132 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 7848 0 0 0 45983 22 0 0 25 0 1 0 548827132 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7825 603 41 0 8320 0 vsize: 33444 [startup+470.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 8469 0 0 0 46982 23 0 0 25 0 1 0 548827132 36802560 8446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8985 8446 603 41 0 8944 0 vsize: 35940 [startup+480.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9015 0 0 0 47981 24 0 0 25 0 1 0 548827132 38944768 8992 4294967295 134512640 134672761 3221224544 3221223676 1075347104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9508 8992 603 41 0 9467 0 vsize: 38032 [startup+490.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 11446 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9096 0 0 0 48980 24 0 0 25 0 1 0 548827132 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+500.006 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9096 0 0 0 49981 24 0 0 25 0 1 0 548827132 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+510.007 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9096 0 0 0 50980 25 0 0 25 0 1 0 548827132 39350272 9073 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+520.007 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9096 0 0 0 51980 25 0 0 25 0 1 0 548827132 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9073 603 41 0 9566 0 vsize: 38428 [startup+530.014 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 52981 25 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+540.014 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 53980 26 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+550.015 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 11499 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 54980 26 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+560.016 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 55980 26 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+570.015 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 56980 27 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+580.015 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 57979 28 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+590.015 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 58979 28 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+600.015 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 59978 29 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+610.016 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 60978 30 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+620.016 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 61977 30 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+630.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 62977 30 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+640.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 63977 31 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+650.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 64977 31 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+660.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9097 0 0 0 65977 31 0 0 25 0 1 0 548827132 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9074 603 41 0 9566 0 vsize: 38428 [startup+670.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 66977 32 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+680.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 67977 32 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+690.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 68977 32 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+700.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 69976 33 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+710.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 70976 34 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+720.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 71976 34 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+730.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 72976 34 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+740.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 73976 34 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+750.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 74975 35 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+760.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 75975 36 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+770.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 76974 36 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134558754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+780.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 77974 37 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+790.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 78973 37 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+800.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 79974 38 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+810.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 80973 38 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+820.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11501 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 81973 38 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+830.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 82973 39 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+840.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 83973 39 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+850.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 84973 39 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+860.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 85973 40 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+870.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 86972 41 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+880.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 87972 41 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+890.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 88972 41 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+900.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 89972 42 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+910.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 90971 42 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+920.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 91971 42 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+930.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 92971 43 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+940.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 93971 43 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+950.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 94971 44 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+960.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 95971 44 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+970.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 96970 44 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+980.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 97970 45 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+990.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 98970 45 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1000.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 99970 45 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1010.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 100970 46 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1020.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 101969 46 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1030.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 102969 47 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1040.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 103969 47 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134558413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 104969 47 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1060.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 105968 48 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134554926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1070.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 106968 48 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 107968 48 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 108968 49 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1100.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 109968 49 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1110.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 110968 50 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1120.03 s] Raw data (loadavg): 1.08 1.00 0.92 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 111967 50 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1130.03 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 112967 50 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1140.03 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 113967 51 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1150.03 s] Raw data (loadavg): 1.20 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 114966 51 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1160.03 s] Raw data (loadavg): 1.17 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 115966 52 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1170.03 s] Raw data (loadavg): 1.14 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 116966 52 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1180.03 s] Raw data (loadavg): 1.12 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 117966 53 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1190.03 s] Raw data (loadavg): 1.10 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 118966 53 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9607 9075 603 41 0 9566 0 vsize: 38428 [startup+1200.03 s] Raw data (loadavg): 1.09 1.03 0.93 2/54 11503 Raw data (stat): 11446 (minisat+) R 11445 22612 22611 0 -1 0 9098 0 0 0 119965 53 0 0 25 0 1 0 548827132 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 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): 1.09 1.03 0.93 1/54 11503 Raw data (stat): 11446 (minisat+) Z 11445 22612 22611 0 -1 12 9101 0 0 0 119965 55 0 0 25 0 1 0 548827132 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.22 CPU user time (s): 1199.66 CPU system time (s): 0.555915 CPU usage (%): 100.014 Max. virtual memory (Kb): 38428 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####