%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO455+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 09:52:42 AM UTC 2026
% Result : Theorem 50.47s 14.63s
% Output : Refutation 93.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 24 ( 24 unt; 0 def)
% Number of atoms : 24 ( 23 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 16 con; 0-2 aty)
% Number of variables : 31 ( 29 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2406,axiom,
s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))) = s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aDIMINDEXu_1) ).
fof(f2756,axiom,
! [X0,X1,X2,X3] : s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(num,X3))) = s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),X1))),s(num,X3))))),s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),X2))),s(num,X3))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aVECTORu_SUBu_COMPONENT) ).
fof(f3206,axiom,
! [X0] : s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))) = s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),X0))),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',adrop) ).
fof(f3208,axiom,
! [X0] : s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))) = s(cart(real,n10),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aLIFTu_DROPu_conjunct0) ).
fof(f3209,axiom,
! [X0] : s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))) = s(real,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aLIFTu_DROPu_conjunct1) ).
fof(f3234,conjecture,
! [X0,X1] : s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,X0))),s(real,X1))))) = s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aLIFTu_SUB) ).
fof(f3235,negated_conjecture,
~ ! [X0,X1] : s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,X0))),s(real,X1))))) = s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X1))))),
inference(negated_conjecture,[status(cth)],[f3234]) ).
fof(f4103,plain,
? [X0,X1] : s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,X0))),s(real,X1))))) != s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X1))))),
inference(ennf_transformation,[],[f3235]) ).
fof(f6077,plain,
s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,sK576))),s(real,sK577))))) != s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,sK576))))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,sK577))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK576,sK577]),skolemize(X0,sK576),skolemize(X1,sK577)],[f4103]) ).
fof(f8485,plain,
! [X2,X3,X0,X1] : s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(cart(real,X0),fun(cart(real,X0),cart(real,X0))),vectoru_sub),s(cart(real,X0),X1))),s(cart(real,X0),X2))))),s(num,X3))) = s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),X1))),s(num,X3))))),s(real,i(s(fun(num,real),i(s(fun(cart(real,X0),fun(num,real)),d_),s(cart(real,X0),X2))),s(num,X3))))),
inference(cnf_transformation,[],[f2756]) ).
fof(f9211,plain,
! [X0] : s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),X0))),s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))))) = s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))),
inference(cnf_transformation,[],[f3206]) ).
fof(f9213,plain,
! [X0] : s(cart(real,n10),X0) = s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))),
inference(cnf_transformation,[],[f3208]) ).
fof(f9214,plain,
! [X0] : s(real,X0) = s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))),
inference(cnf_transformation,[],[f3209]) ).
fof(f9253,plain,
s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,sK576))),s(real,sK577))))) != s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,sK576))))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,sK577))))),
inference(cnf_transformation,[],[f6077]) ).
fof(f10172,plain,
s(num,i(s(fun(num,num),numeral),s(num,i(s(fun(num,num),bit1),s(num,u_0))))) = s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))),
inference(cnf_transformation,[],[f2406]) ).
fof(f15970,plain,
! [X0] : s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))) = s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),X0))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))),
inference(forward_demodulation,[],[f9211,f10172]) ).
fof(f18249,plain,
! [X0,X1] : s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),X1))),s(cart(real,n10),X0))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))) = s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),X1))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))))),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))),
inference(superposition,[],[f8485,f15970]) ).
fof(f18262,plain,
! [X0,X1] : s(real,i(s(fun(num,real),i(s(fun(cart(real,n10),fun(num,real)),d_),s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),X1))),s(cart(real,n10),X0))))),s(num,i(s(fun(fun(n10,bool),num),dimindex),s(fun(n10,bool),univ))))) = s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X1))))),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))),
inference(forward_demodulation,[],[f18249,f15970]) ).
fof(f18266,plain,
! [X0,X1] : s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X1))))),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))) = s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),X1))),s(cart(real,n10),X0))))),
inference(forward_demodulation,[],[f18262,f15970]) ).
fof(f18283,plain,
! [X0,X1] : s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),X0))),s(cart(real,n10),X1))) = s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X0))))),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X1))))))),
inference(superposition,[],[f9213,f18266]) ).
fof(f18306,plain,
! [X0,X1] : s(cart(real,n10),i(s(fun(cart(real,n10),cart(real,n10)),i(s(fun(cart(real,n10),fun(cart(real,n10),cart(real,n10))),vectoru_sub),s(cart(real,n10),X1))),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,X0))))) = s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),X1))))),s(real,X0))))),
inference(superposition,[],[f18283,f9214]) ).
fof(f18357,plain,
s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,sK576))),s(real,sK577))))) != s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,i(s(fun(cart(real,n10),real),drop),s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,sK576))))))),s(real,sK577))))),
inference(superposition,[],[f9253,f18306]) ).
fof(f18385,plain,
s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,sK576))),s(real,sK577))))) != s(cart(real,n10),i(s(fun(real,cart(real,n10)),lift),s(real,i(s(fun(real,real),i(s(fun(real,fun(real,real)),realu_sub),s(real,sK576))),s(real,sK577))))),
inference(forward_demodulation,[],[f18357,f9214]) ).
fof(f18386,plain,
$false,
inference(trivial_inequality_removal,[],[f18385]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO455+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 % Computer : n017.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 08:10:05 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.45 Running first-order theorem proving
% 0.14/0.45 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
% 15.76/3.93 % (2232896)Detected formulas, will run a generic FOF schedule.
% 15.76/3.93 % (2232906)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1110157573:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 15.76/3.93 % (2232908)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3790340999:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 15.76/3.93 % (2232909)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4246931768:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 15.76/3.93 % (2232910)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1690919050:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 15.76/3.93 % (2232911)dis-21_1_sil=8000:lcm=predicate:random_seed=71181652:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 15.76/3.93 % (2232907)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2518997675:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 15.76/3.93 % (2232905)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=984993722:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 15.76/3.93 % (2232908)Instruction limit reached!
% 15.76/3.93 % (2232908)------------------------------
% 15.76/3.93 % (2232908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/3.93 % (2232908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/3.93 % (2232908)CaDiCaL version: 2.1.3
% 15.76/3.93 % (2232908)Termination reason: Instruction limit
% 15.76/3.93 % (2232908)Termination phase: Blocked clause elimination
% 15.76/3.93 % (2232908)Time elapsed: 0.088 s
% 15.76/3.93 % (2232908)Peak memory usage: 92 MB
% 15.76/3.93 % (2232908)Instructions burned: 110 (million)
% 15.76/3.93 % (2232909)Instruction limit reached!
% 15.76/3.93 % (2232909)------------------------------
% 15.76/3.93 % (2232909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/3.93 % (2232909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/3.93 % (2232909)CaDiCaL version: 2.1.3
% 15.76/3.93 % (2232909)Termination reason: Instruction limit
% 15.76/3.93 % (2232909)Termination phase: Preprocessing 2
% 15.76/3.93 % (2232909)Time elapsed: 0.100 s
% 15.76/3.93 % (2232909)Peak memory usage: 91 MB
% 15.76/3.93 % (2232909)Instructions burned: 119 (million)
% 15.76/3.93 % (2232911)Instruction limit reached!
% 15.76/3.93 % (2232911)------------------------------
% 15.76/3.93 % (2232911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/3.93 % (2232911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/3.93 % (2232911)CaDiCaL version: 2.1.3
% 15.76/3.93 % (2232911)Termination reason: Instruction limit
% 15.76/3.93 % (2232911)Termination phase: SInE selection
% 15.76/3.93 % (2232911)Time elapsed: 0.100 s
% 15.76/3.93 % (2232911)Peak memory usage: 89 MB
% 15.76/3.93 % (2232911)Instructions burned: 130 (million)
% 15.76/3.93 % (2232910)Instruction limit reached!
% 15.76/3.93 % (2232910)------------------------------
% 15.76/3.93 % (2232910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/3.93 % (2232910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/3.93 % (2232910)CaDiCaL version: 2.1.3
% 15.76/3.93 % (2232910)Termination reason: Instruction limit
% 15.76/3.93 % (2232910)Termination phase: Property scanning
% 15.76/3.93 % (2232910)Time elapsed: 0.104 s
% 15.76/3.93 % (2232910)Peak memory usage: 90 MB
% 15.76/3.93 % (2232910)Instructions burned: 139 (million)
% 15.76/3.93 % (2232921)lrs+1011_1_sil=32000:sp=occurrence:random_seed=606444930:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.76/3.93 % (2232919)lrs+10_1_sil=8000:sp=occurrence:random_seed=2117377681:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 15.76/3.93 % (2232922)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3505307522:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 15.76/3.93 % (2232920)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2512541897:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 15.76/3.93 % (2232921)Instruction limit reached!
% 27.00/5.40 % (2232921)------------------------------
% 27.00/5.40 % (2232921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232921)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232921)Termination reason: Instruction limit
% 27.00/5.40 % (2232921)Termination phase: Saturation
% 27.00/5.40 % (2232921)Time elapsed: 0.146 s
% 27.00/5.40 % (2232921)Peak memory usage: 96 MB
% 27.00/5.40 % (2232921)Instructions burned: 327 (million)
% 27.00/5.40 % (2232920)Instruction limit reached!
% 27.00/5.40 % (2232920)------------------------------
% 27.00/5.40 % (2232920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232920)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232920)Termination reason: Instruction limit
% 27.00/5.40 % (2232920)Termination phase: Property scanning
% 27.00/5.40 % (2232920)Time elapsed: 0.117 s
% 27.00/5.40 % (2232920)Peak memory usage: 90 MB
% 27.00/5.40 % (2232920)Instructions burned: 157 (million)
% 27.00/5.40 % (2232922)Instruction limit reached!
% 27.00/5.40 % (2232922)------------------------------
% 27.00/5.40 % (2232922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232922)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232922)Termination reason: Instruction limit
% 27.00/5.40 % (2232922)Termination phase: Property scanning
% 27.00/5.40 % (2232922)Time elapsed: 0.185 s
% 27.00/5.40 % (2232922)Peak memory usage: 90 MB
% 27.00/5.40 % (2232922)Instructions burned: 249 (million)
% 27.00/5.40 % (2232919)Instruction limit reached!
% 27.00/5.40 % (2232919)------------------------------
% 27.00/5.40 % (2232919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232919)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232919)Termination reason: Instruction limit
% 27.00/5.40 % (2232919)Termination phase: Property scanning
% 27.00/5.40 % (2232919)Time elapsed: 0.235 s
% 27.00/5.40 % (2232919)Peak memory usage: 96 MB
% 27.00/5.40 % (2232919)Instructions burned: 285 (million)
% 27.00/5.40 % (2232927)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3703631061:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2987 on theBenchmark for (2987ds/294Mi)
% 27.00/5.40 % (2232928)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3743454945:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 27.00/5.40 % (2232929)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=621517391:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 27.00/5.40 % (2232930)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2949258920:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 27.00/5.40 % (2232927)Instruction limit reached!
% 27.00/5.40 % (2232927)------------------------------
% 27.00/5.40 % (2232927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232927)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232927)Termination reason: Instruction limit
% 27.00/5.40 % (2232927)Termination phase: Preprocessing 3
% 27.00/5.40 % (2232927)Time elapsed: 0.241 s
% 27.00/5.40 % (2232927)Peak memory usage: 95 MB
% 27.00/5.40 % (2232927)Instructions burned: 295 (million)
% 27.00/5.40 % (2232929)Instruction limit reached!
% 27.00/5.40 % (2232929)------------------------------
% 27.00/5.40 % (2232929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232929)CaDiCaL version: 2.1.3
% 27.00/5.40 % (2232929)Termination reason: Instruction limit
% 27.00/5.40 % (2232929)Termination phase: Preprocessing 1
% 27.00/5.40 % (2232929)Time elapsed: 0.096 s
% 27.00/5.40 % (2232929)Peak memory usage: 90 MB
% 27.00/5.40 % (2232929)Instructions burned: 113 (million)
% 27.00/5.40 % (2232930)Instruction limit reached!
% 27.00/5.40 % (2232930)------------------------------
% 27.00/5.40 % (2232930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.00/5.40 % (2232930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.00/5.40 % (2232930)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232930)Termination reason: Instruction limit
% 68.96/11.23 % (2232930)Termination phase: Naming
% 68.96/11.23 % (2232930)Time elapsed: 0.111 s
% 68.96/11.23 % (2232930)Peak memory usage: 93 MB
% 68.96/11.23 % (2232930)Instructions burned: 128 (million)
% 68.96/11.23 % (2232935)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1862900019:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 68.96/11.23 % (2232936)lrs+10_1_sil=8000:sp=occurrence:random_seed=1769693232:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 68.96/11.23 % (2232937)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=995120752:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 68.96/11.23 % (2232935)Instruction limit reached!
% 68.96/11.23 % (2232935)------------------------------
% 68.96/11.23 % (2232935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232935)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232935)Termination reason: Instruction limit
% 68.96/11.23 % (2232935)Termination phase: Property scanning
% 68.96/11.23 % (2232935)Time elapsed: 0.084 s
% 68.96/11.23 % (2232935)Peak memory usage: 90 MB
% 68.96/11.23 % (2232935)Instructions burned: 114 (million)
% 68.96/11.23 % (2232941)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4051188390:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 68.96/11.23 % (2232928)Instruction limit reached!
% 68.96/11.23 % (2232928)------------------------------
% 68.96/11.23 % (2232928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232928)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232928)Termination reason: Instruction limit
% 68.96/11.23 % (2232928)Termination phase: Twee Goal Transformation
% 68.96/11.23 % (2232928)Time elapsed: 0.887 s
% 68.96/11.23 % (2232928)Peak memory usage: 105 MB
% 68.96/11.23 % (2232928)Instructions burned: 2351 (million)
% 68.96/11.23 % (2232937)Instruction limit reached!
% 68.96/11.23 % (2232937)------------------------------
% 68.96/11.23 % (2232937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232937)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232937)Termination reason: Instruction limit
% 68.96/11.23 % (2232937)Termination phase: Property scanning
% 68.96/11.23 % (2232937)Time elapsed: 0.356 s
% 68.96/11.23 % (2232937)Peak memory usage: 98 MB
% 68.96/11.23 % (2232937)Instructions burned: 437 (million)
% 68.96/11.23 % (2232944)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2814757946:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 68.96/11.23 % (2232943)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=87746253:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 68.96/11.23 % (2232936)Instruction limit reached!
% 68.96/11.23 % (2232936)------------------------------
% 68.96/11.23 % (2232936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232936)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232936)Termination reason: Instruction limit
% 68.96/11.23 % (2232936)Termination phase: Saturation
% 68.96/11.23 % (2232936)Time elapsed: 0.701 s
% 68.96/11.23 % (2232936)Peak memory usage: 102 MB
% 68.96/11.23 % (2232936)Instructions burned: 907 (million)
% 68.96/11.23 % (2232943)Instruction limit reached!
% 68.96/11.23 % (2232943)------------------------------
% 68.96/11.23 % (2232943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232943)CaDiCaL version: 2.1.3
% 68.96/11.23 % (2232943)Termination reason: Instruction limit
% 68.96/11.23 % (2232943)Termination phase: Preprocessing 1
% 68.96/11.23 % (2232943)Time elapsed: 0.111 s
% 68.96/11.23 % (2232943)Peak memory usage: 91 MB
% 68.96/11.23 % (2232943)Instructions burned: 134 (million)
% 68.96/11.23 % (2232944)Instruction limit reached!
% 68.96/11.23 % (2232944)------------------------------
% 68.96/11.23 % (2232944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.23 % (2232944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.23 % (2232944)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232944)Termination reason: Instruction limit
% 50.47/14.63 % (2232944)Termination phase: Preprocessing 3
% 50.47/14.63 % (2232944)Time elapsed: 0.261 s
% 50.47/14.63 % (2232944)Peak memory usage: 102 MB
% 50.47/14.63 % (2232944)Instructions burned: 592 (million)
% 50.47/14.63 % (2232947)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1225607103:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 50.47/14.63 % (2232948)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2305820764:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 50.47/14.63 % (2232948)Instruction limit reached!
% 50.47/14.63 % (2232948)------------------------------
% 50.47/14.63 % (2232948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232948)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232948)Termination reason: Instruction limit
% 50.47/14.63 % (2232948)Termination phase: Property scanning
% 50.47/14.63 % (2232948)Time elapsed: 0.097 s
% 50.47/14.63 % (2232948)Peak memory usage: 90 MB
% 50.47/14.63 % (2232948)Instructions burned: 125 (million)
% 50.47/14.63 % (2232950)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1854397027:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 50.47/14.63 % (2232950)Instruction limit reached!
% 50.47/14.63 % (2232950)------------------------------
% 50.47/14.63 % (2232950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232950)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232950)Termination reason: Instruction limit
% 50.47/14.63 % (2232950)Termination phase: Property scanning
% 50.47/14.63 % (2232950)Time elapsed: 0.101 s
% 50.47/14.63 % (2232950)Peak memory usage: 90 MB
% 50.47/14.63 % (2232950)Instructions burned: 135 (million)
% 50.47/14.63 % (2232952)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2870823413:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 50.47/14.63 % (2232952)Refutation not found, incomplete strategy
% 50.47/14.63 % (2232952)------------------------------
% 50.47/14.63 % (2232952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232952)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232952)Termination reason: Refutation not found, incomplete strategy
% 50.47/14.63 % (2232952)Time elapsed: 0.095 s
% 50.47/14.63 % (2232952)Peak memory usage: 94 MB
% 50.47/14.63 % (2232952)Instructions burned: 111 (million)
% 50.47/14.63 % (2232954)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=210554230:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 50.47/14.63 % (2232954)Instruction limit reached!
% 50.47/14.63 % (2232954)------------------------------
% 50.47/14.63 % (2232954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232954)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232954)Termination reason: Instruction limit
% 50.47/14.63 % (2232954)Termination phase: Saturation
% 50.47/14.63 % (2232954)Time elapsed: 0.357 s
% 50.47/14.63 % (2232954)Peak memory usage: 95 MB
% 50.47/14.63 % (2232954)Instructions burned: 432 (million)
% 50.47/14.63 % (2232952)------------------------------
% 50.47/14.63 % (2232952)------------------------------
% 50.47/14.63 % (2232957)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2991445620:i=6060:aac=none:ins=25_2961 on theBenchmark for (2961ds/6060Mi)
% 50.47/14.63 % (2232958)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=682718162:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2961 on theBenchmark for (2961ds/150Mi)
% 50.47/14.63 % (2232958)Instruction limit reached!
% 50.47/14.63 % (2232958)------------------------------
% 50.47/14.63 % (2232958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232958)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232958)Termination reason: Instruction limit
% 50.47/14.63 % (2232958)Termination phase: Preprocessing 1
% 50.47/14.63 % (2232958)Time elapsed: 0.133 s
% 50.47/14.63 % (2232958)Peak memory usage: 91 MB
% 50.47/14.63 % (2232958)Instructions burned: 151 (million)
% 50.47/14.63 % (2232961)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4097468444:i=14155:bd=all_2956 on theBenchmark for (2956ds/14155Mi)
% 50.47/14.63 % (2232941)Instruction limit reached!
% 50.47/14.63 % (2232941)------------------------------
% 50.47/14.63 % (2232941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232941)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232941)Termination reason: Instruction limit
% 50.47/14.63 % (2232941)Termination phase: Saturation
% 50.47/14.63 % (2232941)Time elapsed: 4.899 s
% 50.47/14.63 % (2232941)Peak memory usage: 227 MB
% 50.47/14.63 % (2232941)Instructions burned: 5202 (million)
% 50.47/14.63 % (2232965)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1367441950:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 50.47/14.63 % (2232965)Instruction limit reached!
% 50.47/14.63 % (2232965)------------------------------
% 50.47/14.63 % (2232965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232965)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232965)Termination reason: Instruction limit
% 50.47/14.63 % (2232965)Termination phase: Property scanning
% 50.47/14.63 % (2232965)Time elapsed: 0.540 s
% 50.47/14.63 % (2232965)Peak memory usage: 102 MB
% 50.47/14.63 % (2232965)Instructions burned: 667 (million)
% 50.47/14.63 % (2232967)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=413370753:s2a=on:i=185:s2at=1.8:fdi=4_2918 on theBenchmark for (2918ds/185Mi)
% 50.47/14.63 % (2232967)Instruction limit reached!
% 50.47/14.63 % (2232967)------------------------------
% 50.47/14.63 % (2232967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232967)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232967)Termination reason: Instruction limit
% 50.47/14.63 % (2232967)Termination phase: Preprocessing 1
% 50.47/14.63 % (2232967)Time elapsed: 0.158 s
% 50.47/14.63 % (2232967)Peak memory usage: 91 MB
% 50.47/14.63 % (2232967)Instructions burned: 185 (million)
% 50.47/14.63 % (2232969)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1787830991:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/193Mi)
% 50.47/14.63 % (2232969)Instruction limit reached!
% 50.47/14.63 % (2232969)------------------------------
% 50.47/14.63 % (2232969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232969)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232969)Termination reason: Instruction limit
% 50.47/14.63 % (2232969)Termination phase: Preprocessing 1
% 50.47/14.63 % (2232969)Time elapsed: 0.169 s
% 50.47/14.63 % (2232969)Peak memory usage: 90 MB
% 50.47/14.63 % (2232969)Instructions burned: 193 (million)
% 50.47/14.63 % (2232971)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4088441886:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2909 on theBenchmark for (2909ds/4850Mi)
% 50.47/14.63 % (2232947)Instruction limit reached!
% 50.47/14.63 % (2232947)------------------------------
% 50.47/14.63 % (2232947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232947)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232947)Termination reason: Instruction limit
% 50.47/14.63 % (2232947)Termination phase: Saturation
% 50.47/14.63 % (2232947)Time elapsed: 6.678 s
% 50.47/14.63 % (2232947)Peak memory usage: 331 MB
% 50.47/14.63 % (2232947)Instructions burned: 13195 (million)
% 50.47/14.63 % (2232973)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2892957571:i=12111:sd=1:ss=included_2904 on theBenchmark for (2904ds/12111Mi)
% 50.47/14.63 % (2232957)Instruction limit reached!
% 50.47/14.63 % (2232957)------------------------------
% 50.47/14.63 % (2232957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232957)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232957)Termination reason: Instruction limit
% 50.47/14.63 % (2232957)Termination phase: Saturation
% 50.47/14.63 % (2232957)Time elapsed: 6.042 s
% 50.47/14.63 % (2232957)Peak memory usage: 408 MB
% 50.47/14.63 % (2232957)Instructions burned: 6062 (million)
% 50.47/14.63 % (2232975)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3007692863:i=319:kws=precedence:fsr=off_2897 on theBenchmark for (2897ds/319Mi)
% 50.47/14.63 % (2232975)Instruction limit reached!
% 50.47/14.63 % (2232975)------------------------------
% 50.47/14.63 % (2232975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232975)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232975)Termination reason: Instruction limit
% 50.47/14.63 % (2232975)Termination phase: Preprocessing 3
% 50.47/14.63 % (2232975)Time elapsed: 0.271 s
% 50.47/14.63 % (2232975)Peak memory usage: 99 MB
% 50.47/14.63 % (2232975)Instructions burned: 319 (million)
% 50.47/14.63 % (2232971)Refutation not found, incomplete strategy
% 50.47/14.63 % (2232971)------------------------------
% 50.47/14.63 % (2232971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232971)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232971)Termination reason: Refutation not found, incomplete strategy
% 50.47/14.63 % (2232971)Time elapsed: 1.694 s
% 50.47/14.63 % (2232971)Peak memory usage: 121 MB
% 50.47/14.63 % (2232971)Instructions burned: 2164 (million)
% 50.47/14.63 % (2232977)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3871453020:i=2064:ep=RST_2892 on theBenchmark for (2892ds/2064Mi)
% 50.47/14.63 % (2232971)------------------------------
% 50.47/14.63 % (2232971)------------------------------
% 50.47/14.63 % (2232979)dis-1011_128_sil=32000:random_seed=1221945829:i=3706:ep=RST:av=off_2886 on theBenchmark for (2886ds/3706Mi)
% 50.47/14.63 % (2232977)Instruction limit reached!
% 50.47/14.63 % (2232977)------------------------------
% 50.47/14.63 % (2232977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.47/14.63 % (2232977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.47/14.63 % (2232977)CaDiCaL version: 2.1.3
% 50.47/14.63 % (2232977)Termination reason: Instruction limit
% 50.47/14.63 % (2232977)Termination phase: Property scanning
% 50.47/14.63 % (2232977)Time elapsed: 1.516 s
% 50.47/14.63 % (2232977)Peak memory usage: 106 MB
% 50.47/14.63 % (2232977)Instructions burned: 2064 (million)
% 50.47/14.63 % (2232981)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1468598650:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2873 on theBenchmark for (2873ds/757Mi)
% 50.47/14.63 % (2232906)First to succeed.
% 50.47/14.63 % (2232906)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2232896"
% 50.47/14.63 % (2232906)Refutation found. Thanks to Tanya!
% 50.47/14.63 % SZS status Theorem for theBenchmark
% 50.47/14.63 % SZS output start Proof for theBenchmark
% See solution above
% 93.27/14.84 % (2232906)------------------------------
% 93.27/14.84 % (2232906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.27/14.84 % (2232906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.27/14.84 % (2232906)CaDiCaL version: 2.1.3
% 93.27/14.84 % (2232906)Termination reason: Refutation
% 93.27/14.84 % (2232906)Time elapsed: 12.201 s
% 93.27/14.84 % (2232906)Peak memory usage: 382 MB
% 93.27/14.84 % (2232906)Instructions burned: 13687 (million)
% 93.27/14.84 % (2232906)------------------------------
% 93.27/14.84 % (2232906)------------------------------
% 93.27/14.84 % (2232896)Success in time 13.568 s
% 93.27/14.84 % Vampire exiting
%------------------------------------------------------------------------------