%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR096+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:45:11 AM UTC 2026
% Result : Theorem 15.00s 2.53s
% Output : Refutation 15.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 12
% Syntax : Number of formulae : 62 ( 17 unt; 2 def)
% Number of atoms : 162 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 190 ( 90 ~; 84 |; 5 &)
% ( 2 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 40 ( 0 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f5748,axiom,
s__subclass(s__AstronomicalBody,s__Object),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5820) ).
fof(f14789,axiom,
s__subclass(s__Planet26_1,s__AstronomicalBody),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f14790,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__Planet26_1)
=> ( s__attribute(X0,s__Solid)
| s__attribute(X0,s__Gaseous) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f14791,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__Planet26_1)
=> ( s__attribute(X0,s__Earthlike)
| s__attribute(X0,s__HostileToEarthLife) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(f14792,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( ( s__instance(X0,s__Planet26_1)
& s__attribute(X0,s__Gaseous) )
=> ~ s__attribute(X0,s__Earthlike) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(f14793,axiom,
s__instance(s__Object26_1,s__Planet26_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_6) ).
fof(f14794,axiom,
~ s__attribute(s__Object26_1,s__Solid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_7) ).
fof(f14795,conjecture,
s__attribute(s__Object26_1,s__HostileToEarthLife),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f14796,negated_conjecture,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(negated_conjecture,[status(cth)],[f14795]) ).
fof(f14800,plain,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(flattening,[],[f14796]) ).
fof(f14891,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f14892,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f14893,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f14892]) ).
fof(f19985,plain,
! [X0] :
( s__attribute(X0,s__Solid)
| s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f14790]) ).
fof(f19986,plain,
! [X0] :
( s__attribute(X0,s__Solid)
| s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f19985]) ).
fof(f19987,plain,
! [X0] :
( s__attribute(X0,s__Earthlike)
| s__attribute(X0,s__HostileToEarthLife)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f14791]) ).
fof(f19988,plain,
! [X0] :
( s__attribute(X0,s__Earthlike)
| s__attribute(X0,s__HostileToEarthLife)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f19987]) ).
fof(f19989,plain,
! [X0] :
( ~ s__attribute(X0,s__Earthlike)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f14792]) ).
fof(f19990,plain,
! [X0] :
( ~ s__attribute(X0,s__Earthlike)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f19989]) ).
fof(f21295,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f14891]) ).
fof(f21296,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f14891]) ).
fof(f21297,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f14893]) ).
fof(f27856,plain,
s__subclass(s__AstronomicalBody,s__Object),
inference(cnf_transformation,[],[f5748]) ).
fof(f37132,plain,
s__subclass(s__Planet26_1,s__AstronomicalBody),
inference(cnf_transformation,[],[f14789]) ).
fof(f37133,plain,
! [X0] :
( s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object)
| s__attribute(X0,s__Solid) ),
inference(cnf_transformation,[],[f19986]) ).
fof(f37134,plain,
! [X0] :
( s__attribute(X0,s__HostileToEarthLife)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object)
| s__attribute(X0,s__Earthlike) ),
inference(cnf_transformation,[],[f19988]) ).
fof(f37135,plain,
! [X0] :
( ~ s__attribute(X0,s__Earthlike)
| ~ s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[],[f19990]) ).
fof(f37136,plain,
s__instance(s__Object26_1,s__Planet26_1),
inference(cnf_transformation,[],[f14793]) ).
fof(f37137,plain,
~ s__attribute(s__Object26_1,s__Solid),
inference(cnf_transformation,[],[f14794]) ).
fof(f37138,plain,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(cnf_transformation,[],[f14800]) ).
fof(f54448,plain,
( ~ s__instance(s__Object26_1,s__Planet26_1)
| ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Earthlike) ),
inference(resolution,[],[f37134,f37138]) ).
fof(f54451,plain,
( ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Earthlike) ),
inference(forward_subsumption_resolution,[],[f54448,f37136]) ).
fof(f54453,definition,
( spl478_250
<=> s__attribute(s__Object26_1,s__Earthlike) ),
introduced(definition,[new_symbols(definition,[spl478_250])],[avatar_definition]) ).
fof(f54455,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ spl478_250 ),
inference(avatar_component_clause,[],[f54453]) ).
fof(f54457,definition,
( spl478_251
<=> s__instance(s__Object26_1,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_251])],[avatar_definition]) ).
fof(f54458,plain,
( s__instance(s__Object26_1,s__Object)
| ~ spl478_251 ),
inference(avatar_component_clause,[],[f54457]) ).
fof(f54459,plain,
( ~ s__instance(s__Object26_1,s__Object)
| spl478_251 ),
inference(avatar_component_clause,[],[f54457]) ).
fof(f54460,plain,
( spl478_250
| ~ spl478_251 ),
inference(avatar_split_clause,[],[f54451,f54457,f54453]) ).
fof(f55835,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f21297,f21295]) ).
fof(f55836,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f55835,f21296]) ).
fof(f55894,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| ~ s__instance(s__Object26_1,X0) )
| spl478_251 ),
inference(resolution,[],[f55836,f54459]) ).
fof(f55975,plain,
( ~ s__instance(s__Object26_1,s__AstronomicalBody)
| spl478_251 ),
inference(resolution,[],[f55894,f27856]) ).
fof(f57860,plain,
( ! [X0] :
( ~ s__subclass(X0,s__AstronomicalBody)
| ~ s__instance(s__Object26_1,X0) )
| spl478_251 ),
inference(resolution,[],[f55975,f55836]) ).
fof(f74216,plain,
( ~ s__instance(s__Object26_1,s__Planet26_1)
| spl478_251 ),
inference(resolution,[],[f57860,f37132]) ).
fof(f74217,plain,
( $false
| spl478_251 ),
inference(forward_subsumption_resolution,[],[f74216,f37136]) ).
fof(f74218,plain,
spl478_251,
inference(avatar_contradiction_clause,[],[f74217]) ).
fof(f74222,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| ~ s__instance(s__Object26_1,s__Planet26_1)
| ~ s__instance(s__Object26_1,s__Object)
| ~ spl478_250 ),
inference(resolution,[],[f54455,f37135]) ).
fof(f74224,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| ~ s__instance(s__Object26_1,s__Object)
| ~ spl478_250 ),
inference(forward_subsumption_resolution,[],[f74222,f37136]) ).
fof(f74229,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| ~ spl478_250
| ~ spl478_251 ),
inference(forward_subsumption_resolution,[],[f74224,f54458]) ).
fof(f74246,plain,
( ~ s__instance(s__Object26_1,s__Planet26_1)
| ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Solid)
| ~ spl478_250
| ~ spl478_251 ),
inference(resolution,[],[f74229,f37133]) ).
fof(f74247,plain,
( ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Solid)
| ~ spl478_250
| ~ spl478_251 ),
inference(forward_subsumption_resolution,[],[f74246,f37136]) ).
fof(f74248,plain,
( s__attribute(s__Object26_1,s__Solid)
| ~ spl478_250
| ~ spl478_251 ),
inference(forward_subsumption_resolution,[],[f74247,f54458]) ).
fof(f74249,plain,
( $false
| ~ spl478_250
| ~ spl478_251 ),
inference(forward_subsumption_resolution,[],[f74248,f37137]) ).
fof(f74250,plain,
( ~ spl478_250
| ~ spl478_251 ),
inference(avatar_contradiction_clause,[],[f74249]) ).
cnf(s126,plain,
( spl478_250
| ~ spl478_251 ),
inference(sat_conversion,[],[f54460]) ).
cnf(s217,plain,
spl478_251,
inference(sat_conversion,[],[f74218]) ).
cnf(s218,plain,
( ~ spl478_250
| ~ spl478_251 ),
inference(sat_conversion,[],[f74250]) ).
cnf(s219,plain,
~ spl478_250,
inference(rat,[],[s218,s217]) ).
cnf(s220,plain,
$false,
inference(rat,[],[s126,s217,s219]) ).
fof(f74251,plain,
$false,
inference(avatar_sat_refutation,[],[s220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR096+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.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:48:07 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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
% 7.53/1.70 % (862232)Will run a generic schedule for satisfiability detection.
% 7.53/1.70 % (862243)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3965596454:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.53/1.70 % (862238)% WARNING: option uhcvi not known.
% 7.53/1.70 % (862237)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1547680508_2998 on theBenchmark for (2998ds/0Mi)
% 7.53/1.70 % (862238)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1131591734:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.53/1.70 % (862239)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2863751494:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.53/1.70 % (862240)dis+10_1_sil=32000:sp=arity:random_seed=1851940181:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.53/1.70 % (862241)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=102837678:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.53/1.70 % (862242)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=774931414:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.53/1.70 % (862243)Instruction limit reached!
% 7.53/1.70 % (862243)------------------------------
% 7.53/1.70 % (862243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.70 % (862243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.70 % (862243)CaDiCaL version: 2.1.3
% 7.53/1.70 % (862243)Termination reason: Instruction limit
% 7.53/1.70 % (862243)Termination phase: Property scanning
% 7.53/1.70 % (862243)Time elapsed: 0.053 s
% 7.53/1.70 % (862243)Peak memory usage: 31 MB
% 7.53/1.70 % (862243)Instructions burned: 162 (million)
% 7.53/1.70 % (862252)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3721614379:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.53/1.70 % (862240)Instruction limit reached!
% 7.53/1.70 % (862240)------------------------------
% 7.53/1.70 % (862240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.70 % (862240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.70 % (862240)CaDiCaL version: 2.1.3
% 7.53/1.70 % (862240)Termination reason: Instruction limit
% 7.53/1.70 % (862240)Termination phase: Preprocessing 3
% 7.53/1.70 % (862240)Time elapsed: 0.063 s
% 7.53/1.70 % (862240)Peak memory usage: 29 MB
% 7.53/1.70 % (862240)Instructions burned: 106 (million)
% 7.53/1.70 % (862242)Instruction limit reached!
% 7.53/1.70 % (862242)------------------------------
% 7.53/1.70 % (862242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.70 % (862241)Instruction limit reached!
% 7.53/1.70 % (862241)------------------------------
% 7.53/1.70 % (862241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.70 % (862241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.70 % (862242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.70 % (862242)CaDiCaL version: 2.1.3
% 7.53/1.70 % (862241)CaDiCaL version: 2.1.3
% 7.53/1.70 % (862241)Termination reason: Instruction limit
% 7.53/1.70 % (862241)Termination phase: NewCNF
% 7.53/1.70 % (862242)Termination reason: Instruction limit
% 7.53/1.70 % (862242)Termination phase: Clausification
% 7.53/1.70 % (862241)Time elapsed: 0.075 s
% 7.53/1.70 % (862242)Time elapsed: 0.074 s
% 7.53/1.70 % (862241)Peak memory usage: 31 MB
% 7.53/1.70 % (862242)Peak memory usage: 30 MB
% 7.53/1.70 % (862242)Instructions burned: 131 (million)
% 7.53/1.70 % (862241)Instructions burned: 117 (million)
% 7.53/1.70 % (862254)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=175541990:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.53/1.70 % (862255)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=1669050114:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.53/1.70 % (862256)ott-21_1_sil=16000:fs=off:random_seed=3243725893:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.53/1.70 % (862254)Instruction limit reached!
% 7.53/1.70 % (862254)------------------------------
% 7.53/1.70 % (862254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.70 % (862254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.70 % (862254)CaDiCaL version: 2.1.3
% 7.53/1.70 % (862254)Termination reason: Instruction limit
% 15.00/2.53 % (862254)Termination phase: Property scanning
% 15.00/2.53 % (862254)Time elapsed: 0.077 s
% 15.00/2.53 % (862254)Peak memory usage: 31 MB
% 15.00/2.53 % (862254)Instructions burned: 134 (million)
% 15.00/2.53 % (862260)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3648542200:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 15.00/2.53 % (862256)Instruction limit reached!
% 15.00/2.53 % (862256)------------------------------
% 15.00/2.53 % (862256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862256)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862256)Termination reason: Instruction limit
% 15.00/2.53 % (862256)Termination phase: Property scanning
% 15.00/2.53 % (862256)Time elapsed: 0.101 s
% 15.00/2.53 % (862256)Peak memory usage: 31 MB
% 15.00/2.53 % (862256)Instructions burned: 182 (million)
% 15.00/2.53 % (862262)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2311395054:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 15.00/2.53 % (862252)Instruction limit reached!
% 15.00/2.53 % (862252)------------------------------
% 15.00/2.53 % (862252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862252)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862252)Termination reason: Instruction limit
% 15.00/2.53 % (862252)Termination phase: Finite model building preprocessing
% 15.00/2.53 % (862252)Time elapsed: 0.192 s
% 15.00/2.53 % (862252)Peak memory usage: 42 MB
% 15.00/2.53 % (862252)Instructions burned: 719 (million)
% 15.00/2.53 % (862264)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2972279947:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 15.00/2.53 % (862260)Instruction limit reached!
% 15.00/2.53 % (862260)------------------------------
% 15.00/2.53 % (862260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862260)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862260)Termination reason: Instruction limit
% 15.00/2.53 % (862260)Termination phase: Saturation
% 15.00/2.53 % (862260)Time elapsed: 0.234 s
% 15.00/2.53 % (862260)Peak memory usage: 36 MB
% 15.00/2.53 % (862260)Instructions burned: 478 (million)
% 15.00/2.53 % (862255)Instruction limit reached!
% 15.00/2.53 % (862255)------------------------------
% 15.00/2.53 % (862255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862255)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862255)Termination reason: Instruction limit
% 15.00/2.53 % (862255)Termination phase: Saturation
% 15.00/2.53 % (862255)Time elapsed: 0.332 s
% 15.00/2.53 % (862255)Peak memory usage: 38 MB
% 15.00/2.53 % (862255)Instructions burned: 684 (million)
% 15.00/2.53 % (862266)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2614036662:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 15.00/2.53 % (862267)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=3443443419: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)
% 15.00/2.53 % (862264)Instruction limit reached!
% 15.00/2.53 % (862264)------------------------------
% 15.00/2.53 % (862264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862264)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862264)Termination reason: Instruction limit
% 15.00/2.53 % (862264)Termination phase: Saturation
% 15.00/2.53 % (862264)Time elapsed: 0.335 s
% 15.00/2.53 % (862264)Peak memory usage: 44 MB
% 15.00/2.53 % (862264)Instructions burned: 1181 (million)
% 15.00/2.53 % (862270)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=719203651:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 15.00/2.53 % (862262)Instruction limit reached!
% 15.00/2.53 % (862262)------------------------------
% 15.00/2.53 % (862262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862262)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862262)Termination reason: Instruction limit
% 15.00/2.53 % (862262)Termination phase: Finite model building preprocessing
% 15.00/2.53 % (862262)Time elapsed: 0.415 s
% 15.00/2.53 % (862262)Peak memory usage: 46 MB
% 15.00/2.53 % (862262)Instructions burned: 865 (million)
% 15.00/2.53 % (862272)fmb+10_1_sil=64000:random_seed=226926870:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 15.00/2.53 % (862267)Instruction limit reached!
% 15.00/2.53 % (862267)------------------------------
% 15.00/2.53 % (862267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862267)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862267)Termination reason: Instruction limit
% 15.00/2.53 % (862267)Termination phase: Saturation
% 15.00/2.53 % (862267)Time elapsed: 0.359 s
% 15.00/2.53 % (862267)Peak memory usage: 42 MB
% 15.00/2.53 % (862267)Instructions burned: 693 (million)
% 15.00/2.53 % (862274)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1270592186:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 15.00/2.53 % (862270)Instruction limit reached!
% 15.00/2.53 % (862270)------------------------------
% 15.00/2.53 % (862270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862270)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862270)Termination reason: Instruction limit
% 15.00/2.53 % (862270)Termination phase: Saturation
% 15.00/2.53 % (862270)Time elapsed: 0.238 s
% 15.00/2.53 % (862270)Peak memory usage: 44 MB
% 15.00/2.53 % (862270)Instructions burned: 881 (million)
% 15.00/2.53 % (862276)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=414848230:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 15.00/2.53 % Detected minimum model sizes of [51]
% 15.00/2.53 % Detected maximum model sizes of [max]
% 15.00/2.53 % (862237)Cannot represent all propositional literals internally
% 15.00/2.53 % (862237)Refutation not found, incomplete strategy
% 15.00/2.53 % (862237)------------------------------
% 15.00/2.53 % (862237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862237)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862237)Termination reason: Refutation not found, incomplete strategy
% 15.00/2.53 % (862237)Time elapsed: 0.875 s
% 15.00/2.53 % (862237)Peak memory usage: 58 MB
% 15.00/2.53 % (862237)Instructions burned: 1854 (million)
% 15.00/2.53 % (862266)Instruction limit reached!
% 15.00/2.53 % (862266)------------------------------
% 15.00/2.53 % (862266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862266)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862266)Termination reason: Instruction limit
% 15.00/2.53 % (862266)Termination phase: Finite model building preprocessing
% 15.00/2.53 % (862266)Time elapsed: 0.430 s
% 15.00/2.53 % (862266)Peak memory usage: 47 MB
% 15.00/2.53 % (862266)Instructions burned: 891 (million)
% 15.00/2.53 % (862237)------------------------------
% 15.00/2.53 % (862237)------------------------------
% 15.00/2.53 % (862278)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=198533276:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 15.00/2.53 % (862280)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4159453164:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 15.00/2.53 % (862276)Instruction limit reached!
% 15.00/2.53 % (862276)------------------------------
% 15.00/2.53 % (862276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862276)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862276)Termination reason: Instruction limit
% 15.00/2.53 % (862276)Termination phase: Finite model building preprocessing
% 15.00/2.53 % (862276)Time elapsed: 0.243 s
% 15.00/2.53 % (862276)Peak memory usage: 47 MB
% 15.00/2.53 % (862276)Instructions burned: 922 (million)
% 15.00/2.53 % (862282)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2515828424:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 15.00/2.53 % Detected minimum model sizes of [51]
% 15.00/2.53 % Detected maximum model sizes of [max]
% 15.00/2.53 % (862272)Cannot represent all propositional literals internally
% 15.00/2.53 % (862272)Refutation not found, incomplete strategy
% 15.00/2.53 % (862272)------------------------------
% 15.00/2.53 % (862272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862272)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862272)Termination reason: Refutation not found, incomplete strategy
% 15.00/2.53 % (862272)Time elapsed: 0.665 s
% 15.00/2.53 % (862272)Peak memory usage: 52 MB
% 15.00/2.53 % (862272)Instructions burned: 1453 (million)
% 15.00/2.53 % (862272)------------------------------
% 15.00/2.53 % (862272)------------------------------
% 15.00/2.53 % (862284)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1825558364:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 15.00/2.53 % Detected minimum model sizes of [51]
% 15.00/2.53 % Detected maximum model sizes of [max]
% 15.00/2.53 % (862274)Cannot represent all propositional literals internally
% 15.00/2.53 % (862274)Refutation not found, incomplete strategy
% 15.00/2.53 % (862274)------------------------------
% 15.00/2.53 % (862274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862274)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862274)Termination reason: Refutation not found, incomplete strategy
% 15.00/2.53 % (862274)Time elapsed: 0.713 s
% 15.00/2.53 % (862274)Peak memory usage: 52 MB
% 15.00/2.53 % (862274)Instructions burned: 1528 (million)
% 15.00/2.53 % (862274)------------------------------
% 15.00/2.53 % (862274)------------------------------
% 15.00/2.53 % Detected minimum model sizes of [51]
% 15.00/2.53 % Detected maximum model sizes of [max]
% 15.00/2.53 % (862282)Cannot represent all propositional literals internally
% 15.00/2.53 % (862282)Refutation not found, incomplete strategy
% 15.00/2.53 % (862282)------------------------------
% 15.00/2.53 % (862282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862282)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862282)Termination reason: Refutation not found, incomplete strategy
% 15.00/2.53 % (862282)Time elapsed: 0.474 s
% 15.00/2.53 % (862282)Peak memory usage: 58 MB
% 15.00/2.53 % (862282)Instructions burned: 1851 (million)
% 15.00/2.53 % (862286)ott-2_1_sil=16000:newcnf=on:random_seed=788604734:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi)
% 15.00/2.53 % (862282)------------------------------
% 15.00/2.53 % (862282)------------------------------
% 15.00/2.53 % (862288)ott+10_1_sil=32000:tgt=ground:random_seed=408740838:i=5114:av=off_2982 on theBenchmark for (2982ds/5114Mi)
% 15.00/2.53 % (862280)Instruction limit reached!
% 15.00/2.53 % (862280)------------------------------
% 15.00/2.53 % (862280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862280)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862280)Termination reason: Instruction limit
% 15.00/2.53 % (862280)Termination phase: Saturation
% 15.00/2.53 % (862280)Time elapsed: 0.788 s
% 15.00/2.53 % (862280)Peak memory usage: 49 MB
% 15.00/2.53 % (862280)Instructions burned: 1472 (million)
% 15.00/2.53 % (862290)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=136136452:i=54282_2981 on theBenchmark for (2981ds/54282Mi)
% 15.00/2.53 % (862286)Instruction limit reached!
% 15.00/2.53 % (862286)------------------------------
% 15.00/2.53 % (862286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.53 % (862286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.53 % (862286)CaDiCaL version: 2.1.3
% 15.00/2.53 % (862286)Termination reason: Instruction limit
% 15.00/2.53 % (862286)Termination phase: Saturation
% 15.00/2.53 % (862286)Time elapsed: 0.434 s
% 15.00/2.53 % (862286)Peak memory usage: 43 MB
% 15.00/2.53 % (862286)Instructions burned: 869 (million)
% 15.00/2.53 % (862292)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1197845892:i=3512:aac=none_2978 on theBenchmark for (2978ds/3512Mi)
% 15.00/2.53 % (862278) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-862232-862278"...
% 15.00/2.53 % (862278)...printing done.
% 15.00/2.53 % (862278)Refutation found. Thanks to Tanya!
% 15.00/2.53 % SZS status Theorem for theBenchmark
% 15.00/2.53 % SZS output start Proof for theBenchmark
% See solution above
% 15.00/2.55 % (862278)------------------------------
% 15.00/2.55 % (862278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.00/2.55 % (862278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.00/2.55 % (862278)CaDiCaL version: 2.1.3
% 15.00/2.55 % (862278)Termination reason: Refutation
% 15.00/2.55 % (862278)Time elapsed: 1.224 s
% 15.00/2.55 % (862278)Peak memory usage: 58 MB
% 15.00/2.55 % (862278)Instructions burned: 2416 (million)
% 15.00/2.55 % (862232)Success in time 2.307 s
% 15.00/2.55 % Vampire exiting
%------------------------------------------------------------------------------