%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM630+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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:05 PM UTC 2026
% Result : Theorem 6.01s 6.33s
% Output : Refutation 6.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 31 ( 17 unt; 0 def)
% Number of atoms : 76 ( 32 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 67 ( 22 ~; 22 |; 20 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 16 ( 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f86,axiom,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( ( aSet0(X1)
& aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4151) ).
fof(f91,axiom,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4660) ).
fof(f104,axiom,
( aSet0(xP)
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5164) ).
fof(f111,axiom,
( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(xn,szNzAzT0)
& sdtlpdtrp0(xe,xn) = xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5309) ).
fof(f114,axiom,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5585) ).
fof(f115,axiom,
aElementOf0(xP,slbdtsldtrb0(xD,xk)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5599) ).
fof(f116,conjecture,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f117,negated_conjecture,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(negated_conjecture,[status(cth)],[f116]) ).
fof(f118,plain,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(flattening,[],[f117]) ).
fof(f240,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(X1)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f241,plain,
( aFunction0(xC)
& szDzozmdt0(xC) = szNzAzT0
& ! [X0] :
( ( aFunction0(sdtlpdtrp0(xC,X0))
& szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
& ! [X1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ aSet0(X1)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)) ) )
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(flattening,[],[f240]) ).
fof(f249,plain,
( aFunction0(xe)
& szDzozmdt0(xe) = szNzAzT0
& ! [X0] :
( sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f416,plain,
! [X0,X1] :
( ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
| ~ aSet0(X1)
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(cnf_transformation,[],[f241]) ).
fof(f429,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| szmzizndt0(sdtlpdtrp0(xN,X0)) = sdtlpdtrp0(xe,X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f453,plain,
aSet0(xP),
inference(cnf_transformation,[],[f104]) ).
fof(f460,plain,
xp = sdtlpdtrp0(xe,xn),
inference(cnf_transformation,[],[f111]) ).
fof(f461,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[],[f111]) ).
fof(f465,plain,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
inference(cnf_transformation,[],[f114]) ).
fof(f466,plain,
aElementOf0(xP,slbdtsldtrb0(xD,xk)),
inference(cnf_transformation,[],[f115]) ).
fof(f467,plain,
sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP),
inference(cnf_transformation,[],[f118]) ).
fof(f623,plain,
! [X0,X1] :
( ~ aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))
| ~ aElementOf0(X0,szNzAzT0)
| aSet0(X1)
| sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) ),
inference(consistent_polarity_flipping,[],[f416]) ).
fof(f635,plain,
~ aSet0(xP),
inference(consistent_polarity_flipping,[],[f453]) ).
fof(f990,plain,
sdtlpdtrp0(xe,xn) = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(resolution,[],[f429,f461]) ).
fof(f996,plain,
xp = szmzizndt0(sdtlpdtrp0(xN,xn)),
inference(forward_demodulation,[],[f990,f460]) ).
fof(f2328,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xD,xk))
| ~ aElementOf0(xn,szNzAzT0)
| aSet0(X0)
| sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0) = sdtlpdtrp0(xc,sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(superposition,[],[f623,f465]) ).
fof(f2329,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xD,xk))
| aSet0(X0)
| sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0) = sdtlpdtrp0(xc,sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xn)))) ),
inference(forward_subsumption_resolution,[],[f2328,f461]) ).
fof(f2876,plain,
sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) != sdtlpdtrp0(xc,sdtpldt0(xP,xp)),
inference(superposition,[],[f467,f996]) ).
fof(f22674,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xD,xk))
| sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0) = sdtlpdtrp0(xc,sdtpldt0(X0,xp))
| aSet0(X0) ),
inference(forward_demodulation,[],[f2329,f996]) ).
fof(f28012,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) = sdtlpdtrp0(xc,sdtpldt0(xP,xp))
| aSet0(xP) ),
inference(resolution,[],[f22674,f466]) ).
fof(f28061,plain,
aSet0(xP),
inference(forward_subsumption_resolution,[],[f28012,f2876]) ).
fof(f28091,plain,
$false,
inference(forward_subsumption_resolution,[],[f28061,f635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM630+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/5.38 % Computer : n014.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sun Sep 27 20:50:36 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.14/5.41 Running first-order model finding
% 0.14/5.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.01/6.33 % (1146691)Will run a generic schedule for satisfiability detection.
% 6.01/6.33 % (1146698)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4202904121:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.01/6.33 % (1146697)% WARNING: option uhcvi not known.
% 6.01/6.33 % (1146696)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1359422522_2999 on theBenchmark for (2999ds/0Mi)
% 6.01/6.33 % (1146697)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2247456630:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.01/6.33 % (1146699)dis+10_1_sil=32000:sp=arity:random_seed=730512121:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.01/6.33 % (1146700)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1524044304:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.01/6.33 % (1146701)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=148837548:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.01/6.33 % (1146702)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1904902112:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.01/6.33 % TRYING [1]
% 6.01/6.33 % TRYING [2]
% 6.01/6.33 % TRYING [3]
% 6.01/6.33 % TRYING [4]
% 6.01/6.33 % (1146699)Instruction limit reached!
% 6.01/6.33 % (1146699)------------------------------
% 6.01/6.33 % (1146699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146699)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146699)Termination reason: Instruction limit
% 6.01/6.33 % (1146699)Termination phase: Saturation
% 6.01/6.33 % (1146699)Time elapsed: 0.069 s
% 6.01/6.33 % (1146699)Peak memory usage: 13 MB
% 6.01/6.33 % (1146699)Instructions burned: 104 (million)
% 6.01/6.33 % (1146700)Instruction limit reached!
% 6.01/6.33 % (1146700)------------------------------
% 6.01/6.33 % (1146700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146700)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146700)Termination reason: Instruction limit
% 6.01/6.33 % (1146700)Termination phase: Saturation
% 6.01/6.33 % (1146700)Time elapsed: 0.074 s
% 6.01/6.33 % (1146700)Peak memory usage: 13 MB
% 6.01/6.33 % (1146700)Instructions burned: 117 (million)
% 6.01/6.33 % (1146701)Instruction limit reached!
% 6.01/6.33 % (1146701)------------------------------
% 6.01/6.33 % (1146701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146701)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146701)Termination reason: Instruction limit
% 6.01/6.33 % (1146701)Termination phase: Saturation
% 6.01/6.33 % (1146701)Time elapsed: 0.079 s
% 6.01/6.33 % (1146701)Peak memory usage: 13 MB
% 6.01/6.33 % (1146701)Instructions burned: 133 (million)
% 6.01/6.33 % (1146710)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4102267612:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.01/6.33 % (1146711)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=960667763:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.01/6.33 % (1146712)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=3058390496:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.01/6.33 % TRYING [1]
% 6.01/6.33 % TRYING [2]
% 6.01/6.33 % (1146702)Instruction limit reached!
% 6.01/6.33 % (1146702)------------------------------
% 6.01/6.33 % (1146702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146702)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146702)Termination reason: Instruction limit
% 6.01/6.33 % (1146702)Termination phase: Saturation
% 6.01/6.33 % (1146702)Time elapsed: 0.110 s
% 6.01/6.33 % (1146702)Peak memory usage: 14 MB
% 6.01/6.33 % (1146702)Instructions burned: 159 (million)
% 6.01/6.33 % TRYING [3]
% 6.01/6.33 % (1146716)ott-21_1_sil=16000:fs=off:random_seed=1945194157:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.01/6.33 % TRYING [5]
% 6.01/6.33 % TRYING [4]
% 6.01/6.33 % (1146711)Instruction limit reached!
% 6.01/6.33 % (1146711)------------------------------
% 6.01/6.33 % (1146711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146711)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146711)Termination reason: Instruction limit
% 6.01/6.33 % (1146711)Termination phase: Saturation
% 6.01/6.33 % (1146711)Time elapsed: 0.086 s
% 6.01/6.33 % (1146711)Peak memory usage: 13 MB
% 6.01/6.33 % (1146711)Instructions burned: 132 (million)
% 6.01/6.33 % (1146718)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3142153850:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.01/6.33 % (1146716)Instruction limit reached!
% 6.01/6.33 % (1146716)------------------------------
% 6.01/6.33 % (1146716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146716)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146716)Termination reason: Instruction limit
% 6.01/6.33 % (1146716)Termination phase: Saturation
% 6.01/6.33 % (1146716)Time elapsed: 0.102 s
% 6.01/6.33 % (1146716)Peak memory usage: 13 MB
% 6.01/6.33 % (1146716)Instructions burned: 180 (million)
% 6.01/6.33 % TRYING [5]
% 6.01/6.33 % (1146720)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3036229739:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.01/6.33 % TRYING [1]
% 6.01/6.33 % TRYING [2]
% 6.01/6.33 % TRYING [6]
% 6.01/6.33 % TRYING [3]
% 6.01/6.33 % (1146710)Instruction limit reached!
% 6.01/6.33 % (1146710)------------------------------
% 6.01/6.33 % (1146710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146710)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146710)Termination reason: Instruction limit
% 6.01/6.33 % (1146710)Termination phase: Finite model building constraint generation
% 6.01/6.33 % (1146710)Time elapsed: 0.312 s
% 6.01/6.33 % (1146710)Peak memory usage: 35 MB
% 6.01/6.33 % (1146710)Instructions burned: 715 (million)
% 6.01/6.33 % TRYING [4]
% 6.01/6.33 % (1146722)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2492884614:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.01/6.33 % (1146712)Instruction limit reached!
% 6.01/6.33 % (1146712)------------------------------
% 6.01/6.33 % (1146712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146712)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146712)Termination reason: Instruction limit
% 6.01/6.33 % (1146712)Termination phase: Saturation
% 6.01/6.33 % (1146712)Time elapsed: 0.382 s
% 6.01/6.33 % (1146712)Peak memory usage: 17 MB
% 6.01/6.33 % (1146712)Instructions burned: 685 (million)
% 6.01/6.33 % (1146724)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=524346364:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.01/6.33 % (1146718)Instruction limit reached!
% 6.01/6.33 % (1146718)------------------------------
% 6.01/6.33 % (1146718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146718)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146718)Termination reason: Instruction limit
% 6.01/6.33 % (1146718)Termination phase: Saturation
% 6.01/6.33 % (1146718)Time elapsed: 0.328 s
% 6.01/6.33 % (1146718)Peak memory usage: 15 MB
% 6.01/6.33 % (1146718)Instructions burned: 477 (million)
% 6.01/6.33 % (1146726)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=1183631789: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)
% 6.01/6.33 % (1146720)Instruction limit reached!
% 6.01/6.33 % (1146720)------------------------------
% 6.01/6.33 % (1146720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146720)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146720)Termination reason: Instruction limit
% 6.01/6.33 % (1146720)Termination phase: Finite model building SAT solving
% 6.01/6.33 % (1146720)Time elapsed: 0.366 s
% 6.01/6.33 % (1146720)Peak memory usage: 23 MB
% 6.01/6.33 % (1146720)Instructions burned: 866 (million)
% 6.01/6.33 % (1146728)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1709753390:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 6.01/6.33 % TRYING [7]
% 6.01/6.33 % TRYING [14]
% 6.01/6.33 % (1146697) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1146691-1146697"...
% 6.01/6.33 % (1146697)...printing done.
% 6.01/6.33 % (1146697)Refutation found. Thanks to Tanya!
% 6.01/6.33 % SZS status Theorem for theBenchmark
% 6.01/6.33 % SZS output start Proof for theBenchmark
% See solution above
% 6.01/6.33 % (1146697)------------------------------
% 6.01/6.33 % (1146697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.01/6.33 % (1146697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/6.33 % (1146697)CaDiCaL version: 2.1.3
% 6.01/6.33 % (1146697)Termination reason: Refutation
% 6.01/6.33 % (1146697)Time elapsed: 0.860 s
% 6.01/6.33 % (1146697)Peak memory usage: 24 MB
% 6.01/6.33 % (1146697)Instructions burned: 1418 (million)
% 6.01/6.33 % (1146691)Success in time 0.91 s
% 6.01/6.33 % Vampire exiting
%------------------------------------------------------------------------------