Q2_33_sol.txt

c CommonSolverConfig { filename: Some("Q2_33.qdimacs"), verbosity: Warn, statistics: None, specific: CaqeSpecificSolverConfig { options: SolverOptions { abstraction: AbstractionOptions { reuse_b_literals: Some(Partial), reuse_t_literals: Some(Partial), additional_t_literal_constraints: Some(Partial), additional_b_literal_constraints: false, equivalence_constraints: true, universal_reuse_b_literals: true, replace_t_literal_by_variable: true }, expansion: ExpansionOptions { expansion_refinement: Some(Full), dependency_schemes: false, conflict_clause_expansion: true, hamming_heuristics: false }, strong_unsat_refinement: false, refinement_literal_subsumption: false, miniscoping: true, build_conflict_clauses: false, flip_assignments_from_sat_solver: false, skip_levels: None }, qdimacs_output: true, preprocessor: None } }
s cnf 1 2921 24754
V -1 0
V -2 0
V -3 0
V -4 0
V -5 0
V -6 0
V 7 0
V 8 0
V 9 0
V -10 0
V 11 0
V 12 0
V 13 0
V -14 0
V -15 0
V -16 0
V 17 0
V 18 0
V -19 0
V -20 0
V -21 0
V -22 0
V -23 0
V -24 0
V -25 0
V -26 0
V -27 0
V 28 0
V -29 0
V -30 0
V -31 0
V -32 0
V -33 0
V -34 0
V 35 0
V 36 0
V -37 0
V -38 0
V 39 0
V 40 0
V 41 0
V -42 0
V -43 0
V -44 0
V 45 0
V -46 0
V 47 0
V -48 0
V -49 0
V -50 0
V 51 0
V 52 0
V -53 0
V 54 0
V -55 0
V 56 0
V -57 0
V 58 0
V 59 0
V -60 0
V -61 0
V -62 0
V 63 0
V -64 0
V 65 0
V -66 0
V -67 0
V -68 0
V -69 0
V -70 0
V -71 0
V -72 0
V -73 0
V -74 0
V -75 0
V 76 0
V 77 0
V -78 0
V -79 0
V -80 0
V -81 0
V -82 0
V -83 0
V -84 0
V -85 0
V -86 0
V -87 0
V -88 0
V -89 0
V -90 0
V -91 0
V 92 0
V -93 0
V 94 0
V -95 0
V 96 0
V -97 0
V 98 0
V -99 0
V -100 0
V -101 0
V 102 0
V -103 0
V -104 0
V -105 0
V 106 0
V -107 0
V -108 0
V -109 0
V -110 0
V 111 0
V -112 0
V -113 0
V -114 0
V -115 0
V -116 0
V -117 0
V -118 0
V -119 0
V -120 0
V -121 0
V -122 0
V -123 0
V -124 0
V -250 0
V -251 0
V -252 0
V -253 0
V -254 0
V -255 0
V -256 0
V -257 0
V -258 0
V -259 0
V -260 0
V -261 0
V -262 0
V -263 0
V -264 0
V -265 0
V -266 0
V -267 0
V -268 0
V -269 0
V -270 0
V -271 0
V -272 0
V -273 0
V -274 0
V -275 0
V -276 0
V -277 0
V -278 0
V -279 0
V -280 0
V -281 0
V -282 0
V -283 0
V -284 0
V -285 0
V -286 0
V -287 0
V -288 0
V -289 0
V -290 0
V -291 0
V -292 0
V -293 0
V -294 0
V -295 0
V -296 0
V -297 0
V -298 0
V -299 0
V -300 0
V -301 0
V -302 0
V -303 0
V -304 0
V -305 0
V -306 0
V -307 0
V -308 0
V -309 0
V -310 0
V -311 0
V -312 0
V -313 0
V -314 0
V -315 0
V -316 0
V -317 0
V -318 0
V -319 0
V -320 0
V -321 0
V -322 0
V 323 0
V -324 0
V -325 0
V -326 0
V -327 0
V -328 0
V -329 0
V -330 0
V -331 0
V -332 0
V -333 0
V -334 0
V -335 0
V -336 0
V -337 0
V -338 0
V -339 0
V -340 0
V -341 0
V -342 0
V -343 0
V -344 0
V -345 0
V -346 0
V -347 0
V -348 0
V -349 0
V -350 0
V -351 0
V -352 0
V -353 0
V -354 0
V -355 0
V -356 0
V -357 0
V -358 0
V -359 0
V -360 0
V -361 0
V -362 0
V -363 0
V -364 0
V -365 0
V -366 0
V -367 0
V -368 0
V -369 0
V -370 0
V -371 0
V -372 0
V -373 0
V -374 0
V -375 0
V -376 0
V -377 0
V -378 0
V -379 0
V -380 0
V -381 0
V -382 0
V -383 0
V -384 0
V -385 0
V -386 0
V -387 0
V -388 0
V -389 0
V -390 0
V -391 0
V -392 0
V -393 0
V -394 0
V -395 0
V -396 0
V -397 0
V -398 0
V -399 0
V -400 0
V -401 0
V -402 0
V -403 0
V -404 0
V -405 0
V -406 0
V -407 0
V -408 0
V -409 0
V -410 0
V -411 0
V -412 0
V -413 0
V -414 0
V -415 0
V -416 0
V -417 0
V -418 0
V -419 0
V -420 0
V -421 0
V -422 0
V -423 0
V -424 0
V -425 0
V -426 0
V -427 0
V -428 0
V -429 0
V -430 0
V -431 0
V -432 0
V -433 0
V -434 0
V -435 0
V -436 0
V -437 0
V -438 0
V -439 0
V -440 0
V -441 0
V -442 0
V -443 0
V -444 0
V -445 0
V -446 0
V -447 0
V -448 0
V -449 0
V -450 0
V -451 0
V -452 0
V -453 0
V -454 0
V -455 0
V -456 0
V -457 0
V -458 0
V -459 0
V -460 0
V -461 0
V -462 0
V -463 0
V -464 0
V -465 0
V -466 0
V -467 0
V -468 0
V -469 0
V -470 0
V -471 0
V -472 0
V -473 0
V -474 0
V -475 0
V -476 0
V -477 0
V -478 0
V -479 0
V -480 0
V -481 0
V -482 0
V -483 0
V -484 0
V -485 0
V -486 0
V -487 0
V -488 0
V -489 0
V -490 0
V -491 0
V -492 0
V -493 0
V -494 0
V -495 0
V -496 0
V -497 0
V -498 0
V -499 0
V -500 0
V -501 0
V -502 0
V -503 0
V -504 0
V -505 0
V -506 0
V -507 0
V -508 0
V -509 0
V -510 0
V -511 0
V -512 0
V -513 0
V -514 0
V -515 0
V -516 0
V -517 0
V -518 0
V -519 0
V -520 0
V -521 0
V -522 0
V -523 0
V -524 0
V -525 0
V -526 0
V -527 0
V -528 0
V -529 0
V -530 0
V -531 0
V -532 0
V -533 0
V -534 0
V -535 0
V -536 0
V -537 0
V -538 0
V -539 0
V -540 0
V -541 0
V -542 0
V -543 0
V -544 0
V -545 0
V -546 0
V -547 0
V -548 0
V -549 0
V -550 0
V -551 0
V -552 0
V -553 0
V -554 0
V -555 0
V -556 0
V -557 0
V -558 0
V -559 0
V -560 0
V -561 0
V -562 0
V -563 0
V -564 0
V -565 0
V -566 0
V -567 0
V -568 0
V -569 0
V -570 0
V -571 0
V -572 0
V -573 0
V -574 0
V -575 0
V -576 0
V -577 0
V -578 0
V -579 0
V -580 0
V -581 0
V -582 0
V -583 0
V -584 0
V -585 0
V -586 0
V -587 0
V -588 0
V -589 0
V -590 0
V -591 0
V -592 0
V -593 0
V -594 0
V -595 0
V -596 0
V -597 0
V -598 0
V -599 0
V -600 0
V -601 0
V -602 0
V -603 0
V -604 0
V -605 0
V -606 0
V -607 0
V -608 0
V -609 0
V -610 0
V -611 0
V -612 0
V -613 0
V -614 0
V -615 0
V -616 0
V -617 0
V -618 0
V -619 0
V -620 0
V -621 0
V -622 0
V -623 0
V -624 0
V -625 0
V -626 0
V -627 0
V -628 0
V -629 0
V -630 0
V -631 0
V -632 0
V -633 0
V -634 0
V -635 0
V -636 0
V -637 0
V -638 0
V -639 0
V -640 0
V -641 0
V -642 0
V -643 0
V -644 0
V -645 0
V -646 0
V -647 0
V -648 0
V -649 0
V -650 0
V -651 0
V -652 0
V -653 0
V -654 0
V -655 0
V -656 0
V -657 0
V -658 0
V -659 0
V -660 0
V -661 0
V -662 0
V -663 0
V -664 0
V -665 0
V -666 0
V -667 0
V -668 0
V -669 0
V -670 0
V -671 0
V -672 0
V -673 0
V -674 0
V -675 0
V -676 0
V -677 0
V -678 0
V -679 0
V -680 0
V -681 0
V -682 0
V -683 0
V -684 0
V -685 0
V -686 0
V -687 0
V -688 0
V -689 0
V -690 0
V -691 0
V -692 0
V -693 0
V -694 0
V -695 0
V -696 0
V -697 0
V 2058 0
V 2059 0
V 2060 0
V 2061 0
V 2062 0
V 2063 0
V 2064 0
V 2065 0
V 2066 0
V 2067 0
V 2068 0
V 2069 0
V 2070 0
V 2071 0
V 2072 0
V 2073 0
V 2074 0
V 2075 0
V 2076 0
V 2077 0
V 2078 0
V 2079 0
V 2080 0
V 2081 0
V 2082 0
V 2083 0
V 2084 0
V 2085 0
V 2086 0
V 2087 0
V 2088 0
V 2089 0
V 2090 0
V 2091 0
V 2092 0
V 2093 0
V 2094 0
V 2095 0
V 2096 0
V 2097 0
V 2098 0
V 2099 0
V 2100 0
V 2101 0
V 2102 0
V 2103 0
V 2104 0
V 2105 0
V 2106 0
V 2107 0
V 2108 0
V 2109 0
V 2110 0
V 2111 0
V 2112 0
V 2113 0
V 2114 0
V 2115 0
V 2116 0
V 2117 0
V 2118 0
V 2119 0
V 2120 0
V 2121 0
V 2122 0
V 2123 0
V 2124 0
V 2125 0
V 2126 0
V 2127 0
V 2128 0
V 2129 0
V 2130 0
V 2131 0
V 2132 0
V 2133 0
V 2134 0
V 2135 0
V 2136 0
V 2137 0
V 2138 0
V 2139 0
V 2140 0
V 2141 0
V 2142 0
V 2143 0
V 2144 0
V 2145 0
V 2146 0
V 2147 0
V 2148 0
V -2149 0
V -2150 0
V -2151 0
V -2152 0
V -2153 0
V -2154 0
V -2155 0
V -2156 0
V -2157 0
V -2158 0
V -2159 0
V -2160 0
V -2161 0
V -2162 0
V -2163 0
V -2164 0
V -2165 0
V -2166 0
V -2167 0
V -2168 0
V -2169 0
V -2170 0
V -2171 0
V -2172 0
V -2173 0
V -2174 0
V -2175 0
V -2176 0
V -2177 0
V -2178 0
V -2179 0
V -2180 0
V -2181 0
V 2182 0
V 2183 0
V 2184 0
V 2185 0
V 2186 0
V 2187 0
V 2188 0
V 2189 0
V 2190 0
V 2191 0
V 2192 0
V 2193 0
V 2194 0
V 2195 0
V 2196 0
V 2197 0
V 2198 0
V 2199 0
V 2200 0
V 2201 0
V 2202 0
V 2203 0
V 2204 0
V 2205 0
V 2206 0
V 2207 0
V 2208 0
V 2209 0
V 2210 0
V 2211 0
V 2212 0
V 2213 0
V 2214 0
V 2215 0
V 2216 0
V 2217 0
V 2218 0
V 2219 0
V 2220 0
V 2221 0
V -2222 0
V -2223 0
V -2224 0
V -2225 0
V -2226 0
V -2227 0
V -2228 0
V -2229 0
V -2230 0
V -2231 0
V -2232 0
V -2233 0
V -2234 0
V -2235 0
V -2236 0
V -2237 0
V -2238 0
V -2239 0
V -2240 0
V -2241 0
V -2242 0
V -2243 0
V 2244 0
V 2245 0
V 2246 0
V 2247 0
V 2248 0
V 2249 0
V 2250 0
V 2251 0
V 2252 0
V 2253 0
V 2254 0
V 2255 0
V 2256 0
V 2257 0
V 2258 0
V 2259 0
V 2260 0
V 2261 0
V 2262 0
V 2263 0
V 2264 0
V 2265 0
V -2266 0
V -2267 0
V -2268 0
V -2269 0
V -2270 0
V -2271 0
V -2272 0
V -2273 0
V -2274 0
V 2275 0
V 2276 0
V 2277 0
V 2278 0
V 2279 0
V 2280 0
V 2281 0
V 2282 0
V 2283 0
V -2284 0
V -2285 0
V -2286 0
V -2287 0
V -2288 0
V -2289 0
V 2290 0
V 2291 0
V 2292 0
V 2293 0
V 2294 0
V 2295 0
V -2296 0
V 2297 0
V 2298 0
V 2299 0
V 2300 0
V 2301 0
V 2302 0
V 2303 0
V 2304 0
V -2305 0
V 2306 0
V 2307 0
V 2308 0
V -2309 0
V 2310 0
V 2311 0
V 2312 0
V -2313 0
V -2314 0
V -2315 0
V -2316 0
V -2317 0
V 2318 0
V -2319 0
V -2320 0
V -2321 0
V -2322 0
V -2323 0
V 2324 0
V -2325 0
V 2326 0
V 2327 0
V -2328 0
V -2329 0
V -2330 0
V -2331 0
V 2332 0
V 2333 0
V 2334 0
V 2335 0
V 2336 0
V 2337 0
V 2338 0
V 2339 0
V 2340 0
V 2341 0
V 2342 0
V 2343 0
V 2344 0
V 2345 0
V 2346 0
V -2347 0
V -2348 0
V -2349 0
V 2350 0
V 2351 0
V 2352 0
V 2353 0
V 2354 0
V 2355 0
V -2356 0
V -2357 0
V 2358 0
V 2359 0
V -2360 0
V -2361 0
V 2362 0
V -2363 0
V 2364 0
V -2365 0
V 2366 0
V 2367 0
V 2368 0
V 2369 0
V 2370 0
V 2371 0
V 2372 0
V 2373 0
V 2374 0
V 2375 0
V 2376 0
V 2377 0
V 2378 0
V 2379 0
V 2380 0
V -2381 0
V 2382 0
V 2383 0
V 2384 0
V 2385 0
V 2386 0
V 2387 0
V 2388 0
V 2389 0
V 2390 0
V 2391 0
V 2392 0
V -2393 0
V 2394 0
V -2395 0
V 2396 0
V 2397 0
V 2398 0
V 2399 0
V 2400 0
V 2401 0
V 2402 0
V 2403 0
V 2404 0
V 2405 0
V 2406 0
V 2407 0
V 2408 0
V 2409 0
V 2410 0
V 2411 0
V 2412 0
V 2413 0
V 2414 0
V 2415 0
V -2416 0
V -2417 0
V -2418 0
V -2419 0
V -2420 0
V -2421 0
V -2422 0
V -2423 0
V -2424 0
V -2425 0
V -2426 0
V -2427 0
V -2428 0
V 2429 0
V 2430 0
V 2431 0
V 2432 0
V 2433 0
V 2434 0
V 2435 0
V 2436 0
V 2437 0
V -2438 0
V -2439 0
V -2440 0
V -2441 0
V -2442 0
V -2443 0
V 2444 0
V 2445 0
V 2446 0
V 2447 0
V 2448 0
V -2449 0
V -2450 0
V 2451 0
V 2452 0
V 2453 0
V 2454 0
V 2455 0
V 2456 0
V 2457 0
V -2458 0
V -2459 0
V -2460 0
V -2461 0
V 2462 0
V 2463 0
V 2464 0
V 2465 0
V 2466 0
V 2467 0
V -2468 0
V -2469 0
V -2470 0
V -2471 0
V 2472 0
V -2473 0
V -2474 0
V -2475 0
V -2476 0
V -2477 0
V 2478 0
V -2479 0
V 2480 0
V 2481 0
V 2482 0
V -2483 0
V 2484 0
V 2485 0
V 2486 0
V -2487 0
V 2488 0
V 2489 0
V 2490 0
V 2491 0
V 2492 0
V 2493 0
V 2494 0
V 2495 0
V 2496 0
V -2497 0
V -2498 0
V -2499 0
V -2500 0
V -2501 0
V -2502 0
V -2503 0
V 2504 0
V 2505 0
V 2506 0
V 2507 0
V -2508 0
V -2509 0
V -2510 0
V -2511 0
V 2512 0
V 2513 0
V 2514 0
V -2515 0
V 2516 0
V -2517 0
V 2518 0
V 2519 0
V 2520 0
V -2521 0
V -2522 0
V -2523 0
V -2524 0
V -2525 0
V 2526 0
V -2527 0
V 2528 0
V 2529 0
V 2530 0
V 2531 0
V 2532 0
V -2533 0
V -2534 0
V -2535 0
V 2536 0
V 2537 0
V -2538 0
V -2539 0
V 2540 0
V -2541 0
V 2542 0
V -2543 0
V 2544 0
V 2545 0
V 2546 0
V -2547 0
V 2548 0
V -2549 0
V 2550 0
V 2551 0
V 2552 0
V 2553 0
V 2554 0
V 2555 0
V 2556 0
V 2557 0
V 2558 0
V 2559 0
V 2560 0
V 2561 0
V 2562 0
V 2563 0
V 2564 0
V 2565 0
V 2566 0
V 2567 0
V 2568 0
V 2569 0
V 2570 0
V 2571 0
V 2572 0
V 2573 0
V 2574 0
V 2575 0
V 2576 0
V 2577 0
V 2578 0
V 2579 0
V 2580 0
V 2581 0
V 2582 0
V 2583 0
V 2584 0
V 2585 0
V 2586 0
V 2587 0
V 2588 0
V 2589 0
V 2590 0
V 2591 0
V 2592 0
V 2593 0
V 2594 0
V 2595 0
V 2596 0
V 2597 0
V 2598 0
V 2599 0
V 2600 0
V 2601 0
V 2602 0
V -2603 0
V -2604 0
V -2605 0
V -2606 0
V -2607 0
V -2608 0
V -2609 0
V -2610 0
V -2611 0
V -2612 0
V -2613 0
V 2614 0
V 2615 0
V 2616 0
V 2617 0
V 2618 0
V 2619 0
V 2620 0
V 2621 0
V 2622 0
V 2623 0
V 2624 0
V 2625 0
V 2626 0
V 2627 0
V 2628 0
V 2629 0
V 2630 0
V 2631 0
V 2632 0
V 2633 0
V 2634 0
V 2635 0
V 2636 0
V 2637 0
V 2638 0
V 2639 0
V -2640 0
V -2641 0
V -2642 0
V -2643 0
V -2644 0
V 2645 0
V 2646 0
V 2647 0
V 2648 0
V 2649 0
V 2650 0
V 2651 0
V 2652 0
V 2653 0
V 2654 0
V 2655 0
V -2656 0
V -2657 0
V -2658 0
V -2659 0
V 2660 0
V 2661 0
V 2662 0
V 2663 0
V 2664 0
V -2665 0
V -2666 0
V 2667 0
V -2668 0
V -2669 0
V 2670 0
V -2671 0
V 2672 0
V 2673 0
V 2674 0
V 2675 0
V 2676 0
V 2677 0
V 2678 0
V 2679 0
V 2680 0
V 2681 0
V 2682 0
V 2683 0
V 2684 0
V 2685 0
V -2686 0
V -2687 0
V 2688 0
V 2689 0
V 2690 0
V 2691 0
V 2692 0
V 2693 0
V 2694 0
V 2695 0
V 2696 0
V 2697 0
V -2698 0
V -2699 0
V 2700 0
V 2701 0
V -2702 0
V -2703 0
V 2704 0
V 2705 0
V 2706 0
V 2707 0
V 2708 0
V 2709 0
V 2710 0
V 2711 0
V 2712 0
V 2713 0
V 2714 0
V 2715 0
V 2716 0
V 2717 0
V 2718 0
V -2719 0
V 2720 0
V 2721 0
V 2722 0
V 2723 0
V 2724 0
V 2725 0
V 2726 0
V 2727 0
V 2728 0
V 2729 0
V 2730 0
V 2731 0
V 2732 0
V 2733 0
V 2734 0
V 2735 0
V 2736 0
V 2737 0
V 2738 0
V 2739 0
V 2740 0
V 2741 0
V 2742 0
V 2743 0
V 2744 0
V 2745 0
V 2746 0
V 2747 0
V 2748 0
V 2749 0
V 2750 0
V -2751 0
V 2752 0
V 2753 0
V 2754 0
V 2755 0
V 2756 0
V 2757 0
V 2758 0
V 2759 0
V 2760 0
V 2761 0
V 2762 0
V -2763 0
V 2764 0
V 2765 0
V 2766 0
V -2767 0
V 2768 0
V 2769 0
V 2770 0
V 2771 0
V 2772 0
V 2773 0
V 2774 0
V 2775 0
V 2776 0
V 2777 0
V 2778 0
V 2779 0
V 2780 0
V 2781 0
V 2782 0
V 2783 0
V 2784 0
V 2785 0
V 2786 0
V 2787 0
V 2788 0
V 2789 0
V 2790 0
V 2791 0
V 2792 0
V -2793 0
V -2794 0
V -2795 0
V -2796 0
V -2797 0
V -2798 0
V 2799 0
V 2800 0
V 2801 0
V 2802 0
V 2803 0
V 2804 0
V 2805 0
V 2806 0
V 2807 0
V 2808 0
V -2809 0
V -2810 0
V -2811 0
V -2812 0
V -2813 0
V 2814 0
V 2815 0
V 2816 0
V 2817 0
V -2818 0
V -2819 0
V -2820 0
V 2821 0
V -2822 0
V -2823 0
V 2824 0
V -2825 0
V 2826 0
V 2827 0
V 2828 0
V -2829 0
V 2830 0
V -2831 0
V 2832 0
V 2833 0
V 2834 0
V 2835 0
V 2836 0
V 2837 0
V 2838 0
V 2839 0
V -2840 0
V -2841 0
V 2842 0
V 2843 0
V 2844 0
V -2845 0
V 2846 0
V -2847 0
V 2848 0
V 2849 0
V 2850 0
V 2851 0
V 2852 0
V -2853 0
V 2854 0
V -2855 0
V 2856 0
V 2857 0
V 2858 0
V 2859 0
V 2860 0
V 2861 0
V 2862 0
V 2863 0
V 2864 0
V 2865 0
V 2866 0
V 2867 0
V 2868 0
V 2869 0
V 2870 0
V 2871 0
V 2872 0
V -2873 0
V 2874 0
V 2875 0
V 2876 0
V 2877 0
V 2878 0
V 2879 0
V 2880 0
V -2881 0
V 2882 0
V 2883 0
V 2884 0
V -2885 0
V 2886 0
V 2887 0
V 2888 0
V -2889 0
V 2890 0
V 2891 0
V 2892 0
V 2893 0
V 2894 0
V 2895 0
V 2896 0
V 2897 0
V 2898 0
V 2899 0
V 2900 0
V 2901 0
V 2902 0
V 2903 0
V 2904 0
V 2905 0
V 2906 0
V 2907 0
V 2908 0
V 2909 0
V 2910 0
V 2911 0
V 2912 0
V 2913 0
V 2914 0
V 2915 0
V 2916 0
V 2917 0
V 2918 0
V 2919 0
V 2920 0
V 2921 0

c Satisfiable