Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb |
MD5SUM | ba87f5dfbaed559dc55bc00bf07dc880 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3712 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 120 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 6291450 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 6291450 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.68 |
Number of variables | 170 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-21 13:39:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18512 boxname=wulflinc4 idbench=1424 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ba87f5dfbaed559dc55bc00bf07dc880 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-markshare1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-markshare1.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-markshare1.opb IDLAUNCH: 18512 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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.169 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: 226336 kB Buffers: 27132 kB Cached: 758268 kB SwapCached: 0 kB Active: 55664 kB Inactive: 732532 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 226084 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6816 kB Slab: 14512 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 13:59:11 (client local time) WITH STATUS 10 IN 1200.15 SECONDS stats: 18512 7 1200.15 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 405119 bits: 20/19 c ---[ 8]---> Adder-cost: 314 maxlim: 431743 bits: 20/19 c ---[ 6]---> Adder-cost: 348 maxlim: 435327 bits: 20/19 c ---[ 4]---> Adder-cost: 318 maxlim: 411775 bits: 20/19 c ---[ 2]---> Adder-cost: 312 maxlim: 410751 bits: 20/19 c ---[ 0]---> Adder-cost: 314 maxlim: 411135 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 599 6.0 | 11.212 % | c ============================================================================== c [1mFound solution: 621184[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 854 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115 | 15123 50959 | 5041 115 809 7.0 | 11.212 % | c | 216 | 15115 50933 | 5545 215 6283 29.2 | 8.456 % | c ============================================================================== c [1mFound solution: 594432[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 265 | 15217 51193 | 5072 264 12306 46.6 | 8.456 % | c | 368 | 15209 51167 | 5579 366 14797 40.4 | 8.455 % | c | 518 | 15209 51167 | 6137 516 22636 43.9 | 8.455 % | c | 743 | 15201 51141 | 6750 740 45661 61.7 | 8.488 % | c ============================================================================== c [1mFound solution: 434176[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 818 | 15232 51216 | 5077 815 49004 60.1 | 8.488 % | c | 919 | 15232 51216 | 5584 916 64144 70.0 | 8.493 % | c | 1070 | 15232 51216 | 6143 1067 77822 72.9 | 8.493 % | c | 1295 | 15224 51190 | 6757 1291 92578 71.7 | 8.527 % | c | 1632 | 15216 51164 | 7433 1627 124637 76.6 | 8.561 % | c | 2138 | 15216 51164 | 8176 2133 165578 77.6 | 8.561 % | c | 2898 | 15200 51112 | 8994 2891 235730 81.5 | 8.628 % | c | 4038 | 15200 51112 | 9893 4031 329789 81.8 | 8.628 % | c | 5746 | 15200 51112 | 10883 5739 471861 82.2 | 8.628 % | c ============================================================================== c [1mFound solution: 407040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6078 | 15215 51151 | 5071 6071 502716 82.8 | 8.628 % | c | 6179 | 15215 51151 | 5578 3137 220945 70.4 | 8.650 % | c | 6329 | 15215 51151 | 6135 3287 231329 70.4 | 8.650 % | c | 6554 | 15215 51151 | 6749 3512 243726 69.4 | 8.650 % | c | 6891 | 15215 51151 | 7424 3849 280837 73.0 | 8.650 % | c | 7398 | 15215 51151 | 8166 4356 326304 74.9 | 8.650 % | c ============================================================================== c [1mFound solution: 364160[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8022 | 15240 51213 | 5080 4980 367622 73.8 | 8.650 % | c | 8122 | 15240 51213 | 5588 5080 379899 74.8 | 8.661 % | c | 8273 | 15240 51213 | 6146 5231 389905 74.5 | 8.661 % | c | 8498 | 15232 51187 | 6761 5455 409892 75.1 | 8.694 % | c | 8836 | 15232 51187 | 7437 5793 435941 75.3 | 8.694 % | c | 9343 | 15232 51187 | 8181 6300 467577 74.2 | 8.694 % | c | 10104 | 15232 51187 | 8999 7061 522662 74.0 | 8.694 % | c | 11243 | 15216 51135 | 9899 8198 598918 73.1 | 8.761 % | c ============================================================================== c [1mFound solution: 330112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12674 | 15235 51182 | 5078 9629 671552 69.7 | 8.761 % | c | 12774 | 15235 51182 | 5585 4915 258192 52.5 | 8.777 % | c | 12926 | 15235 51182 | 6144 5067 267779 52.8 | 8.777 % | c | 13151 | 15235 51182 | 6758 5292 275192 52.0 | 8.777 % | c | 13489 | 15235 51182 | 7434 5630 296070 52.6 | 8.777 % | c | 13995 | 15235 51182 | 8178 6136 329734 53.7 | 8.777 % | c | 14755 | 15235 51182 | 8995 6896 409961 59.4 | 8.777 % | c | 15894 | 15235 51182 | 9895 8035 529935 66.0 | 8.777 % | c | 17604 | 15235 51182 | 10885 9745 665119 68.3 | 8.777 % | c ============================================================================== c [1mFound solution: 296448[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19485 | 15251 51222 | 5083 5860 429862 73.4 | 8.777 % | c | 19587 | 15251 51222 | 5591 3032 186614 61.5 | 8.796 % | c | 19737 | 15251 51222 | 6150 3182 196098 61.6 | 8.796 % | c | 19964 | 15251 51222 | 6765 3409 215754 63.3 | 8.796 % | c | 20301 | 15243 51196 | 7442 3745 235542 62.9 | 8.829 % | c | 20808 | 15243 51196 | 8186 4252 261088 61.4 | 8.829 % | c | 21568 | 15243 51196 | 9004 5012 320576 64.0 | 8.829 % | c | 22708 | 15243 51196 | 9905 6152 399280 64.9 | 8.829 % | c ============================================================================== c [1mFound solution: 152320[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23074 | 15273 51268 | 5091 6518 414330 63.6 | 8.829 % | c | 23179 | 15273 51268 | 5600 3364 152029 45.2 | 8.833 % | c | 23329 | 15273 51268 | 6160 3514 161262 45.9 | 8.833 % | c | 23555 | 15273 51268 | 6776 3740 173908 46.5 | 8.833 % | c | 23892 | 15265 51246 | 7453 4076 185260 45.5 | 8.900 % | c | 24398 | 15265 51246 | 8199 4582 222534 48.6 | 8.900 % | c | 25158 | 15265 51246 | 9019 5342 277349 51.9 | 8.900 % | c | 26297 | 15265 51246 | 9920 6481 352077 54.3 | 8.900 % | c | 28006 | 15265 51246 | 10913 8190 434594 53.1 | 8.900 % | c | 30568 | 15265 51246 | 12004 10752 538975 50.1 | 8.900 % | c | 34415 | 15248 51204 | 13204 8191 339466 41.4 | 9.033 % | c | 40182 | 15248 51204 | 14525 13958 651976 46.7 | 9.033 % | c | 48831 | 15240 51178 | 15977 14856 701447 47.2 | 9.067 % | c | 61806 | 15240 51178 | 17575 11073 441884 39.9 | 9.067 % | c ============================================================================== c [1mFound solution: 119168[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72763 | 15074 50740 | 5024 12867 612133 47.6 | 9.067 % | c | 72863 | 15074 50740 | 5526 3317 95779 28.9 | 10.679 % | c | 73013 | 15074 50740 | 6079 3467 99247 28.6 | 10.679 % | c | 73239 | 15074 50740 | 6686 3693 102775 27.8 | 10.679 % | c | 73577 | 15002 50568 | 7355 4029 118338 29.4 | 11.311 % | c | 74084 | 15002 50568 | 8091 4536 133378 29.4 | 11.311 % | c | 74844 | 14928 50396 | 8900 5293 157844 29.8 | 12.076 % | c | 75984 | 14928 50396 | 9790 6433 226610 35.2 | 12.076 % | c | 77693 | 14928 50396 | 10769 8142 317799 39.0 | 12.076 % | c | 80257 | 14928 50396 | 11846 10706 422563 39.5 | 12.076 % | c | 84102 | 14928 50396 | 13030 8248 319365 38.7 | 12.076 % | c | 89869 | 14928 50396 | 14334 7148 257900 36.1 | 12.076 % | c | 98518 | 14928 50396 | 15767 8285 337507 40.7 | 12.076 % | c | 111492 | 14913 50361 | 17344 12959 534297 41.2 | 12.242 % | c | 130954 | 14903 50338 | 19078 14271 714478 50.1 | 12.342 % | c ============================================================================== c [1mFound solution: 111744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 152324 | 14898 50329 | 4966 15865 714391 45.0 | 12.342 % | c | 152425 | 14898 50329 | 5462 4068 130389 32.1 | 12.579 % | c | 152576 | 14898 50329 | 6008 4219 132858 31.5 | 12.579 % | c | 152802 | 14898 50329 | 6609 4445 136968 30.8 | 12.579 % | c | 153140 | 14898 50329 | 7270 4783 146433 30.6 | 12.579 % | c | 153646 | 14898 50329 | 7997 5289 162034 30.6 | 12.579 % | c | 154406 | 14898 50329 | 8797 6049 189686 31.4 | 12.579 % | c | 155545 | 14898 50329 | 9677 7188 251116 34.9 | 12.579 % | c | 157253 | 14898 50329 | 10645 8896 346609 39.0 | 12.579 % | c | 159815 | 14898 50329 | 11709 5738 220544 38.4 | 12.579 % | c | 163659 | 14898 50329 | 12880 9582 374267 39.1 | 12.579 % | c | 169425 | 14898 50329 | 14168 8569 268566 31.3 | 12.579 % | c | 178074 | 14898 50329 | 15585 9737 480369 49.3 | 12.579 % | c | 191048 | 14878 50283 | 17143 14613 598853 41.0 | 12.811 % | c | 210510 | 14844 50203 | 18858 16246 764503 47.1 | 13.276 % | c | 239702 | 14833 50179 | 20744 16046 694873 43.3 | 13.375 % | c ============================================================================== c [1mFound solution: 103552[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 271093 | 14834 50183 | 4944 15268 789378 51.7 | 13.375 % | c | 271194 | 14834 50183 | 5438 3918 128594 32.8 | 13.486 % | c | 271345 | 14834 50183 | 5982 4069 132521 32.6 | 13.486 % | c | 271570 | 14834 50183 | 6580 4294 141010 32.8 | 13.486 % | c | 271908 | 14834 50183 | 7238 4632 150744 32.5 | 13.486 % | c | 272414 | 14834 50183 | 7962 5138 170656 33.2 | 13.486 % | c | 273173 | 14834 50183 | 8758 5897 191009 32.4 | 13.486 % | c | 274313 | 14834 50183 | 9634 7037 232241 33.0 | 13.486 % | c ============================================================================== c [1mFound solution: 100736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 274357 | 14845 50210 | 4948 7081 232942 32.9 | 13.486 % | c | 274457 | 14845 50210 | 5442 3641 85848 23.6 | 13.501 % | c | 274607 | 14845 50210 | 5987 3791 89517 23.6 | 13.501 % | c | 274832 | 14845 50210 | 6585 4016 93786 23.4 | 13.501 % | c | 275169 | 14845 50210 | 7244 4353 101362 23.3 | 13.501 % | c | 275677 | 14845 50210 | 7968 4861 119994 24.7 | 13.501 % | c | 276437 | 14845 50210 | 8765 5621 148641 26.4 | 13.501 % | c | 277576 | 14845 50210 | 9642 6760 191898 28.4 | 13.501 % | c | 279284 | 14845 50210 | 10606 8468 249840 29.5 | 13.501 % | c | 281847 | 14835 50186 | 11667 11030 358753 32.5 | 13.600 % | c | 285692 | 14835 50186 | 12833 8613 362190 42.1 | 13.600 % | c | 291459 | 14835 50186 | 14117 7587 289521 38.2 | 13.600 % | c ============================================================================== c [1mFound solution: 89728[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 293988 | 14846 50213 | 4948 10116 390394 38.6 | 13.600 % | c | 294089 | 14846 50213 | 5442 5159 164438 31.9 | 13.615 % | c | 294239 | 14846 50213 | 5987 5309 167333 31.5 | 13.615 % | c | 294464 | 14846 50213 | 6585 5534 172162 31.1 | 13.615 % | c | 294802 | 14846 50213 | 7244 5872 176101 30.0 | 13.615 % | c | 295309 | 14846 50213 | 7968 6379 187425 29.4 | 13.615 % | c | 296068 | 14846 50213 | 8765 7138 204419 28.6 | 13.615 % | c | 297207 | 14846 50213 | 9642 8277 239484 28.9 | 13.615 % | c | 298915 | 14846 50213 | 10606 9985 299663 30.0 | 13.615 % | c | 301477 | 14846 50213 | 11667 6800 209465 30.8 | 13.615 % | c | 305322 | 14846 50213 | 12833 10645 346430 32.5 | 13.615 % | c | 311088 | 14846 50213 | 14117 9572 368611 38.5 | 13.615 % | c | 319737 | 14846 50213 | 15528 10843 449466 41.5 | 13.615 % | c ============================================================================== c [1mFound solution: 80256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 322873 | 14855 50236 | 4951 13979 600064 42.9 | 13.615 % | c | 322973 | 14835 50191 | 5446 3593 115506 32.1 | 13.833 % | c | 323124 | 14835 50191 | 5990 3744 117492 31.4 | 13.833 % | c | 323349 | 14835 50191 | 6589 3969 125254 31.6 | 13.833 % | c | 323686 | 14835 50191 | 7248 4306 136016 31.6 | 13.833 % | c | 324194 | 14835 50191 | 7973 4814 157049 32.6 | 13.833 % | c | 324953 | 14827 50165 | 8770 5572 173243 31.1 | 13.866 % | c | 326092 | 14827 50165 | 9648 6711 216993 32.3 | 13.866 % | c | 327800 | 14827 50165 | 10612 8419 284843 33.8 | 13.866 % | c | 330362 | 14827 50165 | 11674 10981 382052 34.8 | 13.866 % | c | 334206 | 14827 50165 | 12841 8508 317228 37.3 | 13.866 % | c | 339974 | 14827 50165 | 14125 7421 297557 40.1 | 13.866 % | c | 348624 | 14805 50116 | 15538 8654 325463 37.6 | 14.064 % | c | 361598 | 14799 50102 | 17092 13376 498028 37.2 | 14.130 % | c | 381061 | 14794 50091 | 18801 14737 613715 41.6 | 14.196 % | c | 410254 | 14788 50077 | 20681 14622 546277 37.4 | 14.262 % | c ============================================================================== c [1mFound solution: 69120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 448552 | 14800 50107 | 4933 20848 921959 44.2 | 14.262 % | c | 448654 | 14800 50107 | 5426 5314 192008 36.1 | 14.276 % | c | 448804 | 14800 50107 | 5968 5464 198470 36.3 | 14.276 % | c | 449030 | 14800 50107 | 6565 5690 204641 36.0 | 14.276 % | c | 449367 | 14800 50107 | 7222 6027 210942 35.0 | 14.276 % | c | 449875 | 14800 50107 | 7944 6535 229402 35.1 | 14.276 % | c | 450637 | 14800 50107 | 8739 7297 246014 33.7 | 14.276 % | c | 451776 | 14800 50107 | 9613 8436 273334 32.4 | 14.276 % | c | 453484 | 14800 50107 | 10574 10144 325289 32.1 | 14.276 % | c | 456047 | 14800 50107 | 11631 7110 185707 26.1 | 14.276 % | c | 459892 | 14800 50107 | 12794 10955 322234 29.4 | 14.276 % | c | 465659 | 14800 50107 | 14074 9990 334936 33.5 | 14.276 % | c | 474308 | 14776 50052 | 15481 11251 381453 33.9 | 14.474 % | c | 487282 | 14776 50052 | 17030 16095 695932 43.2 | 14.474 % | c | 506743 | 14776 50052 | 18733 17741 685125 38.6 | 14.474 % | c | 535935 | 14772 50043 | 20606 17662 769860 43.6 | 14.540 % | c | 579726 | 14758 50010 | 22667 18855 721884 38.3 | 14.672 % | c | 645411 | 14758 50010 | 24933 14376 590893 41.1 | 14.672 % | c | 743938 | 14754 49999 | 27427 23200 1041232 44.9 | 14.738 % | c | 891728 | 14738 49963 | 30169 14367 580925 40.4 | 14.903 % | c ============================================================================== c [1mFound solution: 65024[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 937679 | 14686 49792 | 4895 27281 1216508 44.6 | 14.903 % | c | 937780 | 14686 49792 | 5384 3512 101768 29.0 | 15.349 % | c | 937930 | 14686 49792 | 5922 3662 107681 29.4 | 15.349 % | c | 938155 | 14686 49792 | 6515 3887 113416 29.2 | 15.349 % | c | 938493 | 14686 49792 | 7166 4225 119019 28.2 | 15.349 % | c | 939000 | 14686 49792 | 7883 4732 131245 27.7 | 15.349 % | c | 939759 | 14674 49764 | 8671 5485 164145 29.9 | 15.481 % | c | 940898 | 14674 49764 | 9538 6624 203787 30.8 | 15.481 % | c | 942606 | 14674 49764 | 10492 8332 279933 33.6 | 15.481 % | c | 945169 | 14674 49764 | 11542 10895 380159 34.9 | 15.481 % | c | 949015 | 14674 49764 | 12696 8579 284432 33.2 | 15.481 % | c | 954782 | 14674 49764 | 13966 7628 238535 31.3 | 15.481 % | c ============================================================================== c [1mFound solution: 57088[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 955134 | 14687 49797 | 4895 7980 248620 31.2 | 15.481 % | c | 955235 | 14687 49797 | 5384 4091 112116 27.4 | 15.493 % | c | 955385 | 14687 49797 | 5922 4241 114167 26.9 | 15.493 % | c | 955610 | 14687 49797 | 6515 4466 118571 26.5 | 15.493 % | c | 955949 | 14687 49797 | 7166 4805 128136 26.7 | 15.493 % | c | 956455 | 14687 49797 | 7883 5311 140244 26.4 | 15.493 % | c | 957215 | 14687 49797 | 8671 6071 160201 26.4 | 15.493 % | c ============================================================================== c [1mFound solution: 56960[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 957980 | 14691 49807 | 4897 6836 205567 30.1 | 15.493 % | c | 958080 | 14691 49807 | 5386 3518 94034 26.7 | 15.516 % | c | 958231 | 14691 49807 | 5925 3669 96617 26.3 | 15.516 % | c | 958456 | 14691 49807 | 6517 3894 101457 26.1 | 15.516 % | c | 958794 | 14691 49807 | 7169 4232 109343 25.8 | 15.516 % | c | 959302 | 14691 49807 | 7886 4740 126403 26.7 | 15.516 % | c | 960061 | 14691 49807 | 8675 5499 149349 27.2 | 15.516 % | c | 961201 | 14691 49807 | 9542 6639 186304 28.1 | 15.516 % | c | 962911 | 14691 49807 | 10497 8349 243091 29.1 | 15.516 % | c | 965474 | 14691 49807 | 11546 10912 362945 33.3 | 15.516 % | c | 969318 | 14593 49560 | 12701 8608 287632 33.4 | 16.535 % | c ============================================================================== c [1mFound solution: 56064[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 970826 | 14606 49591 | 4868 10116 367239 36.3 | 16.535 % | c | 970927 | 14606 49591 | 5354 5159 173658 33.7 | 16.541 % | c | 971077 | 14606 49591 | 5890 5309 174962 33.0 | 16.541 % | c | 971303 | 14606 49591 | 6479 5535 179538 32.4 | 16.541 % | c | 971640 | 14606 49591 | 7127 5872 189053 32.2 | 16.541 % | c | 972146 | 14606 49591 | 7839 6378 206505 32.4 | 16.541 % | c | 972906 | 14606 49591 | 8623 7138 229514 32.2 | 16.541 % | #### 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.91 0.97 0.91 2/54 8851 Raw data (stat): 8851 (runsolver) R 8850 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487279550 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.9997 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1240 0 0 0 995 4 0 0 25 0 1 0 487279550 6578176 1218 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1606 1218 603 41 0 1565 0 vsize: 6424 [startup+20.0009 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1388 0 0 0 1994 5 0 0 25 0 1 0 487279550 7282688 1366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1778 1366 603 41 0 1737 0 vsize: 7112 [startup+30.0014 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1471 0 0 0 2993 5 0 0 25 0 1 0 487279550 7548928 1449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1843 1449 603 41 0 1802 0 vsize: 7372 [startup+40.0022 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1679 0 0 0 3993 6 0 0 25 0 1 0 487279550 8351744 1657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2039 1657 603 41 0 1998 0 vsize: 8156 [startup+50.0034 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1679 0 0 0 4993 6 0 0 25 0 1 0 487279550 8351744 1657 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2039 1657 603 41 0 1998 0 vsize: 8156 [startup+60.003 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1681 0 0 0 5993 6 0 0 25 0 1 0 487279550 8351744 1659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2039 1659 603 41 0 1998 0 vsize: 8156 [startup+70.004 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1683 0 0 0 6993 6 0 0 25 0 1 0 487279550 8351744 1661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2039 1661 603 41 0 1998 0 vsize: 8156 [startup+80.0051 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1741 0 0 0 7992 7 0 0 25 0 1 0 487279550 8736768 1719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2133 1719 603 41 0 2092 0 vsize: 8532 [startup+90.0055 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1741 0 0 0 8992 7 0 0 25 0 1 0 487279550 8736768 1719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2133 1719 603 41 0 2092 0 vsize: 8532 [startup+100.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1893 0 0 0 9992 7 0 0 25 0 1 0 487279550 9269248 1871 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2263 1871 603 41 0 2222 0 vsize: 9052 [startup+110.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1893 0 0 0 10992 7 0 0 25 0 1 0 487279550 9269248 1871 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2263 1871 603 41 0 2222 0 vsize: 9052 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1893 0 0 0 11992 7 0 0 25 0 1 0 487279550 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2263 1871 603 41 0 2222 0 vsize: 9052 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1893 0 0 0 12993 7 0 0 25 0 1 0 487279550 9269248 1871 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2263 1871 603 41 0 2222 0 vsize: 9052 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1893 0 0 0 13993 7 0 0 25 0 1 0 487279550 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2263 1871 603 41 0 2222 0 vsize: 9052 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 1914 0 0 0 14992 7 0 0 25 0 1 0 487279550 9400320 1892 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2295 1892 603 41 0 2254 0 vsize: 9180 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2022 0 0 0 15991 8 0 0 25 0 1 0 487279550 9805824 2000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2394 2000 603 41 0 2353 0 vsize: 9576 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2089 0 0 0 16990 9 0 0 25 0 1 0 487279550 10072064 2067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2459 2067 603 41 0 2418 0 vsize: 9836 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2175 0 0 0 17990 9 0 0 25 0 1 0 487279550 10477568 2153 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2153 603 41 0 2517 0 vsize: 10232 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 18990 10 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 19989 10 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 20989 10 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 21989 11 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+230.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 22989 11 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 23989 11 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 24988 12 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2178 0 0 0 25988 12 0 0 25 0 1 0 487279550 10477568 2156 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2558 2156 603 41 0 2517 0 vsize: 10232 [startup+270.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2199 0 0 0 26988 12 0 0 25 0 1 0 487279550 10612736 2177 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2591 2177 603 41 0 2550 0 vsize: 10364 [startup+280.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2200 0 0 0 27988 12 0 0 25 0 1 0 487279550 10612736 2178 4294967295 134512640 134672761 3221224544 3221223692 134559754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2591 2178 603 41 0 2550 0 vsize: 10364 [startup+290.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2263 0 0 0 28988 13 0 0 25 0 1 0 487279550 10883072 2241 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2657 2241 603 41 0 2616 0 vsize: 10628 [startup+300.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2266 0 0 0 29988 13 0 0 25 0 1 0 487279550 10883072 2244 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2657 2244 603 41 0 2616 0 vsize: 10628 [startup+310.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2282 0 0 0 30987 14 0 0 25 0 1 0 487279550 10883072 2260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2657 2260 603 41 0 2616 0 vsize: 10628 [startup+320.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2373 0 0 0 31987 14 0 0 25 0 1 0 487279550 11276288 2351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2351 603 41 0 2712 0 vsize: 11012 [startup+330.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2381 0 0 0 32987 14 0 0 25 0 1 0 487279550 11276288 2359 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2359 603 41 0 2712 0 vsize: 11012 [startup+340.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2600 0 0 0 33986 15 0 0 25 0 1 0 487279550 12214272 2578 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2578 603 41 0 2941 0 vsize: 11928 [startup+350.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 34986 15 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223728 134558671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+360.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 35986 15 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+370.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 36986 16 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 37986 16 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 38986 16 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223648 134560483 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+400.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 39985 17 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 40985 17 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+420.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 41985 17 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+430.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 42985 17 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+440.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 43985 18 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+450.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 44985 18 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 45984 19 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+470.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 46984 19 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223728 134558859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 47984 19 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+490.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2603 0 0 0 48984 19 0 0 25 0 1 0 487279550 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2982 2581 603 41 0 2941 0 vsize: 11928 [startup+500.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2672 0 0 0 49984 20 0 0 25 0 1 0 487279550 12480512 2650 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3047 2650 603 41 0 3006 0 vsize: 12188 [startup+510.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 50983 20 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+520.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 51983 20 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+530.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 52983 21 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+540.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 53983 21 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+550.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 54983 21 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+560.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 55982 21 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+570.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2687 0 0 0 56982 22 0 0 25 0 1 0 487279550 12615680 2665 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2665 603 41 0 3039 0 vsize: 12320 [startup+580.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2688 0 0 0 57982 22 0 0 25 0 1 0 487279550 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2666 603 41 0 3039 0 vsize: 12320 [startup+590.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2688 0 0 0 58982 22 0 0 25 0 1 0 487279550 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2666 603 41 0 3039 0 vsize: 12320 [startup+600.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2688 0 0 0 59982 22 0 0 25 0 1 0 487279550 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3080 2666 603 41 0 3039 0 vsize: 12320 [startup+610.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2732 0 0 0 60982 23 0 0 25 0 1 0 487279550 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2710 603 41 0 3071 0 vsize: 12448 [startup+620.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2732 0 0 0 61981 23 0 0 25 0 1 0 487279550 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2710 603 41 0 3071 0 vsize: 12448 [startup+630.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2732 0 0 0 62981 23 0 0 25 0 1 0 487279550 12746752 2710 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2710 603 41 0 3071 0 vsize: 12448 [startup+640.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2732 0 0 0 63981 24 0 0 25 0 1 0 487279550 12746752 2710 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2710 603 41 0 3071 0 vsize: 12448 [startup+650.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2732 0 0 0 64981 24 0 0 25 0 1 0 487279550 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2710 603 41 0 3071 0 vsize: 12448 [startup+660.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2737 0 0 0 65980 24 0 0 25 0 1 0 487279550 12746752 2715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2715 603 41 0 3071 0 vsize: 12448 [startup+670.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2746 0 0 0 66980 25 0 0 25 0 1 0 487279550 12746752 2724 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3112 2724 603 41 0 3071 0 vsize: 12448 [startup+680.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2853 0 0 0 67979 26 0 0 25 0 1 0 487279550 13283328 2831 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3243 2831 603 41 0 3202 0 vsize: 12972 [startup+690.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2856 0 0 0 68979 26 0 0 25 0 1 0 487279550 13283328 2834 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3243 2834 603 41 0 3202 0 vsize: 12972 [startup+700.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2965 0 0 0 69979 26 0 0 25 0 1 0 487279550 13680640 2943 4294967295 134512640 134672761 3221224544 3221223680 134565070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2943 603 41 0 3299 0 vsize: 13360 [startup+710.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2965 0 0 0 70979 26 0 0 25 0 1 0 487279550 13680640 2943 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2943 603 41 0 3299 0 vsize: 13360 [startup+720.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2965 0 0 0 71979 26 0 0 25 0 1 0 487279550 13680640 2943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2943 603 41 0 3299 0 vsize: 13360 [startup+730.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2969 0 0 0 72980 26 0 0 25 0 1 0 487279550 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2947 603 41 0 3299 0 vsize: 13360 [startup+740.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2969 0 0 0 73980 26 0 0 25 0 1 0 487279550 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2947 603 41 0 3299 0 vsize: 13360 [startup+750.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2969 0 0 0 74980 26 0 0 25 0 1 0 487279550 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2947 603 41 0 3299 0 vsize: 13360 [startup+760.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2969 0 0 0 75980 26 0 0 25 0 1 0 487279550 13680640 2947 4294967295 134512640 134672761 3221224544 3221223680 134565121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3340 2947 603 41 0 3299 0 vsize: 13360 [startup+770.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2971 0 0 0 76979 27 0 0 25 0 1 0 487279550 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3340 2949 603 41 0 3299 0 vsize: 13360 [startup+780.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2971 0 0 0 77979 27 0 0 25 0 1 0 487279550 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2949 603 41 0 3299 0 vsize: 13360 [startup+790.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2971 0 0 0 78979 27 0 0 25 0 1 0 487279550 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2949 603 41 0 3299 0 vsize: 13360 [startup+800.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2971 0 0 0 79979 27 0 0 25 0 1 0 487279550 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2949 603 41 0 3299 0 vsize: 13360 [startup+810.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2981 0 0 0 80979 27 0 0 25 0 1 0 487279550 13819904 2959 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2959 603 41 0 3333 0 vsize: 13496 [startup+820.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2985 0 0 0 81980 27 0 0 25 0 1 0 487279550 13819904 2963 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2963 603 41 0 3333 0 vsize: 13496 [startup+830.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 2985 0 0 0 82980 27 0 0 25 0 1 0 487279550 13819904 2963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3374 2963 603 41 0 3333 0 vsize: 13496 [startup+840.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3036 0 0 0 83980 27 0 0 25 0 1 0 487279550 13950976 3014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3406 3014 603 41 0 3365 0 vsize: 13624 [startup+850.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3081 0 0 0 84981 27 0 0 25 0 1 0 487279550 14225408 3059 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3473 3059 603 41 0 3432 0 vsize: 13892 [startup+860.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3175 0 0 0 85980 27 0 0 25 0 1 0 487279550 14618624 3153 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3569 3153 603 41 0 3528 0 vsize: 14276 [startup+870.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3177 0 0 0 86981 27 0 0 25 0 1 0 487279550 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3569 3155 603 41 0 3528 0 vsize: 14276 [startup+880.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3177 0 0 0 87981 27 0 0 25 0 1 0 487279550 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3569 3155 603 41 0 3528 0 vsize: 14276 [startup+890.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3177 0 0 0 88981 27 0 0 25 0 1 0 487279550 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3569 3155 603 41 0 3528 0 vsize: 14276 [startup+900.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3180 0 0 0 89980 27 0 0 25 0 1 0 487279550 14618624 3158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3569 3158 603 41 0 3528 0 vsize: 14276 [startup+910.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3212 0 0 0 90980 28 0 0 25 0 1 0 487279550 14766080 3190 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3605 3190 603 41 0 3564 0 vsize: 14420 [startup+920.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3215 0 0 0 91980 28 0 0 25 0 1 0 487279550 14766080 3193 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3605 3193 603 41 0 3564 0 vsize: 14420 [startup+930.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3239 0 0 0 92981 28 0 0 25 0 1 0 487279550 14929920 3217 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3217 603 41 0 3604 0 vsize: 14580 [startup+940.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3240 0 0 0 93981 28 0 0 25 0 1 0 487279550 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3218 603 41 0 3604 0 vsize: 14580 [startup+950.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3240 0 0 0 94981 28 0 0 25 0 1 0 487279550 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3218 603 41 0 3604 0 vsize: 14580 [startup+960.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3240 0 0 0 95981 28 0 0 25 0 1 0 487279550 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3218 603 41 0 3604 0 vsize: 14580 [startup+970.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3255 0 0 0 96981 28 0 0 25 0 1 0 487279550 14929920 3233 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3233 603 41 0 3604 0 vsize: 14580 [startup+980.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3256 0 0 0 97982 28 0 0 25 0 1 0 487279550 14929920 3234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3234 603 41 0 3604 0 vsize: 14580 [startup+990.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3262 0 0 0 98982 28 0 0 25 0 1 0 487279550 14929920 3240 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3240 603 41 0 3604 0 vsize: 14580 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3266 0 0 0 99982 28 0 0 25 0 1 0 487279550 14929920 3244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3645 3244 603 41 0 3604 0 vsize: 14580 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3281 0 0 0 100982 28 0 0 25 0 1 0 487279550 15077376 3259 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3681 3259 603 41 0 3640 0 vsize: 14724 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3293 0 0 0 101982 28 0 0 25 0 1 0 487279550 15077376 3271 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3681 3271 603 41 0 3640 0 vsize: 14724 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3293 0 0 0 102982 28 0 0 25 0 1 0 487279550 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3681 3271 603 41 0 3640 0 vsize: 14724 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3293 0 0 0 103982 28 0 0 25 0 1 0 487279550 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3681 3271 603 41 0 3640 0 vsize: 14724 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3293 0 0 0 104983 28 0 0 25 0 1 0 487279550 15077376 3271 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3681 3271 603 41 0 3640 0 vsize: 14724 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3299 0 0 0 105983 28 0 0 25 0 1 0 487279550 15241216 3277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3721 3277 603 41 0 3680 0 vsize: 14884 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3299 0 0 0 106983 28 0 0 25 0 1 0 487279550 15241216 3277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3721 3277 603 41 0 3680 0 vsize: 14884 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3333 0 0 0 107983 28 0 0 25 0 1 0 487279550 15372288 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3753 3311 603 41 0 3712 0 vsize: 15012 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3335 0 0 0 108983 28 0 0 25 0 1 0 487279550 15372288 3313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3753 3313 603 41 0 3712 0 vsize: 15012 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3337 0 0 0 109984 28 0 0 25 0 1 0 487279550 15372288 3315 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3753 3315 603 41 0 3712 0 vsize: 15012 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3401 0 0 0 110983 28 0 0 25 0 1 0 487279550 15638528 3379 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3818 3379 603 41 0 3777 0 vsize: 15272 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3406 0 0 0 111983 28 0 0 25 0 1 0 487279550 15638528 3384 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3818 3384 603 41 0 3777 0 vsize: 15272 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3413 0 0 0 112983 28 0 0 25 0 1 0 487279550 15638528 3391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3818 3391 603 41 0 3777 0 vsize: 15272 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3421 0 0 0 113983 28 0 0 25 0 1 0 487279550 15638528 3399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3818 3399 603 41 0 3777 0 vsize: 15272 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3439 0 0 0 114984 28 0 0 25 0 1 0 487279550 15769600 3417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3850 3417 603 41 0 3809 0 vsize: 15400 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3554 0 0 0 115984 28 0 0 25 0 1 0 487279550 16310272 3532 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3982 3532 603 41 0 3941 0 vsize: 15928 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3562 0 0 0 116984 28 0 0 25 0 1 0 487279550 16310272 3540 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3982 3540 603 41 0 3941 0 vsize: 15928 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3562 0 0 0 117984 29 0 0 25 0 1 0 487279550 16310272 3540 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3982 3540 603 41 0 3941 0 vsize: 15928 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3562 0 0 0 118984 29 0 0 25 0 1 0 487279550 16310272 3540 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3982 3540 603 41 0 3941 0 vsize: 15928 [startup+1200.07 s] Raw data (loadavg): 1.07 0.99 0.92 2/54 8851 Raw data (stat): 8851 (minisat+) R 8850 5897 5896 0 -1 0 3562 0 0 0 119984 29 0 0 25 0 1 0 487279550 16310272 3540 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3982 3540 603 41 0 3941 0 vsize: 15928 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 1.07 0.99 0.92 1/54 8851 Raw data (stat): 8851 (minisat+) Z 8850 5897 5896 0 -1 12 3565 0 0 0 119984 29 0 0 25 0 1 0 487279550 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.08 CPU time (s): 1200.15 CPU user time (s): 1199.85 CPU system time (s): 0.297954 CPU usage (%): 100.006 Max. virtual memory (Kb): 15928 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####