Name | normalized-opb/submitted/manquinho/logic-synthesis/normalized-count.b.opb |
MD5SUM | f13ba9c997276002b5bd6db1f679a6f5 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 24 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 467 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 467 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 467 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04584 |
Number of variables | 466 |
Total number of constraints | 694 |
Number of constraints which are clauses | 694 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 78 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-13 19:42:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3449 boxname=wulflinc7 idbench=65 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f13ba9c997276002b5bd6db1f679a6f5 /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb IDLAUNCH: 3449 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 918852 kB Buffers: 36568 kB Cached: 60196 kB SwapCached: 0 kB Active: 71992 kB Inactive: 27628 kB HighTotal: 131008 kB HighFree: 66920 kB LowTotal: 903652 kB LowFree: 851932 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 10760 kB Committed_AS: 63472 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:03:06 (client local time) WITH STATUS 10 IN 1209.97 SECONDS stats: 3449 7 1209.97 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 694 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 694 17335 | 231 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 922 maxlim: 436 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 7110 40242 | 2370 0 0 nan | 0.000 % | c | 101 | 7110 40242 | 2607 101 393 3.9 | 0.502 % | c | 252 | 7085 40159 | 2867 248 1017 4.1 | 0.789 % | c | 479 | 7085 40159 | 3154 475 2831 6.0 | 0.789 % | c | 816 | 7085 40159 | 3469 812 7492 9.2 | 0.789 % | c | 1322 | 7061 40077 | 3816 1313 24085 18.3 | 1.076 % | c | 2081 | 7061 40077 | 4198 2072 53707 25.9 | 1.076 % | c | 3221 | 7048 40033 | 4618 3208 115274 35.9 | 1.291 % | c | 4929 | 7048 40033 | 5080 2525 99100 39.2 | 1.291 % | c ============================================================================== c [1mFound solution: 29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 438 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5420 | 7054 40064 | 2351 3016 150367 49.9 | 1.291 % | c | 5522 | 7054 40064 | 2586 1610 45952 28.5 | 1.433 % | c | 5674 | 7054 40064 | 2844 1762 49846 28.3 | 1.433 % | c | 5901 | 7054 40064 | 3129 1989 59731 30.0 | 1.433 % | c | 6238 | 7054 40064 | 3442 2326 73345 31.5 | 1.433 % | c | 6745 | 7054 40064 | 3786 2833 97149 34.3 | 1.433 % | c | 7505 | 7054 40064 | 4164 3593 154807 43.1 | 1.433 % | c | 8648 | 7054 40064 | 4581 2397 75310 31.4 | 1.433 % | c | 10357 | 7054 40064 | 5039 4106 191200 46.6 | 1.433 % | c | 12919 | 7054 40064 | 5543 4029 156820 38.9 | 1.433 % | c | 16763 | 7054 40064 | 6097 4939 303955 61.5 | 1.433 % | c ============================================================================== c [1mFound solution: 28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 439 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18018 | 7029 39979 | 2343 6186 398934 64.5 | 1.433 % | c | 18118 | 7029 39979 | 2577 1647 37724 22.9 | 1.790 % | c | 18268 | 7029 39979 | 2835 1797 44606 24.8 | 1.790 % | c | 18493 | 7029 39979 | 3118 2022 53892 26.7 | 1.790 % | c | 18830 | 7029 39979 | 3430 2359 73429 31.1 | 1.790 % | c | 19337 | 7029 39979 | 3773 2866 105054 36.7 | 1.790 % | c | 20096 | 7029 39979 | 4150 3625 151110 41.7 | 1.790 % | c | 21235 | 7029 39979 | 4565 2554 89975 35.2 | 1.790 % | c | 22949 | 7029 39979 | 5022 4268 234958 55.1 | 1.790 % | c | 25512 | 7029 39979 | 5524 4220 230171 54.5 | 1.790 % | c | 29356 | 7006 39900 | 6077 5156 279123 54.1 | 2.076 % | c ============================================================================== c [1mFound solution: 27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 440 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32912 | 7009 39914 | 2336 5492 322571 58.7 | 2.076 % | c | 33012 | 7009 39914 | 2569 1473 26068 17.7 | 2.146 % | c | 33162 | 7009 39914 | 2826 1623 30813 19.0 | 2.146 % | c | 33388 | 7009 39914 | 3109 1849 37520 20.3 | 2.146 % | c | 33725 | 7009 39914 | 3420 2186 58694 26.8 | 2.146 % | c | 34231 | 7009 39914 | 3762 2692 92786 34.5 | 2.146 % | c | 34992 | 7009 39914 | 4138 3453 143239 41.5 | 2.146 % | c | 36132 | 7009 39914 | 4552 2401 76246 31.8 | 2.146 % | c | 37842 | 7009 39914 | 5007 4111 169147 41.1 | 2.146 % | c | 40408 | 7009 39914 | 5508 4025 184357 45.8 | 2.146 % | c | 44252 | 7000 39883 | 6058 5034 273751 54.4 | 2.218 % | c ============================================================================== c [1mFound solution: 26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 441 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46493 | 7001 39890 | 2333 4149 216281 52.1 | 2.218 % | c | 46595 | 7001 39890 | 2566 2177 78882 36.2 | 2.287 % | c | 46747 | 7001 39890 | 2822 2329 82427 35.4 | 2.288 % | c | 46975 | 7001 39890 | 3105 2557 92633 36.2 | 2.287 % | c | 47313 | 7001 39890 | 3415 2895 114105 39.4 | 2.287 % | c | 47820 | 7001 39890 | 3757 3402 139889 41.1 | 2.287 % | c | 48581 | 7001 39890 | 4133 2193 62645 28.6 | 2.287 % | c | 49721 | 7001 39890 | 4546 3333 135828 40.8 | 2.287 % | c | 51429 | 7001 39890 | 5000 2613 118260 45.3 | 2.287 % | c | 53994 | 7001 39890 | 5501 5178 329833 63.7 | 2.288 % | c | 57840 | 6975 39800 | 6051 3301 150037 45.5 | 2.573 % | c | 63606 | 6975 39800 | 6656 5862 518264 88.4 | 2.573 % | c | 72255 | 6975 39800 | 7321 4182 308523 73.8 | 2.573 % | c | 85230 | 6975 39800 | 8054 5562 316547 56.9 | 2.573 % | c | 104692 | 6975 39800 | 8859 8323 489432 58.8 | 2.573 % | c | 133884 | 6975 39800 | 9745 5507 389569 70.7 | 2.573 % | c | 177674 | 6975 39800 | 10720 9526 718740 75.5 | 2.573 % | c | 243359 | 6975 39800 | 11792 9247 663097 71.7 | 2.573 % | c ============================================================================== c [1mFound solution: 25[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 442 bits: 9/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 320244 | 6976 39808 | 2325 6802 665186 97.8 | 2.573 % | c | 320344 | 6976 39808 | 2557 1801 48359 26.9 | 2.643 % | c | 320494 | 6976 39808 | 2813 1951 49295 25.3 | 2.643 % | c | 320720 | 6976 39808 | 3094 2177 56151 25.8 | 2.645 % | c | 321058 | 6976 39808 | 3404 2515 69890 27.8 | 2.643 % | c | 321566 | 6976 39808 | 3744 3023 99236 32.8 | 2.643 % | c | 322326 | 6976 39808 | 4118 3783 143580 38.0 | 2.643 % | c | 323465 | 6976 39808 | 4530 2783 95001 34.1 | 2.643 % | c | 325175 | 6976 39808 | 4983 4493 199268 44.4 | 2.643 % | c | 327737 | 6976 39808 | 5482 4386 217539 49.6 | 2.643 % | c | 331587 | 6976 39808 | 6030 5370 277732 51.7 | 2.643 % | c | 337355 | 6976 39808 | 6633 4895 175658 35.9 | 2.643 % | c | 346004 | 6976 39808 | 7296 6698 451883 67.5 | 2.643 % | c | 358978 | 6976 39808 | 8026 4617 255848 55.4 | 2.643 % | c | 378440 | 6976 39808 | 8829 7286 534197 73.3 | 2.643 % | c | 407632 | 6976 39808 | 9712 4672 235153 50.3 | 2.643 % | c | 451422 | 6976 39808 | 10683 8849 612372 69.2 | 2.643 % | c | 517107 | 6976 39808 | 11751 8467 791823 93.5 | 2.643 % | c | 615635 | 6976 39808 | 12926 10995 934963 85.0 | 2.643 % | c | 763425 | 6976 39808 | 14219 13131 1159728 88.3 | 2.643 % | c | 985110 | 6976 39808 | 15641 9804 864343 88.2 | 2.643 % | c | 1317635 | 6976 39808 | 17205 9301 784747 84.4 | 2.643 % | #### 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.95 0.69 2/54 24846 Raw data (stat): 24846 (runsolver) R 24845 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420341765 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.93 0.95 0.69 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1003 0 0 0 996 2 0 0 25 0 1 0 420341765 5582848 981 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1363 981 603 41 0 1322 0 vsize: 5452 [startup+20.0016 s] Raw data (loadavg): 0.94 0.95 0.69 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1013 0 0 0 1995 2 0 0 25 0 1 0 420341765 5582848 991 4294967295 134512640 134672761 3221224576 3221223760 134558925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1363 991 603 41 0 1322 0 vsize: 5452 [startup+30.0025 s] Raw data (loadavg): 0.95 0.96 0.70 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1176 0 0 0 2995 3 0 0 25 0 1 0 420341765 6373376 1154 4294967295 134512640 134672761 3221224576 3221223760 134559559 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1556 1154 603 41 0 1515 0 vsize: 6224 [startup+40.0026 s] Raw data (loadavg): 0.95 0.96 0.70 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1461 0 0 0 3993 4 0 0 25 0 1 0 420341765 7446528 1439 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1818 1439 603 41 0 1777 0 vsize: 7272 [startup+50.0025 s] Raw data (loadavg): 0.96 0.96 0.70 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1466 0 0 0 4993 4 0 0 25 0 1 0 420341765 7593984 1444 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1854 1444 603 41 0 1813 0 vsize: 7416 [startup+60.0031 s] Raw data (loadavg): 0.97 0.96 0.71 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1467 0 0 0 5993 4 0 0 25 0 1 0 420341765 7593984 1445 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1854 1445 603 41 0 1813 0 vsize: 7416 [startup+70.0034 s] Raw data (loadavg): 0.97 0.96 0.71 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1467 0 0 0 6993 4 0 0 25 0 1 0 420341765 7593984 1445 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1854 1445 603 41 0 1813 0 vsize: 7416 [startup+80.0044 s] Raw data (loadavg): 0.98 0.96 0.71 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1840 0 0 0 7993 5 0 0 25 0 1 0 420341765 9068544 1818 4294967295 134512640 134672761 3221224576 3221222604 134566355 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2214 1818 603 41 0 2173 0 vsize: 8856 [startup+90.0043 s] Raw data (loadavg): 0.98 0.96 0.71 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 8993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2214 1819 603 41 0 2173 0 vsize: 8856 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.72 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 9993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2214 1819 603 41 0 2173 0 vsize: 8856 [startup+110.004 s] Raw data (loadavg): 0.98 0.96 0.72 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 10993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2214 1819 603 41 0 2173 0 vsize: 8856 [startup+120.005 s] Raw data (loadavg): 0.99 0.96 0.72 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1842 0 0 0 11993 5 0 0 25 0 1 0 420341765 9068544 1820 4294967295 134512640 134672761 3221224576 3221223760 134559055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2214 1820 603 41 0 2173 0 vsize: 8856 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.73 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1919 0 0 0 12993 5 0 0 25 0 1 0 420341765 9330688 1897 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2278 1897 603 41 0 2237 0 vsize: 9112 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.73 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 13993 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2313 1909 603 41 0 2272 0 vsize: 9252 [startup+150.005 s] Raw data (loadavg): 0.99 0.97 0.73 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 14994 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223680 134555126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2313 1909 603 41 0 2272 0 vsize: 9252 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.73 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 15994 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2313 1909 603 41 0 2272 0 vsize: 9252 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.73 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2117 0 0 0 16994 5 0 0 25 0 1 0 420341765 10141696 2095 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2476 2095 603 41 0 2435 0 vsize: 9904 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.74 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 17992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.74 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 18992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.74 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 19992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.74 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 20993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.74 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 21993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+230.008 s] Raw data (loadavg): 0.99 0.97 0.75 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 22993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2640 2248 603 41 0 2599 0 vsize: 10560 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.75 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2619 0 0 0 23992 7 0 0 25 0 1 0 420341765 12279808 2597 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2998 2597 603 41 0 2957 0 vsize: 11992 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.75 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 24993 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.75 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 25992 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 26992 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.76 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 27992 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.76 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 28991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+300.012 s] Raw data (loadavg): 0.99 0.97 0.76 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 29991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.76 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 30991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+320.013 s] Raw data (loadavg): 0.99 0.97 0.76 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 31991 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+330.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 32990 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 33990 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 34989 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223532 1075350145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+360.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 35989 10 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+370.015 s] Raw data (loadavg): 0.99 0.97 0.77 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 36988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+380.016 s] Raw data (loadavg): 0.99 0.97 0.78 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 37988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223816 134564425 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+390.017 s] Raw data (loadavg): 0.99 0.97 0.78 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 38988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223576 1075350763 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+400.016 s] Raw data (loadavg): 0.99 0.97 0.78 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 39987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+410.017 s] Raw data (loadavg): 0.99 0.97 0.78 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 40987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+420.018 s] Raw data (loadavg): 0.99 0.97 0.78 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 41987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+430.019 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 42987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+440.019 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 43986 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+450.019 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 44986 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+460.02 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 45985 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+470.02 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 46985 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2990 2600 603 41 0 2949 0 vsize: 11960 [startup+480.02 s] Raw data (loadavg): 0.99 0.97 0.79 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 47984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2721 603 41 0 3083 0 vsize: 12496 [startup+490.02 s] Raw data (loadavg): 0.99 0.97 0.80 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 48984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2721 603 41 0 3083 0 vsize: 12496 [startup+500.021 s] Raw data (loadavg): 0.99 0.97 0.80 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 49984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2721 603 41 0 3083 0 vsize: 12496 [startup+510.022 s] Raw data (loadavg): 0.99 0.97 0.80 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 50983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2722 603 41 0 3083 0 vsize: 12496 [startup+520.022 s] Raw data (loadavg): 0.99 0.97 0.80 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 51983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2722 603 41 0 3083 0 vsize: 12496 [startup+530.022 s] Raw data (loadavg): 0.99 0.97 0.80 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 52983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2722 603 41 0 3083 0 vsize: 12496 [startup+540.023 s] Raw data (loadavg): 0.99 0.97 0.81 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 53982 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2722 603 41 0 3083 0 vsize: 12496 [startup+550.022 s] Raw data (loadavg): 0.99 0.97 0.81 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2753 0 0 0 54982 16 0 0 25 0 1 0 420341765 12795904 2731 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3124 2731 603 41 0 3083 0 vsize: 12496 [startup+560.023 s] Raw data (loadavg): 0.99 0.97 0.81 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 55981 16 0 0 25 0 1 0 420341765 13066240 2785 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3190 2785 603 41 0 3149 0 vsize: 12760 [startup+570.024 s] Raw data (loadavg): 0.99 0.97 0.81 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 56981 16 0 0 25 0 1 0 420341765 13066240 2785 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3190 2785 603 41 0 3149 0 vsize: 12760 [startup+580.024 s] Raw data (loadavg): 0.99 0.97 0.81 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 57981 17 0 0 25 0 1 0 420341765 13053952 2785 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2785 603 41 0 3146 0 vsize: 12748 [startup+590.024 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 58980 17 0 0 25 0 1 0 420341765 13053952 2785 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2785 603 41 0 3146 0 vsize: 12748 [startup+600.024 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 59980 17 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2795 603 41 0 3146 0 vsize: 12748 [startup+610.025 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 60979 18 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2795 603 41 0 3146 0 vsize: 12748 [startup+620.025 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 61979 18 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223760 134559514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2795 603 41 0 3146 0 vsize: 12748 [startup+630.025 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2824 0 0 0 62979 18 0 0 25 0 1 0 420341765 13053952 2802 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2802 603 41 0 3146 0 vsize: 12748 [startup+640.025 s] Raw data (loadavg): 0.99 0.97 0.82 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2824 0 0 0 63978 19 0 0 25 0 1 0 420341765 13053952 2802 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3187 2802 603 41 0 3146 0 vsize: 12748 [startup+650.026 s] Raw data (loadavg): 1.07 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2927 0 0 0 64977 20 0 0 25 0 1 0 420341765 13455360 2905 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3285 2905 603 41 0 3244 0 vsize: 13140 [startup+660.026 s] Raw data (loadavg): 1.06 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2940 0 0 0 65977 20 0 0 25 0 1 0 420341765 13594624 2918 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3319 2918 603 41 0 3278 0 vsize: 13276 [startup+670.026 s] Raw data (loadavg): 1.05 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2966 0 0 0 66977 20 0 0 25 0 1 0 420341765 13729792 2944 4294967295 134512640 134672761 3221224576 3221223680 134560231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2944 603 41 0 3311 0 vsize: 13408 [startup+680.027 s] Raw data (loadavg): 1.04 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2972 0 0 0 67976 21 0 0 25 0 1 0 420341765 13729792 2950 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2950 603 41 0 3311 0 vsize: 13408 [startup+690.027 s] Raw data (loadavg): 1.03 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2972 0 0 0 68976 21 0 0 25 0 1 0 420341765 13729792 2950 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2950 603 41 0 3311 0 vsize: 13408 [startup+700.027 s] Raw data (loadavg): 1.03 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2983 0 0 0 69976 21 0 0 25 0 1 0 420341765 13729792 2961 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2961 603 41 0 3311 0 vsize: 13408 [startup+710.028 s] Raw data (loadavg): 1.02 0.99 0.83 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2983 0 0 0 70975 21 0 0 25 0 1 0 420341765 13729792 2961 4294967295 134512640 134672761 3221224576 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2961 603 41 0 3311 0 vsize: 13408 [startup+720.029 s] Raw data (loadavg): 1.02 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2984 0 0 0 71975 22 0 0 25 0 1 0 420341765 13729792 2962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2962 603 41 0 3311 0 vsize: 13408 [startup+730.028 s] Raw data (loadavg): 1.02 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2986 0 0 0 72975 22 0 0 25 0 1 0 420341765 13729792 2964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3352 2964 603 41 0 3311 0 vsize: 13408 [startup+740.029 s] Raw data (loadavg): 1.01 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 73974 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3153 603 41 0 3507 0 vsize: 14192 [startup+750.029 s] Raw data (loadavg): 1.01 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 74973 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223576 1075349975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3153 603 41 0 3507 0 vsize: 14192 [startup+760.029 s] Raw data (loadavg): 1.01 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 75973 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3153 603 41 0 3507 0 vsize: 14192 [startup+770.029 s] Raw data (loadavg): 1.01 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 76973 23 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+780.03 s] Raw data (loadavg): 1.00 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 77972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+790.03 s] Raw data (loadavg): 1.00 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 78972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+800.03 s] Raw data (loadavg): 1.00 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 79972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+810.031 s] Raw data (loadavg): 1.00 0.99 0.84 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 80971 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+820.031 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 81971 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+830.031 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 82971 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+840.032 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 83970 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+850.031 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 84969 26 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+860.032 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 85969 26 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3548 3154 603 41 0 3507 0 vsize: 14192 [startup+870.033 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 86969 26 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3647 3245 603 41 0 3606 0 vsize: 14588 [startup+880.033 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 87969 26 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3647 3245 603 41 0 3606 0 vsize: 14588 [startup+890.033 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 88968 27 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3647 3245 603 41 0 3606 0 vsize: 14588 [startup+900.033 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3328 0 0 0 89968 27 0 0 25 0 1 0 420341765 15216640 3306 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3306 603 41 0 3674 0 vsize: 14860 [startup+910.034 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 90967 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3310 603 41 0 3674 0 vsize: 14860 [startup+920.034 s] Raw data (loadavg): 1.00 0.99 0.85 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 91967 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3310 603 41 0 3674 0 vsize: 14860 [startup+930.034 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 92966 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3310 603 41 0 3674 0 vsize: 14860 [startup+940.034 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 93966 29 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223760 134559327 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3310 603 41 0 3674 0 vsize: 14860 [startup+950.034 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 94965 29 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223728 134565116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+960.035 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 95965 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+970.035 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 96964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+980.035 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 97964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+990.036 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 98964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223776 134557796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+1000.04 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 99963 31 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3316 603 41 0 3674 0 vsize: 14860 [startup+1010.04 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3344 0 0 0 100963 31 0 0 25 0 1 0 420341765 15216640 3322 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3715 3322 603 41 0 3674 0 vsize: 14860 [startup+1020.04 s] Raw data (loadavg): 1.00 0.99 0.86 2/54 24846 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3350 0 0 0 101963 31 0 0 25 0 1 0 420341765 15364096 3328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3751 3328 603 41 0 3710 0 vsize: 15004 [startup+1030.04 s] Raw data (loadavg): 1.00 0.99 0.87 2/57 24849 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3357 0 0 0 102959 35 0 0 25 0 1 0 420341765 15364096 3335 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3335 603 41 0 3710 0 vsize: 15004 [startup+1040.04 s] Raw data (loadavg): 1.07 1.00 0.87 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3357 0 0 0 103958 35 0 0 25 0 1 0 420341765 15364096 3335 4294967295 134512640 134672761 3221224576 3221223680 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3335 603 41 0 3710 0 vsize: 15004 [startup+1050.04 s] Raw data (loadavg): 1.06 1.00 0.87 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 104958 35 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1060.04 s] Raw data (loadavg): 1.05 1.00 0.87 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 105958 35 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1070.04 s] Raw data (loadavg): 1.04 1.00 0.87 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 106959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1080.04 s] Raw data (loadavg): 1.04 1.00 0.88 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 107959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1090.04 s] Raw data (loadavg): 1.03 1.00 0.88 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 108959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1100.04 s] Raw data (loadavg): 1.02 1.00 0.88 2/54 24899 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 109959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3751 3354 603 41 0 3710 0 vsize: 15004 [startup+1110.04 s] Raw data (loadavg): 1.02 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3436 0 0 0 110959 36 0 0 25 0 1 0 420341765 15626240 3414 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3815 3414 603 41 0 3774 0 vsize: 15260 [startup+1120.04 s] Raw data (loadavg): 1.02 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3493 0 0 0 111959 36 0 0 25 0 1 0 420341765 15892480 3471 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3880 3471 603 41 0 3839 0 vsize: 15520 [startup+1130.04 s] Raw data (loadavg): 1.01 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3512 0 0 0 112959 36 0 0 25 0 1 0 420341765 16056320 3490 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3920 3490 603 41 0 3879 0 vsize: 15680 [startup+1140.04 s] Raw data (loadavg): 1.01 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 113959 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3920 3496 603 41 0 3879 0 vsize: 15680 [startup+1150.04 s] Raw data (loadavg): 1.01 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 114959 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3920 3496 603 41 0 3879 0 vsize: 15680 [startup+1160.04 s] Raw data (loadavg): 1.01 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 115960 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3920 3496 603 41 0 3879 0 vsize: 15680 [startup+1170.04 s] Raw data (loadavg): 1.01 1.00 0.88 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3561 0 0 0 116960 36 0 0 25 0 1 0 420341765 16191488 3539 4294967295 134512640 134672761 3221224576 3221223760 134559609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3953 3539 603 41 0 3912 0 vsize: 15812 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.89 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3569 0 0 0 117960 36 0 0 25 0 1 0 420341765 16330752 3547 4294967295 134512640 134672761 3221224576 3221222592 134565819 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3987 3547 603 41 0 3946 0 vsize: 15948 [startup+1190.04 s] Raw data (loadavg): 1.00 1.00 0.89 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3645 0 0 0 118960 36 0 0 25 0 1 0 420341765 16601088 3623 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4053 3623 603 41 0 4012 0 vsize: 16212 [startup+1200.03 s] Raw data (loadavg): 1.00 1.00 0.89 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3837 0 0 0 119959 37 0 0 25 0 1 0 420341765 17432576 3815 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4256 3815 603 41 0 4215 0 vsize: 17024 [startup+1210.04 s] Raw data (loadavg): 1.00 1.00 0.89 2/54 24901 Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3855 0 0 0 120959 37 0 0 25 0 1 0 420341765 17596416 3833 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4296 3833 603 41 0 4255 0 vsize: 17184 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1210.05 s] Raw data (loadavg): 1.00 1.00 0.89 1/54 24901 Raw data (stat): 24846 (minisat+) Z 24845 22932 22931 0 -1 12 3858 0 0 0 120959 38 0 0 25 0 1 0 420341765 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): 1210.05 CPU time (s): 1209.97 CPU user time (s): 1209.59 CPU system time (s): 0.381941 CPU usage (%): 99.994 Max. virtual memory (Kb): 17184 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####