%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:42:29 AM UTC 2026
% Result : Theorem 13.10s 2.64s
% Output : Refutation 13.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 14
% Syntax : Number of formulae : 55 ( 13 unt; 0 def)
% Number of atoms : 97 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 79 ( 37 ~; 30 |; 1 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 57 ( 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] :
~ ( intangible(X0)
& partiallytangible(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_3) ).
fof(f9,axiom,
! [X0] :
( inanimateobject(X0)
=> partiallytangible(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_9) ).
fof(f112,axiom,
! [X0] :
( setorcollection(X0)
=> mathematicalthing(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_112) ).
fof(f132,axiom,
! [X0] :
( mathematicalorcomputationalthing(X0)
=> intangible(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_132) ).
fof(f180,axiom,
! [X0] :
( mathematicalthing(X0)
=> mathematicalorcomputationalthing(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_180) ).
fof(f196,axiom,
! [X0] :
( inanimateobject_nonnatural(X0)
=> inanimateobject(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_196) ).
fof(f211,axiom,
! [X0] :
( artifact(X0)
=> inanimateobject_nonnatural(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_211) ).
fof(f413,axiom,
! [X0,X1] :
( genls(X0,X1)
=> subsetof(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_413) ).
fof(f494,axiom,
! [X0] :
( computerdataartifact(X0)
=> artifact(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_494) ).
fof(f1059,axiom,
! [X0,X1] :
( subsetof(X0,X1)
=> setorcollection(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1059) ).
fof(f1085,axiom,
! [X0] : computerdataartifact(f_urlreferentfn(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1085) ).
fof(f1110,axiom,
! [X0] :
( collection(X0)
=> genls(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1110) ).
fof(f1119,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> collection(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1119) ).
fof(f1132,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query113) ).
fof(f1133,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1134,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(flattening,[],[f1133]) ).
fof(f1228,plain,
! [X0,X1] :
( collection(X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f1119]) ).
fof(f1242,plain,
! [X0] :
( genls(X0,X0)
| ~ collection(X0) ),
inference(ennf_transformation,[],[f1110]) ).
fof(f1296,plain,
! [X0] :
( artifact(X0)
| ~ computerdataartifact(X0) ),
inference(ennf_transformation,[],[f494]) ).
fof(f1345,plain,
! [X0,X1] :
( setorcollection(X1)
| ~ subsetof(X0,X1) ),
inference(ennf_transformation,[],[f1059]) ).
fof(f1352,plain,
! [X0,X1] :
( subsetof(X0,X1)
| ~ genls(X0,X1) ),
inference(ennf_transformation,[],[f413]) ).
fof(f1370,plain,
! [X0] :
( intangible(X0)
| ~ mathematicalorcomputationalthing(X0) ),
inference(ennf_transformation,[],[f132]) ).
fof(f1371,plain,
! [X0] :
( ~ intangible(X0)
| ~ partiallytangible(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f1377,plain,
! [X0] :
( partiallytangible(X0)
| ~ inanimateobject(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f1405,plain,
! [X0] :
( inanimateobject_nonnatural(X0)
| ~ artifact(X0) ),
inference(ennf_transformation,[],[f211]) ).
fof(f1441,plain,
! [X0] :
( mathematicalorcomputationalthing(X0)
| ~ mathematicalthing(X0) ),
inference(ennf_transformation,[],[f180]) ).
fof(f1442,plain,
! [X0] :
( mathematicalthing(X0)
| ~ setorcollection(X0) ),
inference(ennf_transformation,[],[f112]) ).
fof(f1470,plain,
! [X0] :
( inanimateobject(X0)
| ~ inanimateobject_nonnatural(X0) ),
inference(ennf_transformation,[],[f196]) ).
fof(f1961,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf_transformation,[],[f1134]) ).
fof(f1965,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| collection(X0) ),
inference(cnf_transformation,[],[f1228]) ).
fof(f1986,plain,
! [X0] : computerdataartifact(f_urlreferentfn(X0)),
inference(cnf_transformation,[],[f1085]) ).
fof(f1992,plain,
! [X0] :
( genls(X0,X0)
| ~ collection(X0) ),
inference(cnf_transformation,[],[f1242]) ).
fof(f2066,plain,
! [X0] :
( artifact(X0)
| ~ computerdataartifact(X0) ),
inference(cnf_transformation,[],[f1296]) ).
fof(f2117,plain,
! [X0,X1] :
( ~ subsetof(X0,X1)
| setorcollection(X1) ),
inference(cnf_transformation,[],[f1345]) ).
fof(f2121,plain,
! [X0,X1] :
( subsetof(X0,X1)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[],[f1352]) ).
fof(f2145,plain,
! [X0] :
( ~ mathematicalorcomputationalthing(X0)
| intangible(X0) ),
inference(cnf_transformation,[],[f1370]) ).
fof(f2146,plain,
! [X0] :
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[],[f1371]) ).
fof(f2152,plain,
! [X0] :
( ~ inanimateobject(X0)
| partiallytangible(X0) ),
inference(cnf_transformation,[],[f1377]) ).
fof(f2187,plain,
! [X0] :
( ~ artifact(X0)
| inanimateobject_nonnatural(X0) ),
inference(cnf_transformation,[],[f1405]) ).
fof(f2235,plain,
! [X0] :
( mathematicalorcomputationalthing(X0)
| ~ mathematicalthing(X0) ),
inference(cnf_transformation,[],[f1441]) ).
fof(f2236,plain,
! [X0] :
( mathematicalthing(X0)
| ~ setorcollection(X0) ),
inference(cnf_transformation,[],[f1442]) ).
fof(f2263,plain,
! [X0] :
( ~ inanimateobject_nonnatural(X0)
| inanimateobject(X0) ),
inference(cnf_transformation,[],[f1470]) ).
fof(f3243,plain,
collection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolution,[],[f1965,f1961]) ).
fof(f4362,plain,
! [X0] :
( ~ mathematicalthing(X0)
| intangible(X0) ),
inference(resolution,[],[f2145,f2235]) ).
fof(f4391,plain,
! [X0,X1] :
( ~ genls(X1,X0)
| setorcollection(X0) ),
inference(resolution,[],[f2117,f2121]) ).
fof(f4393,plain,
! [X0] :
( ~ collection(X0)
| setorcollection(X0) ),
inference(resolution,[],[f4391,f1992]) ).
fof(f4635,plain,
! [X0] :
( inanimateobject_nonnatural(X0)
| ~ computerdataartifact(X0) ),
inference(resolution,[],[f2187,f2066]) ).
fof(f4687,plain,
! [X0] :
( ~ computerdataartifact(X0)
| inanimateobject(X0) ),
inference(resolution,[],[f2263,f4635]) ).
fof(f4688,plain,
! [X0] : inanimateobject(f_urlreferentfn(X0)),
inference(resolution,[],[f4687,f1986]) ).
fof(f4689,plain,
! [X0] : partiallytangible(f_urlreferentfn(X0)),
inference(resolution,[],[f4688,f2152]) ).
fof(f4690,plain,
! [X0] : ~ intangible(f_urlreferentfn(X0)),
inference(resolution,[],[f4689,f2146]) ).
fof(f5046,plain,
setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolution,[],[f4393,f3243]) ).
fof(f6091,plain,
! [X0] :
( ~ setorcollection(X0)
| intangible(X0) ),
inference(resolution,[],[f2236,f4362]) ).
fof(f6093,plain,
intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolution,[],[f6091,f5046]) ).
fof(f6094,plain,
$false,
inference(forward_subsumption_resolution,[],[f6093,f4690]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR063+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 22:24:13 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.98/2.11 % (2101799)Detected formulas, will run a generic FOF schedule.
% 9.98/2.11 % (2101814)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2518388210:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.98/2.11 % (2101814)Refutation not found, incomplete strategy
% 9.98/2.11 % (2101814)------------------------------
% 9.98/2.11 % (2101814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.11 % (2101814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.11 % (2101814)CaDiCaL version: 2.1.3
% 9.98/2.11 % (2101814)Termination reason: Refutation not found, incomplete strategy
% 9.98/2.11 % (2101814)Time elapsed: 0.002 s
% 9.98/2.11 % (2101814)Peak memory usage: 88 MB
% 9.98/2.11 % (2101814)Instructions burned: 3 (million)
% 9.98/2.11 % (2101813)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=3788830982:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.98/2.11 % (2101812)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=4259910140:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.98/2.11 % (2101816)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3174140539:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.98/2.11 % (2101817)dis-21_1_sil=8000:lcm=predicate:random_seed=2744974394:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.98/2.11 % (2101815)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2115458974:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.98/2.11 % (2101811)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=1390093822:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.98/2.11 % (2101815)Instruction limit reached!
% 9.98/2.11 % (2101815)------------------------------
% 9.98/2.11 % (2101815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.11 % (2101815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.11 % (2101815)CaDiCaL version: 2.1.3
% 9.98/2.11 % (2101815)Termination reason: Instruction limit
% 9.98/2.11 % (2101815)Termination phase: Saturation
% 9.98/2.11 % (2101815)Time elapsed: 0.046 s
% 9.98/2.11 % (2101815)Peak memory usage: 88 MB
% 9.98/2.11 % (2101815)Instructions burned: 121 (million)
% 9.98/2.11 % (2101817)Instruction limit reached!
% 9.98/2.11 % (2101817)------------------------------
% 9.98/2.11 % (2101817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.11 % (2101817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.11 % (2101817)CaDiCaL version: 2.1.3
% 9.98/2.11 % (2101817)Termination reason: Instruction limit
% 9.98/2.11 % (2101817)Termination phase: Saturation
% 9.98/2.11 % (2101817)Time elapsed: 0.074 s
% 9.98/2.11 % (2101817)Peak memory usage: 91 MB
% 9.98/2.11 % (2101817)Instructions burned: 131 (million)
% 9.98/2.11 % (2101816)Instruction limit reached!
% 9.98/2.11 % (2101816)------------------------------
% 9.98/2.11 % (2101816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.11 % (2101816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.11 % (2101816)CaDiCaL version: 2.1.3
% 9.98/2.11 % (2101816)Termination reason: Instruction limit
% 9.98/2.11 % (2101816)Termination phase: Saturation
% 9.98/2.11 % (2101816)Time elapsed: 0.077 s
% 9.98/2.11 % (2101816)Peak memory usage: 90 MB
% 9.98/2.11 % (2101816)Instructions burned: 140 (million)
% 9.98/2.11 % (2101814)------------------------------
% 9.98/2.11 % (2101814)------------------------------
% 9.98/2.11 % (2101825)lrs+10_1_sil=8000:sp=occurrence:random_seed=2459515508:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.98/2.11 % (2101825)Refutation not found, incomplete strategy
% 9.98/2.11 % (2101825)------------------------------
% 9.98/2.11 % (2101825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.98/2.11 % (2101825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.98/2.11 % (2101825)CaDiCaL version: 2.1.3
% 9.98/2.11 % (2101825)Termination reason: Refutation not found, incomplete strategy
% 9.98/2.11 % (2101825)Time elapsed: 0.005 s
% 12.07/2.44 % (2101825)Peak memory usage: 89 MB
% 12.07/2.44 % (2101825)Instructions burned: 4 (million)
% 12.07/2.44 % (2101827)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3445015481:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.07/2.44 % (2101826)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3630189245:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.07/2.44 % (2101827)Refutation not found, incomplete strategy
% 12.07/2.44 % (2101827)------------------------------
% 12.07/2.44 % (2101827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101827)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101827)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.44 % (2101827)Time elapsed: 0.003 s
% 12.07/2.44 % (2101827)Peak memory usage: 88 MB
% 12.07/2.44 % (2101827)Instructions burned: 3 (million)
% 12.07/2.44 % (2101826)Refutation not found, incomplete strategy
% 12.07/2.44 % (2101826)------------------------------
% 12.07/2.44 % (2101826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101826)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101826)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.44 % (2101826)Time elapsed: 0.005 s
% 12.07/2.44 % (2101826)Peak memory usage: 89 MB
% 12.07/2.44 % (2101826)Instructions burned: 7 (million)
% 12.07/2.44 % (2101828)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=2074917471:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.07/2.44 % (2101828)Instruction limit reached!
% 12.07/2.44 % (2101828)------------------------------
% 12.07/2.44 % (2101828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101828)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101828)Termination reason: Instruction limit
% 12.07/2.44 % (2101828)Termination phase: Saturation
% 12.07/2.44 % (2101828)Time elapsed: 0.072 s
% 12.07/2.44 % (2101828)Peak memory usage: 91 MB
% 12.07/2.44 % (2101828)Instructions burned: 250 (million)
% 12.07/2.44 % (2101833)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=337411710:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 12.07/2.44 % (2101833)Refutation not found, incomplete strategy
% 12.07/2.44 % (2101833)------------------------------
% 12.07/2.44 % (2101833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101833)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101833)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.44 % (2101833)Time elapsed: 0.003 s
% 12.07/2.44 % (2101833)Peak memory usage: 88 MB
% 12.07/2.44 % (2101833)Instructions burned: 6 (million)
% 12.07/2.44 % (2101825)------------------------------
% 12.07/2.44 % (2101825)------------------------------
% 12.07/2.44 % (2101827)------------------------------
% 12.07/2.44 % (2101827)------------------------------
% 12.07/2.44 % (2101826)------------------------------
% 12.07/2.44 % (2101826)------------------------------
% 12.07/2.44 % (2101833)------------------------------
% 12.07/2.44 % (2101833)------------------------------
% 12.07/2.44 % (2101835)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=597591586:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 12.07/2.44 % (2101813)Refutation not found, incomplete strategy
% 12.07/2.44 % (2101813)------------------------------
% 12.07/2.44 % (2101813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101813)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101813)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.44 % (2101813)Time elapsed: 0.618 s
% 12.07/2.44 % (2101813)Peak memory usage: 130 MB
% 12.07/2.44 % (2101813)Instructions burned: 914 (million)
% 12.07/2.44 % (2101837)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1422165230:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 12.07/2.44 % (2101836)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3907670439:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 12.07/2.44 % (2101836)Instruction limit reached!
% 12.07/2.44 % (2101836)------------------------------
% 12.07/2.44 % (2101836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101836)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101836)Termination reason: Instruction limit
% 12.07/2.44 % (2101836)Termination phase: Saturation
% 12.07/2.44 % (2101836)Time elapsed: 0.054 s
% 12.07/2.44 % (2101836)Peak memory usage: 89 MB
% 12.07/2.44 % (2101836)Instructions burned: 115 (million)
% 12.07/2.44 % (2101837)Instruction limit reached!
% 12.07/2.44 % (2101837)------------------------------
% 12.07/2.44 % (2101837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.44 % (2101837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.44 % (2101837)CaDiCaL version: 2.1.3
% 12.07/2.44 % (2101837)Termination reason: Instruction limit
% 12.07/2.44 % (2101837)Termination phase: Saturation
% 12.07/2.44 % (2101837)Time elapsed: 0.063 s
% 12.07/2.44 % (2101837)Peak memory usage: 90 MB
% 12.07/2.44 % (2101837)Instructions burned: 127 (million)
% 12.07/2.45 % (2101838)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2464775439:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 12.07/2.45 % (2101838)Instruction limit reached!
% 12.07/2.45 % (2101838)------------------------------
% 12.07/2.45 % (2101838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.45 % (2101838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.45 % (2101838)CaDiCaL version: 2.1.3
% 12.07/2.45 % (2101838)Termination reason: Instruction limit
% 12.07/2.45 % (2101838)Termination phase: Saturation
% 12.07/2.45 % (2101838)Time elapsed: 0.034 s
% 12.07/2.45 % (2101838)Peak memory usage: 90 MB
% 12.07/2.45 % (2101838)Instructions burned: 118 (million)
% 12.07/2.45 % (2101842)lrs+10_1_sil=8000:sp=occurrence:random_seed=2559927976:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 12.07/2.45 % (2101843)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2439414304:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 12.07/2.45 % (2101843)Refutation not found, incomplete strategy
% 12.07/2.45 % (2101843)------------------------------
% 12.07/2.45 % (2101843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.45 % (2101843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.45 % (2101843)CaDiCaL version: 2.1.3
% 12.07/2.45 % (2101843)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.45 % (2101843)Time elapsed: 0.003 s
% 12.07/2.45 % (2101843)Peak memory usage: 88 MB
% 12.07/2.45 % (2101843)Instructions burned: 2 (million)
% 12.07/2.45 % (2101813)------------------------------
% 12.07/2.45 % (2101813)------------------------------
% 12.07/2.45 % (2101845)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=365594695:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 12.07/2.45 % (2101849)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2970518412:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 12.07/2.45 % (2101849)Refutation not found, incomplete strategy
% 12.07/2.45 % (2101849)------------------------------
% 12.07/2.45 % (2101849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.45 % (2101849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.45 % (2101849)CaDiCaL version: 2.1.3
% 12.07/2.45 % (2101849)Termination reason: Refutation not found, incomplete strategy
% 12.07/2.45 % (2101849)Time elapsed: 0.004 s
% 12.07/2.45 % (2101849)Peak memory usage: 89 MB
% 12.07/2.45 % (2101849)Instructions burned: 4 (million)
% 12.07/2.45 % (2101843)------------------------------
% 12.07/2.45 % (2101843)------------------------------
% 12.07/2.45 % (2101842)Instruction limit reached!
% 12.07/2.45 % (2101842)------------------------------
% 12.07/2.45 % (2101842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.07/2.45 % (2101842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.07/2.45 % (2101842)CaDiCaL version: 2.1.3
% 12.07/2.45 % (2101842)Termination reason: Instruction limit
% 12.07/2.45 % (2101842)Termination phase: Saturation
% 12.07/2.45 % (2101842)Time elapsed: 0.419 s
% 12.07/2.45 % (2101842)Peak memory usage: 114 MB
% 12.07/2.45 % (2101842)Instructions burned: 908 (million)
% 13.10/2.64 % (2101851)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2143853063:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 13.10/2.64 % (2101851)Refutation not found, incomplete strategy
% 13.10/2.64 % (2101851)------------------------------
% 13.10/2.64 % (2101851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.64 % (2101851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.64 % (2101851)CaDiCaL version: 2.1.3
% 13.10/2.64 % (2101851)Termination reason: Refutation not found, incomplete strategy
% 13.10/2.64 % (2101851)Time elapsed: 0.006 s
% 13.10/2.64 % (2101851)Peak memory usage: 88 MB
% 13.10/2.64 % (2101851)Instructions burned: 9 (million)
% 13.10/2.64 % (2101849)------------------------------
% 13.10/2.64 % (2101849)------------------------------
% 13.10/2.64 % (2101845)First to succeed.
% 13.10/2.64 % (2101845)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2101799"
% 13.10/2.64 % (2101853)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=214590882:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 13.10/2.64 % (2101854)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=4044380933:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 13.10/2.64 % (2101851)------------------------------
% 13.10/2.64 % (2101851)------------------------------
% 13.10/2.64 % (2101854)Instruction limit reached!
% 13.10/2.64 % (2101854)------------------------------
% 13.10/2.64 % (2101854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.64 % (2101854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.64 % (2101854)CaDiCaL version: 2.1.3
% 13.10/2.64 % (2101854)Termination reason: Instruction limit
% 13.10/2.64 % (2101854)Termination phase: Saturation
% 13.10/2.64 % (2101854)Time elapsed: 0.076 s
% 13.10/2.64 % (2101854)Peak memory usage: 91 MB
% 13.10/2.64 % (2101854)Instructions burned: 125 (million)
% 13.10/2.64 % (2101845)Refutation found. Thanks to Tanya!
% 13.10/2.64 % SZS status Theorem for theBenchmark
% 13.10/2.64 % SZS output start Proof for theBenchmark
% See solution above
% 13.10/2.64 % (2101845)------------------------------
% 13.10/2.64 % (2101845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.64 % (2101845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.64 % (2101845)CaDiCaL version: 2.1.3
% 13.10/2.64 % (2101845)Termination reason: Refutation
% 13.10/2.64 % (2101845)Time elapsed: 0.550 s
% 13.10/2.64 % (2101845)Peak memory usage: 139 MB
% 13.10/2.64 % (2101845)Instructions burned: 1544 (million)
% 13.10/2.64 % (2101845)------------------------------
% 13.10/2.64 % (2101845)------------------------------
% 13.10/2.64 % (2101799)Success in time 1.776 s
% 13.10/2.64 % Vampire exiting
%------------------------------------------------------------------------------