%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO282+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:54:21 AM UTC 2026
% Result : Theorem 14.71s 2.73s
% Output : Refutation 14.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 8
% Syntax : Number of formulae : 72 ( 28 unt; 0 def)
% Number of atoms : 250 ( 77 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 327 ( 149 ~; 138 |; 33 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 114 ( 106 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ rinside(vd1125,vd1146),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','neg(neg(254))') ).
fof(f2,negated_conjecture,
~ ~ rinside(vd1125,vd1146),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( ron(vd1129,vd1146)
& rcenter(vd1123,vd1146)
& rcircle(vd1146)
& ron(vd1125,vd1145)
& ron(vd1123,vd1145) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(253))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(253))), 0), and(pred(comma_conjunct2(comma_conjunct2(253)), 0), pred(comma_conjunct1(comma_conjunct2(253)), 0)))), pred(comma_conjunct1(253), 0))') ).
fof(f5,axiom,
vd1123 = vd1127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(252, 1144, 0)') ).
fof(f18,axiom,
( rless(vf(vd1127,vd1129),vf(vd1123,vd1125))
& vd1127 != vd1129
& vd1123 != vd1125
& vd1129 = vd1130
& rpoint(vd1130)
& vd1127 = vd1128
& rpoint(vd1128)
& vd1125 = vd1126
& rpoint(vd1126)
& vd1123 = vd1124
& rpoint(vd1124) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))') ).
fof(f21,axiom,
! [X0,X1,X2,X3] :
( ( ron(X1,X3)
& rcenter(X2,X3)
& ? [X4] :
( X1 = X4
& rpoint(X4) )
& ? [X5] :
( X0 = X5
& rpoint(X5) ) )
=> ( rless(vf(X2,X0),vf(X2,X1))
<=> rinside(X0,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))') ).
fof(f23,axiom,
! [X0,X1] :
( ( ? [X2] :
( X1 = X2
& rpoint(X2) )
& ? [X3] :
( X0 = X3
& rpoint(X3) ) )
=> ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))') ).
fof(f24,axiom,
! [X0,X1] :
( ( X0 = X1
& rreal(X1) )
=> ~ rless(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(149), 0), imp(cond(axiom(149), 0)))') ).
fof(f25,axiom,
! [X0,X1,X2,X3] :
( ( rless(X0,X2)
& X2 = X3
& rreal(X3)
& X0 = X1
& rreal(X1) )
=> ( ~ rless(X2,X0)
| X0 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(axiom(147), 0), imp(cond(axiom(147), 0)))') ).
fof(f126,plain,
rinside(vd1125,vd1146),
inference(flattening,[],[f2]) ).
fof(f159,plain,
! [X0,X1,X2,X3] :
( ( rless(vf(X2,X0),vf(X2,X1))
<=> rinside(X0,X3) )
| ~ ron(X1,X3)
| ~ rcenter(X2,X3)
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f160,plain,
! [X0,X1,X2,X3] :
( ( rless(vf(X2,X0),vf(X2,X1))
<=> rinside(X0,X3) )
| ~ ron(X1,X3)
| ~ rcenter(X2,X3)
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(flattening,[],[f159]) ).
fof(f163,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f164,plain,
! [X0,X1] :
( ? [X4] :
( vf(X0,X1) = X4
& rreal(X4) )
| ! [X2] :
( X1 != X2
| ~ rpoint(X2) )
| ! [X3] :
( X0 != X3
| ~ rpoint(X3) ) ),
inference(flattening,[],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| X0 != X1
| ~ rreal(X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f166,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| X0 != X1
| ~ rreal(X1) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( ~ rless(X2,X0)
| X0 = X2
| ~ rless(X0,X2)
| X2 != X3
| ~ rreal(X3)
| X0 != X1
| ~ rreal(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( ~ rless(X2,X0)
| X0 = X2
| ~ rless(X0,X2)
| X2 != X3
| ~ rreal(X3)
| X0 != X1
| ~ rreal(X1) ),
inference(flattening,[],[f167]) ).
fof(f359,plain,
! [X0,X1,X2,X3] :
( ( ( rless(vf(X2,X0),vf(X2,X1))
| ~ rinside(X0,X3) )
& ( rinside(X0,X3)
| ~ rless(vf(X2,X0),vf(X2,X1)) ) )
| ~ ron(X1,X3)
| ~ rcenter(X2,X3)
| ! [X4] :
( X1 != X4
| ~ rpoint(X4) )
| ! [X5] :
( X0 != X5
| ~ rpoint(X5) ) ),
inference(nnf_transformation,[],[f160]) ).
fof(f361,plain,
! [X0,X1] :
( ? [X2] :
( vf(X0,X1) = X2
& rreal(X2) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(rectify,[],[f164]) ).
fof(f362,plain,
! [X0,X1] :
( ( vf(X0,X1) = sK3(X0,X1)
& rreal(sK3(X0,X1)) )
| ! [X3] :
( X1 != X3
| ~ rpoint(X3) )
| ! [X4] :
( X0 != X4
| ~ rpoint(X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f361]) ).
fof(f427,plain,
rinside(vd1125,vd1146),
inference(cnf_transformation,[],[f126]) ).
fof(f431,plain,
rcenter(vd1123,vd1146),
inference(cnf_transformation,[],[f3]) ).
fof(f432,plain,
ron(vd1129,vd1146),
inference(cnf_transformation,[],[f3]) ).
fof(f434,plain,
vd1123 = vd1127,
inference(cnf_transformation,[],[f5]) ).
fof(f453,plain,
rpoint(vd1126),
inference(cnf_transformation,[],[f18]) ).
fof(f454,plain,
vd1125 = vd1126,
inference(cnf_transformation,[],[f18]) ).
fof(f455,plain,
rpoint(vd1128),
inference(cnf_transformation,[],[f18]) ).
fof(f456,plain,
vd1127 = vd1128,
inference(cnf_transformation,[],[f18]) ).
fof(f457,plain,
rpoint(vd1130),
inference(cnf_transformation,[],[f18]) ).
fof(f458,plain,
vd1129 = vd1130,
inference(cnf_transformation,[],[f18]) ).
fof(f461,plain,
rless(vf(vd1127,vd1129),vf(vd1123,vd1125)),
inference(cnf_transformation,[],[f18]) ).
fof(f469,plain,
! [X2,X3,X0,X1,X4,X5] :
( rless(vf(X2,X0),vf(X2,X1))
| ~ rinside(X0,X3)
| ~ ron(X1,X3)
| ~ rcenter(X2,X3)
| X1 != X4
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(cnf_transformation,[],[f359]) ).
fof(f472,plain,
! [X3,X0,X1,X4] :
( rreal(sK3(X0,X1))
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f362]) ).
fof(f473,plain,
! [X3,X0,X1,X4] :
( vf(X0,X1) = sK3(X0,X1)
| X1 != X3
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(cnf_transformation,[],[f362]) ).
fof(f474,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| X0 != X1
| ~ rreal(X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f475,plain,
! [X2,X3,X0,X1] :
( ~ rless(X2,X0)
| X0 = X2
| ~ rless(X0,X2)
| X2 != X3
| ~ rreal(X3)
| X0 != X1
| ~ rreal(X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f692,plain,
vd1123 = vd1128,
inference(definition_unfolding,[],[f434,f456]) ).
fof(f693,plain,
rinside(vd1126,vd1146),
inference(definition_unfolding,[],[f427,f454]) ).
fof(f694,plain,
ron(vd1130,vd1146),
inference(definition_unfolding,[],[f432,f458]) ).
fof(f695,plain,
rcenter(vd1128,vd1146),
inference(definition_unfolding,[],[f431,f692]) ).
fof(f714,plain,
rless(vf(vd1128,vd1130),vf(vd1128,vd1126)),
inference(definition_unfolding,[],[f461,f456,f458,f692,f454]) ).
fof(f739,plain,
! [X2,X3,X0,X4,X5] :
( rless(vf(X2,X0),vf(X2,X4))
| ~ rinside(X0,X3)
| ~ ron(X4,X3)
| ~ rcenter(X2,X3)
| ~ rpoint(X4)
| X0 != X5
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f469]) ).
fof(f740,plain,
! [X2,X3,X4,X5] :
( ~ rcenter(X2,X3)
| ~ rinside(X5,X3)
| ~ ron(X4,X3)
| rless(vf(X2,X5),vf(X2,X4))
| ~ rpoint(X4)
| ~ rpoint(X5) ),
inference(equality_resolution,[],[f739]) ).
fof(f747,plain,
! [X3,X0,X4] :
( vf(X0,X3) = sK3(X0,X3)
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f473]) ).
fof(f748,plain,
! [X3,X4] :
( ~ rpoint(X4)
| ~ rpoint(X3)
| vf(X4,X3) = sK3(X4,X3) ),
inference(equality_resolution,[],[f747]) ).
fof(f749,plain,
! [X3,X0,X4] :
( rreal(sK3(X0,X3))
| ~ rpoint(X3)
| X0 != X4
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f472]) ).
fof(f750,plain,
! [X3,X4] :
( rreal(sK3(X4,X3))
| ~ rpoint(X3)
| ~ rpoint(X4) ),
inference(equality_resolution,[],[f749]) ).
fof(f751,plain,
! [X1] :
( ~ rless(X1,X1)
| ~ rreal(X1) ),
inference(equality_resolution,[],[f474]) ).
fof(f752,plain,
! [X3,X0,X1] :
( ~ rless(X3,X0)
| X0 = X3
| ~ rless(X0,X3)
| ~ rreal(X3)
| X0 != X1
| ~ rreal(X1) ),
inference(equality_resolution,[],[f475]) ).
fof(f753,plain,
! [X3,X1] :
( ~ rless(X3,X1)
| X1 = X3
| ~ rless(X1,X3)
| ~ rreal(X3)
| ~ rreal(X1) ),
inference(equality_resolution,[],[f752]) ).
fof(f1464,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1128,X0) = sK3(vd1128,X0) ),
inference(resolution,[],[f748,f455]) ).
fof(f1785,plain,
vf(vd1128,vd1130) = sK3(vd1128,vd1130),
inference(resolution,[],[f1464,f457]) ).
fof(f1787,plain,
vf(vd1128,vd1126) = sK3(vd1128,vd1126),
inference(resolution,[],[f1464,f453]) ).
fof(f1814,plain,
( rreal(vf(vd1128,vd1130))
| ~ rpoint(vd1130)
| ~ rpoint(vd1128) ),
inference(superposition,[],[f750,f1785]) ).
fof(f1815,plain,
( rreal(vf(vd1128,vd1130))
| ~ rpoint(vd1128) ),
inference(forward_subsumption_resolution,[],[f1814,f457]) ).
fof(f1816,plain,
rreal(vf(vd1128,vd1130)),
inference(forward_subsumption_resolution,[],[f1815,f455]) ).
fof(f1817,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rless(vf(vd1128,vd1126),vf(vd1128,vd1130))
| ~ rreal(vf(vd1128,vd1130))
| ~ rreal(vf(vd1128,vd1126)) ),
inference(resolution,[],[f753,f714]) ).
fof(f1818,plain,
( ~ rless(vf(vd1128,vd1126),vf(vd1128,vd1130))
| vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rreal(vf(vd1128,vd1126)) ),
inference(forward_subsumption_resolution,[],[f1817,f1816]) ).
fof(f1833,plain,
( rreal(vf(vd1128,vd1126))
| ~ rpoint(vd1126)
| ~ rpoint(vd1128) ),
inference(superposition,[],[f750,f1787]) ).
fof(f1834,plain,
( rreal(vf(vd1128,vd1126))
| ~ rpoint(vd1128) ),
inference(forward_subsumption_resolution,[],[f1833,f453]) ).
fof(f1835,plain,
rreal(vf(vd1128,vd1126)),
inference(forward_subsumption_resolution,[],[f1834,f455]) ).
fof(f2603,plain,
! [X0,X1] :
( rless(vf(vd1128,X0),vf(vd1128,X1))
| ~ ron(X1,vd1146)
| ~ rinside(X0,vd1146)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(resolution,[],[f740,f695]) ).
fof(f13445,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rreal(vf(vd1128,vd1126))
| ~ ron(vd1130,vd1146)
| ~ rinside(vd1126,vd1146)
| ~ rpoint(vd1130)
| ~ rpoint(vd1126) ),
inference(resolution,[],[f1818,f2603]) ).
fof(f13450,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ ron(vd1130,vd1146)
| ~ rinside(vd1126,vd1146)
| ~ rpoint(vd1130)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[],[f13445,f1835]) ).
fof(f13451,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rinside(vd1126,vd1146)
| ~ rpoint(vd1130)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[],[f13450,f694]) ).
fof(f13452,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rpoint(vd1130)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[],[f13451,f693]) ).
fof(f13453,plain,
( vf(vd1128,vd1130) = vf(vd1128,vd1126)
| ~ rpoint(vd1126) ),
inference(forward_subsumption_resolution,[],[f13452,f457]) ).
fof(f13454,plain,
vf(vd1128,vd1130) = vf(vd1128,vd1126),
inference(forward_subsumption_resolution,[],[f13453,f453]) ).
fof(f13456,plain,
rless(vf(vd1128,vd1130),vf(vd1128,vd1130)),
inference(superposition,[],[f714,f13454]) ).
fof(f13490,plain,
~ rreal(vf(vd1128,vd1130)),
inference(resolution,[],[f13456,f751]) ).
fof(f13498,plain,
$false,
inference(forward_subsumption_resolution,[],[f13490,f1816]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO282+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.38 % Computer : n010.cluster.edu
% 0.07/0.38 % Model : x86_64 x86_64
% 0.07/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.38 % Memory : 8046.5625MB
% 0.07/0.38 % OS : Linux 6.8.0-71-generic
% 0.07/0.39 % CPULimit : 300
% 0.07/0.39 % WCLimit : 300
% 0.07/0.39 % DateTime : Sun Sep 27 07:59:32 UTC 2026
% 0.07/0.39 % CPUTime :
% 0.07/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.42 Running first-order model finding
% 0.07/0.42 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
% 6.99/1.53 % (621391)Will run a generic schedule for satisfiability detection.
% 6.99/1.53 % (621396)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=346597488_2999 on theBenchmark for (2999ds/0Mi)
% 6.99/1.53 % (621397)% WARNING: option uhcvi not known.
% 6.99/1.53 % (621397)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2193173147:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.99/1.53 % (621398)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2645325393:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.99/1.53 % (621399)dis+10_1_sil=32000:sp=arity:random_seed=738529214:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.99/1.53 % (621400)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2871090812:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.99/1.53 % (621401)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3115634098:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.99/1.53 % (621402)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=325694211:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.99/1.53 % TRYING [1]
% 6.99/1.53 % TRYING [2]
% 6.99/1.53 % (621400)Instruction limit reached!
% 6.99/1.53 % (621400)------------------------------
% 6.99/1.53 % (621400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.53 % (621400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.53 % (621400)CaDiCaL version: 2.1.3
% 6.99/1.53 % (621400)Termination reason: Instruction limit
% 6.99/1.53 % (621400)Termination phase: Saturation
% 6.99/1.53 % (621400)Time elapsed: 0.054 s
% 6.99/1.53 % (621400)Peak memory usage: 13 MB
% 6.99/1.53 % (621400)Instructions burned: 116 (million)
% 6.99/1.53 % (621399)Instruction limit reached!
% 6.99/1.53 % (621399)------------------------------
% 6.99/1.53 % (621399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.53 % (621399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.53 % (621399)CaDiCaL version: 2.1.3
% 6.99/1.53 % (621399)Termination reason: Instruction limit
% 6.99/1.53 % (621399)Termination phase: Saturation
% 6.99/1.53 % (621399)Time elapsed: 0.058 s
% 6.99/1.53 % (621399)Peak memory usage: 13 MB
% 6.99/1.53 % (621399)Instructions burned: 104 (million)
% 6.99/1.53 % (621401)Instruction limit reached!
% 6.99/1.53 % (621401)------------------------------
% 6.99/1.53 % (621401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.53 % (621401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.53 % (621401)CaDiCaL version: 2.1.3
% 6.99/1.53 % (621401)Termination reason: Instruction limit
% 6.99/1.53 % (621401)Termination phase: Saturation
% 6.99/1.53 % (621401)Time elapsed: 0.062 s
% 6.99/1.53 % (621401)Peak memory usage: 13 MB
% 6.99/1.53 % (621401)Instructions burned: 131 (million)
% 6.99/1.53 % (621410)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=511939836:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.99/1.53 % (621411)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4238177415:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.99/1.53 % (621412)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=1440000659:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.99/1.53 % (621402)Instruction limit reached!
% 6.99/1.53 % (621402)------------------------------
% 6.99/1.53 % (621402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.53 % (621402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.53 % (621402)CaDiCaL version: 2.1.3
% 6.99/1.53 % (621402)Termination reason: Instruction limit
% 6.99/1.53 % (621402)Termination phase: Saturation
% 6.99/1.53 % (621402)Time elapsed: 0.094 s
% 6.99/1.53 % (621402)Peak memory usage: 16 MB
% 6.99/1.53 % (621402)Instructions burned: 160 (million)
% 6.99/1.53 % TRYING [1]
% 6.99/1.53 % TRYING [2]
% 6.99/1.53 % (621416)ott-21_1_sil=16000:fs=off:random_seed=3054475272:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.99/1.53 % (621411)Instruction limit reached!
% 6.99/1.53 % (621411)------------------------------
% 6.99/1.53 % (621411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.53 % (621411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.53 % (621411)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621411)Termination reason: Instruction limit
% 14.71/2.73 % (621411)Termination phase: Saturation
% 14.71/2.73 % (621411)Time elapsed: 0.053 s
% 14.71/2.73 % (621411)Peak memory usage: 12 MB
% 14.71/2.73 % (621411)Instructions burned: 133 (million)
% 14.71/2.73 % (621418)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3981632923:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 14.71/2.73 % (621416)Instruction limit reached!
% 14.71/2.73 % (621416)------------------------------
% 14.71/2.73 % (621416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621416)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621416)Termination reason: Instruction limit
% 14.71/2.73 % (621416)Termination phase: Saturation
% 14.71/2.73 % (621416)Time elapsed: 0.095 s
% 14.71/2.73 % (621416)Peak memory usage: 14 MB
% 14.71/2.73 % (621416)Instructions burned: 181 (million)
% 14.71/2.73 % (621420)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3540988271:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 14.71/2.73 % TRYING [1]
% 14.71/2.73 % (621410)Instruction limit reached!
% 14.71/2.73 % (621410)------------------------------
% 14.71/2.73 % (621410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621410)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621410)Termination reason: Instruction limit
% 14.71/2.73 % (621410)Termination phase: Finite model building constraint generation
% 14.71/2.73 % (621410)Time elapsed: 0.246 s
% 14.71/2.73 % (621410)Peak memory usage: 35 MB
% 14.71/2.73 % (621410)Instructions burned: 717 (million)
% 14.71/2.73 % (621422)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4149664900:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 14.71/2.73 % (621418)Instruction limit reached!
% 14.71/2.73 % (621418)------------------------------
% 14.71/2.73 % (621418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621418)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621418)Termination reason: Instruction limit
% 14.71/2.73 % (621418)Termination phase: Saturation
% 14.71/2.73 % (621418)Time elapsed: 0.302 s
% 14.71/2.73 % (621418)Peak memory usage: 15 MB
% 14.71/2.73 % (621418)Instructions burned: 478 (million)
% 14.71/2.73 % (621412)Instruction limit reached!
% 14.71/2.73 % (621412)------------------------------
% 14.71/2.73 % (621412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621412)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621412)Termination reason: Instruction limit
% 14.71/2.73 % (621412)Termination phase: Saturation
% 14.71/2.73 % (621412)Time elapsed: 0.378 s
% 14.71/2.73 % (621412)Peak memory usage: 21 MB
% 14.71/2.73 % (621412)Instructions burned: 684 (million)
% 14.71/2.73 % (621424)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3512430430:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 14.71/2.73 % (621425)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=3840919265:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 14.71/2.73 % (621424)Cannot represent all propositional literals internally
% 14.71/2.73 % (621424)Refutation not found, incomplete strategy
% 14.71/2.73 % (621424)------------------------------
% 14.71/2.73 % (621424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621424)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621424)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.73 % (621424)Time elapsed: 0.028 s
% 14.71/2.73 % (621424)Peak memory usage: 12 MB
% 14.71/2.73 % (621424)Instructions burned: 58 (million)
% 14.71/2.73 % (621424)------------------------------
% 14.71/2.73 % (621424)------------------------------
% 14.71/2.73 % (621428)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2904603352:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 14.71/2.73 % (621420)Instruction limit reached!
% 14.71/2.73 % (621420)------------------------------
% 14.71/2.73 % (621420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621420)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621420)Termination reason: Instruction limit
% 14.71/2.73 % (621420)Termination phase: Finite model building constraint generation
% 14.71/2.73 % (621420)Time elapsed: 0.398 s
% 14.71/2.73 % (621420)Peak memory usage: 100 MB
% 14.71/2.73 % (621420)Instructions burned: 866 (million)
% 14.71/2.73 % (621430)fmb+10_1_sil=64000:random_seed=962813941:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 14.71/2.73 % TRYING [1]
% 14.71/2.73 % (621425)Instruction limit reached!
% 14.71/2.73 % (621425)------------------------------
% 14.71/2.73 % (621425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621425)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621425)Termination reason: Instruction limit
% 14.71/2.73 % (621425)Termination phase: Saturation
% 14.71/2.73 % (621425)Time elapsed: 0.369 s
% 14.71/2.73 % (621425)Peak memory usage: 24 MB
% 14.71/2.73 % (621425)Instructions burned: 693 (million)
% 14.71/2.73 % (621432)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=543398207:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 14.71/2.73 % (621432)Cannot represent all propositional literals internally
% 14.71/2.73 % (621432)Refutation not found, incomplete strategy
% 14.71/2.73 % (621432)------------------------------
% 14.71/2.73 % (621432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621432)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621432)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.73 % (621432)Time elapsed: 0.028 s
% 14.71/2.73 % (621432)Peak memory usage: 12 MB
% 14.71/2.73 % (621432)Instructions burned: 58 (million)
% 14.71/2.73 % (621432)------------------------------
% 14.71/2.73 % (621432)------------------------------
% 14.71/2.73 % (621434)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3509357824:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 14.71/2.73 % (621434)Cannot represent all propositional literals internally
% 14.71/2.73 % (621434)Refutation not found, incomplete strategy
% 14.71/2.73 % (621434)------------------------------
% 14.71/2.73 % (621434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621434)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621434)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.73 % (621434)Time elapsed: 0.028 s
% 14.71/2.73 % (621434)Peak memory usage: 12 MB
% 14.71/2.73 % (621434)Instructions burned: 58 (million)
% 14.71/2.73 % (621434)------------------------------
% 14.71/2.73 % (621434)------------------------------
% 14.71/2.73 % (621422)Instruction limit reached!
% 14.71/2.73 % (621422)------------------------------
% 14.71/2.73 % (621422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621422)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621422)Termination reason: Instruction limit
% 14.71/2.73 % (621422)Termination phase: Saturation
% 14.71/2.73 % (621422)Time elapsed: 0.622 s
% 14.71/2.73 % (621422)Peak memory usage: 26 MB
% 14.71/2.73 % (621422)Instructions burned: 1179 (million)
% 14.71/2.73 % (621436)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=711655217:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 14.71/2.73 % (621438)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1767771845:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 14.71/2.73 % (621428)Instruction limit reached!
% 14.71/2.73 % (621428)------------------------------
% 14.71/2.73 % (621428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621428)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621428)Termination reason: Instruction limit
% 14.71/2.73 % (621428)Termination phase: Saturation
% 14.71/2.73 % (621428)Time elapsed: 0.477 s
% 14.71/2.73 % (621428)Peak memory usage: 20 MB
% 14.71/2.73 % (621428)Instructions burned: 879 (million)
% 14.71/2.73 % (621440)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=55382932:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 14.71/2.73 % (621440)Cannot represent all propositional literals internally
% 14.71/2.73 % (621440)Refutation not found, incomplete strategy
% 14.71/2.73 % (621440)------------------------------
% 14.71/2.73 % (621440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621440)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621440)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.73 % (621440)Time elapsed: 0.039 s
% 14.71/2.73 % (621440)Peak memory usage: 12 MB
% 14.71/2.73 % (621440)Instructions burned: 83 (million)
% 14.71/2.73 % (621440)------------------------------
% 14.71/2.73 % (621440)------------------------------
% 14.71/2.73 % (621442)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=148967300:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi)
% 14.71/2.73 % TRYING [2]
% 14.71/2.73 % (621442)Cannot represent all propositional literals internally
% 14.71/2.73 % (621442)Refutation not found, incomplete strategy
% 14.71/2.73 % (621442)------------------------------
% 14.71/2.73 % (621442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621442)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621442)Termination reason: Refutation not found, incomplete strategy
% 14.71/2.73 % (621442)Time elapsed: 0.028 s
% 14.71/2.73 % (621442)Peak memory usage: 12 MB
% 14.71/2.73 % (621442)Instructions burned: 59 (million)
% 14.71/2.73 % (621442)------------------------------
% 14.71/2.73 % (621442)------------------------------
% 14.71/2.73 % (621444)ott-2_1_sil=16000:newcnf=on:random_seed=2515144779:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 14.71/2.73 % (621444)Instruction limit reached!
% 14.71/2.73 % (621444)------------------------------
% 14.71/2.73 % (621444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621444)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621444)Termination reason: Instruction limit
% 14.71/2.73 % (621444)Termination phase: Saturation
% 14.71/2.73 % (621444)Time elapsed: 0.404 s
% 14.71/2.73 % (621444)Peak memory usage: 15 MB
% 14.71/2.73 % (621444)Instructions burned: 870 (million)
% 14.71/2.73 % (621446)ott+10_1_sil=32000:tgt=ground:random_seed=1662029997:i=5114:av=off_2984 on theBenchmark for (2984ds/5114Mi)
% 14.71/2.73 % (621438)Instruction limit reached!
% 14.71/2.73 % (621438)------------------------------
% 14.71/2.73 % (621438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621438)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621438)Termination reason: Instruction limit
% 14.71/2.73 % (621438)Termination phase: Saturation
% 14.71/2.73 % (621438)Time elapsed: 0.601 s
% 14.71/2.73 % (621438)Peak memory usage: 17 MB
% 14.71/2.73 % (621438)Instructions burned: 1474 (million)
% 14.71/2.73 % (621448)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1976177536:i=54282_2983 on theBenchmark for (2983ds/54282Mi)
% 14.71/2.73 % TRYING [1]
% 14.71/2.73 % TRYING [2]
% 14.71/2.73 % (621446) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-621391-621446"...
% 14.71/2.73 % (621446)...printing done.
% 14.71/2.73 % (621446)Refutation found. Thanks to Tanya!
% 14.71/2.73 % SZS status Theorem for theBenchmark
% 14.71/2.73 % SZS output start Proof for theBenchmark
% See solution above
% 14.71/2.73 % (621446)------------------------------
% 14.71/2.73 % (621446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.71/2.73 % (621446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/2.73 % (621446)CaDiCaL version: 2.1.3
% 14.71/2.73 % (621446)Termination reason: Refutation
% 14.71/2.73 % (621446)Time elapsed: 0.664 s
% 14.71/2.73 % (621446)Peak memory usage: 25 MB
% 14.71/2.73 % (621446)Instructions burned: 1221 (million)
% 14.71/2.73 % (621391)Success in time 2.302 s
% 14.71/2.73 % Vampire exiting
%------------------------------------------------------------------------------