%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB087+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 01:00:55 PM UTC 2026
% Result : Theorem 14.53s 6.08s
% Output : Refutation 14.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 33 ( 13 unt; 2 def)
% Number of atoms : 71 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 71 ( 33 ~; 26 |; 5 &)
% ( 6 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0,X1] :
( iext(uri_rdf_type,X0,X1)
<=> icext(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax',rdfs_cext_def) ).
fof(f314,axiom,
! [X0,X1,X2] :
( ( iext(uri_owl_hasSelf,X0,X2)
& iext(uri_owl_onProperty,X0,X1) )
=> ! [X3] :
( icext(X0,X3)
<=> iext(X1,X3,X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB001+0.ax',owl_restrict_hasself) ).
fof(f559,conjecture,
iext(uri_rdf_type,uri_ex_w,uri_ex_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conclusion_rdfbased_sem_restrict_hasself_inst_subj) ).
fof(f560,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_z),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
( iext(uri_owl_hasSelf,uri_ex_z,literal_typed(dat_str_true,uri_xsd_boolean))
& iext(uri_owl_onProperty,uri_ex_z,uri_ex_p)
& iext(uri_ex_p,uri_ex_w,uri_ex_w) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_rdfbased_sem_restrict_hasself_inst_subj) ).
fof(f572,plain,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_z),
inference(flattening,[],[f560]) ).
fof(f735,plain,
! [X0,X1,X2] :
( ! [X3] :
( icext(X0,X3)
<=> iext(X1,X3,X3) )
| ~ iext(uri_owl_hasSelf,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1) ),
inference(ennf_transformation,[],[f314]) ).
fof(f736,plain,
! [X0,X1,X2] :
( ! [X3] :
( icext(X0,X3)
<=> iext(X1,X3,X3) )
| ~ iext(uri_owl_hasSelf,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1) ),
inference(flattening,[],[f735]) ).
fof(f1236,plain,
! [X0,X1] :
( ( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) )
& ( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f1479,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( icext(X0,X3)
| ~ iext(X1,X3,X3) )
& ( iext(X1,X3,X3)
| ~ icext(X0,X3) ) )
| ~ iext(uri_owl_hasSelf,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1) ),
inference(nnf_transformation,[],[f736]) ).
fof(f1852,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[],[f1236]) ).
fof(f2551,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(X1,X3,X3)
| ~ iext(uri_owl_hasSelf,X0,X2)
| icext(X0,X3) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f3286,plain,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_z),
inference(cnf_transformation,[],[f572]) ).
fof(f3287,plain,
iext(uri_ex_p,uri_ex_w,uri_ex_w),
inference(cnf_transformation,[],[f561]) ).
fof(f3288,plain,
iext(uri_owl_onProperty,uri_ex_z,uri_ex_p),
inference(cnf_transformation,[],[f561]) ).
fof(f3289,plain,
iext(uri_owl_hasSelf,uri_ex_z,literal_typed(dat_str_true,uri_xsd_boolean)),
inference(cnf_transformation,[],[f561]) ).
fof(f3483,definition,
( spl373_1
<=> ! [X1] : ~ iext(uri_owl_hasSelf,uri_ex_z,X1) ),
introduced(definition,[new_symbols(definition,[spl373_1])],[avatar_definition]) ).
fof(f3484,plain,
( ! [X1] : ~ iext(uri_owl_hasSelf,uri_ex_z,X1)
| ~ spl373_1 ),
inference(avatar_component_clause,[],[f3483]) ).
fof(f3489,plain,
! [X0,X1] :
( ~ iext(uri_ex_p,X0,X0)
| ~ iext(uri_owl_hasSelf,uri_ex_z,X1)
| icext(uri_ex_z,X0) ),
inference(resolution,[],[f2551,f3288]) ).
fof(f3491,definition,
( spl373_3
<=> ! [X0] :
( ~ iext(uri_ex_p,X0,X0)
| icext(uri_ex_z,X0) ) ),
introduced(definition,[new_symbols(definition,[spl373_3])],[avatar_definition]) ).
fof(f3492,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,X0)
| icext(uri_ex_z,X0) )
| ~ spl373_3 ),
inference(avatar_component_clause,[],[f3491]) ).
fof(f3493,plain,
( spl373_1
| spl373_3 ),
inference(avatar_split_clause,[],[f3489,f3491,f3483]) ).
fof(f3545,plain,
( $false
| ~ spl373_1 ),
inference(resolution,[],[f3484,f3289]) ).
fof(f3546,plain,
~ spl373_1,
inference(avatar_contradiction_clause,[],[f3545]) ).
fof(f3932,plain,
( icext(uri_ex_z,uri_ex_w)
| ~ spl373_3 ),
inference(resolution,[],[f3492,f3287]) ).
fof(f3940,plain,
( iext(uri_rdf_type,uri_ex_w,uri_ex_z)
| ~ spl373_3 ),
inference(resolution,[],[f3932,f1852]) ).
fof(f3943,plain,
( $false
| ~ spl373_3 ),
inference(global_subsumption,[],[f3940,f3286]) ).
fof(f3944,plain,
~ spl373_3,
inference(avatar_contradiction_clause,[],[f3943]) ).
cnf(s1508,plain,
( spl373_1
| spl373_3 ),
inference(sat_conversion,[],[f3493]) ).
cnf(s1519,plain,
~ spl373_1,
inference(sat_conversion,[],[f3546]) ).
cnf(s1637,plain,
~ spl373_3,
inference(sat_conversion,[],[f3944]) ).
cnf(s1638,plain,
$false,
inference(rat,[],[s1508,s1637,s1519]) ).
fof(f3945,plain,
$false,
inference(avatar_sat_refutation,[],[s1638]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB087+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n004.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 07:17:52 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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
% 15.26/2.67 % (173535)Will run a generic schedule for satisfiability detection.
% 15.26/2.67 % (173544)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=529637678:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.26/2.67 % (173541)% WARNING: option uhcvi not known.
% 15.26/2.67 % (173541)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4217130160:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.26/2.67 % (173540)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3846780639_2999 on theBenchmark for (2999ds/0Mi)
% 15.26/2.67 % (173545)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2628916208:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.26/2.67 % (173542)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4228213452:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.26/2.67 % (173543)dis+10_1_sil=32000:sp=arity:random_seed=2102859395:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.26/2.67 % (173546)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2773765221:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.26/2.67 % (173544)Instruction limit reached!
% 15.26/2.67 % (173544)------------------------------
% 15.26/2.67 % (173544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.26/2.67 % (173544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/2.67 % (173544)CaDiCaL version: 2.1.3
% 15.26/2.67 % (173544)Termination reason: Instruction limit
% 15.26/2.67 % (173544)Termination phase: Saturation
% 15.26/2.67 % (173544)Time elapsed: 0.031 s
% 15.26/2.67 % (173544)Peak memory usage: 13 MB
% 15.26/2.67 % (173544)Instructions burned: 119 (million)
% 15.26/2.67 % (173554)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3102447347:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.26/2.67 % (173543)Instruction limit reached!
% 15.26/2.67 % (173543)------------------------------
% 15.26/2.67 % (173543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.26/2.67 % (173543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/2.67 % (173543)CaDiCaL version: 2.1.3
% 15.26/2.67 % (173543)Termination reason: Instruction limit
% 15.26/2.67 % (173543)Termination phase: Saturation
% 15.26/2.67 % (173543)Time elapsed: 0.057 s
% 15.26/2.67 % (173543)Peak memory usage: 14 MB
% 15.26/2.67 % (173543)Instructions burned: 109 (million)
% 15.26/2.67 % (173545)Instruction limit reached!
% 15.26/2.67 % (173545)------------------------------
% 15.26/2.67 % (173545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.26/2.67 % (173545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/2.67 % (173545)CaDiCaL version: 2.1.3
% 15.26/2.67 % (173545)Termination reason: Instruction limit
% 15.26/2.67 % (173545)Termination phase: Saturation
% 15.26/2.67 % (173545)Time elapsed: 0.067 s
% 15.26/2.67 % (173545)Peak memory usage: 14 MB
% 15.26/2.67 % (173545)Instructions burned: 131 (million)
% 15.26/2.67 % (173556)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2601581191:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.26/2.67 % TRYING [1]
% 15.26/2.67 % TRYING [2]
% 15.26/2.67 % (173546)Instruction limit reached!
% 15.26/2.67 % (173546)------------------------------
% 15.26/2.67 % (173546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.26/2.67 % (173546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/2.67 % (173546)CaDiCaL version: 2.1.3
% 15.26/2.67 % (173546)Termination reason: Instruction limit
% 15.26/2.67 % (173546)Termination phase: Saturation
% 15.26/2.67 % (173546)Time elapsed: 0.083 s
% 15.26/2.67 % (173546)Peak memory usage: 16 MB
% 15.26/2.67 % (173546)Instructions burned: 159 (million)
% 15.26/2.67 % (173557)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=75891872:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.26/2.67 % (173559)ott-21_1_sil=16000:fs=off:random_seed=139735196:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.26/2.67 % TRYING [3]
% 15.26/2.67 % TRYING [1]
% 15.26/2.67 % TRYING [2]
% 15.26/2.67 % (173556)Instruction limit reached!
% 15.26/2.67 % (173556)------------------------------
% 15.26/2.67 % (173556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.26/2.67 % (173556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.26/2.67 % (173556)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173556)Termination reason: Instruction limit
% 38.37/5.92 % (173556)Termination phase: Saturation
% 38.37/5.92 % (173556)Time elapsed: 0.068 s
% 38.37/5.92 % (173556)Peak memory usage: 14 MB
% 38.37/5.92 % (173556)Instructions burned: 132 (million)
% 38.37/5.92 % (173562)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3684165385:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 38.37/5.92 % TRYING [3]
% 38.37/5.92 % (173559)Instruction limit reached!
% 38.37/5.92 % (173559)------------------------------
% 38.37/5.92 % (173559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.37/5.92 % (173559)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173559)Termination reason: Instruction limit
% 38.37/5.92 % (173559)Termination phase: Saturation
% 38.37/5.92 % (173559)Time elapsed: 0.085 s
% 38.37/5.92 % (173559)Peak memory usage: 15 MB
% 38.37/5.92 % (173559)Instructions burned: 182 (million)
% 38.37/5.92 % (173554)Instruction limit reached!
% 38.37/5.92 % (173554)------------------------------
% 38.37/5.92 % (173554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.37/5.92 % (173554)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173554)Termination reason: Instruction limit
% 38.37/5.92 % (173554)Termination phase: Finite model building SAT solving
% 38.37/5.92 % (173554)Time elapsed: 0.164 s
% 38.37/5.92 % (173554)Peak memory usage: 42 MB
% 38.37/5.92 % (173554)Instructions burned: 715 (million)
% 38.37/5.92 % (173564)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4290367394:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.37/5.92 % (173565)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1859902224:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 38.37/5.92 % TRYING [1]
% 38.37/5.92 % TRYING [2]
% 38.37/5.92 % TRYING [4]
% 38.37/5.92 % (173562)Instruction limit reached!
% 38.37/5.92 % (173562)------------------------------
% 38.37/5.92 % (173562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.37/5.92 % (173562)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173562)Termination reason: Instruction limit
% 38.37/5.92 % (173562)Termination phase: Saturation
% 38.37/5.92 % (173562)Time elapsed: 0.272 s
% 38.37/5.92 % (173562)Peak memory usage: 17 MB
% 38.37/5.92 % (173562)Instructions burned: 477 (million)
% 38.37/5.92 % (173557)Instruction limit reached!
% 38.37/5.92 % (173557)------------------------------
% 38.37/5.92 % (173557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.37/5.92 % (173557)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173557)Termination reason: Instruction limit
% 38.37/5.92 % (173557)Termination phase: Saturation
% 38.37/5.92 % (173557)Time elapsed: 0.360 s
% 38.37/5.92 % (173557)Peak memory usage: 24 MB
% 38.37/5.92 % (173557)Instructions burned: 686 (million)
% 38.37/5.92 % (173568)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2736235345:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.37/5.92 % (173569)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=1387415298: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)
% 38.37/5.92 % TRYING [3]
% 38.37/5.92 % (173565)Instruction limit reached!
% 38.37/5.92 % (173565)------------------------------
% 38.37/5.92 % (173565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.37/5.92 % (173565)CaDiCaL version: 2.1.3
% 38.37/5.92 % (173565)Termination reason: Instruction limit
% 38.37/5.92 % (173565)Termination phase: Saturation
% 38.37/5.92 % (173565)Time elapsed: 0.323 s
% 38.37/5.92 % (173565)Peak memory usage: 32 MB
% 38.37/5.92 % (173565)Instructions burned: 1182 (million)
% 38.37/5.92 % (173572)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=679957755:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 38.37/5.92 % (173564)Instruction limit reached!
% 38.37/5.92 % (173564)------------------------------
% 38.37/5.92 % (173564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.37/5.92 % (173564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173564)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173564)Termination reason: Instruction limit
% 14.53/6.08 % (173564)Termination phase: Finite model building constraint generation
% 14.53/6.08 % (173564)Time elapsed: 0.370 s
% 14.53/6.08 % (173564)Peak memory usage: 30 MB
% 14.53/6.08 % (173564)Instructions burned: 866 (million)
% 14.53/6.08 % (173574)fmb+10_1_sil=64000:random_seed=2348328575:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 14.53/6.08 % TRYING [1]
% 14.53/6.08 % TRYING [2]
% 14.53/6.08 % TRYING [3]
% 14.53/6.08 % (173572)Instruction limit reached!
% 14.53/6.08 % (173572)------------------------------
% 14.53/6.08 % (173572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173572)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173572)Termination reason: Instruction limit
% 14.53/6.08 % (173572)Termination phase: Saturation
% 14.53/6.08 % (173572)Time elapsed: 0.265 s
% 14.53/6.08 % (173572)Peak memory usage: 30 MB
% 14.53/6.08 % (173572)Instructions burned: 882 (million)
% 14.53/6.08 % (173576)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3523274791:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 14.53/6.08 % (173569)Instruction limit reached!
% 14.53/6.08 % (173569)------------------------------
% 14.53/6.08 % (173569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173569)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173569)Termination reason: Instruction limit
% 14.53/6.08 % (173569)Termination phase: Saturation
% 14.53/6.08 % (173569)Time elapsed: 0.376 s
% 14.53/6.08 % (173569)Peak memory usage: 21 MB
% 14.53/6.08 % (173569)Instructions burned: 693 (million)
% 14.53/6.08 % (173578)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=594677838:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 14.53/6.08 % TRYING [20]
% 14.53/6.08 % (173568)Instruction limit reached!
% 14.53/6.08 % (173568)------------------------------
% 14.53/6.08 % (173568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173568)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173568)Termination reason: Instruction limit
% 14.53/6.08 % (173568)Termination phase: Finite model building constraint generation
% 14.53/6.08 % (173568)Time elapsed: 0.422 s
% 14.53/6.08 % (173568)Peak memory usage: 96 MB
% 14.53/6.08 % (173568)Instructions burned: 891 (million)
% 14.53/6.08 % (173580)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=497835126:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 14.53/6.08 % TRYING [8]
% 14.53/6.08 % TRYING [5]
% 14.53/6.08 % (173578)Instruction limit reached!
% 14.53/6.08 % (173578)------------------------------
% 14.53/6.08 % (173578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173578)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173578)Termination reason: Instruction limit
% 14.53/6.08 % (173578)Termination phase: Finite model building constraint generation
% 14.53/6.08 % (173578)Time elapsed: 0.325 s
% 14.53/6.08 % (173578)Peak memory usage: 52 MB
% 14.53/6.08 % (173578)Instructions burned: 922 (million)
% 14.53/6.08 % (173582)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2938793295:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 14.53/6.08 % TRYING [4]
% 14.53/6.08 % (173582)Instruction limit reached!
% 14.53/6.08 % (173582)------------------------------
% 14.53/6.08 % (173582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173582)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173582)Termination reason: Instruction limit
% 14.53/6.08 % (173582)Termination phase: Saturation
% 14.53/6.08 % (173582)Time elapsed: 0.836 s
% 14.53/6.08 % (173582)Peak memory usage: 39 MB
% 14.53/6.08 % (173582)Instructions burned: 1472 (million)
% 14.53/6.08 % (173584)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4056669556:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 14.53/6.08 % (173584)Cannot represent all propositional literals internally
% 14.53/6.08 % (173584)Refutation not found, incomplete strategy
% 14.53/6.08 % (173584)------------------------------
% 14.53/6.08 % (173584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173584)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173584)Termination reason: Refutation not found, incomplete strategy
% 14.53/6.08 % (173584)Time elapsed: 0.118 s
% 14.53/6.08 % (173584)Peak memory usage: 16 MB
% 14.53/6.08 % (173584)Instructions burned: 251 (million)
% 14.53/6.08 % (173584)------------------------------
% 14.53/6.08 % (173584)------------------------------
% 14.53/6.08 % (173586)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2138416976:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 14.53/6.08 % (173576)Instruction limit reached!
% 14.53/6.08 % (173576)------------------------------
% 14.53/6.08 % (173576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173576)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173576)Termination reason: Instruction limit
% 14.53/6.08 % (173576)Termination phase: Finite model building constraint generation
% 14.53/6.08 % (173576)Time elapsed: 1.732 s
% 14.53/6.08 % (173576)Peak memory usage: 527 MB
% 14.53/6.08 % (173576)Instructions burned: 9521 (million)
% 14.53/6.08 % (173588)ott-2_1_sil=16000:newcnf=on:random_seed=2744836942:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi)
% 14.53/6.08 % (173586)Cannot represent all propositional literals internally
% 14.53/6.08 % (173586)Refutation not found, incomplete strategy
% 14.53/6.08 % (173586)------------------------------
% 14.53/6.08 % (173586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173586)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173586)Termination reason: Refutation not found, incomplete strategy
% 14.53/6.08 % (173586)Time elapsed: 0.475 s
% 14.53/6.08 % (173586)Peak memory usage: 25 MB
% 14.53/6.08 % (173586)Instructions burned: 990 (million)
% 14.53/6.08 % (173586)------------------------------
% 14.53/6.08 % (173586)------------------------------
% 14.53/6.08 % (173590)ott+10_1_sil=32000:tgt=ground:random_seed=1382241220:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 14.53/6.08 % (173588)Instruction limit reached!
% 14.53/6.08 % (173588)------------------------------
% 14.53/6.08 % (173588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173588)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173588)Termination reason: Instruction limit
% 14.53/6.08 % (173588)Termination phase: Saturation
% 14.53/6.08 % (173588)Time elapsed: 0.238 s
% 14.53/6.08 % (173588)Peak memory usage: 25 MB
% 14.53/6.08 % (173588)Instructions burned: 874 (million)
% 14.53/6.08 % (173592)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=910673142:i=54282_2971 on theBenchmark for (2971ds/54282Mi)
% 14.53/6.08 % TRYING [5]
% 14.53/6.08 % TRYING [1]
% 14.53/6.08 % TRYING [2]
% 14.53/6.08 % TRYING [3]
% 14.53/6.08 % TRYING [4]
% 14.53/6.08 % (173580)Instruction limit reached!
% 14.53/6.08 % (173580)------------------------------
% 14.53/6.08 % (173580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173580)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173580)Termination reason: Instruction limit
% 14.53/6.08 % (173580)Termination phase: Saturation
% 14.53/6.08 % (173580)Time elapsed: 2.388 s
% 14.53/6.08 % (173580)Peak memory usage: 31 MB
% 14.53/6.08 % (173580)Instructions burned: 5133 (million)
% 14.53/6.08 % (173594)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1136408256:i=3512:aac=none_2966 on theBenchmark for (2966ds/3512Mi)
% 14.53/6.08 % TRYING [5]
% 14.53/6.08 % TRYING [6]
% 14.53/6.08 % (173594)Instruction limit reached!
% 14.53/6.08 % (173594)------------------------------
% 14.53/6.08 % (173594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173594)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173594)Termination reason: Instruction limit
% 14.53/6.08 % (173594)Termination phase: Saturation
% 14.53/6.08 % (173594)Time elapsed: 1.741 s
% 14.53/6.08 % (173594)Peak memory usage: 34 MB
% 14.53/6.08 % (173594)Instructions burned: 3514 (million)
% 14.53/6.08 % (173596)dis+21_1_sil=32000:sas=cadical:random_seed=1915030599:i=3773:amm=off_2948 on theBenchmark for (2948ds/3773Mi)
% 14.53/6.08 % TRYING [6]
% 14.53/6.08 % (173590)Instruction limit reached!
% 14.53/6.08 % (173590)------------------------------
% 14.53/6.08 % (173590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173590)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173590)Termination reason: Instruction limit
% 14.53/6.08 % (173590)Termination phase: Saturation
% 14.53/6.08 % (173590)Time elapsed: 2.721 s
% 14.53/6.08 % (173590)Peak memory usage: 64 MB
% 14.53/6.08 % (173590)Instructions burned: 5114 (million)
% 14.53/6.08 % (173598)ott+11_1_sil=16000:gs=on:random_seed=169535015:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2945 on theBenchmark for (2945ds/2251Mi)
% 14.53/6.08 % (173598) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-173535-173598"...
% 14.53/6.08 % (173598)...printing done.
% 14.53/6.08 % (173598)Refutation found. Thanks to Tanya!
% 14.53/6.08 % SZS status Theorem for theBenchmark
% 14.53/6.08 % SZS output start Proof for theBenchmark
% See solution above
% 14.53/6.08 % (173598)------------------------------
% 14.53/6.08 % (173598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.53/6.08 % (173598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.53/6.08 % (173598)CaDiCaL version: 2.1.3
% 14.53/6.08 % (173598)Termination reason: Refutation
% 14.53/6.08 % (173598)Time elapsed: 0.070 s
% 14.53/6.08 % (173598)Peak memory usage: 16 MB
% 14.53/6.08 % (173598)Instructions burned: 123 (million)
% 14.53/6.08 % (173535)Success in time 5.65 s
% 14.53/6.08 % Vampire exiting
%------------------------------------------------------------------------------