%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR096+4 : 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 : n008.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:12 AM UTC 2026
% Result : Theorem 6.93s 1.53s
% Output : Refutation 6.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 13
% Syntax : Number of formulae : 73 ( 21 unt; 3 def)
% Number of atoms : 186 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 187 ( 74 ~; 96 |; 5 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 50 ( 0 sgn 50 !; 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(f7219,axiom,
s__subclass(s__Planet26_1,s__AstronomicalBody),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f7220,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(f7221,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(f7222,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(f7223,axiom,
s__instance(s__Object26_1,s__Planet26_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_6) ).
fof(f7224,axiom,
~ s__attribute(s__Object26_1,s__Solid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_7) ).
fof(f7225,conjecture,
s__attribute(s__Object26_1,s__HostileToEarthLife),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f7226,negated_conjecture,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(negated_conjecture,[status(cth)],[f7225]) ).
fof(f7230,plain,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(flattening,[],[f7226]) ).
fof(f7321,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f7322,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(f7323,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,[],[f7322]) ).
fof(f12415,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,[],[f7220]) ).
fof(f12416,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,[],[f12415]) ).
fof(f12417,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,[],[f7221]) ).
fof(f12418,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,[],[f12417]) ).
fof(f12419,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,[],[f7222]) ).
fof(f12420,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,[],[f12419]) ).
fof(f13725,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f7321]) ).
fof(f13726,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f7321]) ).
fof(f13727,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,[],[f7323]) ).
fof(f20286,plain,
s__subclass(s__AstronomicalBody,s__Object),
inference(cnf_transformation,[],[f5748]) ).
fof(f21992,plain,
s__subclass(s__Planet26_1,s__AstronomicalBody),
inference(cnf_transformation,[],[f7219]) ).
fof(f21993,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__instance(X0,s__Planet26_1)
| s__attribute(X0,s__Gaseous)
| s__attribute(X0,s__Solid) ),
inference(cnf_transformation,[],[f12416]) ).
fof(f21994,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__instance(X0,s__Planet26_1)
| s__attribute(X0,s__HostileToEarthLife)
| s__attribute(X0,s__Earthlike) ),
inference(cnf_transformation,[],[f12418]) ).
fof(f21995,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1)
| ~ s__attribute(X0,s__Earthlike) ),
inference(cnf_transformation,[],[f12420]) ).
fof(f21996,plain,
s__instance(s__Object26_1,s__Planet26_1),
inference(cnf_transformation,[],[f7223]) ).
fof(f21997,plain,
~ s__attribute(s__Object26_1,s__Solid),
inference(cnf_transformation,[],[f7224]) ).
fof(f21998,plain,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(cnf_transformation,[],[f7230]) ).
fof(f22400,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f13726]) ).
fof(f22401,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| s__subclass(X0,X1) ),
inference(consistent_polarity_flipping,[],[f13725]) ).
fof(f22402,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(consistent_polarity_flipping,[],[f13727]) ).
fof(f27944,plain,
~ s__subclass(s__AstronomicalBody,s__Object),
inference(consistent_polarity_flipping,[],[f20286]) ).
fof(f29214,plain,
~ s__subclass(s__Planet26_1,s__AstronomicalBody),
inference(consistent_polarity_flipping,[],[f21992]) ).
fof(f29215,plain,
! [X0] :
( s__attribute(X0,s__Gaseous)
| s__instance(X0,s__Planet26_1)
| s__instance(X0,s__Object)
| s__attribute(X0,s__Solid) ),
inference(consistent_polarity_flipping,[],[f21993]) ).
fof(f29216,plain,
! [X0] :
( s__attribute(X0,s__HostileToEarthLife)
| s__instance(X0,s__Planet26_1)
| s__instance(X0,s__Object)
| s__attribute(X0,s__Earthlike) ),
inference(consistent_polarity_flipping,[],[f21994]) ).
fof(f29217,plain,
! [X0] :
( ~ s__attribute(X0,s__Earthlike)
| ~ s__attribute(X0,s__Gaseous)
| s__instance(X0,s__Planet26_1)
| s__instance(X0,s__Object) ),
inference(consistent_polarity_flipping,[],[f21995]) ).
fof(f29218,plain,
~ s__instance(s__Object26_1,s__Planet26_1),
inference(consistent_polarity_flipping,[],[f21996]) ).
fof(f72719,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,[],[f29216,f21998]) ).
fof(f72739,plain,
( s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Earthlike) ),
inference(forward_subsumption_resolution,[],[f72719,f29218]) ).
fof(f72741,definition,
( spl478_989
<=> s__attribute(s__Object26_1,s__Earthlike) ),
introduced(definition,[new_symbols(definition,[spl478_989])],[avatar_definition]) ).
fof(f72743,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ spl478_989 ),
inference(avatar_component_clause,[],[f72741]) ).
fof(f72745,definition,
( spl478_990
<=> s__instance(s__Object26_1,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_990])],[avatar_definition]) ).
fof(f72747,plain,
( s__instance(s__Object26_1,s__Object)
| ~ spl478_990 ),
inference(avatar_component_clause,[],[f72745]) ).
fof(f72748,plain,
( spl478_989
| spl478_990 ),
inference(avatar_split_clause,[],[f72739,f72745,f72741]) ).
fof(f72749,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| s__instance(s__Object26_1,s__Planet26_1)
| s__instance(s__Object26_1,s__Object)
| ~ spl478_989 ),
inference(resolution,[],[f72743,f29217]) ).
fof(f72750,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| s__instance(s__Object26_1,s__Object)
| ~ spl478_989 ),
inference(forward_subsumption_resolution,[],[f72749,f29218]) ).
fof(f72752,definition,
( spl478_991
<=> s__attribute(s__Object26_1,s__Gaseous) ),
introduced(definition,[new_symbols(definition,[spl478_991])],[avatar_definition]) ).
fof(f72754,plain,
( ~ s__attribute(s__Object26_1,s__Gaseous)
| spl478_991 ),
inference(avatar_component_clause,[],[f72752]) ).
fof(f72755,plain,
( spl478_990
| ~ spl478_991
| ~ spl478_989 ),
inference(avatar_split_clause,[],[f72750,f72741,f72752,f72745]) ).
fof(f72792,plain,
( s__instance(s__Object26_1,s__Planet26_1)
| s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Solid)
| spl478_991 ),
inference(resolution,[],[f72754,f29215]) ).
fof(f72793,plain,
( s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Solid)
| spl478_991 ),
inference(forward_subsumption_resolution,[],[f72792,f29218]) ).
fof(f72794,plain,
( s__instance(s__Object26_1,s__Object)
| spl478_991 ),
inference(forward_subsumption_resolution,[],[f72793,f21997]) ).
fof(f72795,plain,
( spl478_990
| spl478_991 ),
inference(avatar_split_clause,[],[f72794,f72752,f72745]) ).
fof(f74885,plain,
! [X2,X0,X1] :
( s__instance(X1,s__SetOrClass)
| s__instance(X2,X0)
| s__subclass(X0,X1)
| ~ s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f22402,f22400]) ).
fof(f74886,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f74885,f22401]) ).
fof(f75244,plain,
( ! [X0] :
( s__subclass(X0,s__Object)
| s__instance(s__Object26_1,X0) )
| ~ spl478_990 ),
inference(resolution,[],[f74886,f72747]) ).
fof(f75278,plain,
( s__instance(s__Object26_1,s__AstronomicalBody)
| ~ spl478_990 ),
inference(resolution,[],[f75244,f27944]) ).
fof(f75286,plain,
( ! [X0] :
( s__subclass(X0,s__AstronomicalBody)
| s__instance(s__Object26_1,X0) )
| ~ spl478_990 ),
inference(resolution,[],[f75278,f74886]) ).
fof(f75896,plain,
( s__instance(s__Object26_1,s__Planet26_1)
| ~ spl478_990 ),
inference(resolution,[],[f75286,f29214]) ).
fof(f75897,plain,
( $false
| ~ spl478_990 ),
inference(forward_subsumption_resolution,[],[f75896,f29218]) ).
fof(f75898,plain,
~ spl478_990,
inference(avatar_contradiction_clause,[],[f75897]) ).
cnf(s5382,plain,
( spl478_989
| spl478_990 ),
inference(sat_conversion,[],[f72748]) ).
cnf(s5383,plain,
( ~ spl478_989
| spl478_990
| ~ spl478_991 ),
inference(sat_conversion,[],[f72755]) ).
cnf(s5387,plain,
( spl478_990
| spl478_991 ),
inference(sat_conversion,[],[f72795]) ).
cnf(s5714,plain,
~ spl478_990,
inference(sat_conversion,[],[f75898]) ).
cnf(s5792,plain,
spl478_991,
inference(rat,[],[s5387,s5714]) ).
cnf(s5793,plain,
~ spl478_989,
inference(rat,[],[s5383,s5792,s5714]) ).
cnf(s5794,plain,
$false,
inference(rat,[],[s5382,s5714,s5793]) ).
fof(f75899,plain,
$false,
inference(avatar_sat_refutation,[],[s5794]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR096+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n008.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 22:46:40 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.25 Running first-order model finding
% 0.10/0.25 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.93/1.50 % (2737814)Will run a generic schedule for satisfiability detection.
% 6.93/1.50 % (2737825)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4138400140:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.93/1.50 % (2737820)% WARNING: option uhcvi not known.
% 6.93/1.50 % (2737819)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2456257450_2999 on theBenchmark for (2999ds/0Mi)
% 6.93/1.50 % (2737823)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=763166059:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.93/1.50 % (2737822)dis+10_1_sil=32000:sp=arity:random_seed=2544886690:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.93/1.50 % (2737820)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4090396843:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.93/1.50 % (2737821)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=358975811:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.93/1.50 % (2737824)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4131492920:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.93/1.50 % (2737825)Instruction limit reached!
% 6.93/1.50 % (2737825)------------------------------
% 6.93/1.50 % (2737825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.50 % (2737825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.50 % (2737825)CaDiCaL version: 2.1.3
% 6.93/1.50 % (2737825)Termination reason: Instruction limit
% 6.93/1.50 % (2737825)Termination phase: Equality resolution with deletion
% 6.93/1.50 % (2737825)Time elapsed: 0.051 s
% 6.93/1.50 % (2737825)Peak memory usage: 25 MB
% 6.93/1.50 % (2737825)Instructions burned: 161 (million)
% 6.93/1.50 % (2737833)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1626828658:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.93/1.50 % (2737822)Instruction limit reached!
% 6.93/1.50 % (2737822)------------------------------
% 6.93/1.50 % (2737822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.50 % (2737822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.50 % (2737822)CaDiCaL version: 2.1.3
% 6.93/1.50 % (2737822)Termination reason: Instruction limit
% 6.93/1.50 % (2737822)Termination phase: Property scanning
% 6.93/1.50 % (2737822)Time elapsed: 0.066 s
% 6.93/1.50 % (2737822)Peak memory usage: 24 MB
% 6.93/1.50 % (2737822)Instructions burned: 105 (million)
% 6.93/1.50 % (2737823)Instruction limit reached!
% 6.93/1.50 % (2737823)------------------------------
% 6.93/1.50 % (2737823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.50 % (2737823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.50 % (2737823)CaDiCaL version: 2.1.3
% 6.93/1.50 % (2737823)Termination reason: Instruction limit
% 6.93/1.50 % (2737823)Termination phase: Property scanning
% 6.93/1.50 % (2737823)Time elapsed: 0.071 s
% 6.93/1.50 % (2737823)Peak memory usage: 26 MB
% 6.93/1.50 % (2737823)Instructions burned: 116 (million)
% 6.93/1.50 % (2737824)Instruction limit reached!
% 6.93/1.50 % (2737824)------------------------------
% 6.93/1.50 % (2737824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.50 % (2737824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.50 % (2737824)CaDiCaL version: 2.1.3
% 6.93/1.50 % (2737824)Termination reason: Instruction limit
% 6.93/1.50 % (2737824)Termination phase: Property scanning
% 6.93/1.50 % (2737824)Time elapsed: 0.079 s
% 6.93/1.50 % (2737824)Peak memory usage: 24 MB
% 6.93/1.50 % (2737824)Instructions burned: 131 (million)
% 6.93/1.50 % (2737835)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=671320711:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.93/1.50 % (2737836)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=2982712870:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.93/1.50 % (2737837)ott-21_1_sil=16000:fs=off:random_seed=1191303465:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.93/1.50 % (2737835)Instruction limit reached!
% 6.93/1.50 % (2737835)------------------------------
% 6.93/1.50 % (2737835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.50 % (2737835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737835)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737835)Termination reason: Instruction limit
% 6.93/1.53 % (2737835)Termination phase: Property scanning
% 6.93/1.53 % (2737835)Time elapsed: 0.079 s
% 6.93/1.53 % (2737835)Peak memory usage: 25 MB
% 6.93/1.53 % (2737835)Instructions burned: 131 (million)
% 6.93/1.53 % (2737841)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4030013469:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.93/1.53 % (2737837)Instruction limit reached!
% 6.93/1.53 % (2737837)------------------------------
% 6.93/1.53 % (2737837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737837)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737837)Termination reason: Instruction limit
% 6.93/1.53 % (2737837)Termination phase: Property scanning
% 6.93/1.53 % (2737837)Time elapsed: 0.101 s
% 6.93/1.53 % (2737837)Peak memory usage: 25 MB
% 6.93/1.53 % (2737837)Instructions burned: 182 (million)
% 6.93/1.53 % (2737843)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1910070472:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 6.93/1.53 % (2737833)Instruction limit reached!
% 6.93/1.53 % (2737833)------------------------------
% 6.93/1.53 % (2737833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737833)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737833)Termination reason: Instruction limit
% 6.93/1.53 % (2737833)Termination phase: Finite model building preprocessing
% 6.93/1.53 % (2737833)Time elapsed: 0.186 s
% 6.93/1.53 % (2737833)Peak memory usage: 36 MB
% 6.93/1.53 % (2737833)Instructions burned: 715 (million)
% 6.93/1.53 % (2737845)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3210036642:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 6.93/1.53 % (2737836)Instruction limit reached!
% 6.93/1.53 % (2737836)------------------------------
% 6.93/1.53 % (2737836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737836)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737836)Termination reason: Instruction limit
% 6.93/1.53 % (2737836)Termination phase: Saturation
% 6.93/1.53 % (2737836)Time elapsed: 0.355 s
% 6.93/1.53 % (2737836)Peak memory usage: 33 MB
% 6.93/1.53 % (2737836)Instructions burned: 685 (million)
% 6.93/1.53 % (2737841)Instruction limit reached!
% 6.93/1.53 % (2737841)------------------------------
% 6.93/1.53 % (2737841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737841)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737841)Termination reason: Instruction limit
% 6.93/1.53 % (2737841)Termination phase: Saturation
% 6.93/1.53 % (2737841)Time elapsed: 0.258 s
% 6.93/1.53 % (2737841)Peak memory usage: 30 MB
% 6.93/1.53 % (2737841)Instructions burned: 478 (million)
% 6.93/1.53 % (2737847)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1940940739:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.93/1.53 % (2737848)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=2180832149:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.93/1.53 % (2737845)Instruction limit reached!
% 6.93/1.53 % (2737845)------------------------------
% 6.93/1.53 % (2737845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737845)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737845)Termination reason: Instruction limit
% 6.93/1.53 % (2737845)Termination phase: Saturation
% 6.93/1.53 % (2737845)Time elapsed: 0.322 s
% 6.93/1.53 % (2737845)Peak memory usage: 36 MB
% 6.93/1.53 % (2737845)Instructions burned: 1181 (million)
% 6.93/1.53 % (2737851)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1429925194:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 6.93/1.53 % (2737843)Instruction limit reached!
% 6.93/1.53 % (2737843)------------------------------
% 6.93/1.53 % (2737843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737843)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737843)Termination reason: Instruction limit
% 6.93/1.53 % (2737843)Termination phase: Finite model building preprocessing
% 6.93/1.53 % (2737843)Time elapsed: 0.414 s
% 6.93/1.53 % (2737843)Peak memory usage: 39 MB
% 6.93/1.53 % (2737843)Instructions burned: 867 (million)
% 6.93/1.53 % (2737853)fmb+10_1_sil=64000:random_seed=315794210:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 6.93/1.53 % Detected minimum model sizes of [51]
% 6.93/1.53 % Detected maximum model sizes of [max]
% 6.93/1.53 % (2737819)Cannot represent all propositional literals internally
% 6.93/1.53 % (2737819)Refutation not found, incomplete strategy
% 6.93/1.53 % (2737819)------------------------------
% 6.93/1.53 % (2737819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737819)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737819)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.53 % (2737819)Time elapsed: 0.714 s
% 6.93/1.53 % (2737819)Peak memory usage: 49 MB
% 6.93/1.53 % (2737819)Instructions burned: 1473 (million)
% 6.93/1.53 % (2737819)------------------------------
% 6.93/1.53 % (2737819)------------------------------
% 6.93/1.53 % (2737855)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4127602307:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 6.93/1.53 % (2737851)Instruction limit reached!
% 6.93/1.53 % (2737851)------------------------------
% 6.93/1.53 % (2737851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737851)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737851)Termination reason: Instruction limit
% 6.93/1.53 % (2737851)Termination phase: Saturation
% 6.93/1.53 % (2737851)Time elapsed: 0.225 s
% 6.93/1.53 % (2737851)Peak memory usage: 37 MB
% 6.93/1.53 % (2737851)Instructions burned: 882 (million)
% 6.93/1.53 % (2737857)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2828700946:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 6.93/1.53 % (2737848)Instruction limit reached!
% 6.93/1.53 % (2737848)------------------------------
% 6.93/1.53 % (2737848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737848)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737848)Termination reason: Instruction limit
% 6.93/1.53 % (2737848)Termination phase: Saturation
% 6.93/1.53 % (2737848)Time elapsed: 0.385 s
% 6.93/1.53 % (2737848)Peak memory usage: 36 MB
% 6.93/1.53 % (2737848)Instructions burned: 693 (million)
% 6.93/1.53 % (2737859)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4283131524:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 6.93/1.53 % (2737847)Instruction limit reached!
% 6.93/1.53 % (2737847)------------------------------
% 6.93/1.53 % (2737847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737847)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737847)Termination reason: Instruction limit
% 6.93/1.53 % (2737847)Termination phase: Finite model building preprocessing
% 6.93/1.53 % (2737847)Time elapsed: 0.427 s
% 6.93/1.53 % (2737847)Peak memory usage: 40 MB
% 6.93/1.53 % (2737847)Instructions burned: 890 (million)
% 6.93/1.53 % (2737861)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2053519080:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 6.93/1.53 % (2737857)Instruction limit reached!
% 6.93/1.53 % (2737857)------------------------------
% 6.93/1.53 % (2737857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.53 % (2737857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.53 % (2737857)CaDiCaL version: 2.1.3
% 6.93/1.53 % (2737857)Termination reason: Instruction limit
% 6.93/1.53 % (2737857)Termination phase: Finite model building preprocessing
% 6.93/1.53 % (2737857)Time elapsed: 0.240 s
% 6.93/1.53 % (2737857)Peak memory usage: 39 MB
% 6.93/1.53 % (2737857)Instructions burned: 925 (million)
% 6.93/1.53 % (2737863)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1656952268:i=6324_2988 on theBenchmark for (2988ds/6324Mi)
% 6.93/1.53 % (2737820) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2737814-2737820"...
% 6.93/1.53 % (2737820)...printing done.
% 6.93/1.53 % (2737820)Refutation found. Thanks to Tanya!
% 6.93/1.53 % SZS status Theorem for theBenchmark
% 6.93/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 6.93/1.54 % (2737820)------------------------------
% 6.93/1.54 % (2737820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.93/1.54 % (2737820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.54 % (2737820)CaDiCaL version: 2.1.3
% 6.93/1.54 % (2737820)Termination reason: Refutation
% 6.93/1.54 % (2737820)Time elapsed: 1.138 s
% 6.93/1.54 % (2737820)Peak memory usage: 49 MB
% 6.93/1.54 % (2737820)Instructions burned: 2137 (million)
% 6.93/1.54 % (2737814)Success in time 1.27 s
% 6.93/1.54 % Vampire exiting
%------------------------------------------------------------------------------