%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV536-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 SAT
% Computer : n016.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:25:06 PM UTC 2026
% Result : Satisfiable 3.47s 0.91s
% Output : Saturation 3.47s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u177,axiom,
sF0 = select(sF1,i3) ).
cnf(u186,axiom,
i3 != i1 ).
cnf(u191,axiom,
sF4 = select(sF1,i1) ).
cnf(u195,axiom,
i3 != i2 ).
cnf(u200,axiom,
sF6 = select(sF1,i2) ).
cnf(u269,axiom,
sF8 = select(sF5,i5) ).
cnf(u272,axiom,
i3 != i5 ).
cnf(u278,axiom,
sF10 = select(sF5,i0) ).
cnf(u294,axiom,
i1 = i0 ).
cnf(u402,axiom,
i3 != sF48 ).
cnf(u410,axiom,
i2 != i1 ).
cnf(u415,axiom,
sF19 = select(sF17,i2) ).
cnf(u427,axiom,
i2 = sF48 ).
cnf(u445,axiom,
i2 != i0 ).
cnf(u450,axiom,
sF29 = select(sF27,i0) ).
cnf(u531,axiom,
i2 != i6 ).
cnf(u536,axiom,
sF46 = select(sF41,i6) ).
cnf(u551,axiom,
sF50 != select(sF45,sF48) ).
cnf(u908,axiom,
i5 = sF48 ).
cnf(u995,axiom,
sF4 = sF35 ).
cnf(u1005,axiom,
sF4 = sF16 ).
cnf(u1024,axiom,
i2 = i5 ).
cnf(u1042,axiom,
sF8 = sF31 ).
cnf(u1428,axiom,
sF37 = select(sF34,i1) ).
cnf(u1431,axiom,
i1 != sF48 ).
cnf(u1438,axiom,
sF16 = select(sF13,i1) ).
cnf(u1444,axiom,
sF40 = select(sF38,sF48) ).
cnf(u1645,axiom,
sF46 = select(sF38,i6) ).
cnf(u1721,axiom,
sF46 = select(sF36,i6) ).
cnf(u1764,axiom,
sF46 = select(sF30,i6) ).
cnf(u1795,axiom,
sF46 = select(sF3,i6) ).
cnf(u1807,axiom,
i3 = i6 ).
cnf(u97,axiom,
select(sF43,i6) = sF46 ).
cnf(u1505,axiom,
sF26 = store(sF24,sF48,sF14) ).
cnf(u63,axiom,
select(sF28,i0) = sF29 ).
cnf(u1140,axiom,
sF19 = select(sF20,sF48) ).
cnf(u2027,axiom,
sF4 = select(sF43,sF48) ).
cnf(u1596,axiom,
sF4 = sF14 ).
cnf(u1547,axiom,
sF18 = store(sF17,i1,sF4) ).
cnf(u1827,axiom,
sF46 = select(sF36,i3) ).
cnf(u1143,axiom,
sF33 = select(sF34,sF48) ).
cnf(u1160,axiom,
sF21 = sF25 ).
cnf(u1295,axiom,
sF11 = store(sF9,sF48,sF6) ).
cnf(u1714,axiom,
( select(sF30,X0) = select(sF32,X0)
| i1 = X0 ) ).
cnf(u1068,axiom,
sF43 = store(sF41,sF48,sF42) ).
cnf(u123,axiom,
sF29 = select(sF30,i5) ).
cnf(u2021,axiom,
sF4 = select(sF7,i1) ).
cnf(u1059,axiom,
sF14 = select(sF11,sF48) ).
cnf(u139,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u142,axiom,
( select(sF15,X0) = select(sF17,X0)
| i1 = X0 ) ).
cnf(u1061,axiom,
sF22 = store(sF20,sF48,sF21) ).
cnf(u141,axiom,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0 ) ).
cnf(u1854,axiom,
sF4 = select(sF39,i1) ).
cnf(u128,axiom,
sF37 = select(sF39,i1) ).
cnf(u1064,axiom,
sF28 = store(sF27,sF48,sF4) ).
cnf(u2017,axiom,
sF4 = select(sF27,i1) ).
cnf(u1071,axiom,
sF4 = select(sF5,sF48) ).
cnf(u1537,axiom,
sF38 = store(sF36,i1,sF4) ).
cnf(u91,axiom,
store(sF41,i2,sF42) = sF43 ).
cnf(u1817,axiom,
sF4 = select(sF30,sF48) ).
cnf(u93,axiom,
select(sF43,i2) = sF44 ).
cnf(u1860,axiom,
sF4 = select(sF38,i1) ).
cnf(u49,axiom,
store(sF20,i2,sF21) = sF22 ).
cnf(u1534,axiom,
sF4 = select(sF11,i1) ).
cnf(u87,axiom,
store(sF39,i5,sF40) = sF41 ).
cnf(u1752,axiom,
sF46 = select(sF32,i6) ).
cnf(u43,axiom,
select(sF18,i2) = sF19 ).
cnf(u73,axiom,
store(sF32,i5,sF33) = sF34 ).
cnf(u1699,axiom,
sF4 = sF42 ).
cnf(u1845,axiom,
sF47 = store(sF45,sF48,sF2) ).
cnf(u45,axiom,
store(sF18,i5,sF19) = sF20 ).
cnf(u2039,axiom,
sF4 = sF25 ).
cnf(u67,axiom,
select(sF28,i5) = sF31 ).
cnf(u39,axiom,
store(sF15,i1,sF16) = sF17 ).
cnf(u1832,axiom,
sF46 = select(sF27,i3) ).
cnf(u69,axiom,
store(sF30,i0,sF31) = sF32 ).
cnf(u25,axiom,
select(sF7,i0) = sF10 ).
cnf(u1494,axiom,
sF4 = select(sF13,i1) ).
cnf(u19,axiom,
store(sF5,i1,sF6) = sF7 ).
cnf(u1844,axiom,
sF4 = select(sF11,sF48) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u2040,axiom,
sF4 = sF49 ).
cnf(u1868,axiom,
sF4 = select(sF41,sF48) ).
cnf(u15,axiom,
store(sF3,i2,sF4) = sF5 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1687,axiom,
( select(sF11,X0) = select(sF13,X0)
| sF48 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u125,axiom,
sF33 = select(sF34,i5) ).
cnf(u1788,axiom,
( select(sF39,X0) = select(sF41,X0)
| sF48 = X0 ) ).
cnf(u1076,axiom,
sF35 = select(sF36,sF48) ).
cnf(u1238,axiom,
sF33 = sF35 ).
cnf(u1057,axiom,
sF6 = select(sF3,sF48) ).
cnf(u1632,axiom,
sF4 != sF46 ).
cnf(u2151,axiom,
sF2 = select(sF47,sF48) ).
cnf(u1247,axiom,
sF29 = sF33 ).
cnf(u106,negated_conjecture,
sF49 != sF50 ).
cnf(u1826,axiom,
sF46 = select(sF38,i3) ).
cnf(u1665,axiom,
( select(sF27,X0) = select(sF28,X0)
| sF48 = X0 ) ).
cnf(u1139,axiom,
sF14 = select(sF15,sF48) ).
cnf(u1142,axiom,
sF29 = select(sF30,sF48) ).
cnf(u1493,axiom,
sF4 = select(sF34,i1) ).
cnf(u2133,axiom,
sF4 = select(sF15,sF48) ).
cnf(u1144,axiom,
sF40 = select(sF41,sF48) ).
cnf(u1151,axiom,
sF21 = select(sF24,sF48) ).
cnf(u1574,axiom,
sF45 = store(sF43,i6,sF4) ).
cnf(u1138,axiom,
sF10 = select(sF11,sF48) ).
cnf(u1769,axiom,
( select(sF28,X0) = select(sF30,X0)
| sF48 = X0 ) ).
cnf(u160,axiom,
sF10 = sF12 ).
cnf(u167,axiom,
sF45 = store(sF43,i6,sF42) ).
cnf(u1395,axiom,
sF27 = store(sF3,i1,sF4) ).
cnf(u154,axiom,
( select(sF38,X0) = select(sF39,X0)
| i1 = X0 ) ).
cnf(u1864,axiom,
sF4 = sF10 ).
cnf(u153,axiom,
( select(sF36,X0) = select(sF38,X0)
| i1 = X0 ) ).
cnf(u126,axiom,
sF35 = select(sF36,i2) ).
cnf(u1849,axiom,
sF20 = store(sF18,sF48,sF4) ).
cnf(u156,axiom,
( select(sF41,X0) = select(sF43,X0)
| i2 = X0 ) ).
cnf(u147,axiom,
( select(sF24,X0) = select(sF26,X0)
| i2 = X0 ) ).
cnf(u112,axiom,
sF8 = select(sF9,i0) ).
cnf(u2048,axiom,
sF4 = sF21 ).
cnf(u150,axiom,
( select(sF30,X0) = select(sF32,X0)
| i0 = X0 ) ).
cnf(u119,axiom,
sF21 = select(sF22,i2) ).
cnf(u149,axiom,
( select(sF28,X0) = select(sF30,X0)
| i5 = X0 ) ).
cnf(u1830,axiom,
sF46 = select(sF30,i3) ).
cnf(u1829,axiom,
sF46 = select(sF32,i3) ).
cnf(u136,axiom,
( select(sF3,X0) = select(sF27,X0)
| i1 = X0 ) ).
cnf(u105,axiom,
select(sF47,sF48) = sF50 ).
cnf(u143,axiom,
( select(sF17,X0) = select(sF18,X0)
| i1 = X0 ) ).
cnf(u108,axiom,
sF2 = select(sF3,i3) ).
cnf(u1709,axiom,
sF43 = store(sF41,sF48,sF4) ).
cnf(u130,axiom,
sF42 = select(sF43,i2) ).
cnf(u99,axiom,
store(sF45,i2,sF46) = sF47 ).
cnf(u129,axiom,
sF40 = select(sF41,i5) ).
cnf(u1755,axiom,
( select(sF18,X0) = select(sF20,X0)
| sF48 = X0 ) ).
cnf(u1825,axiom,
sF46 = select(sF39,i3) ).
cnf(u132,axiom,
sF46 = select(sF47,i2) ).
cnf(u101,axiom,
sk(sF26,sF47) = sF48 ).
cnf(u1564,axiom,
sF24 = store(sF22,sF48,sF14) ).
cnf(u2035,axiom,
sF4 = select(sF26,sF48) ).
cnf(u57,axiom,
store(sF24,i2,sF25) = sF26 ).
cnf(u95,axiom,
store(sF43,i6,sF44) = sF45 ).
cnf(u51,axiom,
select(sF22,i2) = sF23 ).
cnf(u81,axiom,
store(sF36,i1,sF37) = sF38 ).
cnf(u1707,axiom,
sF4 = select(sF34,sF48) ).
cnf(u53,axiom,
store(sF22,i5,sF23) = sF24 ).
cnf(u1522,axiom,
sF4 = sF33 ).
cnf(u47,axiom,
select(sF18,i5) = sF21 ).
cnf(u1540,axiom,
sF41 = store(sF39,sF48,sF4) ).
cnf(u1161,axiom,
sF24 = store(sF22,sF48,sF21) ).
cnf(u1659,axiom,
( select(sF24,X0) = select(sF26,X0)
| sF48 = X0 ) ).
cnf(u1276,axiom,
sF6 = sF10 ).
cnf(u1852,axiom,
sF4 = select(sF20,sF48) ).
cnf(u1127,axiom,
sF15 = store(sF13,sF48,sF14) ).
cnf(u1269,axiom,
sF10 = select(sF5,i1) ).
cnf(u1536,axiom,
sF39 = store(sF38,i1,sF4) ).
cnf(u1067,axiom,
sF40 = select(sF39,sF48) ).
cnf(u77,axiom,
store(sF34,i2,sF35) = sF36 ).
cnf(u1272,axiom,
sF6 = sF29 ).
cnf(u1070,axiom,
sF47 = store(sF45,sF48,sF46) ).
cnf(u1746,axiom,
( select(sF13,X0) = select(sF15,X0)
| sF48 = X0 ) ).
cnf(u1100,axiom,
sF10 = select(sF13,sF48) ).
cnf(u1265,axiom,
sF29 = select(sF28,i1) ).
cnf(u1354,axiom,
sF36 = store(sF34,sF48,sF6) ).
cnf(u1252,axiom,
sF34 = store(sF32,sF48,sF29) ).
cnf(u1243,axiom,
sF29 = sF35 ).
cnf(u1066,axiom,
sF36 = store(sF34,sF48,sF35) ).
cnf(u1065,axiom,
sF33 = select(sF32,sF48) ).
cnf(u1697,axiom,
sF4 = select(sF36,sF48) ).
cnf(u1653,axiom,
( select(sF20,X0) = select(sF22,X0)
| sF48 = X0 ) ).
cnf(u1525,axiom,
sF36 = store(sF34,sF48,sF4) ).
cnf(u1678,axiom,
( select(sF41,X0) = select(sF43,X0)
| sF48 = X0 ) ).
cnf(u1838,axiom,
sF45 = store(sF43,i3,sF4) ).
cnf(u2068,axiom,
sF4 = select(sF24,sF48) ).
cnf(u75,axiom,
select(sF32,i5) = sF35 ).
cnf(u1834,axiom,
sF2 = sF46 ).
cnf(u1630,axiom,
sF46 = sF50 ).
cnf(u33,axiom,
select(sF11,i2) = sF14 ).
cnf(u71,axiom,
select(sF32,i2) = sF33 ).
cnf(u27,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u1743,axiom,
sF46 = select(sF34,i6) ).
cnf(u1367,axiom,
sF14 = sF49 ).
cnf(u29,axiom,
select(sF11,i5) = sF12 ).
cnf(u23,axiom,
store(sF7,i0,sF8) = sF9 ).
cnf(u9,axiom,
select(a1,i4) = sF2 ).
cnf(u161,axiom,
sF13 = store(sF11,i2,sF10) ).
cnf(u1828,axiom,
sF46 = select(sF34,i3) ).
cnf(u164,axiom,
sF24 = store(sF22,i5,sF21) ).
cnf(u5,axiom,
select(a1,i3) = sF0 ).
cnf(u120,axiom,
sF23 = select(sF24,i5) ).
cnf(u594,axiom,
sF6 = select(sF1,sF48) ).
cnf(u127,axiom,
sF37 = select(sF38,i1) ).
cnf(u1282,axiom,
sF14 = sF19 ).
cnf(u114,axiom,
sF12 = select(sF13,i2) ).
cnf(u1824,axiom,
sF4 = select(sF45,i3) ).
cnf(u113,axiom,
sF10 = select(sF11,i5) ).
cnf(u1241,axiom,
sF10 = select(sF3,i0) ).
cnf(u2148,axiom,
( select(sF43,X0) = select(sF45,X0)
| i3 = X0 ) ).
cnf(u1627,axiom,
sF4 != sF50 ).
cnf(u1392,axiom,
sF4 = sF6 ).
cnf(u1147,axiom,
sF4 = sF8 ).
cnf(u1180,axiom,
sF19 = select(sF17,sF48) ).
cnf(u1724,axiom,
( select(sF7,X0) = select(sF9,X0)
| i1 = X0 ) ).
cnf(u1568,axiom,
sF34 = store(sF32,sF48,sF4) ).
cnf(u1453,axiom,
sF43 = store(sF41,sF48,sF40) ).
cnf(u1132,axiom,
sF30 = store(sF28,sF48,sF29) ).
cnf(u1203,axiom,
sF19 = sF21 ).
cnf(u1125,axiom,
sF11 = store(sF9,sF48,sF10) ).
cnf(u1275,axiom,
sF32 = store(sF30,i1,sF4) ).
cnf(u1622,axiom,
sF15 = store(sF13,sF48,sF4) ).
cnf(u1128,axiom,
sF20 = store(sF18,sF48,sF19) ).
cnf(u1602,axiom,
i6 != sF48 ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u1075,axiom,
sF4 = select(sF28,sF48) ).
cnf(u155,axiom,
( select(sF39,X0) = select(sF41,X0)
| i5 = X0 ) ).
cnf(u1737,axiom,
( select(sF9,X0) = select(sF11,X0)
| sF48 = X0 ) ).
cnf(u1078,axiom,
sF46 = select(sF47,sF48) ).
cnf(u158,axiom,
( select(sF45,X0) = select(sF47,X0)
| i2 = X0 ) ).
cnf(u1108,axiom,
sF13 = store(sF11,sF48,sF10) ).
cnf(u1077,axiom,
sF42 = select(sF43,sF48) ).
cnf(u157,axiom,
( select(sF43,X0) = select(sF45,X0)
| i6 = X0 ) ).
cnf(u144,axiom,
( select(sF18,X0) = select(sF20,X0)
| i5 = X0 ) ).
cnf(u151,axiom,
( select(sF32,X0) = select(sF34,X0)
| i5 = X0 ) ).
cnf(u116,axiom,
sF16 = select(sF17,i1) ).
cnf(u138,axiom,
( select(sF7,X0) = select(sF9,X0)
| i0 = X0 ) ).
cnf(u1074,axiom,
sF25 = select(sF26,sF48) ).
cnf(u107,axiom,
sF0 = select(sF1,i4) ).
cnf(u137,axiom,
( select(sF5,X0) = select(sF7,X0)
| i1 = X0 ) ).
cnf(u110,axiom,
sF6 = select(sF27,i1) ).
cnf(u140,axiom,
( select(sF11,X0) = select(sF13,X0)
| i2 = X0 ) ).
cnf(u109,axiom,
sF4 = select(sF5,i2) ).
cnf(u131,axiom,
sF44 = select(sF45,i6) ).
cnf(u134,axiom,
( select(sF1,X0) = select(sF3,X0)
| i3 = X0 ) ).
cnf(u103,axiom,
select(sF26,sF48) = sF49 ).
cnf(u133,axiom,
( select(a1,X0) = select(sF1,X0)
| i4 = X0 ) ).
cnf(u59,axiom,
store(sF3,i1,sF6) = sF27 ).
cnf(u1775,axiom,
sF46 = select(sF28,i6) ).
cnf(u89,axiom,
select(sF39,i5) = sF42 ).
cnf(u61,axiom,
store(sF27,i2,sF4) = sF28 ).
cnf(u83,axiom,
store(sF38,i1,sF37) = sF39 ).
cnf(u55,axiom,
select(sF22,i5) = sF25 ).
cnf(u85,axiom,
select(sF39,i2) = sF40 ).
cnf(u1548,axiom,
sF17 = store(sF15,i1,sF4) ).
cnf(u41,axiom,
store(sF17,i1,sF16) = sF18 ).
cnf(u79,axiom,
select(sF36,i1) = sF37 ).
cnf(u35,axiom,
store(sF13,i5,sF14) = sF15 ).
cnf(u65,axiom,
store(sF28,i5,sF29) = sF30 ).
cnf(u1691,axiom,
sF4 = sF44 ).
cnf(u1277,axiom,
sF9 = store(sF7,i1,sF4) ).
cnf(u1544,axiom,
sF30 = store(sF28,sF48,sF4) ).
cnf(u2056,axiom,
sF4 = select(sF17,i1) ).
cnf(u1608,axiom,
sF4 = select(sF45,i6) ).
cnf(u1506,axiom,
sF22 = store(sF20,sF48,sF14) ).
cnf(u1884,axiom,
sF4 = select(sF13,sF48) ).
cnf(u31,axiom,
store(sF11,i2,sF12) = sF13 ).
cnf(u1492,axiom,
sF4 = sF40 ).
cnf(u1831,axiom,
sF46 = select(sF28,i3) ).
cnf(u1274,axiom,
sF4 = select(sF9,i1) ).
cnf(u1703,axiom,
( select(sF32,X0) = select(sF34,X0)
| sF48 = X0 ) ).
cnf(u17,axiom,
select(sF3,i2) = sF6 ).
cnf(u1273,axiom,
sF4 = select(sF32,i1) ).
cnf(u1292,axiom,
sF4 = sF37 ).
cnf(u2167,axiom,
sF2 = sF50 ).
cnf(u1073,axiom,
sF21 = select(sF22,sF48) ).
cnf(u1060,axiom,
sF19 = select(sF18,sF48) ).
cnf(u1648,axiom,
( select(sF3,X0) = select(sF5,X0)
| sF48 = X0 ) ).
cnf(u1799,axiom,
( select(sF22,X0) = select(sF24,X0)
| sF48 = X0 ) ).
cnf(u1250,axiom,
sF36 = store(sF34,sF48,sF29) ).
cnf(u1056,axiom,
sF5 = store(sF3,sF48,sF4) ).
cnf(u2042,axiom,
sF22 = store(sF20,sF48,sF4) ).
cnf(u1881,axiom,
sF4 = sF19 ).
cnf(u1063,axiom,
sF26 = store(sF24,sF48,sF25) ).
cnf(u1205,axiom,
sF4 = select(sF7,sF48) ).
cnf(u1555,axiom,
sF13 = store(sF11,sF48,sF4) ).
cnf(u1396,axiom,
sF7 = store(sF5,i1,sF4) ).
cnf(u1529,axiom,
sF20 = store(sF18,sF48,sF14) ).
cnf(u1682,axiom,
( select(sF45,X0) = select(sF47,X0)
| sF48 = X0 ) ).
cnf(u1507,axiom,
sF4 = sF29 ).
cnf(u1202,axiom,
sF4 = sF31 ).
cnf(u111,axiom,
sF6 = select(sF7,i1) ).
cnf(u1201,axiom,
sF40 = sF42 ).
cnf(u1822,axiom,
sF46 = select(sF41,i3) ).
cnf(u1819,axiom,
sF46 = select(sF43,i3) ).
cnf(u2058,axiom,
sF24 = store(sF22,sF48,sF4) ).
cnf(u1785,axiom,
sF46 = select(sF27,i6) ).
cnf(u1134,axiom,
sF34 = store(sF32,sF48,sF33) ).
cnf(u2052,axiom,
sF4 = select(sF18,i1) ).
cnf(u1136,axiom,
sF41 = store(sF39,sF48,sF40) ).
cnf(u11,axiom,
store(sF1,i3,sF2) = sF3 ).
cnf(u1285,axiom,
sF30 = store(sF28,sF48,sF6) ).
cnf(u1846,axiom,
sF2 != sF4 ).
cnf(u13,axiom,
select(sF3,i1) = sF4 ).
cnf(u2045,axiom,
sF4 = select(sF22,sF48) ).
cnf(u163,axiom,
sF21 = sF23 ).
cnf(u166,axiom,
sF42 = sF44 ).
cnf(u7,axiom,
store(a1,i4,sF0) = sF1 ).
cnf(u1672,axiom,
( select(sF34,X0) = select(sF36,X0)
| sF48 = X0 ) ).
cnf(u122,axiom,
sF4 = select(sF28,i2) ).
cnf(u152,axiom,
( select(sF34,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u121,axiom,
sF25 = select(sF26,i2) ).
cnf(u1619,axiom,
sF46 = select(sF39,i6) ).
cnf(u124,axiom,
sF31 = select(sF32,i0) ).
cnf(u146,axiom,
( select(sF22,X0) = select(sF24,X0)
| i5 = X0 ) ).
cnf(u115,axiom,
sF14 = select(sF15,i5) ).
cnf(u145,axiom,
( select(sF20,X0) = select(sF22,X0)
| i2 = X0 ) ).
cnf(u1230,axiom,
i0 != sF48 ).
cnf(u118,axiom,
sF19 = select(sF20,i5) ).
cnf(u135,axiom,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u1841,axiom,
sF11 = store(sF9,sF48,sF4) ).
cnf(u148,axiom,
( select(sF27,X0) = select(sF28,X0)
| i2 = X0 ) ).
cnf(u117,axiom,
sF16 = select(sF18,i1) ).
cnf(u2032,axiom,
sF26 = store(sF24,sF48,sF4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV536-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n016.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 11:40:49 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.25 Running first-order model finding
% 0.10/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.47/0.91 % (3573702)Will run a generic schedule for satisfiability detection.
% 3.47/0.91 % (3573707)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=900201261_2998 on theBenchmark for (2998ds/0Mi)
% 3.47/0.91 % TRYING [1]
% 3.47/0.91 % TRYING [2]
% 3.47/0.91 % (3573708)% WARNING: option uhcvi not known.
% 3.47/0.91 % TRYING [3]
% 3.47/0.91 % TRYING [4]
% 3.47/0.91 % (3573708)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3903447565:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 3.47/0.91 % (3573709)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1705601917:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 3.47/0.91 % (3573710)dis+10_1_sil=32000:sp=arity:random_seed=475914537:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 3.47/0.91 % (3573711)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3474135124:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 3.47/0.91 % (3573712)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2261150510:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 3.47/0.91 % (3573713)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3576187226:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 3.47/0.91 % TRYING [5]
% 3.47/0.91 % TRYING [6]
% 3.47/0.91 % (3573711)Instruction limit reached!
% 3.47/0.91 % (3573711)------------------------------
% 3.47/0.91 % (3573711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573711)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573711)Termination reason: Instruction limit
% 3.47/0.91 % (3573711)Termination phase: Saturation
% 3.47/0.91 % (3573711)Time elapsed: 0.048 s
% 3.47/0.91 % (3573711)Peak memory usage: 13 MB
% 3.47/0.91 % (3573711)Instructions burned: 116 (million)
% 3.47/0.91 % (3573712)Instruction limit reached!
% 3.47/0.91 % (3573712)------------------------------
% 3.47/0.91 % (3573712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573712)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573712)Termination reason: Instruction limit
% 3.47/0.91 % (3573712)Termination phase: Saturation
% 3.47/0.91 % (3573712)Time elapsed: 0.053 s
% 3.47/0.91 % (3573712)Peak memory usage: 13 MB
% 3.47/0.91 % (3573712)Instructions burned: 134 (million)
% 3.47/0.91 % (3573721)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2501516844:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 3.47/0.91 % TRYING [7]
% 3.47/0.91 % (3573722)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2515304444:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 3.47/0.91 % (3573713)Instruction limit reached!
% 3.47/0.91 % (3573713)------------------------------
% 3.47/0.91 % (3573713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573713)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573713)Termination reason: Instruction limit
% 3.47/0.91 % (3573713)Termination phase: Saturation
% 3.47/0.91 % (3573713)Time elapsed: 0.074 s
% 3.47/0.91 % (3573713)Peak memory usage: 17 MB
% 3.47/0.91 % (3573713)Instructions burned: 159 (million)
% 3.47/0.91 % (3573710)Instruction limit reached!
% 3.47/0.91 % (3573710)------------------------------
% 3.47/0.91 % (3573710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573710)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573710)Termination reason: Instruction limit
% 3.47/0.91 % (3573710)Termination phase: Saturation
% 3.47/0.91 % (3573710)Time elapsed: 0.078 s
% 3.47/0.91 % (3573710)Peak memory usage: 17 MB
% 3.47/0.91 % (3573710)Instructions burned: 104 (million)
% 3.47/0.91 % TRYING [1]
% 3.47/0.91 % TRYING [2]
% 3.47/0.91 % TRYING [3]
% 3.47/0.91 % TRYING [4]
% 3.47/0.91 % (3573725)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2030657773:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 3.47/0.91 % (3573726)ott-21_1_sil=16000:fs=off:random_seed=2372419414:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 3.47/0.91 % TRYING [5]
% 3.47/0.91 % (3573722)Instruction limit reached!
% 3.47/0.91 % (3573722)------------------------------
% 3.47/0.91 % (3573722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573722)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573722)Termination reason: Instruction limit
% 3.47/0.91 % (3573722)Termination phase: Saturation
% 3.47/0.91 % (3573722)Time elapsed: 0.079 s
% 3.47/0.91 % (3573722)Peak memory usage: 19 MB
% 3.47/0.91 % (3573722)Instructions burned: 131 (million)
% 3.47/0.91 % (3573726)Instruction limit reached!
% 3.47/0.91 % (3573726)------------------------------
% 3.47/0.91 % (3573726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573726)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573726)Termination reason: Instruction limit
% 3.47/0.91 % (3573726)Termination phase: Saturation
% 3.47/0.91 % (3573726)Time elapsed: 0.066 s
% 3.47/0.91 % (3573726)Peak memory usage: 12 MB
% 3.47/0.91 % (3573726)Instructions burned: 183 (million)
% 3.47/0.91 % (3573729)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3964499336:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 3.47/0.91 % (3573730)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=818375827:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 3.47/0.91 % TRYING [6]
% 3.47/0.91 % TRYING [1]
% 3.47/0.91 % TRYING [2]
% 3.47/0.91 % TRYING [3]
% 3.47/0.91 % TRYING [8]
% 3.47/0.91 % TRYING [4]
% 3.47/0.91 % TRYING [5]
% 3.47/0.91 % (3573721)Instruction limit reached!
% 3.47/0.91 % (3573721)------------------------------
% 3.47/0.91 % (3573721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573721)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573721)Termination reason: Instruction limit
% 3.47/0.91 % (3573721)Termination phase: Finite model building SAT solving
% 3.47/0.91 % (3573721)Time elapsed: 0.336 s
% 3.47/0.91 % (3573721)Peak memory usage: 23 MB
% 3.47/0.91 % (3573721)Instructions burned: 716 (million)
% 3.47/0.91 % TRYING [6]
% 3.47/0.91 % (3573733)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1621235915:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 3.47/0.91 % (3573733) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3573702-3573733"...
% 3.47/0.91 % (3573730)Instruction limit reached!
% 3.47/0.91 % (3573730)------------------------------
% 3.47/0.91 % (3573730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573730)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573730)Termination reason: Instruction limit
% 3.47/0.91 % (3573730)Termination phase: Finite model building SAT solving
% 3.47/0.91 % (3573730)Time elapsed: 0.298 s
% 3.47/0.91 % (3573730)Peak memory usage: 16 MB
% 3.47/0.91 % (3573730)Instructions burned: 865 (million)
% 3.47/0.91 % (3573733)...printing done.
% 3.47/0.91 % SZS status Satisfiable for theBenchmark
% 3.47/0.91 % SZS output start Saturation.
% See solution above
% 3.47/0.91 % SZS output start Definitions and Model Updates.
% 3.47/0.91 % SZS output end Definitions and Model Updates.
% 3.47/0.91 % (3573733)------------------------------
% 3.47/0.91 % (3573733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.91 % (3573733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.91 % (3573733)CaDiCaL version: 2.1.3
% 3.47/0.91 % (3573733)Termination reason: Satisfiable
% 3.47/0.91 % (3573733)Time elapsed: 0.056 s
% 3.47/0.91 % (3573733)Peak memory usage: 12 MB
% 3.47/0.91 % (3573733)Instructions burned: 108 (million)
% 3.47/0.91 % (3573702)Success in time 0.646 s
% 3.47/0.91 % Vampire exiting
%------------------------------------------------------------------------------