Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb |
MD5SUM | 70070c820bc7d178cc8f33b42e0deead |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
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 | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 28143 |
Number of constraints which are clauses | 28143 |
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 | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-13 22:50:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3707 boxname=wulflinc12 idbench=323 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 70070c820bc7d178cc8f33b42e0deead /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb IDLAUNCH: 3707 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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: 918032 kB Buffers: 34796 kB Cached: 62632 kB SwapCached: 16 kB Active: 60384 kB Inactive: 39860 kB HighTotal: 131008 kB HighFree: 64512 kB LowTotal: 903652 kB LowFree: 853520 kB SwapTotal: 2097136 kB SwapFree: 2097120 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 10948 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 23:10:42 (client local time) WITH STATUS 10 IN 1200.17 SECONDS stats: 3707 7 1200.17 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28143 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 | 28143 56286 | 9381 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -21[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1165 maxlim: 21 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 36101 84741 | 12033 0 0 nan | 0.000 % | c | 100 | 36101 84741 | 13236 100 1163 11.6 | 0.177 % | c | 250 | 36101 84741 | 14559 250 2484 9.9 | 0.172 % | c ============================================================================== c [1mFound solution: -22[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 365 | 36110 84780 | 12036 365 3527 9.7 | 0.172 % | c | 465 | 36110 84780 | 13239 465 5075 10.9 | 0.232 % | c | 617 | 36101 84749 | 14563 610 6239 10.2 | 0.286 % | c ============================================================================== c [1mFound solution: -23[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 741 | 36102 84753 | 12034 734 7681 10.5 | 0.286 % | c | 844 | 36093 84722 | 13237 834 9135 11.0 | 0.400 % | c ============================================================================== c [1mFound solution: -24[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 24 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 930 | 36096 84735 | 12032 920 10039 10.9 | 0.400 % | c | 1030 | 36087 84704 | 13235 1017 11684 11.5 | 0.519 % | c | 1181 | 36063 84622 | 14558 1163 14118 12.1 | 0.691 % | c | 1406 | 36054 84591 | 16014 1386 17386 12.5 | 0.743 % | c | 1744 | 36027 84498 | 17616 1716 22319 13.0 | 0.919 % | c ============================================================================== c [1mFound solution: -25[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 25 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1883 | 36028 84504 | 12009 1855 25294 13.6 | 0.919 % | c | 1983 | 36028 84504 | 13209 1955 26238 13.4 | 0.971 % | c | 2133 | 36019 84473 | 14530 2102 28249 13.4 | 1.033 % | c | 2361 | 36010 84442 | 15983 2326 33754 14.5 | 1.085 % | c | 2698 | 35956 84256 | 17582 2646 39058 14.8 | 1.432 % | c | 3205 | 35899 84061 | 19340 3137 49155 15.7 | 1.832 % | c | 3964 | 35480 82628 | 21274 3764 63671 16.9 | 4.969 % | c ============================================================================== c [1mFound solution: -26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 26 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4515 | 35341 82153 | 11780 4272 74597 17.5 | 4.969 % | c | 4615 | 35341 82153 | 12958 4372 77222 17.7 | 6.221 % | c | 4765 | 35332 82122 | 14253 4519 80061 17.7 | 6.279 % | c | 4990 | 35237 81795 | 15679 4720 83804 17.8 | 7.078 % | c | 5327 | 35177 81587 | 17247 5043 96133 19.1 | 7.648 % | c | 5833 | 35069 81219 | 18971 5521 113249 20.5 | 8.448 % | c ============================================================================== c [1mFound solution: -27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 27 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6483 | 34835 80411 | 11611 6092 133615 21.9 | 8.448 % | c | 6583 | 34744 80098 | 12772 6166 136198 22.1 | 11.585 % | c | 6733 | 34744 80098 | 14049 6316 140060 22.2 | 11.580 % | c | 6959 | 34726 80036 | 15454 6536 147481 22.6 | 11.694 % | c | 7297 | 34708 79974 | 16999 6867 157111 22.9 | 11.814 % | c | 7805 | 34616 79654 | 18699 7341 174815 23.8 | 12.611 % | c | 8564 | 34581 79533 | 20569 8061 207977 25.8 | 12.892 % | c | 9705 | 34519 79319 | 22626 9184 311530 33.9 | 13.463 % | c ============================================================================== c [1mFound solution: -28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 28 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10256 | 34446 79070 | 11482 9682 335078 34.6 | 13.463 % | c | 10356 | 34429 79011 | 12630 9773 336266 34.4 | 14.310 % | c | 10506 | 34429 79011 | 13893 9923 348268 35.1 | 14.310 % | c | 10733 | 34401 78917 | 15282 10142 360700 35.6 | 14.652 % | c | 11071 | 34375 78827 | 16810 10437 379825 36.4 | 14.880 % | c | 11577 | 34317 78625 | 18491 10931 415056 38.0 | 15.450 % | c | 12336 | 34292 78538 | 20341 11686 465604 39.8 | 15.741 % | c | 13475 | 34239 78355 | 22375 12808 565144 44.1 | 16.253 % | c | 15183 | 34177 78143 | 24612 14428 659625 45.7 | 16.762 % | c | 17745 | 34115 77931 | 27073 16966 963360 56.8 | 17.446 % | c | 21589 | 33845 76997 | 29781 20555 1183069 57.6 | 20.074 % | c | 27356 | 33834 76958 | 32759 26318 1847608 70.2 | 20.187 % | c | 36006 | 33834 76958 | 36035 15707 1114508 71.0 | 20.182 % | c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 29 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37004 | 33835 76964 | 11278 16705 1174855 70.3 | 20.182 % | c | 37104 | 33835 76964 | 12405 8453 514747 60.9 | 20.234 % | c | 37255 | 33835 76964 | 13646 8604 517801 60.2 | 20.228 % | c | 37480 | 33756 76691 | 15011 8819 525936 59.6 | 21.083 % | c | 37818 | 33756 76691 | 16512 9157 536437 58.6 | 21.083 % | c | 38324 | 33756 76691 | 18163 9663 567451 58.7 | 21.087 % | c | 39083 | 33734 76613 | 19979 10418 610457 58.6 | 21.311 % | c | 40222 | 33734 76613 | 21977 11557 718310 62.2 | 21.315 % | c | 41930 | 33725 76582 | 24175 13260 840942 63.4 | 21.368 % | c | 44492 | 33680 76429 | 26592 15796 1036951 65.6 | 21.716 % | c ============================================================================== c [1mFound solution: -30[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44944 | 33682 76438 | 11227 16248 1069251 65.8 | 21.716 % | c | 45045 | 33682 76438 | 12349 8225 494828 60.2 | 21.745 % | c | 45195 | 33682 76438 | 13584 8375 499675 59.7 | 21.742 % | c | 45420 | 33682 76438 | 14943 8600 507467 59.0 | 21.746 % | c | 45757 | 33682 76438 | 16437 8937 527977 59.1 | 21.748 % | c | 46264 | 33664 76376 | 18081 9416 553647 58.8 | 21.855 % | c | 47023 | 33636 76282 | 19889 10171 584191 57.4 | 22.197 % | c | 48162 | 33606 76176 | 21878 11297 663440 58.7 | 22.538 % | c | 49872 | 33606 76176 | 24066 13007 808827 62.2 | 22.544 % | c | 52434 | 33536 75932 | 26472 15556 998471 64.2 | 23.278 % | c | 56279 | 33536 75932 | 29119 19401 1384240 71.3 | 23.278 % | c | 62046 | 33536 75932 | 32031 25168 1934417 76.9 | 23.284 % | c | 70696 | 33463 75677 | 35235 15338 1064191 69.4 | 24.137 % | c | 83670 | 33454 75646 | 38758 28307 2294448 81.1 | 24.194 % | c | 103132 | 33404 75476 | 42634 22620 1640426 72.5 | 24.701 % | c | 132324 | 33404 75476 | 46897 22042 1951618 88.5 | 24.701 % | c | 176115 | 33239 74903 | 51587 31538 2912876 92.4 | 26.466 % | c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 31 bits: 6/5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 186700 | 33218 74803 | 11072 40948 3543868 86.5 | 26.466 % | c | 186801 | 33218 74803 | 12179 7164 364940 50.9 | 26.584 % | c | 186951 | 33218 74803 | 13397 7314 369609 50.5 | 26.579 % | c | 187177 | 33218 74803 | 14736 7540 381681 50.6 | 26.584 % | c | 187514 | 33210 74775 | 16210 7873 397823 50.5 | 26.698 % | c | 188020 | 33202 74747 | 17831 8375 427968 51.1 | 26.807 % | c | 188781 | 33202 74747 | 19614 9136 473935 51.9 | 26.807 % | c | 189921 | 33181 74672 | 21576 10267 526660 51.3 | 27.092 % | c | 191629 | 33181 74672 | 23733 11975 628906 52.5 | 27.096 % | c | 194192 | 33181 74672 | 26107 14538 791381 54.4 | 27.092 % | c | 198038 | 33181 74672 | 28717 18384 1043836 56.8 | 27.092 % | c | 203804 | 33181 74672 | 31589 24150 1601403 66.3 | 27.092 % | c | 212454 | 33181 74672 | 34748 32800 2608188 79.5 | 27.097 % | c | 225429 | 33181 74672 | 38223 23671 2229221 94.2 | 27.096 % | c | 244890 | 33175 74652 | 42045 17966 1498822 83.4 | 27.152 % | c | 274083 | 33175 74652 | 46250 17738 1472813 83.0 | 27.153 % | c | 317872 | 33110 74429 | 50875 27986 3537495 126.4 | 27.775 % | c | 383556 | 33081 74332 | 55963 19681 931131 47.3 | 28.059 % | c ============================================================================== c [1mFound solution: -32[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 26 maxlim: 32 bits: 7/6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 388658 | 33160 74591 | 11053 24783 1188869 48.0 | 28.059 % | c | 388758 | 33160 74591 | 12158 6297 212150 33.7 | 28.054 % | c | 388908 | 33160 74591 | 13374 6447 216384 33.6 | 28.049 % | c | 389133 | 33160 74591 | 14711 6672 221396 33.2 | 28.050 % | c | 389470 | 33160 74591 | 16182 7009 238156 34.0 | 28.049 % | c | 389976 | 33160 74591 | 17800 7515 264868 35.2 | 28.049 % | c | 390735 | 33160 74591 | 19581 8274 303119 36.6 | 28.055 % | c | 391876 | 33160 74591 | 21539 9415 364934 38.8 | 28.055 % | c | 393584 | 33160 74591 | 23693 11123 492392 44.3 | 28.050 % | c | 396147 | 33160 74591 | 26062 13686 722846 52.8 | 28.049 % | c | 399991 | 33160 74591 | 28668 17530 1008079 57.5 | 28.049 % | c | 405757 | 33160 74591 | 31535 23296 1541127 66.2 | 28.049 % | c | 414406 | 33124 74467 | 34689 31929 2189444 68.6 | 28.387 % | c | 427380 | 33124 74467 | 38157 23346 1470958 63.0 | 28.391 % | c | 446842 | 33124 74467 | 41973 17779 1338626 75.3 | 28.391 % | c | 476034 | 33124 74467 | 46171 18854 1485856 78.8 | 28.390 % | c | 519825 | 33118 74447 | 50788 30102 2592981 86.1 | 28.447 % | c | 585509 | 33104 74399 | 55867 22844 2072675 90.7 | 28.612 % | c | 684035 | 33066 74267 | 61453 42318 2856598 67.5 | 28.893 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.95 0.90 2/54 29036 Raw data (stat): 29036 (runsolver) R 29035 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421461184 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0015 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 1599 0 0 0 994 4 0 0 25 0 1 0 421461184 7999488 1577 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1953 1577 603 41 0 1912 0 vsize: 7812 [startup+20.0023 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 2630 0 0 0 1990 8 0 0 25 0 1 0 421461184 12333056 2608 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3011 2608 603 41 0 2970 0 vsize: 12044 [startup+30.0027 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3417 0 0 0 2988 10 0 0 25 0 1 0 421461184 15544320 3395 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3795 3395 603 41 0 3754 0 vsize: 15180 [startup+40.003 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 3987 11 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4056 3638 603 41 0 4015 0 vsize: 16224 [startup+50.0039 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 4986 12 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4056 3638 603 41 0 4015 0 vsize: 16224 [startup+60.0043 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 5986 12 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4056 3638 603 41 0 4015 0 vsize: 16224 [startup+70.0058 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3832 0 0 0 6985 13 0 0 25 0 1 0 421461184 17285120 3810 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4220 3810 603 41 0 4179 0 vsize: 16880 [startup+80.0064 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3832 0 0 0 7985 13 0 0 25 0 1 0 421461184 17285120 3810 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4220 3810 603 41 0 4179 0 vsize: 16880 [startup+90.0068 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4045 0 0 0 8983 14 0 0 25 0 1 0 421461184 18223104 4023 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4449 4023 603 41 0 4408 0 vsize: 17796 [startup+100.007 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4508 0 0 0 9981 17 0 0 25 0 1 0 421461184 20099072 4486 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4907 4486 603 41 0 4866 0 vsize: 19628 [startup+110.008 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 10981 17 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4939 4528 603 41 0 4898 0 vsize: 19756 [startup+120.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 11980 18 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4939 4528 603 41 0 4898 0 vsize: 19756 [startup+130.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 12980 18 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4939 4528 603 41 0 4898 0 vsize: 19756 [startup+140.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4810 0 0 0 13980 18 0 0 25 0 1 0 421461184 21282816 4788 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5196 4788 603 41 0 5155 0 vsize: 20784 [startup+150.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5238 0 0 0 14979 19 0 0 25 0 1 0 421461184 23015424 5216 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5619 5216 603 41 0 5578 0 vsize: 22476 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 15979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5651 5246 603 41 0 5610 0 vsize: 22604 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 16979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5651 5246 603 41 0 5610 0 vsize: 22604 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 17979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5651 5246 603 41 0 5610 0 vsize: 22604 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 18979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5651 5246 603 41 0 5610 0 vsize: 22604 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 19980 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5651 5246 603 41 0 5610 0 vsize: 22604 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5667 0 0 0 20979 20 0 0 25 0 1 0 421461184 24870912 5645 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6072 5645 603 41 0 6031 0 vsize: 24288 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5737 0 0 0 21979 20 0 0 25 0 1 0 421461184 25137152 5715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6137 5715 603 41 0 6096 0 vsize: 24548 [startup+230.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5737 0 0 0 22979 20 0 0 25 0 1 0 421461184 25137152 5715 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5715 603 41 0 6096 0 vsize: 24548 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 23979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+250.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 24979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+260.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 25979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+270.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 26978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 27978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 28978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6137 5716 603 41 0 6096 0 vsize: 24548 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 29978 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6131 5716 603 41 0 6090 0 vsize: 24524 [startup+310.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 30978 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6131 5716 603 41 0 6090 0 vsize: 24524 [startup+320.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 31979 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6131 5716 603 41 0 6090 0 vsize: 24524 [startup+330.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 32979 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6131 5716 603 41 0 6090 0 vsize: 24524 [startup+340.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 33979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5716 603 41 0 6084 0 vsize: 24500 [startup+350.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 34979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5716 603 41 0 6084 0 vsize: 24500 [startup+360.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 35979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5716 603 41 0 6084 0 vsize: 24500 [startup+370.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 36979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5716 603 41 0 6084 0 vsize: 24500 [startup+380.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 37980 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6125 5716 603 41 0 6084 0 vsize: 24500 [startup+390.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 38979 21 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6254 5843 603 41 0 6213 0 vsize: 25016 [startup+400.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 39979 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6254 5843 603 41 0 6213 0 vsize: 25016 [startup+410.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 40980 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6254 5843 603 41 0 6213 0 vsize: 25016 [startup+420.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 41980 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6254 5843 603 41 0 6213 0 vsize: 25016 [startup+430.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5872 0 0 0 42980 22 0 0 25 0 1 0 421461184 25616384 5850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6254 5850 603 41 0 6213 0 vsize: 25016 [startup+440.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6363 0 0 0 43978 23 0 0 25 0 1 0 421461184 27607040 6341 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6341 603 41 0 6699 0 vsize: 26960 [startup+450.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 44978 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6342 603 41 0 6699 0 vsize: 26960 [startup+460.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 45979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223744 134559385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6342 603 41 0 6699 0 vsize: 26960 [startup+470.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 46979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6342 603 41 0 6699 0 vsize: 26960 [startup+480.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 47979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6342 603 41 0 6699 0 vsize: 26960 [startup+490.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6731 0 0 0 48977 25 0 0 25 0 1 0 421461184 29208576 6709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7131 6709 603 41 0 7090 0 vsize: 28524 [startup+500.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7144 0 0 0 49976 26 0 0 25 0 1 0 421461184 30830592 7122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7527 7122 603 41 0 7486 0 vsize: 30108 [startup+510.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7531 0 0 0 50976 27 0 0 25 0 1 0 421461184 32452608 7509 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7923 7509 603 41 0 7882 0 vsize: 31692 [startup+520.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7873 0 0 0 51974 29 0 0 25 0 1 0 421461184 33910784 7851 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7851 603 41 0 8238 0 vsize: 33116 [startup+530.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8322 0 0 0 52973 30 0 0 25 0 1 0 421461184 35651584 8300 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8704 8300 603 41 0 8663 0 vsize: 34816 [startup+540.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 53973 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+550.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 54974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+560.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29036 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 55974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+570.023 s] Raw data (loadavg): 1.07 0.99 0.91 4/59 29088 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 56974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+580.022 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 57974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+590.022 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 58974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+600.021 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 59974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+610.022 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 60975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+620.021 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 61974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+630.021 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 62974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+640.022 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 29089 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 63975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+650.022 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 64975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+660.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 65975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+670.023 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 66975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+680.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 67975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+690.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 68975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+700.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 69975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+710.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 70976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+720.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 71976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+730.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 72976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+740.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 73976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+750.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 74976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+760.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 75976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+770.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 76976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+780.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 77977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+790.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 78977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+800.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 79977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+810.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 80977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+820.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 81977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+830.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 82977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+840.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 83978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+850.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 84978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560285 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+860.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 85978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+870.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 86978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+880.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 87978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+890.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 88978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+900.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29091 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 89979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+910.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 90979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+920.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 91979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+930.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 92979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+940.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 93979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+950.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 94980 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+960.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 95979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+970.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 96979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+980.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 97979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+990.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 98979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+1000.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 99980 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8358 603 41 0 8728 0 vsize: 35076 [startup+1010.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8384 0 0 0 100980 31 0 0 25 0 1 0 421461184 35917824 8362 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8362 603 41 0 8728 0 vsize: 35076 [startup+1020.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 101980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1030.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 102980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1040.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 103980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 104981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1060.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 105981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1070.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 106981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 107981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 108981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1100.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 109982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1110.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 110982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1120.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 111982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1130.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 112982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1140.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 113982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1150.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 114982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8363 603 41 0 8728 0 vsize: 35076 [startup+1160.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8386 0 0 0 115982 31 0 0 25 0 1 0 421461184 35917824 8364 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8364 603 41 0 8728 0 vsize: 35076 [startup+1170.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8390 0 0 0 116983 31 0 0 25 0 1 0 421461184 35917824 8368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8368 603 41 0 8728 0 vsize: 35076 [startup+1180.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 117983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8369 603 41 0 8728 0 vsize: 35076 [startup+1190.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 118983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8369 603 41 0 8728 0 vsize: 35076 [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 29093 Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 119983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8769 8369 603 41 0 8728 0 vsize: 35076 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 29093 Raw data (stat): 29036 (minisat+) Z 29035 25285 25284 0 -1 12 8394 0 0 0 119983 33 0 0 25 0 1 0 421461184 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.17 CPU user time (s): 1199.84 CPU system time (s): 0.332949 CPU usage (%): 100.01 Max. virtual memory (Kb): 35076 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####