%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV554-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 THM
% Computer : n008.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:18:11 PM UTC 2026
% Result : Satisfiable 26.54s 4.46s
% Output : Saturation 26.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u85,hypothesis,
i9 = i10 ).
cnf(u156,hypothesis,
i8 = i10 ).
cnf(u222,hypothesis,
i7 = i10 ).
cnf(u308,hypothesis,
i2 = i3 ).
cnf(u372,hypothesis,
i3 = i4 ).
cnf(u461,hypothesis,
i4 = i5 ).
cnf(u549,hypothesis,
i5 = i6 ).
cnf(u629,hypothesis,
i6 = i10 ).
cnf(u685,hypothesis,
i1 != i10 ).
cnf(u690,hypothesis,
select(a1,i1) = select(store(a2,i1,select(a1,i1)),i10) ).
cnf(u888,negated_conjecture,
i1 = sF0 ).
cnf(u891,negated_conjecture,
i10 != sF0 ).
cnf(u942,negated_conjecture,
( select(store(a2,sF0,sF1),X0) = select(store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),sF0,sF1),X0)
| i10 = X0 ) ).
cnf(u637,hypothesis,
i3 = i10 ).
cnf(u1069,negated_conjecture,
( select(a1,X0) = select(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u635,hypothesis,
i5 = i10 ).
cnf(u1054,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u957,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u912,negated_conjecture,
( select(a2,X0) = select(a1,X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u962,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u954,negated_conjecture,
( select(a1,X0) = select(store(store(a1,sF0,sF2),i10,sF1),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u1044,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u924,negated_conjecture,
sF1 = select(a2,i10) ).
cnf(u960,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u8,axiom,
select(a1,sF0) = sF1 ).
cnf(u10,axiom,
select(a2,sF0) = sF2 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1059,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u6,axiom,
sk(a1,a2) = sF0 ).
cnf(u939,negated_conjecture,
select(a1,i10) = select(store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),sF0,sF1),i10) ).
cnf(u929,negated_conjecture,
sF1 = select(store(a2,sF0,sF1),i10) ).
cnf(u638,hypothesis,
i2 = i10 ).
cnf(u943,negated_conjecture,
select(store(a1,sF0,sF2),i10) = select(store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),sF0,sF1),i10) ).
cnf(u961,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u944,negated_conjecture,
store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),sF0,sF1) = store(store(store(store(store(store(store(store(store(store(a2,sF0,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)) ).
cnf(u940,negated_conjecture,
( select(store(a2,sF0,sF1),X0) = select(store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),sF0,sF1),X0)
| i10 = X0 ) ).
cnf(u636,hypothesis,
i4 = i10 ).
cnf(u955,negated_conjecture,
( select(a1,X0) = select(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u1064,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u1049,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),i10,sF1),i10,select(store(a1,sF0,sF2),i10)),X0)
| i10 = X0
| sF0 = X0 ) ).
cnf(u959,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u958,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u956,negated_conjecture,
( select(a1,X0) = select(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),X0)
| sF0 = X0
| i10 = X0 ) ).
cnf(u11,negated_conjecture,
sF1 != sF2 ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u938,negated_conjecture,
store(store(store(store(store(store(store(store(store(store(a2,sF0,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)) = store(store(store(store(store(store(store(store(store(store(a1,sF0,sF2),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),i10,sF1),i10,select(a1,i10)),sF0,sF1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV554-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n008.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 11:46:09 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 9.99/2.12 % (2194666)Input is clausal, will run a generic CNF schedule.
% 9.99/2.12 % (2194677)dis-21_1_sil=8000:lcm=predicate:random_seed=2266240703: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)
% 9.99/2.12 % (2194677)Refutation not found, incomplete strategy
% 9.99/2.12 % (2194677)------------------------------
% 9.99/2.12 % (2194677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.99/2.12 % (2194677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.99/2.12 % (2194677)CaDiCaL version: 2.1.3
% 9.99/2.12 % (2194677)Termination reason: Refutation not found, incomplete strategy
% 9.99/2.12 % (2194677)Time elapsed: 0.006 s
% 9.99/2.12 % (2194677)Peak memory usage: 88 MB
% 9.99/2.12 % (2194677)Instructions burned: 25 (million)
% 9.99/2.12 % (2194674)lrs+10_1_sil=8000:sp=occurrence:random_seed=1726927579:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.99/2.12 % (2194673)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=871397967:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.99/2.12 % (2194671)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=185217130:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.99/2.12 % (2194672)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3591080466:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.99/2.12 % (2194675)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3683585512:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.99/2.12 % (2194676)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=297385950:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.99/2.12 % (2194674)Instruction limit reached!
% 9.99/2.12 % (2194674)------------------------------
% 9.99/2.12 % (2194674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.99/2.12 % (2194674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.99/2.12 % (2194674)CaDiCaL version: 2.1.3
% 9.99/2.12 % (2194674)Termination reason: Instruction limit
% 9.99/2.12 % (2194674)Termination phase: Saturation
% 9.99/2.12 % (2194674)Time elapsed: 0.041 s
% 9.99/2.12 % (2194674)Peak memory usage: 90 MB
% 9.99/2.12 % (2194674)Instructions burned: 108 (million)
% 9.99/2.12 % (2194675)Instruction limit reached!
% 9.99/2.12 % (2194675)------------------------------
% 9.99/2.12 % (2194675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.99/2.12 % (2194675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.99/2.12 % (2194675)CaDiCaL version: 2.1.3
% 9.99/2.12 % (2194675)Termination reason: Instruction limit
% 9.99/2.12 % (2194675)Termination phase: Saturation
% 9.99/2.12 % (2194675)Time elapsed: 0.042 s
% 9.99/2.12 % (2194675)Peak memory usage: 88 MB
% 9.99/2.12 % (2194675)Instructions burned: 115 (million)
% 9.99/2.12 % (2194676)Instruction limit reached!
% 9.99/2.12 % (2194676)------------------------------
% 9.99/2.12 % (2194676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.99/2.12 % (2194676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.99/2.12 % (2194676)CaDiCaL version: 2.1.3
% 9.99/2.12 % (2194676)Termination reason: Instruction limit
% 9.99/2.12 % (2194676)Termination phase: Saturation
% 9.99/2.12 % (2194676)Time elapsed: 0.069 s
% 9.99/2.12 % (2194676)Peak memory usage: 90 MB
% 9.99/2.12 % (2194676)Instructions burned: 181 (million)
% 9.99/2.12 % (2194677)------------------------------
% 9.99/2.12 % (2194677)------------------------------
% 9.99/2.12 % (2194686)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3054179836: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)
% 9.99/2.12 % (2194685)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=227570596:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.99/2.12 % (2194688)lrs+10_64_to=lpo:sil=8000:random_seed=2532605478:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 9.99/2.12 % (2194685)Instruction limit reached!
% 9.99/2.12 % (2194685)------------------------------
% 9.99/2.12 % (2194685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194685)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194685)Termination reason: Instruction limit
% 14.34/2.86 % (2194685)Termination phase: Saturation
% 14.34/2.86 % (2194685)Time elapsed: 0.055 s
% 14.34/2.86 % (2194685)Peak memory usage: 90 MB
% 14.34/2.86 % (2194685)Instructions burned: 145 (million)
% 14.34/2.86 % (2194687)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2417271963:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 14.34/2.86 % (2194686)Instruction limit reached!
% 14.34/2.86 % (2194686)------------------------------
% 14.34/2.86 % (2194686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194686)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194686)Termination reason: Instruction limit
% 14.34/2.86 % (2194686)Termination phase: Saturation
% 14.34/2.86 % (2194686)Time elapsed: 0.071 s
% 14.34/2.86 % (2194686)Peak memory usage: 91 MB
% 14.34/2.86 % (2194686)Instructions burned: 190 (million)
% 14.34/2.86 % (2194688)Instruction limit reached!
% 14.34/2.86 % (2194688)------------------------------
% 14.34/2.86 % (2194688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194688)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194688)Termination reason: Instruction limit
% 14.34/2.86 % (2194688)Termination phase: Saturation
% 14.34/2.86 % (2194688)Time elapsed: 0.027 s
% 14.34/2.86 % (2194688)Peak memory usage: 90 MB
% 14.34/2.86 % (2194688)Instructions burned: 131 (million)
% 14.34/2.86 % (2194687)Instruction limit reached!
% 14.34/2.86 % (2194687)------------------------------
% 14.34/2.86 % (2194687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194687)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194687)Termination reason: Instruction limit
% 14.34/2.86 % (2194687)Termination phase: Saturation
% 14.34/2.86 % (2194687)Time elapsed: 0.079 s
% 14.34/2.86 % (2194687)Peak memory usage: 90 MB
% 14.34/2.86 % (2194687)Instructions burned: 219 (million)
% 14.34/2.86 % (2194695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2007548115:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 14.34/2.86 % (2194693)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1714353967:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 14.34/2.86 % (2194694)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1511508765:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 14.34/2.86 % (2194693)Instruction limit reached!
% 14.34/2.86 % (2194693)------------------------------
% 14.34/2.86 % (2194693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194693)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194693)Termination reason: Instruction limit
% 14.34/2.86 % (2194693)Termination phase: Saturation
% 14.34/2.86 % (2194693)Time elapsed: 0.073 s
% 14.34/2.86 % (2194693)Peak memory usage: 89 MB
% 14.34/2.86 % (2194693)Instructions burned: 197 (million)
% 14.34/2.86 % (2194696)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=2678451664:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 14.34/2.86 % (2194694)Instruction limit reached!
% 14.34/2.86 % (2194694)------------------------------
% 14.34/2.86 % (2194694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.34/2.86 % (2194694)CaDiCaL version: 2.1.3
% 14.34/2.86 % (2194694)Termination reason: Instruction limit
% 14.34/2.86 % (2194694)Termination phase: Saturation
% 14.34/2.86 % (2194694)Time elapsed: 0.095 s
% 14.34/2.86 % (2194694)Peak memory usage: 90 MB
% 14.34/2.86 % (2194694)Instructions burned: 158 (million)
% 14.34/2.86 % (2194696)Instruction limit reached!
% 14.34/2.86 % (2194696)------------------------------
% 14.34/2.86 % (2194696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.34/2.86 % (2194696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194696)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194696)Termination reason: Instruction limit
% 26.02/4.36 % (2194696)Termination phase: Saturation
% 26.02/4.36 % (2194696)Time elapsed: 0.037 s
% 26.02/4.36 % (2194696)Peak memory usage: 87 MB
% 26.02/4.36 % (2194696)Instructions burned: 106 (million)
% 26.02/4.36 % (2194701)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2496234747:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 26.02/4.36 % (2194701)Instruction limit reached!
% 26.02/4.36 % (2194701)------------------------------
% 26.02/4.36 % (2194701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194701)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194701)Termination reason: Instruction limit
% 26.02/4.36 % (2194701)Termination phase: Saturation
% 26.02/4.36 % (2194701)Time elapsed: 0.042 s
% 26.02/4.36 % (2194701)Peak memory usage: 90 MB
% 26.02/4.36 % (2194701)Instructions burned: 109 (million)
% 26.02/4.36 % (2194703)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=516902814:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 26.02/4.36 % (2194704)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3608747665:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 26.02/4.36 % (2194703)Refutation not found, incomplete strategy
% 26.02/4.36 % (2194703)------------------------------
% 26.02/4.36 % (2194703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194703)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194703)Termination reason: Refutation not found, incomplete strategy
% 26.02/4.36 % (2194703)Time elapsed: 0.045 s
% 26.02/4.36 % (2194703)Peak memory usage: 88 MB
% 26.02/4.36 % (2194703)Instructions burned: 101 (million)
% 26.02/4.36 % (2194706)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1816846325:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 26.02/4.36 % (2194706)Instruction limit reached!
% 26.02/4.36 % (2194706)------------------------------
% 26.02/4.36 % (2194706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194706)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194706)Termination reason: Instruction limit
% 26.02/4.36 % (2194706)Termination phase: Saturation
% 26.02/4.36 % (2194706)Time elapsed: 0.051 s
% 26.02/4.36 % (2194706)Peak memory usage: 90 MB
% 26.02/4.36 % (2194706)Instructions burned: 136 (million)
% 26.02/4.36 % (2194703)------------------------------
% 26.02/4.36 % (2194703)------------------------------
% 26.02/4.36 % (2194710)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1482978826:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 26.02/4.36 % (2194711)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2146914503:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 26.02/4.36 % (2194711)Instruction limit reached!
% 26.02/4.36 % (2194711)------------------------------
% 26.02/4.36 % (2194711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194711)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194711)Termination reason: Instruction limit
% 26.02/4.36 % (2194711)Termination phase: Saturation
% 26.02/4.36 % (2194711)Time elapsed: 0.069 s
% 26.02/4.36 % (2194711)Peak memory usage: 89 MB
% 26.02/4.36 % (2194711)Instructions burned: 191 (million)
% 26.02/4.36 % (2194710)Instruction limit reached!
% 26.02/4.36 % (2194710)------------------------------
% 26.02/4.36 % (2194710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194710)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194710)Termination reason: Instruction limit
% 26.02/4.36 % (2194710)Termination phase: Saturation
% 26.02/4.36 % (2194710)Time elapsed: 0.182 s
% 26.02/4.36 % (2194710)Peak memory usage: 92 MB
% 26.02/4.36 % (2194710)Instructions burned: 503 (million)
% 26.02/4.36 % (2194695)Instruction limit reached!
% 26.02/4.36 % (2194695)------------------------------
% 26.02/4.36 % (2194695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194695)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194695)Termination reason: Instruction limit
% 26.02/4.36 % (2194695)Termination phase: Saturation
% 26.02/4.36 % (2194695)Time elapsed: 0.885 s
% 26.02/4.36 % (2194695)Peak memory usage: 149 MB
% 26.02/4.36 % (2194695)Instructions burned: 3396 (million)
% 26.02/4.36 % (2194714)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2389400131:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 26.02/4.36 % (2194715)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=929719894:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 26.02/4.36 % (2194716)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3832641264:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 26.02/4.36 % (2194715)Instruction limit reached!
% 26.02/4.36 % (2194715)------------------------------
% 26.02/4.36 % (2194715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194715)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194715)Termination reason: Instruction limit
% 26.02/4.36 % (2194715)Termination phase: Saturation
% 26.02/4.36 % (2194715)Time elapsed: 0.058 s
% 26.02/4.36 % (2194715)Peak memory usage: 91 MB
% 26.02/4.36 % (2194715)Instructions burned: 156 (million)
% 26.02/4.36 % (2194714)Instruction limit reached!
% 26.02/4.36 % (2194714)------------------------------
% 26.02/4.36 % (2194714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194714)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194714)Termination reason: Instruction limit
% 26.02/4.36 % (2194714)Termination phase: Saturation
% 26.02/4.36 % (2194714)Time elapsed: 0.102 s
% 26.02/4.36 % (2194714)Peak memory usage: 95 MB
% 26.02/4.36 % (2194714)Instructions burned: 265 (million)
% 26.02/4.36 % (2194720)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1580385572:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 26.02/4.36 % (2194721)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1127923999:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi)
% 26.02/4.36 % (2194721)Instruction limit reached!
% 26.02/4.36 % (2194721)------------------------------
% 26.02/4.36 % (2194721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194721)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194721)Termination reason: Instruction limit
% 26.02/4.36 % (2194721)Termination phase: Saturation
% 26.02/4.36 % (2194721)Time elapsed: 0.067 s
% 26.02/4.36 % (2194721)Peak memory usage: 91 MB
% 26.02/4.36 % (2194721)Instructions burned: 182 (million)
% 26.02/4.36 % (2194720)Instruction limit reached!
% 26.02/4.36 % (2194720)------------------------------
% 26.02/4.36 % (2194720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.02/4.36 % (2194720)CaDiCaL version: 2.1.3
% 26.02/4.36 % (2194720)Termination reason: Instruction limit
% 26.02/4.36 % (2194720)Termination phase: Saturation
% 26.02/4.36 % (2194720)Time elapsed: 0.218 s
% 26.02/4.36 % (2194720)Peak memory usage: 93 MB
% 26.02/4.36 % (2194720)Instructions burned: 538 (million)
% 26.02/4.36 % (2194724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2872288860:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 26.02/4.36 % (2194725)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=307045261:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi)
% 26.02/4.36 % (2194725)Refutation not found, incomplete strategy
% 26.02/4.36 % (2194725)------------------------------
% 26.02/4.36 % (2194725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.02/4.36 % (2194725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194725)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194725)Termination reason: Refutation not found, incomplete strategy
% 26.54/4.46 % (2194725)Time elapsed: 0.050 s
% 26.54/4.46 % (2194725)Peak memory usage: 90 MB
% 26.54/4.46 % (2194725)Instructions burned: 88 (million)
% 26.54/4.46 % (2194725)------------------------------
% 26.54/4.46 % (2194725)------------------------------
% 26.54/4.46 % (2194716)Instruction limit reached!
% 26.54/4.46 % (2194716)------------------------------
% 26.54/4.46 % (2194716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.54/4.46 % (2194716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194716)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194716)Termination reason: Instruction limit
% 26.54/4.46 % (2194716)Termination phase: Saturation
% 26.54/4.46 % (2194716)Time elapsed: 0.885 s
% 26.54/4.46 % (2194716)Peak memory usage: 170 MB
% 26.54/4.46 % (2194716)Instructions burned: 3261 (million)
% 26.54/4.46 % (2194728)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3669684175:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 26.54/4.46 % (2194729)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=810649835:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2975 on theBenchmark for (2975ds/303Mi)
% 26.54/4.46 % (2194729)Refutation not found, incomplete strategy
% 26.54/4.46 % (2194729)------------------------------
% 26.54/4.46 % (2194729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.54/4.46 % (2194729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194729)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194729)Termination reason: Refutation not found, incomplete strategy
% 26.54/4.46 % (2194729)Time elapsed: 0.014 s
% 26.54/4.46 % (2194729)Peak memory usage: 89 MB
% 26.54/4.46 % (2194729)Instructions burned: 61 (million)
% 26.54/4.46 % (2194729)------------------------------
% 26.54/4.46 % (2194729)------------------------------
% 26.54/4.46 % (2194732)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1261715054:st=4:i=720:sd=3:fsr=off:ss=axioms_2972 on theBenchmark for (2972ds/720Mi)
% 26.54/4.46 % (2194732)Instruction limit reached!
% 26.54/4.46 % (2194732)------------------------------
% 26.54/4.46 % (2194732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.54/4.46 % (2194732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194732)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194732)Termination reason: Instruction limit
% 26.54/4.46 % (2194732)Termination phase: Saturation
% 26.54/4.46 % (2194732)Time elapsed: 0.136 s
% 26.54/4.46 % (2194732)Peak memory usage: 92 MB
% 26.54/4.46 % (2194732)Instructions burned: 725 (million)
% 26.54/4.46 % (2194734)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1770309811:i=598:bs=on:bd=preordered:av=off:ss=axioms_2969 on theBenchmark for (2969ds/598Mi)
% 26.54/4.46 % (2194734)Instruction limit reached!
% 26.54/4.46 % (2194734)------------------------------
% 26.54/4.46 % (2194734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.54/4.46 % (2194734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194734)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194734)Termination reason: Instruction limit
% 26.54/4.46 % (2194734)Termination phase: Saturation
% 26.54/4.46 % (2194734)Time elapsed: 0.125 s
% 26.54/4.46 % (2194734)Peak memory usage: 106 MB
% 26.54/4.46 % (2194734)Instructions burned: 602 (million)
% 26.54/4.46 % (2194736)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2158303169:i=2989:sd=3:ss=axioms:sgt=60_2967 on theBenchmark for (2967ds/2989Mi)
% 26.54/4.46 % (2194724)First to succeed.
% 26.54/4.46 % (2194724)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2194666"
% 26.54/4.46 % SZS status Satisfiable for theBenchmark
% 26.54/4.46 % SZS output start Saturation.
% See solution above
% 26.54/4.46 % SZS output start Definitions and Model Updates.
% 26.54/4.46 % SZS output end Definitions and Model Updates.
% 26.54/4.46 % (2194724)------------------------------
% 26.54/4.46 % (2194724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.54/4.46 % (2194724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.54/4.46 % (2194724)CaDiCaL version: 2.1.3
% 26.54/4.46 % (2194724)Termination reason: Satisfiable
% 26.54/4.46 % (2194724)Time elapsed: 1.391 s
% 26.54/4.46 % (2194724)Peak memory usage: 150 MB
% 26.54/4.46 % (2194724)Instructions burned: 2850 (million)
% 26.54/4.46 % (2194724)------------------------------
% 26.54/4.46 % (2194724)------------------------------
% 26.54/4.46 % (2194666)Success in time 3.701 s
% 26.54/4.46 % Vampire exiting
%------------------------------------------------------------------------------