%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : HWV089-1 : TPTP v9.2.1. Released v6.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:24:24 PM UTC 2026 % Result : Unsatisfiable 0.30s 0.99s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.17 % Problem : HWV089-1 : TPTP v9.2.1. Released v6.1.0. % 0.11/0.18 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.44 % Computer : n004.cluster.edu % 0.16/0.44 % Model : x86_64 x86_64 % 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.44 % Memory : 8042.1875MB % 0.16/0.44 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.44 % CPULimit : 300 % 0.16/0.44 % WCLimit : 300 % 0.16/0.44 % DateTime : Thu May 7 12:08:34 EDT 2026 % 0.16/0.44 % CPUTime : % 0.16/0.44 SPASS-SCL-FOL version: % 0.20/0.53 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.30/0.95 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.95 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.95 Execution resolution_1 ended with status: unsatisfiable % 0.30/0.95 Used heuristic: resolution_1 % 0.30/0.95 % 0.30/0.95 Input Clauses: % 0.30/0.97 % 0.30/0.97 Predicates: v2123 sP296 sP164_aig_name nextState reachableState = v1 v1019 addressVal address v1019_range_3_to_0_address_association v953 v953_range_3_to_0_address_association v869 v869_range_3_to_0_address_association v791 v791_range_3_to_0_address_association addressDiff v3679 v3684 v8 range_2_0 v3660 v3668 v3666 v21 v18 v3661 v3662 v295 v284 v3643 v3644 v3645 v3650 b101 v3635 v31 sP295 v3636 v1253 v3637 v3639 v1247 v3611 v36 sP39_aig_name v898 v56 sP294 v1377 v1196 v3601 v3602 v3588 v3603 v3605 v3582 v3558 v67 v3556 v3555 v3593 v3594 v3595 v3597 v3577 v3578 v3586 v3579 v3580 v3560 v3561 v3563 v3567 v3569 v3568 v3565 v3564 range_3_1 sP50_aig_name v3571 v3562 v3453 v3552 v3551 v3536 v3546 v3544 v3455 v3537 v3538 v3540 v3521 v3491 sP293 v3487 v3479 v3471 v3467 v3463 v3475 v3483 v3524 b01 v3500 sP12_v3516_bitIndex6 v3426 v3434 v3432 v3436 v3437 sP290 sP291 sP292 v3427 v3428 v3398 sP289 v1017 v91 v896 v892 v889 v885 v97 v95 v3309 v3371 v3390 v3388 v3391 v3313 v887 v894 sP46_aig_name v3372 v3381 sP288 sP14_aig_name sP13_aig_name v109 v3373 v3375 sP287 v3358 v3331 sP283 sP284 sP285 sP286 v3323 sP282 v3324 v3325 v3327 v3205 v3285 v3293 v3291 v3207 v3286 v3287 v823 v3209 v3211 v3252 v3254 v3253 v3213 v3212 v3255 v3256 b10000 sP15_aig_name v3263 v3262 v3261 v3282 v3214 v3215 v3221 v3216 range_5_0 v3222 v3228 v3226 v3224 range_4_0 v3210 v1928 v1918 v1920 v1922 v1924 v1926 v3150 v3185 v3183 v3186 v3163 v3188 v2163 v2061 v1982 v3191 v3151 v3160 sP29_aig_name v3168 v3152 v3154 v1966 v1968 v1970 v1972 v1974 v1976 v1978 v1980 v3133 v3134 v2034 v3135 v3137 v2028 v2009 v1987 v1989 v1991 v1993 v1995 v1997 v1999 v2001 v2003 v2005 v2007 v3167 v2261 v3079 v3087 v3085 v2263 v2952 v3080 v3081 v1891 v3058 v3005 v2993 v2989 v741 v3059 v743 v3061 v3060 v2290 v3065 v3062 b10 sP281 v3101 v3006 v3008 v3009 v3010 v2927 v2876 v3022 v3021 v3026 v3019 v3030 v3017 v3035 v3015 sP278 sP279 sP280 sP276 sP277 sP275 v3004 v2994 v2996 v451 v2997 sP274 v2992 v2265 v2990 v2991 v2275 sP28_aig_name v2940 v2957 v2955 v2958 sP17_aig_name v2959 sP16_aig_name v2929 v2966 v2965 v2964 v2941 v2948 sP273 v2942 v2855 v2874 v2872 v2875 v2867 v2901 v2292 v2910 v2908 v2906 v2883 v2882 v2881 v2856 v2863 v2836 v2300 v2857 v2781 v2837 v2847 v2845 v2785 v2838 v2839 v2841 v2832 v2412 v2793 v2322 v2394 v2804 v2805 v151 v160 sP49_aig_name sP272 sP20_aig_name v145 sP19_aig_name v2828 sP21_aig_name sP18_aig_name sP267 sP268 sP269 sP270 sP271 v2831 v2830 v2829 v2825 sP253 sP254 sP255 sP256 sP257 sP258 sP259 sP260 sP261 sP262 sP263 sP264 sP265 sP266 b1001010 b1111010 b1110000 b1010000 b1111000 b1011000 b1100000 b1000000 v147 range_2_1 sP48_aig_name v149 range_14_13 v156 v2756 v2764 v2762 sP250 v2432 v2447 sP26_aig_name sP251 v2302 sP252 v2747 v2757 v2758 v204 v2750 b0001010 v2737 v2397 v2371 v2655 v2717 v2657 v2718 v2719 sP23_aig_name range_7_0 v2658 v2715 v2712 v2659 v2713 v2714 sP22_aig_name range_3_0 v2660 v2710 v2707 v2661 v2708 v2709 v2654 range_1_0 v2662 v2705 v2702 v2663 v2703 v2704 v2664 v2665 sP249 range_16_0 v2667 v2454 range_8_5 v2449 v2556 v2456 v2557 v2649 v2453 v2559 range_23_0 v2604 v2560 v2605 v2648 v2606 range_15_0 v2627 v2607 v2628 v2647 v2629 range_11_0 v2638 v2630 v2639 v2646 v2640 range_9_0 v2643 v2641 v2644 v2645 sP248 v2465 v2633 v2642 v2631 v2637 v2616 v2634 v2632 v2635 v2636 sP247 v2608 v2626 v2581 v2617 v2609 v2618 v2625 v2619 range_13_0 v2622 v2620 v2623 v2624 sP246 v2621 v2610 v2613 v2611 v2614 v2615 v2612 v2561 v2603 v2506 v2582 v2562 v2583 v2602 v2584 range_19_0 v2593 v2585 v2594 v2601 v2595 range_17_0 v2598 v2596 v2599 v2600 v2597 v2586 v2592 v2589 v2587 v2590 v2591 sP245 v2588 v2563 v2572 v2564 v2573 v2580 v2574 range_21_0 v2577 v2575 v2578 v2579 sP244 v2576 v2565 v2571 v2568 v2566 v2569 v2570 sP243 v2567 v2457 v2554 v2508 v2458 v2509 v2553 v2511 range_31_0 v2532 v2512 v2533 v2552 v2534 range_27_0 v2543 v2535 v2544 v2551 v2545 range_25_0 v2548 v2546 v2549 v2550 sP242 v2547 v2536 v2542 v2539 v2537 v2540 v2541 sP241 v2538 v2513 v2531 v2522 v2514 v2523 v2530 v2524 range_29_0 v2527 v2525 v2528 v2529 sP240 v2526 v2515 v2521 v2518 v2516 v2519 v2520 v2517 v2459 v2485 v2460 v2486 v2505 v2487 range_35_0 v2496 v2488 v2497 v2504 v2498 range_33_0 v2501 v2499 v2502 v2503 sP239 v2500 v2489 v2495 v2492 v2490 v2493 v2494 v2491 v2461 v2483 v2474 v2462 v2475 v2482 v2476 range_37_0 v2479 v2477 v2480 v2481 sP238 v2478 v2463 v2472 v2469 v2464 v2470 v2471 v2467 sP237 range_39_0 v2451 v2810 v2306 v2409 v2406 v2399 v2308 v2338 sP25_aig_name v2361 sP27_aig_name v2335 v2326 v2324 v2214 v2249 v2247 v2250 v2252 v2255 v2215 v2224 b001 b010 b100 v2216 v2218 v2190 v2198 v2196 v2187 v2191 v2193 v2136 v2144 v2142 v2065 v2063 v2137 v2138 v2129 v2089 v2099 sP30_aig_name b000000011100110100000000011 b000000011000110100000000011 sP236 range_26_0 v2023 v2024 v2032 sP235 range_63_0 v2025 v2026 v2231 v318 v1887 v1903 v1901 v1904 v1888 v1897 v668 v1889 v745 v747 range_66_63 v867 sP47_aig_name v1869 v1877 v1875 v871 v1870 v1872 v1846 v1847 v1848 v1854 v1853 v1831 sP234 v1823 sP233 v1824 v1825 v1827 v1805 sP231 sP232 v919 v921 v1787 v1795 v1793 v1021 v1788 v1790 v984 sP44_aig_name v1764 sP43_aig_name v1765 v1766 v1772 v1771 v1753 sP230 v1754 v1755 v1757 v1730 sP226 sP227 sP228 sP229 v1717 v1725 v1723 v1718 v1720 sP222 sP33_aig_name sP223 sP32_aig_name sP224 sP225 sP31_aig_name v1660 sP215 sP216 sP217 sP218 sP219 sP220 sP221 v1643 v1651 v1649 v1202 v1644 v1645 v1549 v1602 v1626 v1563 v1204 v1627 v1218 v1536 v1589 v1597 v1595 v1206 v1590 v1591 v1585 v1576 v1574 v1565 v1564 v1507 v1545 v1555 v1553 v1546 v1547 v1512 v1529 v1527 v1530 v1222 v1513 v1520 v1514 v1409 v1482 v1490 v1488 v1492 v1483 v1484 v1470 sP41_aig_name v1462 v1463 v1415 v1464 v1466 v1457 v1449 v1450 v1451 v1453 v1435 sP212 v1372 sP213 sP214 v1427 v1428 v1429 v1431 v1421 v1404 v1405 v1413 v1406 v1407 sP211 sP37_aig_name v1384 sP210 v1333 sP209 v1325 sP208 v1326 v1327 v1329 v1311 sP205 sP206 sP207 v1302 sP204 v1303 v1304 v1306 v1296 v1288 sP203 v1289 v1290 v1292 v1280 sP202 v1281 v1282 v1284 v1274 v1266 sP201 v1267 v1268 v1270 v1258 sP200 v1259 v1260 v1262 v1242 sP199 v1243 v1251 sP187 sP188 sP189 sP190 sP191 sP192 sP193 sP194 sP195 sP196 sP197 sP198 v1244 v1245 v1233 v1142 v1037 v1118 v1126 v1124 v1039 v1119 v1120 v1042 v1044 v1085 v1086 v1087 v1045 v1046 v1043 v1115 v1088 v1089 sP45_aig_name v1096 v1095 v1094 sP185 sP186 v1047 v1048 v1054 v1049 v1055 v1061 v1059 v1057 b00001 sP183 sP184 v923_array v923_1__array v1009 b000000000000000000 v1010 v1015 v1012 v997 v930 sP182 v998 v1004 v999 v980 v990 v988 v955 v981 v982 v957 v958 v959 v965 v964 v942 v936 v895 v888 v899 v900 v749_array v749_1__array v859 b0000000000000000000000000000000000000000000000000000000000000000000 v860 v865 v862 v847 v756 sP181 range_66_0 v848 v854 v849 v819 v829 v827 v793 v820 v821 v796 v797 v798 v804 v803 v780 range_10_0 v774 v768 v762 sP180 sP179 sP178 v724 v734 v682 v725 v726 v728 v704 v714 v696 v705 v706 v708 v657 v658 v661 v334 v659 v662 v412 v548 v660 v645 v653 v651 v342 v646 v648 v524 v638 v641 v637 v642 v348 v385 v621 v631 v629 v352 v622 v623 v625 v543 v545 v586 v588 v587 v547 v546 v589 v590 b01111 v597 v596 v595 v616 v549 v555 v550 v556 v562 v560 v558 v544 v536 v540 v537 v541 v538 v520 v530 v528 v521 v522 v508 v515 v507 v516 v491 v501 v499 v389 v492 v493 v495 v407 v409 v450 v452 v411 v410 v453 v454 v461 v460 v459 v480 v413 v419 v414 v420 v426 v424 v422 v408 v374 v372 sP2_v364_bitIndex8 v228 v291 v301 v299 v111 v292 v293 v223 v225 v260 v262 v261 v227 v226 v263 v264 v270 v269 v229 sP177 v235 v230 v236 v241 v239 v224 v200 v210 v208 v135 sP176 v184 v143 v201 v202 sP175 v170 v167 b0001001 b0100001 b0000001 b0100000 range_6_0 range_60_54 sP174 sP42_aig_name sP40_aig_name sP38_aig_name sP173 sP172 sP171 v2318 sP170 v2363 sP24_aig_name sP169 sP167 sP168 v3107 % 0.30/0.97 Fol Constants: bitIndex18 bitIndex19 bitIndex20 bitIndex21 bitIndex22 bitIndex23 bitIndex24 bitIndex25 bitIndex26 constB19 constB20 constB18 constB17 constB16 constB15 constB14 constB13 constB12 constB11 constB10 constB9 constB8 constB7 constB6 constB5 constB4 constB3 constB2 constB1 constB0 v1019_range_3_to_0_address_term_bound_20 v1019_range_3_to_0_address_term_bound_19 v1019_range_3_to_0_address_term_bound_18 v1019_range_3_to_0_address_term_bound_17 v1019_range_3_to_0_address_term_bound_16 v1019_range_3_to_0_address_term_bound_15 v1019_range_3_to_0_address_term_bound_14 v1019_range_3_to_0_address_term_bound_13 v1019_range_3_to_0_address_term_bound_12 v1019_range_3_to_0_address_term_bound_11 v1019_range_3_to_0_address_term_bound_10 v1019_range_3_to_0_address_term_bound_9 v1019_range_3_to_0_address_term_bound_8 v1019_range_3_to_0_address_term_bound_7 v1019_range_3_to_0_address_term_bound_6 v1019_range_3_to_0_address_term_bound_5 v1019_range_3_to_0_address_term_bound_4 v1019_range_3_to_0_address_term_bound_3 v1019_range_3_to_0_address_term_bound_2 v1019_range_3_to_0_address_term_bound_1 v1019_range_3_to_0_address_term_bound_0 v953_range_3_to_0_address_term_bound_20 v953_range_3_to_0_address_term_bound_19 v953_range_3_to_0_address_term_bound_18 v953_range_3_to_0_address_term_bound_17 v953_range_3_to_0_address_term_bound_16 v953_range_3_to_0_address_term_bound_15 v953_range_3_to_0_address_term_bound_14 v953_range_3_to_0_address_term_bound_13 v953_range_3_to_0_address_term_bound_12 v953_range_3_to_0_address_term_bound_11 v953_range_3_to_0_address_term_bound_10 v953_range_3_to_0_address_term_bound_9 v953_range_3_to_0_address_term_bound_8 v953_range_3_to_0_address_term_bound_7 v953_range_3_to_0_address_term_bound_6 v953_range_3_to_0_address_term_bound_5 v953_range_3_to_0_address_term_bound_4 v953_range_3_to_0_address_term_bound_3 v953_range_3_to_0_address_term_bound_2 v953_range_3_to_0_address_term_bound_1 v953_range_3_to_0_address_term_bound_0 v869_range_3_to_0_address_term_bound_20 v869_range_3_to_0_address_term_bound_19 v869_range_3_to_0_address_term_bound_18 v869_range_3_to_0_address_term_bound_17 v869_range_3_to_0_address_term_bound_16 v869_range_3_to_0_address_term_bound_15 v869_range_3_to_0_address_term_bound_14 v869_range_3_to_0_address_term_bound_13 v869_range_3_to_0_address_term_bound_12 v869_range_3_to_0_address_term_bound_11 v869_range_3_to_0_address_term_bound_10 v869_range_3_to_0_address_term_bound_9 v869_range_3_to_0_address_term_bound_8 v869_range_3_to_0_address_term_bound_7 v869_range_3_to_0_address_term_bound_6 v869_range_3_to_0_address_term_bound_5 v869_range_3_to_0_address_term_bound_4 v869_range_3_to_0_address_term_bound_3 v869_range_3_to_0_address_term_bound_2 v869_range_3_to_0_address_term_bound_1 v869_range_3_to_0_address_term_bound_0 b1110_address_term b1101_address_term b1100_address_term b1011_address_term b1010_address_term b1001_address_term b1000_address_term b0111_address_term b0100_address_term b0011_address_term b0010_address_term b1111_address_term v791_range_3_to_0_address_term_bound_20 v791_range_3_to_0_address_term_bound_19 v791_range_3_to_0_address_term_bound_18 v791_range_3_to_0_address_term_bound_17 v791_range_3_to_0_address_term_bound_16 v791_range_3_to_0_address_term_bound_15 v791_range_3_to_0_address_term_bound_14 v791_range_3_to_0_address_term_bound_13 v791_range_3_to_0_address_term_bound_12 v791_range_3_to_0_address_term_bound_11 v791_range_3_to_0_address_term_bound_10 v791_range_3_to_0_address_term_bound_9 v791_range_3_to_0_address_term_bound_8 v791_range_3_to_0_address_term_bound_7 v791_range_3_to_0_address_term_bound_6 v791_range_3_to_0_address_term_bound_5 v791_range_3_to_0_address_term_bound_4 v791_range_3_to_0_address_term_bound_3 v791_range_3_to_0_address_term_bound_2 v791_range_3_to_0_address_term_bound_1 v791_range_3_to_0_address_term_bound_0 b0101_address_term b0001_address_term b0110_address_term b0000_address_term bitIndex3 bitIndex2 bitIndex1 bitIndex0 bitIndex4 bitIndex5 bitIndex6 bitIndex11 bitIndex10 bitIndex9 bitIndex8 bitIndex7 bitIndex17 bitIndex12 bitIndex13 bitIndex14 bitIndex15 bitIndex16 bitIndex27 bitIndex28 bitIndex29 bitIndex30 bitIndex31 bitIndex53 bitIndex32 bitIndex33 bitIndex34 bitIndex35 bitIndex36 bitIndex37 bitIndex38 bitIndex39 bitIndex40 bitIndex41 bitIndex42 bitIndex43 bitIndex44 bitIndex45 bitIndex46 bitIndex47 bitIndex48 bitIndex49 bitIndex50 bitIndex51 bitIndex52 bitIndex54 bitIndex55 bitIndex56 bitIndex57 bitIndex58 bitIndex59 bitIndex60 bitIndex61 bitIndex62 bitIndex63 bitIndex66 bitIndex65 bitIndex64 % 0.30/0.97 Fol Functions: % 0.30/0.97 Problem Properties: % 0.30/0.97 This is a Bernays Schoenfinkel Ramsey problem. % 0.30/0.97 % 0.30/0.97 % 0.30/0.97 Reduced Input Clauses: % 0.30/0.97 11792:1:1:[9992.0,139.1]:Top: addressVal(v1019_range_3_to_0_address_term_bound_0,x0) -> % 0.30/0.97 11793:1:1:[10222.0,307.1]:Top: addressVal(v869_range_3_to_0_address_term_bound_0,x0) -> % 0.30/0.97 11794:2:2:[430.1,428.1]:TopTop: v3666(x0,x1) -> v21(x0,x1) % 0.30/0.97 11795:7:1:[506.0,513.3]:Top: v3611(x0) -> v1377(x0,bitIndex4),v1377(x0,bitIndex2),v31(x0,bitIndex9),v31(x0,bitIndex6),v31(x0,bitIndex3),v31(x0,bitIndex0) % 0.30/0.97 11796:2:2:[558.1,556.1]:TopTop: v3586(x0,x1) -> v67(x0,x1) % 0.30/0.97 11797:2:2:[572.1,570.1]:TopTop: v3558(x0,x1) -> v3560(x0,x1) % 0.30/0.97 11798:4:2:[579.0,573.1]:TopTop: v3560(x0,x1) -> v3563(x0),v3567(x0),v56(x0,x1) % 0.30/0.97 11799:4:2:[580.0,574.1]:TopTop: v56(x0,x1) -> v3563(x0),v3567(x0),v3560(x0,x1) % 0.30/0.97 11800:2:2:[633.1,631.1]:TopTop: v3544(x0,x1) -> v3455(x0,x1) % 0.30/0.97 11801:2:2:[643.0,644.2]:TopTop: v3453(x0,bitIndex0),v3455(x0,x1) -> % 0.30/0.97 11803:2:2:[643.0,645.1,11801.0,11802.2]:TopTop: v3455(x0,x1) -> v3521(x0,x1) % 0.30/0.97 11805:2:2:[662.1,659.2,661.1,11804.3]:TopTop: v3524(x0,x1) -> b01(x1) % 0.30/0.97 11806:2:1:[683.1,681.1]:Top: v3432(x0) -> v3436(x0) % 0.30/0.97 11808:4:1:[692.1,697.2,688.1,11807.3]:Top: v36(x0,bitIndex9),sP292(x0) -> v36(x0,bitIndex6),v36(x0,bitIndex3) % 0.30/0.97 11809:2:2:[746.1,745.1]:TopTop: v3391(x0,x1) -> v3388(x0,x1) % 0.30/0.97 11810:2:2:[888.1,886.1]:TopTop: v3291(x0,x1) -> v3207(x0,x1) % 0.30/0.97 11811:4:2:[902.0,896.1]:TopTop: v3207(x0,x1) -> v3211(x0),v3252(x0),v3205(x0,x1) % 0.30/0.97 11812:4:2:[903.0,897.1]:TopTop: v3205(x0,x1) -> v3211(x0),v3252(x0),v3207(x0,x1) % 0.30/0.97 11813:2:1:[1042.0,1043.2]:Top: v3222(x0,bitIndex0) -> v3228(x0) % 0.30/0.97 11814:2:1:[1089.1,1087.1]:Top: v3183(x0) -> v3186(x0) % 0.30/0.97 11815:2:1:[1203.1,1204.0]:Top: -> sP281(x0),v3065(x0,bitIndex3) % 0.30/0.97 11817:2:1:[11815.2,1205.0,1203.1,11816.1]:Top: -> sP281(x0),v3065(x0,bitIndex2) % 0.30/0.97 11820:2:1:[11817.3,1206.0,11815.2,11818.1,1203.1,11819.2]:Top: -> sP281(x0),v3065(x0,bitIndex1) % 0.30/0.97 11824:2:1:[11820.4,1207.0,11817.3,11821.1,11815.2,11822.2,1203.1,11823.3]:Top: -> sP281(x0),v3065(x0,bitIndex0) % 0.30/0.97 11825:4:1:[1285.0,1282.4]:Top: v2290(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP278(x0) % 0.30/0.97 11826:4:1:[11825.0,1283.4]:Top: v2927(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP278(x0) % 0.30/0.97 11827:3:1:[1292.0,1294.3]:Top: sP278(x0),v2290(x0,bitIndex2) -> sP279(x0) % 0.30/0.97 11828:3:1:[1292.1,1295.3]:Top: sP278(x0),v2927(x0,bitIndex2) -> sP279(x0) % 0.30/0.97 11829:3:1:[1303.0,1305.3]:Top: sP279(x0),v2290(x0,bitIndex3) -> sP280(x0) % 0.30/0.97 11830:3:1:[1303.1,1306.3]:Top: sP279(x0),v2927(x0,bitIndex3) -> sP280(x0) % 0.30/0.97 11831:4:1:[1328.0,1325.4]:Top: v2290(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP276(x0) % 0.30/0.97 11832:4:1:[11831.0,1326.4]:Top: v2927(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP276(x0) % 0.30/0.97 11833:3:1:[1335.0,1337.3]:Top: sP276(x0),v2290(x0,bitIndex2) -> sP277(x0) % 0.30/0.97 11834:3:1:[1335.1,1338.3]:Top: sP276(x0),v2927(x0,bitIndex2) -> sP277(x0) % 0.30/0.97 11835:3:1:[11751.1,11758.2]:Top: v160(x0,bitIndex3) -> sP18_aig_name(x0),v160(x0,bitIndex4) % 0.30/0.97 11836:4:1:[1360.0,1357.4]:Top: v2290(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP275(x0) % 0.30/0.97 11837:4:1:[11836.0,1358.4]:Top: v2927(x0,bitIndex1),v2927(x0,bitIndex0),v2290(x0,bitIndex0) -> sP275(x0) % 0.30/0.97 11838:2:1:[1520.0,1521.2]:Top: v2290(x0,bitIndex0) -> v2910(x0) % 0.30/0.97 11839:2:2:[1592.1,1590.1]:TopTop: v2845(x0,x1) -> v2785(x0,x1) % 0.30/0.97 11840:5:1:[1612.2,1614.0]:Top: v160(x0,bitIndex6),v145(x0,bitIndex2),sP272(x0) -> v145(x0,bitIndex1),sP20_aig_name(x0) % 0.30/0.97 11841:5:1:[1612.2,1615.0]:Top: v145(x0,bitIndex1),v160(x0,bitIndex6),sP272(x0) -> v145(x0,bitIndex2),sP20_aig_name(x0) % 0.30/0.97 11842:8:2:[1653.4,1651.0]:TopTop: v160(x0,bitIndex3),v160(x0,bitIndex4),v160(x0,bitIndex5),v160(x0,bitIndex6),v2828(x0,x1) -> v160(x0,bitIndex0),v160(x0,bitIndex2),addressVal(b0100_address_term,x1) % 0.30/0.97 11843:7:2:[1653.0,1654.2]:TopTop: v160(x0,bitIndex6),v2828(x0,x1) -> v160(x0,bitIndex3),v160(x0,bitIndex0),v160(x0,bitIndex1),v160(x0,bitIndex2),v2829(x0,x1) % 0.30/0.97 11844:2:2:[1666.1,1667.1]:TopTop: v2829(x0,x1) -> addressVal(b0001_address_term,x1) % 0.30/0.97 11845:3:1:[1674.1,1681.3]:Top: v160(x0,bitIndex1),sP254(x0) -> v160(x0,bitIndex3) % 0.30/0.97 11846:3:1:[11741.3,11745.1]:Top: v160(x0,bitIndex4),sP20_aig_name(x0) -> v160(x0,bitIndex1) % 0.30/0.97 11848:3:1:[11742.4,11744.0,11846.0,11847.2]:Top: sP20_aig_name(x0) -> v160(x0,bitIndex3),v160(x0,bitIndex1) % 0.30/0.97 11849:4:1:[11846.0,11742.3]:Top: sP20_aig_name(x0) -> v160(x0,bitIndex1),v160(x0,bitIndex3),v160(x0,bitIndex5) % 0.30/0.97 11850:3:1:[1689.1,1696.3]:Top: v160(x0,bitIndex1),sP256(x0) -> v160(x0,bitIndex3) % 0.30/0.97 11851:3:1:[1704.1,1710.3]:Top: v160(x0,bitIndex1),sP258(x0) -> v160(x0,bitIndex3) % 0.30/0.97 11852:3:1:[1724.1,1730.3]:Top: v160(x0,bitIndex1),sP261(x0) -> v160(x0,bitIndex3) % 0.30/0.97 11853:3:1:[1738.1,1745.3]:Top: v160(x0,bitIndex1),sP263(x0) -> v160(x0,bitIndex3) % 0.30/0.97 11856:6:1:[1865.1,1871.2,1850.1,11854.3,8282.1,11855.5]:Top: v2322(x0),sP252(x0) -> v2302(x0,bitIndex12),v2302(x0,bitIndex9),v2302(x0,bitIndex6),v2302(x0,bitIndex3) % 0.30/0.97 11858:7:1:[1866.0,1873.1,1851.0,11857.2]:Top: sP252(x0) -> v2394(x0,bitIndex1),v2302(x0,bitIndex12),v2412(x0),v2302(x0,bitIndex9),v2302(x0,bitIndex6),v2302(x0,bitIndex3) % 0.30/0.97 11859:2:1:[1884.1,1882.1]:Top: v2762(x0) -> sP252(x0) % 0.30/0.98 11860:2:1:[8365.1,8363.1]:Top: v2247(x0) -> v2250(x0) % 0.30/0.98 11861:2:1:[8405.1,8403.1]:Top: v2196(x0) -> v2187(x0) % 0.30/0.98 11862:2:1:[8424.1,8421.1]:Top: v2142(x0) -> v2065(x0) % 0.30/0.98 11863:2:1:[8424.1,8422.1]:Top: v2142(x0) -> v2063(x0) % 0.30/0.98 11864:2:1:[8436.1,8434.1]:Top: v2065(x0) -> v2129(x0) % 0.30/0.98 11865:2:1:[8442.2,8438.1]:Top: v2129(x0) -> sP30_aig_name(x0) % 0.30/0.98 11866:2:1:[8444.2,8440.1]:Top: v2129(x0) -> sP164_aig_name(x0) % 0.30/0.98 11867:2:2:[8557.1,8555.1]:TopTop: v2032(x0,x1) -> v1987(x0,x1) % 0.30/0.98 11868:2:1:[8670.1,8668.1]:Top: v1901(x0) -> v1904(x0) % 0.30/0.98 11869:2:2:[8720.1,8718.1]:TopTop: v1875(x0,x1) -> v871(x0,x1) % 0.30/0.98 11870:4:1:[8823.1,8821.3]:Top: v1377(x0,bitIndex2),v31(x0,bitIndex8) -> sP231(x0),v31(x0,bitIndex2) % 0.30/0.98 11871:4:1:[8824.1,8822.3]:Top: v1377(x0,bitIndex4),v31(x0,bitIndex8) -> sP231(x0),v31(x0,bitIndex2) % 0.30/0.98 11872:4:1:[8820.0,8832.3]:Top: sP232(x0) -> v1377(x0,bitIndex4),v1377(x0,bitIndex2),v31(x0,bitIndex9) % 0.30/0.98 11873:2:2:[8853.1,8851.1]:TopTop: v1793(x0,x1) -> v1021(x0,x1) % 0.30/0.98 11874:4:1:[8939.1,8937.3]:Top: v1377(x0,bitIndex2),v31(x0,bitIndex8) -> sP226(x0),v31(x0,bitIndex2) % 0.30/0.98 11875:4:1:[8940.1,8938.3]:Top: v1377(x0,bitIndex4),v31(x0,bitIndex8) -> sP226(x0),v31(x0,bitIndex2) % 0.30/0.98 11876:6:1:[8936.0,8943.3]:Top: sP227(x0) -> v1377(x0,bitIndex4),v1377(x0,bitIndex2),v31(x0,bitIndex6),v31(x0,bitIndex3),v31(x0,bitIndex0) % 0.30/0.98 11877:2:1:[8950.1,8959.2]:Top: v898(x0,bitIndex1),sP229(x0) -> % 0.30/0.98 11878:2:1:[8951.1,8960.2]:Top: v898(x0,bitIndex2),sP229(x0) -> % 0.30/0.98 11879:2:1:[8952.0,8961.2]:Top: sP229(x0) -> v898(x0,bitIndex0) % 0.30/0.98 11880:2:1:[8953.1,8962.2]:Top: v1017(x0,bitIndex17),sP229(x0) -> % 0.30/0.98 11881:2:1:[8954.1,8963.2]:Top: v1017(x0,bitIndex15),sP229(x0) -> % 0.30/0.98 11882:2:1:[8955.0,8964.2]:Top: sP229(x0) -> v1017(x0,bitIndex0) % 0.30/0.98 11883:2:1:[8957.1,8965.2]:Top: v56(x0,bitIndex2),sP229(x0) -> % 0.30/0.98 11884:2:1:[8979.1,8978.1]:Top: v36(x0,bitIndex0) -> v1723(x0) % 0.30/0.98 11886:6:1:[8995.1,8999.5,8993.1,11885.6]:Top: v36(x0,bitIndex0),sP32_aig_name(x0) -> v31(x0,bitIndex0),v31(x0,bitIndex6),sP225(x0),sP222(x0) % 0.30/0.98 11887:6:1:[8997.1,9004.3]:Top: v36(x0,bitIndex0),sP31_aig_name(x0) -> v31(x0,bitIndex8),sP224(x0),sP223(x0),sP222(x0) % 0.30/0.98 11890:4:1:[8997.1,9005.3,8995.1,11888.4,8993.1,11889.5]:Top: v36(x0,bitIndex0),sP31_aig_name(x0),sP32_aig_name(x0) -> sP222(x0) % 0.30/0.98 11891:9:1:[9007.7,9009.1]:Top: v1377(x0,bitIndex2),v1196(x0),v31(x0,bitIndex2),sP215(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11892:9:1:[9007.7,9010.2]:Top: v1377(x0,bitIndex2),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex2),sP215(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11893:9:1:[9008.7,9011.1]:Top: v1377(x0,bitIndex4),v1196(x0),v31(x0,bitIndex2),sP215(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11894:9:1:[9008.7,9012.2]:Top: v1377(x0,bitIndex4),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex2),sP215(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11895:9:1:[9013.7,9015.1]:Top: v1377(x0,bitIndex2),v1196(x0),v31(x0,bitIndex5),sP216(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11896:9:1:[9013.7,9016.2]:Top: v1377(x0,bitIndex2),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex5),sP216(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11897:9:1:[9014.7,9017.1]:Top: v1377(x0,bitIndex4),v1196(x0),v31(x0,bitIndex5),sP216(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11898:9:1:[9014.7,9018.2]:Top: v1377(x0,bitIndex4),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex5),sP216(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11899:9:1:[9019.7,9021.1]:Top: v1377(x0,bitIndex2),v1196(x0),v31(x0,bitIndex8),sP217(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11900:9:1:[9019.7,9022.2]:Top: v1377(x0,bitIndex2),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex8),sP217(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11901:9:1:[9020.7,9023.1]:Top: v1377(x0,bitIndex4),v1196(x0),v31(x0,bitIndex8),sP217(x0) -> v1017(x0,bitIndex0),v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11902:9:1:[9020.7,9024.2]:Top: v1377(x0,bitIndex4),v1017(x0,bitIndex15),v1196(x0),v31(x0,bitIndex8),sP217(x0) -> v56(x0,bitIndex2),v1017(x0,bitIndex17),v898(x0,bitIndex2),v898(x0,bitIndex1) % 0.30/0.99 11903:2:1:[9055.1,9053.1]:Top: v1649(x0) -> v1202(x0) % 0.30/0.99 11904:2:1:[9063.1,9064.1]:Top: v1202(x0) -> v1626(x0) % 0.30/0.99 11905:2:1:[1102.0,9071.2]:Top: v1218(x0) -> v1627(x0) % 0.30/0.99 11906:2:2:[9085.1,9083.1]:TopTop: v1595(x0,x1) -> v1206(x0,x1) % 0.30/0.99 11907:3:2:[9100.3,9098.3]:TopTop: v1206(x0,x1),v1204(x0,bitIndex1),v1204(x0,bitIndex2) -> % 0.30/0.99 11908:5:2:[11907.1,9101.5]:TopTop: v1206(x0,x1),v1204(x0,bitIndex3),v1204(x0,bitIndex2),v1204(x0,bitIndex0) -> v1585(x0,x1) % 0.30/0.99 11909:5:2:[9097.1,9104.5]:TopTop: v1206(x0,x1),v1204(x0,bitIndex2),v1204(x0,bitIndex0) -> v1574(x0,x1),v1204(x0,bitIndex3) % 0.30/0.99 11910:5:2:[9095.1,9107.2]:TopTop: v1206(x0,x1) -> v1564(x0,x1),v1204(x0,bitIndex2),v1204(x0,bitIndex1),v1204(x0,bitIndex0) % 0.30/0.99 11911:1:2:[9110.1,9109.1]:TopTop: v1585(x0,x1) -> % 0.30/0.99 11912:1:2:[9131.1,9130.1]:TopTop: v1574(x0,x1) -> % 0.30/0.99 11913:2:2:[9143.1,9144.1]:TopTop: v1564(x0,x1) -> v1507(x0,x1) % 0.30/0.99 11914:1:1:[9158.1,9157.1]:Top: v1553(x0) -> % 0.30/0.99 11915:2:2:[9177.1,9175.1]:TopTop: v1527(x0,x1) -> v1530(x0,x1) % 0.30/0.99 11916:3:2:[9198.2,9196.0]:TopTop: v1222(x0,bitIndex3),nextState(x0,x1) -> v1520(x1) % 0.30/0.99 11918:3:2:[9198.2,9197.0,11916.1,11917.4]:TopTop: v1222(x0,bitIndex1),nextState(x0,x1) -> v1520(x1) % 0.30/0.99 11919:2:1:[9212.1,9210.1]:Top: v1488(x0) -> v1492(x0) % 0.30/0.99 11920:5:1:[9387.1,9281.2]:Top: v36(x0,bitIndex1),v1377(x0,bitIndex2),v1196(x0) -> sP212(x0),v1372(x0,bitIndex0) % 0.30/0.99 11921:5:1:[9388.1,9283.2]:Top: v36(x0,bitIndex7),v1377(x0,bitIndex2),v1196(x0) -> sP212(x0),v1372(x0,bitIndex0) % 0.30/0.99 11922:5:1:[9387.1,9289.2]:Top: v36(x0,bitIndex1),v1377(x0,bitIndex4),v1196(x0) -> sP213(x0),v1372(x0,bitIndex0) % 0.30/0.99 11923:5:1:[9388.1,9291.2]:Top: v36(x0,bitIndex7),v1377(x0,bitIndex4),v1196(x0) -> sP213(x0),v1372(x0,bitIndex0) % 0.30/0.99 11925:2:1:[9285.1,9292.2,9277.1,11924.3]:Top: v1372(x0,bitIndex0),sP214(x0) -> % 0.30/0.99 11927:2:1:[9286.0,9293.2,9278.0,11926.3]:Top: sP214(x0) -> v1372(x0,bitIndex1) % 0.30/0.99 11929:4:1:[9288.0,9295.4,9280.0,11928.5]:Top: sP214(x0) -> v36(x0,bitIndex7),v36(x0,bitIndex4),v36(x0,bitIndex1) % 0.30/0.99 11930:4:1:[9387.1,9298.2]:Top: v36(x0,bitIndex1),v1377(x0,bitIndex0) -> sP214(x0),v1372(x0,bitIndex0) % 0.30/0.99 11931:4:1:[9388.1,9300.2]:Top: v36(x0,bitIndex7),v1377(x0,bitIndex0) -> sP214(x0),v1372(x0,bitIndex0) % 0.30/0.99 11932:2:1:[9350.1,9342.1]:Top: v1413(x0,bitIndex3) -> v1222(x0,bitIndex4) % 0.30/0.99 11933:2:1:[9350.1,9344.1]:Top: v1413(x0,bitIndex2) -> v1222(x0,bitIndex3) % 0.30/0.99 11934:2:1:[9350.1,9346.1]:Top: v1413(x0,bitIndex1) -> v1222(x0,bitIndex2) % 0.30/0.99 11935:2:1:[9350.1,9348.1]:Top: v1413(x0,bitIndex0) -> v1222(x0,bitIndex1) % 0.30/0.99 11936:3:1:[9360.0,9363.3]:Top: v1222(x0,bitIndex3) -> v1377(x0,bitIndex0),v1196(x0) % 0.30/0.99 11937:2:1:[9362.0,9368.2]:Top: v1222(x0,bitIndex3) -> sP37_aig_name(x0) % 0.30/0.99 11938:5:1:[9384.1,9371.0]:Top: v1377(x0,bitIndex2),v1372(x0,bitIndex0),v1196(x0),sP210(x0) -> v1372(x0,bitIndex1) % 0.30/0.99 11939:5:1:[9384.1,9375.0]:Top: v1377(x0,bitIndex4),v1372(x0,bitIndex0),v1196(x0) -> v1384(x0),v1372(x0,bitIndex1) % 0.30/0.99 11940:4:1:[9384.1,9378.0]:Top: v1377(x0,bitIndex0),v1372(x0,bitIndex0) -> v1384(x0),v1372(x0,bitIndex1) % 0.30/0.99 11986:2:1:[11653.1,11661.2]:Top: v898(x0,bitIndex2) -> sP32_aig_name(x0) % 0.30/0.99 11985:2:1:[11652.1,11660.2]:Top: v898(x0,bitIndex1) -> sP32_aig_name(x0) % 0.30/0.99 11941:7:1:[9397.0,9405.3]:Top: v1333(x0) -> v1377(x0,bitIndex4),v1377(x0,bitIndex2),v31(x0,bitIndex9),v31(x0,bitIndex6),v31(x0,bitIndex3),v31(x0,bitIndex0) % 0.30/0.99 11943:3:1:[9448.0,9454.3,9442.0,11942.4]:Top: sP207(x0) -> v31(x0,bitIndex9),v1196(x0) % 0.30/0.99 11984:2:1:[11650.1,11659.2]:Top: sP42_aig_name(x0) -> sP32_aig_name(x0) % 0.30/0.99 11945:4:1:[9451.0,9457.4,9445.0,11944.5]:Top: sP207(x0) -> v31(x0,bitIndex9),v1377(x0,bitIndex4),v1377(x0,bitIndex2) % 0.30/0.99 11983:2:1:[11649.0,11657.1]:Top: -> sP32_aig_name(x0),v1196(x0) % 0.30/0.99 11947:2:1:[9450.0,9460.2,9444.0,11946.3]:Top: sP207(x0) -> v56(x0,bitIndex2) % 0.30/0.99 11948:2:2:[9764.1,9762.1]:TopTop: v1124(x0,x1) -> v1039(x0,x1) % 0.30/0.99 11949:2:1:[9938.0,9939.2]:Top: v1055(x0,bitIndex0) -> v1061(x0) % 0.30/0.99 11950:2:2:[10118.1,10116.1]:TopTop: v988(x0,x1) -> v955(x0,x1) % 0.30/0.99 11951:2:2:[10463.1,10461.1]:TopTop: v827(x0,x1) -> v793(x0,x1) % 0.30/0.99 11952:2:1:[10732.1,10734.0]:Top: v451(x0,bitIndex0) -> v658(x0) % 0.30/0.99 11953:2:1:[10741.1,10740.1]:Top: v662(x0) -> v661(x0) % 0.30/0.99 11954:1:1:[10743.1,10742.1]:Top: v662(x0) -> % 0.30/0.99 11955:2:1:[10746.1,10744.1]:Top: v659(x0) -> v660(x0) % 0.30/0.99 11956:2:1:[10757.1,10756.1]:Top: v342(x0,bitIndex0) -> v651(x0) % 0.30/0.99 11957:1:1:[10773.1,10772.0]:Top: -> v642(x0) % 0.30/0.99 11958:2:2:[10794.1,10792.1]:TopTop: v629(x0,x1) -> v352(x0,x1) % 0.30/0.99 11959:4:2:[10810.0,10804.1]:TopTop: v352(x0,x1) -> v545(x0),v586(x0),v348(x0,x1) % 0.30/0.99 11960:4:2:[10811.0,10805.1]:TopTop: v348(x0,x1) -> v545(x0),v586(x0),v352(x0,x1) % 0.30/0.99 11961:2:1:[10951.0,10952.2]:Top: v556(x0,bitIndex0) -> v562(x0) % 0.30/0.99 11962:2:1:[10985.1,10983.1]:Top: v540(x0) -> v541(x0) % 0.30/0.99 11963:2:1:[10990.0,10989.0]:Top: v538(x0) -> v537(x0) % 0.30/0.99 11964:1:1:[10992.1,10991.1]:Top: v538(x0) -> % 0.30/0.99 11965:2:1:[11004.1,11002.1]:Top: v528(x0) -> v342(x0,bitIndex1) % 0.30/0.99 11966:1:1:[11022.0,11021.0]:Top: -> v516(x0) % 0.30/0.99 11967:2:2:[11041.1,11039.1]:TopTop: v499(x0,x1) -> v389(x0,x1) % 0.30/0.99 11968:4:2:[11057.0,11051.1]:TopTop: v389(x0,x1) -> v409(x0),v450(x0),v385(x0,x1) % 0.30/0.99 11969:4:2:[11058.0,11052.1]:TopTop: v385(x0,x1) -> v409(x0),v450(x0),v389(x0,x1) % 0.30/0.99 11970:2:1:[11210.0,11211.2]:Top: v420(x0,bitIndex0) -> v426(x0) % 0.30/0.99 11971:2:2:[11250.1,11248.1]:TopTop: v299(x0,x1) -> v111(x0,x1) % 0.30/0.99 11972:4:2:[11266.0,11260.1]:TopTop: v111(x0,x1) -> v225(x0),v260(x0),v109(x0,x1) % 0.30/0.99 11973:4:2:[11267.0,11261.1]:TopTop: v109(x0,x1) -> v225(x0),v260(x0),v111(x0,x1) % 0.30/0.99 11974:2:1:[11431.0,11432.2]:Top: v236(x0,bitIndex0) -> v241(x0) % 0.30/0.99 11975:4:1:[11475.1,11469.1]:Top: v208(x0) -> v184(x0,bitIndex0),v184(x0,bitIndex1),v184(x0,bitIndex2) % 0.30/0.99 11976:2:1:[11475.1,11470.1]:Top: v208(x0) -> sP176(x0) % 0.30/0.99 11977:2:1:[11475.1,11471.1]:Top: v208(x0) -> v143(x0) % 0.30/0.99 11978:7:1:[11499.0,11498.7]:Top: v151(x0,bitIndex12) -> v167(x0),v160(x0,bitIndex6),v160(x0,bitIndex4),v160(x0,bitIndex3),v160(x0,bitIndex2),v160(x0,bitIndex1) % 0.30/0.99 11979:4:1:[11621.0,11620.1]:Top: -> sP174(x0),v1017(x0,bitIndex0),v1047(x0),v1017(x0,bitIndex17) % 0.30/0.99 11980:4:1:[11638.0,11639.4]:Top: v31(x0,bitIndex5),v1196(x0),sP39_aig_name(x0) -> sP42_aig_name(x0) % 0.30/0.99 11982:4:1:[11980.0,11640.3,11638.0,11981.5]:Top: v31(x0,bitIndex8),v1196(x0),sP39_aig_name(x0) -> sP42_aig_name(x0) % 0.30/0.99 % 0.30/0.99 SZS status Unsatisfiable % 0.30/0.99 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.30/0.99 % 0.30/0.99 SPASS-SCL-FOL Statistics: % 0.30/0.99 Number of learned clauses: 0 % 0.30/0.99 Number of propagations: 0 % 0.30/0.99 Number of decisions: 0 % 0.30/0.99 Number of resolutions: 0 % 0.30/0.99 Number of condensations: 0 % 0.30/0.99 Number of sub resolutions: 195 % 0.30/0.99 % 0.30/0.99 Needed: 0:00:00.30 % 0.30/0.99 %------------------------------------------------------------------------------