%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR082+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:02 AM UTC 2026
% Result : Theorem 9.70s 1.80s
% Output : Refutation 9.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 76 ( 19 unt; 5 def)
% Number of atoms : 173 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 178 ( 81 ~; 79 |; 6 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 6 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 58 ( 0 sgn 54 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_27) ).
fof(f5278,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__CognitiveAgent)
=> s__capability(s__Reasoning,s__agent__m,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5315) ).
fof(f5629,axiom,
! [X0] :
( s__instance(X0,s__Object)
=> ( s__instance(X0,s__SentientAgent)
=> s__capability(s__Perception,s__experiencer__m,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_5688) ).
fof(f6013,axiom,
s__subclass(s__Human,s__CognitiveAgent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_6087) ).
fof(f13268,axiom,
s__subclass(s__Human,s__SentientAgent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+3.ax',kb_SUMOcache_6051) ).
fof(f13275,axiom,
s__subclass(s__Human,s__Object),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+3.ax',kb_SUMOcache_6058) ).
fof(f14788,axiom,
s__instance(s__Jane8_1,s__Human),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f14789,conjecture,
? [X0,X1] :
( s__capability(s__Reasoning,X0,s__Jane8_1)
& s__capability(s__Perception,X1,s__Jane8_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO) ).
fof(f14790,negated_conjecture,
~ ? [X0,X1] :
( s__capability(s__Reasoning,X0,s__Jane8_1)
& s__capability(s__Perception,X1,s__Jane8_1) ),
inference(negated_conjecture,[status(cth)],[f14789]) ).
fof(f14884,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f14885,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(f14886,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,[],[f14885]) ).
fof(f19442,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f5278]) ).
fof(f19443,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f19442]) ).
fof(f19568,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(ennf_transformation,[],[f5629]) ).
fof(f19569,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(flattening,[],[f19568]) ).
fof(f19978,plain,
! [X0,X1] :
( ~ s__capability(s__Reasoning,X0,s__Jane8_1)
| ~ s__capability(s__Perception,X1,s__Jane8_1) ),
inference(ennf_transformation,[],[f14790]) ).
fof(f21283,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f14884]) ).
fof(f21284,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f14884]) ).
fof(f21285,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,[],[f14886]) ).
fof(f27207,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__instance(X0,s__CognitiveAgent)
| s__capability(s__Reasoning,s__agent__m,X0) ),
inference(cnf_transformation,[],[f19443]) ).
fof(f27698,plain,
! [X0] :
( ~ s__instance(X0,s__Object)
| ~ s__instance(X0,s__SentientAgent)
| s__capability(s__Perception,s__experiencer__m,X0) ),
inference(cnf_transformation,[],[f19569]) ).
fof(f28136,plain,
s__subclass(s__Human,s__CognitiveAgent),
inference(cnf_transformation,[],[f6013]) ).
fof(f35599,plain,
s__subclass(s__Human,s__SentientAgent),
inference(cnf_transformation,[],[f13268]) ).
fof(f35606,plain,
s__subclass(s__Human,s__Object),
inference(cnf_transformation,[],[f13275]) ).
fof(f37119,plain,
s__instance(s__Jane8_1,s__Human),
inference(cnf_transformation,[],[f14788]) ).
fof(f37120,plain,
! [X0,X1] :
( ~ s__capability(s__Perception,X1,s__Jane8_1)
| ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
inference(cnf_transformation,[],[f19978]) ).
fof(f37527,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(consistent_polarity_flipping,[],[f21284]) ).
fof(f37528,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass) ),
inference(consistent_polarity_flipping,[],[f21283]) ).
fof(f37529,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,[],[f21285]) ).
fof(f42877,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| s__instance(X0,s__CognitiveAgent)
| s__instance(X0,s__Object) ),
inference(consistent_polarity_flipping,[],[f27207]) ).
fof(f43267,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| s__instance(X0,s__SentientAgent)
| s__instance(X0,s__Object) ),
inference(consistent_polarity_flipping,[],[f27698]) ).
fof(f48771,plain,
~ s__instance(s__Jane8_1,s__Human),
inference(consistent_polarity_flipping,[],[f37119]) ).
fof(f48781,definition,
( spl478_1
<=> ! [X0] : ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[spl478_1])],[avatar_definition]) ).
fof(f48782,plain,
( ! [X0] : ~ s__capability(s__Reasoning,X0,s__Jane8_1)
| ~ spl478_1 ),
inference(avatar_component_clause,[],[f48781]) ).
fof(f48784,definition,
( spl478_2
<=> ! [X1] : ~ s__capability(s__Perception,X1,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[spl478_2])],[avatar_definition]) ).
fof(f48785,plain,
( ! [X1] : ~ s__capability(s__Perception,X1,s__Jane8_1)
| ~ spl478_2 ),
inference(avatar_component_clause,[],[f48784]) ).
fof(f48786,plain,
( spl478_1
| spl478_2 ),
inference(avatar_split_clause,[],[f37120,f48784,f48781]) ).
fof(f69829,definition,
( spl478_592
<=> s__instance(s__Jane8_1,s__Object) ),
introduced(definition,[new_symbols(definition,[spl478_592])],[avatar_definition]) ).
fof(f69830,plain,
( ~ s__instance(s__Jane8_1,s__Object)
| spl478_592 ),
inference(avatar_component_clause,[],[f69829]) ).
fof(f69831,plain,
( s__instance(s__Jane8_1,s__Object)
| ~ spl478_592 ),
inference(avatar_component_clause,[],[f69829]) ).
fof(f69833,definition,
( spl478_593
<=> s__instance(s__Jane8_1,s__SentientAgent) ),
introduced(definition,[new_symbols(definition,[spl478_593])],[avatar_definition]) ).
fof(f69835,plain,
( s__instance(s__Jane8_1,s__SentientAgent)
| ~ spl478_593 ),
inference(avatar_component_clause,[],[f69833]) ).
fof(f69837,plain,
( s__instance(s__Jane8_1,s__CognitiveAgent)
| s__instance(s__Jane8_1,s__Object)
| ~ spl478_1 ),
inference(resolution,[],[f48782,f42877]) ).
fof(f69839,definition,
( spl478_594
<=> s__instance(s__Jane8_1,s__CognitiveAgent) ),
introduced(definition,[new_symbols(definition,[spl478_594])],[avatar_definition]) ).
fof(f69841,plain,
( s__instance(s__Jane8_1,s__CognitiveAgent)
| ~ spl478_594 ),
inference(avatar_component_clause,[],[f69839]) ).
fof(f69844,plain,
( s__instance(s__Jane8_1,s__SentientAgent)
| s__instance(s__Jane8_1,s__Object)
| ~ spl478_2 ),
inference(resolution,[],[f48785,f43267]) ).
fof(f69845,plain,
( spl478_592
| spl478_593
| ~ spl478_2 ),
inference(avatar_split_clause,[],[f69844,f48784,f69833,f69829]) ).
fof(f95102,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,[],[f37529,f37527]) ).
fof(f95103,plain,
! [X2,X0,X1] :
( ~ s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f95102,f37528]) ).
fof(f95157,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Object)
| s__instance(s__Jane8_1,X0) )
| ~ spl478_592 ),
inference(resolution,[],[f95103,f69831]) ).
fof(f99086,plain,
( s__instance(s__Jane8_1,s__Human)
| ~ spl478_592 ),
inference(resolution,[],[f95157,f35606]) ).
fof(f99277,plain,
( $false
| ~ spl478_592 ),
inference(forward_subsumption_resolution,[],[f99086,f48771]) ).
fof(f99278,plain,
~ spl478_592,
inference(avatar_contradiction_clause,[],[f99277]) ).
fof(f99303,plain,
( ! [X0] :
( ~ s__subclass(X0,s__SentientAgent)
| s__instance(s__Jane8_1,X0) )
| ~ spl478_593 ),
inference(resolution,[],[f69835,f95103]) ).
fof(f99319,plain,
( s__instance(s__Jane8_1,s__Human)
| ~ spl478_593 ),
inference(resolution,[],[f99303,f35599]) ).
fof(f99322,plain,
( $false
| ~ spl478_593 ),
inference(forward_subsumption_resolution,[],[f99319,f48771]) ).
fof(f99323,plain,
~ spl478_593,
inference(avatar_contradiction_clause,[],[f99322]) ).
fof(f99324,plain,
( s__instance(s__Jane8_1,s__CognitiveAgent)
| ~ spl478_1
| spl478_592 ),
inference(forward_subsumption_resolution,[],[f69837,f69830]) ).
fof(f99325,plain,
( spl478_594
| ~ spl478_1
| spl478_592 ),
inference(avatar_split_clause,[],[f99324,f69829,f48781,f69839]) ).
fof(f99333,plain,
( ! [X0] :
( ~ s__subclass(X0,s__CognitiveAgent)
| s__instance(s__Jane8_1,X0) )
| ~ spl478_594 ),
inference(resolution,[],[f69841,f95103]) ).
fof(f99365,plain,
( s__instance(s__Jane8_1,s__Human)
| ~ spl478_594 ),
inference(resolution,[],[f99333,f28136]) ).
fof(f99366,plain,
( $false
| ~ spl478_594 ),
inference(forward_subsumption_resolution,[],[f99365,f48771]) ).
fof(f99367,plain,
~ spl478_594,
inference(avatar_contradiction_clause,[],[f99366]) ).
cnf(s1,plain,
( spl478_1
| spl478_2 ),
inference(sat_conversion,[],[f48786]) ).
cnf(s3623,plain,
( ~ spl478_2
| spl478_592
| spl478_593 ),
inference(sat_conversion,[],[f69845]) ).
cnf(s7638,plain,
~ spl478_592,
inference(sat_conversion,[],[f99278]) ).
cnf(s7645,plain,
~ spl478_593,
inference(sat_conversion,[],[f99323]) ).
cnf(s7646,plain,
( ~ spl478_1
| spl478_592
| spl478_594 ),
inference(sat_conversion,[],[f99325]) ).
cnf(s7649,plain,
~ spl478_594,
inference(sat_conversion,[],[f99367]) ).
cnf(s7650,plain,
( ~ spl478_1
| spl478_592 ),
inference(rat,[],[s7646,s7649]) ).
cnf(s7651,plain,
~ spl478_1,
inference(rat,[],[s7650,s7638]) ).
cnf(s8737,plain,
~ spl478_2,
inference(rat,[],[s3623,s7645,s7638]) ).
cnf(s9795,plain,
$false,
inference(rat,[],[s1,s8737,s7651]) ).
fof(f99368,plain,
$false,
inference(avatar_sat_refutation,[],[s9795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR082+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.16 % Computer : n001.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 22:38:04 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 Running first-order model finding
% 0.08/0.19 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
% 7.48/1.80 % (826419)Will run a generic schedule for satisfiability detection.
% 7.48/1.80 % (826429)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=620717449:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 7.48/1.80 % (826425)% WARNING: option uhcvi not known.
% 7.48/1.80 % (826424)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2770772751_2997 on theBenchmark for (2997ds/0Mi)
% 7.48/1.80 % (826425)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3837810264:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 7.48/1.80 % (826426)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2026047954:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 7.48/1.80 % (826427)dis+10_1_sil=32000:sp=arity:random_seed=4283827069:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 7.48/1.80 % (826428)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1664354630:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 7.48/1.80 % (826430)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2218926114:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 7.48/1.80 % (826429)Instruction limit reached!
% 7.48/1.80 % (826429)------------------------------
% 7.48/1.80 % (826429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.48/1.80 % (826429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.48/1.80 % (826429)CaDiCaL version: 2.1.3
% 7.48/1.80 % (826429)Termination reason: Instruction limit
% 7.48/1.80 % (826429)Termination phase: Clausification
% 7.48/1.80 % (826429)Time elapsed: 0.044 s
% 7.48/1.80 % (826429)Peak memory usage: 31 MB
% 7.48/1.80 % (826429)Instructions burned: 133 (million)
% 7.48/1.80 % (826438)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1759007972:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 7.48/1.80 % (826427)Instruction limit reached!
% 7.48/1.80 % (826427)------------------------------
% 7.48/1.80 % (826427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.48/1.80 % (826427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.48/1.80 % (826427)CaDiCaL version: 2.1.3
% 7.48/1.80 % (826427)Termination reason: Instruction limit
% 7.48/1.80 % (826427)Termination phase: Preprocessing 3
% 7.48/1.80 % (826427)Time elapsed: 0.063 s
% 7.48/1.80 % (826427)Peak memory usage: 29 MB
% 7.48/1.80 % (826427)Instructions burned: 105 (million)
% 7.48/1.80 % (826428)Instruction limit reached!
% 7.48/1.80 % (826428)------------------------------
% 7.48/1.80 % (826428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.48/1.80 % (826428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.48/1.80 % (826428)CaDiCaL version: 2.1.3
% 7.48/1.80 % (826428)Termination reason: Instruction limit
% 7.48/1.80 % (826428)Termination phase: NewCNF
% 7.48/1.80 % (826428)Time elapsed: 0.077 s
% 7.48/1.80 % (826428)Peak memory usage: 32 MB
% 7.48/1.80 % (826428)Instructions burned: 116 (million)
% 7.48/1.80 % (826440)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1829421081:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 7.48/1.80 % (826430)Instruction limit reached!
% 7.48/1.80 % (826430)------------------------------
% 7.48/1.80 % (826430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.48/1.80 % (826430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.48/1.80 % (826430)CaDiCaL version: 2.1.3
% 7.48/1.80 % (826430)Termination reason: Instruction limit
% 7.48/1.80 % (826430)Termination phase: Property scanning
% 7.48/1.80 % (826430)Time elapsed: 0.095 s
% 7.48/1.80 % (826430)Peak memory usage: 31 MB
% 7.48/1.80 % (826430)Instructions burned: 160 (million)
% 7.48/1.80 % (826441)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=2457652458:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 7.48/1.80 % (826443)ott-21_1_sil=16000:fs=off:random_seed=2668488427:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 7.48/1.80 % (826440)Instruction limit reached!
% 7.48/1.80 % (826440)------------------------------
% 7.48/1.80 % (826440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.48/1.80 % (826440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.48/1.80 % (826440)CaDiCaL version: 2.1.3
% 7.48/1.80 % (826440)Termination reason: Instruction limit
% 9.70/1.80 % (826440)Termination phase: Clausification
% 9.70/1.80 % (826440)Time elapsed: 0.076 s
% 9.70/1.80 % (826440)Peak memory usage: 31 MB
% 9.70/1.80 % (826440)Instructions burned: 133 (million)
% 9.70/1.80 % (826446)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1188735290:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 9.70/1.80 % (826443)Instruction limit reached!
% 9.70/1.80 % (826443)------------------------------
% 9.70/1.80 % (826443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826443)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826443)Termination reason: Instruction limit
% 9.70/1.80 % (826443)Termination phase: Property scanning
% 9.70/1.80 % (826443)Time elapsed: 0.101 s
% 9.70/1.80 % (826443)Peak memory usage: 31 MB
% 9.70/1.80 % (826443)Instructions burned: 182 (million)
% 9.70/1.80 % (826438)Instruction limit reached!
% 9.70/1.80 % (826438)------------------------------
% 9.70/1.80 % (826438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826438)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826438)Termination reason: Instruction limit
% 9.70/1.80 % (826438)Termination phase: Finite model building preprocessing
% 9.70/1.80 % (826438)Time elapsed: 0.191 s
% 9.70/1.80 % (826438)Peak memory usage: 42 MB
% 9.70/1.80 % (826438)Instructions burned: 717 (million)
% 9.70/1.80 % (826448)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1760389250:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 9.70/1.80 % (826450)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2161869383:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 9.70/1.80 % (826446)Instruction limit reached!
% 9.70/1.80 % (826446)------------------------------
% 9.70/1.80 % (826446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826446)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826446)Termination reason: Instruction limit
% 9.70/1.80 % (826446)Termination phase: Saturation
% 9.70/1.80 % (826446)Time elapsed: 0.233 s
% 9.70/1.80 % (826446)Peak memory usage: 35 MB
% 9.70/1.80 % (826446)Instructions burned: 478 (million)
% 9.70/1.80 % (826441)Instruction limit reached!
% 9.70/1.80 % (826441)------------------------------
% 9.70/1.80 % (826441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826441)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826441)Termination reason: Instruction limit
% 9.70/1.80 % (826441)Termination phase: Saturation
% 9.70/1.80 % (826441)Time elapsed: 0.337 s
% 9.70/1.80 % (826441)Peak memory usage: 40 MB
% 9.70/1.80 % (826441)Instructions burned: 684 (million)
% 9.70/1.80 % (826452)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2419674813:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 9.70/1.80 % (826454)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=3946308761:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 9.70/1.80 % (826450)Instruction limit reached!
% 9.70/1.80 % (826450)------------------------------
% 9.70/1.80 % (826450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826450)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826450)Termination reason: Instruction limit
% 9.70/1.80 % (826450)Termination phase: Saturation
% 9.70/1.80 % (826450)Time elapsed: 0.331 s
% 9.70/1.80 % (826450)Peak memory usage: 44 MB
% 9.70/1.80 % (826450)Instructions burned: 1181 (million)
% 9.70/1.80 % (826456)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3668908327:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 9.70/1.80 % (826448)Instruction limit reached!
% 9.70/1.80 % (826448)------------------------------
% 9.70/1.80 % (826448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826448)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826448)Termination reason: Instruction limit
% 9.70/1.80 % (826448)Termination phase: Finite model building preprocessing
% 9.70/1.80 % (826448)Time elapsed: 0.419 s
% 9.70/1.80 % (826448)Peak memory usage: 46 MB
% 9.70/1.80 % (826448)Instructions burned: 866 (million)
% 9.70/1.80 % (826458)fmb+10_1_sil=64000:random_seed=1871573173:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 9.70/1.80 % (826454)Instruction limit reached!
% 9.70/1.80 % (826454)------------------------------
% 9.70/1.80 % (826454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826454)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826454)Termination reason: Instruction limit
% 9.70/1.80 % (826454)Termination phase: Saturation
% 9.70/1.80 % (826454)Time elapsed: 0.350 s
% 9.70/1.80 % (826454)Peak memory usage: 42 MB
% 9.70/1.80 % (826454)Instructions burned: 692 (million)
% 9.70/1.80 % (826460)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3722693239:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 9.70/1.80 % (826456)Instruction limit reached!
% 9.70/1.80 % (826456)------------------------------
% 9.70/1.80 % (826456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826456)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826456)Termination reason: Instruction limit
% 9.70/1.80 % (826456)Termination phase: Saturation
% 9.70/1.80 % (826456)Time elapsed: 0.236 s
% 9.70/1.80 % (826456)Peak memory usage: 44 MB
% 9.70/1.80 % (826456)Instructions burned: 880 (million)
% 9.70/1.80 % (826462)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3275540570:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 9.70/1.80 % (826452)Instruction limit reached!
% 9.70/1.80 % (826452)------------------------------
% 9.70/1.80 % (826452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826452)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826452)Termination reason: Instruction limit
% 9.70/1.80 % (826452)Termination phase: Finite model building preprocessing
% 9.70/1.80 % (826452)Time elapsed: 0.426 s
% 9.70/1.80 % (826452)Peak memory usage: 47 MB
% 9.70/1.80 % (826452)Instructions burned: 891 (million)
% 9.70/1.80 % Detected minimum model sizes of [51]
% 9.70/1.80 % Detected maximum model sizes of [max]
% 9.70/1.80 % (826424)Cannot represent all propositional literals internally
% 9.70/1.80 % (826424)Refutation not found, incomplete strategy
% 9.70/1.80 % (826424)------------------------------
% 9.70/1.80 % (826424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826424)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826424)Termination reason: Refutation not found, incomplete strategy
% 9.70/1.80 % (826424)Time elapsed: 0.885 s
% 9.70/1.80 % (826424)Peak memory usage: 59 MB
% 9.70/1.80 % (826424)Instructions burned: 1864 (million)
% 9.70/1.80 % (826464)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3670660936:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 9.70/1.80 % (826424)------------------------------
% 9.70/1.80 % (826424)------------------------------
% 9.70/1.80 % (826466)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1724671552:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 9.70/1.80 % (826462)Instruction limit reached!
% 9.70/1.80 % (826462)------------------------------
% 9.70/1.80 % (826462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.80 % (826462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.80 % (826462)CaDiCaL version: 2.1.3
% 9.70/1.80 % (826462)Termination reason: Instruction limit
% 9.70/1.80 % (826462)Termination phase: Finite model building preprocessing
% 9.70/1.80 % (826462)Time elapsed: 0.301 s
% 9.70/1.80 % (826462)Peak memory usage: 47 MB
% 9.70/1.80 % (826462)Instructions burned: 923 (million)
% 9.70/1.80 % (826468)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3493019047:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 9.70/1.80 % (826425) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-826419-826425"...
% 9.70/1.80 % (826425)...printing done.
% 9.70/1.80 % (826425)Refutation found. Thanks to Tanya!
% 9.70/1.80 % SZS status Theorem for theBenchmark
% 9.70/1.80 % SZS output start Proof for theBenchmark
% See solution above
% 9.70/1.82 % (826425)------------------------------
% 9.70/1.82 % (826425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.70/1.82 % (826425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.70/1.82 % (826425)CaDiCaL version: 2.1.3
% 9.70/1.82 % (826425)Termination reason: Refutation
% 9.70/1.82 % (826425)Time elapsed: 1.253 s
% 9.70/1.82 % (826425)Peak memory usage: 67 MB
% 9.70/1.82 % (826425)Instructions burned: 2394 (million)
% 9.70/1.82 % (826419)Success in time 1.596 s
% 9.70/1.82 % Vampire exiting
%------------------------------------------------------------------------------