%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV549-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:17:57 PM UTC 2026
% Result : Satisfiable 3.75s 0.91s
% Output : Saturation 3.75s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u65,negated_conjecture,
a1 != a2 ).
cnf(u70,negated_conjecture,
sF25 = sF27 ).
cnf(u75,axiom,
select(a2,i1) = sF0 ).
cnf(u80,axiom,
store(a1,i1,sF0) = sF1 ).
cnf(u85,axiom,
select(a1,i1) = sF2 ).
cnf(u90,axiom,
store(a2,i1,sF2) = sF3 ).
cnf(u95,axiom,
select(sF3,i2) = sF4 ).
cnf(u100,axiom,
store(sF1,i2,sF4) = sF5 ).
cnf(u105,axiom,
select(sF1,i2) = sF6 ).
cnf(u110,axiom,
store(sF3,i2,sF6) = sF7 ).
cnf(u115,axiom,
select(sF7,i3) = sF8 ).
cnf(u120,axiom,
store(sF5,i3,sF8) = sF9 ).
cnf(u125,axiom,
select(sF5,i3) = sF10 ).
cnf(u130,axiom,
store(sF7,i3,sF10) = sF11 ).
cnf(u135,axiom,
select(sF11,i4) = sF12 ).
cnf(u140,axiom,
store(sF9,i4,sF12) = sF13 ).
cnf(u145,axiom,
select(sF9,i4) = sF14 ).
cnf(u150,axiom,
store(sF11,i4,sF14) = sF15 ).
cnf(u155,axiom,
select(sF15,i5) = sF16 ).
cnf(u160,axiom,
store(sF13,i5,sF16) = sF17 ).
cnf(u165,axiom,
select(sF13,i5) = sF18 ).
cnf(u170,axiom,
store(sF15,i5,sF18) = sF19 ).
cnf(u175,axiom,
select(sF19,i6) = sF20 ).
cnf(u180,axiom,
store(sF17,i6,sF20) = sF21 ).
cnf(u185,axiom,
select(sF17,i6) = sF22 ).
cnf(u190,axiom,
store(sF19,i6,sF22) = sF23 ).
cnf(u195,axiom,
select(sF23,i7) = sF24 ).
cnf(u200,axiom,
store(sF21,i7,sF24) = sF25 ).
cnf(u205,axiom,
select(sF21,i7) = sF26 ).
cnf(u210,axiom,
store(sF23,i7,sF26) = sF27 ).
cnf(u216,negated_conjecture,
sF25 = store(sF23,i7,sF26) ).
cnf(u235,negated_conjecture,
sF26 = select(sF25,i7) ).
cnf(u240,axiom,
sF24 = select(sF25,i7) ).
cnf(u245,axiom,
sF22 = select(sF23,i6) ).
cnf(u250,axiom,
sF20 = select(sF21,i6) ).
cnf(u255,axiom,
sF18 = select(sF19,i5) ).
cnf(u260,axiom,
sF16 = select(sF17,i5) ).
cnf(u265,axiom,
sF14 = select(sF15,i4) ).
cnf(u270,axiom,
sF12 = select(sF13,i4) ).
cnf(u275,axiom,
sF10 = select(sF11,i3) ).
cnf(u280,axiom,
sF8 = select(sF9,i3) ).
cnf(u285,axiom,
sF6 = select(sF7,i2) ).
cnf(u290,axiom,
sF4 = select(sF5,i2) ).
cnf(u295,axiom,
sF2 = select(sF3,i1) ).
cnf(u300,axiom,
sF0 = select(sF1,i1) ).
cnf(u321,negated_conjecture,
sF24 = sF26 ).
cnf(u327,negated_conjecture,
sF25 = store(sF23,i7,sF24) ).
cnf(u335,axiom,
i1 != i2 ).
cnf(u340,axiom,
sF6 = select(a1,i2) ).
cnf(u348,axiom,
sF4 = select(a2,i2) ).
cnf(u362,axiom,
sF4 = select(sF5,i1) ).
cnf(u371,axiom,
sF7 != store(sF3,i1,sF6) ).
cnf(u377,axiom,
sF5 != store(sF1,i1,sF4) ).
cnf(u384,axiom,
sF2 = sF6 ).
cnf(u389,axiom,
sF0 = sF6 ).
cnf(u394,axiom,
sF2 = sF4 ).
cnf(u401,axiom,
sF0 = sF2 ).
cnf(u411,axiom,
sF10 = select(sF1,i3) ).
cnf(u415,axiom,
i1 = i3 ).
cnf(u425,axiom,
sF8 = select(sF3,i3) ).
cnf(u439,axiom,
sF8 = select(sF9,i1) ).
cnf(u444,axiom,
sF10 = select(sF11,i1) ).
cnf(u449,axiom,
sF11 = store(sF7,i1,sF10) ).
cnf(u455,axiom,
sF9 = store(sF5,i1,sF8) ).
cnf(u463,axiom,
sF2 = sF10 ).
cnf(u468,axiom,
sF0 = sF8 ).
cnf(u483,axiom,
sF0 = select(a1,i2) ).
cnf(u488,axiom,
sF2 = select(a2,i2) ).
cnf(u498,axiom,
sF14 = select(sF5,i4) ).
cnf(u501,axiom,
i2 != i4 ).
cnf(u507,axiom,
i3 != i4 ).
cnf(u516,axiom,
sF12 = select(sF7,i4) ).
cnf(u526,axiom,
sF18 = select(sF9,i5) ).
cnf(u529,axiom,
i3 != i5 ).
cnf(u535,axiom,
i4 != i5 ).
cnf(u544,axiom,
sF16 = select(sF11,i5) ).
cnf(u554,axiom,
sF22 = select(sF13,i6) ).
cnf(u558,axiom,
i4 = i6 ).
cnf(u563,axiom,
i5 != i6 ).
cnf(u572,axiom,
sF20 = select(sF15,i6) ).
cnf(u583,axiom,
sF20 != select(sF21,i5) ).
cnf(u593,axiom,
sF23 != store(sF19,i5,sF22) ).
cnf(u599,axiom,
sF21 != store(sF17,i5,sF20) ).
cnf(u605,axiom,
sF16 != sF22 ).
cnf(u610,axiom,
sF18 != sF20 ).
cnf(u620,negated_conjecture,
i6 = i7 ).
cnf(u624,negated_conjecture,
sF24 = select(sF17,i7) ).
cnf(u637,negated_conjecture,
sF25 = store(sF23,i6,sF24) ).
cnf(u642,negated_conjecture,
sF24 = select(sF25,i6) ).
cnf(u650,negated_conjecture,
sF25 = store(sF21,i6,sF24) ).
cnf(u658,negated_conjecture,
sF20 = sF26 ).
cnf(u663,negated_conjecture,
sF22 = sF24 ).
cnf(u672,negated_conjecture,
sF24 = select(sF19,i7) ).
cnf(u702,negated_conjecture,
sF20 = sF24 ).
cnf(u707,negated_conjecture,
sF25 = store(sF23,i6,sF20) ).
cnf(u718,negated_conjecture,
sF22 = select(sF19,i7) ).
cnf(u726,negated_conjecture,
sF20 = sF22 ).
cnf(u734,negated_conjecture,
i5 != i7 ).
cnf(u739,negated_conjecture,
sF24 = select(sF13,i7) ).
cnf(u776,negated_conjecture,
sF18 != sF26 ).
cnf(u781,negated_conjecture,
sF16 != sF24 ).
cnf(u790,negated_conjecture,
sF18 != sF24 ).
cnf(u801,negated_conjecture,
sF25 != store(sF23,i5,sF18) ).
cnf(u808,negated_conjecture,
sF16 = select(sF19,i5) ).
cnf(u815,negated_conjecture,
sF25 = store(sF23,i7,sF20) ).
cnf(u842,negated_conjecture,
sF20 = select(sF17,i6) ).
cnf(u877,negated_conjecture,
sF23 = store(sF19,i6,sF20) ).
cnf(u895,negated_conjecture,
sF25 = store(sF21,i6,sF20) ).
cnf(u915,negated_conjecture,
sF20 = select(sF9,i6) ).
cnf(u930,axiom,
sF20 = select(sF21,i4) ).
cnf(u938,axiom,
sF21 = store(sF17,i4,sF20) ).
cnf(u943,axiom,
sF20 = select(sF19,i4) ).
cnf(u948,negated_conjecture,
sF20 = select(sF25,i4) ).
cnf(u953,negated_conjecture,
sF20 = select(sF23,i4) ).
cnf(u958,negated_conjecture,
sF23 = store(sF19,i4,sF20) ).
cnf(u963,negated_conjecture,
sF20 = select(sF17,i4) ).
cnf(u974,negated_conjecture,
sF20 = select(sF13,i6) ).
cnf(u992,negated_conjecture,
sF16 = sF18 ).
cnf(u1017,negated_conjecture,
sF25 != store(sF23,i6,sF18) ).
cnf(u1025,negated_conjecture,
sF18 != select(sF13,i6) ).
cnf(u1058,negated_conjecture,
sF25 != store(sF21,i6,sF18) ).
cnf(u1068,axiom,
sF10 = select(a1,i3) ).
cnf(u1077,axiom,
sF8 = select(a2,i3) ).
cnf(u1085,negated_conjecture,
i3 != i6 ).
cnf(u1089,negated_conjecture,
sF18 != select(sF5,i6) ).
cnf(u1098,axiom,
sF14 = select(sF1,i4) ).
cnf(u1172,axiom,
sF12 = select(sF3,i4) ).
cnf(u1232,negated_conjecture,
sF18 != select(sF9,i6) ).
cnf(u1239,negated_conjecture,
i2 != i6 ).
cnf(u1243,negated_conjecture,
sF18 != select(sF1,i6) ).
cnf(u1252,axiom,
sF18 = select(sF5,i5) ).
cnf(u1281,negated_conjecture,
i2 != i5 ).
cnf(u1344,axiom,
sF16 = select(sF7,i5) ).
cnf(u1354,negated_conjecture,
sF18 != sF22 ).
cnf(u1365,negated_conjecture,
sF23 != store(sF19,i6,sF18) ).
cnf(u1391,negated_conjecture,
i1 != i6 ).
cnf(u1395,negated_conjecture,
sF18 != select(a1,i6) ).
cnf(u1452,negated_conjecture,
i1 != i4 ).
cnf(u1524,axiom,
sF21 != store(sF17,i6,sF18) ).
cnf(u1540,axiom,
sF0 = sF4 ).
cnf(u1548,negated_conjecture,
sF18 != select(sF25,i6) ).
cnf(u1569,axiom,
sF7 = store(sF3,i2,sF2) ).
cnf(u1576,negated_conjecture,
sF18 = select(sF25,i5) ).
cnf(u1592,axiom,
sF16 != sF20 ).
cnf(u1603,axiom,
sF18 = select(sF21,i5) ).
cnf(u1634,negated_conjecture,
sF18 = select(sF23,i5) ).
cnf(u1677,negated_conjecture,
sF20 = select(sF25,i6) ).
cnf(u1713,negated_conjecture,
sF14 != sF18 ).
cnf(u1719,negated_conjecture,
sF14 = sF20 ).
cnf(u1742,negated_conjecture,
sF18 != select(a1,i4) ).
cnf(u1759,negated_conjecture,
sF25 = store(sF23,i4,sF14) ).
cnf(u1766,axiom,
sF12 = sF22 ).
cnf(u1771,negated_conjecture,
sF25 = store(sF21,i4,sF14) ).
cnf(u1787,negated_conjecture,
sF21 = store(sF17,i4,sF14) ).
cnf(u1798,negated_conjecture,
sF12 = sF20 ).
cnf(u1809,negated_conjecture,
sF12 = sF14 ).
cnf(u1814,negated_conjecture,
sF21 = store(sF17,i4,sF12) ).
cnf(u1819,negated_conjecture,
sF25 = store(sF23,i4,sF12) ).
cnf(u1832,negated_conjecture,
sF15 = store(sF11,i4,sF12) ).
cnf(u1842,negated_conjecture,
sF23 = store(sF19,i4,sF12) ).
cnf(u1850,negated_conjecture,
sF12 != sF18 ).
cnf(u1901,negated_conjecture,
sF12 = select(a1,i4) ).
cnf(u1911,negated_conjecture,
sF12 = select(a2,i4) ).
cnf(u1918,axiom,
sF18 = select(sF1,i5) ).
cnf(u1939,negated_conjecture,
sF25 != store(sF23,i4,sF18) ).
cnf(u1944,negated_conjecture,
sF18 != select(sF25,i4) ).
cnf(u1960,axiom,
sF16 = select(sF3,i5) ).
cnf(u1970,negated_conjecture,
sF25 = store(sF21,i4,sF12) ).
cnf(u1975,negated_conjecture,
sF12 = select(sF25,i4) ).
cnf(u1997,negated_conjecture,
sF19 = store(sF15,i5,sF16) ).
cnf(u2003,negated_conjecture,
sF12 != sF16 ).
cnf(u2008,negated_conjecture,
sF25 != store(sF23,i5,sF16) ).
cnf(u2018,axiom,
sF7 != store(sF3,i1,sF2) ).
cnf(u2057,negated_conjecture,
sF25 != store(sF21,i4,sF16) ).
cnf(u2079,axiom,
sF23 != store(sF19,i5,sF12) ).
cnf(u2096,negated_conjecture,
sF12 = select(sF21,i4) ).
cnf(u2107,negated_conjecture,
sF21 != store(sF17,i5,sF12) ).
cnf(u2143,negated_conjecture,
sF12 = select(sF23,i4) ).
cnf(u2183,negated_conjecture,
sF25 != store(sF23,i4,sF16) ).
cnf(u2191,axiom,
sF5 = store(sF1,i2,sF0) ).
cnf(u2195,axiom,
sF5 != store(sF1,i1,sF0) ).
cnf(u2212,negated_conjecture,
sF16 = select(a1,i5) ).
cnf(u2220,axiom,
sF16 = select(a2,i5) ).
cnf(u2233,negated_conjecture,
sF21 != store(sF17,i4,sF16) ).
cnf(u2246,axiom,
sF2 = select(sF7,i2) ).
cnf(u2258,negated_conjecture,
sF23 != store(sF19,i4,sF16) ).
cnf(u2331,negated_conjecture,
sF12 = select(sF15,i4) ).
cnf(u2358,axiom,
sF0 = select(sF5,i2) ).
cnf(u2488,negated_conjecture,
sF8 = sF10 ).
cnf(u2494,negated_conjecture,
sF11 = store(sF7,i3,sF8) ).
cnf(u2501,negated_conjecture,
sF8 = select(sF11,i3) ).
cnf(u2569,axiom,
sF4 = sF10 ).
cnf(u2576,axiom,
sF8 = select(sF7,i1) ).
cnf(u2593,axiom,
sF0 = sF10 ).
cnf(u2598,axiom,
sF0 = select(a2,i2) ).
cnf(u2604,negated_conjecture,
sF11 = store(sF7,i1,sF0) ).
cnf(u2609,negated_conjecture,
sF0 = select(sF11,i1) ).
cnf(u2620,axiom,
sF0 = select(sF7,i1) ).
cnf(u2786,axiom,
sF3 = store(a2,i1,sF0) ).
cnf(u2791,axiom,
sF7 = store(sF3,i2,sF0) ).
cnf(u2796,axiom,
sF7 != store(sF3,i1,sF0) ).
cnf(u2827,negated_conjecture,
select(a1,i1) = sF0 ).
cnf(u2876,axiom,
sF9 = store(sF5,i1,sF0) ).
cnf(u2923,axiom,
sF0 = select(sF3,i1) ).
cnf(u2943,axiom,
sF0 = select(sF9,i1) ).
cnf(u3010,axiom,
sF0 = select(sF7,i2) ).
cnf(u884,negated_conjecture,
( select(sF19,X0) = select(sF21,X0)
| i6 = X0 ) ).
cnf(u313,axiom,
( select(sF19,X0) = select(sF23,X0)
| i6 = X0 ) ).
cnf(u2477,negated_conjecture,
( select(sF7,X0) = select(sF9,X0)
| i3 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u302,axiom,
( select(a1,X0) = select(sF1,X0)
| i1 = X0 ) ).
cnf(u314,axiom,
( select(sF21,X0) = select(sF25,X0)
| i7 = X0 ) ).
cnf(u1529,negated_conjecture,
( select(sF23,X0) = select(sF25,X0)
| i6 = X0 ) ).
cnf(u305,axiom,
( select(sF3,X0) = select(sF7,X0)
| i2 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u1964,negated_conjecture,
( select(sF21,X0) = select(sF25,X0)
| i4 = X0 ) ).
cnf(u2408,negated_conjecture,
( select(sF19,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u2521,negated_conjecture,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u309,axiom,
( select(sF11,X0) = select(sF15,X0)
| i4 = X0 ) ).
cnf(u1836,negated_conjecture,
( select(sF19,X0) = select(sF23,X0)
| i4 = X0 ) ).
cnf(u312,axiom,
( select(sF17,X0) = select(sF21,X0)
| i6 = X0 ) ).
cnf(u307,axiom,
( select(sF7,X0) = select(sF11,X0)
| i3 = X0 ) ).
cnf(u2453,negated_conjecture,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0
| i5 = X0 ) ).
cnf(u311,axiom,
( select(sF15,X0) = select(sF19,X0)
| i5 = X0 ) ).
cnf(u2423,negated_conjecture,
( select(sF17,X0) = select(sF19,X0)
| i4 = X0 ) ).
cnf(u2892,negated_conjecture,
( select(sF1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u2882,negated_conjecture,
( select(sF1,X0) = select(sF3,X0)
| i1 = X0
| i2 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u304,axiom,
( select(sF1,X0) = select(sF5,X0)
| i2 = X0 ) ).
cnf(u2068,negated_conjecture,
( select(sF23,X0) = select(sF25,X0)
| i4 = X0 ) ).
cnf(u2843,negated_conjecture,
( select(sF7,X0) = select(sF11,X0)
| i1 = X0 ) ).
cnf(u2463,negated_conjecture,
( select(sF9,X0) = select(sF11,X0)
| i4 = X0
| i5 = X0 ) ).
cnf(u2975,negated_conjecture,
( select(sF3,X0) = select(sF5,X0)
| i2 = X0
| i4 = X0
| i5 = X0
| i1 = X0 ) ).
cnf(u2906,negated_conjecture,
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u303,axiom,
( select(a2,X0) = select(sF3,X0)
| i1 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u306,axiom,
( select(sF5,X0) = select(sF9,X0)
| i3 = X0 ) ).
cnf(u1403,negated_conjecture,
( select(sF17,X0) = select(sF19,X0)
| i6 = X0 ) ).
cnf(u310,axiom,
( select(sF13,X0) = select(sF17,X0)
| i5 = X0 ) ).
cnf(u2091,negated_conjecture,
( select(sF17,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u2963,negated_conjecture,
( select(sF5,X0) = select(sF7,X0)
| i4 = X0
| i5 = X0
| i1 = X0 ) ).
cnf(u691,negated_conjecture,
( select(sF21,X0) = select(sF23,X0)
| i7 = X0 ) ).
cnf(u2512,negated_conjecture,
( select(sF5,X0) = select(sF7,X0)
| i3 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u1385,negated_conjecture,
( select(sF21,X0) = select(sF25,X0)
| i6 = X0 ) ).
cnf(u308,axiom,
( select(sF9,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u2930,axiom,
( select(sF5,X0) = select(sF9,X0)
| i1 = X0 ) ).
cnf(u315,negated_conjecture,
( select(sF23,X0) = select(sF25,X0)
| i7 = X0 ) ).
cnf(u2310,negated_conjecture,
( select(sF21,X0) = select(sF23,X0)
| i4 = X0 ) ).
cnf(u2341,negated_conjecture,
( select(sF13,X0) = select(sF15,X0)
| i5 = X0
| i4 = X0 ) ).
cnf(u2854,negated_conjecture,
( select(sF7,X0) = select(sF9,X0)
| i4 = X0
| i5 = X0
| i1 = X0 ) ).
cnf(u2158,negated_conjecture,
( select(sF15,X0) = select(sF17,X0)
| i4 = X0
| i5 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV549-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 11:43:49 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.75/0.91 % (3328075)Input is clausal, will run a generic CNF schedule.
% 3.75/0.91 % (3328086)dis-21_1_sil=8000:lcm=predicate:random_seed=3911871736: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)
% 3.75/0.91 % (3328083)lrs+10_1_sil=8000:sp=occurrence:random_seed=3702074487:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.75/0.91 % (3328081)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4292559391:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.75/0.91 % (3328080)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=693438069:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.75/0.91 % (3328084)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3150646503:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.75/0.91 % (3328085)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2086900071:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.75/0.91 % (3328082)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1822504875:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.75/0.91 % (3328086)Refutation not found, incomplete strategy
% 3.75/0.91 % (3328086)------------------------------
% 3.75/0.91 % (3328086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328086)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328086)Termination reason: Refutation not found, incomplete strategy
% 3.75/0.91 % (3328086)Time elapsed: 0.001 s
% 3.75/0.91 % (3328086)Peak memory usage: 88 MB
% 3.75/0.91 % (3328086)Instructions burned: 3 (million)
% 3.75/0.91 % (3328083)Instruction limit reached!
% 3.75/0.91 % (3328083)------------------------------
% 3.75/0.91 % (3328083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328083)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328083)Termination reason: Instruction limit
% 3.75/0.91 % (3328083)Termination phase: Saturation
% 3.75/0.91 % (3328083)Time elapsed: 0.024 s
% 3.75/0.91 % (3328083)Peak memory usage: 88 MB
% 3.75/0.91 % (3328083)Instructions burned: 107 (million)
% 3.75/0.91 % (3328084)Instruction limit reached!
% 3.75/0.91 % (3328084)------------------------------
% 3.75/0.91 % (3328084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328084)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328084)Termination reason: Instruction limit
% 3.75/0.91 % (3328084)Termination phase: Saturation
% 3.75/0.91 % (3328084)Time elapsed: 0.026 s
% 3.75/0.91 % (3328084)Peak memory usage: 88 MB
% 3.75/0.91 % (3328084)Instructions burned: 116 (million)
% 3.75/0.91 % (3328085)Instruction limit reached!
% 3.75/0.91 % (3328085)------------------------------
% 3.75/0.91 % (3328085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328085)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328085)Termination reason: Instruction limit
% 3.75/0.91 % (3328085)Termination phase: Saturation
% 3.75/0.91 % (3328085)Time elapsed: 0.043 s
% 3.75/0.91 % (3328085)Peak memory usage: 89 MB
% 3.75/0.91 % (3328085)Instructions burned: 184 (million)
% 3.75/0.91 % (3328095)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3399223199:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 3.75/0.91 % (3328094)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=811732528:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.75/0.91 % (3328096)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2582921426:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 3.75/0.91 % (3328094)Refutation not found, incomplete strategy
% 3.75/0.91 % (3328094)------------------------------
% 3.75/0.91 % (3328094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328094)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328094)Termination reason: Refutation not found, incomplete strategy
% 3.75/0.91 % (3328094)Time elapsed: 0.023 s
% 3.75/0.91 % (3328094)Peak memory usage: 89 MB
% 3.75/0.91 % (3328094)Instructions burned: 96 (million)
% 3.75/0.91 % (3328086)------------------------------
% 3.75/0.91 % (3328086)------------------------------
% 3.75/0.91 % (3328095)Instruction limit reached!
% 3.75/0.91 % (3328095)------------------------------
% 3.75/0.91 % (3328095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328095)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328095)Termination reason: Instruction limit
% 3.75/0.91 % (3328095)Termination phase: Saturation
% 3.75/0.91 % (3328095)Time elapsed: 0.040 s
% 3.75/0.91 % (3328095)Peak memory usage: 88 MB
% 3.75/0.91 % (3328095)Instructions burned: 189 (million)
% 3.75/0.91 % (3328096)Instruction limit reached!
% 3.75/0.91 % (3328096)------------------------------
% 3.75/0.91 % (3328096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328096)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328096)Termination reason: Instruction limit
% 3.75/0.91 % (3328096)Termination phase: Saturation
% 3.75/0.91 % (3328096)Time elapsed: 0.050 s
% 3.75/0.91 % (3328096)Peak memory usage: 89 MB
% 3.75/0.91 % (3328096)Instructions burned: 219 (million)
% 3.75/0.91 % (3328100)lrs+10_64_to=lpo:sil=8000:random_seed=2046841614:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 3.75/0.91 % (3328101)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3291035745:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 3.75/0.91 % (3328100)Instruction limit reached!
% 3.75/0.91 % (3328100)------------------------------
% 3.75/0.91 % (3328100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328100)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328100)Termination reason: Instruction limit
% 3.75/0.91 % (3328100)Termination phase: Saturation
% 3.75/0.91 % (3328100)Time elapsed: 0.027 s
% 3.75/0.91 % (3328100)Peak memory usage: 88 MB
% 3.75/0.91 % (3328100)Instructions burned: 129 (million)
% 3.75/0.91 % (3328102)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1580842287:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 3.75/0.91 % (3328094)------------------------------
% 3.75/0.91 % (3328094)------------------------------
% 3.75/0.91 % (3328101)Refutation not found, incomplete strategy
% 3.75/0.91 % (3328101)------------------------------
% 3.75/0.91 % (3328101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328101)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328101)Termination reason: Refutation not found, incomplete strategy
% 3.75/0.91 % (3328101)Time elapsed: 0.041 s
% 3.75/0.91 % (3328101)Peak memory usage: 89 MB
% 3.75/0.91 % (3328101)Instructions burned: 169 (million)
% 3.75/0.91 % (3328102)First to succeed.
% 3.75/0.91 % (3328102)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3328075"
% 3.75/0.91 % (3328105)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3780047188:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 3.75/0.91 % (3328107)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=3524408081:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 3.75/0.91 % (3328107)Instruction limit reached!
% 3.75/0.91 % (3328107)------------------------------
% 3.75/0.91 % (3328107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/0.91 % (3328107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/0.91 % (3328107)CaDiCaL version: 2.1.3
% 3.75/0.91 % (3328107)Termination reason: Instruction limit
% 3.75/0.91 % (3328107)Termination phase: Saturation
% 3.75/0.91 % (3328107)Time elapsed: 0.023 s
% 3.75/0.91 % (3328107)Peak memory usage: 89 MB
% 3.75/0.91 % (3328107)Instructions burned: 106 (million)
% 3.75/0.91 % (3328101)------------------------------
% 3.75/0.91 % (3328101)------------------------------
% 3.75/0.91 % SZS status Satisfiable for theBenchmark
% 3.75/0.91 % SZS output start Saturation.
% See solution above
% 3.75/1.01 % SZS output start Definitions and Model Updates.
% 3.75/1.01 % SZS output end Definitions and Model Updates.
% 3.75/1.01 % (3328102)------------------------------
% 3.75/1.01 % (3328102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.01 % (3328102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.01 % (3328102)CaDiCaL version: 2.1.3
% 3.75/1.01 % (3328102)Termination reason: Satisfiable
% 3.75/1.01 % (3328102)Time elapsed: 0.033 s
% 3.75/1.01 % (3328102)Peak memory usage: 89 MB
% 3.75/1.01 % (3328102)Instructions burned: 91 (million)
% 3.75/1.01 % (3328102)------------------------------
% 3.75/1.01 % (3328102)------------------------------
% 3.75/1.01 % (3328075)Success in time 0.603 s
% 3.75/1.01 % Vampire exiting
%------------------------------------------------------------------------------