%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP004+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 11:27:45 AM UTC 2026
% Result : Theorem 0.16s 3.40s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 5
% Syntax : Number of formulae : 27 ( 6 unt; 0 def)
% Number of atoms : 68 ( 5 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 72 ( 31 ~; 25 |; 4 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 39 ( 37 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_tp) ).
fof(f2230,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epred__set_2ECHOICE) ).
fof(f2430,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,X0)
=> ! [X2] :
( mem(X2,arr(X0,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X2),X1)),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EDELETE__SUBSET) ).
fof(f2442,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_thm_2Epred__set_2EREST__DEF) ).
fof(f2447,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EREST__SUBSET) ).
fof(f2448,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,arr(X0,bool))
=> p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1)) ) ),
inference(negated_conjecture,[status(cth)],[f2447]) ).
fof(f2522,plain,
! [X0] :
( mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2230]) ).
fof(f2739,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X2),X1)),X2))
| ~ mem(X2,arr(X0,bool)) )
| ~ mem(X1,X0) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2430]) ).
fof(f2753,plain,
! [X0] :
( ! [X1] :
( ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1))
| ~ mem(X1,arr(X0,bool)) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2442]) ).
fof(f2759,plain,
? [X0] :
( ? [X1] :
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(c_2Epred__set_2EREST(X0),X1)),X1))
& mem(X1,arr(X0,bool)) )
& ne(X0) ),
inference(ennf_transformation,[],[f2448]) ).
fof(f2965,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f4135,plain,
( ~ p(ap(ap(c_2Epred__set_2ESUBSET(sK74),ap(c_2Epred__set_2EREST(sK74),sK75)),sK75))
& mem(sK75,arr(sK74,bool))
& ne(sK74) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74,sK75]),skolemize(X0,sK74),skolemize(X1,sK75)],[f2759]) ).
fof(f4985,plain,
! [X0] :
( mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f2522]) ).
fof(f5358,plain,
! [X2,X0,X1] :
( p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X2),X1)),X2))
| ~ mem(X2,arr(X0,bool))
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f2739]) ).
fof(f5381,plain,
! [X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| ap(c_2Epred__set_2EREST(X0),X1) = ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)) ),
inference(cnf_transformation,[],[f2753]) ).
fof(f5390,plain,
ne(sK74),
inference(cnf_transformation,[],[f4135]) ).
fof(f5391,plain,
mem(sK75,arr(sK74,bool)),
inference(cnf_transformation,[],[f4135]) ).
fof(f5392,plain,
~ p(ap(ap(c_2Epred__set_2ESUBSET(sK74),ap(c_2Epred__set_2EREST(sK74),sK75)),sK75)),
inference(cnf_transformation,[],[f4135]) ).
fof(f6251,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f2965]) ).
fof(f9133,plain,
! [X0] :
( ~ mem(X0,arr(sK74,bool))
| ap(c_2Epred__set_2EREST(sK74),X0) = ap(ap(c_2Epred__set_2EDELETE(sK74),X0),ap(c_2Epred__set_2ECHOICE(sK74),X0)) ),
inference(resolution,[],[f5381,f5390]) ).
fof(f9134,plain,
ap(c_2Epred__set_2EREST(sK74),sK75) = ap(ap(c_2Epred__set_2EDELETE(sK74),sK75),ap(c_2Epred__set_2ECHOICE(sK74),sK75)),
inference(resolution,[],[f9133,f5391]) ).
fof(f9135,plain,
( p(ap(ap(c_2Epred__set_2ESUBSET(sK74),ap(c_2Epred__set_2EREST(sK74),sK75)),sK75))
| ~ mem(sK75,arr(sK74,bool))
| ~ mem(ap(c_2Epred__set_2ECHOICE(sK74),sK75),sK74)
| ~ ne(sK74) ),
inference(superposition,[],[f5358,f9134]) ).
fof(f9136,plain,
! [X0,X1] :
( ~ ne(X0)
| ~ mem(X1,arr(X0,bool))
| mem(ap(c_2Epred__set_2ECHOICE(X0),X1),X0) ),
inference(resolution,[],[f4985,f6251]) ).
fof(f9148,plain,
( p(ap(ap(c_2Epred__set_2ESUBSET(sK74),ap(c_2Epred__set_2EREST(sK74),sK75)),sK75))
| ~ mem(sK75,arr(sK74,bool))
| ~ ne(sK74) ),
inference(forward_subsumption_resolution,[],[f9135,f9136]) ).
fof(f9149,plain,
( ~ mem(sK75,arr(sK74,bool))
| ~ ne(sK74) ),
inference(forward_subsumption_resolution,[],[f9148,f5392]) ).
fof(f9150,plain,
~ ne(sK74),
inference(forward_subsumption_resolution,[],[f9149,f5391]) ).
fof(f9151,plain,
$false,
inference(forward_subsumption_resolution,[],[f9150,f5390]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP004+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 % Computer : n005.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 27 11:50:18 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.46 Running first-order theorem proving
% 0.14/0.46 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
% 10.45/2.56 % (3854056)Detected formulas, will run a generic FOF schedule.
% 10.45/2.56 % (3854066)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1210996305:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.45/2.56 % (3854062)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=3326215687:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.45/2.56 % (3854061)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=756311004:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.45/2.56 % (3854063)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=3793590877:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.45/2.56 % (3854066)Instruction limit reached!
% 10.45/2.56 % (3854066)------------------------------
% 10.45/2.56 % (3854066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.56 % (3854066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.56 % (3854066)CaDiCaL version: 2.1.3
% 10.45/2.56 % (3854066)Termination reason: Instruction limit
% 10.45/2.56 % (3854066)Termination phase: Preprocessing 3
% 10.45/2.56 % (3854066)Time elapsed: 0.048 s
% 10.45/2.56 % (3854066)Peak memory usage: 92 MB
% 10.45/2.56 % (3854066)Instructions burned: 142 (million)
% 10.45/2.56 % (3854065)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1850853793:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.45/2.56 % (3854064)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=639104515:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.45/2.56 % (3854067)dis-21_1_sil=8000:lcm=predicate:random_seed=1015636361:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.45/2.56 % (3854064)Instruction limit reached!
% 10.45/2.56 % (3854064)------------------------------
% 10.45/2.56 % (3854064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.56 % (3854064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.56 % (3854064)CaDiCaL version: 2.1.3
% 10.45/2.56 % (3854064)Termination reason: Instruction limit
% 10.45/2.56 % (3854064)Termination phase: Saturation
% 10.45/2.56 % (3854064)Time elapsed: 0.058 s
% 10.45/2.56 % (3854064)Peak memory usage: 93 MB
% 10.45/2.56 % (3854064)Instructions burned: 111 (million)
% 10.45/2.56 % (3854065)Instruction limit reached!
% 10.45/2.56 % (3854065)------------------------------
% 10.45/2.56 % (3854065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.56 % (3854065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.56 % (3854065)CaDiCaL version: 2.1.3
% 10.45/2.56 % (3854065)Termination reason: Instruction limit
% 10.45/2.56 % (3854065)Termination phase: Saturation
% 10.45/2.56 % (3854065)Time elapsed: 0.063 s
% 10.45/2.56 % (3854065)Peak memory usage: 93 MB
% 10.45/2.56 % (3854065)Instructions burned: 119 (million)
% 10.45/2.56 % (3854067)Instruction limit reached!
% 10.45/2.56 % (3854067)------------------------------
% 10.45/2.56 % (3854067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.56 % (3854067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.56 % (3854067)CaDiCaL version: 2.1.3
% 10.45/2.56 % (3854067)Termination reason: Instruction limit
% 10.45/2.56 % (3854067)Termination phase: Property scanning
% 10.45/2.56 % (3854067)Time elapsed: 0.082 s
% 10.45/2.56 % (3854067)Peak memory usage: 94 MB
% 10.45/2.56 % (3854067)Instructions burned: 131 (million)
% 10.45/2.56 % (3854074)lrs+10_1_sil=8000:sp=occurrence:random_seed=2123167218:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.45/2.56 % (3854076)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3718681097:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.45/2.56 % (3854074)Instruction limit reached!
% 10.45/2.56 % (3854074)------------------------------
% 10.45/2.56 % (3854074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.56 % (3854074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.56 % (3854074)CaDiCaL version: 2.1.3
% 10.45/2.56 % (3854074)Termination reason: Instruction limit
% 15.02/3.18 % (3854074)Termination phase: Saturation
% 15.02/3.18 % (3854074)Time elapsed: 0.091 s
% 15.02/3.18 % (3854074)Peak memory usage: 96 MB
% 15.02/3.18 % (3854074)Instructions burned: 285 (million)
% 15.02/3.18 % (3854077)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4077733002:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 15.02/3.18 % (3854078)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=3841658335:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 15.02/3.18 % (3854076)Instruction limit reached!
% 15.02/3.18 % (3854076)------------------------------
% 15.02/3.18 % (3854076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.18 % (3854076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.18 % (3854076)CaDiCaL version: 2.1.3
% 15.02/3.18 % (3854076)Termination reason: Instruction limit
% 15.02/3.18 % (3854076)Termination phase: Saturation
% 15.02/3.18 % (3854076)Time elapsed: 0.080 s
% 15.02/3.18 % (3854076)Peak memory usage: 94 MB
% 15.02/3.18 % (3854076)Instructions burned: 159 (million)
% 15.02/3.18 % (3854081)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4130290758:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 15.02/3.18 % (3854078)Instruction limit reached!
% 15.02/3.18 % (3854078)------------------------------
% 15.02/3.18 % (3854078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.18 % (3854078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.18 % (3854078)CaDiCaL version: 2.1.3
% 15.02/3.18 % (3854078)Termination reason: Instruction limit
% 15.02/3.18 % (3854078)Termination phase: Property scanning
% 15.02/3.18 % (3854078)Time elapsed: 0.133 s
% 15.02/3.18 % (3854078)Peak memory usage: 95 MB
% 15.02/3.18 % (3854078)Instructions burned: 248 (million)
% 15.02/3.18 % (3854081)Instruction limit reached!
% 15.02/3.18 % (3854081)------------------------------
% 15.02/3.18 % (3854081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.18 % (3854081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.18 % (3854081)CaDiCaL version: 2.1.3
% 15.02/3.18 % (3854081)Termination reason: Instruction limit
% 15.02/3.18 % (3854081)Termination phase: Saturation
% 15.02/3.18 % (3854081)Time elapsed: 0.085 s
% 15.02/3.18 % (3854081)Peak memory usage: 96 MB
% 15.02/3.18 % (3854081)Instructions burned: 297 (million)
% 15.02/3.18 % (3854084)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=865894240:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 15.02/3.18 % (3854077)Instruction limit reached!
% 15.02/3.18 % (3854077)------------------------------
% 15.02/3.18 % (3854077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.18 % (3854077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.18 % (3854077)CaDiCaL version: 2.1.3
% 15.02/3.18 % (3854077)Termination reason: Instruction limit
% 15.02/3.18 % (3854077)Termination phase: Saturation
% 15.02/3.18 % (3854077)Time elapsed: 0.202 s
% 15.02/3.18 % (3854077)Peak memory usage: 96 MB
% 15.02/3.18 % (3854077)Instructions burned: 326 (million)
% 15.02/3.18 % (3854087)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3984950972:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 15.02/3.18 % (3854086)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=432877390:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 15.02/3.18 % (3854089)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=648728074:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 15.02/3.18 % (3854086)Instruction limit reached!
% 15.02/3.18 % (3854086)------------------------------
% 15.02/3.18 % (3854086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.18 % (3854086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.18 % (3854086)CaDiCaL version: 2.1.3
% 15.02/3.18 % (3854086)Termination reason: Instruction limit
% 15.02/3.18 % (3854086)Termination phase: Property scanning
% 15.02/3.18 % (3854086)Time elapsed: 0.061 s
% 15.02/3.18 % (3854086)Peak memory usage: 92 MB
% 15.02/3.18 % (3854086)Instructions burned: 115 (million)
% 15.02/3.18 % (3854087)Instruction limit reached!
% 15.02/3.18 % (3854087)------------------------------
% 15.02/3.18 % (3854087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854087)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854087)Termination reason: Instruction limit
% 8.88/3.21 % (3854087)Termination phase: Property scanning
% 8.88/3.21 % (3854087)Time elapsed: 0.079 s
% 8.88/3.21 % (3854087)Peak memory usage: 95 MB
% 8.88/3.21 % (3854087)Instructions burned: 129 (million)
% 8.88/3.21 % (3854089)Instruction limit reached!
% 8.88/3.21 % (3854089)------------------------------
% 8.88/3.21 % (3854089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854089)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854089)Termination reason: Instruction limit
% 8.88/3.21 % (3854089)Termination phase: Property scanning
% 8.88/3.21 % (3854089)Time elapsed: 0.046 s
% 8.88/3.21 % (3854089)Peak memory usage: 88 MB
% 8.88/3.21 % (3854089)Instructions burned: 117 (million)
% 8.88/3.21 % (3854093)lrs+10_1_sil=8000:sp=occurrence:random_seed=162647559:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 8.88/3.21 % (3854094)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3309168570:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.88/3.21 % (3854095)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1345796271:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 8.88/3.21 % (3854094)Instruction limit reached!
% 8.88/3.21 % (3854094)------------------------------
% 8.88/3.21 % (3854094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854094)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854094)Termination reason: Instruction limit
% 8.88/3.21 % (3854094)Termination phase: Saturation
% 8.88/3.21 % (3854094)Time elapsed: 0.243 s
% 8.88/3.21 % (3854094)Peak memory usage: 97 MB
% 8.88/3.21 % (3854094)Instructions burned: 437 (million)
% 8.88/3.21 % (3854099)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4264561601:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 8.88/3.21 % (3854099)Instruction limit reached!
% 8.88/3.21 % (3854099)------------------------------
% 8.88/3.21 % (3854099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854099)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854099)Termination reason: Instruction limit
% 8.88/3.21 % (3854099)Termination phase: Saturation
% 8.88/3.21 % (3854099)Time elapsed: 0.074 s
% 8.88/3.21 % (3854099)Peak memory usage: 94 MB
% 8.88/3.21 % (3854099)Instructions burned: 134 (million)
% 8.88/3.21 % (3854093)Instruction limit reached!
% 8.88/3.21 % (3854093)------------------------------
% 8.88/3.21 % (3854093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854093)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854093)Termination reason: Instruction limit
% 8.88/3.21 % (3854093)Termination phase: Saturation
% 8.88/3.21 % (3854093)Time elapsed: 0.523 s
% 8.88/3.21 % (3854093)Peak memory usage: 103 MB
% 8.88/3.21 % (3854093)Instructions burned: 908 (million)
% 8.88/3.21 % (3854084)Instruction limit reached!
% 8.88/3.21 % (3854084)------------------------------
% 8.88/3.21 % (3854084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.88/3.21 % (3854084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.88/3.21 % (3854084)CaDiCaL version: 2.1.3
% 8.88/3.21 % (3854084)Termination reason: Instruction limit
% 8.88/3.21 % (3854084)Termination phase: Saturation
% 8.88/3.21 % (3854084)Time elapsed: 0.825 s
% 8.88/3.21 % (3854084)Peak memory usage: 217 MB
% 8.88/3.21 % (3854084)Instructions burned: 2352 (million)
% 8.88/3.21 % (3854103)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=3120013721:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 8.88/3.21 % (3854101)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3684417462:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 8.88/3.21 % (3854102)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3927670955:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 0.16/3.40 % (3854103)Instruction limit reached!
% 0.16/3.40 % (3854103)------------------------------
% 0.16/3.40 % (3854103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854103)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854103)Termination reason: Instruction limit
% 0.16/3.40 % (3854103)Termination phase: Property scanning
% 0.16/3.40 % (3854103)Time elapsed: 0.036 s
% 0.16/3.40 % (3854103)Peak memory usage: 91 MB
% 0.16/3.40 % (3854103)Instructions burned: 127 (million)
% 0.16/3.40 % (3854107)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1084617628:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 0.16/3.40 % (3854107)Instruction limit reached!
% 0.16/3.40 % (3854107)------------------------------
% 0.16/3.40 % (3854107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854107)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854107)Termination reason: Instruction limit
% 0.16/3.40 % (3854107)Termination phase: SInE selection
% 0.16/3.40 % (3854107)Time elapsed: 0.033 s
% 0.16/3.40 % (3854107)Peak memory usage: 88 MB
% 0.16/3.40 % (3854107)Instructions burned: 135 (million)
% 0.16/3.40 % (3854109)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2405902171:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 0.16/3.40 % (3854109)Instruction limit reached!
% 0.16/3.40 % (3854109)------------------------------
% 0.16/3.40 % (3854109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854109)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854109)Termination reason: Instruction limit
% 0.16/3.40 % (3854109)Termination phase: Saturation
% 0.16/3.40 % (3854109)Time elapsed: 0.042 s
% 0.16/3.40 % (3854109)Peak memory usage: 95 MB
% 0.16/3.40 % (3854109)Instructions burned: 143 (million)
% 0.16/3.40 % (3854101)Instruction limit reached!
% 0.16/3.40 % (3854101)------------------------------
% 0.16/3.40 % (3854101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854101)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854101)Termination reason: Instruction limit
% 0.16/3.40 % (3854101)Termination phase: Saturation
% 0.16/3.40 % (3854101)Time elapsed: 0.314 s
% 0.16/3.40 % (3854101)Peak memory usage: 100 MB
% 0.16/3.40 % (3854101)Instructions burned: 594 (million)
% 0.16/3.40 % (3854062)First to succeed.
% 0.16/3.40 % (3854062)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3854056"
% 0.16/3.40 % (3854111)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=561322657:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 0.16/3.40 % (3854095)Also succeeded, but the first one will report.
% 0.16/3.40 % (3854112)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=305753550:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 0.16/3.40 % (3854111)Instruction limit reached!
% 0.16/3.40 % (3854111)------------------------------
% 0.16/3.40 % (3854111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854111)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854111)Termination reason: Instruction limit
% 0.16/3.40 % (3854111)Termination phase: Saturation
% 0.16/3.40 % (3854111)Time elapsed: 0.124 s
% 0.16/3.40 % (3854111)Peak memory usage: 98 MB
% 0.16/3.40 % (3854111)Instructions burned: 432 (million)
% 0.16/3.40 % (3854115)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=2264257593:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 0.16/3.40 % (3854115)Instruction limit reached!
% 0.16/3.40 % (3854115)------------------------------
% 0.16/3.40 % (3854115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854115)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854115)Termination reason: Instruction limit
% 0.16/3.40 % (3854115)Termination phase: Property scanning
% 0.16/3.40 % (3854115)Time elapsed: 0.052 s
% 0.16/3.40 % (3854115)Peak memory usage: 95 MB
% 0.16/3.40 % (3854115)Instructions burned: 152 (million)
% 0.16/3.40 % (3854062)Refutation found. Thanks to Tanya!
% 0.16/3.40 % SZS status Theorem for theBenchmark
% 0.16/3.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/3.40 % (3854062)------------------------------
% 0.16/3.40 % (3854062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.40 % (3854062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.40 % (3854062)CaDiCaL version: 2.1.3
% 0.16/3.40 % (3854062)Termination reason: Refutation
% 0.16/3.40 % (3854062)Time elapsed: 1.692 s
% 0.16/3.40 % (3854062)Peak memory usage: 163 MB
% 0.16/3.40 % (3854062)Instructions burned: 3120 (million)
% 0.16/3.40 % (3854062)------------------------------
% 0.16/3.40 % (3854062)------------------------------
% 0.16/3.40 % (3854056)Success in time 2.312 s
% 0.16/3.40 % Vampire exiting
%------------------------------------------------------------------------------