%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV536-1.004 : 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 : n006.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:16 PM UTC 2026
% Result : Satisfiable 6.87s 1.76s
% Output : Saturation 6.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u64,negated_conjecture,
sF26 != sF27 ).
cnf(u69,axiom,
select(a1,i1) = sF0 ).
cnf(u74,axiom,
store(a1,i1,sF0) = sF1 ).
cnf(u79,axiom,
store(sF1,i1,sF0) = sF2 ).
cnf(u84,axiom,
select(sF2,i3) = sF3 ).
cnf(u89,axiom,
store(sF2,i0,sF3) = sF4 ).
cnf(u94,axiom,
select(sF2,i0) = sF5 ).
cnf(u99,axiom,
store(sF4,i3,sF5) = sF6 ).
cnf(u104,axiom,
select(sF6,i2) = sF7 ).
cnf(u109,axiom,
store(sF6,i3,sF7) = sF8 ).
cnf(u114,axiom,
select(sF6,i3) = sF9 ).
cnf(u119,axiom,
store(sF8,i2,sF9) = sF10 ).
cnf(u124,axiom,
select(sF10,i0) = sF11 ).
cnf(u129,axiom,
store(sF10,i2,sF11) = sF12 ).
cnf(u134,axiom,
select(sF10,i2) = sF13 ).
cnf(u139,axiom,
store(sF12,i0,sF13) = sF14 ).
cnf(u144,axiom,
store(sF2,i3,sF5) = sF15 ).
cnf(u149,axiom,
store(sF15,i0,sF3) = sF16 ).
cnf(u154,axiom,
select(sF16,i2) = sF17 ).
cnf(u159,axiom,
store(sF16,i3,sF17) = sF18 ).
cnf(u164,axiom,
select(sF16,i3) = sF19 ).
cnf(u169,axiom,
store(sF18,i2,sF19) = sF20 ).
cnf(u174,axiom,
select(sF20,i3) = sF21 ).
cnf(u179,axiom,
store(sF20,i0,sF21) = sF22 ).
cnf(u184,axiom,
select(sF20,i0) = sF23 ).
cnf(u189,axiom,
store(sF22,i3,sF23) = sF24 ).
cnf(u194,axiom,
sk(sF14,sF24) = sF25 ).
cnf(u199,axiom,
select(sF14,sF25) = sF26 ).
cnf(u204,axiom,
select(sF24,sF25) = sF27 ).
cnf(u223,axiom,
sF19 = select(sF20,i2) ).
cnf(u228,axiom,
sF11 = select(sF12,i2) ).
cnf(u233,axiom,
sF9 = select(sF10,i2) ).
cnf(u238,axiom,
sF23 = select(sF24,i3) ).
cnf(u243,axiom,
sF17 = select(sF18,i3) ).
cnf(u248,axiom,
sF7 = select(sF8,i3) ).
cnf(u253,axiom,
sF5 = select(sF6,i3) ).
cnf(u258,axiom,
sF5 = select(sF15,i3) ).
cnf(u263,axiom,
sF21 = select(sF22,i0) ).
cnf(u268,axiom,
sF3 = select(sF16,i0) ).
cnf(u273,axiom,
sF13 = select(sF14,i0) ).
cnf(u278,axiom,
sF3 = select(sF4,i0) ).
cnf(u283,axiom,
sF0 = select(sF2,i1) ).
cnf(u288,axiom,
sF0 = select(sF1,i1) ).
cnf(u309,axiom,
sF9 = sF13 ).
cnf(u315,axiom,
sF14 = store(sF12,i0,sF9) ).
cnf(u322,axiom,
sF5 = sF9 ).
cnf(u328,axiom,
sF10 = store(sF8,i2,sF5) ).
cnf(u337,axiom,
sF14 = store(sF12,i0,sF5) ).
cnf(u342,axiom,
sF5 = select(sF14,i0) ).
cnf(u353,axiom,
sF5 = sF13 ).
cnf(u362,axiom,
i0 != i2 ).
cnf(u367,axiom,
sF11 = select(sF14,i2) ).
cnf(u376,axiom,
i0 != i3 ).
cnf(u381,axiom,
sF5 = sF19 ).
cnf(u399,axiom,
sF5 != select(sF14,i3) ).
cnf(u406,axiom,
sF3 = select(sF4,i3) ).
cnf(u412,axiom,
sF3 = select(sF16,i3) ).
cnf(u417,axiom,
sF21 = select(sF22,i3) ).
cnf(u422,axiom,
sF22 != store(sF20,i3,sF21) ).
cnf(u428,axiom,
sF16 = store(sF15,i3,sF3) ).
cnf(u433,axiom,
sF11 != select(sF10,i3) ).
cnf(u439,axiom,
sF4 != store(sF2,i3,sF3) ).
cnf(u444,axiom,
sF14 != store(sF12,i3,sF5) ).
cnf(u450,axiom,
sF21 != sF23 ).
cnf(u457,axiom,
sF3 = sF5 ).
cnf(u467,axiom,
sF20 = store(sF18,i2,sF5) ).
cnf(u478,axiom,
sF3 = select(sF6,i0) ).
cnf(u485,axiom,
sF5 = select(sF10,i2) ).
cnf(u500,axiom,
sF21 = select(sF24,i0) ).
cnf(u508,axiom,
i3 != i2 ).
cnf(u513,axiom,
sF7 = select(sF10,i3) ).
cnf(u530,axiom,
sF5 != select(sF10,i3) ).
cnf(u535,axiom,
sF11 != select(sF14,i3) ).
cnf(u540,axiom,
sF10 != store(sF8,i3,sF5) ).
cnf(u546,axiom,
sF11 != select(sF12,i3) ).
cnf(u553,axiom,
sF17 != select(sF16,i3) ).
cnf(u559,axiom,
sF12 != store(sF10,i3,sF11) ).
cnf(u567,axiom,
sF5 != select(sF20,i3) ).
cnf(u572,axiom,
sF20 != store(sF18,i3,sF5) ).
cnf(u579,axiom,
sF5 != sF7 ).
cnf(u594,axiom,
sF17 = select(sF20,i3) ).
cnf(u632,axiom,
sF8 != store(sF6,i3,sF5) ).
cnf(u644,axiom,
sF5 != sF17 ).
cnf(u657,axiom,
sF5 != sF21 ).
cnf(u665,axiom,
sF17 = sF21 ).
cnf(u723,axiom,
sF7 != sF11 ).
cnf(u730,axiom,
sF3 != sF17 ).
cnf(u737,axiom,
sF3 != select(sF10,i3) ).
cnf(u743,axiom,
sF3 != select(sF20,i3) ).
cnf(u749,axiom,
sF3 != sF7 ).
cnf(u772,axiom,
sF8 != store(sF6,i3,sF3) ).
cnf(u803,axiom,
sF5 = sF11 ).
cnf(u811,axiom,
sF5 = select(sF16,i3) ).
cnf(u841,axiom,
sF18 != store(sF16,i3,sF5) ).
cnf(u850,axiom,
sF24 = store(sF22,i3,sF5) ).
cnf(u856,axiom,
sF5 = sF23 ).
cnf(u867,axiom,
sF22 != store(sF20,i0,sF5) ).
cnf(u875,axiom,
i3 = sF25 ).
cnf(u878,axiom,
i0 != sF25 ).
cnf(u882,axiom,
sF27 != select(sF20,sF25) ).
cnf(u901,axiom,
sF3 = sF11 ).
cnf(u925,axiom,
sF23 = sF27 ).
cnf(u929,axiom,
sF3 != sF26 ).
cnf(u942,axiom,
sF26 = select(sF10,sF25) ).
cnf(u959,axiom,
sF5 = sF27 ).
cnf(u985,axiom,
sF3 = sF23 ).
cnf(u999,axiom,
sF3 = sF27 ).
cnf(u1006,axiom,
sF12 != store(sF10,i3,sF3) ).
cnf(u1014,axiom,
sF24 = store(sF22,i3,sF3) ).
cnf(u1044,axiom,
sF27 = select(sF16,sF25) ).
cnf(u1056,axiom,
sF26 != select(sF6,sF25) ).
cnf(u1068,axiom,
sF27 = select(sF2,sF25) ).
cnf(u1076,axiom,
sF22 != store(sF20,i3,sF5) ).
cnf(u1092,axiom,
sF26 != select(sF2,sF25) ).
cnf(u1104,axiom,
sF12 = store(sF10,i2,sF3) ).
cnf(u1122,axiom,
i2 != sF25 ).
cnf(u1135,axiom,
sF5 != select(sF2,i2) ).
cnf(u1184,axiom,
sF26 = select(sF14,i3) ).
cnf(u1199,axiom,
sF22 = store(sF20,i0,sF17) ).
cnf(u1206,axiom,
sF22 != store(sF20,i3,sF17) ).
cnf(u1211,axiom,
sF17 = select(sF2,i2) ).
cnf(u1217,axiom,
sF7 = select(sF2,i2) ).
cnf(u1224,axiom,
sF3 != select(sF14,i3) ).
cnf(u1229,axiom,
sF3 != select(sF12,i3) ).
cnf(u1270,axiom,
sF6 = store(sF4,i3,sF3) ).
cnf(u1275,axiom,
sF15 = store(sF2,i3,sF3) ).
cnf(u1280,axiom,
sF10 = store(sF8,i2,sF3) ).
cnf(u1305,axiom,
sF7 = sF26 ).
cnf(u1316,axiom,
sF3 = sF19 ).
cnf(u1325,axiom,
sF20 = store(sF18,i2,sF3) ).
cnf(u1332,axiom,
sF7 = sF17 ).
cnf(u1339,axiom,
sF18 = store(sF16,i3,sF7) ).
cnf(u1372,axiom,
sF3 = select(sF20,i2) ).
cnf(u1390,axiom,
sF20 != store(sF18,i3,sF3) ).
cnf(u1406,axiom,
sF18 != store(sF16,i3,sF3) ).
cnf(u1420,axiom,
sF22 != store(sF20,i3,sF7) ).
cnf(u1428,axiom,
sF14 = store(sF12,i0,sF3) ).
cnf(u1436,axiom,
sF14 != store(sF12,i3,sF3) ).
cnf(u1448,axiom,
sF10 != store(sF8,i3,sF3) ).
cnf(u1480,axiom,
sF3 = select(sF24,i3) ).
cnf(u1490,axiom,
sF22 != store(sF20,i0,sF3) ).
cnf(u1506,axiom,
sF22 != store(sF20,i3,sF3) ).
cnf(u1513,axiom,
sF3 = select(sF12,i2) ).
cnf(u1524,axiom,
sF3 = select(sF14,i2) ).
cnf(u1533,axiom,
sF22 = store(sF20,i0,sF7) ).
cnf(u1538,axiom,
sF7 = select(sF22,i0) ).
cnf(u1548,axiom,
sF7 = sF21 ).
cnf(u1554,axiom,
sF7 = select(sF24,i0) ).
cnf(u1561,axiom,
sF3 = select(sF6,i3) ).
cnf(u1572,axiom,
sF3 = select(sF15,i3) ).
cnf(u1577,axiom,
sF4 != sF15 ).
cnf(u1584,axiom,
sF3 = select(sF10,i2) ).
cnf(u1593,axiom,
sF3 = sF9 ).
cnf(u1616,axiom,
sF3 = sF13 ).
cnf(u1630,axiom,
sF7 = select(sF18,i3) ).
cnf(u1641,axiom,
sF3 = select(sF14,i0) ).
cnf(u1652,axiom,
sF7 = select(sF20,i3) ).
cnf(u1675,axiom,
sF3 = select(sF2,i0) ).
cnf(u300,axiom,
( select(sF22,X0) = select(sF24,X0)
| i3 = X0 ) ).
cnf(u291,axiom,
( select(sF1,X0) = select(sF2,X0)
| i1 = X0 ) ).
cnf(u462,axiom,
( select(sF2,X0) = select(sF16,X0)
| i0 = X0
| i3 = X0 ) ).
cnf(u292,axiom,
( select(sF2,X0) = select(sF4,X0)
| i0 = X0 ) ).
cnf(u302,axiom,
( select(sF12,X0) = select(sF10,X0)
| i2 = X0 ) ).
cnf(u299,axiom,
( select(sF16,X0) = select(sF18,X0)
| i3 = X0 ) ).
cnf(u1353,axiom,
( select(sF15,X0) = select(sF16,X0)
| i3 = X0 ) ).
cnf(u293,axiom,
( select(sF12,X0) = select(sF14,X0)
| i0 = X0 ) ).
cnf(u472,axiom,
( select(sF2,X0) = select(sF6,X0)
| i0 = X0
| i3 = X0 ) ).
cnf(u346,axiom,
( select(a1,X0) = select(sF2,X0)
| i1 = X0 ) ).
cnf(u1605,axiom,
( select(sF2,X0) = select(sF16,X0)
| i3 = X0 ) ).
cnf(u301,axiom,
( select(sF8,X0) = select(sF10,X0)
| i2 = X0 ) ).
cnf(u294,axiom,
( select(sF15,X0) = select(sF16,X0)
| i0 = X0 ) ).
cnf(u494,axiom,
( select(sF20,X0) = select(sF24,X0)
| i0 = X0
| i3 = X0 ) ).
cnf(u296,axiom,
( select(sF2,X0) = select(sF15,X0)
| i3 = X0 ) ).
cnf(u584,axiom,
( select(sF14,X0) = select(sF10,X0)
| i0 = X0
| i2 = X0 ) ).
cnf(u588,axiom,
( select(sF16,X0) = select(sF20,X0)
| i3 = X0
| i2 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u295,axiom,
( select(sF20,X0) = select(sF22,X0)
| i0 = X0 ) ).
cnf(u297,axiom,
( select(sF4,X0) = select(sF6,X0)
| i3 = X0 ) ).
cnf(u290,axiom,
( select(a1,X0) = select(sF1,X0)
| i1 = X0 ) ).
cnf(u303,axiom,
( select(sF20,X0) = select(sF18,X0)
| i2 = X0 ) ).
cnf(u505,axiom,
( select(sF6,X0) = select(sF10,X0)
| i3 = X0
| i2 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u298,axiom,
( select(sF6,X0) = select(sF8,X0)
| i3 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV536-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:36:25 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 5.31/1.56 % (3904286)Input is clausal, will run a generic CNF schedule.
% 5.31/1.56 % (3904295)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2160074304:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.31/1.56 % (3904295)Instruction limit reached!
% 5.31/1.56 % (3904295)------------------------------
% 5.31/1.56 % (3904295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904295)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904295)Termination reason: Instruction limit
% 5.31/1.56 % (3904295)Termination phase: Saturation
% 5.31/1.56 % (3904295)Time elapsed: 0.026 s
% 5.31/1.56 % (3904295)Peak memory usage: 89 MB
% 5.31/1.56 % (3904295)Instructions burned: 118 (million)
% 5.31/1.56 % (3904292)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3998936888:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.31/1.56 % (3904296)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1136932482:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.31/1.56 % (3904293)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1877551318:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.31/1.56 % (3904291)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=1052149375:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.31/1.56 % (3904294)lrs+10_1_sil=8000:sp=occurrence:random_seed=2500008444:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.31/1.56 % (3904297)dis-21_1_sil=8000:lcm=predicate:random_seed=3264854814:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.31/1.56 % (3904297)Refutation not found, incomplete strategy
% 5.31/1.56 % (3904297)------------------------------
% 5.31/1.56 % (3904297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904297)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904297)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.56 % (3904297)Time elapsed: 0.004 s
% 5.31/1.56 % (3904297)Peak memory usage: 88 MB
% 5.31/1.56 % (3904297)Instructions burned: 7 (million)
% 5.31/1.56 % (3904294)Instruction limit reached!
% 5.31/1.56 % (3904294)------------------------------
% 5.31/1.56 % (3904294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904294)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904294)Termination reason: Instruction limit
% 5.31/1.56 % (3904294)Termination phase: Saturation
% 5.31/1.56 % (3904294)Time elapsed: 0.044 s
% 5.31/1.56 % (3904294)Peak memory usage: 89 MB
% 5.31/1.56 % (3904294)Instructions burned: 108 (million)
% 5.31/1.56 % (3904296)Instruction limit reached!
% 5.31/1.56 % (3904296)------------------------------
% 5.31/1.56 % (3904296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904296)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904296)Termination reason: Instruction limit
% 5.31/1.56 % (3904296)Termination phase: Saturation
% 5.31/1.56 % (3904296)Time elapsed: 0.074 s
% 5.31/1.56 % (3904296)Peak memory usage: 89 MB
% 5.31/1.56 % (3904296)Instructions burned: 182 (million)
% 5.31/1.56 % (3904299)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=2858734036:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.31/1.56 % (3904299)Instruction limit reached!
% 5.31/1.56 % (3904299)------------------------------
% 5.31/1.56 % (3904299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904299)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904299)Termination reason: Instruction limit
% 5.31/1.56 % (3904299)Termination phase: Saturation
% 5.31/1.56 % (3904299)Time elapsed: 0.032 s
% 5.31/1.56 % (3904299)Peak memory usage: 89 MB
% 5.31/1.56 % (3904299)Instructions burned: 146 (million)
% 5.31/1.56 % (3904306)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=563532366:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.31/1.56 % (3904307)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4276732443:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.31/1.56 % (3904297)------------------------------
% 5.31/1.56 % (3904297)------------------------------
% 5.31/1.56 % (3904309)lrs+10_64_to=lpo:sil=8000:random_seed=824890848:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.31/1.56 % (3904306)Instruction limit reached!
% 5.31/1.56 % (3904306)------------------------------
% 5.31/1.56 % (3904306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904306)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904306)Termination reason: Instruction limit
% 5.31/1.56 % (3904306)Termination phase: Saturation
% 5.31/1.56 % (3904306)Time elapsed: 0.080 s
% 5.31/1.56 % (3904306)Peak memory usage: 92 MB
% 5.31/1.56 % (3904306)Instructions burned: 192 (million)
% 5.31/1.56 % (3904309)Instruction limit reached!
% 5.31/1.56 % (3904309)------------------------------
% 5.31/1.56 % (3904309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904309)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904309)Termination reason: Instruction limit
% 5.31/1.56 % (3904309)Termination phase: Saturation
% 5.31/1.56 % (3904309)Time elapsed: 0.028 s
% 5.31/1.56 % (3904309)Peak memory usage: 90 MB
% 5.31/1.56 % (3904309)Instructions burned: 127 (million)
% 5.31/1.56 % (3904307)Instruction limit reached!
% 5.31/1.56 % (3904307)------------------------------
% 5.31/1.56 % (3904307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904307)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904307)Termination reason: Instruction limit
% 5.31/1.56 % (3904307)Termination phase: Saturation
% 5.31/1.56 % (3904307)Time elapsed: 0.089 s
% 5.31/1.56 % (3904307)Peak memory usage: 90 MB
% 5.31/1.56 % (3904307)Instructions burned: 221 (million)
% 5.31/1.56 % (3904312)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1101225155:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.31/1.56 % (3904314)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2713444775:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.31/1.56 % (3904315)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1950858643:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.31/1.56 % (3904314)First to succeed.
% 5.31/1.56 % (3904314)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3904286"
% 5.31/1.56 % (3904312)Instruction limit reached!
% 5.31/1.56 % (3904312)------------------------------
% 5.31/1.56 % (3904312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904312)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904312)Termination reason: Instruction limit
% 5.31/1.56 % (3904312)Termination phase: Saturation
% 5.31/1.56 % (3904312)Time elapsed: 0.082 s
% 5.31/1.56 % (3904312)Peak memory usage: 91 MB
% 5.31/1.56 % (3904312)Instructions burned: 195 (million)
% 5.31/1.56 % (3904316)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=1967406710:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.31/1.56 % (3904316)Instruction limit reached!
% 5.31/1.56 % (3904316)------------------------------
% 5.31/1.56 % (3904316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.56 % (3904316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.56 % (3904316)CaDiCaL version: 2.1.3
% 5.31/1.56 % (3904316)Termination reason: Instruction limit
% 5.31/1.56 % (3904316)Termination phase: Saturation
% 5.31/1.56 % (3904316)Time elapsed: 0.041 s
% 5.31/1.56 % (3904316)Peak memory usage: 89 MB
% 5.31/1.56 % (3904316)Instructions burned: 108 (million)
% 5.31/1.56 % (3904320)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2042493257:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.87/1.76 % (3904291)Refutation not found, incomplete strategy
% 6.87/1.76 % (3904291)------------------------------
% 6.87/1.76 % (3904291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.76 % (3904291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.76 % (3904291)CaDiCaL version: 2.1.3
% 6.87/1.76 % (3904291)Termination reason: Refutation not found, incomplete strategy
% 6.87/1.76 % (3904291)Time elapsed: 0.661 s
% 6.87/1.76 % (3904291)Peak memory usage: 127 MB
% 6.87/1.76 % (3904291)Instructions burned: 972 (million)
% 6.87/1.76 % (3904293)Refutation not found, incomplete strategy
% 6.87/1.76 % (3904293)------------------------------
% 6.87/1.76 % (3904293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.76 % (3904293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.76 % (3904293)CaDiCaL version: 2.1.3
% 6.87/1.76 % (3904293)Termination reason: Refutation not found, incomplete strategy
% 6.87/1.76 % (3904293)Time elapsed: 0.672 s
% 6.87/1.76 % (3904293)Peak memory usage: 127 MB
% 6.87/1.76 % (3904293)Instructions burned: 996 (million)
% 6.87/1.76 % (3904320)Instruction limit reached!
% 6.87/1.76 % (3904320)------------------------------
% 6.87/1.76 % (3904320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.76 % (3904320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.76 % (3904320)CaDiCaL version: 2.1.3
% 6.87/1.76 % (3904320)Termination reason: Instruction limit
% 6.87/1.76 % (3904320)Termination phase: Saturation
% 6.87/1.76 % (3904320)Time elapsed: 0.044 s
% 6.87/1.76 % (3904320)Peak memory usage: 89 MB
% 6.87/1.76 % (3904320)Instructions burned: 108 (million)
% 6.87/1.76 % (3904322)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3204833212:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 6.87/1.76 % (3904322)Refutation not found, incomplete strategy
% 6.87/1.76 % (3904322)------------------------------
% 6.87/1.76 % (3904322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.76 % (3904322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.76 % (3904322)CaDiCaL version: 2.1.3
% 6.87/1.76 % (3904322)Termination reason: Refutation not found, incomplete strategy
% 6.87/1.76 % (3904322)Time elapsed: 0.012 s
% 6.87/1.76 % (3904322)Peak memory usage: 88 MB
% 6.87/1.76 % (3904322)Instructions burned: 24 (million)
% 6.87/1.76 % SZS status Satisfiable for theBenchmark
% 6.87/1.76 % SZS output start Saturation.
% See solution above
% 6.87/1.76 % SZS output start Definitions and Model Updates.
% 6.87/1.76 % SZS output end Definitions and Model Updates.
% 6.87/1.76 % (3904314)------------------------------
% 6.87/1.76 % (3904314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.76 % (3904314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.76 % (3904314)CaDiCaL version: 2.1.3
% 6.87/1.76 % (3904314)Termination reason: Satisfiable
% 6.87/1.76 % (3904314)Time elapsed: 0.034 s
% 6.87/1.76 % (3904314)Peak memory usage: 89 MB
% 6.87/1.76 % (3904314)Instructions burned: 53 (million)
% 6.87/1.76 % (3904314)------------------------------
% 6.87/1.76 % (3904314)------------------------------
% 6.87/1.76 % (3904286)Success in time 0.894 s
% 6.87/1.76 % Vampire exiting
%------------------------------------------------------------------------------