%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV532-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:16:55 PM UTC 2026
% Result : Satisfiable 6.42s 1.69s
% Output : Saturation 6.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u58,negated_conjecture,
sF14 != sF24 ).
cnf(u63,axiom,
select(a1,i1) = sF0 ).
cnf(u68,axiom,
store(a1,i1,sF0) = sF1 ).
cnf(u73,axiom,
store(sF1,i1,sF0) = sF2 ).
cnf(u78,axiom,
select(sF2,i3) = sF3 ).
cnf(u83,axiom,
store(sF2,i0,sF3) = sF4 ).
cnf(u88,axiom,
select(sF2,i0) = sF5 ).
cnf(u93,axiom,
store(sF4,i3,sF5) = sF6 ).
cnf(u98,axiom,
select(sF6,i2) = sF7 ).
cnf(u103,axiom,
store(sF6,i3,sF7) = sF8 ).
cnf(u108,axiom,
select(sF6,i3) = sF9 ).
cnf(u113,axiom,
store(sF8,i2,sF9) = sF10 ).
cnf(u118,axiom,
select(sF10,i0) = sF11 ).
cnf(u123,axiom,
store(sF10,i2,sF11) = sF12 ).
cnf(u128,axiom,
select(sF10,i2) = sF13 ).
cnf(u133,axiom,
store(sF12,i0,sF13) = sF14 ).
cnf(u138,axiom,
store(sF2,i3,sF5) = sF15 ).
cnf(u143,axiom,
store(sF15,i0,sF3) = sF16 ).
cnf(u148,axiom,
select(sF16,i2) = sF17 ).
cnf(u153,axiom,
store(sF16,i3,sF17) = sF18 ).
cnf(u158,axiom,
select(sF16,i3) = sF19 ).
cnf(u163,axiom,
store(sF18,i2,sF19) = sF20 ).
cnf(u168,axiom,
select(sF20,i3) = sF21 ).
cnf(u173,axiom,
store(sF20,i0,sF21) = sF22 ).
cnf(u178,axiom,
select(sF20,i0) = sF23 ).
cnf(u183,axiom,
store(sF22,i3,sF23) = sF24 ).
cnf(u202,axiom,
sF19 = select(sF20,i2) ).
cnf(u207,axiom,
sF11 = select(sF12,i2) ).
cnf(u212,axiom,
sF9 = select(sF10,i2) ).
cnf(u217,axiom,
sF23 = select(sF24,i3) ).
cnf(u222,axiom,
sF17 = select(sF18,i3) ).
cnf(u227,axiom,
sF7 = select(sF8,i3) ).
cnf(u232,axiom,
sF5 = select(sF6,i3) ).
cnf(u237,axiom,
sF5 = select(sF15,i3) ).
cnf(u242,axiom,
sF21 = select(sF22,i0) ).
cnf(u247,axiom,
sF3 = select(sF16,i0) ).
cnf(u252,axiom,
sF13 = select(sF14,i0) ).
cnf(u257,axiom,
sF3 = select(sF4,i0) ).
cnf(u262,axiom,
sF0 = select(sF2,i1) ).
cnf(u267,axiom,
sF0 = select(sF1,i1) ).
cnf(u288,axiom,
sF9 = sF13 ).
cnf(u294,axiom,
sF14 = store(sF12,i0,sF9) ).
cnf(u301,axiom,
sF5 = sF9 ).
cnf(u307,axiom,
sF10 = store(sF8,i2,sF5) ).
cnf(u316,axiom,
sF14 = store(sF12,i0,sF5) ).
cnf(u321,axiom,
sF5 = select(sF14,i0) ).
cnf(u328,axiom,
sF5 = sF13 ).
cnf(u342,axiom,
sF5 = select(sF10,i2) ).
cnf(u354,axiom,
i0 != i3 ).
cnf(u359,axiom,
sF5 = sF19 ).
cnf(u366,axiom,
sF20 = store(sF18,i2,sF5) ).
cnf(u373,axiom,
sF5 = select(sF20,i2) ).
cnf(u386,axiom,
sF3 = select(sF6,i0) ).
cnf(u404,axiom,
sF5 != select(sF14,i3) ).
cnf(u411,axiom,
sF3 = select(sF4,i3) ).
cnf(u416,axiom,
sF3 != select(sF16,i3) ).
cnf(u422,axiom,
sF21 = select(sF22,i3) ).
cnf(u427,axiom,
sF22 != store(sF20,i3,sF21) ).
cnf(u432,axiom,
sF16 != store(sF15,i3,sF3) ).
cnf(u439,axiom,
sF11 = select(sF10,i3) ).
cnf(u444,axiom,
sF4 != store(sF2,i3,sF3) ).
cnf(u449,axiom,
sF14 != store(sF12,i3,sF5) ).
cnf(u456,axiom,
sF21 = sF23 ).
cnf(u461,axiom,
sF3 != sF5 ).
cnf(u474,axiom,
i3 != i2 ).
cnf(u479,axiom,
sF7 = select(sF10,i3) ).
cnf(u497,axiom,
sF5 != select(sF20,i3) ).
cnf(u502,axiom,
sF20 != store(sF18,i3,sF5) ).
cnf(u507,axiom,
sF5 != select(sF10,i3) ).
cnf(u512,axiom,
sF10 != store(sF8,i3,sF5) ).
cnf(u519,axiom,
sF11 = select(sF12,i3) ).
cnf(u525,axiom,
sF17 != select(sF16,i3) ).
cnf(u531,axiom,
sF12 != store(sF10,i3,sF11) ).
cnf(u543,axiom,
sF5 != sF7 ).
cnf(u556,axiom,
sF17 = select(sF20,i3) ).
cnf(u592,axiom,
sF8 != store(sF6,i3,sF5) ).
cnf(u604,axiom,
sF5 != sF17 ).
cnf(u616,axiom,
sF5 != sF21 ).
cnf(u625,axiom,
sF17 = sF21 ).
cnf(u687,axiom,
sF7 = sF11 ).
cnf(u694,axiom,
sF3 = sF17 ).
cnf(u701,axiom,
sF3 = select(sF10,i3) ).
cnf(u706,axiom,
sF3 = select(sF20,i3) ).
cnf(u714,axiom,
sF3 = sF7 ).
cnf(u737,axiom,
sF8 = store(sF6,i3,sF3) ).
cnf(u744,axiom,
sF3 = sF21 ).
cnf(u768,axiom,
sF5 = select(sF16,i3) ).
cnf(u774,axiom,
sF5 != sF11 ).
cnf(u802,axiom,
sF18 != store(sF16,i3,sF5) ).
cnf(u810,axiom,
sF24 != store(sF22,i3,sF5) ).
cnf(u818,axiom,
sF5 != sF23 ).
cnf(u829,axiom,
sF22 != store(sF20,i0,sF5) ).
cnf(u845,axiom,
sF3 = sF11 ).
cnf(u860,axiom,
sF3 = sF23 ).
cnf(u867,axiom,
sF12 != store(sF10,i3,sF3) ).
cnf(u875,axiom,
sF24 = store(sF22,i3,sF3) ).
cnf(u894,axiom,
sF5 != select(sF12,i3) ).
cnf(u904,axiom,
sF22 != store(sF20,i3,sF5) ).
cnf(u1020,axiom,
sF12 = store(sF10,i2,sF3) ).
cnf(u1046,axiom,
i0 != i2 ).
cnf(u1087,axiom,
sF24 = store(sF22,i3,sF17) ).
cnf(u1103,axiom,
sF22 = store(sF20,i0,sF17) ).
cnf(u1108,axiom,
sF22 != store(sF20,i3,sF17) ).
cnf(u1118,axiom,
sF17 = sF23 ).
cnf(u1129,axiom,
sF17 = select(sF2,i2) ).
cnf(u1136,axiom,
sF3 = select(sF2,i2) ).
cnf(u1150,axiom,
sF22 = store(sF20,i0,sF3) ).
cnf(u1155,axiom,
sF22 != store(sF20,i3,sF3) ).
cnf(u1162,axiom,
sF18 = store(sF16,i3,sF3) ).
cnf(u1213,axiom,
sF3 = select(sF8,i3) ).
cnf(u1224,axiom,
sF5 != select(sF24,i3) ).
cnf(u1237,axiom,
sF5 != select(sF22,i0) ).
cnf(u1261,axiom,
sF3 = select(sF24,i3) ).
cnf(u1270,axiom,
sF3 = select(sF12,i2) ).
cnf(u1279,axiom,
sF3 = select(sF22,i0) ).
cnf(u1288,axiom,
sF3 = select(sF18,i3) ).
cnf(u269,axiom,
( select(a1,X0) = select(sF1,X0)
| i1 = X0 ) ).
cnf(u279,axiom,
( select(sF22,X0) = select(sF24,X0)
| i3 = X0 ) ).
cnf(u550,axiom,
( select(sF16,X0) = select(sF20,X0)
| i3 = X0
| i2 = X0 ) ).
cnf(u272,axiom,
( select(sF12,X0) = select(sF14,X0)
| i0 = X0 ) ).
cnf(u282,axiom,
( select(sF20,X0) = select(sF18,X0)
| i2 = X0 ) ).
cnf(u275,axiom,
( select(sF2,X0) = select(sF15,X0)
| i3 = X0 ) ).
cnf(u376,axiom,
( select(sF2,X0) = select(sF16,X0)
| i0 = X0
| i3 = X0 ) ).
cnf(u276,axiom,
( select(sF4,X0) = select(sF6,X0)
| i3 = X0 ) ).
cnf(u271,axiom,
( select(sF2,X0) = select(sF4,X0)
| i0 = X0 ) ).
cnf(u471,axiom,
( select(sF6,X0) = select(sF10,X0)
| i3 = X0
| i2 = X0 ) ).
cnf(u273,axiom,
( select(sF15,X0) = select(sF16,X0)
| i0 = X0 ) ).
cnf(u277,axiom,
( select(sF6,X0) = select(sF8,X0)
| i3 = X0 ) ).
cnf(u270,axiom,
( select(sF1,X0) = select(sF2,X0)
| i1 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u278,axiom,
( select(sF16,X0) = select(sF18,X0)
| i3 = X0 ) ).
cnf(u280,axiom,
( select(sF8,X0) = select(sF10,X0)
| i2 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u332,axiom,
( select(a1,X0) = select(sF2,X0)
| i1 = X0 ) ).
cnf(u274,axiom,
( select(sF20,X0) = select(sF22,X0)
| i0 = X0 ) ).
cnf(u281,axiom,
( select(sF12,X0) = select(sF10,X0)
| i2 = X0 ) ).
cnf(u382,axiom,
( select(sF2,X0) = select(sF6,X0)
| i0 = X0
| i3 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV532-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n026.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 11:37:27 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.80/1.49 % (3798368)Input is clausal, will run a generic CNF schedule.
% 4.80/1.49 % (3798379)dis-21_1_sil=8000:lcm=predicate:random_seed=2099973662: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)
% 4.80/1.49 % (3798379)Refutation not found, incomplete strategy
% 4.80/1.49 % (3798379)------------------------------
% 4.80/1.49 % (3798379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798379)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798379)Termination reason: Refutation not found, incomplete strategy
% 4.80/1.49 % (3798379)Time elapsed: 0.001 s
% 4.80/1.49 % (3798379)Peak memory usage: 88 MB
% 4.80/1.49 % (3798379)Instructions burned: 2 (million)
% 4.80/1.49 % (3798373)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=2053461216:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.80/1.49 % (3798374)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2663209360:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.80/1.49 % (3798375)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2487980242:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.80/1.49 % (3798378)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3254181528:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.80/1.49 % (3798377)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2350758774:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.80/1.49 % (3798376)lrs+10_1_sil=8000:sp=occurrence:random_seed=2998767175:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.80/1.49 % (3798376)Instruction limit reached!
% 4.80/1.49 % (3798376)------------------------------
% 4.80/1.49 % (3798376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798376)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798376)Termination reason: Instruction limit
% 4.80/1.49 % (3798376)Termination phase: Saturation
% 4.80/1.49 % (3798376)Time elapsed: 0.048 s
% 4.80/1.49 % (3798376)Peak memory usage: 89 MB
% 4.80/1.49 % (3798376)Instructions burned: 109 (million)
% 4.80/1.49 % (3798377)Instruction limit reached!
% 4.80/1.49 % (3798377)------------------------------
% 4.80/1.49 % (3798377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798377)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798377)Termination reason: Instruction limit
% 4.80/1.49 % (3798377)Termination phase: Saturation
% 4.80/1.49 % (3798377)Time elapsed: 0.054 s
% 4.80/1.49 % (3798377)Peak memory usage: 89 MB
% 4.80/1.49 % (3798377)Instructions burned: 115 (million)
% 4.80/1.49 % (3798378)Instruction limit reached!
% 4.80/1.49 % (3798378)------------------------------
% 4.80/1.49 % (3798378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798378)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798378)Termination reason: Instruction limit
% 4.80/1.49 % (3798378)Termination phase: Saturation
% 4.80/1.49 % (3798378)Time elapsed: 0.080 s
% 4.80/1.49 % (3798378)Peak memory usage: 89 MB
% 4.80/1.49 % (3798378)Instructions burned: 182 (million)
% 4.80/1.49 % (3798379)------------------------------
% 4.80/1.49 % (3798379)------------------------------
% 4.80/1.49 % (3798388)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3009325623: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)
% 4.80/1.49 % (3798387)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=1211049812:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.80/1.49 % (3798390)lrs+10_64_to=lpo:sil=8000:random_seed=1794412513:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.80/1.49 % (3798389)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3738284566:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.80/1.49 % (3798390)Instruction limit reached!
% 4.80/1.49 % (3798390)------------------------------
% 4.80/1.49 % (3798390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798390)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798390)Termination reason: Instruction limit
% 4.80/1.49 % (3798390)Termination phase: Saturation
% 4.80/1.49 % (3798390)Time elapsed: 0.029 s
% 4.80/1.49 % (3798390)Peak memory usage: 88 MB
% 4.80/1.49 % (3798390)Instructions burned: 129 (million)
% 4.80/1.49 % (3798387)Instruction limit reached!
% 4.80/1.49 % (3798387)------------------------------
% 4.80/1.49 % (3798387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798387)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798387)Termination reason: Instruction limit
% 4.80/1.49 % (3798387)Termination phase: Saturation
% 4.80/1.49 % (3798387)Time elapsed: 0.065 s
% 4.80/1.49 % (3798387)Peak memory usage: 89 MB
% 4.80/1.49 % (3798387)Instructions burned: 143 (million)
% 4.80/1.49 % (3798388)Instruction limit reached!
% 4.80/1.49 % (3798388)------------------------------
% 4.80/1.49 % (3798388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798388)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798388)Termination reason: Instruction limit
% 4.80/1.49 % (3798388)Termination phase: Saturation
% 4.80/1.49 % (3798388)Time elapsed: 0.082 s
% 4.80/1.49 % (3798388)Peak memory usage: 89 MB
% 4.80/1.49 % (3798388)Instructions burned: 190 (million)
% 4.80/1.49 % (3798389)Instruction limit reached!
% 4.80/1.49 % (3798389)------------------------------
% 4.80/1.49 % (3798389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798389)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798389)Termination reason: Instruction limit
% 4.80/1.49 % (3798389)Termination phase: Saturation
% 4.80/1.49 % (3798389)Time elapsed: 0.093 s
% 4.80/1.49 % (3798389)Peak memory usage: 88 MB
% 4.80/1.49 % (3798389)Instructions burned: 219 (million)
% 4.80/1.49 % (3798395)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4034190335:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 4.80/1.49 % (3798395)Instruction limit reached!
% 4.80/1.49 % (3798395)------------------------------
% 4.80/1.49 % (3798395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798395)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798395)Termination reason: Instruction limit
% 4.80/1.49 % (3798395)Termination phase: Saturation
% 4.80/1.49 % (3798395)Time elapsed: 0.048 s
% 4.80/1.49 % (3798395)Peak memory usage: 89 MB
% 4.80/1.49 % (3798395)Instructions burned: 196 (million)
% 4.80/1.49 % (3798397)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3351824602:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 4.80/1.49 % (3798396)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3839268298:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 4.80/1.49 % (3798396)First to succeed.
% 4.80/1.49 % (3798396)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3798368"
% 4.80/1.49 % (3798398)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=3053100083:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 4.80/1.49 % (3798400)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=166082709:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 4.80/1.49 % (3798400)Instruction limit reached!
% 4.80/1.49 % (3798400)------------------------------
% 4.80/1.49 % (3798400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.80/1.49 % (3798400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.49 % (3798400)CaDiCaL version: 2.1.3
% 4.80/1.49 % (3798400)Termination reason: Instruction limit
% 4.80/1.49 % (3798400)Termination phase: Saturation
% 4.80/1.49 % (3798400)Time elapsed: 0.027 s
% 4.80/1.49 % (3798400)Peak memory usage: 88 MB
% 6.42/1.69 % (3798400)Instructions burned: 111 (million)
% 6.42/1.69 % (3798398)Instruction limit reached!
% 6.42/1.69 % (3798398)------------------------------
% 6.42/1.69 % (3798398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.42/1.69 % (3798398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.69 % (3798398)CaDiCaL version: 2.1.3
% 6.42/1.69 % (3798398)Termination reason: Instruction limit
% 6.42/1.69 % (3798398)Time elapsed: 0.047 s
% 6.42/1.69 % (3798398)Peak memory usage: 89 MB
% 6.42/1.69 % (3798398)Instructions burned: 106 (million)
% 6.42/1.69 % (3798405)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3894661769:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 6.42/1.69 % (3798405)Refutation not found, incomplete strategy
% 6.42/1.69 % (3798405)------------------------------
% 6.42/1.69 % (3798405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.42/1.69 % (3798405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.69 % (3798405)CaDiCaL version: 2.1.3
% 6.42/1.69 % (3798405)Termination reason: Refutation not found, incomplete strategy
% 6.42/1.69 % (3798405)Time elapsed: 0.004 s
% 6.42/1.69 % (3798405)Peak memory usage: 88 MB
% 6.42/1.69 % (3798405)Instructions burned: 14 (million)
% 6.42/1.69 % (3798406)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2950867160:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 6.42/1.69 % (3798373)Refutation not found, incomplete strategy
% 6.42/1.69 % (3798373)------------------------------
% 6.42/1.69 % (3798373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.42/1.69 % (3798373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.69 % (3798373)CaDiCaL version: 2.1.3
% 6.42/1.69 % (3798373)Termination reason: Refutation not found, incomplete strategy
% 6.42/1.69 % (3798373)Time elapsed: 0.660 s
% 6.42/1.69 % (3798373)Peak memory usage: 128 MB
% 6.42/1.69 % (3798373)Instructions burned: 962 (million)
% 6.42/1.69 % SZS status Satisfiable for theBenchmark
% 6.42/1.69 % SZS output start Saturation.
% See solution above
% 6.42/1.69 % SZS output start Definitions and Model Updates.
% 6.42/1.69 % SZS output end Definitions and Model Updates.
% 6.42/1.69 % (3798396)------------------------------
% 6.42/1.69 % (3798396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.42/1.69 % (3798396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.42/1.69 % (3798396)CaDiCaL version: 2.1.3
% 6.42/1.69 % (3798396)Termination reason: Satisfiable
% 6.42/1.69 % (3798396)Time elapsed: 0.025 s
% 6.42/1.69 % (3798396)Peak memory usage: 89 MB
% 6.42/1.69 % (3798396)Instructions burned: 37 (million)
% 6.42/1.69 % (3798396)------------------------------
% 6.42/1.69 % (3798396)------------------------------
% 6.42/1.69 % (3798368)Success in time 0.828 s
% 6.42/1.69 % Vampire exiting
%------------------------------------------------------------------------------