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 23415

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