%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV498-1.040 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:16:05 PM UTC 2026
% Result : Satisfiable 7.93s 1.96s
% Output : Saturation 9.79s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u870,negated_conjecture,
a_1398 != a_1438 ).
cnf(u875,hypothesis,
i1 != i2 ).
cnf(u880,hypothesis,
i1 != i3 ).
cnf(u885,hypothesis,
i1 != i4 ).
cnf(u890,hypothesis,
i1 != i5 ).
cnf(u895,hypothesis,
i1 != i6 ).
cnf(u900,hypothesis,
i1 != i7 ).
cnf(u905,hypothesis,
i1 != i8 ).
cnf(u910,hypothesis,
i1 != i9 ).
cnf(u915,hypothesis,
i1 != i10 ).
cnf(u920,hypothesis,
i1 != i11 ).
cnf(u925,hypothesis,
i1 != i12 ).
cnf(u930,hypothesis,
i1 != i13 ).
cnf(u935,hypothesis,
i1 != i14 ).
cnf(u940,hypothesis,
i1 != i15 ).
cnf(u945,hypothesis,
i1 != i16 ).
cnf(u950,hypothesis,
i1 != i17 ).
cnf(u955,hypothesis,
i1 != i18 ).
cnf(u960,hypothesis,
i1 != i19 ).
cnf(u965,hypothesis,
i1 != i20 ).
cnf(u970,hypothesis,
i1 != i21 ).
cnf(u975,hypothesis,
i1 != i22 ).
cnf(u980,hypothesis,
i1 != i23 ).
cnf(u985,hypothesis,
i1 != i24 ).
cnf(u990,hypothesis,
i1 != i25 ).
cnf(u995,hypothesis,
i1 != i26 ).
cnf(u1000,hypothesis,
i1 != i27 ).
cnf(u1005,hypothesis,
i1 != i28 ).
cnf(u1010,hypothesis,
i1 != i29 ).
cnf(u1015,hypothesis,
i1 != i30 ).
cnf(u1020,hypothesis,
i1 != i31 ).
cnf(u1025,hypothesis,
i1 != i32 ).
cnf(u1030,hypothesis,
i1 != i33 ).
cnf(u1035,hypothesis,
i1 != i34 ).
cnf(u1040,hypothesis,
i1 != i35 ).
cnf(u1045,hypothesis,
i1 != i36 ).
cnf(u1050,hypothesis,
i1 != i37 ).
cnf(u1055,hypothesis,
i1 != i38 ).
cnf(u1060,hypothesis,
i1 != i39 ).
cnf(u1065,hypothesis,
i1 != i40 ).
cnf(u1070,hypothesis,
i2 != i3 ).
cnf(u1075,hypothesis,
i2 != i4 ).
cnf(u1080,hypothesis,
i2 != i5 ).
cnf(u1085,hypothesis,
i2 != i6 ).
cnf(u1090,hypothesis,
i2 != i7 ).
cnf(u1095,hypothesis,
i2 != i8 ).
cnf(u1100,hypothesis,
i2 != i9 ).
cnf(u1105,hypothesis,
i2 != i10 ).
cnf(u1110,hypothesis,
i2 != i11 ).
cnf(u1115,hypothesis,
i2 != i12 ).
cnf(u1120,hypothesis,
i2 != i13 ).
cnf(u1125,hypothesis,
i2 != i14 ).
cnf(u1130,hypothesis,
i2 != i15 ).
cnf(u1135,hypothesis,
i2 != i16 ).
cnf(u1140,hypothesis,
i2 != i17 ).
cnf(u1145,hypothesis,
i2 != i18 ).
cnf(u1150,hypothesis,
i2 != i19 ).
cnf(u1155,hypothesis,
i2 != i20 ).
cnf(u1160,hypothesis,
i2 != i21 ).
cnf(u1165,hypothesis,
i2 != i22 ).
cnf(u1170,hypothesis,
i2 != i23 ).
cnf(u1175,hypothesis,
i2 != i24 ).
cnf(u1180,hypothesis,
i2 != i25 ).
cnf(u1185,hypothesis,
i2 != i26 ).
cnf(u1190,hypothesis,
i2 != i27 ).
cnf(u1195,hypothesis,
i2 != i28 ).
cnf(u1200,hypothesis,
i2 != i29 ).
cnf(u1205,hypothesis,
i2 != i30 ).
cnf(u1210,hypothesis,
i2 != i31 ).
cnf(u1215,hypothesis,
i2 != i32 ).
cnf(u1220,hypothesis,
i2 != i33 ).
cnf(u1225,hypothesis,
i2 != i34 ).
cnf(u1230,hypothesis,
i2 != i35 ).
cnf(u1235,hypothesis,
i2 != i36 ).
cnf(u1240,hypothesis,
i2 != i37 ).
cnf(u1245,hypothesis,
i2 != i38 ).
cnf(u1250,hypothesis,
i2 != i39 ).
cnf(u1255,hypothesis,
i2 != i40 ).
cnf(u1260,hypothesis,
i3 != i4 ).
cnf(u1265,hypothesis,
i3 != i5 ).
cnf(u1270,hypothesis,
i3 != i6 ).
cnf(u1275,hypothesis,
i3 != i7 ).
cnf(u1280,hypothesis,
i3 != i8 ).
cnf(u1285,hypothesis,
i3 != i9 ).
cnf(u1290,hypothesis,
i3 != i10 ).
cnf(u1295,hypothesis,
i3 != i11 ).
cnf(u1300,hypothesis,
i3 != i12 ).
cnf(u1305,hypothesis,
i3 != i13 ).
cnf(u1310,hypothesis,
i3 != i14 ).
cnf(u1315,hypothesis,
i3 != i15 ).
cnf(u1320,hypothesis,
i3 != i16 ).
cnf(u1325,hypothesis,
i3 != i17 ).
cnf(u1330,hypothesis,
i3 != i18 ).
cnf(u1335,hypothesis,
i3 != i19 ).
cnf(u1340,hypothesis,
i3 != i20 ).
cnf(u1345,hypothesis,
i3 != i21 ).
cnf(u1350,hypothesis,
i3 != i22 ).
cnf(u1355,hypothesis,
i3 != i23 ).
cnf(u1360,hypothesis,
i3 != i24 ).
cnf(u1365,hypothesis,
i3 != i25 ).
cnf(u1370,hypothesis,
i3 != i26 ).
cnf(u1375,hypothesis,
i3 != i27 ).
cnf(u1380,hypothesis,
i3 != i28 ).
cnf(u1385,hypothesis,
i3 != i29 ).
cnf(u1390,hypothesis,
i3 != i30 ).
cnf(u1395,hypothesis,
i3 != i31 ).
cnf(u1400,hypothesis,
i3 != i32 ).
cnf(u1405,hypothesis,
i3 != i33 ).
cnf(u1410,hypothesis,
i3 != i34 ).
cnf(u1415,hypothesis,
i3 != i35 ).
cnf(u1420,hypothesis,
i3 != i36 ).
cnf(u1425,hypothesis,
i3 != i37 ).
cnf(u1430,hypothesis,
i3 != i38 ).
cnf(u1435,hypothesis,
i3 != i39 ).
cnf(u1440,hypothesis,
i3 != i40 ).
cnf(u1445,hypothesis,
i4 != i5 ).
cnf(u1450,hypothesis,
i4 != i6 ).
cnf(u1455,hypothesis,
i4 != i7 ).
cnf(u1460,hypothesis,
i4 != i8 ).
cnf(u1465,hypothesis,
i4 != i9 ).
cnf(u1470,hypothesis,
i4 != i10 ).
cnf(u1475,hypothesis,
i4 != i11 ).
cnf(u1480,hypothesis,
i4 != i12 ).
cnf(u1485,hypothesis,
i4 != i13 ).
cnf(u1490,hypothesis,
i4 != i14 ).
cnf(u1495,hypothesis,
i4 != i15 ).
cnf(u1500,hypothesis,
i4 != i16 ).
cnf(u1505,hypothesis,
i4 != i17 ).
cnf(u1510,hypothesis,
i4 != i18 ).
cnf(u1515,hypothesis,
i4 != i19 ).
cnf(u1520,hypothesis,
i4 != i20 ).
cnf(u1525,hypothesis,
i4 != i21 ).
cnf(u1530,hypothesis,
i4 != i22 ).
cnf(u1535,hypothesis,
i4 != i23 ).
cnf(u1540,hypothesis,
i4 != i24 ).
cnf(u1545,hypothesis,
i4 != i25 ).
cnf(u1550,hypothesis,
i4 != i26 ).
cnf(u1555,hypothesis,
i4 != i27 ).
cnf(u1560,hypothesis,
i4 != i28 ).
cnf(u1565,hypothesis,
i4 != i29 ).
cnf(u1570,hypothesis,
i4 != i30 ).
cnf(u1575,hypothesis,
i4 != i31 ).
cnf(u1580,hypothesis,
i4 != i32 ).
cnf(u1585,hypothesis,
i4 != i33 ).
cnf(u1590,hypothesis,
i4 != i34 ).
cnf(u1595,hypothesis,
i4 != i35 ).
cnf(u1600,hypothesis,
i4 != i36 ).
cnf(u1605,hypothesis,
i4 != i37 ).
cnf(u1610,hypothesis,
i4 != i38 ).
cnf(u1615,hypothesis,
i4 != i39 ).
cnf(u1620,hypothesis,
i4 != i40 ).
cnf(u1625,hypothesis,
i5 != i6 ).
cnf(u1630,hypothesis,
i5 != i7 ).
cnf(u1635,hypothesis,
i5 != i8 ).
cnf(u1640,hypothesis,
i5 != i9 ).
cnf(u1645,hypothesis,
i5 != i10 ).
cnf(u1650,hypothesis,
i5 != i11 ).
cnf(u1655,hypothesis,
i5 != i12 ).
cnf(u1660,hypothesis,
i5 != i13 ).
cnf(u1665,hypothesis,
i5 != i14 ).
cnf(u1670,hypothesis,
i5 != i15 ).
cnf(u1675,hypothesis,
i5 != i16 ).
cnf(u1680,hypothesis,
i5 != i17 ).
cnf(u1685,hypothesis,
i5 != i18 ).
cnf(u1690,hypothesis,
i5 != i19 ).
cnf(u1695,hypothesis,
i5 != i20 ).
cnf(u1700,hypothesis,
i5 != i21 ).
cnf(u1705,hypothesis,
i5 != i22 ).
cnf(u1710,hypothesis,
i5 != i23 ).
cnf(u1715,hypothesis,
i5 != i24 ).
cnf(u1720,hypothesis,
i5 != i25 ).
cnf(u1725,hypothesis,
i5 != i26 ).
cnf(u1730,hypothesis,
i5 != i27 ).
cnf(u1735,hypothesis,
i5 != i28 ).
cnf(u1740,hypothesis,
i5 != i29 ).
cnf(u1745,hypothesis,
i5 != i30 ).
cnf(u1750,hypothesis,
i5 != i31 ).
cnf(u1755,hypothesis,
i5 != i32 ).
cnf(u1760,hypothesis,
i5 != i33 ).
cnf(u1765,hypothesis,
i5 != i34 ).
cnf(u1770,hypothesis,
i5 != i35 ).
cnf(u1775,hypothesis,
i5 != i36 ).
cnf(u1780,hypothesis,
i5 != i37 ).
cnf(u1785,hypothesis,
i5 != i38 ).
cnf(u1790,hypothesis,
i5 != i39 ).
cnf(u1795,hypothesis,
i5 != i40 ).
cnf(u1800,hypothesis,
i6 != i7 ).
cnf(u1805,hypothesis,
i6 != i8 ).
cnf(u1810,hypothesis,
i6 != i9 ).
cnf(u1815,hypothesis,
i6 != i10 ).
cnf(u1820,hypothesis,
i6 != i11 ).
cnf(u1825,hypothesis,
i6 != i12 ).
cnf(u1830,hypothesis,
i6 != i13 ).
cnf(u1835,hypothesis,
i6 != i14 ).
cnf(u1840,hypothesis,
i6 != i15 ).
cnf(u1845,hypothesis,
i6 != i16 ).
cnf(u1850,hypothesis,
i6 != i17 ).
cnf(u1855,hypothesis,
i6 != i18 ).
cnf(u1860,hypothesis,
i6 != i19 ).
cnf(u1865,hypothesis,
i6 != i20 ).
cnf(u1870,hypothesis,
i6 != i21 ).
cnf(u1875,hypothesis,
i6 != i22 ).
cnf(u1880,hypothesis,
i6 != i23 ).
cnf(u1885,hypothesis,
i6 != i24 ).
cnf(u1890,hypothesis,
i6 != i25 ).
cnf(u1895,hypothesis,
i6 != i26 ).
cnf(u1900,hypothesis,
i6 != i27 ).
cnf(u1905,hypothesis,
i6 != i28 ).
cnf(u1910,hypothesis,
i6 != i29 ).
cnf(u1915,hypothesis,
i6 != i30 ).
cnf(u1920,hypothesis,
i6 != i31 ).
cnf(u1925,hypothesis,
i6 != i32 ).
cnf(u1930,hypothesis,
i6 != i33 ).
cnf(u1935,hypothesis,
i6 != i34 ).
cnf(u1940,hypothesis,
i6 != i35 ).
cnf(u1945,hypothesis,
i6 != i36 ).
cnf(u1950,hypothesis,
i6 != i37 ).
cnf(u1955,hypothesis,
i6 != i38 ).
cnf(u1960,hypothesis,
i6 != i39 ).
cnf(u1965,hypothesis,
i6 != i40 ).
cnf(u1970,hypothesis,
i7 != i8 ).
cnf(u1975,hypothesis,
i7 != i9 ).
cnf(u1980,hypothesis,
i7 != i10 ).
cnf(u1985,hypothesis,
i7 != i11 ).
cnf(u1990,hypothesis,
i7 != i12 ).
cnf(u1995,hypothesis,
i7 != i13 ).
cnf(u2000,hypothesis,
i7 != i14 ).
cnf(u2005,hypothesis,
i7 != i15 ).
cnf(u2010,hypothesis,
i7 != i16 ).
cnf(u2015,hypothesis,
i7 != i17 ).
cnf(u2020,hypothesis,
i7 != i18 ).
cnf(u2025,hypothesis,
i7 != i19 ).
cnf(u2030,hypothesis,
i7 != i20 ).
cnf(u2035,hypothesis,
i7 != i21 ).
cnf(u2040,hypothesis,
i7 != i22 ).
cnf(u2045,hypothesis,
i7 != i23 ).
cnf(u2050,hypothesis,
i7 != i24 ).
cnf(u2055,hypothesis,
i7 != i25 ).
cnf(u2060,hypothesis,
i7 != i26 ).
cnf(u2065,hypothesis,
i7 != i27 ).
cnf(u2070,hypothesis,
i7 != i28 ).
cnf(u2075,hypothesis,
i7 != i29 ).
cnf(u2080,hypothesis,
i7 != i30 ).
cnf(u2085,hypothesis,
i7 != i31 ).
cnf(u2090,hypothesis,
i7 != i32 ).
cnf(u2095,hypothesis,
i7 != i33 ).
cnf(u2100,hypothesis,
i7 != i34 ).
cnf(u2105,hypothesis,
i7 != i35 ).
cnf(u2110,hypothesis,
i7 != i36 ).
cnf(u2115,hypothesis,
i7 != i37 ).
cnf(u2120,hypothesis,
i7 != i38 ).
cnf(u2125,hypothesis,
i7 != i39 ).
cnf(u2130,hypothesis,
i7 != i40 ).
cnf(u2135,hypothesis,
i8 != i9 ).
cnf(u2140,hypothesis,
i8 != i10 ).
cnf(u2145,hypothesis,
i8 != i11 ).
cnf(u2150,hypothesis,
i8 != i12 ).
cnf(u2155,hypothesis,
i8 != i13 ).
cnf(u2160,hypothesis,
i8 != i14 ).
cnf(u2165,hypothesis,
i8 != i15 ).
cnf(u2170,hypothesis,
i8 != i16 ).
cnf(u2175,hypothesis,
i8 != i17 ).
cnf(u2180,hypothesis,
i8 != i18 ).
cnf(u2185,hypothesis,
i8 != i19 ).
cnf(u2190,hypothesis,
i8 != i20 ).
cnf(u2195,hypothesis,
i8 != i21 ).
cnf(u2200,hypothesis,
i8 != i22 ).
cnf(u2205,hypothesis,
i8 != i23 ).
cnf(u2210,hypothesis,
i8 != i24 ).
cnf(u2215,hypothesis,
i8 != i25 ).
cnf(u2220,hypothesis,
i8 != i26 ).
cnf(u2225,hypothesis,
i8 != i27 ).
cnf(u2230,hypothesis,
i8 != i28 ).
cnf(u2235,hypothesis,
i8 != i29 ).
cnf(u2240,hypothesis,
i8 != i30 ).
cnf(u2245,hypothesis,
i8 != i31 ).
cnf(u2250,hypothesis,
i8 != i32 ).
cnf(u2255,hypothesis,
i8 != i33 ).
cnf(u2260,hypothesis,
i8 != i34 ).
cnf(u2265,hypothesis,
i8 != i35 ).
cnf(u2270,hypothesis,
i8 != i36 ).
cnf(u2275,hypothesis,
i8 != i37 ).
cnf(u2280,hypothesis,
i8 != i38 ).
cnf(u2285,hypothesis,
i8 != i39 ).
cnf(u2290,hypothesis,
i8 != i40 ).
cnf(u2295,hypothesis,
i9 != i10 ).
cnf(u2300,hypothesis,
i9 != i11 ).
cnf(u2305,hypothesis,
i9 != i12 ).
cnf(u2310,hypothesis,
i9 != i13 ).
cnf(u2315,hypothesis,
i9 != i14 ).
cnf(u2320,hypothesis,
i9 != i15 ).
cnf(u2325,hypothesis,
i9 != i16 ).
cnf(u2330,hypothesis,
i9 != i17 ).
cnf(u2335,hypothesis,
i9 != i18 ).
cnf(u2340,hypothesis,
i9 != i19 ).
cnf(u2345,hypothesis,
i9 != i20 ).
cnf(u2350,hypothesis,
i9 != i21 ).
cnf(u2355,hypothesis,
i9 != i22 ).
cnf(u2360,hypothesis,
i9 != i23 ).
cnf(u2365,hypothesis,
i9 != i24 ).
cnf(u2370,hypothesis,
i9 != i25 ).
cnf(u2375,hypothesis,
i9 != i26 ).
cnf(u2380,hypothesis,
i9 != i27 ).
cnf(u2385,hypothesis,
i9 != i28 ).
cnf(u2390,hypothesis,
i9 != i29 ).
cnf(u2395,hypothesis,
i9 != i30 ).
cnf(u2400,hypothesis,
i9 != i31 ).
cnf(u2405,hypothesis,
i9 != i32 ).
cnf(u2410,hypothesis,
i9 != i33 ).
cnf(u2415,hypothesis,
i9 != i34 ).
cnf(u2420,hypothesis,
i9 != i35 ).
cnf(u2425,hypothesis,
i9 != i36 ).
cnf(u2430,hypothesis,
i9 != i37 ).
cnf(u2435,hypothesis,
i9 != i38 ).
cnf(u2440,hypothesis,
i9 != i39 ).
cnf(u2445,hypothesis,
i9 != i40 ).
cnf(u2450,hypothesis,
i10 != i11 ).
cnf(u2455,hypothesis,
i10 != i12 ).
cnf(u2460,hypothesis,
i10 != i13 ).
cnf(u2465,hypothesis,
i10 != i14 ).
cnf(u2470,hypothesis,
i10 != i15 ).
cnf(u2475,hypothesis,
i10 != i16 ).
cnf(u2480,hypothesis,
i10 != i17 ).
cnf(u2485,hypothesis,
i10 != i18 ).
cnf(u2490,hypothesis,
i10 != i19 ).
cnf(u2495,hypothesis,
i10 != i20 ).
cnf(u2500,hypothesis,
i10 != i21 ).
cnf(u2505,hypothesis,
i10 != i22 ).
cnf(u2510,hypothesis,
i10 != i23 ).
cnf(u2515,hypothesis,
i10 != i24 ).
cnf(u2520,hypothesis,
i10 != i25 ).
cnf(u2525,hypothesis,
i10 != i26 ).
cnf(u2530,hypothesis,
i10 != i27 ).
cnf(u2535,hypothesis,
i10 != i28 ).
cnf(u2540,hypothesis,
i10 != i29 ).
cnf(u2545,hypothesis,
i10 != i30 ).
cnf(u2550,hypothesis,
i10 != i31 ).
cnf(u2555,hypothesis,
i10 != i32 ).
cnf(u2560,hypothesis,
i10 != i33 ).
cnf(u2565,hypothesis,
i10 != i34 ).
cnf(u2570,hypothesis,
i10 != i35 ).
cnf(u2575,hypothesis,
i10 != i36 ).
cnf(u2580,hypothesis,
i10 != i37 ).
cnf(u2585,hypothesis,
i10 != i38 ).
cnf(u2590,hypothesis,
i10 != i39 ).
cnf(u2595,hypothesis,
i10 != i40 ).
cnf(u2600,hypothesis,
i11 != i12 ).
cnf(u2605,hypothesis,
i11 != i13 ).
cnf(u2610,hypothesis,
i11 != i14 ).
cnf(u2615,hypothesis,
i11 != i15 ).
cnf(u2620,hypothesis,
i11 != i16 ).
cnf(u2625,hypothesis,
i11 != i17 ).
cnf(u2630,hypothesis,
i11 != i18 ).
cnf(u2635,hypothesis,
i11 != i19 ).
cnf(u2640,hypothesis,
i11 != i20 ).
cnf(u2645,hypothesis,
i11 != i21 ).
cnf(u2650,hypothesis,
i11 != i22 ).
cnf(u2655,hypothesis,
i11 != i23 ).
cnf(u2660,hypothesis,
i11 != i24 ).
cnf(u2665,hypothesis,
i11 != i25 ).
cnf(u2670,hypothesis,
i11 != i26 ).
cnf(u2675,hypothesis,
i11 != i27 ).
cnf(u2680,hypothesis,
i11 != i28 ).
cnf(u2685,hypothesis,
i11 != i29 ).
cnf(u2690,hypothesis,
i11 != i30 ).
cnf(u2695,hypothesis,
i11 != i31 ).
cnf(u2700,hypothesis,
i11 != i32 ).
cnf(u2705,hypothesis,
i11 != i33 ).
cnf(u2710,hypothesis,
i11 != i34 ).
cnf(u2715,hypothesis,
i11 != i35 ).
cnf(u2720,hypothesis,
i11 != i36 ).
cnf(u2725,hypothesis,
i11 != i37 ).
cnf(u2730,hypothesis,
i11 != i38 ).
cnf(u2735,hypothesis,
i11 != i39 ).
cnf(u2740,hypothesis,
i11 != i40 ).
cnf(u2745,hypothesis,
i12 != i13 ).
cnf(u2750,hypothesis,
i12 != i14 ).
cnf(u2755,hypothesis,
i12 != i15 ).
cnf(u2760,hypothesis,
i12 != i16 ).
cnf(u2765,hypothesis,
i12 != i17 ).
cnf(u2770,hypothesis,
i12 != i18 ).
cnf(u2775,hypothesis,
i12 != i19 ).
cnf(u2780,hypothesis,
i12 != i20 ).
cnf(u2785,hypothesis,
i12 != i21 ).
cnf(u2790,hypothesis,
i12 != i22 ).
cnf(u2795,hypothesis,
i12 != i23 ).
cnf(u2800,hypothesis,
i12 != i24 ).
cnf(u2805,hypothesis,
i12 != i25 ).
cnf(u2810,hypothesis,
i12 != i26 ).
cnf(u2815,hypothesis,
i12 != i27 ).
cnf(u2820,hypothesis,
i12 != i28 ).
cnf(u2825,hypothesis,
i12 != i29 ).
cnf(u2830,hypothesis,
i12 != i30 ).
cnf(u2835,hypothesis,
i12 != i31 ).
cnf(u2840,hypothesis,
i12 != i32 ).
cnf(u2845,hypothesis,
i12 != i33 ).
cnf(u2850,hypothesis,
i12 != i34 ).
cnf(u2855,hypothesis,
i12 != i35 ).
cnf(u2860,hypothesis,
i12 != i36 ).
cnf(u2865,hypothesis,
i12 != i37 ).
cnf(u2870,hypothesis,
i12 != i38 ).
cnf(u2875,hypothesis,
i12 != i39 ).
cnf(u2880,hypothesis,
i12 != i40 ).
cnf(u2885,hypothesis,
i13 != i14 ).
cnf(u2890,hypothesis,
i13 != i15 ).
cnf(u2895,hypothesis,
i13 != i16 ).
cnf(u2900,hypothesis,
i13 != i17 ).
cnf(u2905,hypothesis,
i13 != i18 ).
cnf(u2910,hypothesis,
i13 != i19 ).
cnf(u2915,hypothesis,
i13 != i20 ).
cnf(u2920,hypothesis,
i13 != i21 ).
cnf(u2925,hypothesis,
i13 != i22 ).
cnf(u2930,hypothesis,
i13 != i23 ).
cnf(u2935,hypothesis,
i13 != i24 ).
cnf(u2940,hypothesis,
i13 != i25 ).
cnf(u2945,hypothesis,
i13 != i26 ).
cnf(u2950,hypothesis,
i13 != i27 ).
cnf(u2955,hypothesis,
i13 != i28 ).
cnf(u2960,hypothesis,
i13 != i29 ).
cnf(u2965,hypothesis,
i13 != i30 ).
cnf(u2970,hypothesis,
i13 != i31 ).
cnf(u2975,hypothesis,
i13 != i32 ).
cnf(u2980,hypothesis,
i13 != i33 ).
cnf(u2985,hypothesis,
i13 != i34 ).
cnf(u2990,hypothesis,
i13 != i35 ).
cnf(u2995,hypothesis,
i13 != i36 ).
cnf(u3000,hypothesis,
i13 != i37 ).
cnf(u3005,hypothesis,
i13 != i38 ).
cnf(u3010,hypothesis,
i13 != i39 ).
cnf(u3015,hypothesis,
i13 != i40 ).
cnf(u3020,hypothesis,
i14 != i15 ).
cnf(u3025,hypothesis,
i14 != i16 ).
cnf(u3030,hypothesis,
i14 != i17 ).
cnf(u3035,hypothesis,
i14 != i18 ).
cnf(u3040,hypothesis,
i14 != i19 ).
cnf(u3045,hypothesis,
i14 != i20 ).
cnf(u3050,hypothesis,
i14 != i21 ).
cnf(u3055,hypothesis,
i14 != i22 ).
cnf(u3060,hypothesis,
i14 != i23 ).
cnf(u3065,hypothesis,
i14 != i24 ).
cnf(u3070,hypothesis,
i14 != i25 ).
cnf(u3075,hypothesis,
i14 != i26 ).
cnf(u3080,hypothesis,
i14 != i27 ).
cnf(u3085,hypothesis,
i14 != i28 ).
cnf(u3090,hypothesis,
i14 != i29 ).
cnf(u3095,hypothesis,
i14 != i30 ).
cnf(u3100,hypothesis,
i14 != i31 ).
cnf(u3105,hypothesis,
i14 != i32 ).
cnf(u3110,hypothesis,
i14 != i33 ).
cnf(u3115,hypothesis,
i14 != i34 ).
cnf(u3120,hypothesis,
i14 != i35 ).
cnf(u3125,hypothesis,
i14 != i36 ).
cnf(u3130,hypothesis,
i14 != i37 ).
cnf(u3135,hypothesis,
i14 != i38 ).
cnf(u3140,hypothesis,
i14 != i39 ).
cnf(u3145,hypothesis,
i14 != i40 ).
cnf(u3150,hypothesis,
i15 != i16 ).
cnf(u3155,hypothesis,
i15 != i17 ).
cnf(u3160,hypothesis,
i15 != i18 ).
cnf(u3165,hypothesis,
i15 != i19 ).
cnf(u3170,hypothesis,
i15 != i20 ).
cnf(u3175,hypothesis,
i15 != i21 ).
cnf(u3180,hypothesis,
i15 != i22 ).
cnf(u3185,hypothesis,
i15 != i23 ).
cnf(u3190,hypothesis,
i15 != i24 ).
cnf(u3195,hypothesis,
i15 != i25 ).
cnf(u3200,hypothesis,
i15 != i26 ).
cnf(u3205,hypothesis,
i15 != i27 ).
cnf(u3210,hypothesis,
i15 != i28 ).
cnf(u3215,hypothesis,
i15 != i29 ).
cnf(u3220,hypothesis,
i15 != i30 ).
cnf(u3225,hypothesis,
i15 != i31 ).
cnf(u3230,hypothesis,
i15 != i32 ).
cnf(u3235,hypothesis,
i15 != i33 ).
cnf(u3240,hypothesis,
i15 != i34 ).
cnf(u3245,hypothesis,
i15 != i35 ).
cnf(u3250,hypothesis,
i15 != i36 ).
cnf(u3255,hypothesis,
i15 != i37 ).
cnf(u3260,hypothesis,
i15 != i38 ).
cnf(u3265,hypothesis,
i15 != i39 ).
cnf(u3270,hypothesis,
i15 != i40 ).
cnf(u3275,hypothesis,
i16 != i17 ).
cnf(u3280,hypothesis,
i16 != i18 ).
cnf(u3285,hypothesis,
i16 != i19 ).
cnf(u3290,hypothesis,
i16 != i20 ).
cnf(u3295,hypothesis,
i16 != i21 ).
cnf(u3300,hypothesis,
i16 != i22 ).
cnf(u3305,hypothesis,
i16 != i23 ).
cnf(u3310,hypothesis,
i16 != i24 ).
cnf(u3315,hypothesis,
i16 != i25 ).
cnf(u3320,hypothesis,
i16 != i26 ).
cnf(u3325,hypothesis,
i16 != i27 ).
cnf(u3330,hypothesis,
i16 != i28 ).
cnf(u3335,hypothesis,
i16 != i29 ).
cnf(u3340,hypothesis,
i16 != i30 ).
cnf(u3345,hypothesis,
i16 != i31 ).
cnf(u3350,hypothesis,
i16 != i32 ).
cnf(u3355,hypothesis,
i16 != i33 ).
cnf(u3360,hypothesis,
i16 != i34 ).
cnf(u3365,hypothesis,
i16 != i35 ).
cnf(u3370,hypothesis,
i16 != i36 ).
cnf(u3375,hypothesis,
i16 != i37 ).
cnf(u3380,hypothesis,
i16 != i38 ).
cnf(u3385,hypothesis,
i16 != i39 ).
cnf(u3390,hypothesis,
i16 != i40 ).
cnf(u3395,hypothesis,
i17 != i18 ).
cnf(u3400,hypothesis,
i17 != i19 ).
cnf(u3405,hypothesis,
i17 != i20 ).
cnf(u3410,hypothesis,
i17 != i21 ).
cnf(u3415,hypothesis,
i17 != i22 ).
cnf(u3420,hypothesis,
i17 != i23 ).
cnf(u3425,hypothesis,
i17 != i24 ).
cnf(u3430,hypothesis,
i17 != i25 ).
cnf(u3435,hypothesis,
i17 != i26 ).
cnf(u3440,hypothesis,
i17 != i27 ).
cnf(u3445,hypothesis,
i17 != i28 ).
cnf(u3450,hypothesis,
i17 != i29 ).
cnf(u3455,hypothesis,
i17 != i30 ).
cnf(u3460,hypothesis,
i17 != i31 ).
cnf(u3465,hypothesis,
i17 != i32 ).
cnf(u3470,hypothesis,
i17 != i33 ).
cnf(u3475,hypothesis,
i17 != i34 ).
cnf(u3480,hypothesis,
i17 != i35 ).
cnf(u3485,hypothesis,
i17 != i36 ).
cnf(u3490,hypothesis,
i17 != i37 ).
cnf(u3495,hypothesis,
i17 != i38 ).
cnf(u3500,hypothesis,
i17 != i39 ).
cnf(u3505,hypothesis,
i17 != i40 ).
cnf(u3510,hypothesis,
i18 != i19 ).
cnf(u3515,hypothesis,
i18 != i20 ).
cnf(u3520,hypothesis,
i18 != i21 ).
cnf(u3525,hypothesis,
i18 != i22 ).
cnf(u3530,hypothesis,
i18 != i23 ).
cnf(u3535,hypothesis,
i18 != i24 ).
cnf(u3540,hypothesis,
i18 != i25 ).
cnf(u3545,hypothesis,
i18 != i26 ).
cnf(u3550,hypothesis,
i18 != i27 ).
cnf(u3555,hypothesis,
i18 != i28 ).
cnf(u3560,hypothesis,
i18 != i29 ).
cnf(u3565,hypothesis,
i18 != i30 ).
cnf(u3570,hypothesis,
i18 != i31 ).
cnf(u3575,hypothesis,
i18 != i32 ).
cnf(u3580,hypothesis,
i18 != i33 ).
cnf(u3585,hypothesis,
i18 != i34 ).
cnf(u3590,hypothesis,
i18 != i35 ).
cnf(u3595,hypothesis,
i18 != i36 ).
cnf(u3600,hypothesis,
i18 != i37 ).
cnf(u3605,hypothesis,
i18 != i38 ).
cnf(u3610,hypothesis,
i18 != i39 ).
cnf(u3615,hypothesis,
i18 != i40 ).
cnf(u3620,hypothesis,
i19 != i20 ).
cnf(u3625,hypothesis,
i19 != i21 ).
cnf(u3630,hypothesis,
i19 != i22 ).
cnf(u3635,hypothesis,
i19 != i23 ).
cnf(u3640,hypothesis,
i19 != i24 ).
cnf(u3645,hypothesis,
i19 != i25 ).
cnf(u3650,hypothesis,
i19 != i26 ).
cnf(u3655,hypothesis,
i19 != i27 ).
cnf(u3660,hypothesis,
i19 != i28 ).
cnf(u3665,hypothesis,
i19 != i29 ).
cnf(u3670,hypothesis,
i19 != i30 ).
cnf(u3675,hypothesis,
i19 != i31 ).
cnf(u3680,hypothesis,
i19 != i32 ).
cnf(u3685,hypothesis,
i19 != i33 ).
cnf(u3690,hypothesis,
i19 != i34 ).
cnf(u3695,hypothesis,
i19 != i35 ).
cnf(u3700,hypothesis,
i19 != i36 ).
cnf(u3705,hypothesis,
i19 != i37 ).
cnf(u3710,hypothesis,
i19 != i38 ).
cnf(u3715,hypothesis,
i19 != i39 ).
cnf(u3720,hypothesis,
i19 != i40 ).
cnf(u3725,hypothesis,
i20 != i21 ).
cnf(u3730,hypothesis,
i20 != i22 ).
cnf(u3735,hypothesis,
i20 != i23 ).
cnf(u3740,hypothesis,
i20 != i24 ).
cnf(u3745,hypothesis,
i20 != i25 ).
cnf(u3750,hypothesis,
i20 != i26 ).
cnf(u3755,hypothesis,
i20 != i27 ).
cnf(u3760,hypothesis,
i20 != i28 ).
cnf(u3765,hypothesis,
i20 != i29 ).
cnf(u3770,hypothesis,
i20 != i30 ).
cnf(u3775,hypothesis,
i20 != i31 ).
cnf(u3780,hypothesis,
i20 != i32 ).
cnf(u3785,hypothesis,
i20 != i33 ).
cnf(u3790,hypothesis,
i20 != i34 ).
cnf(u3795,hypothesis,
i20 != i35 ).
cnf(u3800,hypothesis,
i20 != i36 ).
cnf(u3805,hypothesis,
i20 != i37 ).
cnf(u3810,hypothesis,
i20 != i38 ).
cnf(u3815,hypothesis,
i20 != i39 ).
cnf(u3820,hypothesis,
i20 != i40 ).
cnf(u3825,hypothesis,
i21 != i22 ).
cnf(u3830,hypothesis,
i21 != i23 ).
cnf(u3835,hypothesis,
i21 != i24 ).
cnf(u3840,hypothesis,
i21 != i25 ).
cnf(u3845,hypothesis,
i21 != i26 ).
cnf(u3850,hypothesis,
i21 != i27 ).
cnf(u3855,hypothesis,
i21 != i28 ).
cnf(u3860,hypothesis,
i21 != i29 ).
cnf(u3865,hypothesis,
i21 != i30 ).
cnf(u3870,hypothesis,
i21 != i31 ).
cnf(u3875,hypothesis,
i21 != i32 ).
cnf(u3880,hypothesis,
i21 != i33 ).
cnf(u3885,hypothesis,
i21 != i34 ).
cnf(u3890,hypothesis,
i21 != i35 ).
cnf(u3895,hypothesis,
i21 != i36 ).
cnf(u3900,hypothesis,
i21 != i37 ).
cnf(u3905,hypothesis,
i21 != i38 ).
cnf(u3910,hypothesis,
i21 != i39 ).
cnf(u3915,hypothesis,
i21 != i40 ).
cnf(u3920,hypothesis,
i22 != i23 ).
cnf(u3925,hypothesis,
i22 != i24 ).
cnf(u3930,hypothesis,
i22 != i25 ).
cnf(u3935,hypothesis,
i22 != i26 ).
cnf(u3940,hypothesis,
i22 != i27 ).
cnf(u3945,hypothesis,
i22 != i28 ).
cnf(u3950,hypothesis,
i22 != i29 ).
cnf(u3955,hypothesis,
i22 != i30 ).
cnf(u3960,hypothesis,
i22 != i31 ).
cnf(u3965,hypothesis,
i22 != i32 ).
cnf(u3970,hypothesis,
i22 != i33 ).
cnf(u3975,hypothesis,
i22 != i34 ).
cnf(u3980,hypothesis,
i22 != i35 ).
cnf(u3985,hypothesis,
i22 != i36 ).
cnf(u3990,hypothesis,
i22 != i37 ).
cnf(u3995,hypothesis,
i22 != i38 ).
cnf(u4000,hypothesis,
i22 != i39 ).
cnf(u4005,hypothesis,
i22 != i40 ).
cnf(u4010,hypothesis,
i23 != i24 ).
cnf(u4015,hypothesis,
i23 != i25 ).
cnf(u4020,hypothesis,
i23 != i26 ).
cnf(u4025,hypothesis,
i23 != i27 ).
cnf(u4030,hypothesis,
i23 != i28 ).
cnf(u4035,hypothesis,
i23 != i29 ).
cnf(u4040,hypothesis,
i23 != i30 ).
cnf(u4045,hypothesis,
i23 != i31 ).
cnf(u4050,hypothesis,
i23 != i32 ).
cnf(u4055,hypothesis,
i23 != i33 ).
cnf(u4060,hypothesis,
i23 != i34 ).
cnf(u4065,hypothesis,
i23 != i35 ).
cnf(u4070,hypothesis,
i23 != i36 ).
cnf(u4075,hypothesis,
i23 != i37 ).
cnf(u4080,hypothesis,
i23 != i38 ).
cnf(u4085,hypothesis,
i23 != i39 ).
cnf(u4090,hypothesis,
i23 != i40 ).
cnf(u4095,hypothesis,
i24 != i25 ).
cnf(u4100,hypothesis,
i24 != i26 ).
cnf(u4105,hypothesis,
i24 != i27 ).
cnf(u4110,hypothesis,
i24 != i28 ).
cnf(u4115,hypothesis,
i24 != i29 ).
cnf(u4120,hypothesis,
i24 != i30 ).
cnf(u4125,hypothesis,
i24 != i31 ).
cnf(u4130,hypothesis,
i24 != i32 ).
cnf(u4135,hypothesis,
i24 != i33 ).
cnf(u4140,hypothesis,
i24 != i34 ).
cnf(u4145,hypothesis,
i24 != i35 ).
cnf(u4150,hypothesis,
i24 != i36 ).
cnf(u4155,hypothesis,
i24 != i37 ).
cnf(u4160,hypothesis,
i24 != i38 ).
cnf(u4165,hypothesis,
i24 != i39 ).
cnf(u4170,hypothesis,
i24 != i40 ).
cnf(u4175,hypothesis,
i25 != i26 ).
cnf(u4180,hypothesis,
i25 != i27 ).
cnf(u4185,hypothesis,
i25 != i28 ).
cnf(u4190,hypothesis,
i25 != i29 ).
cnf(u4195,hypothesis,
i25 != i30 ).
cnf(u4200,hypothesis,
i25 != i31 ).
cnf(u4205,hypothesis,
i25 != i32 ).
cnf(u4210,hypothesis,
i25 != i33 ).
cnf(u4215,hypothesis,
i25 != i34 ).
cnf(u4220,hypothesis,
i25 != i35 ).
cnf(u4225,hypothesis,
i25 != i36 ).
cnf(u4230,hypothesis,
i25 != i37 ).
cnf(u4235,hypothesis,
i25 != i38 ).
cnf(u4240,hypothesis,
i25 != i39 ).
cnf(u4245,hypothesis,
i25 != i40 ).
cnf(u4250,hypothesis,
i26 != i27 ).
cnf(u4255,hypothesis,
i26 != i28 ).
cnf(u4260,hypothesis,
i26 != i29 ).
cnf(u4265,hypothesis,
i26 != i30 ).
cnf(u4270,hypothesis,
i26 != i31 ).
cnf(u4275,hypothesis,
i26 != i32 ).
cnf(u4280,hypothesis,
i26 != i33 ).
cnf(u4285,hypothesis,
i26 != i34 ).
cnf(u4290,hypothesis,
i26 != i35 ).
cnf(u4295,hypothesis,
i26 != i36 ).
cnf(u4300,hypothesis,
i26 != i37 ).
cnf(u4305,hypothesis,
i26 != i38 ).
cnf(u4310,hypothesis,
i26 != i39 ).
cnf(u4315,hypothesis,
i26 != i40 ).
cnf(u4320,hypothesis,
i27 != i28 ).
cnf(u4325,hypothesis,
i27 != i29 ).
cnf(u4330,hypothesis,
i27 != i30 ).
cnf(u4335,hypothesis,
i27 != i31 ).
cnf(u4340,hypothesis,
i27 != i32 ).
cnf(u4345,hypothesis,
i27 != i33 ).
cnf(u4350,hypothesis,
i27 != i34 ).
cnf(u4355,hypothesis,
i27 != i35 ).
cnf(u4360,hypothesis,
i27 != i36 ).
cnf(u4365,hypothesis,
i27 != i37 ).
cnf(u4370,hypothesis,
i27 != i38 ).
cnf(u4375,hypothesis,
i27 != i39 ).
cnf(u4380,hypothesis,
i27 != i40 ).
cnf(u4385,hypothesis,
i28 != i29 ).
cnf(u4390,hypothesis,
i28 != i30 ).
cnf(u4395,hypothesis,
i28 != i31 ).
cnf(u4400,hypothesis,
i28 != i32 ).
cnf(u4405,hypothesis,
i28 != i33 ).
cnf(u4410,hypothesis,
i28 != i34 ).
cnf(u4415,hypothesis,
i28 != i35 ).
cnf(u4420,hypothesis,
i28 != i36 ).
cnf(u4425,hypothesis,
i28 != i37 ).
cnf(u4430,hypothesis,
i28 != i38 ).
cnf(u4435,hypothesis,
i28 != i39 ).
cnf(u4440,hypothesis,
i28 != i40 ).
cnf(u4445,hypothesis,
i29 != i30 ).
cnf(u4450,hypothesis,
i29 != i31 ).
cnf(u4455,hypothesis,
i29 != i32 ).
cnf(u4460,hypothesis,
i29 != i33 ).
cnf(u4465,hypothesis,
i29 != i34 ).
cnf(u4470,hypothesis,
i29 != i35 ).
cnf(u4475,hypothesis,
i29 != i36 ).
cnf(u4480,hypothesis,
i29 != i37 ).
cnf(u4485,hypothesis,
i29 != i38 ).
cnf(u4490,hypothesis,
i29 != i39 ).
cnf(u4495,hypothesis,
i29 != i40 ).
cnf(u4500,hypothesis,
i30 != i31 ).
cnf(u4505,hypothesis,
i30 != i32 ).
cnf(u4510,hypothesis,
i30 != i33 ).
cnf(u4515,hypothesis,
i30 != i34 ).
cnf(u4520,hypothesis,
i30 != i35 ).
cnf(u4525,hypothesis,
i30 != i36 ).
cnf(u4530,hypothesis,
i30 != i37 ).
cnf(u4535,hypothesis,
i30 != i38 ).
cnf(u4540,hypothesis,
i30 != i39 ).
cnf(u4545,hypothesis,
i30 != i40 ).
cnf(u4550,hypothesis,
i31 != i32 ).
cnf(u4555,hypothesis,
i31 != i33 ).
cnf(u4560,hypothesis,
i31 != i34 ).
cnf(u4565,hypothesis,
i31 != i35 ).
cnf(u4570,hypothesis,
i31 != i36 ).
cnf(u4575,hypothesis,
i31 != i37 ).
cnf(u4580,hypothesis,
i31 != i38 ).
cnf(u4585,hypothesis,
i31 != i39 ).
cnf(u4590,hypothesis,
i31 != i40 ).
cnf(u4595,hypothesis,
i32 != i33 ).
cnf(u4600,hypothesis,
i32 != i34 ).
cnf(u4605,hypothesis,
i32 != i35 ).
cnf(u4610,hypothesis,
i32 != i36 ).
cnf(u4615,hypothesis,
i32 != i37 ).
cnf(u4620,hypothesis,
i32 != i38 ).
cnf(u4625,hypothesis,
i32 != i39 ).
cnf(u4630,hypothesis,
i32 != i40 ).
cnf(u4635,hypothesis,
i33 != i34 ).
cnf(u4640,hypothesis,
i33 != i35 ).
cnf(u4645,hypothesis,
i33 != i36 ).
cnf(u4650,hypothesis,
i33 != i37 ).
cnf(u4655,hypothesis,
i33 != i38 ).
cnf(u4660,hypothesis,
i33 != i39 ).
cnf(u4665,hypothesis,
i33 != i40 ).
cnf(u4670,hypothesis,
i34 != i35 ).
cnf(u4675,hypothesis,
i34 != i36 ).
cnf(u4680,hypothesis,
i34 != i37 ).
cnf(u4685,hypothesis,
i34 != i38 ).
cnf(u4690,hypothesis,
i34 != i39 ).
cnf(u4695,hypothesis,
i34 != i40 ).
cnf(u4700,hypothesis,
i35 != i36 ).
cnf(u4705,hypothesis,
i35 != i37 ).
cnf(u4710,hypothesis,
i35 != i38 ).
cnf(u4715,hypothesis,
i35 != i39 ).
cnf(u4720,hypothesis,
i35 != i40 ).
cnf(u4725,hypothesis,
i36 != i37 ).
cnf(u4730,hypothesis,
i36 != i38 ).
cnf(u4735,hypothesis,
i36 != i39 ).
cnf(u4740,hypothesis,
i36 != i40 ).
cnf(u4745,hypothesis,
i37 != i38 ).
cnf(u4750,hypothesis,
i37 != i39 ).
cnf(u4755,hypothesis,
i37 != i40 ).
cnf(u4760,hypothesis,
i38 != i39 ).
cnf(u4765,hypothesis,
i38 != i40 ).
cnf(u4770,hypothesis,
i39 != i40 ).
cnf(u4775,hypothesis,
a_1438 = store(a_1437,i19,e19) ).
cnf(u4780,hypothesis,
a_1437 = store(a_1436,i29,e29) ).
cnf(u4785,hypothesis,
a_1436 = store(a_1435,i28,e28) ).
cnf(u4790,hypothesis,
a_1435 = store(a_1434,i34,e34) ).
cnf(u4795,hypothesis,
a_1434 = store(a_1433,i15,e15) ).
cnf(u4800,hypothesis,
a_1433 = store(a_1432,i30,e30) ).
cnf(u4805,hypothesis,
a_1432 = store(a_1431,i4,e4) ).
cnf(u4810,hypothesis,
a_1431 = store(a_1430,i5,e5) ).
cnf(u4815,hypothesis,
a_1430 = store(a_1429,i3,e3) ).
cnf(u4820,hypothesis,
a_1429 = store(a_1428,i9,e9) ).
cnf(u4825,hypothesis,
a_1428 = store(a_1427,i1,e1) ).
cnf(u4830,hypothesis,
a_1427 = store(a_1426,i39,e39) ).
cnf(u4835,hypothesis,
a_1426 = store(a_1425,i38,e38) ).
cnf(u4840,negated_conjecture,
a_1425 = sF0 ).
cnf(u4845,hypothesis,
a_1424 = store(a_1423,i2,e2) ).
cnf(u4850,hypothesis,
a_1423 = store(a_1422,i33,e33) ).
cnf(u4855,hypothesis,
a_1422 = store(a_1421,i8,e8) ).
cnf(u4860,hypothesis,
a_1421 = store(a_1420,i22,e22) ).
cnf(u4865,hypothesis,
a_1420 = store(a_1419,i10,e10) ).
cnf(u4870,hypothesis,
a_1419 = store(a_1418,i27,e27) ).
cnf(u4875,hypothesis,
a_1418 = store(a_1417,i21,e21) ).
cnf(u4880,hypothesis,
a_1417 = store(a_1416,i26,e26) ).
cnf(u4885,hypothesis,
a_1416 = store(a_1415,i23,e23) ).
cnf(u4890,hypothesis,
a_1415 = store(a_1414,i35,e35) ).
cnf(u4895,hypothesis,
a_1414 = store(a_1413,i20,e20) ).
cnf(u4900,hypothesis,
a_1413 = store(a_1412,i36,e36) ).
cnf(u4905,hypothesis,
a_1412 = store(a_1411,i12,e12) ).
cnf(u4910,hypothesis,
a_1411 = store(a_1410,i13,e13) ).
cnf(u4915,hypothesis,
a_1410 = store(a_1409,i31,e31) ).
cnf(u4920,hypothesis,
a_1409 = store(a_1408,i37,e37) ).
cnf(u4925,hypothesis,
a_1408 = store(a_1407,i18,e18) ).
cnf(u4930,hypothesis,
a_1407 = store(a_1406,i6,e6) ).
cnf(u4935,hypothesis,
a_1406 = store(a_1405,i32,e32) ).
cnf(u4940,hypothesis,
a_1405 = store(a_1404,i7,e7) ).
cnf(u4945,hypothesis,
a_1404 = store(a_1403,i17,e17) ).
cnf(u4950,hypothesis,
a_1403 = store(a_1402,i25,e25) ).
cnf(u4955,hypothesis,
a_1402 = store(a_1401,i11,e11) ).
cnf(u4960,hypothesis,
a_1401 = store(a_1400,i24,e24) ).
cnf(u4965,hypothesis,
a_1400 = store(a_1399,i14,e14) ).
cnf(u4970,hypothesis,
a_1399 = store(a1,i16,e16) ).
cnf(u4975,hypothesis,
a_1398 = store(a_1397,i1,e1) ).
cnf(u4980,hypothesis,
a_1397 = store(a_1396,i39,e39) ).
cnf(u4985,hypothesis,
a_1396 = store(a_1395,i38,e38) ).
cnf(u4990,hypothesis,
a_1395 = store(a_1394,i37,e37) ).
cnf(u4995,hypothesis,
a_1394 = store(a_1393,i36,e36) ).
cnf(u5000,hypothesis,
a_1393 = store(a_1392,i35,e35) ).
cnf(u5005,hypothesis,
a_1392 = store(a_1391,i34,e34) ).
cnf(u5010,hypothesis,
a_1391 = store(a_1390,i33,e33) ).
cnf(u5015,hypothesis,
a_1390 = store(a_1389,i32,e32) ).
cnf(u5020,hypothesis,
a_1389 = store(a_1388,i31,e31) ).
cnf(u5025,hypothesis,
a_1388 = store(a_1387,i30,e30) ).
cnf(u5030,hypothesis,
a_1387 = store(a_1386,i29,e29) ).
cnf(u5035,hypothesis,
a_1386 = store(a_1385,i28,e28) ).
cnf(u5040,hypothesis,
a_1385 = store(a_1384,i27,e27) ).
cnf(u5045,hypothesis,
a_1384 = store(a_1383,i26,e26) ).
cnf(u5050,hypothesis,
a_1383 = store(a_1382,i25,e25) ).
cnf(u5055,hypothesis,
a_1382 = store(a_1381,i24,e24) ).
cnf(u5060,hypothesis,
a_1381 = store(a_1380,i23,e23) ).
cnf(u5065,hypothesis,
a_1380 = store(a_1379,i22,e22) ).
cnf(u5070,hypothesis,
a_1379 = store(a_1378,i21,e21) ).
cnf(u5075,hypothesis,
a_1378 = store(a_1377,i20,e20) ).
cnf(u5080,hypothesis,
a_1377 = store(a_1376,i19,e19) ).
cnf(u5085,hypothesis,
a_1376 = store(a_1375,i18,e18) ).
cnf(u5090,hypothesis,
a_1375 = store(a_1374,i17,e17) ).
cnf(u5095,hypothesis,
a_1374 = store(a_1373,i16,e16) ).
cnf(u5100,hypothesis,
a_1373 = store(a_1372,i15,e15) ).
cnf(u5105,hypothesis,
a_1372 = store(a_1371,i14,e14) ).
cnf(u5110,hypothesis,
a_1371 = store(a_1370,i13,e13) ).
cnf(u5115,hypothesis,
a_1370 = store(a_1369,i12,e12) ).
cnf(u5120,hypothesis,
a_1369 = store(a_1368,i11,e11) ).
cnf(u5125,hypothesis,
a_1368 = store(a_1367,i10,e10) ).
cnf(u5130,hypothesis,
a_1367 = store(a_1366,i9,e9) ).
cnf(u5135,hypothesis,
a_1366 = store(a_1365,i8,e8) ).
cnf(u5140,hypothesis,
a_1365 = store(a_1364,i7,e7) ).
cnf(u5145,hypothesis,
a_1364 = store(a_1363,i6,e6) ).
cnf(u5150,hypothesis,
a_1363 = store(a_1362,i5,e5) ).
cnf(u5155,hypothesis,
a_1362 = store(a_1361,i4,e4) ).
cnf(u5160,hypothesis,
a_1361 = store(a_1360,i3,e3) ).
cnf(u5165,hypothesis,
a_1360 = store(a_1359,i2,e2) ).
cnf(u5170,hypothesis,
a_1359 = store(a1,i1,e1) ).
cnf(u5175,axiom,
store(a_1424,i40,e40) = sF0 ).
cnf(u5181,negated_conjecture,
a_1425 = store(a_1424,i40,e40) ).
cnf(u5266,hypothesis,
e19 = select(a_1438,i19) ).
cnf(u5271,hypothesis,
e29 = select(a_1437,i29) ).
cnf(u5276,hypothesis,
e28 = select(a_1436,i28) ).
cnf(u5281,hypothesis,
e34 = select(a_1435,i34) ).
cnf(u5286,hypothesis,
e15 = select(a_1434,i15) ).
cnf(u5291,hypothesis,
e30 = select(a_1433,i30) ).
cnf(u5296,hypothesis,
e4 = select(a_1432,i4) ).
cnf(u5301,hypothesis,
e5 = select(a_1431,i5) ).
cnf(u5306,hypothesis,
e3 = select(a_1430,i3) ).
cnf(u5311,hypothesis,
e9 = select(a_1429,i9) ).
cnf(u5316,hypothesis,
e1 = select(a_1428,i1) ).
cnf(u5321,hypothesis,
e39 = select(a_1427,i39) ).
cnf(u5326,hypothesis,
e38 = select(a_1426,i38) ).
cnf(u5331,negated_conjecture,
e40 = select(a_1425,i40) ).
cnf(u5336,hypothesis,
e2 = select(a_1424,i2) ).
cnf(u5341,hypothesis,
e33 = select(a_1423,i33) ).
cnf(u5346,hypothesis,
e8 = select(a_1422,i8) ).
cnf(u5351,hypothesis,
e22 = select(a_1421,i22) ).
cnf(u5356,hypothesis,
e10 = select(a_1420,i10) ).
cnf(u5361,hypothesis,
e27 = select(a_1419,i27) ).
cnf(u5366,hypothesis,
e21 = select(a_1418,i21) ).
cnf(u5371,hypothesis,
e26 = select(a_1417,i26) ).
cnf(u5376,hypothesis,
e23 = select(a_1416,i23) ).
cnf(u5381,hypothesis,
e35 = select(a_1415,i35) ).
cnf(u5386,hypothesis,
e20 = select(a_1414,i20) ).
cnf(u5391,hypothesis,
e36 = select(a_1413,i36) ).
cnf(u5396,hypothesis,
e12 = select(a_1412,i12) ).
cnf(u5401,hypothesis,
e13 = select(a_1411,i13) ).
cnf(u5406,hypothesis,
e31 = select(a_1410,i31) ).
cnf(u5411,hypothesis,
e37 = select(a_1409,i37) ).
cnf(u5416,hypothesis,
e18 = select(a_1408,i18) ).
cnf(u5421,hypothesis,
e6 = select(a_1407,i6) ).
cnf(u5426,hypothesis,
e32 = select(a_1406,i32) ).
cnf(u5431,hypothesis,
e7 = select(a_1405,i7) ).
cnf(u5436,hypothesis,
e17 = select(a_1404,i17) ).
cnf(u5441,hypothesis,
e25 = select(a_1403,i25) ).
cnf(u5446,hypothesis,
e11 = select(a_1402,i11) ).
cnf(u5451,hypothesis,
e24 = select(a_1401,i24) ).
cnf(u5456,hypothesis,
e14 = select(a_1400,i14) ).
cnf(u5461,hypothesis,
e1 = select(a_1398,i1) ).
cnf(u5466,hypothesis,
e39 = select(a_1397,i39) ).
cnf(u5471,hypothesis,
e38 = select(a_1396,i38) ).
cnf(u5476,hypothesis,
e37 = select(a_1395,i37) ).
cnf(u5481,hypothesis,
e36 = select(a_1394,i36) ).
cnf(u5486,hypothesis,
e35 = select(a_1393,i35) ).
cnf(u5491,hypothesis,
e34 = select(a_1392,i34) ).
cnf(u5496,hypothesis,
e33 = select(a_1391,i33) ).
cnf(u5501,hypothesis,
e32 = select(a_1390,i32) ).
cnf(u5506,hypothesis,
e31 = select(a_1389,i31) ).
cnf(u5511,hypothesis,
e30 = select(a_1388,i30) ).
cnf(u5516,hypothesis,
e29 = select(a_1387,i29) ).
cnf(u5521,hypothesis,
e28 = select(a_1386,i28) ).
cnf(u5526,hypothesis,
e27 = select(a_1385,i27) ).
cnf(u5531,hypothesis,
e26 = select(a_1384,i26) ).
cnf(u5536,hypothesis,
e25 = select(a_1383,i25) ).
cnf(u5541,hypothesis,
e24 = select(a_1382,i24) ).
cnf(u5546,hypothesis,
e23 = select(a_1381,i23) ).
cnf(u5551,hypothesis,
e22 = select(a_1380,i22) ).
cnf(u5556,hypothesis,
e21 = select(a_1379,i21) ).
cnf(u5561,hypothesis,
e20 = select(a_1378,i20) ).
cnf(u5566,hypothesis,
e19 = select(a_1377,i19) ).
cnf(u5571,hypothesis,
e18 = select(a_1376,i18) ).
cnf(u5576,hypothesis,
e17 = select(a_1375,i17) ).
cnf(u5581,hypothesis,
e16 = select(a_1374,i16) ).
cnf(u5586,hypothesis,
e15 = select(a_1373,i15) ).
cnf(u5591,hypothesis,
e14 = select(a_1372,i14) ).
cnf(u5596,hypothesis,
e13 = select(a_1371,i13) ).
cnf(u5601,hypothesis,
e12 = select(a_1370,i12) ).
cnf(u5606,hypothesis,
e11 = select(a_1369,i11) ).
cnf(u5611,hypothesis,
e10 = select(a_1368,i10) ).
cnf(u5616,hypothesis,
e9 = select(a_1367,i9) ).
cnf(u5621,hypothesis,
e8 = select(a_1366,i8) ).
cnf(u5626,hypothesis,
e7 = select(a_1365,i7) ).
cnf(u5631,hypothesis,
e6 = select(a_1364,i6) ).
cnf(u5636,hypothesis,
e5 = select(a_1363,i5) ).
cnf(u5641,hypothesis,
e4 = select(a_1362,i4) ).
cnf(u5646,hypothesis,
e3 = select(a_1361,i3) ).
cnf(u5651,hypothesis,
e1 = select(a_1359,i1) ).
cnf(u5656,hypothesis,
e16 = select(a_1399,i16) ).
cnf(u5661,hypothesis,
e2 = select(a_1360,i2) ).
cnf(u5684,hypothesis,
( select(a_1378,X0) = select(a_1379,X0)
| i21 = X0 ) ).
cnf(u5688,hypothesis,
( select(a_1382,X0) = select(a_1383,X0)
| i25 = X0 ) ).
cnf(u5726,hypothesis,
( select(a_1421,X0) = select(a_1422,X0)
| i8 = X0 ) ).
cnf(u5692,hypothesis,
( select(a_1386,X0) = select(a_1387,X0)
| i29 = X0 ) ).
cnf(u5701,hypothesis,
( select(a_1395,X0) = select(a_1396,X0)
| i38 = X0 ) ).
cnf(u5707,hypothesis,
( select(a_1402,X0) = select(a_1403,X0)
| i25 = X0 ) ).
cnf(u5718,hypothesis,
( select(a_1413,X0) = select(a_1414,X0)
| i20 = X0 ) ).
cnf(u5719,hypothesis,
( select(a_1414,X0) = select(a_1415,X0)
| i35 = X0 ) ).
cnf(u5712,hypothesis,
( select(a_1407,X0) = select(a_1408,X0)
| i18 = X0 ) ).
cnf(u5741,hypothesis,
( select(a_1436,X0) = select(a_1437,X0)
| i29 = X0 ) ).
cnf(u5702,hypothesis,
( select(a_1396,X0) = select(a_1397,X0)
| i39 = X0 ) ).
cnf(u5728,hypothesis,
( select(a_1423,X0) = select(a_1424,X0)
| i2 = X0 ) ).
cnf(u5663,hypothesis,
( select(a_1359,X0) = select(a_1360,X0)
| i2 = X0 ) ).
cnf(u5666,hypothesis,
( select(a_1360,X0) = select(a_1361,X0)
| i3 = X0 ) ).
cnf(u5685,hypothesis,
( select(a_1379,X0) = select(a_1380,X0)
| i22 = X0 ) ).
cnf(u5671,hypothesis,
( select(a_1365,X0) = select(a_1366,X0)
| i8 = X0 ) ).
cnf(u5738,hypothesis,
( select(a_1433,X0) = select(a_1434,X0)
| i15 = X0 ) ).
cnf(u5679,hypothesis,
( select(a_1373,X0) = select(a_1374,X0)
| i16 = X0 ) ).
cnf(u5665,hypothesis,
( select(a_1359,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(u5715,hypothesis,
( select(a_1410,X0) = select(a_1411,X0)
| i13 = X0 ) ).
cnf(u5735,hypothesis,
( select(a_1430,X0) = select(a_1431,X0)
| i5 = X0 ) ).
cnf(u5723,hypothesis,
( select(a_1418,X0) = select(a_1419,X0)
| i27 = X0 ) ).
cnf(u5740,hypothesis,
( select(a_1435,X0) = select(a_1436,X0)
| i28 = X0 ) ).
cnf(u5669,hypothesis,
( select(a_1363,X0) = select(a_1364,X0)
| i6 = X0 ) ).
cnf(u5686,hypothesis,
( select(a_1380,X0) = select(a_1381,X0)
| i23 = X0 ) ).
cnf(u5737,hypothesis,
( select(a_1432,X0) = select(a_1433,X0)
| i30 = X0 ) ).
cnf(u5689,hypothesis,
( select(a_1383,X0) = select(a_1384,X0)
| i26 = X0 ) ).
cnf(u5687,hypothesis,
( select(a_1381,X0) = select(a_1382,X0)
| i24 = X0 ) ).
cnf(u5742,hypothesis,
( select(a_1437,X0) = select(a_1438,X0)
| i19 = X0 ) ).
cnf(u5683,hypothesis,
( select(a_1377,X0) = select(a_1378,X0)
| i20 = X0 ) ).
cnf(u5713,hypothesis,
( select(a_1408,X0) = select(a_1409,X0)
| i37 = X0 ) ).
cnf(u5709,hypothesis,
( select(a_1404,X0) = select(a_1405,X0)
| i7 = X0 ) ).
cnf(u5670,hypothesis,
( select(a_1364,X0) = select(a_1365,X0)
| i7 = X0 ) ).
cnf(u5722,hypothesis,
( select(a_1417,X0) = select(a_1418,X0)
| i21 = X0 ) ).
cnf(u5732,hypothesis,
( select(a_1427,X0) = select(a_1428,X0)
| i1 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u5691,hypothesis,
( select(a_1385,X0) = select(a_1386,X0)
| i28 = X0 ) ).
cnf(u5703,hypothesis,
( select(a_1397,X0) = select(a_1398,X0)
| i1 = X0 ) ).
cnf(u5708,hypothesis,
( select(a_1403,X0) = select(a_1404,X0)
| i17 = X0 ) ).
cnf(u5729,negated_conjecture,
( select(a_1424,X0) = select(a_1425,X0)
| i40 = X0 ) ).
cnf(u5731,hypothesis,
( select(a_1426,X0) = select(a_1427,X0)
| i39 = X0 ) ).
cnf(u5739,hypothesis,
( select(a_1434,X0) = select(a_1435,X0)
| i34 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u5696,hypothesis,
( select(a_1390,X0) = select(a_1391,X0)
| i33 = X0 ) ).
cnf(u5736,hypothesis,
( select(a_1431,X0) = select(a_1432,X0)
| i4 = X0 ) ).
cnf(u5673,hypothesis,
( select(a_1367,X0) = select(a_1368,X0)
| i10 = X0 ) ).
cnf(u5677,hypothesis,
( select(a_1371,X0) = select(a_1372,X0)
| i14 = X0 ) ).
cnf(u5717,hypothesis,
( select(a_1412,X0) = select(a_1413,X0)
| i36 = X0 ) ).
cnf(u5706,hypothesis,
( select(a_1401,X0) = select(a_1402,X0)
| i11 = X0 ) ).
cnf(u5721,hypothesis,
( select(a_1416,X0) = select(a_1417,X0)
| i26 = X0 ) ).
cnf(u5730,hypothesis,
( select(a_1425,X0) = select(a_1426,X0)
| i38 = X0 ) ).
cnf(u5667,hypothesis,
( select(a_1361,X0) = select(a_1362,X0)
| i4 = X0 ) ).
cnf(u5725,hypothesis,
( select(a_1420,X0) = select(a_1421,X0)
| i22 = X0 ) ).
cnf(u5710,hypothesis,
( select(a_1405,X0) = select(a_1406,X0)
| i32 = X0 ) ).
cnf(u5676,hypothesis,
( select(a_1370,X0) = select(a_1371,X0)
| i13 = X0 ) ).
cnf(u5693,hypothesis,
( select(a_1387,X0) = select(a_1388,X0)
| i30 = X0 ) ).
cnf(u5678,hypothesis,
( select(a_1372,X0) = select(a_1373,X0)
| i15 = X0 ) ).
cnf(u5680,hypothesis,
( select(a_1374,X0) = select(a_1375,X0)
| i17 = X0 ) ).
cnf(u5697,hypothesis,
( select(a_1391,X0) = select(a_1392,X0)
| i34 = X0 ) ).
cnf(u5705,hypothesis,
( select(a_1400,X0) = select(a_1401,X0)
| i24 = X0 ) ).
cnf(u5699,hypothesis,
( select(a_1393,X0) = select(a_1394,X0)
| i36 = X0 ) ).
cnf(u5720,hypothesis,
( select(a_1415,X0) = select(a_1416,X0)
| i23 = X0 ) ).
cnf(u5724,hypothesis,
( select(a_1419,X0) = select(a_1420,X0)
| i10 = X0 ) ).
cnf(u5674,hypothesis,
( select(a_1368,X0) = select(a_1369,X0)
| i11 = X0 ) ).
cnf(u5681,hypothesis,
( select(a_1375,X0) = select(a_1376,X0)
| i18 = X0 ) ).
cnf(u5690,hypothesis,
( select(a_1384,X0) = select(a_1385,X0)
| i27 = X0 ) ).
cnf(u5727,hypothesis,
( select(a_1422,X0) = select(a_1423,X0)
| i33 = X0 ) ).
cnf(u5664,hypothesis,
( select(a1,X0) = select(a_1399,X0)
| i16 = X0 ) ).
cnf(u5700,hypothesis,
( select(a_1394,X0) = select(a_1395,X0)
| i37 = X0 ) ).
cnf(u5734,hypothesis,
( select(a_1429,X0) = select(a_1430,X0)
| i3 = X0 ) ).
cnf(u5704,hypothesis,
( select(a_1399,X0) = select(a_1400,X0)
| i14 = X0 ) ).
cnf(u5675,hypothesis,
( select(a_1369,X0) = select(a_1370,X0)
| i12 = X0 ) ).
cnf(u5668,hypothesis,
( select(a_1362,X0) = select(a_1363,X0)
| i5 = X0 ) ).
cnf(u5695,hypothesis,
( select(a_1389,X0) = select(a_1390,X0)
| i32 = X0 ) ).
cnf(u5694,hypothesis,
( select(a_1388,X0) = select(a_1389,X0)
| i31 = X0 ) ).
cnf(u5672,hypothesis,
( select(a_1366,X0) = select(a_1367,X0)
| i9 = X0 ) ).
cnf(u5711,hypothesis,
( select(a_1406,X0) = select(a_1407,X0)
| i6 = X0 ) ).
cnf(u5698,hypothesis,
( select(a_1392,X0) = select(a_1393,X0)
| i35 = X0 ) ).
cnf(u5714,hypothesis,
( select(a_1409,X0) = select(a_1410,X0)
| i31 = X0 ) ).
cnf(u5733,hypothesis,
( select(a_1428,X0) = select(a_1429,X0)
| i9 = X0 ) ).
cnf(u5682,hypothesis,
( select(a_1376,X0) = select(a_1377,X0)
| i19 = X0 ) ).
cnf(u5716,hypothesis,
( select(a_1411,X0) = select(a_1412,X0)
| i12 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV498-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n006.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:16:55 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.93/1.96 % (3895093)Input is clausal, will run a generic CNF schedule.
% 7.93/1.96 % (3895225)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2728151235:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.93/1.96 % (3895237)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1624838603:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.93/1.96 % (3895235)lrs+10_1_sil=8000:sp=occurrence:random_seed=524611893:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.93/1.96 % (3895234)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=242855849:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.93/1.96 % (3895236)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3086012950:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.93/1.96 % (3895238)dis-21_1_sil=8000:lcm=predicate:random_seed=4261292030:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.93/1.96 % (3895230)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3246616346:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.93/1.96 % (3895235)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895235)------------------------------
% 7.93/1.96 % (3895235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895235)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895235)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895235)Time elapsed: 0.013 s
% 7.93/1.96 % (3895235)Peak memory usage: 88 MB
% 7.93/1.96 % (3895235)Instructions burned: 28 (million)
% 7.93/1.96 % (3895238)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895238)------------------------------
% 7.93/1.96 % (3895238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895238)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895238)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895238)Time elapsed: 0.021 s
% 7.93/1.96 % (3895238)Peak memory usage: 89 MB
% 7.93/1.96 % (3895238)Instructions burned: 42 (million)
% 7.93/1.96 % (3895236)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895236)------------------------------
% 7.93/1.96 % (3895236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895236)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895236)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895236)Time elapsed: 0.027 s
% 7.93/1.96 % (3895236)Peak memory usage: 88 MB
% 7.93/1.96 % (3895236)Instructions burned: 55 (million)
% 7.93/1.96 % (3895237)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895237)------------------------------
% 7.93/1.96 % (3895237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895237)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895237)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895237)Time elapsed: 0.029 s
% 7.93/1.96 % (3895237)Peak memory usage: 88 MB
% 7.93/1.96 % (3895237)Instructions burned: 59 (million)
% 7.93/1.96 % (3895235)------------------------------
% 7.93/1.96 % (3895235)------------------------------
% 7.93/1.96 % (3895238)------------------------------
% 7.93/1.96 % (3895238)------------------------------
% 7.93/1.96 % (3895236)------------------------------
% 7.93/1.96 % (3895236)------------------------------
% 7.93/1.96 % (3895237)------------------------------
% 7.93/1.96 % (3895237)------------------------------
% 7.93/1.96 % (3895330)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=403515441:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 7.93/1.96 % (3895327)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3365697032:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 7.93/1.96 % (3895327)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895327)------------------------------
% 7.93/1.96 % (3895327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895327)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895327)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895327)Time elapsed: 0.018 s
% 7.93/1.96 % (3895327)Peak memory usage: 88 MB
% 7.93/1.96 % (3895327)Instructions burned: 34 (million)
% 7.93/1.96 % (3895332)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3780392447:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 7.93/1.96 % (3895333)lrs+10_64_to=lpo:sil=8000:random_seed=1298389694:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 7.93/1.96 % (3895330)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895330)------------------------------
% 7.93/1.96 % (3895330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895330)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895330)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895330)Time elapsed: 0.032 s
% 7.93/1.96 % (3895330)Peak memory usage: 89 MB
% 7.93/1.96 % (3895330)Instructions burned: 67 (million)
% 7.93/1.96 % (3895332)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895332)------------------------------
% 7.93/1.96 % (3895332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895332)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895332)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895332)Time elapsed: 0.015 s
% 7.93/1.96 % (3895332)Peak memory usage: 88 MB
% 7.93/1.96 % (3895332)Instructions burned: 32 (million)
% 7.93/1.96 % (3895333)Instruction limit reached!
% 7.93/1.96 % (3895333)------------------------------
% 7.93/1.96 % (3895333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895333)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895333)Termination reason: Instruction limit
% 7.93/1.96 % (3895333)Termination phase: Saturation
% 7.93/1.96 % (3895333)Time elapsed: 0.058 s
% 7.93/1.96 % (3895333)Peak memory usage: 88 MB
% 7.93/1.96 % (3895333)Instructions burned: 128 (million)
% 7.93/1.96 % (3895367)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2785916578:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 7.93/1.96 % (3895327)------------------------------
% 7.93/1.96 % (3895327)------------------------------
% 7.93/1.96 % (3895367)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895367)------------------------------
% 7.93/1.96 % (3895367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895367)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895367)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895367)Time elapsed: 0.026 s
% 7.93/1.96 % (3895367)Peak memory usage: 88 MB
% 7.93/1.96 % (3895367)Instructions burned: 54 (million)
% 7.93/1.96 % (3895330)------------------------------
% 7.93/1.96 % (3895330)------------------------------
% 7.93/1.96 % (3895332)------------------------------
% 7.93/1.96 % (3895332)------------------------------
% 7.93/1.96 % (3895225)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895225)------------------------------
% 7.93/1.96 % (3895225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895225)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895225)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895225)Time elapsed: 0.763 s
% 7.93/1.96 % (3895225)Peak memory usage: 134 MB
% 7.93/1.96 % (3895225)Instructions burned: 1184 (million)
% 7.93/1.96 % (3895234)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895234)------------------------------
% 7.93/1.96 % (3895234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895234)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895234)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895234)Time elapsed: 0.767 s
% 7.93/1.96 % (3895234)Peak memory usage: 135 MB
% 7.93/1.96 % (3895234)Instructions burned: 1197 (million)
% 7.93/1.96 % (3895416)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2413043628:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 7.93/1.96 % (3895417)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3350195739:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 7.93/1.96 % (3895418)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3449487323:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 7.93/1.96 % (3895416)First to succeed.
% 7.93/1.96 % (3895418)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895418)------------------------------
% 7.93/1.96 % (3895418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895418)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895418)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895418)Time elapsed: 0.022 s
% 7.93/1.96 % (3895418)Peak memory usage: 88 MB
% 7.93/1.96 % (3895418)Instructions burned: 44 (million)
% 7.93/1.96 % (3895416)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3895093"
% 7.93/1.96 % (3895367)------------------------------
% 7.93/1.96 % (3895367)------------------------------
% 7.93/1.96 % (3895225)------------------------------
% 7.93/1.96 % (3895225)------------------------------
% 7.93/1.96 % (3895234)------------------------------
% 7.93/1.96 % (3895234)------------------------------
% 7.93/1.96 % (3895422)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1112804856:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 7.93/1.96 % (3895418)------------------------------
% 7.93/1.96 % (3895418)------------------------------
% 7.93/1.96 % (3895422)Refutation not found, incomplete strategy
% 7.93/1.96 % (3895422)------------------------------
% 7.93/1.96 % (3895422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/1.96 % (3895422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/1.96 % (3895422)CaDiCaL version: 2.1.3
% 7.93/1.96 % (3895422)Termination reason: Refutation not found, incomplete strategy
% 7.93/1.96 % (3895422)Time elapsed: 0.023 s
% 7.93/1.96 % (3895422)Peak memory usage: 88 MB
% 7.93/1.96 % (3895422)Instructions burned: 46 (million)
% 7.93/1.96 % SZS status Satisfiable for theBenchmark
% 7.93/1.96 % SZS output start Saturation.
% See solution above
% 9.79/2.14 % SZS output start Definitions and Model Updates.
% 9.79/2.14 % SZS output end Definitions and Model Updates.
% 9.79/2.14 % (3895416)------------------------------
% 9.79/2.14 % (3895416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.14 % (3895416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.14 % (3895416)CaDiCaL version: 2.1.3
% 9.79/2.14 % (3895416)Termination reason: Satisfiable
% 9.79/2.14 % (3895416)Time elapsed: 0.044 s
% 9.79/2.14 % (3895416)Peak memory usage: 91 MB
% 9.79/2.14 % (3895416)Instructions burned: 82 (million)
% 9.79/2.14 % (3895416)------------------------------
% 9.79/2.14 % (3895416)------------------------------
% 9.79/2.14 % (3895093)Success in time 1.299 s
% 9.79/2.14 % Vampire exiting
%------------------------------------------------------------------------------