%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV531-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 : n004.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:54 PM UTC 2026
% Result : Satisfiable 2.72s 1.96s
% Output : Saturation 2.72s
% 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(u360,axiom,
sF12 = select(sF9,i9) ).
cnf(u364,axiom,
i8 = i9 ).
cnf(u369,axiom,
sF14 = select(sF9,i4) ).
cnf(u372,axiom,
i8 != i4 ).
cnf(u379,axiom,
i5 != i9 ).
cnf(u395,axiom,
i9 != i1 ).
cnf(u400,axiom,
sF16 = select(sF13,i1) ).
cnf(u404,axiom,
i7 != i9 ).
cnf(u409,axiom,
sF18 = select(sF13,i7) ).
cnf(u464,axiom,
sF22 = select(sF17,i4) ).
cnf(u468,axiom,
i7 = i4 ).
cnf(u473,axiom,
sF20 = select(sF17,i5) ).
cnf(u477,axiom,
i7 = i5 ).
cnf(u485,axiom,
i4 = i1 ).
cnf(u498,axiom,
i5 != i0 ).
cnf(u503,axiom,
sF24 = select(sF21,i0) ).
cnf(u539,axiom,
sF27 = select(sF25,i2) ).
cnf(u548,axiom,
sF29 = select(sF25,i1) ).
cnf(u555,axiom,
i0 = i2 ).
cnf(u568,axiom,
i6 != i5 ).
cnf(u573,axiom,
sF8 = select(sF3,i5) ).
cnf(u583,axiom,
i2 = i3 ).
cnf(u638,axiom,
i9 = i0 ).
cnf(u768,axiom,
sF51 = select(sF46,i4) ).
cnf(u1226,axiom,
sF53 = select(sF67,i8) ).
cnf(u1582,axiom,
( select(sF60,X0) = select(sF62,X0)
| i8 = X0 ) ).
cnf(u1604,axiom,
sF71 = store(sF69,i8,sF0) ).
cnf(u97,axiom,
store(sF44,i5,sF45) = sF46 ).
cnf(u1182,axiom,
sF53 = select(sF65,i8) ).
cnf(u1837,axiom,
sF23 = store(sF21,i7,sF0) ).
cnf(u857,axiom,
sF0 = select(sF46,i7) ).
cnf(u890,axiom,
sF64 = select(sF62,i1) ).
cnf(u1576,axiom,
( select(sF25,X0) = select(sF26,X0)
| i8 = X0 ) ).
cnf(u2298,axiom,
sF0 = sF35 ).
cnf(u1505,axiom,
( select(sF28,X0) = select(sF30,X0)
| i8 = X0 ) ).
cnf(u779,axiom,
sF75 = store(sF73,i8,sF74) ).
cnf(u996,axiom,
sF18 = select(sF19,i7) ).
cnf(u63,axiom,
select(sF26,i1) = sF29 ).
cnf(u2370,axiom,
sF0 = select(sF71,i8) ).
cnf(u682,axiom,
sF0 = sF6 ).
cnf(u1710,axiom,
sF13 = store(sF11,i7,sF0) ).
cnf(u755,axiom,
sF67 = store(sF65,i1,sF61) ).
cnf(u1887,axiom,
sF0 = select(sF75,i8) ).
cnf(u1005,axiom,
sF67 = store(sF65,i7,sF61) ).
cnf(u1234,axiom,
sF69 = store(sF67,i8,sF53) ).
cnf(u833,axiom,
sF23 = store(sF21,i7,sF22) ).
cnf(u2138,axiom,
sF0 = sF72 ).
cnf(u1160,axiom,
sF2 = sF8 ).
cnf(u1086,axiom,
sF47 = select(sF40,i7) ).
cnf(u2448,axiom,
sF0 = select(sF39,i7) ).
cnf(u928,axiom,
sF58 = store(sF56,i4,sF55) ).
cnf(u2251,axiom,
sF0 = select(sF19,i7) ).
cnf(u684,axiom,
sF0 = select(sF5,i8) ).
cnf(u1447,axiom,
sF48 = store(sF46,i8,sF0) ).
cnf(u772,axiom,
sF12 = select(sF11,i8) ).
cnf(u1742,axiom,
sF0 = select(sF7,i8) ).
cnf(u1561,axiom,
sF69 = store(sF67,i8,sF0) ).
cnf(u1259,axiom,
sF73 = store(sF71,i7,sF53) ).
cnf(u1893,axiom,
sF0 = select(sF30,i8) ).
cnf(u1902,axiom,
sF0 = sF74 ).
cnf(u2276,axiom,
sF36 = store(sF34,i8,sF0) ).
cnf(u924,axiom,
sF74 = select(sF69,i7) ).
cnf(u1411,axiom,
sF24 = select(sF17,i8) ).
cnf(u781,axiom,
sF35 = select(sF36,i8) ).
cnf(u139,axiom,
store(sF65,i1,sF66) = sF67 ).
cnf(u1105,axiom,
sF52 = store(sF50,i8,sF0) ).
cnf(u683,axiom,
sF0 = select(sF42,i8) ).
cnf(u141,axiom,
select(sF67,i0) = sF68 ).
cnf(u1693,axiom,
( select(sF44,X0) = select(sF46,X0)
| i7 = X0 ) ).
cnf(u835,axiom,
sF38 = store(sF36,i7,sF37) ).
cnf(u135,axiom,
store(sF63,i2,sF64) = sF65 ).
cnf(u1363,axiom,
sF54 = store(sF52,i7,sF47) ).
cnf(u807,axiom,
sF55 = select(sF50,i1) ).
cnf(u91,axiom,
select(sF40,i6) = sF43 ).
cnf(u987,axiom,
sF13 = store(sF11,i7,sF8) ).
cnf(u2237,axiom,
sF0 = select(sF54,i7) ).
cnf(u1850,axiom,
sF21 = store(sF19,i7,sF0) ).
cnf(u93,axiom,
store(sF42,i8,sF43) = sF44 ).
cnf(u1007,axiom,
sF28 = store(sF26,i7,sF24) ).
cnf(u2466,axiom,
sF0 = select(sF62,i8) ).
cnf(u1373,axiom,
sF19 = store(sF17,i7,sF0) ).
cnf(u49,axiom,
select(sF19,i4) = sF22 ).
cnf(u87,axiom,
select(sF40,i8) = sF41 ).
cnf(u245,axiom,
sF46 = store(sF44,i5,sF43) ).
cnf(u1789,axiom,
sF0 = select(sF60,i7) ).
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(u1703,axiom,
( select(sF56,X0) = select(sF58,X0)
| i7 = X0 ) ).
cnf(u25,axiom,
select(sF7,i8) = sF10 ).
cnf(u239,axiom,
sF11 = store(sF9,i5,sF6) ).
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(u225,axiom,
( select(sF52,X0) = select(sF54,X0)
| i1 = X0 ) ).
cnf(u985,axiom,
sF20 = sF22 ).
cnf(u39,axiom,
store(sF15,i7,sF16) = sF17 ).
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(u658,axiom,
sF61 = select(sF62,i9) ).
cnf(u191,axiom,
sF64 = select(sF65,i2) ).
cnf(u983,axiom,
sF58 = store(sF56,i7,sF55) ).
cnf(u188,axiom,
sF59 = select(sF60,i5) ).
cnf(u178,axiom,
sF0 = select(sF40,i8) ).
cnf(u981,axiom,
sF8 = select(sF13,i7) ).
cnf(u19,axiom,
store(sF5,i8,sF6) = sF7 ).
cnf(u1684,axiom,
( select(sF36,X0) = select(sF38,X0)
| i7 = X0 ) ).
cnf(u177,axiom,
sF37 = select(sF38,i5) ).
cnf(u1347,axiom,
sF3 = store(sF1,i7,sF0) ).
cnf(u180,axiom,
sF43 = select(sF44,i8) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u653,axiom,
sF68 = select(sF67,i9) ).
cnf(u610,axiom,
sF68 = select(sF69,i0) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u609,axiom,
sF31 = select(sF32,i0) ).
cnf(u2404,axiom,
sF0 = select(sF34,i8) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1211,axiom,
sF61 = select(sF60,i8) ).
cnf(u1687,axiom,
( select(sF58,X0) = select(sF60,X0)
| i7 = X0 ) ).
cnf(u1643,axiom,
sF25 = store(sF23,i8,sF0) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u1257,axiom,
sF53 = select(sF71,i8) ).
cnf(u1244,axiom,
sF61 = select(sF63,i8) ).
cnf(u1235,axiom,
sF24 = select(sF25,i8) ).
cnf(u1573,axiom,
sF26 = store(sF25,i8,sF24) ).
cnf(u1788,axiom,
sF60 = store(sF58,i7,sF0) ).
cnf(u605,axiom,
sF32 = store(sF30,i0,sF31) ).
cnf(u1238,axiom,
sF24 = select(sF26,i8) ).
cnf(u1588,axiom,
( select(sF62,X0) = select(sF63,X0)
| i8 = X0 ) ).
cnf(u1579,axiom,
sF62 = store(sF60,i8,sF61) ).
cnf(u659,axiom,
sF61 = select(sF63,i9) ).
cnf(u129,axiom,
store(sF60,i0,sF61) = sF62 ).
cnf(u1874,axiom,
sF0 = select(sF52,i8) ).
cnf(u1670,axiom,
sF63 = store(sF62,i8,sF0) ).
cnf(u1187,axiom,
sF2 = select(sF32,i8) ).
cnf(u1669,axiom,
sF62 = store(sF60,i8,sF0) ).
cnf(u309,axiom,
sF5 = store(sF3,i6,sF0) ).
cnf(u1047,axiom,
sF29 = select(sF25,i7) ).
cnf(u648,axiom,
sF31 = select(sF30,i9) ).
cnf(u1936,axiom,
sF0 = select(sF58,i7) ).
cnf(u808,axiom,
sF53 = select(sF50,i7) ).
cnf(u655,axiom,
sF24 = select(sF25,i9) ).
cnf(u2458,axiom,
sF0 = select(sF26,i8) ).
cnf(u1004,axiom,
sF24 = select(sF28,i7) ).
cnf(u611,axiom,
sF68 = sF70 ).
cnf(u228,axiom,
( select(sF58,X0) = select(sF60,X0)
| i5 = X0 ) ).
cnf(u647,axiom,
sF26 = store(sF25,i9,sF24) ).
cnf(u1139,axiom,
sF53 = sF64 ).
cnf(u101,axiom,
store(sF46,i8,sF47) = sF48 ).
cnf(u222,axiom,
( select(sF46,X0) = select(sF48,X0)
| i8 = X0 ) ).
cnf(u234,axiom,
( select(sF69,X0) = select(sF71,X0)
| i0 = X0 ) ).
cnf(u221,axiom,
( select(sF44,X0) = select(sF46,X0)
| i5 = X0 ) ).
cnf(u984,axiom,
sF50 = store(sF48,i7,sF47) ).
cnf(u607,axiom,
sF69 = store(sF67,i0,sF68) ).
cnf(u208,axiom,
( select(sF19,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u1835,axiom,
sF0 = sF22 ).
cnf(u915,axiom,
sF69 = store(sF67,i8,sF64) ).
cnf(u215,axiom,
( select(sF32,X0) = select(sF34,X0)
| i0 = X0 ) ).
cnf(u202,axiom,
( select(sF7,X0) = select(sF9,X0)
| i8 = X0 ) ).
cnf(u171,axiom,
sF24 = select(sF26,i0) ).
cnf(u596,axiom,
i0 = i3 ).
cnf(u201,axiom,
( select(sF5,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u174,axiom,
sF31 = select(sF32,i3) ).
cnf(u204,axiom,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u229,axiom,
( select(sF60,X0) = select(sF62,X0)
| i0 = X0 ) ).
cnf(u173,axiom,
sF29 = select(sF30,i2) ).
cnf(u195,axiom,
sF72 = select(sF73,i5) ).
cnf(u160,axiom,
sF4 = select(sF5,i6) ).
cnf(u81,axiom,
store(sF36,i5,sF37) = sF38 ).
cnf(u198,axiom,
( select(a1,X0) = select(sF39,X0)
| i7 = X0 ) ).
cnf(u780,axiom,
sF14 = select(sF15,i8) ).
cnf(u167,axiom,
sF18 = select(sF19,i1) ).
cnf(u197,axiom,
( select(a1,X0) = select(sF1,X0)
| i8 = X0 ) ).
cnf(u2450,axiom,
sF0 = select(sF3,i7) ).
cnf(u123,axiom,
select(sF56,i4) = sF59 ).
cnf(u153,axiom,
select(sF71,i5) = sF74 ).
cnf(u1019,axiom,
sF23 = store(sF21,i7,sF20) ).
cnf(u156,negated_conjecture,
sF38 != sF75 ).
cnf(u1856,axiom,
sF0 = select(sF21,i7) ).
cnf(u125,axiom,
store(sF58,i5,sF59) = sF60 ).
cnf(u147,axiom,
store(sF69,i0,sF70) = sF71 ).
cnf(u1644,axiom,
sF26 = store(sF25,i8,sF0) ).
cnf(u119,axiom,
select(sF56,i5) = sF57 ).
cnf(u970,axiom,
sF51 = select(sF48,i7) ).
cnf(u149,axiom,
select(sF71,i9) = sF72 ).
cnf(u105,axiom,
store(sF48,i4,sF49) = sF50 ).
cnf(u143,axiom,
store(sF67,i3,sF68) = sF69 ).
cnf(u994,axiom,
sF64 = select(sF63,i7) ).
cnf(u2406,axiom,
sF0 = select(sF50,i7) ).
cnf(u1708,axiom,
( select(sF48,X0) = select(sF50,X0)
| i7 = X0 ) ).
cnf(u99,axiom,
select(sF44,i5) = sF47 ).
cnf(u688,axiom,
sF5 = store(sF3,i8,sF0) ).
cnf(u2193,axiom,
sF0 = sF37 ).
cnf(u1017,axiom,
sF8 = sF22 ).
cnf(u194,axiom,
sF70 = select(sF71,i0) ).
cnf(u933,axiom,
sF8 = sF12 ).
cnf(u193,axiom,
sF68 = select(sF69,i3) ).
cnf(u57,axiom,
store(sF25,i0,sF24) = sF26 ).
cnf(u775,axiom,
sF37 = select(sF34,i8) ).
cnf(u95,axiom,
select(sF44,i8) = sF45 ).
cnf(u1526,axiom,
sF65 = store(sF63,i8,sF0) ).
cnf(u689,axiom,
sF0 = sF43 ).
cnf(u51,axiom,
store(sF21,i5,sF22) = sF23 ).
cnf(u1716,axiom,
( select(sF17,X0) = select(sF19,X0)
| i7 = X0 ) ).
cnf(u1370,axiom,
sF0 = sF18 ).
cnf(u841,axiom,
sF74 = select(sF71,i7) ).
cnf(u53,axiom,
select(sF23,i0) = sF24 ).
cnf(u686,axiom,
sF42 = store(sF40,i8,sF0) ).
cnf(u1567,axiom,
sF25 = store(sF23,i8,sF24) ).
cnf(u2480,axiom,
sF0 = select(sF67,i7) ).
cnf(u980,axiom,
sF47 = select(sF50,i7) ).
cnf(u47,axiom,
store(sF19,i4,sF20) = sF21 ).
cnf(u1124,axiom,
sF61 = select(sF56,i8) ).
cnf(u2111,axiom,
sF0 = select(sF73,i7) ).
cnf(u1712,axiom,
( select(sF11,X0) = select(sF13,X0)
| i7 = X0 ) ).
cnf(u1847,axiom,
sF0 = sF20 ).
cnf(u837,axiom,
sF47 = select(sF44,i7) ).
cnf(u1540,axiom,
sF32 = store(sF30,i8,sF0) ).
cnf(u666,axiom,
sF34 = store(sF32,i9,sF31) ).
cnf(u665,axiom,
sF71 = store(sF69,i9,sF68) ).
cnf(u1267,axiom,
sF2 = select(sF34,i8) ).
cnf(u1441,axiom,
sF0 = sF47 ).
cnf(u1346,axiom,
sF39 = store(a1,i7,sF0) ).
cnf(u75,axiom,
select(sF34,i5) = sF35 ).
cnf(u1076,axiom,
sF21 = store(sF19,i7,sF8) ).
cnf(u1269,axiom,
sF38 = store(sF36,i7,sF2) ).
cnf(u307,axiom,
sF0 = sF4 ).
cnf(u1360,axiom,
sF47 = sF53 ).
cnf(u618,axiom,
sF35 = select(sF32,i5) ).
cnf(u1619,axiom,
sF34 = store(sF32,i8,sF0) ).
cnf(u1091,axiom,
sF30 = store(sF28,i8,sF8) ).
cnf(u832,axiom,
sF20 = select(sF19,i7) ).
cnf(u1194,axiom,
sF24 = select(sF23,i8) ).
cnf(u1265,axiom,
sF2 = sF37 ).
cnf(u1722,axiom,
( select(sF65,X0) = select(sF67,X0)
| i7 = X0 ) ).
cnf(u2486,axiom,
sF0 = select(sF28,i7) ).
cnf(u1066,axiom,
sF35 = select(sF32,i7) ).
cnf(u1065,axiom,
sF23 = store(sF21,i7,sF8) ).
cnf(u908,axiom,
sF64 = sF68 ).
cnf(u839,axiom,
sF60 = store(sF58,i7,sF59) ).
cnf(u1661,axiom,
( select(sF34,X0) = select(sF36,X0)
| i8 = X0 ) ).
cnf(u893,axiom,
sF50 = store(sF48,i4,sF47) ).
cnf(u2312,axiom,
sF0 = select(sF48,i8) ).
cnf(u1046,axiom,
sF56 = store(sF54,i7,sF53) ).
cnf(u960,axiom,
sF14 = select(sF7,i4) ).
cnf(u989,axiom,
sF19 = store(sF17,i7,sF18) ).
cnf(u991,axiom,
sF29 = select(sF26,i7) ).
cnf(u1677,axiom,
( select(sF73,X0) = select(sF75,X0)
| i8 = X0 ) ).
cnf(u2279,axiom,
sF0 = select(sF36,i8) ).
cnf(u247,axiom,
sF6 = select(sF11,i5) ).
cnf(u656,axiom,
sF24 = select(sF26,i9) ).
cnf(u663,axiom,
sF68 = select(sF71,i9) ).
cnf(u233,axiom,
( select(sF67,X0) = select(sF69,X0)
| i3 = X0 ) ).
cnf(u2330,axiom,
sF0 = select(sF32,i8) ).
cnf(u1674,axiom,
( select(sF50,X0) = select(sF52,X0)
| i8 = X0 ) ).
cnf(u236,axiom,
( select(sF73,X0) = select(sF75,X0)
| i9 = X0 ) ).
cnf(u77,axiom,
store(sF34,i9,sF35) = sF36 ).
cnf(u227,axiom,
( select(sF56,X0) = select(sF58,X0)
| i4 = X0 ) ).
cnf(u652,axiom,
sF63 = store(sF62,i9,sF61) ).
cnf(u33,axiom,
select(sF11,i4) = sF14 ).
cnf(u230,axiom,
( select(sF62,X0) = select(sF63,X0)
| i0 = X0 ) ).
cnf(u71,axiom,
select(sF30,i3) = sF33 ).
cnf(u967,axiom,
sF21 = store(sF19,i7,sF20) ).
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(u185,axiom,
sF53 = select(sF54,i1) ).
cnf(u1154,axiom,
sF65 = store(sF63,i8,sF53) ).
cnf(u223,axiom,
( select(sF48,X0) = select(sF50,X0)
| i4 = X0 ) ).
cnf(u1802,axiom,
sF0 = sF55 ).
cnf(u850,axiom,
sF8 = select(sF5,i7) ).
cnf(u29,axiom,
select(sF11,i9) = sF12 ).
cnf(u210,axiom,
( select(sF23,X0) = select(sF25,X0)
| i0 = X0 ) ).
cnf(u179,axiom,
sF41 = select(sF42,i6) ).
cnf(u157,axiom,
sF0 = select(sF1,i8) ).
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(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(u175,axiom,
sF33 = select(sF34,i0) ).
cnf(u1770,axiom,
sF0 = sF45 ).
cnf(u1810,axiom,
sF0 = sF53 ).
cnf(u162,axiom,
sF8 = select(sF9,i8) ).
cnf(u1002,axiom,
sF8 = sF16 ).
cnf(u998,axiom,
sF53 = select(sF54,i7) ).
cnf(u161,axiom,
sF6 = select(sF7,i8) ).
cnf(u164,axiom,
sF12 = select(sF13,i4) ).
cnf(u1342,axiom,
sF0 = sF2 ).
cnf(u5,axiom,
select(a1,i7) = sF0 ).
cnf(u137,axiom,
select(sF63,i2) = sF66 ).
cnf(u1596,axiom,
( select(sF69,X0) = select(sF71,X0)
| i8 = X0 ) ).
cnf(u127,axiom,
select(sF60,i0) = sF61 ).
cnf(u1255,axiom,
sF53 = sF72 ).
cnf(u1799,axiom,
sF0 = select(sF23,i7) ).
cnf(u113,axiom,
store(sF52,i1,sF53) = sF54 ).
cnf(u1241,axiom,
sF61 = select(sF62,i8) ).
cnf(u1537,axiom,
( select(sF30,X0) = select(sF32,X0)
| i8 = X0 ) ).
cnf(u1432,axiom,
sF36 = store(sF34,i8,sF24) ).
cnf(u778,axiom,
sF72 = select(sF71,i8) ).
cnf(u1521,axiom,
( select(sF63,X0) = select(sF65,X0)
| i8 = X0 ) ).
cnf(u783,axiom,
sF74 = select(sF75,i8) ).
cnf(u1041,axiom,
sF17 = store(sF15,i7,sF8) ).
cnf(u1012,axiom,
sF60 = store(sF58,i7,sF53) ).
cnf(u109,axiom,
store(sF50,i9,sF51) = sF52 ).
cnf(u1616,axiom,
( select(sF32,X0) = select(sF34,X0)
| i8 = X0 ) ).
cnf(u869,axiom,
sF61 = select(sF58,i8) ).
cnf(u774,axiom,
sF36 = store(sF34,i8,sF35) ).
cnf(u1193,axiom,
sF53 = select(sF69,i8) ).
cnf(u1792,axiom,
sF0 = sF59 ).
cnf(u1149,axiom,
sF61 = sF74 ).
cnf(u992,axiom,
sF54 = store(sF52,i7,sF53) ).
cnf(u1386,axiom,
sF17 = store(sF15,i7,sF0) ).
cnf(u1024,axiom,
sF8 = sF20 ).
cnf(u1173,axiom,
sF2 = select(sF30,i8) ).
cnf(u604,axiom,
sF24 = sF27 ).
cnf(u988,axiom,
sF16 = select(sF15,i7) ).
cnf(u602,axiom,
sF64 = select(sF65,i0) ).
cnf(u2344,axiom,
sF0 = select(sF69,i8) ).
cnf(u1170,axiom,
sF2 = sF31 ).
cnf(u1330,axiom,
sF0 = sF8 ).
cnf(u1126,axiom,
sF64 = select(sF62,i7) ).
cnf(u206,axiom,
( select(sF15,X0) = select(sF17,X0)
| i7 = X0 ) ).
cnf(u1156,axiom,
sF75 = store(sF73,i8,sF61) ).
cnf(u205,axiom,
( select(sF13,X0) = select(sF15,X0)
| i9 = X0 ) ).
cnf(u192,axiom,
sF66 = select(sF67,i1) ).
cnf(u1819,axiom,
sF0 = select(sF17,i7) ).
cnf(u1719,axiom,
( select(sF52,X0) = select(sF54,X0)
| i7 = X0 ) ).
cnf(u199,axiom,
( select(sF1,X0) = select(sF3,X0)
| i7 = X0 ) ).
cnf(u2454,axiom,
sF0 = select(sF25,i8) ).
cnf(u155,axiom,
store(sF73,i9,sF74) = sF75 ).
cnf(u2472,axiom,
sF0 = select(sF63,i8) ).
cnf(u158,axiom,
sF2 = select(sF39,i7) ).
cnf(u2178,axiom,
sF0 = select(sF38,i7) ).
cnf(u1077,axiom,
sF47 = select(sF42,i7) ).
cnf(u843,axiom,
sF22 = select(sF23,i7) ).
cnf(u1570,axiom,
( select(sF23,X0) = select(sF25,X0)
| i8 = X0 ) ).
cnf(u1707,axiom,
sF50 = store(sF48,i7,sF0) ).
cnf(u851,axiom,
sF11 = store(sF9,i7,sF0) ).
cnf(u892,axiom,
sF44 = store(sF42,i8,sF0) ).
cnf(u151,axiom,
store(sF71,i5,sF72) = sF73 ).
cnf(u1379,axiom,
sF0 = sF16 ).
cnf(u1553,axiom,
( select(sF67,X0) = select(sF69,X0)
| i8 = X0 ) ).
cnf(u107,axiom,
select(sF48,i4) = sF51 ).
cnf(u974,axiom,
sF20 = select(sF21,i7) ).
cnf(u1003,axiom,
sF61 = select(sF67,i7) ).
cnf(u1706,axiom,
sF58 = store(sF56,i7,sF0) ).
cnf(u847,axiom,
sF72 = select(sF73,i7) ).
cnf(u131,axiom,
store(sF62,i0,sF61) = sF63 ).
cnf(u846,axiom,
sF59 = select(sF60,i7) ).
cnf(u103,axiom,
select(sF48,i9) = sF49 ).
cnf(u263,axiom,
( select(sF1,X0) = select(sF39,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u133,axiom,
select(sF63,i1) = sF64 ).
cnf(u59,axiom,
select(sF26,i2) = sF27 ).
cnf(u1806,axiom,
sF0 = select(sF15,i8) ).
cnf(u89,axiom,
store(sF40,i6,sF41) = sF42 ).
cnf(u1658,axiom,
sF0 = sF61 ).
cnf(u882,axiom,
sF7 = store(sF5,i8,sF0) ).
cnf(u61,axiom,
store(sF26,i1,sF27) = sF28 ).
cnf(u242,axiom,
sF42 = store(sF40,i6,sF0) ).
cnf(u83,axiom,
store(a1,i7,sF2) = sF39 ).
cnf(u1748,axiom,
sF0 = sF10 ).
cnf(u241,axiom,
sF0 = sF41 ).
cnf(u1739,axiom,
( select(sF9,X0) = select(sF11,X0)
| i7 = X0 ) ).
cnf(u55,axiom,
store(sF23,i0,sF24) = sF25 ).
cnf(u244,axiom,
sF43 = sF45 ).
cnf(u85,axiom,
store(sF39,i8,sF0) = sF40 ).
cnf(u172,axiom,
sF27 = select(sF28,i1) ).
cnf(u41,axiom,
select(sF15,i7) = sF18 ).
cnf(u79,axiom,
select(sF34,i9) = sF37 ).
cnf(u1510,axiom,
sF30 = store(sF28,i8,sF0) ).
cnf(u1744,axiom,
sF0 = select(sF44,i8) ).
cnf(u35,axiom,
store(sF13,i9,sF14) = sF15 ).
cnf(u1700,axiom,
( select(sF19,X0) = select(sF21,X0)
| i7 = X0 ) ).
cnf(u65,axiom,
store(sF28,i2,sF29) = sF30 ).
cnf(u1691,axiom,
( select(sF71,X0) = select(sF73,X0)
| i7 = X0 ) ).
cnf(u858,axiom,
sF0 = select(sF11,i7) ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u830,axiom,
sF8 = select(sF7,i7) ).
cnf(u1884,axiom,
sF75 = store(sF73,i8,sF0) ).
cnf(u840,axiom,
sF73 = store(sF71,i7,sF72) ).
cnf(u31,axiom,
store(sF11,i4,sF12) = sF13 ).
cnf(u2414,axiom,
sF0 = select(sF13,i7) ).
cnf(u854,axiom,
sF55 = sF57 ).
cnf(u17,axiom,
select(sF3,i6) = sF6 ).
cnf(u650,axiom,
sF61 = select(sF60,i9) ).
cnf(u777,axiom,
sF52 = store(sF50,i8,sF51) ).
cnf(u1073,axiom,
sF35 = select(sF30,i7) ).
cnf(u1060,axiom,
sF8 = sF29 ).
cnf(u1648,axiom,
( select(sF13,X0) = select(sF15,X0)
| i8 = X0 ) ).
cnf(u773,axiom,
sF15 = store(sF13,i8,sF14) ).
cnf(u121,axiom,
store(sF56,i4,sF57) = sF58 ).
cnf(u1097,axiom,
sF0 = sF51 ).
cnf(u601,axiom,
sF29 = select(sF30,i0) ).
cnf(u664,axiom,
sF31 = select(sF34,i9) ).
cnf(u1227,axiom,
sF53 = sF68 ).
cnf(u1899,axiom,
sF0 = select(sF65,i8) ).
cnf(u979,axiom,
sF55 = select(sF58,i7) ).
cnf(u1343,axiom,
sF9 = store(sF7,i8,sF0) ).
cnf(u1161,axiom,
sF9 = store(sF7,i8,sF2) ).
cnf(u1177,axiom,
sF32 = store(sF30,i8,sF2) ).
cnf(u1681,axiom,
( select(sF21,X0) = select(sF23,X0)
| i7 = X0 ) ).
cnf(u235,axiom,
( select(sF71,X0) = select(sF73,X0)
| i5 = X0 ) ).
cnf(u238,axiom,
sF6 = sF10 ).
cnf(u651,axiom,
sF62 = store(sF60,i9,sF61) ).
cnf(u1811,axiom,
sF56 = store(sF54,i7,sF0) ).
cnf(u1724,axiom,
sF28 = store(sF26,i7,sF0) ).
cnf(u1445,axiom,
sF61 = select(sF54,i8) ).
cnf(u977,axiom,
sF14 = select(sF9,i7) ).
cnf(u1822,axiom,
sF54 = store(sF52,i7,sF0) ).
cnf(u224,axiom,
( select(sF50,X0) = select(sF52,X0)
| i9 = X0 ) ).
cnf(u1032,axiom,
sF24 = select(sF21,i8) ).
cnf(u844,axiom,
sF37 = select(sF38,i7) ).
cnf(u231,axiom,
( select(sF63,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u1039,axiom,
sF24 = select(sF19,i8) ).
cnf(u1429,axiom,
sF24 = sF35 ).
cnf(u1633,axiom,
sF0 = sF24 ).
cnf(u218,axiom,
( select(sF39,X0) = select(sF40,X0)
| i8 = X0 ) ).
cnf(u1026,axiom,
sF15 = store(sF13,i8,sF0) ).
cnf(u187,axiom,
sF57 = select(sF58,i4) ).
cnf(u612,axiom,
sF31 = sF33 ).
cnf(u217,axiom,
( select(sF36,X0) = select(sF38,X0)
| i5 = X0 ) ).
cnf(u190,axiom,
sF61 = select(sF63,i0) ).
cnf(u603,axiom,
sF61 = sF66 ).
cnf(u220,axiom,
( select(sF42,X0) = select(sF44,X0)
| i8 = X0 ) ).
cnf(u189,axiom,
sF61 = select(sF62,i0) ).
cnf(u964,axiom,
i7 = i1 ).
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(u214,axiom,
( select(sF30,X0) = select(sF32,X0)
| i3 = X0 ) ).
cnf(u2105,axiom,
sF73 = store(sF71,i7,sF0) ).
cnf(u183,axiom,
sF49 = select(sF50,i4) ).
cnf(u213,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u1585,axiom,
sF63 = store(sF62,i8,sF61) ).
cnf(u170,axiom,
sF24 = select(sF25,i0) ).
cnf(u599,axiom,
sF65 = store(sF63,i0,sF64) ).
cnf(u200,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u169,axiom,
sF22 = select(sF23,i5) ).
cnf(u1725,axiom,
( select(sF26,X0) = select(sF28,X0)
| i7 = X0 ) ).
cnf(u207,axiom,
( select(sF17,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u834,axiom,
sF35 = select(sF34,i7) ).
cnf(u13,axiom,
select(sF3,i8) = sF4 ).
cnf(u646,axiom,
sF25 = store(sF23,i9,sF24) ).
cnf(u163,axiom,
sF10 = select(sF11,i5) ).
cnf(u645,axiom,
sF24 = select(sF23,i9) ).
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(u1625,axiom,
( select(sF40,X0) = select(sF42,X0)
| i8 = X0 ) ).
cnf(u1832,axiom,
sF0 = select(sF56,i7) ).
cnf(u859,axiom,
sF46 = store(sF44,i7,sF0) ).
cnf(u1006,axiom,
sF53 = sF55 ).
cnf(u159,axiom,
sF2 = select(sF3,i7) ).
cnf(u1721,axiom,
sF67 = store(sF65,i7,sF0) ).
cnf(u786,axiom,
sF47 = sF49 ).
cnf(u753,axiom,
sF47 = select(sF42,i5) ).
cnf(u1635,axiom,
( select(sF3,X0) = select(sF5,X0)
| i8 = X0 ) ).
cnf(u598,axiom,
sF30 = store(sF28,i0,sF29) ).
cnf(u115,axiom,
select(sF52,i1) = sF55 ).
cnf(u982,axiom,
sF55 = sF59 ).
cnf(u145,axiom,
select(sF67,i3) = sF70 ).
cnf(u938,axiom,
sF13 = store(sF11,i4,sF8) ).
cnf(u117,axiom,
store(sF54,i7,sF55) = sF56 ).
cnf(u2032,axiom,
sF0 = select(sF9,i8) ).
cnf(u782,axiom,
sF51 = select(sF52,i8) ).
cnf(u986,axiom,
sF0 = sF14 ).
cnf(u811,axiom,
sF28 = store(sF26,i1,sF24) ).
cnf(u111,axiom,
select(sF52,i7) = sF53 ).
cnf(u2175,axiom,
sF38 = store(sF36,i7,sF0) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV531-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n004.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:34:23 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.22/0.27 Running first-order model finding
% 0.22/0.27 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.72/1.96 % (300641)Will run a generic schedule for satisfiability detection.
% 2.72/1.96 % (300648)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4077869325:i=88024:add=on:rawr=on_2989 on theBenchmark for (2989ds/88024Mi)
% 2.72/1.96 % (300647)% WARNING: option uhcvi not known.
% 2.72/1.96 % (300649)dis+10_1_sil=32000:sp=arity:random_seed=3948794075:i=103:fgj=on_2989 on theBenchmark for (2989ds/103Mi)
% 2.72/1.96 % (300646)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=559294147_2989 on theBenchmark for (2989ds/0Mi)
% 2.72/1.96 % (300650)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1327143354:i=116_2989 on theBenchmark for (2989ds/116Mi)
% 2.72/1.96 % (300647)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1704201286:i=135531:add=off:rawr=on_2989 on theBenchmark for (2989ds/135531Mi)
% 2.72/1.96 % (300652)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1712679778:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2989 on theBenchmark for (2989ds/159Mi)
% 2.72/1.96 % (300651)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1216204651:i=131_2989 on theBenchmark for (2989ds/131Mi)
% 2.72/1.96 % TRYING [1]
% 2.72/1.96 % TRYING [2]
% 2.72/1.96 % TRYING [3]
% 2.72/1.96 % TRYING [4]
% 2.72/1.96 % TRYING [5]
% 2.72/1.96 % (300650)Instruction limit reached!
% 2.72/1.96 % (300650)------------------------------
% 2.72/1.96 % (300650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300650)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300650)Termination reason: Instruction limit
% 2.72/1.96 % (300650)Termination phase: Saturation
% 2.72/1.96 % (300650)Time elapsed: 0.087 s
% 2.72/1.96 % (300650)Peak memory usage: 28 MB
% 2.72/1.96 % (300650)Instructions burned: 117 (million)
% 2.72/1.96 % (300651)Instruction limit reached!
% 2.72/1.96 % (300651)------------------------------
% 2.72/1.96 % (300651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300651)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300651)Termination reason: Instruction limit
% 2.72/1.96 % (300651)Termination phase: Saturation
% 2.72/1.96 % (300651)Time elapsed: 0.092 s
% 2.72/1.96 % (300651)Peak memory usage: 28 MB
% 2.72/1.96 % (300651)Instructions burned: 134 (million)
% 2.72/1.96 % TRYING [6]
% 2.72/1.96 % (300652)Instruction limit reached!
% 2.72/1.96 % (300652)------------------------------
% 2.72/1.96 % (300652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300652)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300652)Termination reason: Instruction limit
% 2.72/1.96 % (300652)Termination phase: Saturation
% 2.72/1.96 % (300652)Time elapsed: 0.103 s
% 2.72/1.96 % (300652)Peak memory usage: 28 MB
% 2.72/1.96 % (300652)Instructions burned: 160 (million)
% 2.72/1.96 % (300660)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1834633190:i=714:nm=2_2987 on theBenchmark for (2987ds/714Mi)
% 2.72/1.96 % (300661)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2360966964:i=131:bd=preordered:fsd=on_2987 on theBenchmark for (2987ds/131Mi)
% 2.72/1.96 % (300662)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=2825146568:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2987 on theBenchmark for (2987ds/684Mi)
% 2.72/1.96 % (300661)Instruction limit reached!
% 2.72/1.96 % (300661)------------------------------
% 2.72/1.96 % (300661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300661)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300661)Termination reason: Instruction limit
% 2.72/1.96 % (300661)Termination phase: Saturation
% 2.72/1.96 % (300661)Time elapsed: 0.064 s
% 2.72/1.96 % (300661)Peak memory usage: 23 MB
% 2.72/1.96 % (300661)Instructions burned: 132 (million)
% 2.72/1.96 % (300666)ott-21_1_sil=16000:fs=off:random_seed=2663905282:i=180:av=off:fsr=off_2987 on theBenchmark for (2987ds/180Mi)
% 2.72/1.96 % TRYING [7]
% 2.72/1.96 % TRYING [1]
% 2.72/1.96 % TRYING [2]
% 2.72/1.96 % TRYING [3]
% 2.72/1.96 % TRYING [4]
% 2.72/1.96 % (300649)Instruction limit reached!
% 2.72/1.96 % (300649)------------------------------
% 2.72/1.96 % (300649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300649)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300649)Termination reason: Instruction limit
% 2.72/1.96 % (300649)Termination phase: Saturation
% 2.72/1.96 % (300649)Time elapsed: 0.253 s
% 2.72/1.96 % (300649)Peak memory usage: 57 MB
% 2.72/1.96 % (300649)Instructions burned: 104 (million)
% 2.72/1.96 % TRYING [5]
% 2.72/1.96 % (300668)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3697963003:i=477:bd=all_2986 on theBenchmark for (2986ds/477Mi)
% 2.72/1.96 % (300666)Instruction limit reached!
% 2.72/1.96 % (300666)------------------------------
% 2.72/1.96 % (300666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300666)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300666)Termination reason: Instruction limit
% 2.72/1.96 % (300666)Termination phase: Saturation
% 2.72/1.96 % (300666)Time elapsed: 0.074 s
% 2.72/1.96 % (300666)Peak memory usage: 19 MB
% 2.72/1.96 % (300666)Instructions burned: 181 (million)
% 2.72/1.96 % (300670)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3215827283:fmbsr=1.3:i=865:ins=25_2986 on theBenchmark for (2986ds/865Mi)
% 2.72/1.96 % (300662)Instruction limit reached!
% 2.72/1.96 % (300662)------------------------------
% 2.72/1.96 % (300662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300662)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300662)Termination reason: Instruction limit
% 2.72/1.96 % (300662)Termination phase: Property scanning
% 2.72/1.96 % (300662)Time elapsed: 0.232 s
% 2.72/1.96 % (300662)Peak memory usage: 9 MB
% 2.72/1.96 % (300662)Instructions burned: 685 (million)
% 2.72/1.96 % TRYING [6]
% 2.72/1.96 % (300672)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3364209803:i=1179_2985 on theBenchmark for (2985ds/1179Mi)
% 2.72/1.96 % (300660)Instruction limit reached!
% 2.72/1.96 % (300660)------------------------------
% 2.72/1.96 % (300660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300660)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300660)Termination reason: Instruction limit
% 2.72/1.96 % (300660)Termination phase: Finite model building constraint generation
% 2.72/1.96 % (300660)Time elapsed: 0.282 s
% 2.72/1.96 % (300660)Peak memory usage: 19 MB
% 2.72/1.96 % (300660)Instructions burned: 715 (million)
% 2.72/1.96 % (300674)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3964238098:i=889:ins=1_2984 on theBenchmark for (2984ds/889Mi)
% 2.72/1.96 % (300672) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-300641-300672"...
% 2.72/1.96 % (300672)...printing done.
% 2.72/1.96 % SZS status Satisfiable for theBenchmark
% 2.72/1.96 % SZS output start Saturation.
% See solution above
% 2.72/1.96 % SZS output start Definitions and Model Updates.
% 2.72/1.96 % SZS output end Definitions and Model Updates.
% 2.72/1.96 % (300672)------------------------------
% 2.72/1.96 % (300672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.72/1.96 % (300672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.72/1.96 % (300672)CaDiCaL version: 2.1.3
% 2.72/1.96 % (300672)Termination reason: Satisfiable
% 2.72/1.96 % (300672)Time elapsed: 0.170 s
% 2.72/1.96 % (300672)Peak memory usage: 16 MB
% 2.72/1.96 % (300672)Instructions burned: 394 (million)
% 2.72/1.96 % (300641)Success in time 1.674 s
% 2.72/1.96 % Vampire exiting
%------------------------------------------------------------------------------