%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV532-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:55 PM UTC 2026
% Result : Satisfiable 5.24s 1.59s
% Output : Saturation 6.82s
% 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,i6,sF44) = sF45 ).
cnf(u339,axiom,
select(sF43,i6) = sF46 ).
cnf(u344,axiom,
store(sF45,i2,sF46) = sF47 ).
cnf(u375,axiom,
sF46 = select(sF47,i2) ).
cnf(u380,axiom,
sF44 = select(sF45,i6) ).
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,i6,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,i6) ).
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(u731,axiom,
sF31 = select(sF32,i5) ).
cnf(u735,axiom,
sF32 != store(sF30,i5,sF31) ).
cnf(u741,axiom,
sF29 = select(sF28,i5) ).
cnf(u746,axiom,
sF9 != store(sF7,i5,sF8) ).
cnf(u752,axiom,
sF8 = sF10 ).
cnf(u762,axiom,
i2 != i5 ).
cnf(u767,axiom,
sF10 = select(sF15,i2) ).
cnf(u796,axiom,
sF21 = select(sF24,i2) ).
cnf(u800,axiom,
sF24 != store(sF22,i2,sF21) ).
cnf(u806,axiom,
sF10 = select(sF11,i2) ).
cnf(u811,axiom,
sF14 = select(sF15,i2) ).
cnf(u816,axiom,
sF19 = select(sF20,i2) ).
cnf(u822,axiom,
sF29 = select(sF30,i2) ).
cnf(u827,axiom,
sF33 = select(sF34,i2) ).
cnf(u832,axiom,
sF40 = select(sF41,i2) ).
cnf(u838,axiom,
sF41 = store(sF39,i2,sF40) ).
cnf(u844,axiom,
sF34 = store(sF32,i2,sF33) ).
cnf(u849,axiom,
sF30 != store(sF28,i2,sF29) ).
cnf(u858,axiom,
sF20 = store(sF18,i2,sF19) ).
cnf(u863,axiom,
sF15 = store(sF13,i2,sF14) ).
cnf(u869,axiom,
sF11 = store(sF9,i2,sF10) ).
cnf(u876,axiom,
sF40 = sF42 ).
cnf(u881,axiom,
sF33 = sF35 ).
cnf(u886,axiom,
sF4 = sF31 ).
cnf(u893,axiom,
sF19 = sF21 ).
cnf(u899,axiom,
sF4 = sF8 ).
cnf(u904,axiom,
sF21 = sF25 ).
cnf(u919,axiom,
sF19 = select(sF22,i5) ).
cnf(u938,axiom,
sF10 = sF14 ).
cnf(u945,axiom,
sF19 = sF25 ).
cnf(u955,axiom,
sF43 = store(sF41,i2,sF40) ).
cnf(u960,axiom,
sF45 = store(sF43,i6,sF40) ).
cnf(u966,axiom,
sF36 = store(sF34,i2,sF33) ).
cnf(u977,axiom,
sF6 = select(sF28,i1) ).
cnf(u983,axiom,
sF32 = store(sF30,i0,sF4) ).
cnf(u990,axiom,
sF22 = store(sF20,i2,sF19) ).
cnf(u995,axiom,
sF24 = store(sF22,i5,sF19) ).
cnf(u1006,axiom,
sF29 = select(sF32,i5) ).
cnf(u1012,axiom,
sF9 = store(sF7,i0,sF4) ).
cnf(u1018,axiom,
sF15 = store(sF13,i5,sF10) ).
cnf(u1029,axiom,
sF33 = select(sF36,i5) ).
cnf(u1035,axiom,
sF26 = store(sF24,i2,sF19) ).
cnf(u1052,axiom,
sF40 = select(sF43,i5) ).
cnf(u1059,axiom,
sF29 = sF35 ).
cnf(u1067,axiom,
sF36 = store(sF34,i2,sF29) ).
cnf(u1072,axiom,
sF29 = sF33 ).
cnf(u1078,axiom,
sF34 = store(sF32,i5,sF29) ).
cnf(u1092,axiom,
sF10 = select(sF18,i2) ).
cnf(u1099,axiom,
i1 != i5 ).
cnf(u1104,axiom,
sF10 = sF19 ).
cnf(u1114,axiom,
sF4 = sF6 ).
cnf(u1152,axiom,
sF29 = sF40 ).
cnf(u1158,axiom,
sF20 = store(sF18,i5,sF10) ).
cnf(u1167,axiom,
sF7 = store(sF5,i2,sF4) ).
cnf(u1173,axiom,
sF5 = sF27 ).
cnf(u1189,axiom,
sF10 = select(sF3,i0) ).
cnf(u1193,axiom,
i2 = i0 ).
cnf(u1204,axiom,
sF4 = select(sF3,i5) ).
cnf(u1210,axiom,
sF41 = store(sF39,i5,sF29) ).
cnf(u1232,axiom,
sF4 = select(sF11,i2) ).
cnf(u1237,axiom,
sF4 = select(sF9,i2) ).
cnf(u1242,axiom,
sF4 = select(sF32,i2) ).
cnf(u1247,axiom,
sF32 = store(sF30,i2,sF4) ).
cnf(u1252,axiom,
sF4 = sF29 ).
cnf(u1257,axiom,
sF4 = sF10 ).
cnf(u1262,axiom,
sF9 = store(sF7,i2,sF4) ).
cnf(u1276,axiom,
sF7 = store(sF5,i1,sF4) ).
cnf(u1284,axiom,
sF10 = sF16 ).
cnf(u1296,axiom,
sF5 = store(sF3,i1,sF4) ).
cnf(u1309,axiom,
sF35 = sF37 ).
cnf(u1314,axiom,
sF4 = sF14 ).
cnf(u1389,axiom,
sF16 = sF29 ).
cnf(u1402,axiom,
sF4 = sF33 ).
cnf(u1408,axiom,
sF11 = store(sF9,i5,sF16) ).
cnf(u1426,axiom,
sF36 = store(sF34,i2,sF37) ).
cnf(u1435,axiom,
sF4 = sF37 ).
cnf(u1440,axiom,
sF16 = sF37 ).
cnf(u1455,axiom,
sF4 = select(sF9,i5) ).
cnf(u1460,axiom,
sF32 != store(sF30,i5,sF4) ).
cnf(u1466,axiom,
sF16 = select(sF28,i5) ).
cnf(u1470,axiom,
sF9 != store(sF7,i5,sF4) ).
cnf(u1477,axiom,
sF4 = sF16 ).
cnf(u1612,axiom,
sF9 = store(sF7,i2,sF8) ).
cnf(u1619,axiom,
sF32 = store(sF30,i2,sF31) ).
cnf(u1624,axiom,
sF31 = select(sF32,i2) ).
cnf(u1629,axiom,
sF8 = select(sF9,i2) ).
cnf(u1634,axiom,
sF8 = select(sF11,i2) ).
cnf(u1674,axiom,
sF30 != store(sF28,i2,sF4) ).
cnf(u1723,axiom,
sF4 = select(sF28,i5) ).
cnf(u1741,axiom,
i2 != i6 ).
cnf(u1745,axiom,
i5 != i6 ).
cnf(u1750,axiom,
sF46 = select(sF39,i6) ).
cnf(u1774,axiom,
sF15 = store(sF13,i5,sF4) ).
cnf(u1781,axiom,
sF30 = store(sF28,i5,sF4) ).
cnf(u1787,axiom,
sF34 = store(sF32,i5,sF4) ).
cnf(u1799,axiom,
sF7 = sF28 ).
cnf(u1819,axiom,
sF11 = store(sF9,i5,sF4) ).
cnf(u1828,axiom,
sF4 = sF19 ).
cnf(u1837,axiom,
sF38 = store(sF36,i2,sF4) ).
cnf(u1842,axiom,
sF39 = store(sF38,i2,sF4) ).
cnf(u1865,axiom,
sF4 = sF40 ).
cnf(u1874,axiom,
sF17 = store(sF15,i2,sF4) ).
cnf(u1879,axiom,
sF18 = store(sF17,i2,sF4) ).
cnf(u1891,axiom,
sF20 = store(sF18,i5,sF4) ).
cnf(u1903,axiom,
sF41 = store(sF39,i5,sF4) ).
cnf(u1919,axiom,
sF4 = select(sF7,i5) ).
cnf(u1926,axiom,
sF30 = store(sF7,i5,sF4) ).
cnf(u1967,axiom,
sF13 = store(sF11,i2,sF4) ).
cnf(u1974,axiom,
sF4 = select(sF13,i2) ).
cnf(u2011,axiom,
sF4 = sF12 ).
cnf(u2017,axiom,
sF4 = select(sF15,i2) ).
cnf(u2054,axiom,
sF41 = store(sF39,i2,sF4) ).
cnf(u2064,axiom,
sF34 = store(sF32,i2,sF4) ).
cnf(u2074,axiom,
sF20 = store(sF18,i2,sF4) ).
cnf(u2085,axiom,
sF15 = store(sF13,i2,sF4) ).
cnf(u2097,axiom,
sF11 = store(sF9,i2,sF4) ).
cnf(u2105,axiom,
sF9 != sF30 ).
cnf(u2114,axiom,
sF46 = select(sF32,i6) ).
cnf(u2151,axiom,
sF4 = select(sF45,i5) ).
cnf(u2155,axiom,
sF45 != store(sF43,i5,sF4) ).
cnf(u2161,axiom,
sF4 != sF46 ).
cnf(u2171,axiom,
sF47 != store(sF45,i2,sF4) ).
cnf(u2182,axiom,
sF24 != store(sF22,i2,sF4) ).
cnf(u2196,axiom,
sF43 = store(sF41,i2,sF4) ).
cnf(u2205,axiom,
sF4 = select(sF43,i2) ).
cnf(u2214,axiom,
sF4 = sF44 ).
cnf(u2219,axiom,
sF4 = sF42 ).
cnf(u2246,axiom,
sF36 = store(sF34,i2,sF4) ).
cnf(u2268,axiom,
sF22 = store(sF20,i2,sF4) ).
cnf(u2277,axiom,
sF4 = select(sF22,i2) ).
cnf(u2288,axiom,
sF24 = store(sF22,i5,sF4) ).
cnf(u2297,axiom,
sF4 = select(sF24,i5) ).
cnf(u2306,axiom,
sF4 = sF23 ).
cnf(u2311,axiom,
sF4 = sF21 ).
cnf(u2330,axiom,
sF4 = select(sF15,i5) ).
cnf(u2346,axiom,
sF26 = store(sF24,i2,sF4) ).
cnf(u2355,axiom,
sF4 = select(sF26,i2) ).
cnf(u2377,axiom,
sF4 = select(sF18,i5) ).
cnf(u2389,axiom,
sF4 = select(sF20,i5) ).
cnf(u2396,axiom,
sF4 = sF25 ).
cnf(u2413,axiom,
sF4 = select(sF41,i5) ).
cnf(u2424,axiom,
sF4 = select(sF22,i5) ).
cnf(u2437,axiom,
sF4 = select(sF43,i5) ).
cnf(u2465,axiom,
sF4 = select(sF11,i5) ).
cnf(u2484,axiom,
sF4 = select(sF30,i5) ).
cnf(u2495,axiom,
sF4 = select(sF32,i5) ).
cnf(u2502,axiom,
sF4 = select(sF34,i5) ).
cnf(u2513,axiom,
sF4 = select(sF36,i5) ).
cnf(u2520,axiom,
sF4 = select(sF34,i2) ).
cnf(u2535,axiom,
sF4 = sF35 ).
cnf(u2557,axiom,
sF4 = select(sF39,i5) ).
cnf(u2598,axiom,
sF4 = select(sF38,i2) ).
cnf(u2637,axiom,
sF4 = select(sF39,i2) ).
cnf(u2664,axiom,
sF4 = select(sF17,i2) ).
cnf(u2687,axiom,
sF4 = select(sF18,i2) ).
cnf(u2704,axiom,
sF4 = select(sF41,i2) ).
cnf(u2711,axiom,
sF4 = select(sF20,i2) ).
cnf(u2736,axiom,
sF45 = store(sF43,i6,sF4) ).
cnf(u2746,axiom,
sF4 = select(sF45,i6) ).
cnf(u2761,axiom,
sF46 = select(sF7,i6) ).
cnf(u2778,axiom,
sF46 = select(sF3,i6) ).
cnf(u2798,axiom,
sF4 = select(sF36,i2) ).
cnf(u520,axiom,
( select(sF32,X0) = select(sF34,X0)
| i5 = X0 ) ).
cnf(u521,axiom,
( select(sF34,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u502,axiom,
( select(a1,X0) = select(sF1,X0)
| i4 = X0 ) ).
cnf(u524,axiom,
( select(sF39,X0) = select(sF41,X0)
| i5 = X0 ) ).
cnf(u519,axiom,
( select(sF30,X0) = select(sF32,X0)
| i0 = X0 ) ).
cnf(u2906,axiom,
( select(sF11,X0) = select(sF18,X0)
| i2 = X0
| i5 = X0 ) ).
cnf(u525,axiom,
( select(sF41,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u2946,axiom,
( select(sF32,X0) = select(sF39,X0)
| i2 = X0 ) ).
cnf(u2439,axiom,
( select(sF7,X0) = select(sF9,X0)
| i2 = X0 ) ).
cnf(u908,axiom,
( select(sF15,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u2026,axiom,
( select(sF15,X0) = select(sF17,X0)
| i2 = X0 ) ).
cnf(u513,axiom,
( select(sF18,X0) = select(sF20,X0)
| i5 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u2426,axiom,
( select(sF30,X0) = select(sF32,X0)
| i2 = X0 ) ).
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(u2591,axiom,
( select(sF3,X0) = select(sF7,X0)
| i2 = X0 ) ).
cnf(u517,axiom,
( select(sF27,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u2090,axiom,
( select(sF9,X0) = select(sF11,X0)
| i2 = X0 ) ).
cnf(u1046,axiom,
( select(sF39,X0) = select(sF43,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u1000,axiom,
( select(sF28,X0) = select(sF32,X0)
| i5 = X0
| i0 = X0 ) ).
cnf(u511,axiom,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u1023,axiom,
( select(sF32,X0) = select(sF36,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u1991,axiom,
( select(sF36,X0) = select(sF38,X0)
| i2 = 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(u2657,axiom,
( select(sF11,X0) = select(sF15,X0)
| i2 = X0 ) ).
cnf(u1789,axiom,
( select(sF5,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u505,axiom,
( select(sF3,X0) = select(sF27,X0)
| i1 = X0 ) ).
cnf(u512,axiom,
( select(sF17,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u526,axiom,
( select(sF43,X0) = select(sF45,X0)
| i6 = X0 ) ).
cnf(u2068,axiom,
( select(sF18,X0) = select(sF20,X0)
| i2 = X0 ) ).
cnf(u2645,axiom,
( select(sF18,X0) = select(sF22,X0)
| i2 = 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(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(u2827,axiom,
( select(sF7,X0) = select(sF30,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(u1039,axiom,
( select(sF36,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u913,axiom,
( select(sF18,X0) = select(sF22,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u2031,axiom,
( select(sF5,X0) = select(sF7,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(u2079,axiom,
( select(sF13,X0) = select(sF15,X0)
| i2 = X0 ) ).
cnf(u1415,axiom,
( select(sF32,X0) = select(sF39,X0)
| i2 = X0
| i5 = X0 ) ).
cnf(u2565,axiom,
( select(sF36,X0) = select(sF39,X0)
| i2 = X0 ) ).
cnf(u508,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u503,axiom,
( select(sF1,X0) = select(sF3,X0)
| i3 = X0 ) ).
cnf(u2606,axiom,
( select(sF39,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u757,axiom,
( select(sF11,X0) = select(sF15,X0)
| i2 = X0
| i5 = X0 ) ).
cnf(u2048,axiom,
( select(sF39,X0) = select(sF41,X0)
| i2 = X0 ) ).
cnf(u2585,axiom,
( select(sF15,X0) = select(sF18,X0)
| i2 = X0 ) ).
cnf(u2020,axiom,
( select(sF17,X0) = select(sF18,X0)
| i2 = X0 ) ).
cnf(u1333,axiom,
( select(sF11,X0) = select(sF18,X0)
| i1 = X0
| i2 = X0
| i5 = X0 ) ).
cnf(u2624,axiom,
( select(sF32,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u510,axiom,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u579,axiom,
( select(a1,X0) = select(sF3,X0)
| i4 = X0
| i3 = X0 ) ).
cnf(u2982,axiom,
( select(sF11,X0) = select(sF18,X0)
| i2 = X0 ) ).
cnf(u1982,axiom,
( select(sF38,X0) = select(sF39,X0)
| i2 = X0 ) ).
cnf(u706,axiom,
( select(sF7,X0) = select(sF11,X0)
| i0 = X0
| i5 = X0 ) ).
cnf(u2835,axiom,
( select(sF7,X0) = select(sF32,X0)
| i5 = X0
| i2 = X0 ) ).
cnf(u2059,axiom,
( select(sF32,X0) = select(sF34,X0)
| i2 = X0 ) ).
cnf(u2673,axiom,
( select(sF7,X0) = select(sF11,X0)
| i2 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV532-1.007 : 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.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:36:55 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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.24/1.59 % (3318812)Input is clausal, will run a generic CNF schedule.
% 5.24/1.59 % (3318818)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1855263844:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.24/1.59 % (3318823)dis-21_1_sil=8000:lcm=predicate:random_seed=230794908: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.24/1.59 % (3318822)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2405017306:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.24/1.59 % (3318819)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1321340920:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.24/1.59 % (3318817)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=3094126159:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.24/1.59 % (3318820)lrs+10_1_sil=8000:sp=occurrence:random_seed=1770306202:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.24/1.59 % (3318821)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=477549259:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.24/1.59 % (3318823)Refutation not found, incomplete strategy
% 5.24/1.59 % (3318823)------------------------------
% 5.24/1.59 % (3318823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318823)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318823)Termination reason: Refutation not found, incomplete strategy
% 5.24/1.59 % (3318823)Time elapsed: 0.026 s
% 5.24/1.59 % (3318823)Peak memory usage: 89 MB
% 5.24/1.59 % (3318823)Instructions burned: 69 (million)
% 5.24/1.59 % (3318821)Instruction limit reached!
% 5.24/1.59 % (3318821)------------------------------
% 5.24/1.59 % (3318821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318821)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318821)Termination reason: Instruction limit
% 5.24/1.59 % (3318821)Termination phase: Saturation
% 5.24/1.59 % (3318821)Time elapsed: 0.040 s
% 5.24/1.59 % (3318821)Peak memory usage: 89 MB
% 5.24/1.59 % (3318821)Instructions burned: 115 (million)
% 5.24/1.59 % (3318820)Instruction limit reached!
% 5.24/1.59 % (3318820)------------------------------
% 5.24/1.59 % (3318820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318820)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318820)Termination reason: Instruction limit
% 5.24/1.59 % (3318820)Termination phase: Saturation
% 5.24/1.59 % (3318820)Time elapsed: 0.041 s
% 5.24/1.59 % (3318820)Peak memory usage: 90 MB
% 5.24/1.59 % (3318820)Instructions burned: 110 (million)
% 5.24/1.59 % (3318822)Instruction limit reached!
% 5.24/1.59 % (3318822)------------------------------
% 5.24/1.59 % (3318822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318822)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318822)Termination reason: Instruction limit
% 5.24/1.59 % (3318822)Termination phase: Saturation
% 5.24/1.59 % (3318822)Time elapsed: 0.069 s
% 5.24/1.59 % (3318822)Peak memory usage: 90 MB
% 5.24/1.59 % (3318822)Instructions burned: 183 (million)
% 5.24/1.59 % (3318832)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2250978237: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.24/1.59 % (3318831)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=2911608746:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.24/1.59 % (3318833)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1035067668:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.24/1.59 % (3318831)Instruction limit reached!
% 5.24/1.59 % (3318831)------------------------------
% 5.24/1.59 % (3318831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318831)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318831)Termination reason: Instruction limit
% 5.24/1.59 % (3318831)Termination phase: Saturation
% 5.24/1.59 % (3318831)Time elapsed: 0.055 s
% 5.24/1.59 % (3318831)Peak memory usage: 90 MB
% 5.24/1.59 % (3318831)Instructions burned: 143 (million)
% 5.24/1.59 % (3318832)Instruction limit reached!
% 5.24/1.59 % (3318832)------------------------------
% 5.24/1.59 % (3318832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318832)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318832)Termination reason: Instruction limit
% 5.24/1.59 % (3318832)Termination phase: Saturation
% 5.24/1.59 % (3318832)Time elapsed: 0.072 s
% 5.24/1.59 % (3318832)Peak memory usage: 92 MB
% 5.24/1.59 % (3318832)Instructions burned: 189 (million)
% 5.24/1.59 % (3318823)------------------------------
% 5.24/1.59 % (3318823)------------------------------
% 5.24/1.59 % (3318833)Instruction limit reached!
% 5.24/1.59 % (3318833)------------------------------
% 5.24/1.59 % (3318833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318833)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318833)Termination reason: Instruction limit
% 5.24/1.59 % (3318833)Termination phase: Saturation
% 5.24/1.59 % (3318833)Time elapsed: 0.082 s
% 5.24/1.59 % (3318833)Peak memory usage: 91 MB
% 5.24/1.59 % (3318833)Instructions burned: 221 (million)
% 5.24/1.59 % (3318837)lrs+10_64_to=lpo:sil=8000:random_seed=4099275171:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.24/1.59 % (3318838)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3289109999:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.24/1.59 % (3318839)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3684168702:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.24/1.59 % (3318837)Instruction limit reached!
% 5.24/1.59 % (3318837)------------------------------
% 5.24/1.59 % (3318837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318837)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318837)Termination reason: Instruction limit
% 5.24/1.59 % (3318837)Termination phase: Saturation
% 5.24/1.59 % (3318837)Time elapsed: 0.050 s
% 5.24/1.59 % (3318837)Peak memory usage: 91 MB
% 5.24/1.59 % (3318837)Instructions burned: 129 (million)
% 5.24/1.59 % (3318840)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=239553563:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.24/1.59 % (3318838)Instruction limit reached!
% 5.24/1.59 % (3318838)------------------------------
% 5.24/1.59 % (3318838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318838)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318838)Termination reason: Instruction limit
% 5.24/1.59 % (3318838)Termination phase: Saturation
% 5.24/1.59 % (3318838)Time elapsed: 0.074 s
% 5.24/1.59 % (3318838)Peak memory usage: 91 MB
% 5.24/1.59 % (3318838)Instructions burned: 196 (million)
% 5.24/1.59 % (3318839)First to succeed.
% 5.24/1.59 % (3318839)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3318812"
% 5.24/1.59 % (3318844)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=3119822850:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.24/1.59 % (3318846)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1241489833:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.24/1.59 % (3318844)Instruction limit reached!
% 5.24/1.59 % (3318844)------------------------------
% 5.24/1.59 % (3318844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318844)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318844)Termination reason: Instruction limit
% 5.24/1.59 % (3318844)Termination phase: Saturation
% 5.24/1.59 % (3318844)Time elapsed: 0.040 s
% 5.24/1.59 % (3318844)Peak memory usage: 90 MB
% 5.24/1.59 % (3318844)Instructions burned: 107 (million)
% 5.24/1.59 % (3318846)Instruction limit reached!
% 5.24/1.59 % (3318846)------------------------------
% 5.24/1.59 % (3318846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.24/1.59 % (3318846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.24/1.59 % (3318846)CaDiCaL version: 2.1.3
% 5.24/1.59 % (3318846)Termination reason: Instruction limit
% 5.24/1.59 % (3318846)Termination phase: Saturation
% 5.24/1.59 % (3318846)Time elapsed: 0.041 s
% 5.24/1.59 % (3318846)Peak memory usage: 90 MB
% 5.24/1.59 % (3318846)Instructions burned: 109 (million)
% 5.24/1.59 % (3318849)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2450878723:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 5.24/1.59 % SZS status Satisfiable for theBenchmark
% 5.24/1.59 % SZS output start Saturation.
% See solution above
% 6.82/1.79 % SZS output start Definitions and Model Updates.
% 6.82/1.79 % SZS output end Definitions and Model Updates.
% 6.82/1.79 % (3318839)------------------------------
% 6.82/1.79 % (3318839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.82/1.79 % (3318839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.82/1.79 % (3318839)CaDiCaL version: 2.1.3
% 6.82/1.79 % (3318839)Termination reason: Satisfiable
% 6.82/1.79 % (3318839)Time elapsed: 0.082 s
% 6.82/1.79 % (3318839)Peak memory usage: 90 MB
% 6.82/1.79 % (3318839)Instructions burned: 153 (million)
% 6.82/1.79 % (3318839)------------------------------
% 6.82/1.79 % (3318839)------------------------------
% 6.82/1.79 % (3318812)Success in time 0.926 s
% 6.82/1.79 % Vampire exiting
%------------------------------------------------------------------------------