Some explanations

1. LAUNCHER DATA
   These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
2. SOLVER DATA
   This is the output of the solver (stdout and stderr).
3. WATCHER DATA
   This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
   Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
   When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
4. VERIFIER DATA
   The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Trace number 23425

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-03 12:04:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=511 boxname=wulflinc31 idbench=57 idsolver=7 numberseed=0
MD5SUM SOLVER: d9a5994a76be78982e492b397ce73911  /oldhome/oroussel/solvers/Pueblo
MD5SUM BENCH:  da4cd22fd601b0d838453ba86be8f9aa  /oldhome/oroussel/tmp/wulflinc31/normalized-fpga45_45_sat_pb.cnf.cr.opb
REAL COMMAND:  Pueblo /oldhome/oroussel/tmp/wulflinc31/normalized-fpga45_45_sat_pb.cnf.cr.opb
IDLAUNCH: 511
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        920692 kB
Buffers:         39856 kB
Cached:          52020 kB
SwapCached:        944 kB
Active:          76920 kB
Inactive:        17416 kB
HighTotal:      131008 kB
HighFree:        77952 kB
LowTotal:       903652 kB
LowFree:        842740 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5536 kB
Slab:            14188 kB
Committed_AS:    63656 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-03 12:04:33 (client local time) WITH STATUS 10 IN 6.73997 SECONDS
stats: 511 0 6.73997 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Pueblo version 1.2 (Sept 2004)
c Developed @ University of Michigan, Ann Arbor, MI
c  by Hossein Sheini
c Solving: /oldhome/oroussel/tmp/wulflinc31/normalized-fpga45_45_sat_pb.cnf.cr.opb
c #variables read: 3038 - #constraints read: 2160
s SATISFIABLE
v -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 v630 -v362 -v2048 -v2049 -v2050 -v2051 -v2052 -v2053 -v2054 -v2055 -v2056 -v2057 -v2058 -v2059 -v2060 -v2061 -v2062 -v2063 -v2064 -v2065 -v2066 -v2067 v2068 -v2069 -v171 -v2809 -v2810 -v2811 -v2812 -v2813 -v2814 -v2815 -v2816 -v2817 -v2818 -v2819 -v2820 -v2821 -v2822 -v2823 -v2824 -v2825 -v2826 -v2827 -v2828 -v2829 v2830 -v2831 -v422 -v2378 -v2379 -v2380 -v2381 -v2382 -v2383 -v2384 -v2385 -v2386 -v2387 -v2388 -v2389 -v2390 -v2391 -v2392 -v2393 -v2394 -v2395 -v2396 v2397 -v2398 -v2399 -v1972 -v2832 -v2833 -v2834 -v2835 -v2836 -v2837 -v2838 -v2839 -v2840 -v2841 -v2842 -v2843 -v2844 -v2845 -v2846 -v2847 -v2848 -v2849 -v2850 -v2851 v2852 -v2853 -v2854 -v1584 -v2202 -v2203 -v2204 -v2205 -v2206 -v2207 -v2208 -v2209 -v2210 -v2211 -v2212 -v2213 -v2214 -v2215 -v2216 -v2217 -v2218 -v2219 v2220 -v2221 -v2222 -v2223 -v1224 -v1338 -v2740 -v2741 -v2742 -v2743 -v2744 -v2745 -v2746 -v2747 -v2748 -v2749 -v2750 -v2751 -v2752 -v2753 -v2754 -v2755 -v2756 -v2757 -v2758 v2759 -v2760 -v2761 -v2762 -v1756 v1757 -v1758 -v1759 -v1760 -v1761 -v1762 -v1763 -v1764 -v1765 -v1766 -v1767 -v1768 -v1769 -v1770 -v1771 -v1772 -v1773 -v1774 -v1775 -v1776 -v1777 -v1778 -v1779 -v1780 -v1781 -v1782 -v1783 -v1784 -v1785 -v1786 -v1787 -v1788 -v1789 -v1790 -v1791 -v1792 -v1793 -v1794 -v1795 -v1796 -v1797 -v1798 -v1799 -v1800 -v1952 -v1004 -v2312 -v2313 -v2314 -v2315 -v2316 -v2317 -v2318 -v2319 -v2320 -v2321 -v2322 -v2323 -v2324 -v2325 -v2326 -v2327 -v2328 v2329 -v2330 -v2331 -v2332 -v2333 -v1445 -v2114 -v2115 -v2116 -v2117 -v2118 -v2119 -v2120 -v2121 -v2122 -v2123 -v2124 -v2125 -v2126 -v2127 -v2128 -v2129 v2130 -v2131 -v2132 -v2133 -v2134 -v2135 -v99 -v1232 -v1543 -v2290 -v2291 -v2292 -v2293 -v2294 -v2295 -v2296 -v2297 -v2298 -v2299 -v2300 -v2301 -v2302 -v2303 -v2304 v2305 -v2306 -v2307 -v2308 -v2309 -v2310 -v2311 -v2015 -v2786 -v2787 -v2788 -v2789 -v2790 -v2791 -v2792 -v2793 -v2794 -v2795 -v2796 -v2797 -v2798 -v2799 -v2800 -v2801 -v2802 -v2803 v2804 -v2805 -v2806 -v2807 -v2808 -v835 -v2556 -v2557 -v2558 -v2559 -v2560 -v2561 -v2562 -v2563 -v2564 -v2565 -v2566 -v2567 -v2568 -v2569 -v2570 -v2571 -v2572 v2573 -v2574 -v2575 -v2576 -v2577 -v2578 -v564 -v2533 -v2534 -v2535 -v2536 -v2537 -v2538 -v2539 -v2540 -v2541 -v2542 -v2543 -v2544 -v2545 -v2546 -v2547 -v2548 v2549 -v2550 -v2551 -v2552 -v2553 -v2554 -v2555 -v1869 -v1286 -v2579 -v2580 -v2581 -v2582 -v2583 -v2584 -v2585 -v2586 -v2587 -v2588 -v2589 -v2590 -v2591 -v2592 -v2593 v2594 -v2595 -v2596 -v2597 -v2598 -v2599 -v2600 -v2601 -v400 -v2901 -v2902 -v2903 -v2904 -v2905 -v2906 -v2907 -v2908 -v2909 -v2910 -v2911 -v2912 -v2913 -v2914 v2915 -v2916 -v2917 -v2918 -v2919 -v2920 -v2921 -v2922 -v2923 -v1463 -v2510 -v2511 -v2512 -v2513 -v2514 -v2515 -v2516 -v2517 -v2518 -v2519 -v2520 -v2521 -v2522 v2523 -v2524 -v2525 -v2526 -v2527 -v2528 -v2529 -v2530 -v2531 -v2532 -v83 -v2855 -v2856 -v2857 -v2858 -v2859 -v2860 -v2861 -v2862 -v2863 -v2864 -v2865 -v2866 v2867 -v2868 -v2869 -v2870 -v2871 -v2872 -v2873 -v2874 -v2875 -v2876 -v2877 -v941 -v2924 -v2925 -v2926 -v2927 -v2928 -v2929 -v2930 -v2931 -v2932 -v2933 -v2934 v2935 -v2936 -v2937 -v2938 -v2939 -v2940 -v2941 -v2942 -v2943 -v2944 -v2945 -v2946 -v463 -v1559 -v2648 -v2649 -v2650 -v2651 -v2652 -v2653 -v2654 -v2655 -v2656 -v2657 v2658 -v2659 -v2660 -v2661 -v2662 -v2663 -v2664 -v2665 -v2666 -v2667 -v2668 -v2669 -v2670 -v1228 -v143 -v2180 -v2181 -v2182 -v2183 -v2184 -v2185 -v2186 -v2187 -v2188 -v2189 -v2190 -v2191 -v2192 -v2193 v2194 -v2195 -v2196 -v2197 -v2198 -v2199 -v2200 -v2201 -v403 -v2970 -v2971 -v2972 -v2973 -v2974 -v2975 -v2976 -v2977 -v2978 v2979 -v2980 -v2981 -v2982 -v2983 -v2984 -v2985 -v2986 -v2987 -v2988 -v2989 -v2990 -v2991 -v2992 -v472 -v2488 -v2489 -v2490 -v2491 -v2492 -v2493 -v2494 -v2495 -v2496 -v2497 -v2498 -v2499 -v2500 v2501 -v2502 -v2503 -v2504 -v2505 -v2506 -v2507 -v2508 -v2509 -v219 -v2878 -v2879 -v2880 -v2881 -v2882 -v2883 -v2884 -v2885 v2886 -v2887 -v2888 -v2889 -v2890 -v2891 -v2892 -v2893 -v2894 -v2895 -v2896 -v2897 -v2898 -v2899 -v2900 -v1631 -v2246 -v2247 -v2248 -v2249 -v2250 -v2251 -v2252 -v2253 -v2254 -v2255 -v2256 -v2257 v2258 -v2259 -v2260 -v2261 -v2262 -v2263 -v2264 -v2265 -v2266 -v2267 -v269 -v2993 -v2994 -v2995 -v2996 -v2997 -v2998 -v2999 v3000 -v3001 -v3002 -v3003 -v3004 -v3005 -v3006 -v3007 -v3008 -v3009 -v3010 -v3011 -v3012 -v3013 -v3014 -v3015 -v1126 -v1127 -v1128 -v1129 -v1130 -v1131 -v1132 -v1133 -v1134 -v1135 -v1136 -v1137 -v1138 -v1139 -v1140 -v1141 -v1142 -v1143 -v1144 -v1145 -v1146 -v1147 -v1148 -v1149 -v1150 -v1151 -v1152 -v1153 -v1154 -v1155 -v1156 -v1157 v1158 -v1159 -v1160 -v1161 -v1162 -v1163 -v1164 -v1165 -v1166 -v1167 -v1168 -v1169 -v1170 -v801 -v285 -v2334 -v2335 -v2336 -v2337 -v2338 -v2339 -v2340 -v2341 -v2342 -v2343 -v2344 v2345 -v2346 -v2347 -v2348 -v2349 -v2350 -v2351 -v2352 -v2353 -v2354 -v2355 -v1650 -v2671 -v2672 -v2673 -v2674 -v2675 -v2676 v2677 -v2678 -v2679 -v2680 -v2681 -v2682 -v2683 -v2684 -v2685 -v2686 -v2687 -v2688 -v2689 -v2690 -v2691 -v2692 -v2693 -v855 -v3016 -v3017 -v3018 -v3019 -v3020 v3021 -v3022 -v3023 -v3024 -v3025 -v3026 -v3027 -v3028 -v3029 -v3030 -v3031 -v3032 -v3033 -v3034 -v3035 -v3036 -v3037 -v3038 -v1000 -v2224 -v2225 -v2226 -v2227 -v2228 -v2229 -v2230 -v2231 -v2232 -v2233 v2234 -v2235 -v2236 -v2237 -v2238 -v2239 -v2240 -v2241 -v2242 -v2243 -v2244 -v2245 -v780 -v1292 -v2717 -v2718 -v2719 -v2720 v2721 -v2722 -v2723 -v2724 -v2725 -v2726 -v2727 -v2728 -v2729 -v2730 -v2731 -v2732 -v2733 -v2734 -v2735 -v2736 -v2737 -v2738 -v2739 -v2024 -v1486 -v1487 -v1488 -v1489 -v1490 -v1491 -v1492 -v1493 -v1494 -v1495 -v1496 -v1497 -v1498 -v1499 -v1500 -v1501 -v1502 -v1503 -v1504 -v1505 -v1506 -v1507 -v1508 -v1509 -v1510 v1511 -v1512 -v1513 -v1514 -v1515 -v1516 -v1517 -v1518 -v1519 -v1520 -v1521 -v1522 -v1523 -v1524 -v1525 -v1526 -v1527 -v1528 -v1529 -v1530 -v1297 -v558 -v2400 -v2401 -v2402 -v2403 -v2404 -v2405 -v2406 -v2407 -v2408 v2409 -v2410 -v2411 -v2412 -v2413 -v2414 -v2415 -v2416 -v2417 -v2418 -v2419 -v2420 -v2421 -v384 -v1891 -v1892 -v1893 -v1894 -v1895 -v1896 -v1897 -v1898 -v1899 -v1900 -v1901 -v1902 -v1903 -v1904 -v1905 -v1906 -v1907 -v1908 -v1909 -v1910 -v1911 -v1912 -v1913 -v1914 v1915 -v1916 -v1917 -v1918 -v1919 -v1920 -v1921 -v1922 -v1923 -v1924 -v1925 -v1926 -v1927 -v1928 -v1929 -v1930 -v1931 -v1932 -v1933 -v1934 -v1935 -v281 -v706 -v2694 -v2695 -v2696 -v2697 -v2698 -v2699 -v2700 -v2701 -v2702 -v2703 -v2704 -v2705 -v2706 -v2707 -v2708 -v2709 -v2710 -v2711 -v2712 -v2713 -v2714 -v2715 v2716 -v1284 -v779 -v765 -v1996 -v2356 -v2357 -v2358 -v2359 -v2360 -v2361 -v2362 -v2363 v2364 -v2365 -v2366 -v2367 -v2368 -v2369 -v2370 -v2371 -v2372 -v2373 -v2374 -v2375 -v2376 -v2377 -v658 -v2625 -v2626 -v2627 v2628 -v2629 -v2630 -v2631 -v2632 -v2633 -v2634 -v2635 -v2636 -v2637 -v2638 -v2639 -v2640 -v2641 -v2642 -v2643 -v2644 -v2645 -v2646 -v2647 -v978 -v531 -v826 -v1351 -v2026 -v2027 -v2028 -v2029 -v2030 -v2031 -v2032 v2033 -v2034 -v2035 -v2036 -v2037 -v2038 -v2039 -v2040 -v2041 -v2042 -v2043 -v2044 -v2045 -v2046 -v2047 -v1605 -v1287 -v2602 -v2603 v2604 -v2605 -v2606 -v2607 -v2608 -v2609 -v2610 -v2611 -v2612 -v2613 -v2614 -v2615 -v2616 -v2617 -v2618 -v2619 -v2620 -v2621 -v2622 -v2623 -v2624 -v1698 -v1886 -v159 -v721 -v802 -v1959 -v1264 -v2092 -v2093 -v2094 -v2095 -v2096 -v2097 v2098 -v2099 -v2100 -v2101 -v2102 -v2103 -v2104 -v2105 -v2106 -v2107 -v2108 -v2109 -v2110 -v2111 -v2112 -v2113 -v1811 -v1295 -v361 -v202 -v1810 -v1581 -v2136 -v2137 -v2138 -v2139 -v2140 v2141 -v2142 -v2143 -v2144 -v2145 -v2146 -v2147 -v2148 -v2149 -v2150 -v2151 -v2152 -v2153 -v2154 -v2155 -v2156 -v2157 -v659 -v2016 -v410 -v517 -v530 -v151 -v125 -v1322 -v409 -v713 -v1753 -v1822 -v91 -v543 -v2070 -v2071 -v2072 -v2073 v2074 -v2075 -v2076 -v2077 -v2078 -v2079 -v2080 -v2081 -v2082 -v2083 -v2084 -v2085 -v2086 -v2087 -v2088 -v2089 -v2090 -v2091 -v566 -v533 -v320 -v523 -v1314 -v182 -v1353 -v749 -v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 -v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v740 -v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v750 -v751 -v752 -v753 -v754 -v755 v756 -v757 -v758 -v759 -v760 -v761 -v762 -v763 -v764 -v60 -v897 -v2947 v2948 -v2949 -v2950 -v2951 -v2952 -v2953 -v2954 -v2955 -v2956 -v2957 -v2958 -v2959 -v2960 -v2961 -v2962 -v2963 -v2964 -v2965 -v2966 -v2967 -v2968 -v2969 -v345 -v1046 -v78 -v1608 -v666 -v95 -v2444 -v2445 v2446 -v2447 -v2448 -v2449 -v2450 -v2451 -v2452 -v2453 -v2454 -v2455 -v2456 -v2457 -v2458 -v2459 -v2460 -v2461 -v2462 -v2463 -v2464 -v2465 -v1638 -v968 -v1812 -v2268 -v2269 -v2270 v2271 -v2272 -v2273 -v2274 -v2275 -v2276 -v2277 -v2278 -v2279 -v2280 -v2281 -v2282 -v2283 -v2284 -v2285 -v2286 -v2287 -v2288 -v2289 -v63 -v645 -v858 -v1257 -v351 -v1620 -v799 v2763 -v2764 -v2765 -v2766 -v2767 -v2768 -v2769 -v2770 -v2771 -v2772 -v2773 -v2774 -v2775 -v2776 -v2777 -v2778 -v2779 -v2780 -v2781 -v2782 -v2783 -v2784 -v2785 -v183 -v1637 -v535 -v999 -v1389 -v1305 -v1854 -v1294 -v433 -v646 -v923 -v965 -v172 -v1956 v2466 -v2467 -v2468 -v2469 -v2470 -v2471 -v2472 -v2473 -v2474 -v2475 -v2476 -v2477 -v2478 -v2479 -v2480 -v2481 -v2482 -v2483 -v2484 -v2485 -v2486 -v2487 -v857 -v1440 -v1341 -v37 -v186 -v1381 -v293 -v1855 -v1692 v1875 -v457 -v2158 -v2159 -v2160 -v2161 -v2162 -v2163 -v2164 -v2165 -v2166 -v2167 -v2168 -v2169 -v2170 -v2171 -v2172 -v2173 -v2174 -v2175 -v2176 -v2177 -v2178 v2179 -v1613 -v1827 -v275 -v852 -v318 -v1086 -v1461 -v1045 -v502 -v1050 -v1344 v1365 -v1622 -v1978 -v1616 -v480 -v1640 -v188 -v1409 -v123 -v925 -v1102 -v1125 -v316 -v327 -v1703 v1282 -v258 -v2006 -v1377 -v1426 -v1386 -v1690 -v120 -v1847 -v368 -v892 -v397 -v1586 -v1980 -v464 -v346 -v1579 -v1747 -v479 -v1335 -v860 -v1352 -v1989 -v1248 -v1955 -v809 -v1639 -v2422 v2423 -v2424 -v2425 -v2426 -v2427 -v2428 -v2429 -v2430 -v2431 -v2432 -v2433 -v2434 -v2435 -v2436 -v2437 -v2438 -v2439 -v2440 -v2441 -v2442 -v2443 -v1644 -v1253 -v1087 -v1739 -v1238 -v1068 -v10 -v776 -v1371 -v265 -v1051 -v465 -v1188 -v1424 -v1047 -v2017 -v180 -v777 -v196 -v1604 v102 -v1625 -v2020 -v1597 -v1354 -v111 -v228 -v1057 -v943 -v1191 -v647 -v1599 -v1887 -v872 -v516 -v264 -v1662 -v1483 -v1034 -v577 -v1667 -v1829 -v1825 -v279 -v191 -v154 -v818 -v181 -v184 -v185 -v187 -v189 -v190 -v192 -v193 -v194 -v195 -v197 -v198 -v199 -v200 -v201 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v210 -v211 -v212 -v213 -v214 v215 -v216 -v217 -v218 -v220 -v221 -v222 -v223 -v224 -v225 -v142 -v81 -v451 -v452 -v453 -v454 -v455 -v456 -v458 v459 -v460 -v461 -v462 -v466 -v467 -v468 -v469 -v470 -v471 -v473 -v474 -v475 -v476 -v477 -v478 -v481 -v482 -v483 -v484 -v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 -v494 -v495 -v1666 -v229 -v1442 -v283 -v1317 -v1648 -v1366 v447 -v663 -v357 -v1968 -v1194 -v1113 -v1096 -v963 -v2000 -v82 -v936 -v1296 -v1393 -v937 -v1361 -v1422 -v363 -v702 -v496 -v1591 -v986 -v1263 -v1289 -v364 -v1552 -v956 -v1245 -v1198 -v685 -v144 -v1688 -v267 -v1805 -v585 -v898 -v1751 -v970 -v1011 -v1987 -v1482 -v333 -v12 -v814 -v1531 -v1532 -v1533 -v1534 -v1535 -v1536 -v1537 -v1538 -v1539 -v1540 -v1541 -v1542 -v1544 -v1545 -v1546 -v1547 -v1548 -v1549 -v1550 -v1551 -v1553 -v1554 -v1555 -v1556 -v1557 -v1558 -v1560 -v1561 -v1562 -v1563 v1564 -v1565 -v1566 -v1567 -v1568 -v1569 -v1570 -v1571 -v1572 -v1573 -v1574 -v1575 -v500 -v1862 -v1414 -v559 -v72 -v280 -v380 -v833 -v356 -v381 -v1708 -v805 -v690 -v1280 -v644 -v819 -v1376 -v906 -v904 -v772 -v929 -v1997 -v653 -v975 -v9 -v903 -v1425 v139 -v1844 -v918 -v568 -v1682 -v1217 -v270 -v694 -v160 -v717 -v331 -v227 -v416 -v667 -v31 -v124 -v520 -v1421 -v1964 -v1743 -v1746 -v79 -v30 -v1084 -v3 -v1802 -v1197 -v1750 -v804 -v1342 -v552 -v1313 v322 -v155 -v843 -v86 -v1225 -v1207 -v1075 -v1209 -v266 -v418 -v1208 -v89 -v49 -v375 -v1670 -v365 -v366 -v367 -v369 -v370 -v371 -v372 -v373 -v374 -v376 -v377 -v378 -v379 -v382 -v383 -v385 -v386 v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v398 -v399 -v401 -v402 -v404 -v405 -v846 -v1270 -v683 -v1008 -v1090 -v709 -v158 -v232 -v769 -v1713 -v1412 -v1083 -v813 -v1369 -v678 v509 -v347 -v1485 -v152 -v983 -v177 -v1484 -v443 -v1301 -v5 -v1835 -v115 -v1954 -v1856 -v1466 -v1685 -v98 v1945 -v1614 -v1408 -v59 -v1706 -v1633 -v1439 -v1436 -v901 -v902 -v905 -v907 -v908 -v909 -v910 -v911 -v912 -v913 -v914 -v915 -v916 -v917 -v919 -v920 -v921 -v922 -v924 -v926 -v927 -v928 -v930 -v931 -v932 -v933 -v934 -v935 -v938 -v939 -v940 -v942 v944 -v945 -v352 -v2010 -v549 -v791 -v1268 -v355 -v1712 -v26 -v1990 -v261 -v1122 -v44 -v575 -v1936 -v165 -v519 -v784 -v1628 -v1309 v271 -v1010 -v868 -v1687 -v984 -v147 -v953 -v439 -v864 -v1030 -v1184 -v282 -v1966 -v1071 -v329 -v312 -v1960 -v1272 -v1957 -v290 -v328 -v109 -v1958 -v1099 -v87 -v173 -v1937 -v353 -v277 v2001 -v503 -v1998 -v1118 -v1042 -v831 -v238 -v1646 -v97 -v1074 -v1333 -v824 -v93 -v1036 -v1391 -v1306 -v2003 -v637 -v1325 -v1725 -v1069 -v41 -v169 -v1801 -v1626 -v1588 -v714 -v174 -v1711 -v1714 -v1715 -v1716 -v1717 -v1718 -v1719 -v1720 -v1721 -v1722 -v1723 -v1724 -v1726 -v1727 -v1728 -v1729 -v1730 -v1731 -v1732 -v1733 -v1734 -v1735 -v1736 -v1737 -v1738 -v1740 -v1741 -v1742 -v1744 -v1745 -v1748 v1749 -v1752 -v1754 -v1755 -v1 -v2 -v4 -v6 -v7 -v8 -v11 -v13 -v14 -v15 v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v27 -v28 -v29 -v32 -v33 -v34 -v35 -v36 -v38 -v39 -v40 -v42 -v43 -v45 -v1994 -v511 -v1815 -v1189 -v1098 -v436 -v1355 -v444 -v951 -v640 -v57 -v1832 -v292 -v1419 -v862 -v1271 -v789 -v1196 -v53 -v162 -v1879 -v321 -v1105 -v278 -v1970 -v1082 -v1457 -v406 -v1818 -v716 -v1186 -v1677 -v429 -v1037 -v1941 -v1420 -v1043 -v1116 -v1672 -v256 -v1434 -v1053 -v2018 -v654 -v672 -v991 -v992 -v993 -v994 -v995 -v996 -v997 -v998 -v1001 -v1002 v1003 -v1005 -v1006 -v1007 -v1009 -v1012 -v1013 -v1014 -v1015 -v1016 -v1017 -v1018 -v1019 -v1020 -v1021 -v1022 -v1023 -v1024 -v1025 -v1026 -v1027 -v1028 -v1029 -v1031 -v1032 -v1033 -v1035 -v844 -v354 -v1598 -v1838 -v578 -v1079 -v1336 -v1836 -v884 -v1841 -v775 -v1593 -v135 v796 -v138 -v557 -v959 -v707 -v425 -v1592 -v161 -v423 -v309 -v832 -v108 -v1081 -v1651 -v1443 -v1233 -v1187 -v1961 -v253 -v969 -v1464 -v260 -v1048 -v1056 -v1231 -v1417 -v1451 -v47 -v1378 -v1831 -v988 -v1110 -v497 -v498 -v499 -v501 -v504 -v505 -v506 -v507 -v508 -v510 -v512 -v513 -v514 -v515 -v518 -v521 -v522 -v524 -v525 -v526 -v527 -v528 -v529 -v532 -v534 -v536 -v537 -v538 -v539 -v540 -v686 -v1962 -v1088 -v891 -v1694 -v1041 -v1629 -v550 -v974 -v1340 -v1826 -v1602 -v296 -v1689 -v655 -v1091 -v167 -v1390 -v1653 -v837 -v1699 -v1410 -v1192 -v1308 -v1222 -v1671 -v1843 -v955 -v153 -v1995 -v1696 -v1820 -v719 -v712 -v847 -v1283 -v1474 -v297 -v1291 -v1267 -v1973 -v304 -v1387 -v660 -v306 -v226 -v427 -v1121 -v1307 -v1310 -v1311 -v1312 -v1315 v1316 -v1318 -v1319 -v1320 -v1321 -v1323 -v1324 -v1326 -v1327 -v1328 -v1329 -v1330 -v1331 -v1332 -v1334 -v1337 -v1339 -v1343 -v1345 -v1346 -v1347 -v1348 -v1349 -v1350 -v1979 -v104 -v684 -v1630 -v1260 -v692 -v1621 -v1623 -v1624 -v1627 -v1632 -v1634 -v1635 -v1636 -v1641 -v1642 v1643 -v1645 -v1647 -v1649 -v1652 -v1654 -v1655 -v1656 -v1657 -v1658 -v1659 -v1660 -v1661 -v1663 -v1664 -v1665 -v1992 -v1383 -v2005 -v1101 -v149 -v1991 -v358 -v58 -v1404 -v1988 -v861 -v1241 -v69 -v972 -v248 -v1385 -v1275 -v1078 -v1967 -v856 -v136 -v582 -v1830 -v807 -v1676 -v129 -v1277 -v1878 -v1223 -v46 -v311 -v1304 -v643 -v272 -v865 -v673 -v308 -v1239 -v287 -v699 -v1580 -v1061 -v1103 -v1450 -v1938 -v1939 -v1940 -v1942 -v1943 -v1944 -v1946 -v1947 -v1948 -v1949 -v1950 -v1951 -v1953 -v1963 -v1965 -v1969 -v1971 -v1974 -v1975 -v1976 -v1977 -v885 -v107 -v1852 -v1617 v1055 -v348 v1702 -v838 -v249 -v881 -v816 -v1100 -v1619 -v674 -v1428 -v698 -v1840 -v335 -v1674 -v289 -v236 -v1819 -v2012 -v767 -v284 -v987 -v1218 -v1872 -v1107 -v1873 -v137 -v1477 -v1246 -v1600 -v324 -v817 -v546 -v680 -v853 -v1356 -v1357 -v1358 -v1359 -v1360 -v1362 -v1363 -v1364 -v1367 -v1368 -v1370 -v1372 -v1373 -v1374 -v1375 -v1379 -v1380 -v1382 -v1384 -v1388 -v1392 -v1394 -v1395 -v1453 -v301 -v766 -v768 -v770 -v771 -v773 -v774 -v778 -v781 -v782 -v783 -v785 -v786 -v787 -v788 -v790 -v792 -v793 -v794 -v795 -v797 -v798 -v800 -v803 -v806 -v808 -v810 -v1456 -v701 -v77 -v1195 -v1243 -v665 -v859 -v1398 -v273 -v274 -v276 -v286 -v288 -v291 -v294 -v295 -v298 -v299 -v300 -v302 -v303 -v305 -v307 -v310 -v313 -v314 -v315 -v2022 -v1240 v1085 -v1089 -v1092 -v1093 -v1094 -v1095 -v1097 -v1104 -v1106 -v1108 -v1109 -v1111 -v1112 -v1114 -v1115 -v1117 -v1119 -v1120 -v1123 -v1124 -v845 -v1204 -v1467 -v126 -v1860 -v811 -v1293 -v239 -v330 -v1438 -v1848 -v1981 -v1982 -v1983 -v1984 -v1985 -v1986 -v1993 -v1999 -v2002 -v2004 -v2007 -v2008 -v2009 -v2011 -v2013 -v2014 -v2019 -v2021 -v2023 -v2025 -v551 -v1465 -v635 -v56 -v96 -v1594 -v1302 -v1583 -v573 v1472 -v1213 -v64 -v1479 -v61 -v326 -v695 -v179 -v1206 -v1300 -v693 -v150 v583 -v235 -v74 -v1183 -v1816 -v105 -v639 -v889 -v874 -v1888 -v641 -v675 -v1073 -v572 -v428 -v830 -v52 -v1842 -v412 -v1668 -v1065 -v563 -v651 -v1595 -v876 -v414 -v1235 -v411 -v424 -v430 -v1059 -v1475 -v1254 -v682 -v946 -v419 -v1418 -v870 -v571 -v1180 -v866 -v636 -v1686 -v1865 -v890 -v250 -v1416 -v1299 -v565 -v1834 -v879 -v1578 -v1193 -v134 -v1265 -v1066 -v1401 -v339 -v252 -v1804 -v1441 -v1444 -v1446 -v1447 -v1448 -v1449 -v1452 -v1454 -v1455 -v1458 -v1459 -v1460 -v1462 -v1468 -v1469 -v1470 -v1471 -v1473 -v1476 -v1478 -v1480 -v1481 -v1288 -v1610 -v1437 -v1433 -v981 -v1274 -v708 -v1211 -v92 -v94 -v100 -v101 -v103 -v106 -v110 -v112 -v113 -v114 -v116 -v117 -v118 -v119 -v121 -v122 -v127 -v128 -v130 -v131 -v132 -v133 -v247 -v434 -v961 -v432 -v1242 -v850 -v711 -v1866 -v257 -v234 -v1709 -v820 -v893 -v1609 -v576 -v851 -v1080 -v553 -v1234 -v966 -v677 -v812 -v815 -v821 -v822 -v823 -v825 -v827 v828 -v829 -v834 -v836 -v839 -v840 -v841 -v842 -v848 -v849 -v854 -v1067 -v407 -v408 -v413 -v415 -v417 -v420 -v421 -v426 -v431 -v435 -v437 -v438 -v440 -v441 -v442 -v445 -v446 -v448 -v449 -v450 -v1237 -v230 -v231 -v233 -v237 -v240 -v241 -v242 -v243 v244 -v245 -v246 -v251 -v254 -v255 -v259 -v262 -v263 -v268 -v1038 -v1226 -v148 -v1273 -v718 -v989 -v157 -v581 -v1063 -v145 v1173 -v1255 -v1691 -v1693 -v952 -v1290 -v178 -v323 -v1803 -v1806 -v1807 -v1808 -v1809 -v1813 -v1814 -v1817 -v1821 -v1823 v1824 -v1828 -v1833 -v1837 -v1839 -v1845 -v547 -v1202 -v1431 -v670 -v163 -v1185 -v976 -v1256 -v990 -v544 -v1054 -v1679 -v1176 -v73 -v631 -v985 -v1427 -v875 -v1278 -v1216 -v1219 -v1220 -v1221 -v1227 -v1229 -v1230 -v1236 v1244 -v1247 -v1249 -v1250 -v1251 -v1252 -v1258 -v1259 -v1611 -v1261 -v700 -v554 -v1429 -v569 -v652 -v1615 -v70 -v656 -v1867 -v1850 -v977 -v75 -v88 -v62 -v1701 -v1181 -v703 -v562 -v1576 -v1405 -v164 -v867 -v1062 -v964 -v1210 -v542 -v1396 -v1178 -v1607 -v1406 -v632 -v633 -v634 -v638 -v642 -v648 -v649 -v650 -v657 -v661 -v662 -v664 v668 -v669 -v671 -v967 -v1669 -v1881 -v140 -v950 -v317 -v863 -v1411 -v1397 -v1399 -v1400 -v1402 v1403 -v1407 -v1413 -v1415 -v1423 -v1430 -v1432 -v1435 -v880 -v567 -v1200 -v319 -v325 -v332 -v334 -v336 -v337 -v338 -v340 -v341 -v342 -v343 -v344 -v349 -v350 -v359 -v360 -v894 -v1863 -v65 -v1215 -v1859 -v570 -v877 -v1077 -v1577 -v1582 -v1585 -v1587 -v1589 -v1590 -v1596 -v1601 v1603 -v1606 -v1612 -v1618 -v899 -v48 -v1040 -v1303 -v1876 v85 -v1880 -v141 -v146 -v156 -v166 -v168 -v170 -v175 -v176 -v705 -v1884 -v1680 -v50 v896 -v873 -v957 -v579 -v1858 -v715 -v878 -v882 -v76 -v1044 -v66 -v1205 -v1684 -v1190 -v688 -v541 -v545 -v548 -v555 -v556 -v560 -v561 -v574 -v580 -v584 -v676 -v679 v681 -v687 -v689 -v691 -v696 -v697 -v704 -v710 -v720 -v1281 -v947 -v948 -v949 -v954 -v958 -v960 v962 -v971 -v973 -v979 -v980 -v982 -v1175 -v1276 -v1182 -v1846 -v1177 -v1695 -v1707 -v1203 -v1710 -v1172 -v1201 -v1070 -v1705 -v1179 -v1877 -v90 -v71 -v51 -v54 -v55 -v67 -v68 -v80 -v84 -v1060 -v900 -v1857 -v1861 -v1673 -v895 -v1214 -v1890 -v1889 -v1882 -v886 -v1697 -v1675 -v1269 -v871 -v1052 -v869 -v1700 -v1058 -v1279 -v1678 -v1681 -v1683 -v1704 -v1049 -v1285 -v1266 -v888 -v1076 -v1868 -v1864 -v883 -v1298 -v1171 -v1174 -v1199 -v1212 -v1039 -v1072 -v1064 -v1262 -v1883 -v1870 -v1849 -v887 -v1874 -v1853 -v1885 -v1851 -v1871 
#### 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.93 0.99 0.99 2/54 2004
Raw data (stat): 2004 (runsolver) R 2003 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 648614949 1056768 100 4294967295 134512640 135381576 3221221680 3221216904 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+6.77218 s]
Raw data (loadavg): 0.93 0.99 0.99 1/53 2004
Raw data (stat): 2004 (runsolver) R 2003 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 648614949 1056768 100 4294967295 134512640 135381576 3221221680 3221216904 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 0

Child status: 10
Real time (s): 6.77158
CPU time (s): 6.73997
CPU user time (s): 6.69898
CPU system time (s): 0.040993
CPU usage (%): 99.5333
Max. virtual memory (Kb): 1032
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	0
#### END VERIFIER DATA ####