%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM621+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 12:25:03 PM UTC 2026
% Result : Theorem 12.78s 2.25s
% Output : Refutation 12.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 51 ( 15 unt; 1 def)
% Number of atoms : 136 ( 21 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 137 ( 52 ~; 44 |; 29 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 2 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 31 ( 0 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,axiom,
! [X0,X1] :
( ( aElementOf0(X0,szNzAzT0)
& aElementOf0(X1,szNzAzT0) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLessASymm) ).
fof(f91,axiom,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0))
& ! [X1] :
( aElementOf0(X1,sdtlpdtrp0(xN,X0))
=> sdtlseqdt0(sdtlpdtrp0(xe,X0),X1) )
& sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__4660) ).
fof(f101,axiom,
( ! [X0] :
( aElementOf0(X0,xQ)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xQ,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5106) ).
fof(f103,axiom,
( aElementOf0(xp,xQ)
& ! [X0] :
( aElementOf0(X0,xQ)
=> sdtlseqdt0(xp,X0) )
& xp = szmzizndt0(xQ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5147) ).
fof(f111,axiom,
( aElementOf0(xn,szDzozmdt0(xd))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(xn,szNzAzT0)
& sdtlpdtrp0(xe,xn) = xp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5309) ).
fof(f113,axiom,
( aElement0(xx)
& aElementOf0(xx,xQ)
& xx != szmzizndt0(xQ)
& aElementOf0(xx,xP) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5348) ).
fof(f116,axiom,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
=> sdtlseqdt0(xx,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__5401) ).
fof(f118,conjecture,
( ( ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xn))
=> aElementOf0(X0,sdtlpdtrp0(xN,xm)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f119,negated_conjecture,
~ ( ( ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xn))
=> aElementOf0(X0,sdtlpdtrp0(xN,xm)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(negated_conjecture,[status(cth)],[f118]) ).
fof(f184,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f185,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f184]) ).
fof(f268,plain,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( ( aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0))
& ! [X1] :
( sdtlseqdt0(sdtlpdtrp0(xe,X0),X1)
| ~ aElementOf0(X1,sdtlpdtrp0(xN,X0)) )
& sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f277,plain,
( ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xQ) )
& aSubsetOf0(xQ,szNzAzT0) ),
inference(ennf_transformation,[],[f101]) ).
fof(f279,plain,
( aElementOf0(xp,xQ)
& ! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xQ) )
& xp = szmzizndt0(xQ) ),
inference(ennf_transformation,[],[f103]) ).
fof(f283,plain,
! [X0] :
( sdtlseqdt0(xx,X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xm)) ),
inference(ennf_transformation,[],[f116]) ).
fof(f285,plain,
( ~ aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xn)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) ),
inference(ennf_transformation,[],[f119]) ).
fof(f286,plain,
( ~ aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xn)) )
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) ),
inference(flattening,[],[f285]) ).
fof(f341,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| X0 = X1 ),
inference(cnf_transformation,[],[f185]) ).
fof(f764,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f813,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[],[f277]) ).
fof(f820,plain,
! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[],[f279]) ).
fof(f821,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[],[f279]) ).
fof(f822,plain,
aElementOf0(xp,xQ),
inference(cnf_transformation,[],[f279]) ).
fof(f839,plain,
xp = sdtlpdtrp0(xe,xn),
inference(cnf_transformation,[],[f111]) ).
fof(f840,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f111]) ).
fof(f846,plain,
szmzizndt0(xQ) != xx,
inference(cnf_transformation,[],[f113]) ).
fof(f847,plain,
aElementOf0(xx,xQ),
inference(cnf_transformation,[],[f113]) ).
fof(f854,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xm))
| sdtlseqdt0(xx,X0) ),
inference(cnf_transformation,[],[f283]) ).
fof(f858,plain,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xn)) ),
inference(cnf_transformation,[],[f286]) ).
fof(f933,plain,
xp != xx,
inference(superposition,[],[f846,f821]) ).
fof(f1000,plain,
! [X0] :
( ~ aElementOf0(X0,sdtlpdtrp0(xN,xn))
| sdtlseqdt0(xx,X0) ),
inference(resolution,[],[f854,f858]) ).
fof(f1173,plain,
( ~ aElementOf0(xn,szNzAzT0)
| sdtlseqdt0(xx,sdtlpdtrp0(xe,xn)) ),
inference(resolution,[],[f764,f1000]) ).
fof(f1182,plain,
sdtlseqdt0(xx,sdtlpdtrp0(xe,xn)),
inference(forward_subsumption_resolution,[],[f1173,f840]) ).
fof(f1184,plain,
sdtlseqdt0(xx,xp),
inference(forward_demodulation,[],[f1182,f839]) ).
fof(f2657,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xp)
| ~ aElementOf0(xp,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| xp = X0
| ~ aElementOf0(X0,xQ) ),
inference(resolution,[],[f341,f820]) ).
fof(f2689,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xp)
| ~ aElementOf0(xp,szNzAzT0)
| xp = X0
| ~ aElementOf0(X0,xQ) ),
inference(forward_subsumption_resolution,[],[f2657,f813]) ).
fof(f13205,definition,
( spl61_93
<=> aElementOf0(xp,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl61_93])],[avatar_definition]) ).
fof(f13206,plain,
( aElementOf0(xp,szNzAzT0)
| ~ spl61_93 ),
inference(avatar_component_clause,[],[f13205]) ).
fof(f13207,plain,
( ~ aElementOf0(xp,szNzAzT0)
| spl61_93 ),
inference(avatar_component_clause,[],[f13205]) ).
fof(f18264,plain,
( ~ aElementOf0(xp,xQ)
| spl61_93 ),
inference(resolution,[],[f13207,f813]) ).
fof(f18277,plain,
( $false
| spl61_93 ),
inference(forward_subsumption_resolution,[],[f18264,f822]) ).
fof(f18278,plain,
spl61_93,
inference(avatar_contradiction_clause,[],[f18277]) ).
fof(f22747,plain,
( ! [X0] :
( ~ sdtlseqdt0(X0,xp)
| xp = X0
| ~ aElementOf0(X0,xQ) )
| ~ spl61_93 ),
inference(forward_subsumption_resolution,[],[f2689,f13206]) ).
fof(f22748,plain,
( xp = xx
| ~ aElementOf0(xx,xQ)
| ~ spl61_93 ),
inference(resolution,[],[f22747,f1184]) ).
fof(f22781,plain,
( ~ aElementOf0(xx,xQ)
| ~ spl61_93 ),
inference(forward_subsumption_resolution,[],[f22748,f933]) ).
fof(f22788,plain,
( $false
| ~ spl61_93 ),
inference(forward_subsumption_resolution,[],[f22781,f847]) ).
fof(f22789,plain,
~ spl61_93,
inference(avatar_contradiction_clause,[],[f22788]) ).
cnf(s118,plain,
spl61_93,
inference(sat_conversion,[],[f18278]) ).
cnf(s148,plain,
~ spl61_93,
inference(sat_conversion,[],[f22789]) ).
cnf(s154,plain,
$false,
inference(rat,[],[s118,s148]) ).
fof(f22794,plain,
$false,
inference(avatar_sat_refutation,[],[s154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM621+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 20:47:07 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 Running first-order model finding
% 0.13/0.38 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.78/2.25 % (1145417)Will run a generic schedule for satisfiability detection.
% 12.78/2.25 % (1145428)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3895679071:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.78/2.25 % (1145423)% WARNING: option uhcvi not known.
% 12.78/2.25 % (1145422)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2893336023_2999 on theBenchmark for (2999ds/0Mi)
% 12.78/2.25 % (1145423)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=716250348:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.78/2.25 % (1145424)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3646145214:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.78/2.25 % (1145425)dis+10_1_sil=32000:sp=arity:random_seed=1298831294:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.78/2.25 % (1145426)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3108802930:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.78/2.25 % (1145427)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3710830813:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.78/2.25 % (1145428)Instruction limit reached!
% 12.78/2.25 % (1145428)------------------------------
% 12.78/2.25 % (1145428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145428)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145428)Termination reason: Instruction limit
% 12.78/2.25 % (1145428)Termination phase: Saturation
% 12.78/2.25 % (1145428)Time elapsed: 0.056 s
% 12.78/2.25 % (1145428)Peak memory usage: 15 MB
% 12.78/2.25 % (1145428)Instructions burned: 159 (million)
% 12.78/2.25 % TRYING [1]
% 12.78/2.25 % TRYING [2]
% 12.78/2.25 % (1145436)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3411761210:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 12.78/2.25 % (1145425)Instruction limit reached!
% 12.78/2.25 % (1145425)------------------------------
% 12.78/2.25 % (1145425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145425)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145425)Termination reason: Instruction limit
% 12.78/2.25 % (1145425)Termination phase: Saturation
% 12.78/2.25 % (1145425)Time elapsed: 0.066 s
% 12.78/2.25 % (1145425)Peak memory usage: 13 MB
% 12.78/2.25 % (1145425)Instructions burned: 104 (million)
% 12.78/2.25 % (1145426)Instruction limit reached!
% 12.78/2.25 % (1145426)------------------------------
% 12.78/2.25 % (1145426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145426)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145426)Termination reason: Instruction limit
% 12.78/2.25 % (1145426)Termination phase: Saturation
% 12.78/2.25 % (1145426)Time elapsed: 0.065 s
% 12.78/2.25 % (1145426)Peak memory usage: 13 MB
% 12.78/2.25 % (1145426)Instructions burned: 117 (million)
% 12.78/2.25 % TRYING [3]
% 12.78/2.25 % (1145427)Instruction limit reached!
% 12.78/2.25 % (1145427)------------------------------
% 12.78/2.25 % (1145427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145427)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145427)Termination reason: Instruction limit
% 12.78/2.25 % (1145427)Termination phase: Saturation
% 12.78/2.25 % (1145427)Time elapsed: 0.076 s
% 12.78/2.25 % (1145427)Peak memory usage: 14 MB
% 12.78/2.25 % (1145427)Instructions burned: 132 (million)
% 12.78/2.25 % TRYING [1]
% 12.78/2.25 % TRYING [2]
% 12.78/2.25 % (1145438)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3226014034:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 12.78/2.25 % (1145439)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3348157546:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.78/2.25 % TRYING [3]
% 12.78/2.25 % (1145440)ott-21_1_sil=16000:fs=off:random_seed=2243634292:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 12.78/2.25 % TRYING [4]
% 12.78/2.25 % TRYING [4]
% 12.78/2.25 % (1145438)Instruction limit reached!
% 12.78/2.25 % (1145438)------------------------------
% 12.78/2.25 % (1145438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145438)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145438)Termination reason: Instruction limit
% 12.78/2.25 % (1145438)Termination phase: Saturation
% 12.78/2.25 % (1145438)Time elapsed: 0.081 s
% 12.78/2.25 % (1145438)Peak memory usage: 14 MB
% 12.78/2.25 % (1145438)Instructions burned: 131 (million)
% 12.78/2.25 % (1145444)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=22504233:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 12.78/2.25 % TRYING [5]
% 12.78/2.25 % (1145440)Instruction limit reached!
% 12.78/2.25 % (1145440)------------------------------
% 12.78/2.25 % (1145440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145440)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145440)Termination reason: Instruction limit
% 12.78/2.25 % (1145440)Termination phase: Saturation
% 12.78/2.25 % (1145440)Time elapsed: 0.101 s
% 12.78/2.25 % (1145440)Peak memory usage: 13 MB
% 12.78/2.25 % (1145440)Instructions burned: 182 (million)
% 12.78/2.25 % (1145436)Instruction limit reached!
% 12.78/2.25 % (1145436)------------------------------
% 12.78/2.25 % (1145436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145436)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145436)Termination reason: Instruction limit
% 12.78/2.25 % (1145436)Termination phase: Finite model building constraint generation
% 12.78/2.25 % (1145436)Time elapsed: 0.152 s
% 12.78/2.25 % (1145436)Peak memory usage: 34 MB
% 12.78/2.25 % (1145436)Instructions burned: 722 (million)
% 12.78/2.25 % (1145446)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=576813833:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 12.78/2.25 % (1145447)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2248926547:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 12.78/2.25 % TRYING [1]
% 12.78/2.25 % TRYING [2]
% 12.78/2.25 % TRYING [3]
% 12.78/2.25 % TRYING [5]
% 12.78/2.25 % (1145439)Instruction limit reached!
% 12.78/2.25 % (1145439)------------------------------
% 12.78/2.25 % (1145439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145439)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145439)Termination reason: Instruction limit
% 12.78/2.25 % (1145439)Termination phase: Saturation
% 12.78/2.25 % (1145439)Time elapsed: 0.394 s
% 12.78/2.25 % (1145439)Peak memory usage: 20 MB
% 12.78/2.25 % (1145439)Instructions burned: 686 (million)
% 12.78/2.25 % (1145450)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3040899610:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 12.78/2.25 % (1145444)Instruction limit reached!
% 12.78/2.25 % (1145444)------------------------------
% 12.78/2.25 % (1145444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145444)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145444)Termination reason: Instruction limit
% 12.78/2.25 % (1145444)Termination phase: Saturation
% 12.78/2.25 % (1145444)Time elapsed: 0.322 s
% 12.78/2.25 % (1145444)Peak memory usage: 15 MB
% 12.78/2.25 % (1145444)Instructions burned: 478 (million)
% 12.78/2.25 % (1145452)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1343511615:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 12.78/2.25 % TRYING [4]
% 12.78/2.25 % (1145446)Instruction limit reached!
% 12.78/2.25 % (1145446)------------------------------
% 12.78/2.25 % (1145446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145446)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145446)Termination reason: Instruction limit
% 12.78/2.25 % (1145446)Termination phase: Finite model building constraint generation
% 12.78/2.25 % (1145446)Time elapsed: 0.369 s
% 12.78/2.25 % (1145446)Peak memory usage: 24 MB
% 12.78/2.25 % (1145446)Instructions burned: 867 (million)
% 12.78/2.25 % (1145454)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=813460906:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 12.78/2.25 % (1145447)Instruction limit reached!
% 12.78/2.25 % (1145447)------------------------------
% 12.78/2.25 % (1145447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145447)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145447)Termination reason: Instruction limit
% 12.78/2.25 % (1145447)Termination phase: Saturation
% 12.78/2.25 % (1145447)Time elapsed: 0.396 s
% 12.78/2.25 % (1145447)Peak memory usage: 27 MB
% 12.78/2.25 % (1145447)Instructions burned: 1181 (million)
% 12.78/2.25 % (1145456)fmb+10_1_sil=64000:random_seed=3610052577:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 12.78/2.25 % TRYING [1]
% 12.78/2.25 % TRYING [2]
% 12.78/2.25 % TRYING [3]
% 12.78/2.25 % TRYING [4]
% 12.78/2.25 % TRYING [6]
% 12.78/2.25 % (1145450)Instruction limit reached!
% 12.78/2.25 % (1145450)------------------------------
% 12.78/2.25 % (1145450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145450)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145450)Termination reason: Instruction limit
% 12.78/2.25 % (1145450)Termination phase: Finite model building constraint generation
% 12.78/2.25 % (1145450)Time elapsed: 0.415 s
% 12.78/2.25 % (1145450)Peak memory usage: 102 MB
% 12.78/2.25 % (1145450)Instructions burned: 889 (million)
% 12.78/2.25 % (1145452)Instruction limit reached!
% 12.78/2.25 % (1145452)------------------------------
% 12.78/2.25 % (1145452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145452)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145452)Termination reason: Instruction limit
% 12.78/2.25 % (1145452)Termination phase: Saturation
% 12.78/2.25 % (1145452)Time elapsed: 0.388 s
% 12.78/2.25 % (1145452)Peak memory usage: 23 MB
% 12.78/2.25 % (1145452)Instructions burned: 693 (million)
% 12.78/2.25 % (1145458)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4187165946:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 12.78/2.25 % (1145459)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1681047598:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 12.78/2.25 % TRYING [5]
% 12.78/2.25 % TRYING [20]
% 12.78/2.25 % TRYING [8]
% 12.78/2.25 % (1145454)Instruction limit reached!
% 12.78/2.25 % (1145454)------------------------------
% 12.78/2.25 % (1145454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145454)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145454)Termination reason: Instruction limit
% 12.78/2.25 % (1145454)Termination phase: Saturation
% 12.78/2.25 % (1145454)Time elapsed: 0.494 s
% 12.78/2.25 % (1145454)Peak memory usage: 22 MB
% 12.78/2.25 % (1145454)Instructions burned: 879 (million)
% 12.78/2.25 % (1145462)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=454001441:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 12.78/2.25 % (1145459)Instruction limit reached!
% 12.78/2.25 % (1145459)------------------------------
% 12.78/2.25 % (1145459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145459)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145459)Termination reason: Instruction limit
% 12.78/2.25 % (1145459)Termination phase: Finite model building constraint generation
% 12.78/2.25 % (1145459)Time elapsed: 0.322 s
% 12.78/2.25 % (1145459)Peak memory usage: 63 MB
% 12.78/2.25 % (1145459)Instructions burned: 922 (million)
% 12.78/2.25 % (1145464)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3693351436:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 12.78/2.25 % TRYING [6]
% 12.78/2.25 % (1145462) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1145417-1145462"...
% 12.78/2.25 % (1145462)...printing done.
% 12.78/2.25 % (1145462)Refutation found. Thanks to Tanya!
% 12.78/2.25 % SZS status Theorem for theBenchmark
% 12.78/2.25 % SZS output start Proof for theBenchmark
% See solution above
% 12.78/2.25 % (1145462)------------------------------
% 12.78/2.25 % (1145462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.78/2.25 % (1145462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.78/2.25 % (1145462)CaDiCaL version: 2.1.3
% 12.78/2.25 % (1145462)Termination reason: Refutation
% 12.78/2.25 % (1145462)Time elapsed: 0.666 s
% 12.78/2.25 % (1145462)Peak memory usage: 21 MB
% 12.78/2.25 % (1145462)Instructions burned: 1101 (million)
% 12.78/2.25 % (1145417)Success in time 1.861 s
% 12.78/2.25 % Vampire exiting
%------------------------------------------------------------------------------