%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV532-1.010 : 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 : n011.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:24:55 PM UTC 2026
% Result : Satisfiable 2.71s 1.94s
% Output : Saturation 2.71s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u252,axiom,
i8 != i7 ).
cnf(u257,axiom,
sF0 = select(sF1,i7) ).
cnf(u267,axiom,
sF2 = select(sF39,i8) ).
cnf(u292,axiom,
sF6 = select(sF1,i6) ).
cnf(u296,axiom,
i8 = i6 ).
cnf(u314,axiom,
i8 != i5 ).
cnf(u319,axiom,
sF8 = select(sF5,i5) ).
cnf(u357,axiom,
sF12 = select(sF9,i9) ).
cnf(u361,axiom,
i8 = i9 ).
cnf(u366,axiom,
sF14 = select(sF9,i4) ).
cnf(u369,axiom,
i8 != i4 ).
cnf(u376,axiom,
i5 != i9 ).
cnf(u392,axiom,
i9 != i1 ).
cnf(u397,axiom,
sF16 = select(sF13,i1) ).
cnf(u401,axiom,
i7 != i9 ).
cnf(u406,axiom,
sF18 = select(sF13,i7) ).
cnf(u461,axiom,
sF22 = select(sF17,i4) ).
cnf(u465,axiom,
i7 = i4 ).
cnf(u470,axiom,
sF20 = select(sF17,i5) ).
cnf(u474,axiom,
i7 = i5 ).
cnf(u482,axiom,
i4 = i1 ).
cnf(u495,axiom,
i5 != i0 ).
cnf(u500,axiom,
sF24 = select(sF21,i0) ).
cnf(u536,axiom,
sF27 = select(sF25,i2) ).
cnf(u545,axiom,
sF29 = select(sF25,i1) ).
cnf(u552,axiom,
i0 = i2 ).
cnf(u565,axiom,
i6 != i5 ).
cnf(u570,axiom,
sF8 = select(sF3,i5) ).
cnf(u580,axiom,
i2 = i3 ).
cnf(u635,axiom,
i9 = i0 ).
cnf(u762,axiom,
sF51 = select(sF46,i4) ).
cnf(u1559,axiom,
( select(sF23,X0) = select(sF25,X0)
| i8 = X0 ) ).
cnf(u263,axiom,
( select(sF1,X0) = select(sF39,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u1225,axiom,
sF61 = select(sF63,i8) ).
cnf(u2298,axiom,
sF0 = sF35 ).
cnf(u829,axiom,
sF38 = store(sF36,i7,sF37) ).
cnf(u1916,axiom,
sF0 = select(sF58,i7) ).
cnf(u996,axiom,
sF61 = select(sF67,i7) ).
cnf(u63,axiom,
select(sF26,i1) = sF29 ).
cnf(u2370,axiom,
sF0 = select(sF69,i8) ).
cnf(u1556,axiom,
sF25 = store(sF23,i8,sF24) ).
cnf(u682,axiom,
sF0 = sF6 ).
cnf(u1368,axiom,
sF0 = sF16 ).
cnf(u976,axiom,
sF58 = store(sF56,i7,sF55) ).
cnf(u1362,axiom,
sF54 = store(sF52,i7,sF47) ).
cnf(u1158,axiom,
sF32 = store(sF30,i8,sF2) ).
cnf(u833,axiom,
sF60 = store(sF58,i7,sF59) ).
cnf(u1141,axiom,
sF2 = sF8 ).
cnf(u776,axiom,
sF51 = select(sF52,i8) ).
cnf(u1005,axiom,
sF60 = store(sF58,i7,sF53) ).
cnf(u1437,axiom,
sF61 = select(sF54,i8) ).
cnf(u1794,axiom,
sF0 = select(sF15,i8) ).
cnf(u1718,axiom,
( select(sF26,X0) = select(sF28,X0)
| i7 = X0 ) ).
cnf(u1705,axiom,
( select(sF11,X0) = select(sF13,X0)
| i7 = X0 ) ).
cnf(u1154,axiom,
sF2 = select(sF30,i8) ).
cnf(u2251,axiom,
sF0 = select(sF19,i7) ).
cnf(u2442,axiom,
sF0 = select(sF25,i8) ).
cnf(u772,axiom,
sF72 = select(sF71,i8) ).
cnf(u1715,axiom,
( select(sF65,X0) = select(sF67,X0)
| i7 = X0 ) ).
cnf(u1741,axiom,
sF0 = select(sF44,i8) ).
cnf(u595,axiom,
sF30 = store(sF28,i0,sF29) ).
cnf(u1714,axiom,
sF67 = store(sF65,i7,sF0) ).
cnf(u1119,axiom,
sF64 = select(sF62,i7) ).
cnf(u229,axiom,
( select(sF60,X0) = select(sF62,X0)
| i0 = X0 ) ).
cnf(u1542,axiom,
( select(sF67,X0) = select(sF69,X0)
| i8 = X0 ) ).
cnf(u1059,axiom,
sF35 = select(sF32,i7) ).
cnf(u139,axiom,
store(sF65,i1,sF66) = sF67 ).
cnf(u1880,axiom,
sF0 = select(sF65,i8) ).
cnf(u683,axiom,
sF0 = select(sF42,i8) ).
cnf(u141,axiom,
select(sF67,i0) = sF68 ).
cnf(u1621,axiom,
( select(sF40,X0) = select(sF42,X0)
| i8 = X0 ) ).
cnf(u972,axiom,
sF55 = select(sF58,i7) ).
cnf(u1693,axiom,
( select(sF19,X0) = select(sF21,X0)
| i7 = X0 ) ).
cnf(u835,axiom,
sF22 = select(sF23,i7) ).
cnf(u2161,axiom,
sF0 = sF37 ).
cnf(u135,axiom,
store(sF63,i2,sF64) = sF65 ).
cnf(u1328,axiom,
sF9 = store(sF7,i8,sF0) ).
cnf(u2390,axiom,
sF0 = select(sF34,i8) ).
cnf(u1058,axiom,
sF23 = store(sF21,i7,sF8) ).
cnf(u91,axiom,
select(sF40,i6) = sF43 ).
cnf(u987,axiom,
sF64 = select(sF63,i7) ).
cnf(u957,axiom,
i7 = i1 ).
cnf(u93,axiom,
store(sF42,i8,sF43) = sF44 ).
cnf(u49,axiom,
select(sF19,i4) = sF22 ).
cnf(u1818,axiom,
sF0 = select(sF56,i7) ).
cnf(u828,axiom,
sF35 = select(sF34,i7) ).
cnf(u87,axiom,
select(sF40,i8) = sF41 ).
cnf(u245,axiom,
sF46 = store(sF44,i5,sF43) ).
cnf(u1797,axiom,
sF0 = sF55 ).
cnf(u43,axiom,
store(sF17,i1,sF18) = sF19 ).
cnf(u232,axiom,
( select(sF65,X0) = select(sF67,X0)
| i1 = X0 ) ).
cnf(u73,axiom,
store(sF32,i0,sF33) = sF34 ).
cnf(u25,axiom,
select(sF7,i8) = sF10 ).
cnf(u45,axiom,
select(sF19,i5) = sF20 ).
cnf(u226,axiom,
( select(sF54,X0) = select(sF56,X0)
| i7 = X0 ) ).
cnf(u67,axiom,
select(sF30,i0) = sF31 ).
cnf(u1732,axiom,
( select(sF9,X0) = select(sF11,X0)
| i7 = X0 ) ).
cnf(u677,axiom,
sF74 = select(sF71,i8) ).
cnf(u1142,axiom,
sF9 = store(sF7,i8,sF2) ).
cnf(u985,axiom,
sF54 = store(sF52,i7,sF53) ).
cnf(u39,axiom,
store(sF15,i7,sF16) = sF17 ).
cnf(u228,axiom,
( select(sF58,X0) = select(sF60,X0)
| i5 = X0 ) ).
cnf(u2199,axiom,
sF0 = sF74 ).
cnf(u69,axiom,
store(sF30,i3,sF31) = sF32 ).
cnf(u219,axiom,
( select(sF40,X0) = select(sF42,X0)
| i6 = X0 ) ).
cnf(u184,axiom,
sF51 = select(sF52,i9) ).
cnf(u191,axiom,
sF64 = select(sF65,i2) ).
cnf(u1494,axiom,
( select(sF28,X0) = select(sF30,X0)
| i8 = X0 ) ).
cnf(u178,axiom,
sF0 = select(sF40,i8) ).
cnf(u650,axiom,
sF68 = select(sF67,i9) ).
cnf(u19,axiom,
store(sF5,i8,sF6) = sF7 ).
cnf(u1735,axiom,
sF0 = select(sF7,i8) ).
cnf(u177,axiom,
sF37 = select(sF38,i5) ).
cnf(u180,axiom,
sF43 = select(sF44,i8) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u1686,axiom,
( select(sF44,X0) = select(sF46,X0)
| i7 = X0 ) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u2079,axiom,
sF73 = store(sF71,i8,sF0) ).
cnf(u609,axiom,
sF31 = sF33 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1335,axiom,
sF39 = store(a1,i7,sF0) ).
cnf(u838,axiom,
sF59 = select(sF60,i7) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u802,axiom,
sF53 = select(sF50,i7) ).
cnf(u606,axiom,
sF31 = select(sF32,i0) ).
cnf(u981,axiom,
sF16 = select(sF15,i7) ).
cnf(u2398,axiom,
sF0 = select(sF50,i7) ).
cnf(u1788,axiom,
sF0 = select(sF23,i7) ).
cnf(u1238,axiom,
sF53 = select(sF71,i8) ).
cnf(u1402,axiom,
sF24 = select(sF17,i8) ).
cnf(u1639,axiom,
sF25 = store(sF23,i8,sF0) ).
cnf(u1240,axiom,
sF73 = store(sF71,i8,sF53) ).
cnf(u1670,axiom,
( select(sF50,X0) = select(sF52,X0)
| i8 = X0 ) ).
cnf(u1683,axiom,
( select(sF58,X0) = select(sF60,X0)
| i7 = X0 ) ).
cnf(u2464,axiom,
sF0 = select(sF63,i8) ).
cnf(u1040,axiom,
sF29 = select(sF25,i7) ).
cnf(u309,axiom,
sF5 = store(sF3,i6,sF0) ).
cnf(u648,axiom,
sF62 = store(sF60,i9,sF61) ).
cnf(u661,axiom,
sF31 = select(sF34,i9) ).
cnf(u1034,axiom,
sF17 = store(sF15,i7,sF8) ).
cnf(u655,axiom,
sF61 = select(sF62,i9) ).
cnf(u1192,axiom,
sF61 = select(sF60,i8) ).
cnf(u963,axiom,
sF51 = select(sF48,i7) ).
cnf(u1327,axiom,
sF0 = sF2 ).
cnf(u1666,axiom,
sF63 = store(sF62,i8,sF0) ).
cnf(u1374,axiom,
sF19 = store(sF17,i7,sF0) ).
cnf(u1826,axiom,
sF23 = store(sF21,i7,sF0) ).
cnf(u1665,axiom,
sF62 = store(sF60,i8,sF0) ).
cnf(u644,axiom,
sF26 = store(sF25,i9,sF24) ).
cnf(u1351,axiom,
sF47 = sF53 ).
cnf(u222,axiom,
( select(sF46,X0) = select(sF48,X0)
| i8 = X0 ) ).
cnf(u600,axiom,
sF61 = sF66 ).
cnf(u221,axiom,
( select(sF44,X0) = select(sF46,X0)
| i5 = X0 ) ).
cnf(u1593,axiom,
sF71 = store(sF69,i8,sF0) ).
cnf(u984,axiom,
sF29 = select(sF26,i7) ).
cnf(u607,axiom,
sF68 = select(sF69,i0) ).
cnf(u208,axiom,
( select(sF19,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u215,axiom,
( select(sF32,X0) = select(sF34,X0)
| i0 = X0 ) ).
cnf(u1151,axiom,
sF2 = sF31 ).
cnf(u1574,axiom,
sF63 = store(sF62,i8,sF61) ).
cnf(u202,axiom,
( select(sF7,X0) = select(sF9,X0)
| i8 = X0 ) ).
cnf(u171,axiom,
sF24 = select(sF26,i0) ).
cnf(u596,axiom,
sF65 = store(sF63,i0,sF64) ).
cnf(u201,axiom,
( select(sF5,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u1137,axiom,
sF65 = store(sF63,i8,sF53) ).
cnf(u174,axiom,
sF31 = select(sF32,i3) ).
cnf(u204,axiom,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u173,axiom,
sF29 = select(sF30,i2) ).
cnf(u195,axiom,
sF72 = select(sF73,i6) ).
cnf(u1379,axiom,
sF17 = store(sF15,i7,sF0) ).
cnf(u160,axiom,
sF4 = select(sF5,i6) ).
cnf(u645,axiom,
sF31 = select(sF30,i9) ).
cnf(u198,axiom,
( select(a1,X0) = select(sF39,X0)
| i7 = X0 ) ).
cnf(u780,axiom,
sF47 = sF49 ).
cnf(u167,axiom,
sF18 = select(sF19,i1) ).
cnf(u197,axiom,
( select(a1,X0) = select(sF1,X0)
| i8 = X0 ) ).
cnf(u2450,axiom,
sF0 = select(sF26,i8) ).
cnf(u123,axiom,
select(sF56,i4) = sF59 ).
cnf(u153,axiom,
select(sF71,i6) = sF74 ).
cnf(u1019,axiom,
sF15 = store(sF13,i8,sF0) ).
cnf(u615,axiom,
sF35 = select(sF32,i5) ).
cnf(u156,negated_conjecture,
sF38 != sF75 ).
cnf(u125,axiom,
store(sF58,i5,sF59) = sF60 ).
cnf(u147,axiom,
store(sF69,i0,sF70) = sF71 ).
cnf(u210,axiom,
( select(sF23,X0) = select(sF25,X0)
| i0 = X0 ) ).
cnf(u2231,axiom,
sF0 = select(sF54,i7) ).
cnf(u1644,axiom,
( select(sF13,X0) = select(sF15,X0)
| i8 = X0 ) ).
cnf(u119,axiom,
select(sF56,i5) = sF57 ).
cnf(u970,axiom,
sF14 = select(sF9,i7) ).
cnf(u149,axiom,
select(sF71,i9) = sF72 ).
cnf(u1791,axiom,
sF0 = sF59 ).
cnf(u1863,axiom,
sF0 = select(sF52,i8) ).
cnf(u105,axiom,
store(sF48,i4,sF49) = sF50 ).
cnf(u143,axiom,
store(sF67,i3,sF68) = sF69 ).
cnf(u188,axiom,
sF59 = select(sF60,i5) ).
cnf(u842,axiom,
sF11 = store(sF9,i7,sF0) ).
cnf(u99,axiom,
select(sF44,i5) = sF47 ).
cnf(u129,axiom,
store(sF60,i0,sF61) = sF62 ).
cnf(u1017,axiom,
sF8 = sF20 ).
cnf(u101,axiom,
store(sF46,i8,sF47) = sF48 ).
cnf(u1615,axiom,
( select(sF71,X0) = select(sF73,X0)
| i8 = X0 ) ).
cnf(u1216,axiom,
sF24 = select(sF25,i8) ).
cnf(u57,axiom,
store(sF25,i0,sF24) = sF26 ).
cnf(u1717,axiom,
sF28 = store(sF26,i7,sF0) ).
cnf(u95,axiom,
select(sF44,i8) = sF45 ).
cnf(u1526,axiom,
( select(sF30,X0) = select(sF32,X0)
| i8 = X0 ) ).
cnf(u689,axiom,
sF0 = sF43 ).
cnf(u1163,axiom,
sF53 = select(sF65,i8) ).
cnf(u51,axiom,
store(sF21,i5,sF22) = sF23 ).
cnf(u81,axiom,
store(sF36,i5,sF37) = sF38 ).
cnf(u841,axiom,
sF8 = select(sF5,i7) ).
cnf(u2085,axiom,
sF0 = select(sF73,i8) ).
cnf(u53,axiom,
select(sF23,i0) = sF24 ).
cnf(u686,axiom,
sF42 = store(sF40,i8,sF0) ).
cnf(u1168,axiom,
sF2 = select(sF32,i8) ).
cnf(u980,axiom,
sF13 = store(sF11,i7,sF8) ).
cnf(u47,axiom,
store(sF19,i4,sF20) = sF21 ).
cnf(u1175,axiom,
sF24 = select(sF23,i8) ).
cnf(u1712,axiom,
( select(sF52,X0) = select(sF54,X0)
| i7 = X0 ) ).
cnf(u1847,axiom,
sF0 = sF20 ).
cnf(u826,axiom,
sF20 = select(sF19,i7) ).
cnf(u1117,axiom,
sF61 = select(sF56,i8) ).
cnf(u960,axiom,
sF21 = store(sF19,i7,sF20) ).
cnf(u1811,axiom,
sF56 = store(sF54,i7,sF0) ).
cnf(u75,axiom,
select(sF34,i5) = sF35 ).
cnf(u307,axiom,
sF0 = sF4 ).
cnf(u1070,axiom,
sF47 = select(sF42,i7) ).
cnf(u1571,axiom,
( select(sF60,X0) = select(sF62,X0)
| i8 = X0 ) ).
cnf(u1069,axiom,
sF21 = store(sF19,i7,sF8) ).
cnf(u2470,axiom,
sF0 = select(sF67,i7) ).
cnf(u1701,axiom,
( select(sF48,X0) = select(sF50,X0)
| i7 = X0 ) ).
cnf(u989,axiom,
sF18 = select(sF19,i7) ).
cnf(u884,axiom,
sF50 = store(sF48,i4,sF47) ).
cnf(u1079,axiom,
sF47 = select(sF40,i7) ).
cnf(u680,axiom,
sF72 = select(sF73,i8) ).
cnf(u1066,axiom,
sF35 = select(sF30,i7) ).
cnf(u805,axiom,
sF28 = store(sF26,i1,sF24) ).
cnf(u995,axiom,
sF8 = sF16 ).
cnf(u1654,axiom,
sF0 = sF61 ).
cnf(u1090,axiom,
sF0 = sF51 ).
cnf(u1699,axiom,
sF58 = store(sF56,i7,sF0) ).
cnf(u676,axiom,
sF73 = store(sF71,i8,sF72) ).
cnf(u1696,axiom,
( select(sF56,X0) = select(sF58,X0)
| i7 = X0 ) ).
cnf(u991,axiom,
sF53 = select(sF54,i7) ).
cnf(u33,axiom,
select(sF11,i4) = sF14 ).
cnf(u2146,axiom,
sF0 = select(sF38,i7) ).
cnf(u2380,axiom,
sF0 = select(sF71,i8) ).
cnf(u1677,axiom,
( select(sF21,X0) = select(sF23,X0)
| i7 = X0 ) ).
cnf(u860,axiom,
sF61 = select(sF58,i8) ).
cnf(u247,axiom,
sF6 = select(sF11,i5) ).
cnf(u656,axiom,
sF61 = select(sF63,i9) ).
cnf(u234,axiom,
( select(sF69,X0) = select(sF71,X0)
| i0 = X0 ) ).
cnf(u663,axiom,
sF34 = store(sF32,i9,sF31) ).
cnf(u1657,axiom,
( select(sF34,X0) = select(sF36,X0)
| i8 = X0 ) ).
cnf(u233,axiom,
( select(sF67,X0) = select(sF69,X0)
| i3 = X0 ) ).
cnf(u2330,axiom,
sF0 = select(sF32,i8) ).
cnf(u236,axiom,
( select(sF73,X0) = select(sF75,X0)
| i9 = X0 ) ).
cnf(u1834,axiom,
sF0 = sF22 ).
cnf(u77,axiom,
store(sF34,i9,sF35) = sF36 ).
cnf(u227,axiom,
( select(sF56,X0) = select(sF58,X0)
| i4 = X0 ) ).
cnf(u1321,axiom,
sF0 = sF8 ).
cnf(u1629,axiom,
sF0 = sF24 ).
cnf(u771,axiom,
sF52 = store(sF50,i8,sF51) ).
cnf(u230,axiom,
( select(sF62,X0) = select(sF63,X0)
| i0 = X0 ) ).
cnf(u244,axiom,
sF43 = sF45 ).
cnf(u71,axiom,
select(sF30,i3) = sF33 ).
cnf(u608,axiom,
sF68 = sF70 ).
cnf(u967,axiom,
sF20 = select(sF21,i7) ).
cnf(u186,axiom,
sF55 = select(sF56,i7) ).
cnf(u27,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u216,axiom,
( select(sF34,X0) = select(sF36,X0)
| i9 = X0 ) ).
cnf(u187,axiom,
sF57 = select(sF58,i4) ).
cnf(u185,axiom,
sF53 = select(sF54,i1) ).
cnf(u223,axiom,
( select(sF48,X0) = select(sF50,X0)
| i4 = X0 ) ).
cnf(u850,axiom,
sF46 = store(sF44,i7,sF0) ).
cnf(u29,axiom,
select(sF11,i9) = sF12 ).
cnf(u662,axiom,
sF71 = store(sF69,i9,sF68) ).
cnf(u179,axiom,
sF41 = select(sF42,i6) ).
cnf(u209,axiom,
( select(sF21,X0) = select(sF23,X0)
| i5 = X0 ) ).
cnf(u182,axiom,
sF47 = select(sF48,i8) ).
cnf(u23,axiom,
store(sF7,i8,sF8) = sF9 ).
cnf(u212,axiom,
( select(sF26,X0) = select(sF28,X0)
| i1 = X0 ) ).
cnf(u1680,axiom,
( select(sF36,X0) = select(sF38,X0)
| i7 = X0 ) ).
cnf(u181,axiom,
sF45 = select(sF46,i5) ).
cnf(u203,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u168,axiom,
sF20 = select(sF21,i4) ).
cnf(u9,axiom,
select(a1,i8) = sF2 ).
cnf(u642,axiom,
sF24 = select(sF23,i9) ).
cnf(u175,axiom,
sF33 = select(sF34,i0) ).
cnf(u162,axiom,
sF8 = select(sF9,i8) ).
cnf(u998,axiom,
sF67 = store(sF65,i7,sF61) ).
cnf(u161,axiom,
sF6 = select(sF7,i8) ).
cnf(u1246,axiom,
sF2 = sF37 ).
cnf(u921,axiom,
sF58 = store(sF56,i4,sF55) ).
cnf(u164,axiom,
sF12 = select(sF13,i4) ).
cnf(u5,axiom,
select(a1,i7) = sF0 ).
cnf(u766,axiom,
sF12 = select(sF11,i8) ).
cnf(u1577,axiom,
( select(sF62,X0) = select(sF63,X0)
| i8 = X0 ) ).
cnf(u1248,axiom,
sF2 = select(sF34,i8) ).
cnf(u827,axiom,
sF23 = store(sF21,i7,sF22) ).
cnf(u127,axiom,
select(sF60,i0) = sF61 ).
cnf(u593,axiom,
i0 = i3 ).
cnf(u113,axiom,
store(sF52,i1,sF53) = sF54 ).
cnf(u1432,axiom,
sF0 = sF47 ).
cnf(u1098,axiom,
sF52 = store(sF50,i8,sF0) ).
cnf(u1219,axiom,
sF24 = select(sF26,i8) ).
cnf(u1222,axiom,
sF61 = select(sF62,i8) ).
cnf(u1012,axiom,
sF23 = store(sF21,i7,sF20) ).
cnf(u1207,axiom,
sF53 = select(sF67,i8) ).
cnf(u1499,axiom,
sF30 = store(sF28,i8,sF0) ).
cnf(u774,axiom,
sF14 = select(sF15,i8) ).
cnf(u1359,axiom,
sF0 = sF18 ).
cnf(u643,axiom,
sF25 = store(sF23,i9,sF24) ).
cnf(u653,axiom,
sF24 = select(sF26,i9) ).
cnf(u2314,axiom,
sF0 = select(sF48,i8) ).
cnf(u1781,axiom,
sF60 = store(sF58,i7,sF0) ).
cnf(u1174,axiom,
sF53 = select(sF69,i8) ).
cnf(u849,axiom,
sF0 = select(sF11,i7) ).
cnf(u1568,axiom,
sF62 = store(sF60,i8,sF61) ).
cnf(u1755,axiom,
sF0 = sF45 ).
cnf(u767,axiom,
sF15 = store(sF13,i8,sF14) ).
cnf(u604,axiom,
sF69 = store(sF67,i0,sF68) ).
cnf(u1336,axiom,
sF3 = store(sF1,i7,sF0) ).
cnf(u1132,axiom,
sF53 = sF64 ).
cnf(u1810,axiom,
sF0 = sF53 ).
cnf(u1606,axiom,
sF34 = store(sF32,i8,sF0) ).
cnf(u845,axiom,
sF55 = sF57 ).
cnf(u2282,axiom,
sF36 = store(sF34,i8,sF0) ).
cnf(u206,axiom,
( select(sF15,X0) = select(sF17,X0)
| i7 = X0 ) ).
cnf(u801,axiom,
sF55 = select(sF50,i1) ).
cnf(u747,axiom,
sF47 = select(sF42,i5) ).
cnf(u205,axiom,
( select(sF13,X0) = select(sF15,X0)
| i9 = X0 ) ).
cnf(u83,axiom,
store(a1,i7,sF2) = sF39 ).
cnf(u192,axiom,
sF66 = select(sF67,i1) ).
cnf(u899,axiom,
sF64 = sF68 ).
cnf(u199,axiom,
( select(sF1,X0) = select(sF3,X0)
| i7 = X0 ) ).
cnf(u1084,axiom,
sF30 = store(sF28,i8,sF8) ).
cnf(u768,axiom,
sF36 = store(sF34,i8,sF35) ).
cnf(u155,axiom,
store(sF73,i9,sF74) = sF75 ).
cnf(u220,axiom,
( select(sF42,X0) = select(sF44,X0)
| i8 = X0 ) ).
cnf(u2438,axiom,
sF0 = select(sF3,i7) ).
cnf(u158,axiom,
sF2 = select(sF39,i7) ).
cnf(u978,axiom,
sF20 = sF22 ).
cnf(u157,axiom,
sF0 = select(sF1,i8) ).
cnf(u1709,axiom,
( select(sF17,X0) = select(sF19,X0)
| i7 = X0 ) ).
cnf(u769,axiom,
sF37 = select(sF34,i8) ).
cnf(u151,axiom,
store(sF71,i6,sF72) = sF73 ).
cnf(u688,axiom,
sF5 = store(sF3,i8,sF0) ).
cnf(u1876,axiom,
sF0 = select(sF30,i8) ).
cnf(u2406,axiom,
sF0 = select(sF13,i7) ).
cnf(u107,axiom,
select(sF48,i4) = sF51 ).
cnf(u974,axiom,
sF8 = select(sF13,i7) ).
cnf(u137,axiom,
select(sF63,i2) = sF66 ).
cnf(u109,axiom,
store(sF50,i9,sF51) = sF52 ).
cnf(u131,axiom,
store(sF62,i0,sF61) = sF63 ).
cnf(u207,axiom,
( select(sF17,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u684,axiom,
sF0 = select(sF5,i8) ).
cnf(u1434,axiom,
sF48 = store(sF46,i8,sF0) ).
cnf(u103,axiom,
select(sF48,i9) = sF49 ).
cnf(u133,axiom,
select(sF63,i1) = sF64 ).
cnf(u1515,axiom,
sF65 = store(sF63,i8,sF0) ).
cnf(u59,axiom,
select(sF26,i2) = sF27 ).
cnf(u926,axiom,
sF8 = sF12 ).
cnf(u1806,axiom,
sF0 = select(sF17,i7) ).
cnf(u89,axiom,
store(sF40,i6,sF41) = sF42 ).
cnf(u873,axiom,
sF7 = store(sF5,i8,sF0) ).
cnf(u61,axiom,
store(sF26,i1,sF27) = sF28 ).
cnf(u242,axiom,
sF42 = store(sF40,i6,sF0) ).
cnf(u241,axiom,
sF0 = sF41 ).
cnf(u1739,axiom,
sF0 = sF10 ).
cnf(u55,axiom,
store(sF23,i0,sF24) = sF25 ).
cnf(u906,axiom,
sF69 = store(sF67,i8,sF64) ).
cnf(u85,axiom,
store(sF39,i8,sF0) = sF40 ).
cnf(u41,axiom,
select(sF15,i7) = sF18 ).
cnf(u79,axiom,
select(sF34,i9) = sF37 ).
cnf(u1510,axiom,
( select(sF63,X0) = select(sF65,X0)
| i8 = X0 ) ).
cnf(u2143,axiom,
sF38 = store(sF36,i7,sF0) ).
cnf(u997,axiom,
sF24 = select(sF28,i7) ).
cnf(u35,axiom,
store(sF13,i9,sF14) = sF15 ).
cnf(u1700,axiom,
sF50 = store(sF48,i7,sF0) ).
cnf(u1603,axiom,
( select(sF32,X0) = select(sF34,X0)
| i8 = X0 ) ).
cnf(u65,axiom,
store(sF28,i2,sF29) = sF30 ).
cnf(u1278,axiom,
sF53 = sF74 ).
cnf(u953,axiom,
sF14 = select(sF7,i4) ).
cnf(u2420,axiom,
sF0 = select(sF39,i7) ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u977,axiom,
sF50 = store(sF48,i7,sF47) ).
cnf(u31,axiom,
store(sF11,i4,sF12) = sF13 ).
cnf(u2285,axiom,
sF0 = select(sF36,i8) ).
cnf(u97,axiom,
store(sF44,i5,sF45) = sF46 ).
cnf(u1703,axiom,
sF13 = store(sF11,i7,sF0) ).
cnf(u17,axiom,
select(sF3,i6) = sF6 ).
cnf(u1053,axiom,
sF8 = sF29 ).
cnf(u1550,axiom,
sF69 = store(sF67,i8,sF0) ).
cnf(u777,axiom,
sF74 = select(sF75,i8) ).
cnf(u649,axiom,
sF63 = store(sF62,i9,sF61) ).
cnf(u973,axiom,
sF47 = select(sF50,i7) ).
cnf(u1425,axiom,
sF36 = store(sF34,i8,sF24) ).
cnf(u836,axiom,
sF37 = select(sF38,i7) ).
cnf(u1836,axiom,
sF21 = store(sF19,i7,sF0) ).
cnf(u773,axiom,
sF75 = store(sF73,i8,sF74) ).
cnf(u602,axiom,
sF32 = store(sF30,i0,sF31) ).
cnf(u601,axiom,
sF24 = sF27 ).
cnf(u999,axiom,
sF53 = sF55 ).
cnf(u1250,axiom,
sF38 = store(sF36,i7,sF2) ).
cnf(u2112,axiom,
sF0 = sF72 ).
cnf(u1282,axiom,
sF75 = store(sF73,i8,sF53) ).
cnf(u881,axiom,
sF64 = select(sF62,i1) ).
cnf(u1236,axiom,
sF53 = sF72 ).
cnf(u2476,axiom,
sF0 = select(sF28,i7) ).
cnf(u824,axiom,
sF8 = select(sF7,i7) ).
cnf(u1529,axiom,
sF32 = store(sF30,i8,sF0) ).
cnf(u1208,axiom,
sF53 = sF68 ).
cnf(u979,axiom,
sF0 = sF14 ).
cnf(u1215,axiom,
sF69 = store(sF67,i8,sF53) ).
cnf(u1842,axiom,
sF0 = select(sF21,i7) ).
cnf(u848,axiom,
sF0 = select(sF46,i7) ).
cnf(u235,axiom,
( select(sF71,X0) = select(sF73,X0)
| i6 = X0 ) ).
cnf(u660,axiom,
sF68 = select(sF71,i9) ).
cnf(u1673,axiom,
( select(sF73,X0) = select(sF75,X0)
| i8 = X0 ) ).
cnf(u238,axiom,
sF6 = sF10 ).
cnf(u652,axiom,
sF24 = select(sF25,i9) ).
cnf(u975,axiom,
sF55 = sF59 ).
cnf(u1000,axiom,
sF28 = store(sF26,i7,sF24) ).
cnf(u2456,axiom,
sF0 = select(sF62,i8) ).
cnf(u1822,axiom,
sF54 = store(sF52,i7,sF0) ).
cnf(u224,axiom,
( select(sF50,X0) = select(sF52,X0)
| i9 = X0 ) ).
cnf(u1032,axiom,
sF24 = select(sF19,i8) ).
cnf(u931,axiom,
sF13 = store(sF11,i4,sF8) ).
cnf(u231,axiom,
( select(sF63,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u1039,axiom,
sF56 = store(sF54,i7,sF53) ).
cnf(u775,axiom,
sF35 = select(sF36,i8) ).
cnf(u218,axiom,
( select(sF39,X0) = select(sF40,X0)
| i8 = X0 ) ).
cnf(u647,axiom,
sF61 = select(sF60,i9) ).
cnf(u217,axiom,
( select(sF36,X0) = select(sF38,X0)
| i5 = X0 ) ).
cnf(u1025,axiom,
sF24 = select(sF21,i8) ).
cnf(u190,axiom,
sF61 = select(sF63,i0) ).
cnf(u1782,axiom,
sF0 = select(sF60,i7) ).
cnf(u1010,axiom,
sF8 = sF22 ).
cnf(u239,axiom,
sF11 = store(sF9,i5,sF6) ).
cnf(u189,axiom,
sF61 = select(sF62,i0) ).
cnf(u211,axiom,
( select(sF25,X0) = select(sF26,X0)
| i0 = X0 ) ).
cnf(u176,axiom,
sF35 = select(sF36,i9) ).
cnf(u11,axiom,
store(sF1,i7,sF2) = sF3 ).
cnf(u883,axiom,
sF44 = store(sF42,i8,sF0) ).
cnf(u214,axiom,
( select(sF30,X0) = select(sF32,X0)
| i3 = X0 ) ).
cnf(u183,axiom,
sF49 = select(sF50,i4) ).
cnf(u213,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u1585,axiom,
( select(sF69,X0) = select(sF71,X0)
| i8 = X0 ) ).
cnf(u170,axiom,
sF24 = select(sF25,i0) ).
cnf(u599,axiom,
sF64 = select(sF65,i0) ).
cnf(u200,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u169,axiom,
sF22 = select(sF23,i5) ).
cnf(u225,axiom,
( select(sF52,X0) = select(sF54,X0)
| i1 = X0 ) ).
cnf(u172,axiom,
sF27 = select(sF28,i1) ).
cnf(u13,axiom,
select(sF3,i8) = sF4 ).
cnf(u194,axiom,
sF70 = select(sF71,i0) ).
cnf(u163,axiom,
sF10 = select(sF11,i5) ).
cnf(u1565,axiom,
( select(sF25,X0) = select(sF26,X0)
| i8 = X0 ) ).
cnf(u193,axiom,
sF68 = select(sF69,i3) ).
cnf(u166,axiom,
sF16 = select(sF17,i7) ).
cnf(u7,axiom,
store(a1,i8,sF0) = sF1 ).
cnf(u196,axiom,
sF74 = select(sF75,i9) ).
cnf(u165,axiom,
sF14 = select(sF15,i9) ).
cnf(u121,axiom,
store(sF56,i4,sF57) = sF58 ).
cnf(u2012,axiom,
sF0 = select(sF9,i8) ).
cnf(u1562,axiom,
sF26 = store(sF25,i8,sF24) ).
cnf(u159,axiom,
sF2 = select(sF3,i7) ).
cnf(u831,axiom,
sF47 = select(sF44,i7) ).
cnf(u598,axiom,
sF29 = select(sF30,i0) ).
cnf(u115,axiom,
select(sF52,i1) = sF55 ).
cnf(u982,axiom,
sF19 = store(sF17,i7,sF18) ).
cnf(u145,axiom,
select(sF67,i3) = sF70 ).
cnf(u2186,axiom,
sF0 = select(sF75,i8) ).
cnf(u2180,axiom,
sF75 = store(sF73,i8,sF0) ).
cnf(u1640,axiom,
sF26 = store(sF25,i8,sF0) ).
cnf(u117,axiom,
store(sF54,i7,sF55) = sF56 ).
cnf(u1420,axiom,
sF24 = sF35 ).
cnf(u1631,axiom,
( select(sF3,X0) = select(sF5,X0)
| i8 = X0 ) ).
cnf(u749,axiom,
sF67 = store(sF65,i1,sF61) ).
cnf(u111,axiom,
select(sF52,i7) = sF53 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV532-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n011.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 11:35:01 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 2.71/1.94 % (3337958)Will run a generic schedule for satisfiability detection.
% 2.71/1.94 % (3337965)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2547880371:i=88024:add=on:rawr=on_2988 on theBenchmark for (2988ds/88024Mi)
% 2.71/1.94 % (3337964)% WARNING: option uhcvi not known.
% 2.71/1.94 % (3337963)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=553925165_2988 on theBenchmark for (2988ds/0Mi)
% 2.71/1.94 % (3337966)dis+10_1_sil=32000:sp=arity:random_seed=466434152:i=103:fgj=on_2988 on theBenchmark for (2988ds/103Mi)
% 2.71/1.94 % (3337967)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=16123146:i=116_2988 on theBenchmark for (2988ds/116Mi)
% 2.71/1.94 % (3337964)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2321871266:i=135531:add=off:rawr=on_2988 on theBenchmark for (2988ds/135531Mi)
% 2.71/1.94 % (3337968)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2109869405:i=131_2988 on theBenchmark for (2988ds/131Mi)
% 2.71/1.94 % (3337969)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1015019080:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2988 on theBenchmark for (2988ds/159Mi)
% 2.71/1.94 % TRYING [1]
% 2.71/1.94 % TRYING [2]
% 2.71/1.94 % TRYING [3]
% 2.71/1.94 % TRYING [4]
% 2.71/1.94 % TRYING [5]
% 2.71/1.94 % (3337967)Instruction limit reached!
% 2.71/1.94 % (3337967)------------------------------
% 2.71/1.94 % (3337967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337967)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337967)Termination reason: Instruction limit
% 2.71/1.94 % (3337967)Termination phase: Saturation
% 2.71/1.94 % (3337967)Time elapsed: 0.087 s
% 2.71/1.94 % (3337967)Peak memory usage: 28 MB
% 2.71/1.94 % (3337967)Instructions burned: 116 (million)
% 2.71/1.94 % (3337968)Instruction limit reached!
% 2.71/1.94 % (3337968)------------------------------
% 2.71/1.94 % (3337968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337968)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337968)Termination reason: Instruction limit
% 2.71/1.94 % (3337968)Termination phase: Saturation
% 2.71/1.94 % (3337968)Time elapsed: 0.092 s
% 2.71/1.94 % (3337968)Peak memory usage: 28 MB
% 2.71/1.94 % (3337968)Instructions burned: 132 (million)
% 2.71/1.94 % TRYING [6]
% 2.71/1.94 % (3337969)Instruction limit reached!
% 2.71/1.94 % (3337969)------------------------------
% 2.71/1.94 % (3337969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337969)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337969)Termination reason: Instruction limit
% 2.71/1.94 % (3337969)Termination phase: Saturation
% 2.71/1.94 % (3337969)Time elapsed: 0.103 s
% 2.71/1.94 % (3337969)Peak memory usage: 28 MB
% 2.71/1.94 % (3337969)Instructions burned: 160 (million)
% 2.71/1.94 % (3337977)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3152771524:i=714:nm=2_2987 on theBenchmark for (2987ds/714Mi)
% 2.71/1.94 % (3337978)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3887333893:i=131:bd=preordered:fsd=on_2987 on theBenchmark for (2987ds/131Mi)
% 2.71/1.94 % (3337979)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=824974935:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2987 on theBenchmark for (2987ds/684Mi)
% 2.71/1.94 % (3337978)Instruction limit reached!
% 2.71/1.94 % (3337978)------------------------------
% 2.71/1.94 % (3337978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337978)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337978)Termination reason: Instruction limit
% 2.71/1.94 % (3337978)Termination phase: Saturation
% 2.71/1.94 % (3337978)Time elapsed: 0.065 s
% 2.71/1.94 % (3337978)Peak memory usage: 23 MB
% 2.71/1.94 % (3337978)Instructions burned: 132 (million)
% 2.71/1.94 % (3337983)ott-21_1_sil=16000:fs=off:random_seed=3576949494:i=180:av=off:fsr=off_2986 on theBenchmark for (2986ds/180Mi)
% 2.71/1.94 % TRYING [7]
% 2.71/1.94 % TRYING [1]
% 2.71/1.94 % TRYING [2]
% 2.71/1.94 % TRYING [3]
% 2.71/1.94 % TRYING [4]
% 2.71/1.94 % (3337966)Instruction limit reached!
% 2.71/1.94 % (3337966)------------------------------
% 2.71/1.94 % (3337966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337966)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337966)Termination reason: Instruction limit
% 2.71/1.94 % (3337966)Termination phase: Saturation
% 2.71/1.94 % (3337966)Time elapsed: 0.252 s
% 2.71/1.94 % (3337966)Peak memory usage: 57 MB
% 2.71/1.94 % (3337966)Instructions burned: 104 (million)
% 2.71/1.94 % TRYING [5]
% 2.71/1.94 % (3337985)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3302125391:i=477:bd=all_2986 on theBenchmark for (2986ds/477Mi)
% 2.71/1.94 % (3337983)Instruction limit reached!
% 2.71/1.94 % (3337983)------------------------------
% 2.71/1.94 % (3337983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337983)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337983)Termination reason: Instruction limit
% 2.71/1.94 % (3337983)Termination phase: Saturation
% 2.71/1.94 % (3337983)Time elapsed: 0.074 s
% 2.71/1.94 % (3337983)Peak memory usage: 19 MB
% 2.71/1.94 % (3337983)Instructions burned: 180 (million)
% 2.71/1.94 % (3337987)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1357611679:fmbsr=1.3:i=865:ins=25_2985 on theBenchmark for (2985ds/865Mi)
% 2.71/1.94 % (3337979)Instruction limit reached!
% 2.71/1.94 % (3337979)------------------------------
% 2.71/1.94 % (3337979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337979)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337979)Termination reason: Instruction limit
% 2.71/1.94 % (3337979)Termination phase: Property scanning
% 2.71/1.94 % (3337979)Time elapsed: 0.232 s
% 2.71/1.94 % (3337979)Peak memory usage: 9 MB
% 2.71/1.94 % (3337979)Instructions burned: 684 (million)
% 2.71/1.94 % TRYING [6]
% 2.71/1.94 % (3337989)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3986164327:i=1179_2985 on theBenchmark for (2985ds/1179Mi)
% 2.71/1.94 % (3337977)Instruction limit reached!
% 2.71/1.94 % (3337977)------------------------------
% 2.71/1.94 % (3337977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337977)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337977)Termination reason: Instruction limit
% 2.71/1.94 % (3337977)Termination phase: Finite model building constraint generation
% 2.71/1.94 % (3337977)Time elapsed: 0.284 s
% 2.71/1.94 % (3337977)Peak memory usage: 19 MB
% 2.71/1.94 % (3337977)Instructions burned: 714 (million)
% 2.71/1.94 % (3337991)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3754389460:i=889:ins=1_2984 on theBenchmark for (2984ds/889Mi)
% 2.71/1.94 % (3337989) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3337958-3337989"...
% 2.71/1.94 % (3337989)...printing done.
% 2.71/1.94 % SZS status Satisfiable for theBenchmark
% 2.71/1.94 % SZS output start Saturation.
% See solution above
% 2.71/1.94 % SZS output start Definitions and Model Updates.
% 2.71/1.94 % SZS output end Definitions and Model Updates.
% 2.71/1.94 % (3337989)------------------------------
% 2.71/1.94 % (3337989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/1.94 % (3337989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/1.94 % (3337989)CaDiCaL version: 2.1.3
% 2.71/1.94 % (3337989)Termination reason: Satisfiable
% 2.71/1.94 % (3337989)Time elapsed: 0.169 s
% 2.71/1.94 % (3337989)Peak memory usage: 16 MB
% 2.71/1.94 % (3337989)Instructions burned: 394 (million)
% 2.71/1.94 % (3337958)Success in time 1.697 s
% 2.71/1.94 % Vampire exiting
%------------------------------------------------------------------------------