%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV531-1.007 : 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 : n018.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:54 PM UTC 2026
% Result : Satisfiable 5.65s 1.63s
% Output : Saturation 7.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u104,negated_conjecture,
sF26 != sF47 ).
cnf(u109,axiom,
select(a1,i3) = sF0 ).
cnf(u114,axiom,
store(a1,i4,sF0) = sF1 ).
cnf(u119,axiom,
select(a1,i4) = sF2 ).
cnf(u124,axiom,
store(sF1,i3,sF2) = sF3 ).
cnf(u129,axiom,
select(sF3,i1) = sF4 ).
cnf(u134,axiom,
store(sF3,i2,sF4) = sF5 ).
cnf(u139,axiom,
select(sF3,i2) = sF6 ).
cnf(u144,axiom,
store(sF5,i1,sF6) = sF7 ).
cnf(u149,axiom,
select(sF7,i5) = sF8 ).
cnf(u154,axiom,
store(sF7,i0,sF8) = sF9 ).
cnf(u159,axiom,
select(sF7,i0) = sF10 ).
cnf(u164,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u169,axiom,
select(sF11,i5) = sF12 ).
cnf(u174,axiom,
store(sF11,i2,sF12) = sF13 ).
cnf(u179,axiom,
select(sF11,i2) = sF14 ).
cnf(u184,axiom,
store(sF13,i5,sF14) = sF15 ).
cnf(u189,axiom,
select(sF15,i1) = sF16 ).
cnf(u194,axiom,
store(sF15,i1,sF16) = sF17 ).
cnf(u199,axiom,
store(sF17,i1,sF16) = sF18 ).
cnf(u204,axiom,
select(sF18,i2) = sF19 ).
cnf(u209,axiom,
store(sF18,i5,sF19) = sF20 ).
cnf(u214,axiom,
select(sF18,i5) = sF21 ).
cnf(u219,axiom,
store(sF20,i2,sF21) = sF22 ).
cnf(u224,axiom,
select(sF22,i2) = sF23 ).
cnf(u229,axiom,
store(sF22,i5,sF23) = sF24 ).
cnf(u234,axiom,
select(sF22,i5) = sF25 ).
cnf(u239,axiom,
store(sF24,i2,sF25) = sF26 ).
cnf(u244,axiom,
store(sF3,i1,sF6) = sF27 ).
cnf(u249,axiom,
store(sF27,i2,sF4) = sF28 ).
cnf(u254,axiom,
select(sF28,i0) = sF29 ).
cnf(u259,axiom,
store(sF28,i5,sF29) = sF30 ).
cnf(u264,axiom,
select(sF28,i5) = sF31 ).
cnf(u269,axiom,
store(sF30,i0,sF31) = sF32 ).
cnf(u274,axiom,
select(sF32,i2) = sF33 ).
cnf(u279,axiom,
store(sF32,i5,sF33) = sF34 ).
cnf(u284,axiom,
select(sF32,i5) = sF35 ).
cnf(u289,axiom,
store(sF34,i2,sF35) = sF36 ).
cnf(u294,axiom,
select(sF36,i1) = sF37 ).
cnf(u299,axiom,
store(sF36,i1,sF37) = sF38 ).
cnf(u304,axiom,
store(sF38,i1,sF37) = sF39 ).
cnf(u309,axiom,
select(sF39,i2) = sF40 ).
cnf(u314,axiom,
store(sF39,i5,sF40) = sF41 ).
cnf(u319,axiom,
select(sF39,i5) = sF42 ).
cnf(u324,axiom,
store(sF41,i2,sF42) = sF43 ).
cnf(u329,axiom,
select(sF43,i2) = sF44 ).
cnf(u334,axiom,
store(sF43,i5,sF44) = sF45 ).
cnf(u339,axiom,
select(sF43,i5) = sF46 ).
cnf(u344,axiom,
store(sF45,i2,sF46) = sF47 ).
cnf(u375,axiom,
sF46 = select(sF47,i2) ).
cnf(u380,axiom,
sF44 = select(sF45,i5) ).
cnf(u385,axiom,
sF42 = select(sF43,i2) ).
cnf(u390,axiom,
sF40 = select(sF41,i5) ).
cnf(u395,axiom,
sF37 = select(sF39,i1) ).
cnf(u400,axiom,
sF37 = select(sF38,i1) ).
cnf(u405,axiom,
sF35 = select(sF36,i2) ).
cnf(u410,axiom,
sF33 = select(sF34,i5) ).
cnf(u415,axiom,
sF31 = select(sF32,i0) ).
cnf(u420,axiom,
sF29 = select(sF30,i5) ).
cnf(u425,axiom,
sF4 = select(sF28,i2) ).
cnf(u430,axiom,
sF25 = select(sF26,i2) ).
cnf(u435,axiom,
sF23 = select(sF24,i5) ).
cnf(u440,axiom,
sF21 = select(sF22,i2) ).
cnf(u445,axiom,
sF19 = select(sF20,i5) ).
cnf(u450,axiom,
sF16 = select(sF18,i1) ).
cnf(u455,axiom,
sF16 = select(sF17,i1) ).
cnf(u460,axiom,
sF14 = select(sF15,i5) ).
cnf(u465,axiom,
sF12 = select(sF13,i2) ).
cnf(u470,axiom,
sF10 = select(sF11,i5) ).
cnf(u475,axiom,
sF8 = select(sF9,i0) ).
cnf(u480,axiom,
sF6 = select(sF7,i1) ).
cnf(u485,axiom,
sF6 = select(sF27,i1) ).
cnf(u490,axiom,
sF4 = select(sF5,i2) ).
cnf(u495,axiom,
sF2 = select(sF3,i3) ).
cnf(u500,axiom,
sF0 = select(sF1,i4) ).
cnf(u533,axiom,
sF42 = sF44 ).
cnf(u539,axiom,
sF45 = store(sF43,i5,sF42) ).
cnf(u546,axiom,
sF21 = sF23 ).
cnf(u552,axiom,
sF24 = store(sF22,i5,sF21) ).
cnf(u559,axiom,
sF10 = sF12 ).
cnf(u565,axiom,
sF13 = store(sF11,i2,sF10) ).
cnf(u572,axiom,
sF42 = select(sF45,i5) ).
cnf(u587,axiom,
sF0 = select(sF3,i4) ).
cnf(u595,axiom,
sF21 = select(sF24,i5) ).
cnf(u606,axiom,
i2 = i1 ).
cnf(u610,axiom,
sF4 = select(sF7,i2) ).
cnf(u631,axiom,
sF6 = select(sF27,i2) ).
cnf(u636,axiom,
sF6 = select(sF7,i2) ).
cnf(u641,axiom,
sF16 = select(sF17,i2) ).
cnf(u646,axiom,
sF16 = select(sF18,i2) ).
cnf(u651,axiom,
sF37 = select(sF38,i2) ).
cnf(u656,axiom,
sF37 = select(sF39,i2) ).
cnf(u661,axiom,
sF39 = store(sF38,i2,sF37) ).
cnf(u666,axiom,
sF38 = store(sF36,i2,sF37) ).
cnf(u671,axiom,
sF37 = select(sF36,i2) ).
cnf(u676,axiom,
sF27 = store(sF3,i2,sF6) ).
cnf(u681,axiom,
sF18 = store(sF17,i2,sF16) ).
cnf(u686,axiom,
sF17 = store(sF15,i2,sF16) ).
cnf(u691,axiom,
sF16 = select(sF15,i2) ).
cnf(u696,axiom,
sF7 = store(sF5,i2,sF6) ).
cnf(u701,axiom,
sF4 = select(sF3,i2) ).
cnf(u709,axiom,
i0 != i5 ).
cnf(u714,axiom,
sF8 = select(sF11,i0) ).
cnf(u726,axiom,
sF8 = select(sF9,i5) ).
cnf(u730,axiom,
sF31 != select(sF32,i5) ).
cnf(u735,axiom,
sF32 != store(sF30,i5,sF31) ).
cnf(u740,axiom,
sF29 != select(sF28,i5) ).
cnf(u746,axiom,
sF9 != store(sF7,i5,sF8) ).
cnf(u751,axiom,
sF8 != sF10 ).
cnf(u763,axiom,
i2 = i5 ).
cnf(u767,axiom,
sF10 = select(sF15,i2) ).
cnf(u796,axiom,
sF4 = select(sF5,i5) ).
cnf(u802,axiom,
sF21 = select(sF22,i5) ).
cnf(u807,axiom,
sF25 = select(sF26,i5) ).
cnf(u812,axiom,
sF4 = select(sF28,i5) ).
cnf(u817,axiom,
sF35 = select(sF36,i5) ).
cnf(u822,axiom,
sF42 = select(sF43,i5) ).
cnf(u827,axiom,
sF46 = select(sF47,i5) ).
cnf(u832,axiom,
sF47 = store(sF45,i5,sF46) ).
cnf(u838,axiom,
sF43 = store(sF41,i5,sF42) ).
cnf(u843,axiom,
sF40 = select(sF39,i5) ).
cnf(u848,axiom,
sF36 = store(sF34,i5,sF35) ).
cnf(u853,axiom,
sF33 = select(sF32,i5) ).
cnf(u858,axiom,
sF28 = store(sF27,i5,sF4) ).
cnf(u863,axiom,
sF26 = store(sF24,i5,sF25) ).
cnf(u869,axiom,
sF22 = store(sF20,i5,sF21) ).
cnf(u874,axiom,
sF19 = select(sF18,i5) ).
cnf(u881,axiom,
sF6 = select(sF3,i5) ).
cnf(u886,axiom,
sF5 = store(sF3,i5,sF4) ).
cnf(u891,axiom,
sF10 = select(sF13,i5) ).
cnf(u899,axiom,
sF13 = store(sF11,i5,sF10) ).
cnf(u904,axiom,
sF10 = sF14 ).
cnf(u919,axiom,
sF19 = select(sF22,i5) ).
cnf(u955,axiom,
sF4 = select(sF7,i5) ).
cnf(u966,axiom,
sF15 = store(sF13,i5,sF10) ).
cnf(u977,axiom,
sF6 = select(sF28,i1) ).
cnf(u988,axiom,
sF29 = select(sF32,i5) ).
cnf(u995,axiom,
sF4 != sF29 ).
cnf(u1002,axiom,
sF4 = sF31 ).
cnf(u1028,axiom,
sF33 = select(sF36,i5) ).
cnf(u1033,axiom,
sF11 != store(sF9,i5,sF8) ).
cnf(u1045,axiom,
sF19 = sF25 ).
cnf(u1051,axiom,
sF26 = store(sF24,i2,sF19) ).
cnf(u1062,axiom,
sF40 = select(sF43,i5) ).
cnf(u1069,axiom,
sF29 = sF35 ).
cnf(u1075,axiom,
sF36 = store(sF34,i2,sF29) ).
cnf(u1082,axiom,
sF40 = sF46 ).
cnf(u1099,axiom,
sF14 = sF21 ).
cnf(u1106,axiom,
sF8 != select(sF18,i2) ).
cnf(u1142,axiom,
sF4 = sF6 ).
cnf(u1152,axiom,
sF8 != sF19 ).
cnf(u1203,axiom,
sF10 = select(sF15,i5) ).
cnf(u1236,axiom,
sF10 = select(sF3,i0) ).
cnf(u1242,axiom,
sF32 = store(sF30,i0,sF4) ).
cnf(u1251,axiom,
sF47 = store(sF45,i5,sF40) ).
cnf(u1272,axiom,
sF24 = store(sF22,i5,sF10) ).
cnf(u1277,axiom,
sF22 = store(sF20,i5,sF10) ).
cnf(u1288,axiom,
sF7 = store(sF5,i5,sF4) ).
cnf(u1293,axiom,
sF5 = sF27 ).
cnf(u1312,axiom,
sF10 = sF29 ).
cnf(u1321,axiom,
sF30 = store(sF28,i5,sF10) ).
cnf(u1326,axiom,
sF4 != sF10 ).
cnf(u1352,axiom,
sF7 = sF28 ).
cnf(u1373,axiom,
sF30 = store(sF7,i5,sF10) ).
cnf(u1383,axiom,
sF16 = select(sF17,i5) ).
cnf(u1391,axiom,
sF16 = sF19 ).
cnf(u1396,axiom,
sF16 = select(sF18,i5) ).
cnf(u1406,axiom,
sF37 = select(sF38,i5) ).
cnf(u1413,axiom,
sF20 = store(sF18,i5,sF16) ).
cnf(u1418,axiom,
sF8 != sF16 ).
cnf(u1426,axiom,
sF37 = sF40 ).
cnf(u1431,axiom,
sF37 = select(sF39,i5) ).
cnf(u1437,axiom,
sF41 = store(sF39,i5,sF37) ).
cnf(u1447,axiom,
sF35 = sF37 ).
cnf(u1452,axiom,
sF37 = select(sF36,i5) ).
cnf(u1461,axiom,
sF29 = sF37 ).
cnf(u1466,axiom,
sF36 = store(sF34,i5,sF37) ).
cnf(u1476,axiom,
sF10 = sF16 ).
cnf(u1481,axiom,
sF16 = select(sF15,i5) ).
cnf(u1489,axiom,
sF11 = store(sF9,i5,sF16) ).
cnf(u1494,axiom,
sF4 != sF16 ).
cnf(u1502,axiom,
sF4 = select(sF3,i5) ).
cnf(u1514,axiom,
sF4 != sF37 ).
cnf(u1521,axiom,
sF30 = store(sF7,i5,sF37) ).
cnf(u1526,axiom,
sF16 = sF37 ).
cnf(u1548,axiom,
sF14 = sF16 ).
cnf(u1558,axiom,
sF15 = store(sF13,i5,sF16) ).
cnf(u1577,axiom,
sF38 = store(sF36,i5,sF16) ).
cnf(u1582,axiom,
sF39 = store(sF38,i5,sF16) ).
cnf(u1604,axiom,
sF16 = sF33 ).
cnf(u1614,axiom,
sF34 = store(sF32,i5,sF16) ).
cnf(u1632,axiom,
sF16 = sF42 ).
cnf(u1644,axiom,
sF45 = store(sF43,i5,sF16) ).
cnf(u1649,axiom,
sF43 = store(sF41,i5,sF16) ).
cnf(u1660,axiom,
sF16 = sF40 ).
cnf(u1674,axiom,
sF16 = sF29 ).
cnf(u1684,axiom,
sF41 = store(sF39,i5,sF16) ).
cnf(u1702,axiom,
sF30 = store(sF7,i5,sF16) ).
cnf(u1713,axiom,
sF4 = sF8 ).
cnf(u1720,axiom,
sF9 = store(sF7,i0,sF4) ).
cnf(u1739,axiom,
sF13 = store(sF11,i5,sF16) ).
cnf(u1759,axiom,
sF16 = sF21 ).
cnf(u1776,axiom,
sF24 = store(sF22,i5,sF16) ).
cnf(u1781,axiom,
sF22 = store(sF20,i5,sF16) ).
cnf(u1802,axiom,
sF18 = store(sF17,i5,sF16) ).
cnf(u1817,axiom,
sF17 = store(sF15,i5,sF16) ).
cnf(u1847,axiom,
sF32 != store(sF30,i5,sF4) ).
cnf(u1862,axiom,
sF9 != store(sF7,i5,sF4) ).
cnf(u1882,axiom,
sF36 = store(sF34,i5,sF16) ).
cnf(u1897,axiom,
sF26 = store(sF24,i5,sF16) ).
cnf(u1928,axiom,
sF11 != store(sF9,i5,sF4) ).
cnf(u1964,axiom,
sF16 = select(sF26,i5) ).
cnf(u1987,axiom,
sF16 = sF25 ).
cnf(u1994,axiom,
sF4 = select(sF32,i0) ).
cnf(u2010,axiom,
sF47 = store(sF45,i5,sF16) ).
cnf(u2017,axiom,
sF16 = select(sF47,i5) ).
cnf(u2028,axiom,
sF16 = select(sF24,i5) ).
cnf(u2037,axiom,
sF16 = sF46 ).
cnf(u2046,axiom,
sF16 = select(sF22,i5) ).
cnf(u2062,axiom,
sF16 = sF23 ).
cnf(u2073,axiom,
sF16 = select(sF30,i5) ).
cnf(u2097,axiom,
sF16 = select(sF32,i5) ).
cnf(u2108,axiom,
sF16 = sF35 ).
cnf(u2115,axiom,
sF16 = select(sF36,i5) ).
cnf(u2147,axiom,
sF16 = select(sF20,i5) ).
cnf(u2176,axiom,
sF16 = select(sF41,i5) ).
cnf(u2210,axiom,
select(sF11,i5) = sF16 ).
cnf(u2223,axiom,
sF12 = sF16 ).
cnf(u2246,axiom,
sF16 = select(sF34,i5) ).
cnf(u2271,axiom,
sF16 = select(sF45,i5) ).
cnf(u2278,axiom,
sF16 = select(sF43,i5) ).
cnf(u2287,axiom,
sF16 = sF44 ).
cnf(u2307,axiom,
sF4 = select(sF9,i0) ).
cnf(u2318,axiom,
sF4 = select(sF11,i0) ).
cnf(u2325,axiom,
sF16 = select(sF13,i5) ).
cnf(u2402,axiom,
sF16 = select(sF38,i5) ).
cnf(u2439,axiom,
sF16 = select(sF39,i5) ).
cnf(u521,axiom,
( select(sF34,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u2239,axiom,
( select(sF18,X0) = select(sF22,X0)
| i5 = X0 ) ).
cnf(u1901,axiom,
( select(sF20,X0) = select(sF22,X0)
| i5 = X0 ) ).
cnf(u502,axiom,
( select(a1,X0) = select(sF1,X0)
| i4 = X0 ) ).
cnf(u2214,axiom,
( select(sF39,X0) = select(sF43,X0)
| i5 = X0 ) ).
cnf(u1798,axiom,
( select(sF17,X0) = select(sF18,X0)
| i5 = X0 ) ).
cnf(u524,axiom,
( select(sF39,X0) = select(sF41,X0)
| i5 = X0 ) ).
cnf(u1813,axiom,
( select(sF15,X0) = select(sF17,X0)
| i5 = X0 ) ).
cnf(u519,axiom,
( select(sF30,X0) = select(sF32,X0)
| i0 = X0 ) ).
cnf(u525,axiom,
( select(sF41,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u2294,axiom,
( select(sF7,X0) = select(sF30,X0)
| i5 = X0 ) ).
cnf(u908,axiom,
( select(sF15,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u579,axiom,
( select(a1,X0) = select(sF3,X0)
| i4 = X0
| i3 = X0 ) ).
cnf(u513,axiom,
( select(sF18,X0) = select(sF20,X0)
| i5 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u602,axiom,
( select(sF3,X0) = select(sF7,X0)
| i2 = X0
| i1 = X0 ) ).
cnf(u507,axiom,
( select(sF7,X0) = select(sF9,X0)
| i0 = X0 ) ).
cnf(u517,axiom,
( select(sF27,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u1346,axiom,
( select(sF5,X0) = select(sF28,X0)
| i5 = X0 ) ).
cnf(u1875,axiom,
( select(sF34,X0) = select(sF36,X0)
| i5 = X0 ) ).
cnf(u1868,axiom,
( select(sF45,X0) = select(sF47,X0)
| i5 = X0 ) ).
cnf(u511,axiom,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u1832,axiom,
( select(sF5,X0) = select(sF7,X0)
| i5 = X0 ) ).
cnf(u1749,axiom,
( select(sF38,X0) = select(sF39,X0)
| i5 = X0 ) ).
cnf(u1891,axiom,
( select(sF24,X0) = select(sF26,X0)
| i5 = X0 ) ).
cnf(u971,axiom,
( select(sF3,X0) = select(sF28,X0)
| i1 = X0
| i2 = X0 ) ).
cnf(u522,axiom,
( select(sF36,X0) = select(sF38,X0)
| i1 = X0 ) ).
cnf(u505,axiom,
( select(sF3,X0) = select(sF27,X0)
| i1 = X0 ) ).
cnf(u512,axiom,
( select(sF17,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u2186,axiom,
( select(sF15,X0) = select(sF18,X0)
| i5 = X0 ) ).
cnf(u1038,axiom,
( select(sF36,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u526,axiom,
( select(sF43,X0) = select(sF45,X0)
| i5 = X0 ) ).
cnf(u523,axiom,
( select(sF38,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u506,axiom,
( select(sF5,X0) = select(sF7,X0)
| i1 = X0 ) ).
cnf(u509,axiom,
( select(sF11,X0) = select(sF13,X0)
| i2 = X0 ) ).
cnf(u2157,axiom,
( select(sF36,X0) = select(sF39,X0)
| i5 = X0 ) ).
cnf(u2197,axiom,
( select(sF3,X0) = select(sF7,X0)
| i5 = X0 ) ).
cnf(u516,axiom,
( select(sF24,X0) = select(sF26,X0)
| i2 = X0 ) ).
cnf(u514,axiom,
( select(sF20,X0) = select(sF22,X0)
| i2 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u982,axiom,
( select(sF28,X0) = select(sF32,X0)
| i5 = X0
| i0 = X0 ) ).
cnf(u2465,axiom,
( select(sF7,X0) = select(sF32,X0)
| i0 = X0
| i5 = X0 ) ).
cnf(u518,axiom,
( select(sF28,X0) = select(sF30,X0)
| i5 = X0 ) ).
cnf(u527,axiom,
( select(sF45,X0) = select(sF47,X0)
| i2 = X0 ) ).
cnf(u1262,axiom,
( select(sF11,X0) = select(sF18,X0)
| i5 = X0 ) ).
cnf(u1904,axiom,
( select(sF3,X0) = select(sF5,X0)
| i5 = X0 ) ).
cnf(u2264,axiom,
( select(sF11,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u913,axiom,
( select(sF18,X0) = select(sF22,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u504,axiom,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u515,axiom,
( select(sF22,X0) = select(sF24,X0)
| i5 = X0 ) ).
cnf(u1337,axiom,
( select(sF32,X0) = select(sF39,X0)
| i5 = X0 ) ).
cnf(u1907,axiom,
( select(sF11,X0) = select(sF13,X0)
| i5 = X0 ) ).
cnf(u508,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u503,axiom,
( select(sF1,X0) = select(sF3,X0)
| i3 = X0 ) ).
cnf(u757,axiom,
( select(sF11,X0) = select(sF15,X0)
| i2 = X0
| i5 = X0 ) ).
cnf(u1765,axiom,
( select(sF36,X0) = select(sF38,X0)
| i5 = X0 ) ).
cnf(u1022,axiom,
( select(sF32,X0) = select(sF36,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u510,axiom,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u2227,axiom,
( select(sF32,X0) = select(sF36,X0)
| i5 = X0 ) ).
cnf(u1056,axiom,
( select(sF39,X0) = select(sF43,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u706,axiom,
( select(sF7,X0) = select(sF11,X0)
| i0 = X0
| i5 = X0 ) ).
cnf(u1871,axiom,
( select(sF41,X0) = select(sF43,X0)
| i5 = X0 ) ).
cnf(u520,axiom,
( select(sF32,X0) = select(sF34,X0)
| i5 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV531-1.007 : 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 : n018.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:36:40 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 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
% 5.65/1.63 % (3318360)Input is clausal, will run a generic CNF schedule.
% 5.65/1.63 % (3318365)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=4130994080:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.65/1.63 % (3318370)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=897222123:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.65/1.63 % (3318367)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=132225379:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.65/1.63 % (3318366)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2896836965:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.65/1.63 % (3318371)dis-21_1_sil=8000:lcm=predicate:random_seed=2957736602: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)
% 5.65/1.63 % (3318369)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2511746907:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.65/1.63 % (3318368)lrs+10_1_sil=8000:sp=occurrence:random_seed=347975961:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.65/1.63 % (3318371)Refutation not found, incomplete strategy
% 5.65/1.63 % (3318371)------------------------------
% 5.65/1.63 % (3318371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318371)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318371)Termination reason: Refutation not found, incomplete strategy
% 5.65/1.63 % (3318371)Time elapsed: 0.026 s
% 5.65/1.63 % (3318371)Peak memory usage: 89 MB
% 5.65/1.63 % (3318371)Instructions burned: 69 (million)
% 5.65/1.63 % (3318369)Instruction limit reached!
% 5.65/1.63 % (3318369)------------------------------
% 5.65/1.63 % (3318369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318369)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318369)Termination reason: Instruction limit
% 5.65/1.63 % (3318369)Termination phase: Saturation
% 5.65/1.63 % (3318369)Time elapsed: 0.041 s
% 5.65/1.63 % (3318369)Peak memory usage: 89 MB
% 5.65/1.63 % (3318369)Instructions burned: 115 (million)
% 5.65/1.63 % (3318368)Instruction limit reached!
% 5.65/1.63 % (3318368)------------------------------
% 5.65/1.63 % (3318368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318368)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318368)Termination reason: Instruction limit
% 5.65/1.63 % (3318368)Termination phase: Saturation
% 5.65/1.63 % (3318368)Time elapsed: 0.042 s
% 5.65/1.63 % (3318368)Peak memory usage: 90 MB
% 5.65/1.63 % (3318368)Instructions burned: 110 (million)
% 5.65/1.63 % (3318370)Instruction limit reached!
% 5.65/1.63 % (3318370)------------------------------
% 5.65/1.63 % (3318370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318370)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318370)Termination reason: Instruction limit
% 5.65/1.63 % (3318370)Termination phase: Saturation
% 5.65/1.63 % (3318370)Time elapsed: 0.070 s
% 5.65/1.63 % (3318370)Peak memory usage: 90 MB
% 5.65/1.63 % (3318370)Instructions burned: 182 (million)
% 5.65/1.63 % (3318379)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=3298643901:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.65/1.63 % (3318380)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1434634910: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)
% 5.65/1.63 % (3318381)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3192821735:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.65/1.63 % (3318379)Instruction limit reached!
% 5.65/1.63 % (3318379)------------------------------
% 5.65/1.63 % (3318379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318379)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318379)Termination reason: Instruction limit
% 5.65/1.63 % (3318379)Termination phase: Saturation
% 5.65/1.63 % (3318379)Time elapsed: 0.057 s
% 5.65/1.63 % (3318379)Peak memory usage: 90 MB
% 5.65/1.63 % (3318379)Instructions burned: 145 (million)
% 5.65/1.63 % (3318380)Instruction limit reached!
% 5.65/1.63 % (3318380)------------------------------
% 5.65/1.63 % (3318380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318380)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318380)Termination reason: Instruction limit
% 5.65/1.63 % (3318380)Termination phase: Saturation
% 5.65/1.63 % (3318380)Time elapsed: 0.073 s
% 5.65/1.63 % (3318380)Peak memory usage: 92 MB
% 5.65/1.63 % (3318380)Instructions burned: 189 (million)
% 5.65/1.63 % (3318371)------------------------------
% 5.65/1.63 % (3318371)------------------------------
% 5.65/1.63 % (3318381)Instruction limit reached!
% 5.65/1.63 % (3318381)------------------------------
% 5.65/1.63 % (3318381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318381)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318381)Termination reason: Instruction limit
% 5.65/1.63 % (3318381)Termination phase: Saturation
% 5.65/1.63 % (3318381)Time elapsed: 0.083 s
% 5.65/1.63 % (3318381)Peak memory usage: 91 MB
% 5.65/1.63 % (3318381)Instructions burned: 221 (million)
% 5.65/1.63 % (3318365)Refutation not found, incomplete strategy
% 5.65/1.63 % (3318365)------------------------------
% 5.65/1.63 % (3318365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318365)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318365)Termination reason: Refutation not found, incomplete strategy
% 5.65/1.63 % (3318365)Time elapsed: 0.409 s
% 5.65/1.63 % (3318365)Peak memory usage: 129 MB
% 5.65/1.63 % (3318365)Instructions burned: 1092 (million)
% 5.65/1.63 % (3318385)lrs+10_64_to=lpo:sil=8000:random_seed=2248451522:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.65/1.63 % (3318386)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3416004902:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.65/1.63 % (3318387)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=875827294:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.65/1.63 % (3318385)Instruction limit reached!
% 5.65/1.63 % (3318385)------------------------------
% 5.65/1.63 % (3318385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318385)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318385)Termination reason: Instruction limit
% 5.65/1.63 % (3318385)Termination phase: Saturation
% 5.65/1.63 % (3318385)Time elapsed: 0.051 s
% 5.65/1.63 % (3318385)Peak memory usage: 91 MB
% 5.65/1.63 % (3318385)Instructions burned: 127 (million)
% 5.65/1.63 % (3318388)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1344554301:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 5.65/1.63 % (3318387)First to succeed.
% 5.65/1.63 % (3318387)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3318360"
% 5.65/1.63 % (3318386)Instruction limit reached!
% 5.65/1.63 % (3318386)------------------------------
% 5.65/1.63 % (3318386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318386)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318386)Termination reason: Instruction limit
% 5.65/1.63 % (3318386)Termination phase: Saturation
% 5.65/1.63 % (3318386)Time elapsed: 0.076 s
% 5.65/1.63 % (3318386)Peak memory usage: 91 MB
% 5.65/1.63 % (3318386)Instructions burned: 196 (million)
% 5.65/1.63 % (3318365)------------------------------
% 5.65/1.63 % (3318365)------------------------------
% 5.65/1.63 % (3318392)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=4054149035:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.65/1.63 % (3318395)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2845523865:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 5.65/1.63 % (3318394)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2885575144:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 5.65/1.63 % (3318392)Instruction limit reached!
% 5.65/1.63 % (3318392)------------------------------
% 5.65/1.63 % (3318392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318392)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318392)Termination reason: Instruction limit
% 5.65/1.63 % (3318392)Termination phase: Saturation
% 5.65/1.63 % (3318392)Time elapsed: 0.041 s
% 5.65/1.63 % (3318392)Peak memory usage: 91 MB
% 5.65/1.63 % (3318392)Instructions burned: 106 (million)
% 5.65/1.63 % (3318395)Refutation not found, incomplete strategy
% 5.65/1.63 % (3318395)------------------------------
% 5.65/1.63 % (3318395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318395)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318395)Termination reason: Refutation not found, incomplete strategy
% 5.65/1.63 % (3318395)Time elapsed: 0.023 s
% 5.65/1.63 % (3318395)Peak memory usage: 88 MB
% 5.65/1.63 % (3318395)Instructions burned: 111 (million)
% 5.65/1.63 % (3318394)Instruction limit reached!
% 5.65/1.63 % (3318394)------------------------------
% 5.65/1.63 % (3318394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.65/1.63 % (3318394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.65/1.63 % (3318394)CaDiCaL version: 2.1.3
% 5.65/1.63 % (3318394)Termination reason: Instruction limit
% 5.65/1.63 % (3318394)Termination phase: Saturation
% 5.65/1.63 % (3318394)Time elapsed: 0.042 s
% 5.65/1.63 % (3318394)Peak memory usage: 90 MB
% 5.65/1.63 % (3318394)Instructions burned: 107 (million)
% 5.65/1.63 % SZS status Satisfiable for theBenchmark
% 5.65/1.63 % SZS output start Saturation.
% See solution above
% 7.16/1.83 % SZS output start Definitions and Model Updates.
% 7.16/1.83 % SZS output end Definitions and Model Updates.
% 7.16/1.83 % (3318387)------------------------------
% 7.16/1.83 % (3318387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.83 % (3318387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.83 % (3318387)CaDiCaL version: 2.1.3
% 7.16/1.83 % (3318387)Termination reason: Satisfiable
% 7.16/1.83 % (3318387)Time elapsed: 0.069 s
% 7.16/1.83 % (3318387)Peak memory usage: 89 MB
% 7.16/1.83 % (3318387)Instructions burned: 132 (million)
% 7.16/1.83 % (3318387)------------------------------
% 7.16/1.83 % (3318387)------------------------------
% 7.16/1.83 % (3318360)Success in time 0.964 s
% 7.16/1.83 % Vampire exiting
%------------------------------------------------------------------------------