%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV502-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 : n014.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:08 PM UTC 2026
% Result : Satisfiable 27.74s 5.00s
% Output : Saturation 0.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1894,axiom,
i1 != sF80 ).
cnf(u1899,axiom,
sF81 = select(sF38,sF80) ).
cnf(u2009,axiom,
i19 != sF80 ).
cnf(u2014,axiom,
sF82 = select(sF78,sF80) ).
cnf(u2161,axiom,
i29 != sF80 ).
cnf(u2166,axiom,
sF82 = select(sF77,sF80) ).
cnf(u2271,axiom,
i39 != sF80 ).
cnf(u2276,axiom,
sF81 = select(sF37,sF80) ).
cnf(u2377,axiom,
i28 != sF80 ).
cnf(u2382,axiom,
sF82 = select(sF76,sF80) ).
cnf(u2490,axiom,
i34 != sF80 ).
cnf(u2495,axiom,
sF82 = select(sF75,sF80) ).
cnf(u2582,axiom,
i38 != sF80 ).
cnf(u2587,axiom,
sF81 = select(sF36,sF80) ).
cnf(u2687,axiom,
i37 != sF80 ).
cnf(u2692,axiom,
sF81 = select(sF35,sF80) ).
cnf(u2863,axiom,
i36 != sF80 ).
cnf(u2868,axiom,
sF81 = select(sF34,sF80) ).
cnf(u3026,axiom,
i15 != sF80 ).
cnf(u3031,axiom,
sF82 = select(sF74,sF80) ).
cnf(u3185,axiom,
i30 != sF80 ).
cnf(u3190,axiom,
sF82 = select(sF73,sF80) ).
cnf(u3287,axiom,
i35 != sF80 ).
cnf(u3292,axiom,
sF81 = select(sF33,sF80) ).
cnf(u3441,axiom,
i33 != sF80 ).
cnf(u3446,axiom,
sF81 = select(sF31,sF80) ).
cnf(u3565,axiom,
i4 != sF80 ).
cnf(u3570,axiom,
sF82 = select(sF72,sF80) ).
cnf(u3762,axiom,
i5 != sF80 ).
cnf(u3767,axiom,
sF82 = select(sF71,sF80) ).
cnf(u3958,axiom,
i3 != sF80 ).
cnf(u3963,axiom,
sF82 = select(sF70,sF80) ).
cnf(u4165,axiom,
i9 != sF80 ).
cnf(u4170,axiom,
sF82 = select(sF69,sF80) ).
cnf(u4364,axiom,
i40 = sF80 ).
cnf(u661,hypothesis,
i36 != i14 ).
cnf(u1816,axiom,
e36 = select(sF54,i36) ).
cnf(u1021,hypothesis,
i27 != i8 ).
cnf(u1415,hypothesis,
i37 != i2 ).
cnf(u1553,hypothesis,
i6 != i1 ).
cnf(u659,hypothesis,
i37 != i14 ).
cnf(u1788,axiom,
e4 = select(sF3,i4) ).
cnf(u1019,hypothesis,
i28 != i8 ).
cnf(u4486,hypothesis,
sF81 = select(sF15,sF80) ).
cnf(u21,hypothesis,
i37 != i36 ).
cnf(u1877,axiom,
( select(sF45,X0) = select(sF46,X0)
| i7 = X0 ) ).
cnf(u151,hypothesis,
i32 != i28 ).
cnf(u289,hypothesis,
i33 != i23 ).
cnf(u1786,axiom,
e24 = select(sF42,i24) ).
cnf(u521,hypothesis,
i34 != i17 ).
cnf(u4389,hypothesis,
i20 != sF80 ).
cnf(u1566,axiom,
store(sF0,i2,e2) = sF1 ).
cnf(u805,hypothesis,
i17 != i12 ).
cnf(u1327,hypothesis,
i8 != i4 ).
cnf(u1664,axiom,
store(sF49,i37,e37) = sF50 ).
cnf(u535,hypothesis,
i27 != i17 ).
cnf(u1171,hypothesis,
i17 != i6 ).
cnf(u1401,hypothesis,
i7 != i3 ).
cnf(u1572,axiom,
store(sF3,i5,e5) = sF4 ).
cnf(u803,hypothesis,
i18 != i12 ).
cnf(u1129,hypothesis,
i38 != i6 ).
cnf(u149,hypothesis,
i33 != i28 ).
cnf(u295,hypothesis,
i30 != i23 ).
cnf(u1570,axiom,
store(sF2,i4,e4) = sF3 ).
cnf(u417,hypothesis,
i23 != i20 ).
cnf(u649,hypothesis,
i17 != i15 ).
cnf(u3429,axiom,
sF81 = select(sF32,sF80) ).
cnf(u1819,axiom,
( select(sF64,X0) = select(sF63,X0)
| i33 = X0 ) ).
cnf(u1694,axiom,
store(sF64,i2,e2) = sF65 ).
cnf(u1576,axiom,
store(sF5,i7,e7) = sF6 ).
cnf(u1455,hypothesis,
i17 != i2 ).
cnf(u663,hypothesis,
i35 != i14 ).
cnf(u1825,axiom,
( select(sF53,X0) = select(sF52,X0)
| i12 = X0 ) ).
cnf(u1700,axiom,
store(sF67,i39,e39) = sF68 ).
cnf(u931,hypothesis,
i11 != i10 ).
cnf(u61,hypothesis,
i39 != i32 ).
cnf(u293,hypothesis,
i31 != i23 ).
cnf(u1698,axiom,
store(sF66,i38,e38) = sF67 ).
cnf(u561,hypothesis,
i37 != i16 ).
cnf(u1169,hypothesis,
i18 != i6 ).
cnf(u4387,hypothesis,
i22 != sF80 ).
cnf(u1077,hypothesis,
i31 != i7 ).
cnf(u1704,axiom,
store(sF69,i9,e9) = sF70 ).
cnf(u575,hypothesis,
i30 != i16 ).
cnf(u1427,hypothesis,
i31 != i2 ).
cnf(u51,hypothesis,
i37 != i33 ).
cnf(u189,hypothesis,
i38 != i26 ).
cnf(u421,hypothesis,
i21 != i20 ).
cnf(u729,hypothesis,
i28 != i13 ).
cnf(u689,hypothesis,
i22 != i14 ).
cnf(u1606,axiom,
store(sF20,i22,e22) = sF21 ).
cnf(u1205,hypothesis,
i34 != i5 ).
cnf(u703,hypothesis,
i15 != i14 ).
cnf(u1499,hypothesis,
i33 != i1 ).
cnf(u1491,hypothesis,
i37 != i1 ).
cnf(u179,hypothesis,
i30 != i27 ).
cnf(u1861,axiom,
( select(sF72,X0) = select(sF73,X0)
| i4 = X0 ) ).
cnf(u335,hypothesis,
i27 != i22 ).
cnf(u571,hypothesis,
i32 != i16 ).
cnf(u1087,hypothesis,
i26 != i7 ).
cnf(u1209,hypothesis,
i32 != i5 ).
cnf(u1859,axiom,
( select(sF73,X0) = select(sF74,X0)
| i30 = X0 ) ).
cnf(u1734,axiom,
e16 = select(sF40,i16) ).
cnf(u4418,axiom,
e40 = select(sF76,sF80) ).
cnf(u1865,axiom,
( select(sF22,X0) = select(sF21,X0)
| i23 = X0 ) ).
cnf(u177,hypothesis,
i31 != i27 ).
cnf(u333,hypothesis,
i28 != i22 ).
cnf(u1879,axiom,
( select(sF37,X0) = select(sF36,X0)
| i38 = X0 ) ).
cnf(u1215,hypothesis,
i29 != i5 ).
cnf(u833,hypothesis,
i31 != i11 ).
cnf(u1117,hypothesis,
i11 != i7 ).
cnf(u1349,hypothesis,
i33 != i3 ).
cnf(u1257,hypothesis,
i8 != i5 ).
cnf(u847,hypothesis,
i24 != i11 ).
cnf(u4546,hypothesis,
sF81 = select(sF0,sF80) ).
cnf(u91,hypothesis,
i32 != i31 ).
cnf(u323,hypothesis,
i33 != i22 ).
cnf(u461,hypothesis,
i21 != i19 ).
cnf(u1313,hypothesis,
i15 != i4 ).
cnf(u961,hypothesis,
i26 != i9 ).
cnf(u1107,hypothesis,
i16 != i7 ).
cnf(u173,hypothesis,
i33 != i27 ).
cnf(u1245,hypothesis,
i14 != i5 ).
cnf(u1477,hypothesis,
i6 != i2 ).
cnf(u4424,axiom,
e40 = select(sF70,sF80) ).
cnf(u975,hypothesis,
i19 != i9 ).
cnf(u89,hypothesis,
i33 != i31 ).
cnf(u451,hypothesis,
i26 != i19 ).
cnf(u1878,axiom,
e38 = select(sF37,i38) ).
cnf(u605,hypothesis,
i39 != i15 ).
cnf(u1127,hypothesis,
i39 != i6 ).
cnf(u391,hypothesis,
i36 != i20 ).
cnf(u1339,hypothesis,
i38 != i3 ).
cnf(u1884,axiom,
e16 = select(sF15,i16) ).
cnf(u1389,hypothesis,
i13 != i3 ).
cnf(u431,hypothesis,
i36 != i19 ).
cnf(u887,hypothesis,
i33 != i10 ).
cnf(u95,hypothesis,
i39 != i30 ).
cnf(u1882,axiom,
e3 = select(sF71,i3) ).
cnf(u217,hypothesis,
i38 != i25 ).
cnf(u363,hypothesis,
i31 != i21 ).
cnf(u1543,hypothesis,
i11 != i1 ).
cnf(u1812,axiom,
e32 = select(sF47,i32) ).
cnf(u733,hypothesis,
i26 != i13 ).
cnf(u1255,hypothesis,
i9 != i5 ).
cnf(u4395,hypothesis,
i14 != sF80 ).
cnf(u1001,hypothesis,
i37 != i8 ).
cnf(u1487,hypothesis,
i39 != i1 ).
cnf(u1147,hypothesis,
i29 != i6 ).
cnf(u731,hypothesis,
i27 != i13 ).
cnf(u1810,axiom,
e19 = select(sF18,i19) ).
cnf(u1517,hypothesis,
i24 != i1 ).
cnf(u1015,hypothesis,
i30 != i8 ).
cnf(u641,hypothesis,
i21 != i15 ).
cnf(u223,hypothesis,
i35 != i25 ).
cnf(u361,hypothesis,
i32 != i21 ).
cnf(u491,hypothesis,
i27 != i18 ).
cnf(u517,hypothesis,
i36 != i17 ).
cnf(u1747,axiom,
( select(sF23,X0) = select(sF24,X0)
| i25 = X0 ) ).
cnf(u877,hypothesis,
i38 != i10 ).
cnf(u1399,hypothesis,
i8 != i3 ).
cnf(u1521,hypothesis,
i22 != i1 ).
cnf(u1796,axiom,
e31 = select(sF30,i31) ).
cnf(u515,hypothesis,
i37 != i17 ).
cnf(u1753,axiom,
( select(sF23,X0) = select(sF22,X0)
| i24 = X0 ) ).
cnf(u875,hypothesis,
i39 != i10 ).
cnf(u7,hypothesis,
i39 != i38 ).
cnf(u1794,axiom,
e18 = select(sF49,i18) ).
cnf(u1767,axiom,
( select(sF9,X0) = select(sF10,X0)
| i11 = X0 ) ).
cnf(u1642,axiom,
store(sF38,i1,e1) = sF39 ).
cnf(u489,hypothesis,
i28 != i18 ).
cnf(u1821,axiom,
( select(sF60,X0) = select(sF61,X0)
| i10 = X0 ) ).
cnf(u645,hypothesis,
i19 != i15 ).
cnf(u1800,axiom,
e31 = select(sF51,i31) ).
cnf(u4410,axiom,
e40 = select(sF66,sF80) ).
cnf(u1005,hypothesis,
i35 != i8 ).
cnf(u1648,axiom,
store(sF41,i24,e24) = sF42 ).
cnf(u1527,hypothesis,
i19 != i1 ).
cnf(u1537,hypothesis,
i14 != i1 ).
cnf(u1839,axiom,
( select(sF51,X0) = select(sF52,X0)
| i13 = X0 ) ).
cnf(u1772,axiom,
e35 = select(sF34,i35) ).
cnf(u1003,hypothesis,
i36 != i8 ).
cnf(u1789,axiom,
( select(sF2,X0) = select(sF3,X0)
| i4 = X0 ) ).
cnf(u273,hypothesis,
i25 != i24 ).
cnf(u495,hypothesis,
i25 != i18 ).
cnf(u1770,axiom,
e27 = select(sF26,i27) ).
cnf(u633,hypothesis,
i25 != i15 ).
cnf(u1787,axiom,
( select(sF41,X0) = select(sF42,X0)
| i24 = X0 ) ).
cnf(u789,hypothesis,
i25 != i12 ).
cnf(u1311,hypothesis,
i16 != i4 ).
cnf(u1163,hypothesis,
i21 != i6 ).
cnf(u1776,axiom,
e13 = select(sF12,i13) ).
cnf(u519,hypothesis,
i35 != i17 ).
cnf(u787,hypothesis,
i26 != i12 ).
cnf(u4502,hypothesis,
sF81 = select(sF11,sF80) ).
cnf(u4388,hypothesis,
i21 != sF80 ).
cnf(u133,hypothesis,
i30 != i29 ).
cnf(u279,hypothesis,
i38 != i23 ).
cnf(u401,hypothesis,
i31 != i20 ).
cnf(u4413,hypothesis,
sF81 = select(sF30,sF80) ).
cnf(u1025,hypothesis,
i25 != i8 ).
cnf(u1155,hypothesis,
i25 != i6 ).
cnf(u1803,axiom,
( select(sF16,X0) = select(sF17,X0)
| i18 = X0 ) ).
cnf(u1678,axiom,
store(sF56,i23,e23) = sF57 ).
cnf(u917,hypothesis,
i18 != i10 ).
cnf(u1439,hypothesis,
i25 != i2 ).
cnf(u1195,hypothesis,
i39 != i5 ).
cnf(u647,hypothesis,
i18 != i15 ).
cnf(u1809,axiom,
( select(sF19,X0) = select(sF20,X0)
| i21 = X0 ) ).
cnf(u1684,axiom,
store(sF59,i27,e27) = sF60 ).
cnf(u915,hypothesis,
i19 != i10 ).
cnf(u4425,axiom,
e40 = select(sF69,sF80) ).
cnf(u277,hypothesis,
i39 != i23 ).
cnf(u1823,axiom,
( select(sF38,X0) = select(sF37,X0)
| i39 = X0 ) ).
cnf(u1682,axiom,
store(sF58,i21,e21) = sF59 ).
cnf(u545,hypothesis,
i22 != i17 ).
cnf(u1137,hypothesis,
i34 != i6 ).
cnf(u1590,axiom,
store(sF12,i14,e14) = sF13 ).
cnf(u829,hypothesis,
i33 != i11 ).
cnf(u1061,hypothesis,
i39 != i7 ).
cnf(u1688,axiom,
store(sF61,i22,e22) = sF62 ).
cnf(u559,hypothesis,
i38 != i16 ).
cnf(u4403,hypothesis,
i6 != sF80 ).
cnf(u1596,axiom,
store(sF15,i17,e17) = sF16 ).
cnf(u35,hypothesis,
i39 != i34 ).
cnf(u1845,axiom,
( select(sF12,X0) = select(sF13,X0)
| i14 = X0 ) ).
cnf(u319,hypothesis,
i35 != i22 ).
cnf(u405,hypothesis,
i29 != i20 ).
cnf(u1065,hypothesis,
i37 != i7 ).
cnf(u4482,hypothesis,
sF81 = select(sF16,sF80) ).
cnf(u1843,axiom,
( select(sF28,X0) = select(sF29,X0)
| i30 = X0 ) ).
cnf(u1718,axiom,
store(sF76,i28,e28) = sF77 ).
cnf(u1411,hypothesis,
i39 != i2 ).
cnf(u1189,hypothesis,
i8 != i6 ).
cnf(u687,hypothesis,
i23 != i14 ).
cnf(u1849,axiom,
( select(sF63,X0) = select(sF62,X0)
| i8 = X0 ) ).
cnf(u1451,hypothesis,
i19 != i2 ).
cnf(u163,hypothesis,
i38 != i27 ).
cnf(u317,hypothesis,
i36 != i22 ).
cnf(u447,hypothesis,
i28 != i19 ).
cnf(u1071,hypothesis,
i34 != i7 ).
cnf(u511,hypothesis,
i39 != i17 ).
cnf(u1333,hypothesis,
i5 != i4 ).
cnf(u831,hypothesis,
i32 != i11 ).
cnf(u161,hypothesis,
i39 != i27 ).
cnf(u307,hypothesis,
i24 != i23 ).
cnf(u445,hypothesis,
i29 != i19 ).
cnf(u1863,axiom,
( select(sF49,X0) = select(sF50,X0)
| i37 = X0 ) ).
cnf(u1199,hypothesis,
i37 != i5 ).
cnf(u945,hypothesis,
i34 != i9 ).
cnf(u1101,hypothesis,
i19 != i7 ).
cnf(u1461,hypothesis,
i14 != i2 ).
cnf(u959,hypothesis,
i27 != i9 ).
cnf(u435,hypothesis,
i34 != i19 ).
cnf(u1766,axiom,
e11 = select(sF10,i11) ).
cnf(u1241,hypothesis,
i16 != i5 ).
cnf(u1465,hypothesis,
i12 != i2 ).
cnf(u1091,hypothesis,
i24 != i7 ).
cnf(u1229,hypothesis,
i22 != i5 ).
cnf(u4442,hypothesis,
sF81 = select(sF26,sF80) ).
cnf(u73,hypothesis,
i33 != i32 ).
cnf(u375,hypothesis,
i25 != i21 ).
cnf(u1297,hypothesis,
i23 != i4 ).
cnf(u1862,axiom,
e37 = select(sF50,i37) ).
cnf(u589,hypothesis,
i23 != i16 ).
cnf(u1111,hypothesis,
i14 != i7 ).
cnf(u857,hypothesis,
i19 != i11 ).
cnf(u1267,hypothesis,
i38 != i4 ).
cnf(u1868,axiom,
e15 = select(sF75,i15) ).
cnf(u1219,hypothesis,
i27 != i5 ).
cnf(u1373,hypothesis,
i21 != i3 ).
cnf(u871,hypothesis,
i12 != i11 ).
cnf(u79,hypothesis,
i38 != i31 ).
cnf(u1866,axiom,
e15 = select(sF14,i15) ).
cnf(u201,hypothesis,
i32 != i26 ).
cnf(u1493,hypothesis,
i36 != i1 ).
cnf(u347,hypothesis,
i39 != i21 ).
cnf(u1323,hypothesis,
i10 != i4 ).
cnf(u1337,hypothesis,
i39 != i3 ).
cnf(u717,hypothesis,
i34 != i13 ).
cnf(u1872,axiom,
e6 = select(sF48,i6) ).
cnf(u1239,hypothesis,
i17 != i5 ).
cnf(u415,hypothesis,
i24 != i20 ).
cnf(u985,hypothesis,
i14 != i9 ).
cnf(u1131,hypothesis,
i37 != i6 ).
cnf(u715,hypothesis,
i35 != i13 ).
cnf(u1501,hypothesis,
i32 != i1 ).
cnf(u999,hypothesis,
i38 != i8 ).
cnf(u207,hypothesis,
i29 != i26 ).
cnf(u475,hypothesis,
i35 != i18 ).
cnf(u1547,hypothesis,
i9 != i1 ).
cnf(u629,hypothesis,
i27 != i15 ).
cnf(u1731,axiom,
( select(sF78,X0) = select(sF79,X0)
| i19 = X0 ) ).
cnf(u861,hypothesis,
i17 != i11 ).
cnf(u1383,hypothesis,
i16 != i3 ).
cnf(u1505,hypothesis,
i30 != i1 ).
cnf(u627,hypothesis,
i28 != i15 ).
cnf(u1737,axiom,
( select(sF38,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u859,hypothesis,
i18 != i11 ).
cnf(u4454,hypothesis,
sF81 = select(sF23,sF80) ).
cnf(u119,hypothesis,
i37 != i29 ).
cnf(u4392,hypothesis,
i17 != sF80 ).
cnf(u1751,axiom,
( select(sF3,X0) = select(sF4,X0)
| i5 = X0 ) ).
cnf(u1626,axiom,
store(sF30,i32,e32) = sF31 ).
cnf(u473,hypothesis,
i36 != i18 ).
cnf(u757,hypothesis,
i14 != i13 ).
cnf(u989,hypothesis,
i12 != i9 ).
cnf(u1632,axiom,
store(sF33,i35,e35) = sF34 ).
cnf(u1511,hypothesis,
i27 != i1 ).
cnf(u755,hypothesis,
i15 != i13 ).
cnf(u1756,axiom,
e35 = select(sF56,i35) ).
cnf(u1113,hypothesis,
i13 != i7 ).
cnf(u117,hypothesis,
i38 != i29 ).
cnf(u1805,axiom,
( select(sF44,X0) = select(sF43,X0)
| i25 = X0 ) ).
cnf(u247,hypothesis,
i38 != i24 ).
cnf(u257,hypothesis,
i33 != i24 ).
cnf(u479,hypothesis,
i33 != i18 ).
cnf(u1754,axiom,
e5 = select(sF72,i5) ).
cnf(u617,hypothesis,
i33 != i15 ).
cnf(u1771,axiom,
( select(sF25,X0) = select(sF26,X0)
| i27 = X0 ) ).
cnf(u1662,axiom,
store(sF48,i18,e18) = sF49 ).
cnf(u773,hypothesis,
i33 != i12 ).
cnf(u1295,hypothesis,
i24 != i4 ).
cnf(u1760,axiom,
e23 = select(sF57,i23) ).
cnf(u631,hypothesis,
i26 != i15 ).
cnf(u1777,axiom,
( select(sF11,X0) = select(sF12,X0)
| i13 = X0 ) ).
cnf(u771,hypothesis,
i34 != i12 ).
cnf(u1557,hypothesis,
i4 != i1 ).
cnf(u1095,hypothesis,
i22 != i7 ).
cnf(u245,hypothesis,
i39 != i24 ).
cnf(u263,hypothesis,
i30 != i24 ).
cnf(u385,hypothesis,
i39 != i20 ).
cnf(u1555,hypothesis,
i5 != i1 ).
cnf(u745,hypothesis,
i20 != i13 ).
cnf(u1790,axiom,
e26 = select(sF58,i26) ).
cnf(u901,hypothesis,
i26 != i10 ).
cnf(u1423,hypothesis,
i33 != i2 ).
cnf(u1561,hypothesis,
i2 != i1 ).
cnf(u1793,axiom,
( select(sF32,X0) = select(sF33,X0)
| i34 = X0 ) ).
cnf(u1668,axiom,
store(sF51,i13,e13) = sF52 ).
cnf(u899,hypothesis,
i27 != i10 ).
cnf(u29,hypothesis,
i37 != i35 ).
cnf(u261,hypothesis,
i31 != i24 ).
cnf(u1807,axiom,
( select(sF42,X0) = select(sF43,X0)
| i11 = X0 ) ).
cnf(u1666,axiom,
store(sF50,i31,e31) = sF51 ).
cnf(u529,hypothesis,
i30 != i17 ).
cnf(u1179,hypothesis,
i13 != i6 ).
cnf(u1574,axiom,
store(sF4,i6,e6) = sF5 ).
cnf(u1045,hypothesis,
i15 != i8 ).
cnf(u1672,axiom,
store(sF53,i36,e36) = sF54 ).
cnf(u543,hypothesis,
i23 != i17 ).
cnf(u1580,axiom,
store(sF7,i9,e9) = sF8 ).
cnf(u19,hypothesis,
i38 != i36 ).
cnf(u157,hypothesis,
i29 != i28 ).
cnf(u303,hypothesis,
i26 != i23 ).
cnf(u389,hypothesis,
i37 != i20 ).
cnf(u1395,hypothesis,
i10 != i3 ).
cnf(u1049,hypothesis,
i13 != i8 ).
cnf(u1827,axiom,
( select(sF67,X0) = select(sF68,X0)
| i39 = X0 ) ).
cnf(u1702,axiom,
store(sF68,i1,e1) = sF69 ).
cnf(u4415,negated_conjecture,
e40 != sF81 ).
cnf(u1173,hypothesis,
i16 != i6 ).
cnf(u671,hypothesis,
i31 != i14 ).
cnf(u4386,hypothesis,
i23 != sF80 ).
cnf(u1833,axiom,
( select(sF10,X0) = select(sF11,X0)
| i12 = X0 ) ).
cnf(u17,hypothesis,
i39 != i36 ).
cnf(u147,hypothesis,
i34 != i28 ).
cnf(u301,hypothesis,
i27 != i23 ).
cnf(u1847,axiom,
( select(sF55,X0) = select(sF54,X0)
| i20 = X0 ) ).
cnf(u569,hypothesis,
i33 != i16 ).
cnf(u1055,hypothesis,
i10 != i8 ).
cnf(u801,hypothesis,
i19 != i12 ).
cnf(u1315,hypothesis,
i14 != i4 ).
cnf(u1085,hypothesis,
i27 != i7 ).
cnf(u1317,hypothesis,
i13 != i4 ).
cnf(u4427,axiom,
e40 = select(sF67,sF80) ).
cnf(u4514,hypothesis,
sF81 = select(sF8,sF80) ).
cnf(u145,hypothesis,
i35 != i28 ).
cnf(u291,hypothesis,
i32 != i23 ).
cnf(u429,hypothesis,
i37 != i19 ).
cnf(u1183,hypothesis,
i11 != i6 ).
cnf(u929,hypothesis,
i12 != i10 ).
cnf(u1075,hypothesis,
i32 != i7 ).
cnf(u1441,hypothesis,
i24 != i2 ).
cnf(u1213,hypothesis,
i30 != i5 ).
cnf(u1445,hypothesis,
i22 != i2 ).
cnf(u943,hypothesis,
i35 != i9 ).
cnf(u4522,hypothesis,
sF81 = select(sF6,sF80) ).
cnf(u57,hypothesis,
i34 != i33 ).
cnf(u187,hypothesis,
i39 != i26 ).
cnf(u419,hypothesis,
i22 != i20 ).
cnf(u1846,axiom,
e20 = select(sF55,i20) ).
cnf(u573,hypothesis,
i31 != i16 ).
cnf(u1449,hypothesis,
i20 != i2 ).
cnf(u1852,axiom,
e9 = select(sF70,i9) ).
cnf(u1203,hypothesis,
i35 != i5 ).
cnf(u101,hypothesis,
i36 != i30 ).
cnf(u63,hypothesis,
i38 != i32 ).
cnf(u1850,axiom,
e14 = select(sF41,i14) ).
cnf(u1225,hypothesis,
i24 != i5 ).
cnf(u1387,hypothesis,
i14 != i3 ).
cnf(u4420,axiom,
e40 = select(sF74,sF80) ).
cnf(u701,hypothesis,
i16 != i14 ).
cnf(u455,hypothesis,
i24 != i19 ).
cnf(u841,hypothesis,
i27 != i11 ).
cnf(u4409,axiom,
sF66 = store(sF65,sF80,e40) ).
cnf(u699,hypothesis,
i17 != i14 ).
cnf(u1357,hypothesis,
i29 != i3 ).
cnf(u855,hypothesis,
i20 != i11 ).
cnf(u191,hypothesis,
i37 != i26 ).
cnf(u141,hypothesis,
i37 != i28 ).
cnf(u331,hypothesis,
i29 != i22 ).
cnf(u1251,hypothesis,
i11 != i5 ).
cnf(u1856,axiom,
e37 = select(sF36,i37) ).
cnf(u1223,hypothesis,
i25 != i5 ).
cnf(u1750,axiom,
e5 = select(sF4,i5) ).
cnf(u969,hypothesis,
i22 != i9 ).
cnf(u1287,hypothesis,
i28 != i4 ).
cnf(u1115,hypothesis,
i12 != i7 ).
cnf(u1347,hypothesis,
i34 != i3 ).
cnf(u1307,hypothesis,
i18 != i4 ).
cnf(u329,hypothesis,
i30 != i22 ).
cnf(u459,hypothesis,
i22 != i19 ).
cnf(u1886,axiom,
e1 = select(sF69,i1) ).
cnf(u613,hypothesis,
i35 != i15 ).
cnf(u1481,hypothesis,
i4 != i2 ).
cnf(u845,hypothesis,
i25 != i11 ).
cnf(u1367,hypothesis,
i24 != i3 ).
cnf(u1489,hypothesis,
i38 != i1 ).
cnf(u611,hypothesis,
i36 != i15 ).
cnf(u1612,axiom,
store(sF23,i25,e25) = sF24 ).
cnf(u843,hypothesis,
i26 != i11 ).
cnf(u1551,hypothesis,
i7 != i1 ).
cnf(u103,hypothesis,
i35 != i30 ).
cnf(u1735,axiom,
( select(a1,X0) = select(sF40,X0)
| i16 = X0 ) ).
cnf(u1610,axiom,
store(sF22,i24,e24) = sF23 ).
cnf(u457,hypothesis,
i23 != i19 ).
cnf(u741,hypothesis,
i22 != i13 ).
cnf(u973,hypothesis,
i20 != i9 ).
cnf(u1616,axiom,
store(sF25,i27,e27) = sF26 ).
cnf(u1495,hypothesis,
i35 != i1 ).
cnf(u817,hypothesis,
i39 != i11 ).
cnf(u739,hypothesis,
i23 != i13 ).
cnf(u4470,hypothesis,
sF81 = select(sF19,sF80) ).
cnf(u1740,axiom,
e29 = select(sF78,i29) ).
cnf(u971,hypothesis,
i21 != i9 ).
cnf(u1757,axiom,
( select(sF55,X0) = select(sF56,X0)
| i35 = X0 ) ).
cnf(u4382,hypothesis,
i27 != sF80 ).
cnf(u231,hypothesis,
i31 != i25 ).
cnf(u369,hypothesis,
i28 != i21 ).
cnf(u463,hypothesis,
i20 != i19 ).
cnf(u1738,axiom,
e2 = select(sF1,i2) ).
cnf(u601,hypothesis,
i17 != i16 ).
cnf(u1773,axiom,
( select(sF33,X0) = select(sF34,X0)
| i35 = X0 ) ).
cnf(u1755,axiom,
( select(sF71,X0) = select(sF72,X0)
| i5 = X0 ) ).
cnf(u1646,axiom,
store(sF40,i14,e14) = sF41 ).
cnf(u885,hypothesis,
i34 != i10 ).
cnf(u4426,axiom,
e40 = select(sF68,sF80) ).
cnf(u1407,hypothesis,
i4 != i3 ).
cnf(u4397,hypothesis,
i12 != sF80 ).
cnf(u1744,axiom,
e3 = select(sF2,i3) ).
cnf(u615,hypothesis,
i34 != i15 ).
cnf(u1791,axiom,
( select(sF57,X0) = select(sF58,X0)
| i26 = X0 ) ).
cnf(u1761,axiom,
( select(sF56,X0) = select(sF57,X0)
| i23 = X0 ) ).
cnf(u1652,axiom,
store(sF43,i25,e25) = sF44 ).
cnf(u883,hypothesis,
i35 != i10 ).
cnf(u1541,hypothesis,
i12 != i1 ).
cnf(u1829,axiom,
( select(sF61,X0) = select(sF62,X0)
| i22 = X0 ) ).
cnf(u229,hypothesis,
i32 != i25 ).
cnf(u1775,axiom,
( select(sF7,X0) = select(sF6,X0)
| i8 = X0 ) ).
cnf(u1650,axiom,
store(sF42,i11,e11) = sF43 ).
cnf(u497,hypothesis,
i24 != i18 ).
cnf(u1539,hypothesis,
i13 != i1 ).
cnf(u1121,hypothesis,
i9 != i7 ).
cnf(u761,hypothesis,
i39 != i12 ).
cnf(u1774,axiom,
e8 = select(sF7,i8) ).
cnf(u1013,hypothesis,
i31 != i8 ).
cnf(u1656,axiom,
store(sF45,i7,e7) = sF46 ).
cnf(u1535,hypothesis,
i15 != i1 ).
cnf(u743,hypothesis,
i21 != i13 ).
cnf(u4430,hypothesis,
sF81 = select(sF29,sF80) ).
cnf(u1780,axiom,
e21 = select(sF59,i21) ).
cnf(u1011,hypothesis,
i32 != i8 ).
cnf(u13,hypothesis,
i38 != i37 ).
cnf(u219,hypothesis,
i37 != i25 ).
cnf(u373,hypothesis,
i26 != i21 ).
cnf(u503,hypothesis,
i21 != i18 ).
cnf(u1778,axiom,
e17 = select(sF16,i17) ).
cnf(u513,hypothesis,
i38 != i17 ).
cnf(u1249,hypothesis,
i12 != i5 ).
cnf(u1029,hypothesis,
i23 != i8 ).
cnf(u1784,axiom,
e36 = select(sF35,i36) ).
cnf(u527,hypothesis,
i31 != i17 ).
cnf(u4421,axiom,
e40 = select(sF73,sF80) ).
cnf(u1564,axiom,
store(a1,i1,e1) = sF0 ).
cnf(u4466,hypothesis,
sF81 = select(sF20,sF80) ).
cnf(u1813,axiom,
( select(sF46,X0) = select(sF47,X0)
| i32 = X0 ) ).
cnf(u1393,hypothesis,
i11 != i3 ).
cnf(u287,hypothesis,
i34 != i23 ).
cnf(u501,hypothesis,
i22 != i18 ).
cnf(u1033,hypothesis,
i21 != i8 ).
cnf(u1811,axiom,
( select(sF17,X0) = select(sF18,X0)
| i19 = X0 ) ).
cnf(u1686,axiom,
store(sF60,i10,e10) = sF61 ).
cnf(u1157,hypothesis,
i24 != i6 ).
cnf(u655,hypothesis,
i39 != i14 ).
cnf(u1817,axiom,
( select(sF53,X0) = select(sF54,X0)
| i36 = X0 ) ).
cnf(u1379,hypothesis,
i18 != i3 ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u131,hypothesis,
i31 != i29 ).
cnf(u285,hypothesis,
i35 != i23 ).
cnf(u1831,axiom,
( select(sF26,X0) = select(sF27,X0)
| i28 = X0 ) ).
cnf(u553,hypothesis,
i18 != i17 ).
cnf(u1039,hypothesis,
i18 != i8 ).
cnf(u785,hypothesis,
i27 != i12 ).
cnf(u4407,hypothesis,
i2 != sF80 ).
cnf(u1069,hypothesis,
i35 != i7 ).
cnf(u1275,hypothesis,
i34 != i4 ).
cnf(u1301,hypothesis,
i21 != i4 ).
cnf(u799,hypothesis,
i20 != i12 ).
cnf(u43,hypothesis,
i35 != i34 ).
cnf(u129,hypothesis,
i32 != i29 ).
cnf(u4450,hypothesis,
sF81 = select(sF24,sF80) ).
cnf(u413,hypothesis,
i25 != i20 ).
cnf(u1419,hypothesis,
i35 != i2 ).
cnf(u1073,hypothesis,
i33 != i7 ).
cnf(u1167,hypothesis,
i19 != i6 ).
cnf(u913,hypothesis,
i20 != i10 ).
cnf(u1197,hypothesis,
i38 != i5 ).
cnf(u1429,hypothesis,
i30 != i2 ).
cnf(u927,hypothesis,
i13 != i10 ).
cnf(u41,hypothesis,
i36 != i34 ).
cnf(u171,hypothesis,
i34 != i27 ).
cnf(u403,hypothesis,
i30 != i20 ).
cnf(u1830,axiom,
e28 = select(sF27,i28) ).
cnf(u557,hypothesis,
i39 != i16 ).
cnf(u1079,hypothesis,
i30 != i7 ).
cnf(u825,hypothesis,
i35 != i11 ).
cnf(u1433,hypothesis,
i28 != i2 ).
cnf(u1836,axiom,
e32 = select(sF31,i32) ).
cnf(u1341,hypothesis,
i37 != i3 ).
cnf(u47,hypothesis,
i39 != i33 ).
cnf(u1834,axiom,
e27 = select(sF60,i27) ).
cnf(u169,hypothesis,
i35 != i27 ).
cnf(u4462,hypothesis,
sF81 = select(sF21,sF80) ).
cnf(u315,hypothesis,
i37 != i22 ).
cnf(u685,hypothesis,
i24 != i14 ).
cnf(u85,hypothesis,
i35 != i31 ).
cnf(u1207,hypothesis,
i33 != i5 ).
cnf(u953,hypothesis,
i30 != i9 ).
cnf(u125,hypothesis,
i34 != i29 ).
cnf(u683,hypothesis,
i25 != i14 ).
cnf(u4414,axiom,
e40 = select(sF79,sF80) ).
cnf(u1469,hypothesis,
i10 != i2 ).
cnf(u839,hypothesis,
i28 != i11 ).
cnf(u175,hypothesis,
i32 != i27 ).
cnf(u313,hypothesis,
i38 != i22 ).
cnf(u443,hypothesis,
i30 != i19 ).
cnf(u343,hypothesis,
i23 != i22 ).
cnf(u1345,hypothesis,
i35 != i3 ).
cnf(u1099,hypothesis,
i20 != i7 ).
cnf(u827,hypothesis,
i34 != i11 ).
cnf(u4542,hypothesis,
sF81 = select(sF1,sF80) ).
cnf(u4416,axiom,
e40 = select(sF78,sF80) ).
cnf(u1235,hypothesis,
i19 != i5 ).
cnf(u1443,hypothesis,
i23 != i2 ).
cnf(u1594,axiom,
store(sF14,i16,e16) = sF15 ).
cnf(u441,hypothesis,
i31 != i19 ).
cnf(u1870,axiom,
e22 = select(sF21,i22) ).
cnf(u597,hypothesis,
i19 != i16 ).
cnf(u957,hypothesis,
i28 != i9 ).
cnf(u1351,hypothesis,
i32 != i3 ).
cnf(u1473,hypothesis,
i8 != i2 ).
cnf(u1291,hypothesis,
i26 != i4 ).
cnf(u595,hypothesis,
i20 != i16 ).
cnf(u1724,axiom,
sk(sF39,sF79) = sF80 ).
cnf(u955,hypothesis,
i29 != i9 ).
cnf(u4422,axiom,
e40 = select(sF72,sF80) ).
cnf(u87,hypothesis,
i34 != i31 ).
cnf(u1874,axiom,
e7 = select(sF6,i7) ).
cnf(u1722,axiom,
store(sF78,i19,e19) = sF79 ).
cnf(u725,hypothesis,
i30 != i13 ).
cnf(u1880,axiom,
e38 = select(sF67,i38) ).
cnf(u1600,axiom,
store(sF17,i19,e19) = sF18 ).
cnf(u1479,hypothesis,
i5 != i2 ).
cnf(u1371,hypothesis,
i22 != i3 ).
cnf(u1523,hypothesis,
i21 != i1 ).
cnf(u4550,hypothesis,
sF81 = select(a1,sF80) ).
cnf(u1741,axiom,
( select(sF78,X0) = select(sF77,X0)
| i29 = X0 ) ).
cnf(u215,hypothesis,
i39 != i25 ).
cnf(u353,hypothesis,
i36 != i21 ).
cnf(u1081,hypothesis,
i29 != i7 ).
cnf(u585,hypothesis,
i25 != i16 ).
cnf(u1739,axiom,
( select(sF0,X0) = select(sF1,X0)
| i2 = X0 ) ).
cnf(u1630,axiom,
store(sF32,i34,e34) = sF33 ).
cnf(u869,hypothesis,
i13 != i11 ).
cnf(u1531,hypothesis,
i17 != i1 ).
cnf(u1391,hypothesis,
i12 != i3 ).
cnf(u599,hypothesis,
i18 != i16 ).
cnf(u1745,axiom,
( select(sF1,X0) = select(sF2,X0)
| i3 = X0 ) ).
cnf(u1636,axiom,
store(sF35,i37,e37) = sF36 ).
cnf(u867,hypothesis,
i14 != i11 ).
cnf(u359,hypothesis,
i33 != i21 ).
cnf(u1634,axiom,
store(sF34,i36,e36) = sF35 ).
cnf(u481,hypothesis,
i32 != i18 ).
cnf(u713,hypothesis,
i36 != i13 ).
cnf(u4510,hypothesis,
sF81 = select(sF9,sF80) ).
cnf(u1883,axiom,
( select(sF71,X0) = select(sF70,X0)
| i3 = X0 ) ).
cnf(u1758,axiom,
e26 = select(sF25,i26) ).
cnf(u997,hypothesis,
i39 != i8 ).
cnf(u1640,axiom,
store(sF37,i39,e39) = sF38 ).
cnf(u1519,hypothesis,
i23 != i1 ).
cnf(u727,hypothesis,
i29 != i13 ).
cnf(u1764,axiom,
e2 = select(sF65,i2) ).
cnf(u1781,axiom,
( select(sF58,X0) = select(sF59,X0)
| i21 = X0 ) ).
cnf(u203,hypothesis,
i31 != i26 ).
cnf(u357,hypothesis,
i34 != i21 ).
cnf(u487,hypothesis,
i29 != i18 ).
cnf(u1762,axiom,
e10 = select(sF9,i10) ).
cnf(u625,hypothesis,
i29 != i15 ).
cnf(u1779,axiom,
( select(sF15,X0) = select(sF16,X0)
| i17 = X0 ) ).
cnf(u1233,hypothesis,
i20 != i5 ).
cnf(u1141,hypothesis,
i32 != i6 ).
cnf(u1768,axiom,
e33 = select(sF32,i33) ).
cnf(u639,hypothesis,
i22 != i15 ).
cnf(u115,hypothesis,
i39 != i29 ).
cnf(u253,hypothesis,
i35 != i24 ).
cnf(u271,hypothesis,
i26 != i24 ).
cnf(u485,hypothesis,
i30 != i18 ).
cnf(u753,hypothesis,
i16 != i13 ).
cnf(u1795,axiom,
( select(sF48,X0) = select(sF49,X0)
| i18 = X0 ) ).
cnf(u1670,axiom,
store(sF52,i12,e12) = sF53 ).
cnf(u4383,hypothesis,
i26 != sF80 ).
cnf(u197,hypothesis,
i34 != i26 ).
cnf(u767,hypothesis,
i36 != i12 ).
cnf(u1377,hypothesis,
i19 != i3 ).
cnf(u1801,axiom,
( select(sF50,X0) = select(sF51,X0)
| i31 = X0 ) ).
cnf(u4378,hypothesis,
i31 != sF80 ).
cnf(u269,hypothesis,
i27 != i24 ).
cnf(u399,hypothesis,
i32 != i20 ).
cnf(u1151,hypothesis,
i27 != i6 ).
cnf(u769,hypothesis,
i35 != i12 ).
cnf(u1053,hypothesis,
i11 != i8 ).
cnf(u1259,hypothesis,
i7 != i5 ).
cnf(u1285,hypothesis,
i29 != i4 ).
cnf(u783,hypothesis,
i28 != i12 ).
cnf(u1840,axiom,
e20 = select(sF19,i20) ).
cnf(u1403,hypothesis,
i6 != i3 ).
cnf(u27,hypothesis,
i38 != i35 ).
cnf(u241,hypothesis,
i26 != i25 ).
cnf(u259,hypothesis,
i32 != i24 ).
cnf(u397,hypothesis,
i33 != i20 ).
cnf(u4412,axiom,
e40 = sF82 ).
cnf(u1057,hypothesis,
i9 != i8 ).
cnf(u1279,hypothesis,
i32 != i4 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u897,hypothesis,
i28 != i10 ).
cnf(u1043,hypothesis,
i16 != i8 ).
cnf(u1876,axiom,
e7 = select(sF46,i7) ).
cnf(u1181,hypothesis,
i12 != i6 ).
cnf(u1177,hypothesis,
i14 != i6 ).
cnf(u1413,hypothesis,
i38 != i2 ).
cnf(u911,hypothesis,
i21 != i10 ).
cnf(u4490,hypothesis,
sF81 = select(sF14,sF80) ).
cnf(u25,hypothesis,
i39 != i35 ).
cnf(u155,hypothesis,
i30 != i28 ).
cnf(u387,hypothesis,
i38 != i20 ).
cnf(u1814,axiom,
e28 = select(sF77,i28) ).
cnf(u541,hypothesis,
i24 != i17 ).
cnf(u1063,hypothesis,
i38 != i7 ).
cnf(u809,hypothesis,
i15 != i12 ).
cnf(u1417,hypothesis,
i36 != i2 ).
cnf(u1820,axiom,
e10 = select(sF61,i10) ).
cnf(u539,hypothesis,
i25 != i17 ).
cnf(u1325,hypothesis,
i9 != i4 ).
cnf(u823,hypothesis,
i36 != i11 ).
cnf(u31,hypothesis,
i36 != i35 ).
cnf(u1818,axiom,
e33 = select(sF64,i33) ).
cnf(u153,hypothesis,
i31 != i28 ).
cnf(u299,hypothesis,
i28 != i23 ).
cnf(u1153,hypothesis,
i26 != i6 ).
cnf(u1283,hypothesis,
i30 != i4 ).
cnf(u669,hypothesis,
i32 != i14 ).
cnf(u1824,axiom,
e12 = select(sF53,i12) ).
cnf(u1191,hypothesis,
i7 != i6 ).
cnf(u937,hypothesis,
i38 != i9 ).
cnf(u1083,hypothesis,
i28 != i7 ).
cnf(u1885,axiom,
( select(sF15,X0) = select(sF14,X0)
| i16 = X0 ) ).
cnf(u667,hypothesis,
i33 != i14 ).
cnf(u1453,hypothesis,
i18 != i2 ).
cnf(u951,hypothesis,
i31 != i9 ).
cnf(u297,hypothesis,
i29 != i23 ).
cnf(u427,hypothesis,
i38 != i19 ).
cnf(u1854,axiom,
e6 = select(sF5,i6) ).
cnf(u109,hypothesis,
i32 != i30 ).
cnf(u813,hypothesis,
i13 != i12 ).
cnf(u1457,hypothesis,
i16 != i2 ).
cnf(u1211,hypothesis,
i31 != i5 ).
cnf(u1369,hypothesis,
i23 != i3 ).
cnf(u811,hypothesis,
i14 != i12 ).
cnf(u1578,axiom,
store(sF6,i8,e8) = sF7 ).
cnf(u425,hypothesis,
i39 != i19 ).
cnf(u581,hypothesis,
i27 != i16 ).
cnf(u941,hypothesis,
i36 != i9 ).
cnf(u1584,axiom,
store(sF9,i11,e11) = sF10 ).
cnf(u1463,hypothesis,
i13 != i2 ).
cnf(u1860,axiom,
e4 = select(sF73,i4) ).
cnf(u579,hypothesis,
i28 != i16 ).
cnf(u1708,axiom,
store(sF71,i5,e5) = sF72 ).
cnf(u939,hypothesis,
i37 != i9 ).
cnf(u71,hypothesis,
i34 != i32 ).
cnf(u1858,axiom,
e30 = select(sF74,i30) ).
cnf(u1706,axiom,
store(sF70,i3,e3) = sF71 ).
cnf(u1299,hypothesis,
i22 != i4 ).
cnf(u709,hypothesis,
i38 != i13 ).
cnf(u1864,axiom,
e23 = select(sF22,i23) ).
cnf(u1712,axiom,
store(sF73,i30,e30) = sF74 ).
cnf(u1355,hypothesis,
i30 != i3 ).
cnf(u4438,hypothesis,
sF81 = select(sF27,sF80) ).
cnf(u69,hypothesis,
i35 != i32 ).
cnf(u199,hypothesis,
i33 != i26 ).
cnf(u337,hypothesis,
i26 != i22 ).
cnf(u1507,hypothesis,
i29 != i1 ).
cnf(u697,hypothesis,
i18 != i14 ).
cnf(u1614,axiom,
store(sF24,i26,e26) = sF25 ).
cnf(u853,hypothesis,
i21 != i11 ).
cnf(u1375,hypothesis,
i20 != i3 ).
cnf(u583,hypothesis,
i26 != i16 ).
cnf(u1620,axiom,
store(sF27,i29,e29) = sF28 ).
cnf(u851,hypothesis,
i22 != i11 ).
cnf(u1475,hypothesis,
i7 != i2 ).
cnf(u1869,axiom,
( select(sF75,X0) = select(sF74,X0)
| i15 = X0 ) ).
cnf(u1743,axiom,
( select(sF7,X0) = select(sF8,X0)
| i9 = X0 ) ).
cnf(u1618,axiom,
store(sF26,i28,e28) = sF27 ).
cnf(u1089,hypothesis,
i25 != i7 ).
cnf(u1867,axiom,
( select(sF13,X0) = select(sF14,X0)
| i15 = X0 ) ).
cnf(u1742,axiom,
e9 = select(sF8,i9) ).
cnf(u981,hypothesis,
i16 != i9 ).
cnf(u1624,axiom,
store(sF29,i31,e31) = sF30 ).
cnf(u1503,hypothesis,
i31 != i1 ).
cnf(u711,hypothesis,
i37 != i13 ).
cnf(u1873,axiom,
( select(sF48,X0) = select(sF47,X0)
| i6 = X0 ) ).
cnf(u1748,axiom,
e34 = select(sF76,i34) ).
cnf(u979,hypothesis,
i17 != i9 ).
cnf(u1765,axiom,
( select(sF64,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u1759,axiom,
( select(sF24,X0) = select(sF25,X0)
| i26 = X0 ) ).
cnf(u341,hypothesis,
i24 != i22 ).
cnf(u471,hypothesis,
i37 != i18 ).
cnf(u1746,axiom,
e25 = select(sF24,i25) ).
cnf(u609,hypothesis,
i37 != i15 ).
cnf(u1797,axiom,
( select(sF29,X0) = select(sF30,X0)
| i31 = X0 ) ).
cnf(u1217,hypothesis,
i28 != i5 ).
cnf(u1752,axiom,
e24 = select(sF23,i24) ).
cnf(u623,hypothesis,
i30 != i15 ).
cnf(u1815,axiom,
( select(sF77,X0) = select(sF76,X0)
| i28 = X0 ) ).
cnf(u1660,axiom,
store(sF47,i6,e6) = sF48 ).
cnf(u4434,hypothesis,
sF81 = select(sF28,sF80) ).
cnf(u99,hypothesis,
i37 != i30 ).
cnf(u4518,hypothesis,
sF81 = select(sF7,sF80) ).
cnf(u237,hypothesis,
i28 != i25 ).
cnf(u1321,hypothesis,
i11 != i4 ).
cnf(u469,hypothesis,
i38 != i18 ).
cnf(u181,hypothesis,
i29 != i27 ).
cnf(u737,hypothesis,
i24 != i13 ).
cnf(u1782,axiom,
e29 = select(sF28,i29) ).
cnf(u1253,hypothesis,
i10 != i5 ).
cnf(u751,hypothesis,
i17 != i13 ).
cnf(u4411,axiom,
( select(sF65,X0) = select(sF66,X0)
| sF80 = X0 ) ).
cnf(u983,hypothesis,
i15 != i9 ).
cnf(u97,hypothesis,
i38 != i30 ).
cnf(u227,hypothesis,
i33 != i25 ).
cnf(u381,hypothesis,
i22 != i21 ).
cnf(u1799,axiom,
( select(sF44,X0) = select(sF45,X0)
| i17 = X0 ) ).
cnf(u1135,hypothesis,
i35 != i6 ).
cnf(u881,hypothesis,
i36 != i10 ).
cnf(u1361,hypothesis,
i27 != i3 ).
cnf(u4526,hypothesis,
sF81 = select(sF5,sF80) ).
cnf(u4399,hypothesis,
i10 != sF80 ).
cnf(u1037,hypothesis,
i19 != i8 ).
cnf(u1243,hypothesis,
i15 != i5 ).
cnf(u4446,hypothesis,
sF81 = select(sF25,sF80) ).
cnf(u1397,hypothesis,
i9 != i3 ).
cnf(u895,hypothesis,
i29 != i10 ).
cnf(u11,hypothesis,
i39 != i37 ).
cnf(u225,hypothesis,
i34 != i25 ).
cnf(u371,hypothesis,
i27 != i21 ).
cnf(u1041,hypothesis,
i17 != i8 ).
cnf(u1009,hypothesis,
i33 != i8 ).
cnf(u4398,hypothesis,
i11 != sF80 ).
cnf(u1027,hypothesis,
i24 != i8 ).
cnf(u1165,hypothesis,
i20 != i6 ).
cnf(u1525,hypothesis,
i20 != i1 ).
cnf(u1023,hypothesis,
i26 != i8 ).
cnf(u139,hypothesis,
i38 != i28 ).
cnf(u499,hypothesis,
i23 != i18 ).
cnf(u1798,axiom,
e17 = select(sF45,i17) ).
cnf(u525,hypothesis,
i32 != i17 ).
cnf(u1047,hypothesis,
i14 != i8 ).
cnf(u793,hypothesis,
i23 != i12 ).
cnf(u1529,hypothesis,
i18 != i1 ).
cnf(u1804,axiom,
e25 = select(sF44,i25) ).
cnf(u523,hypothesis,
i33 != i17 ).
cnf(u1309,hypothesis,
i17 != i4 ).
cnf(u807,hypothesis,
i16 != i12 ).
cnf(u4506,hypothesis,
sF81 = select(sF10,sF80) ).
cnf(u1802,axiom,
e18 = select(sF17,i18) ).
cnf(u137,hypothesis,
i39 != i28 ).
cnf(u283,hypothesis,
i36 != i23 ).
cnf(u1281,hypothesis,
i31 != i4 ).
cnf(u1808,axiom,
e21 = select(sF20,i21) ).
cnf(u1175,hypothesis,
i15 != i6 ).
cnf(u921,hypothesis,
i16 != i10 ).
cnf(u1067,hypothesis,
i36 != i7 ).
cnf(u1545,hypothesis,
i10 != i1 ).
cnf(u651,hypothesis,
i16 != i15 ).
cnf(u1437,hypothesis,
i26 != i2 ).
cnf(u4384,hypothesis,
i25 != sF80 ).
cnf(u935,hypothesis,
i39 != i9 ).
cnf(u49,hypothesis,
i38 != i33 ).
cnf(u143,hypothesis,
i36 != i28 ).
cnf(u281,hypothesis,
i37 != i23 ).
cnf(u411,hypothesis,
i26 != i20 ).
cnf(u1838,axiom,
e13 = select(sF52,i13) ).
cnf(u565,hypothesis,
i35 != i16 ).
cnf(u797,hypothesis,
i21 != i12 ).
cnf(u1319,hypothesis,
i12 != i4 ).
cnf(u507,hypothesis,
i19 != i18 ).
cnf(u1844,axiom,
e14 = select(sF13,i14) ).
cnf(u563,hypothesis,
i36 != i16 ).
cnf(u1887,axiom,
( select(sF68,X0) = select(sF69,X0)
| i1 = X0 ) ).
cnf(u795,hypothesis,
i22 != i12 ).
cnf(u4423,axiom,
e40 = select(sF71,sF80) ).
cnf(u55,hypothesis,
i35 != i33 ).
cnf(u1842,axiom,
e30 = select(sF29,i30) ).
cnf(u409,hypothesis,
i27 != i20 ).
cnf(u693,hypothesis,
i20 != i14 ).
cnf(u1848,axiom,
e8 = select(sF63,i8) ).
cnf(u925,hypothesis,
i14 != i10 ).
cnf(u1568,axiom,
store(sF1,i3,e3) = sF2 ).
cnf(u1447,hypothesis,
i21 != i2 ).
cnf(u4401,hypothesis,
i8 != sF80 ).
cnf(u691,hypothesis,
i21 != i14 ).
cnf(u1692,axiom,
store(sF63,i33,e33) = sF64 ).
cnf(u923,hypothesis,
i15 != i10 ).
cnf(u53,hypothesis,
i36 != i33 ).
cnf(u183,hypothesis,
i28 != i27 ).
cnf(u1353,hypothesis,
i31 != i3 ).
cnf(u1690,axiom,
store(sF62,i8,e8) = sF63 ).
cnf(u1598,axiom,
store(sF16,i18,e18) = sF17 ).
cnf(u567,hypothesis,
i34 != i16 ).
cnf(u1467,hypothesis,
i11 != i2 ).
cnf(u77,hypothesis,
i39 != i31 ).
cnf(u4474,hypothesis,
sF81 = select(sF18,sF80) ).
cnf(u1853,axiom,
( select(sF69,X0) = select(sF70,X0)
| i9 = X0 ) ).
cnf(u4498,hypothesis,
sF81 = select(sF12,sF80) ).
cnf(u321,hypothesis,
i34 != i22 ).
cnf(u681,hypothesis,
i26 != i14 ).
cnf(u1851,axiom,
( select(sF40,X0) = select(sF41,X0)
| i14 = X0 ) ).
cnf(u1726,axiom,
select(sF39,sF80) = sF81 ).
cnf(u837,hypothesis,
i29 != i11 ).
cnf(u1459,hypothesis,
i15 != i2 ).
cnf(u1359,hypothesis,
i28 != i3 ).
cnf(u695,hypothesis,
i19 != i14 ).
cnf(u987,hypothesis,
i13 != i9 ).
cnf(u1604,axiom,
store(sF19,i21,e21) = sF20 ).
cnf(u835,hypothesis,
i30 != i11 ).
cnf(u4419,axiom,
e40 = select(sF75,sF80) ).
cnf(u327,hypothesis,
i31 != i22 ).
cnf(u1602,axiom,
store(sF18,i20,e20) = sF19 ).
cnf(u449,hypothesis,
i27 != i19 ).
cnf(u1201,hypothesis,
i36 != i5 ).
cnf(u965,hypothesis,
i24 != i9 ).
cnf(u1608,axiom,
store(sF21,i23,e23) = sF22 ).
cnf(u1857,axiom,
( select(sF35,X0) = select(sF36,X0)
| i37 = X0 ) ).
cnf(u1732,axiom,
e1 = select(sF0,i1) ).
cnf(u963,hypothesis,
i25 != i9 ).
cnf(u4538,hypothesis,
sF81 = select(sF2,sF80) ).
cnf(u1749,axiom,
( select(sF75,X0) = select(sF76,X0)
| i34 = X0 ) ).
cnf(u325,hypothesis,
i32 != i22 ).
cnf(u1871,axiom,
( select(sF20,X0) = select(sF21,X0)
| i22 = X0 ) ).
cnf(u1730,axiom,
e19 = select(sF79,i19) ).
cnf(u593,hypothesis,
i21 != i16 ).
cnf(u1638,axiom,
store(sF36,i38,e38) = sF37 ).
cnf(u1109,hypothesis,
i15 != i7 ).
cnf(u1736,axiom,
e1 = select(sF39,i1) ).
cnf(u607,hypothesis,
i38 != i15 ).
cnf(u1644,axiom,
store(a1,i16,e16) = sF40 ).
cnf(u83,hypothesis,
i36 != i31 ).
cnf(u221,hypothesis,
i36 != i25 ).
cnf(u367,hypothesis,
i29 != i21 ).
cnf(u453,hypothesis,
i25 != i19 ).
cnf(u721,hypothesis,
i32 != i13 ).
cnf(u1265,hypothesis,
i39 != i4 ).
cnf(u1237,hypothesis,
i18 != i5 ).
cnf(u735,hypothesis,
i25 != i13 ).
cnf(u1305,hypothesis,
i19 != i4 ).
cnf(u967,hypothesis,
i23 != i9 ).
cnf(u4393,hypothesis,
i16 != sF80 ).
cnf(u81,hypothesis,
i37 != i31 ).
cnf(u211,hypothesis,
i27 != i26 ).
cnf(u365,hypothesis,
i30 != i21 ).
cnf(u643,hypothesis,
i20 != i15 ).
cnf(u1119,hypothesis,
i10 != i7 ).
cnf(u865,hypothesis,
i15 != i11 ).
cnf(u1149,hypothesis,
i28 != i6 ).
cnf(u1227,hypothesis,
i23 != i5 ).
cnf(u1381,hypothesis,
i17 != i3 ).
cnf(u879,hypothesis,
i37 != i10 ).
cnf(u4458,hypothesis,
sF81 = select(sF22,sF80) ).
cnf(u1331,hypothesis,
i6 != i4 ).
cnf(u123,hypothesis,
i35 != i29 ).
cnf(u209,hypothesis,
i28 != i26 ).
cnf(u4396,hypothesis,
i13 != sF80 ).
cnf(u355,hypothesis,
i35 != i21 ).
cnf(u493,hypothesis,
i26 != i18 ).
cnf(u1247,hypothesis,
i13 != i5 ).
cnf(u993,hypothesis,
i10 != i9 ).
cnf(u1139,hypothesis,
i33 != i6 ).
cnf(u1277,hypothesis,
i33 != i4 ).
cnf(u723,hypothesis,
i31 != i13 ).
cnf(u1509,hypothesis,
i28 != i1 ).
cnf(u1007,hypothesis,
i34 != i8 ).
cnf(u121,hypothesis,
i36 != i29 ).
cnf(u251,hypothesis,
i36 != i24 ).
cnf(u483,hypothesis,
i31 != i18 ).
cnf(u637,hypothesis,
i23 != i15 ).
cnf(u1031,hypothesis,
i22 != i8 ).
cnf(u4385,hypothesis,
i24 != sF80 ).
cnf(u777,hypothesis,
i31 != i12 ).
cnf(u1513,hypothesis,
i26 != i1 ).
cnf(u673,hypothesis,
i30 != i14 ).
cnf(u635,hypothesis,
i24 != i15 ).
cnf(u1293,hypothesis,
i25 != i4 ).
cnf(u791,hypothesis,
i24 != i12 ).
cnf(u127,hypothesis,
i33 != i29 ).
cnf(u249,hypothesis,
i37 != i24 ).
cnf(u267,hypothesis,
i28 != i24 ).
cnf(u765,hypothesis,
i37 != i12 ).
cnf(u1792,axiom,
e34 = select(sF33,i34) ).
cnf(u1159,hypothesis,
i23 != i6 ).
cnf(u905,hypothesis,
i24 != i10 ).
cnf(u1051,hypothesis,
i12 != i8 ).
cnf(u763,hypothesis,
i38 != i12 ).
cnf(u1421,hypothesis,
i34 != i2 ).
cnf(u1654,axiom,
store(sF44,i17,e17) = sF45 ).
cnf(u919,hypothesis,
i17 != i10 ).
cnf(u255,hypothesis,
i34 != i24 ).
cnf(u265,hypothesis,
i29 != i24 ).
cnf(u395,hypothesis,
i34 != i20 ).
cnf(u1822,axiom,
e39 = select(sF38,i39) ).
cnf(u549,hypothesis,
i20 != i17 ).
cnf(u781,hypothesis,
i29 != i12 ).
cnf(u1303,hypothesis,
i20 != i4 ).
cnf(u1425,hypothesis,
i32 != i2 ).
cnf(u1828,axiom,
e22 = select(sF62,i22) ).
cnf(u547,hypothesis,
i21 != i17 ).
cnf(u1785,axiom,
( select(sF34,X0) = select(sF35,X0)
| i36 = X0 ) ).
cnf(u779,hypothesis,
i30 != i12 ).
cnf(u4377,hypothesis,
i32 != sF80 ).
cnf(u1161,hypothesis,
i22 != i6 ).
cnf(u39,hypothesis,
i37 != i34 ).
cnf(u1826,axiom,
e39 = select(sF68,i39) ).
cnf(u393,hypothesis,
i35 != i20 ).
cnf(u677,hypothesis,
i28 != i14 ).
cnf(u1832,axiom,
e12 = select(sF11,i12) ).
cnf(u909,hypothesis,
i22 != i10 ).
cnf(u1431,hypothesis,
i29 != i2 ).
cnf(u675,hypothesis,
i29 != i14 ).
cnf(u1676,axiom,
store(sF55,i35,e35) = sF56 ).
cnf(u907,hypothesis,
i23 != i10 ).
cnf(u37,hypothesis,
i38 != i34 ).
cnf(u1187,hypothesis,
i9 != i6 ).
cnf(u167,hypothesis,
i36 != i27 ).
cnf(u305,hypothesis,
i25 != i23 ).
cnf(u1674,axiom,
store(sF54,i20,e20) = sF55 ).
cnf(u537,hypothesis,
i26 != i17 ).
cnf(u1582,axiom,
store(sF8,i10,e10) = sF9 ).
cnf(u821,hypothesis,
i37 != i11 ).
cnf(u1343,hypothesis,
i36 != i3 ).
cnf(u1680,axiom,
store(sF57,i26,e26) = sF58 ).
cnf(u551,hypothesis,
i19 != i17 ).
cnf(u1588,axiom,
store(sF11,i13,e13) = sF12 ).
cnf(u819,hypothesis,
i38 != i11 ).
cnf(u4534,hypothesis,
sF81 = select(sF3,sF80) ).
cnf(u1363,hypothesis,
i26 != i3 ).
cnf(u165,hypothesis,
i37 != i27 ).
cnf(u311,hypothesis,
i39 != i22 ).
cnf(u1586,axiom,
store(sF10,i12,e12) = sF11 ).
cnf(u433,hypothesis,
i35 != i19 ).
cnf(u665,hypothesis,
i34 != i14 ).
cnf(u1835,axiom,
( select(sF59,X0) = select(sF60,X0)
| i27 = X0 ) ).
cnf(u1710,axiom,
store(sF72,i4,e4) = sF73 ).
cnf(u949,hypothesis,
i32 != i9 ).
cnf(u1592,axiom,
store(sF13,i15,e15) = sF14 ).
cnf(u1471,hypothesis,
i9 != i2 ).
cnf(u4417,axiom,
e40 = select(sF77,sF80) ).
cnf(u679,hypothesis,
i27 != i14 ).
cnf(u1841,axiom,
( select(sF19,X0) = select(sF18,X0)
| i20 = X0 ) ).
cnf(u1716,axiom,
store(sF75,i34,e34) = sF76 ).
cnf(u947,hypothesis,
i33 != i9 ).
cnf(u1435,hypothesis,
i27 != i2 ).
cnf(u439,hypothesis,
i32 != i19 ).
cnf(u1714,axiom,
store(sF74,i15,e15) = sF75 ).
cnf(u1185,hypothesis,
i10 != i6 ).
cnf(u1515,hypothesis,
i25 != i1 ).
cnf(u1720,axiom,
store(sF77,i29,e29) = sF78 ).
cnf(u4402,hypothesis,
i7 != sF80 ).
cnf(u1733,axiom,
( select(a1,X0) = select(sF0,X0)
| i1 = X0 ) ).
cnf(u437,hypothesis,
i33 != i19 ).
cnf(u577,hypothesis,
i29 != i16 ).
cnf(u1622,axiom,
store(sF28,i30,e30) = sF29 ).
cnf(u1483,hypothesis,
i3 != i2 ).
cnf(u1093,hypothesis,
i23 != i7 ).
cnf(u591,hypothesis,
i22 != i16 ).
cnf(u1628,axiom,
store(sF31,i33,e33) = sF32 ).
cnf(u4530,hypothesis,
sF81 = select(sF4,sF80) ).
cnf(u67,hypothesis,
i36 != i32 ).
cnf(u205,hypothesis,
i30 != i26 ).
cnf(u351,hypothesis,
i37 != i21 ).
cnf(u1097,hypothesis,
i21 != i7 ).
cnf(u1875,axiom,
( select(sF6,X0) = select(sF5,X0)
| i7 = X0 ) ).
cnf(u1269,hypothesis,
i37 != i4 ).
cnf(u587,hypothesis,
i24 != i16 ).
cnf(u1221,hypothesis,
i26 != i5 ).
cnf(u719,hypothesis,
i33 != i13 ).
cnf(u1881,axiom,
( select(sF67,X0) = select(sF66,X0)
| i38 = X0 ) ).
cnf(u65,hypothesis,
i37 != i32 ).
cnf(u195,hypothesis,
i35 != i26 ).
cnf(u1273,hypothesis,
i35 != i4 ).
cnf(u349,hypothesis,
i38 != i21 ).
cnf(u1103,hypothesis,
i18 != i7 ).
cnf(u849,hypothesis,
i23 != i11 ).
cnf(u1289,hypothesis,
i27 != i4 ).
cnf(u1133,hypothesis,
i36 != i6 ).
cnf(u1365,hypothesis,
i25 != i3 ).
cnf(u1329,hypothesis,
i7 != i4 ).
cnf(u863,hypothesis,
i16 != i11 ).
cnf(u107,hypothesis,
i33 != i30 ).
cnf(u193,hypothesis,
i36 != i26 ).
cnf(u339,hypothesis,
i25 != i22 ).
cnf(u477,hypothesis,
i34 != i18 ).
cnf(u1231,hypothesis,
i21 != i5 ).
cnf(u977,hypothesis,
i18 != i9 ).
cnf(u1123,hypothesis,
i8 != i7 ).
cnf(u1261,hypothesis,
i6 != i5 ).
cnf(u707,hypothesis,
i39 != i13 ).
cnf(u407,hypothesis,
i28 != i20 ).
cnf(u991,hypothesis,
i11 != i9 ).
cnf(u105,hypothesis,
i34 != i30 ).
cnf(u235,hypothesis,
i29 != i25 ).
cnf(u467,hypothesis,
i39 != i18 ).
cnf(u621,hypothesis,
i31 != i15 ).
cnf(u1143,hypothesis,
i31 != i6 ).
cnf(u889,hypothesis,
i32 != i10 ).
cnf(u1559,hypothesis,
i3 != i1 ).
cnf(u1497,hypothesis,
i34 != i1 ).
cnf(u619,hypothesis,
i32 != i15 ).
cnf(u1405,hypothesis,
i5 != i3 ).
cnf(u775,hypothesis,
i32 != i12 ).
cnf(u4494,hypothesis,
sF81 = select(sF13,sF80) ).
cnf(u111,hypothesis,
i31 != i30 ).
cnf(u233,hypothesis,
i30 != i25 ).
cnf(u379,hypothesis,
i23 != i21 ).
cnf(u657,hypothesis,
i38 != i14 ).
cnf(u749,hypothesis,
i18 != i13 ).
cnf(u1271,hypothesis,
i36 != i4 ).
cnf(u1017,hypothesis,
i29 != i8 ).
cnf(u1035,hypothesis,
i20 != i8 ).
cnf(u747,hypothesis,
i19 != i13 ).
cnf(u4478,hypothesis,
sF81 = select(sF17,sF80) ).
cnf(u1533,hypothesis,
i16 != i1 ).
cnf(u903,hypothesis,
i25 != i10 ).
cnf(u239,hypothesis,
i27 != i25 ).
cnf(u377,hypothesis,
i24 != i21 ).
cnf(u1105,hypothesis,
i17 != i7 ).
cnf(u1806,axiom,
e11 = select(sF43,i11) ).
cnf(u533,hypothesis,
i28 != i17 ).
cnf(u1763,axiom,
( select(sF8,X0) = select(sF9,X0)
| i10 = X0 ) ).
cnf(u893,hypothesis,
i30 != i10 ).
cnf(u1145,hypothesis,
i30 != i6 ).
cnf(u1837,axiom,
( select(sF31,X0) = select(sF30,X0)
| i32 = X0 ) ).
cnf(u531,hypothesis,
i29 != i17 ).
cnf(u1769,axiom,
( select(sF31,X0) = select(sF32,X0)
| i33 = X0 ) ).
cnf(u891,hypothesis,
i31 != i10 ).
cnf(u1549,hypothesis,
i8 != i1 ).
cnf(u1855,axiom,
( select(sF4,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u1783,axiom,
( select(sF27,X0) = select(sF28,X0)
| i29 = X0 ) ).
cnf(u1658,axiom,
store(sF46,i32,e32) = sF47 ).
cnf(u505,hypothesis,
i20 != i18 ).
cnf(u4391,hypothesis,
i18 != sF80 ).
cnf(u1385,hypothesis,
i15 != i3 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV502-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n014.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 11:21:31 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.28 Running first-order theorem proving
% 0.09/0.28 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
% 13.90/2.84 % (1718540)Input is clausal, will run a generic CNF schedule.
% 13.90/2.84 % (1718568)lrs+10_1_sil=8000:sp=occurrence:random_seed=4024043371:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.90/2.84 % (1718568)Instruction limit reached!
% 13.90/2.84 % (1718568)------------------------------
% 13.90/2.84 % (1718568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.90/2.84 % (1718568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.84 % (1718568)CaDiCaL version: 2.1.3
% 13.90/2.84 % (1718568)Termination reason: Instruction limit
% 13.90/2.84 % (1718568)Termination phase: Saturation
% 13.90/2.84 % (1718568)Time elapsed: 0.036 s
% 13.90/2.84 % (1718568)Peak memory usage: 89 MB
% 13.90/2.84 % (1718568)Instructions burned: 108 (million)
% 13.90/2.84 % (1718569)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1602710337:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.90/2.84 % (1718566)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3556874565:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.90/2.84 % (1718565)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=2849166694:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.90/2.84 % (1718567)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1436086115:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.90/2.84 % (1718571)dis-21_1_sil=8000:lcm=predicate:random_seed=2917305026: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)
% 13.90/2.84 % (1718570)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2106637091:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.90/2.84 % (1718571)Refutation not found, incomplete strategy
% 13.90/2.84 % (1718571)------------------------------
% 13.90/2.84 % (1718571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.90/2.84 % (1718571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.84 % (1718571)CaDiCaL version: 2.1.3
% 13.90/2.84 % (1718571)Termination reason: Refutation not found, incomplete strategy
% 13.90/2.84 % (1718571)Time elapsed: 0.033 s
% 13.90/2.84 % (1718571)Peak memory usage: 89 MB
% 13.90/2.84 % (1718571)Instructions burned: 42 (million)
% 13.90/2.84 % (1718569)Instruction limit reached!
% 13.90/2.84 % (1718569)------------------------------
% 13.90/2.84 % (1718569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.90/2.84 % (1718569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.84 % (1718569)CaDiCaL version: 2.1.3
% 13.90/2.84 % (1718569)Termination reason: Instruction limit
% 13.90/2.84 % (1718569)Termination phase: Saturation
% 13.90/2.84 % (1718569)Time elapsed: 0.091 s
% 13.90/2.84 % (1718569)Peak memory usage: 89 MB
% 13.90/2.84 % (1718569)Instructions burned: 114 (million)
% 13.90/2.84 % (1718576)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=1165522162:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 13.90/2.84 % (1718570)Instruction limit reached!
% 13.90/2.84 % (1718570)------------------------------
% 13.90/2.84 % (1718570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.90/2.84 % (1718570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.84 % (1718570)CaDiCaL version: 2.1.3
% 13.90/2.84 % (1718570)Termination reason: Instruction limit
% 13.90/2.84 % (1718570)Termination phase: Saturation
% 13.90/2.84 % (1718570)Time elapsed: 0.140 s
% 13.90/2.84 % (1718570)Peak memory usage: 89 MB
% 13.90/2.84 % (1718570)Instructions burned: 180 (million)
% 13.90/2.84 % (1718576)Instruction limit reached!
% 13.90/2.84 % (1718576)------------------------------
% 13.90/2.84 % (1718576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.90/2.84 % (1718576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.84 % (1718576)CaDiCaL version: 2.1.3
% 13.90/2.84 % (1718576)Termination reason: Instruction limit
% 13.90/2.84 % (1718576)Termination phase: Saturation
% 13.90/2.84 % (1718576)Time elapsed: 0.051 s
% 13.90/2.84 % (1718576)Peak memory usage: 89 MB
% 13.90/2.84 % (1718576)Instructions burned: 146 (million)
% 13.90/2.84 % (1718585)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3868173921:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 18.56/3.59 % (1718588)lrs+10_64_to=lpo:sil=8000:random_seed=3836575657:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.56/3.59 % (1718588)Instruction limit reached!
% 18.56/3.59 % (1718588)------------------------------
% 18.56/3.59 % (1718588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.59 % (1718588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.59 % (1718588)CaDiCaL version: 2.1.3
% 18.56/3.59 % (1718588)Termination reason: Instruction limit
% 18.56/3.59 % (1718588)Termination phase: Saturation
% 18.56/3.59 % (1718588)Time elapsed: 0.051 s
% 18.56/3.59 % (1718588)Peak memory usage: 89 MB
% 18.56/3.59 % (1718588)Instructions burned: 129 (million)
% 18.56/3.59 % (1718587)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1653506226:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 18.56/3.59 % (1718571)------------------------------
% 18.56/3.59 % (1718571)------------------------------
% 18.56/3.59 % (1718585)Instruction limit reached!
% 18.56/3.59 % (1718585)------------------------------
% 18.56/3.59 % (1718585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.59 % (1718585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.59 % (1718585)CaDiCaL version: 2.1.3
% 18.56/3.59 % (1718585)Termination reason: Instruction limit
% 18.56/3.59 % (1718585)Termination phase: Saturation
% 18.56/3.59 % (1718585)Time elapsed: 0.194 s
% 18.56/3.59 % (1718585)Peak memory usage: 91 MB
% 18.56/3.59 % (1718585)Instructions burned: 190 (million)
% 18.56/3.59 % (1718587)Instruction limit reached!
% 18.56/3.59 % (1718587)------------------------------
% 18.56/3.59 % (1718587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.59 % (1718587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.59 % (1718587)CaDiCaL version: 2.1.3
% 18.56/3.59 % (1718587)Termination reason: Instruction limit
% 18.56/3.59 % (1718587)Termination phase: Saturation
% 18.56/3.59 % (1718587)Time elapsed: 0.162 s
% 18.56/3.59 % (1718587)Peak memory usage: 89 MB
% 18.56/3.59 % (1718587)Instructions burned: 219 (million)
% 18.56/3.59 % (1718596)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1629392078:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 18.56/3.59 % (1718594)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2930550561:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 18.56/3.59 % (1718596)Instruction limit reached!
% 18.56/3.59 % (1718596)------------------------------
% 18.56/3.59 % (1718596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.59 % (1718596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.59 % (1718596)CaDiCaL version: 2.1.3
% 18.56/3.59 % (1718596)Termination reason: Instruction limit
% 18.56/3.59 % (1718596)Termination phase: Saturation
% 18.56/3.59 % (1718596)Time elapsed: 0.066 s
% 18.56/3.59 % (1718596)Peak memory usage: 91 MB
% 18.56/3.59 % (1718596)Instructions burned: 158 (million)
% 18.56/3.59 % (1718598)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1292101342:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 18.56/3.59 % (1718594)Instruction limit reached!
% 18.56/3.59 % (1718594)------------------------------
% 18.56/3.59 % (1718594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.56/3.59 % (1718594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.56/3.59 % (1718594)CaDiCaL version: 2.1.3
% 18.56/3.59 % (1718594)Termination reason: Instruction limit
% 18.56/3.59 % (1718594)Termination phase: Saturation
% 18.56/3.59 % (1718594)Time elapsed: 0.120 s
% 18.56/3.59 % (1718594)Peak memory usage: 89 MB
% 18.56/3.59 % (1718594)Instructions burned: 194 (million)
% 18.56/3.59 % (1718599)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=381122058:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 18.56/3.59 % (1718603)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=244015736:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 18.56/3.59 % (1718603)Instruction limit reached!
% 18.56/3.59 % (1718603)------------------------------
% 24.76/4.37 % (1718603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718603)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718603)Termination reason: Instruction limit
% 24.76/4.37 % (1718603)Termination phase: Saturation
% 24.76/4.37 % (1718603)Time elapsed: 0.035 s
% 24.76/4.37 % (1718603)Peak memory usage: 88 MB
% 24.76/4.37 % (1718603)Instructions burned: 109 (million)
% 24.76/4.37 % (1718599)Instruction limit reached!
% 24.76/4.37 % (1718599)------------------------------
% 24.76/4.37 % (1718599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718599)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718599)Termination reason: Instruction limit
% 24.76/4.37 % (1718599)Termination phase: Saturation
% 24.76/4.37 % (1718599)Time elapsed: 0.107 s
% 24.76/4.37 % (1718599)Peak memory usage: 89 MB
% 24.76/4.37 % (1718599)Instructions burned: 106 (million)
% 24.76/4.37 % (1718606)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3213699285:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 24.76/4.37 % (1718610)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1004980563:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 24.76/4.37 % (1718612)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1956199959:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 24.76/4.37 % (1718606)Instruction limit reached!
% 24.76/4.37 % (1718606)------------------------------
% 24.76/4.37 % (1718606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718606)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718606)Termination reason: Instruction limit
% 24.76/4.37 % (1718606)Termination phase: Saturation
% 24.76/4.37 % (1718606)Time elapsed: 0.188 s
% 24.76/4.37 % (1718606)Peak memory usage: 89 MB
% 24.76/4.37 % (1718606)Instructions burned: 242 (million)
% 24.76/4.37 % (1718612)Instruction limit reached!
% 24.76/4.37 % (1718612)------------------------------
% 24.76/4.37 % (1718612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718612)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718612)Termination reason: Instruction limit
% 24.76/4.37 % (1718612)Termination phase: Saturation
% 24.76/4.37 % (1718612)Time elapsed: 0.101 s
% 24.76/4.37 % (1718612)Peak memory usage: 89 MB
% 24.76/4.37 % (1718612)Instructions burned: 134 (million)
% 24.76/4.37 % (1718617)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3174459702:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 24.76/4.37 % (1718619)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2271175624:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 24.76/4.37 % (1718617)Instruction limit reached!
% 24.76/4.37 % (1718617)------------------------------
% 24.76/4.37 % (1718617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718617)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718617)Termination reason: Instruction limit
% 24.76/4.37 % (1718617)Termination phase: Saturation
% 24.76/4.37 % (1718617)Time elapsed: 0.288 s
% 24.76/4.37 % (1718617)Peak memory usage: 94 MB
% 24.76/4.37 % (1718617)Instructions burned: 499 (million)
% 24.76/4.37 % (1718619)Instruction limit reached!
% 24.76/4.37 % (1718619)------------------------------
% 24.76/4.37 % (1718619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.76/4.37 % (1718619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.76/4.37 % (1718619)CaDiCaL version: 2.1.3
% 24.76/4.37 % (1718619)Termination reason: Instruction limit
% 24.76/4.37 % (1718619)Termination phase: Saturation
% 24.76/4.37 % (1718619)Time elapsed: 0.149 s
% 24.76/4.37 % (1718619)Peak memory usage: 89 MB
% 24.76/4.37 % (1718619)Instructions burned: 192 (million)
% 24.76/4.37 % (1718623)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=48197258:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 27.74/5.00 % (1718624)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1354121088:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 27.74/5.00 % (1718624)Instruction limit reached!
% 27.74/5.00 % (1718624)------------------------------
% 27.74/5.00 % (1718624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718624)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718624)Termination reason: Instruction limit
% 27.74/5.00 % (1718624)Termination phase: Saturation
% 27.74/5.00 % (1718624)Time elapsed: 0.120 s
% 27.74/5.00 % (1718624)Peak memory usage: 90 MB
% 27.74/5.00 % (1718624)Instructions burned: 157 (million)
% 27.74/5.00 % (1718623)Instruction limit reached!
% 27.74/5.00 % (1718623)------------------------------
% 27.74/5.00 % (1718623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718623)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718623)Termination reason: Instruction limit
% 27.74/5.00 % (1718623)Termination phase: Saturation
% 27.74/5.00 % (1718623)Time elapsed: 0.175 s
% 27.74/5.00 % (1718623)Peak memory usage: 91 MB
% 27.74/5.00 % (1718623)Instructions burned: 264 (million)
% 27.74/5.00 % (1718628)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2458489516:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 27.74/5.00 % (1718629)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2328707288:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi)
% 27.74/5.00 % (1718567)Refutation not found, incomplete strategy
% 27.74/5.00 % (1718567)------------------------------
% 27.74/5.00 % (1718567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718567)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718567)Termination reason: Refutation not found, incomplete strategy
% 27.74/5.00 % (1718567)Time elapsed: 2.124 s
% 27.74/5.00 % (1718567)Peak memory usage: 138 MB
% 27.74/5.00 % (1718567)Instructions burned: 2260 (million)
% 27.74/5.00 % (1718629)Instruction limit reached!
% 27.74/5.00 % (1718629)------------------------------
% 27.74/5.00 % (1718629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718629)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718629)Termination reason: Instruction limit
% 27.74/5.00 % (1718629)Termination phase: Saturation
% 27.74/5.00 % (1718629)Time elapsed: 0.207 s
% 27.74/5.00 % (1718629)Peak memory usage: 89 MB
% 27.74/5.00 % (1718629)Instructions burned: 540 (million)
% 27.74/5.00 % (1718567)------------------------------
% 27.74/5.00 % (1718567)------------------------------
% 27.74/5.00 % (1718632)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1585807073:i=180:bd=preordered:av=off_2974 on theBenchmark for (2974ds/180Mi)
% 27.74/5.00 % (1718598)Instruction limit reached!
% 27.74/5.00 % (1718598)------------------------------
% 27.74/5.00 % (1718598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718598)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718598)Termination reason: Instruction limit
% 27.74/5.00 % (1718598)Termination phase: Saturation
% 27.74/5.00 % (1718598)Time elapsed: 1.770 s
% 27.74/5.00 % (1718598)Peak memory usage: 138 MB
% 27.74/5.00 % (1718598)Instructions burned: 3397 (million)
% 27.74/5.00 % (1718632)Instruction limit reached!
% 27.74/5.00 % (1718632)------------------------------
% 27.74/5.00 % (1718632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718632)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718632)Termination reason: Instruction limit
% 27.74/5.00 % (1718632)Termination phase: Saturation
% 27.74/5.00 % (1718632)Time elapsed: 0.082 s
% 27.74/5.00 % (1718632)Peak memory usage: 90 MB
% 27.74/5.00 % (1718632)Instructions burned: 181 (million)
% 27.74/5.00 % (1718634)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=460607753:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2973 on theBenchmark for (2973ds/10307Mi)
% 27.74/5.00 % (1718636)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=952961367:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 27.74/5.00 % (1718636)Refutation not found, incomplete strategy
% 27.74/5.00 % (1718636)------------------------------
% 27.74/5.00 % (1718636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718636)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718636)Termination reason: Refutation not found, incomplete strategy
% 27.74/5.00 % (1718636)Time elapsed: 0.077 s
% 27.74/5.00 % (1718636)Peak memory usage: 93 MB
% 27.74/5.00 % (1718636)Instructions burned: 265 (million)
% 27.74/5.00 % (1718641)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3996463544:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 27.74/5.00 % (1718636)------------------------------
% 27.74/5.00 % (1718636)------------------------------
% 27.74/5.00 % (1718680)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=407062058:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 27.74/5.00 % (1718610)Refutation not found, incomplete strategy
% 27.74/5.00 % (1718610)------------------------------
% 27.74/5.00 % (1718610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718610)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718610)Termination reason: Refutation not found, incomplete strategy
% 27.74/5.00 % (1718610)Time elapsed: 1.916 s
% 27.74/5.00 % (1718610)Peak memory usage: 136 MB
% 27.74/5.00 % (1718610)Instructions burned: 3388 (million)
% 27.74/5.00 % (1718680)Instruction limit reached!
% 27.74/5.00 % (1718680)------------------------------
% 27.74/5.00 % (1718680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718680)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718680)Termination reason: Instruction limit
% 27.74/5.00 % (1718680)Termination phase: Saturation
% 27.74/5.00 % (1718680)Time elapsed: 0.064 s
% 27.74/5.00 % (1718680)Peak memory usage: 91 MB
% 27.74/5.00 % (1718680)Instructions burned: 304 (million)
% 27.74/5.00 % (1718682)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3142560092:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 27.74/5.00 % (1718565)Refutation not found, incomplete strategy
% 27.74/5.00 % (1718565)------------------------------
% 27.74/5.00 % (1718565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718565)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718565)Termination reason: Refutation not found, incomplete strategy
% 27.74/5.00 % (1718565)Time elapsed: 3.062 s
% 27.74/5.00 % (1718565)Peak memory usage: 142 MB
% 27.74/5.00 % (1718565)Instructions burned: 3857 (million)
% 27.74/5.00 % (1718610)------------------------------
% 27.74/5.00 % (1718610)------------------------------
% 27.74/5.00 % (1718682)Instruction limit reached!
% 27.74/5.00 % (1718682)------------------------------
% 27.74/5.00 % (1718682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718682)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718682)Termination reason: Instruction limit
% 27.74/5.00 % (1718682)Termination phase: Saturation
% 27.74/5.00 % (1718682)Time elapsed: 0.185 s
% 27.74/5.00 % (1718682)Peak memory usage: 95 MB
% 27.74/5.00 % (1718682)Instructions burned: 723 (million)
% 27.74/5.00 % (1718684)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3384566725:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 27.74/5.00 % (1718685)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=802675388:i=2989:sd=3:ss=axioms:sgt=60_2965 on theBenchmark for (2965ds/2989Mi)
% 27.74/5.00 % (1718565)------------------------------
% 27.74/5.00 % (1718565)------------------------------
% 27.74/5.00 % (1718688)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3462862219:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2964 on theBenchmark for (2964ds/1997Mi)
% 27.74/5.00 % (1718684)Instruction limit reached!
% 27.74/5.00 % (1718684)------------------------------
% 27.74/5.00 % (1718684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.74/5.00 % (1718684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.74/5.00 % (1718684)CaDiCaL version: 2.1.3
% 27.74/5.00 % (1718684)Termination reason: Instruction limit
% 27.74/5.00 % (1718684)Termination phase: Saturation
% 27.74/5.00 % (1718684)Time elapsed: 0.307 s
% 27.74/5.00 % (1718684)Peak memory usage: 93 MB
% 27.74/5.00 % (1718684)Instructions burned: 599 (million)
% 27.74/5.00 % (1718634)First to succeed.
% 27.74/5.00 % (1718634)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1718540"
% 27.74/5.00 % (1718690)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1263970949:i=2088:bd=preordered:av=off_2961 on theBenchmark for (2961ds/2088Mi)
% 27.74/5.00 % SZS status Satisfiable for theBenchmark
% 27.74/5.00 % SZS output start Saturation.
% See solution above
% 0.26/5.20 % SZS output start Definitions and Model Updates.
% 0.26/5.20 % SZS output end Definitions and Model Updates.
% 0.26/5.20 % (1718634)------------------------------
% 0.26/5.20 % (1718634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.26/5.20 % (1718634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.26/5.20 % (1718634)CaDiCaL version: 2.1.3
% 0.26/5.20 % (1718634)Termination reason: Satisfiable
% 0.26/5.20 % (1718634)Time elapsed: 1.152 s
% 0.26/5.20 % (1718634)Peak memory usage: 136 MB
% 0.26/5.20 % (1718634)Instructions burned: 1724 (million)
% 0.26/5.20 % (1718634)------------------------------
% 0.26/5.20 % (1718634)------------------------------
% 0.26/5.20 % (1718540)Success in time 4.145 s
% 0.26/5.20 % Vampire exiting
%------------------------------------------------------------------------------