%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR188+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:46:26 AM UTC 2026
% Result : Theorem 144.59s 40.14s
% Output : Refutation 144.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 29
% Syntax : Number of formulae : 140 ( 56 unt; 6 def)
% Number of atoms : 294 ( 4 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 269 ( 115 ~; 110 |; 24 &)
% ( 11 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 7 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 16 con; 0-1 aty)
% Number of variables : 117 ( 0 sgn 109 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA12) ).
fof(f5,axiom,
! [X0,X1] :
( p__d__disjoint(X0,X1)
<=> ! [X2] :
( ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA15) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA178) ).
fof(f233,axiom,
p__d__subclass(c__Process,c__Physical),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA324) ).
fof(f1582,axiom,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2309) ).
fof(f1585,axiom,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2312) ).
fof(f1591,axiom,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2318) ).
fof(f1594,axiom,
p__d__subclass(c__Death,c__OrganismProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2321) ).
fof(f1618,axiom,
p__d__disjoint(c__PathologicProcess,c__PhysiologicProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2347) ).
fof(f1620,axiom,
p__d__subclass(c__Injuring,c__PathologicProcess),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2349) ).
fof(f1622,axiom,
! [X0] :
( p__d__instance(X0,c__Process)
=> ( p__d__instance(X0,c__Injuring)
<=> ( p__d__instance(X0,c__Damaging)
& ? [X1] :
( p__d__instance(X1,c__Organism)
& p__patient(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2351) ).
fof(f1827,axiom,
p__d__subclass(c__Destruction,c__Damaging),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2605) ).
fof(f1828,axiom,
! [X0] :
( p__d__instance(X0,c__Process)
=> ( p__d__instance(X0,c__Destruction)
<=> ? [X1] :
( p__d__instance(X1,c__Physical)
& p__patient(X0,X1)
& p__time(X1,f__BeginFn1(f__WhenFn1(X0)))
& ~ p__time(X1,f__EndFn1(f__WhenFn1(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2606) ).
fof(f1829,axiom,
p__d__subclass(c__Killing,c__Destruction),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2607) ).
fof(f1830,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Killing)
& p__agent(X0,X1)
& p__patient(X0,X2) )
=> ( p__d__instance(X1,c__Organism)
& p__d__instance(X2,c__Organism) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2608) ).
fof(f1859,axiom,
p__d__subclass(c__InternalChange,c__Process),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA2644) ).
fof(f4834,axiom,
p__d__subclass(c__Suicide,c__Killing),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',miloA2636) ).
fof(f4835,axiom,
! [X0] :
( p__d__instance(X0,c__Suicide)
=> ? [X1] :
( p__d__instance(X1,c__Agent)
& p__agent(X0,X1)
& p__experiencer(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',miloA2637) ).
fof(f6883,axiom,
! [X0,X1] :
( p__agent(X0,X1)
=> ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',typeA30) ).
fof(f6887,axiom,
! [X0,X1] :
( p__patient(X0,X1)
=> p__d__instance(X0,c__Process) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',typeA34) ).
fof(f7433,conjecture,
c__Death != c__Killing,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',negatedEqualEvent0014) ).
fof(f7434,negated_conjecture,
~ ( c__Death != c__Killing ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7440,plain,
c__Death = c__Killing,
inference(flattening,[],[f7434]) ).
fof(f7450,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7451,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7450]) ).
fof(f7454,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7455,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7454]) ).
fof(f7504,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f8089,plain,
! [X0] :
( ( p__d__instance(X0,c__Injuring)
<=> ( p__d__instance(X0,c__Damaging)
& ? [X1] :
( p__d__instance(X1,c__Organism)
& p__patient(X0,X1) ) ) )
| ~ p__d__instance(X0,c__Process) ),
inference(ennf_transformation,[],[f1622]) ).
fof(f8184,plain,
! [X0] :
( ( p__d__instance(X0,c__Destruction)
<=> ? [X1] :
( p__d__instance(X1,c__Physical)
& p__patient(X0,X1)
& p__time(X1,f__BeginFn1(f__WhenFn1(X0)))
& ~ p__time(X1,f__EndFn1(f__WhenFn1(X0))) ) )
| ~ p__d__instance(X0,c__Process) ),
inference(ennf_transformation,[],[f1828]) ).
fof(f8185,plain,
! [X0,X1,X2] :
( ( p__d__instance(X1,c__Organism)
& p__d__instance(X2,c__Organism) )
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__Killing)
| ~ p__agent(X0,X1)
| ~ p__patient(X0,X2) ),
inference(ennf_transformation,[],[f1830]) ).
fof(f8186,plain,
! [X0,X1,X2] :
( ( p__d__instance(X1,c__Organism)
& p__d__instance(X2,c__Organism) )
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__Killing)
| ~ p__agent(X0,X1)
| ~ p__patient(X0,X2) ),
inference(flattening,[],[f8185]) ).
fof(f9451,plain,
! [X0] :
( ? [X1] :
( p__d__instance(X1,c__Agent)
& p__agent(X0,X1)
& p__experiencer(X0,X1) )
| ~ p__d__instance(X0,c__Suicide) ),
inference(ennf_transformation,[],[f4835]) ).
fof(f11056,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) )
| ~ p__agent(X0,X1) ),
inference(ennf_transformation,[],[f6883]) ).
fof(f11060,plain,
! [X0,X1] :
( p__d__instance(X0,c__Process)
| ~ p__patient(X0,X1) ),
inference(ennf_transformation,[],[f6887]) ).
fof(f11602,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2)
| p__d__subclass(X0,X2) ),
inference(cnf_transformation,[],[f7451]) ).
fof(f11604,plain,
! [X2,X0,X1] :
( ~ p__d__subclass(X1,X2)
| ~ p__d__instance(X0,X1)
| p__d__instance(X0,X2) ),
inference(cnf_transformation,[],[f7455]) ).
fof(f11605,plain,
! [X2,X0,X1] :
( ~ p__d__disjoint(X0,X1)
| ~ p__d__instance(X2,X0)
| ~ p__d__instance(X2,X1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f11883,plain,
! [X0] :
( ~ p__d__subclass(X0,c__Entity)
| p__d__instance(sK34(X0),X0) ),
inference(cnf_transformation,[],[f7504]) ).
fof(f11886,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f12045,plain,
p__d__subclass(c__Process,c__Physical),
inference(cnf_transformation,[],[f233]) ).
fof(f13647,plain,
p__d__subclass(c__BiologicalProcess,c__InternalChange),
inference(cnf_transformation,[],[f1582]) ).
fof(f13651,plain,
p__d__subclass(c__PhysiologicProcess,c__BiologicalProcess),
inference(cnf_transformation,[],[f1585]) ).
fof(f13659,plain,
p__d__subclass(c__OrganismProcess,c__PhysiologicProcess),
inference(cnf_transformation,[],[f1591]) ).
fof(f13663,plain,
p__d__subclass(c__Death,c__OrganismProcess),
inference(cnf_transformation,[],[f1594]) ).
fof(f13695,plain,
p__d__disjoint(c__PathologicProcess,c__PhysiologicProcess),
inference(cnf_transformation,[],[f1618]) ).
fof(f13700,plain,
p__d__subclass(c__Injuring,c__PathologicProcess),
inference(cnf_transformation,[],[f1620]) ).
fof(f13702,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__patient(X0,X1)
| ~ p__d__instance(X1,c__Organism)
| ~ p__d__instance(X0,c__Damaging)
| p__d__instance(X0,c__Injuring) ),
inference(cnf_transformation,[],[f8089]) ).
fof(f14018,plain,
p__d__subclass(c__Destruction,c__Damaging),
inference(cnf_transformation,[],[f1827]) ).
fof(f14021,plain,
! [X0] :
( ~ p__d__instance(X0,c__Process)
| p__patient(X0,sK227(X0))
| ~ p__d__instance(X0,c__Destruction) ),
inference(cnf_transformation,[],[f8184]) ).
fof(f14024,plain,
p__d__subclass(c__Killing,c__Destruction),
inference(cnf_transformation,[],[f1829]) ).
fof(f14025,plain,
! [X2,X0,X1] :
( ~ p__patient(X0,X2)
| ~ p__agent(X0,X1)
| ~ p__d__instance(X0,c__Killing)
| ~ p__d__instance(X1,c__Agent)
| p__d__instance(X2,c__Organism) ),
inference(cnf_transformation,[],[f8186]) ).
fof(f14072,plain,
p__d__subclass(c__InternalChange,c__Process),
inference(cnf_transformation,[],[f1859]) ).
fof(f18259,plain,
p__d__subclass(c__Suicide,c__Killing),
inference(cnf_transformation,[],[f4834]) ).
fof(f18261,plain,
! [X0] :
( ~ p__d__instance(X0,c__Suicide)
| p__agent(X0,sK1001(X0)) ),
inference(cnf_transformation,[],[f9451]) ).
fof(f21330,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| p__d__instance(X1,c__Agent) ),
inference(cnf_transformation,[],[f11056]) ).
fof(f21336,plain,
! [X0,X1] :
( ~ p__patient(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[],[f11060]) ).
fof(f22366,plain,
c__Death = c__Killing,
inference(cnf_transformation,[],[f7440]) ).
fof(f22368,plain,
p__d__subclass(c__Killing,c__OrganismProcess),
inference(definition_unfolding,[],[f13663,f22366]) ).
fof(f22943,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| p__patient(X0,X1)
| ~ p__d__instance(X1,c__Organism)
| ~ p__d__instance(X0,c__Damaging)
| p__d__instance(X0,c__Injuring) ),
inference(consistent_polarity_flipping,[],[f13702]) ).
fof(f23046,plain,
! [X0] :
( ~ p__patient(X0,sK227(X0))
| ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X0,c__Destruction) ),
inference(consistent_polarity_flipping,[],[f14021]) ).
fof(f23048,plain,
! [X2,X0,X1] :
( p__patient(X0,X2)
| p__agent(X0,X1)
| ~ p__d__instance(X0,c__Killing)
| ~ p__d__instance(X1,c__Agent)
| p__d__instance(X2,c__Organism) ),
inference(consistent_polarity_flipping,[],[f14025]) ).
fof(f23757,plain,
! [X0] :
( ~ p__d__instance(X0,c__Suicide)
| ~ p__agent(X0,sK1001(X0)) ),
inference(consistent_polarity_flipping,[],[f18261]) ).
fof(f24885,plain,
! [X0,X1] :
( p__agent(X0,X1)
| p__d__instance(X1,c__Agent) ),
inference(consistent_polarity_flipping,[],[f21330]) ).
fof(f24887,plain,
! [X0,X1] :
( p__patient(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(consistent_polarity_flipping,[],[f21336]) ).
fof(f30591,plain,
! [X0] :
( ~ p__d__subclass(c__OrganismProcess,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f11602,f22368]) ).
fof(f32146,plain,
! [X0] :
( ~ p__d__subclass(c__Killing,X0)
| p__d__subclass(c__Suicide,X0) ),
inference(resolution,[],[f11602,f18259]) ).
fof(f57802,plain,
! [X0] :
( ~ p__d__instance(X0,c__Injuring)
| p__d__instance(X0,c__PathologicProcess) ),
inference(resolution,[],[f11604,f13700]) ).
fof(f57954,plain,
! [X0] :
( ~ p__d__instance(X0,c__Destruction)
| p__d__instance(X0,c__Damaging) ),
inference(resolution,[],[f11604,f14018]) ).
fof(f57956,plain,
! [X0] :
( ~ p__d__instance(X0,c__Killing)
| p__d__instance(X0,c__Destruction) ),
inference(resolution,[],[f11604,f14024]) ).
fof(f59510,plain,
! [X0] :
( ~ p__d__instance(X0,c__Suicide)
| p__d__instance(X0,c__Killing) ),
inference(resolution,[],[f11604,f18259]) ).
fof(f60136,plain,
p__d__subclass(c__Killing,c__PhysiologicProcess),
inference(resolution,[],[f30591,f13659]) ).
fof(f60140,plain,
! [X0] :
( ~ p__d__subclass(c__PhysiologicProcess,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f60136,f11602]) ).
fof(f60150,plain,
p__d__subclass(c__Killing,c__BiologicalProcess),
inference(resolution,[],[f60140,f13651]) ).
fof(f60154,plain,
! [X0] :
( ~ p__d__subclass(c__BiologicalProcess,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f60150,f11602]) ).
fof(f60165,plain,
p__d__subclass(c__Killing,c__InternalChange),
inference(resolution,[],[f60154,f13647]) ).
fof(f60169,plain,
! [X0] :
( ~ p__d__subclass(c__InternalChange,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f60165,f11602]) ).
fof(f60179,plain,
p__d__subclass(c__Killing,c__Process),
inference(resolution,[],[f60169,f14072]) ).
fof(f60183,plain,
! [X0] :
( ~ p__d__subclass(c__Process,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f60179,f11602]) ).
fof(f60206,plain,
p__d__subclass(c__Killing,c__Physical),
inference(resolution,[],[f60183,f12045]) ).
fof(f60210,plain,
! [X0] :
( ~ p__d__subclass(c__Physical,X0)
| p__d__subclass(c__Killing,X0) ),
inference(resolution,[],[f60206,f11602]) ).
fof(f60233,plain,
p__d__subclass(c__Killing,c__Entity),
inference(resolution,[],[f60210,f11886]) ).
fof(f60355,plain,
! [X0] :
( ~ p__d__instance(X0,c__PathologicProcess)
| ~ p__d__instance(X0,c__PhysiologicProcess) ),
inference(resolution,[],[f11605,f13695]) ).
fof(f121364,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Damaging)
| ~ p__d__instance(X1,c__Organism)
| p__patient(X0,X1)
| p__d__instance(X0,c__Injuring) ),
inference(forward_subsumption_resolution,[],[f22943,f24887]) ).
fof(f121410,plain,
! [X2,X0,X1] :
( ~ p__d__instance(X0,c__Killing)
| p__agent(X0,X1)
| p__patient(X0,X2)
| p__d__instance(X2,c__Organism) ),
inference(forward_subsumption_resolution,[],[f23048,f24885]) ).
fof(f363749,plain,
p__d__subclass(c__Suicide,c__Entity),
inference(resolution,[],[f32146,f60233]) ).
fof(f363751,plain,
p__d__subclass(c__Suicide,c__Process),
inference(resolution,[],[f32146,f60179]) ).
fof(f363754,plain,
p__d__subclass(c__Suicide,c__PhysiologicProcess),
inference(resolution,[],[f32146,f60136]) ).
fof(f363845,plain,
! [X0] :
( ~ p__d__instance(X0,c__Suicide)
| p__d__instance(X0,c__PhysiologicProcess) ),
inference(resolution,[],[f363754,f11604]) ).
fof(f364303,plain,
! [X0] :
( ~ p__d__instance(X0,c__Suicide)
| p__d__instance(X0,c__Process) ),
inference(resolution,[],[f363751,f11604]) ).
fof(f364546,plain,
p__d__instance(sK34(c__Suicide),c__Suicide),
inference(resolution,[],[f363749,f11883]) ).
fof(f364802,plain,
~ p__agent(sK34(c__Suicide),sK1001(sK34(c__Suicide))),
inference(resolution,[],[f364546,f23757]) ).
fof(f365544,plain,
p__d__instance(sK34(c__Suicide),c__PhysiologicProcess),
inference(resolution,[],[f363845,f364546]) ).
fof(f366894,plain,
p__d__instance(sK34(c__Suicide),c__Process),
inference(resolution,[],[f364303,f364546]) ).
fof(f376278,definition,
( spl1237_26517
<=> p__d__instance(sK34(c__Suicide),c__PathologicProcess) ),
introduced(definition,[new_symbols(definition,[spl1237_26517])],[avatar_definition]) ).
fof(f376279,plain,
( p__d__instance(sK34(c__Suicide),c__PathologicProcess)
| ~ spl1237_26517 ),
inference(avatar_component_clause,[],[f376278]) ).
fof(f465472,plain,
p__d__instance(sK34(c__Suicide),c__Killing),
inference(resolution,[],[f59510,f364546]) ).
fof(f465639,plain,
p__d__instance(sK34(c__Suicide),c__Destruction),
inference(resolution,[],[f465472,f57956]) ).
fof(f465695,plain,
! [X0,X1] :
( p__agent(sK34(c__Suicide),X0)
| p__patient(sK34(c__Suicide),X1)
| p__d__instance(X1,c__Organism) ),
inference(resolution,[],[f465472,f121410]) ).
fof(f465712,definition,
( spl1237_30674
<=> ! [X1] :
( p__patient(sK34(c__Suicide),X1)
| p__d__instance(X1,c__Organism) ) ),
introduced(definition,[new_symbols(definition,[spl1237_30674])],[avatar_definition]) ).
fof(f465713,plain,
( ! [X1] :
( p__patient(sK34(c__Suicide),X1)
| p__d__instance(X1,c__Organism) )
| ~ spl1237_30674 ),
inference(avatar_component_clause,[],[f465712]) ).
fof(f465715,definition,
( spl1237_30675
<=> ! [X0] : p__agent(sK34(c__Suicide),X0) ),
introduced(definition,[new_symbols(definition,[spl1237_30675])],[avatar_definition]) ).
fof(f465716,plain,
( ! [X0] : p__agent(sK34(c__Suicide),X0)
| ~ spl1237_30675 ),
inference(avatar_component_clause,[],[f465715]) ).
fof(f465717,plain,
( spl1237_30674
| spl1237_30675 ),
inference(avatar_split_clause,[],[f465695,f465715,f465712]) ).
fof(f465719,definition,
( spl1237_30676
<=> ! [X1] : p__patient(sK34(c__Suicide),X1) ),
introduced(definition,[new_symbols(definition,[spl1237_30676])],[avatar_definition]) ).
fof(f465720,plain,
( ! [X1] : p__patient(sK34(c__Suicide),X1)
| ~ spl1237_30676 ),
inference(avatar_component_clause,[],[f465719]) ).
fof(f465912,plain,
p__d__instance(sK34(c__Suicide),c__Damaging),
inference(resolution,[],[f465639,f57954]) ).
fof(f466046,plain,
( ~ p__d__instance(sK34(c__Suicide),c__Process)
| ~ p__d__instance(sK34(c__Suicide),c__Destruction)
| ~ spl1237_30676 ),
inference(resolution,[],[f465720,f23046]) ).
fof(f466063,plain,
( ~ p__d__instance(sK34(c__Suicide),c__Destruction)
| ~ spl1237_30676 ),
inference(forward_subsumption_resolution,[],[f466046,f366894]) ).
fof(f466075,plain,
( $false
| ~ spl1237_30676 ),
inference(forward_subsumption_resolution,[],[f466063,f465639]) ).
fof(f466076,plain,
~ spl1237_30676,
inference(avatar_contradiction_clause,[],[f466075]) ).
fof(f467539,plain,
! [X0] :
( ~ p__d__instance(X0,c__Organism)
| p__patient(sK34(c__Suicide),X0)
| p__d__instance(sK34(c__Suicide),c__Injuring) ),
inference(resolution,[],[f465912,f121364]) ).
fof(f467549,definition,
( spl1237_30704
<=> p__d__instance(sK34(c__Suicide),c__Injuring) ),
introduced(definition,[new_symbols(definition,[spl1237_30704])],[avatar_definition]) ).
fof(f467551,plain,
( p__d__instance(sK34(c__Suicide),c__Injuring)
| ~ spl1237_30704 ),
inference(avatar_component_clause,[],[f467549]) ).
fof(f467553,definition,
( spl1237_30705
<=> ! [X0] :
( ~ p__d__instance(X0,c__Organism)
| p__patient(sK34(c__Suicide),X0) ) ),
introduced(definition,[new_symbols(definition,[spl1237_30705])],[avatar_definition]) ).
fof(f467554,plain,
( ! [X0] :
( ~ p__d__instance(X0,c__Organism)
| p__patient(sK34(c__Suicide),X0) )
| ~ spl1237_30705 ),
inference(avatar_component_clause,[],[f467553]) ).
fof(f467555,plain,
( spl1237_30704
| spl1237_30705 ),
inference(avatar_split_clause,[],[f467539,f467553,f467549]) ).
fof(f467815,plain,
( p__d__instance(sK34(c__Suicide),c__PathologicProcess)
| ~ spl1237_30704 ),
inference(resolution,[],[f467551,f57802]) ).
fof(f483970,plain,
( ! [X0] : p__patient(sK34(c__Suicide),X0)
| ~ spl1237_30674
| ~ spl1237_30705 ),
inference(forward_subsumption_resolution,[],[f467554,f465713]) ).
fof(f483971,plain,
( spl1237_30676
| ~ spl1237_30674
| ~ spl1237_30705 ),
inference(avatar_split_clause,[],[f483970,f467553,f465712,f465719]) ).
fof(f483972,plain,
( $false
| ~ spl1237_30675 ),
inference(backward_subsumption_resolution,[],[f364802,f465716]) ).
fof(f483982,plain,
~ spl1237_30675,
inference(avatar_contradiction_clause,[],[f483972]) ).
fof(f483988,plain,
( spl1237_26517
| ~ spl1237_30704 ),
inference(avatar_split_clause,[],[f467815,f467549,f376278]) ).
fof(f483990,plain,
( ~ p__d__instance(sK34(c__Suicide),c__PhysiologicProcess)
| ~ spl1237_26517 ),
inference(resolution,[],[f376279,f60355]) ).
fof(f484000,plain,
( $false
| ~ spl1237_26517 ),
inference(forward_subsumption_resolution,[],[f483990,f365544]) ).
fof(f484001,plain,
~ spl1237_26517,
inference(avatar_contradiction_clause,[],[f484000]) ).
cnf(s35001,plain,
( spl1237_30674
| spl1237_30675 ),
inference(sat_conversion,[],[f465717]) ).
cnf(s35013,plain,
~ spl1237_30676,
inference(sat_conversion,[],[f466076]) ).
cnf(s35027,plain,
( spl1237_30704
| spl1237_30705 ),
inference(sat_conversion,[],[f467555]) ).
cnf(s35279,plain,
( ~ spl1237_30674
| spl1237_30676
| ~ spl1237_30705 ),
inference(sat_conversion,[],[f483971]) ).
cnf(s35280,plain,
~ spl1237_30675,
inference(sat_conversion,[],[f483982]) ).
cnf(s35283,plain,
( spl1237_26517
| ~ spl1237_30704 ),
inference(sat_conversion,[],[f483988]) ).
cnf(s35285,plain,
~ spl1237_26517,
inference(sat_conversion,[],[f484001]) ).
cnf(s35286,plain,
~ spl1237_30704,
inference(rat,[],[s35283,s35285]) ).
cnf(s35293,plain,
spl1237_30705,
inference(rat,[],[s35027,s35286]) ).
cnf(s35295,plain,
~ spl1237_30674,
inference(rat,[],[s35279,s35293,s35013]) ).
cnf(s35300,plain,
$false,
inference(rat,[],[s35001,s35280,s35295]) ).
fof(f484002,plain,
$false,
inference(avatar_sat_refutation,[],[s35300]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR188+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:40:41 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.74/2.50 % (2972761)Will run a generic schedule for satisfiability detection.
% 15.74/2.50 % (2972767)% WARNING: option uhcvi not known.
% 15.74/2.50 % (2972767)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=148854888:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.74/2.50 % (2972766)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3554137877_2999 on theBenchmark for (2999ds/0Mi)
% 15.74/2.50 % (2972768)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3520900402:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.74/2.50 % (2972769)dis+10_1_sil=32000:sp=arity:random_seed=1621761923:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.74/2.50 % (2972770)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=658845257:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.74/2.50 % (2972771)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3553031159:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.74/2.50 % (2972772)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=739547312:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.74/2.50 % (2972769)Instruction limit reached!
% 15.74/2.50 % (2972769)------------------------------
% 15.74/2.50 % (2972769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.74/2.50 % (2972769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/2.50 % (2972769)CaDiCaL version: 2.1.3
% 15.74/2.50 % (2972769)Termination reason: Instruction limit
% 15.74/2.50 % (2972769)Termination phase: Clausification
% 15.74/2.50 % (2972769)Time elapsed: 0.064 s
% 15.74/2.50 % (2972769)Peak memory usage: 23 MB
% 15.74/2.50 % (2972769)Instructions burned: 104 (million)
% 15.74/2.50 % (2972770)Instruction limit reached!
% 15.74/2.50 % (2972770)------------------------------
% 15.74/2.50 % (2972770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.74/2.50 % (2972770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/2.50 % (2972770)CaDiCaL version: 2.1.3
% 15.74/2.50 % (2972770)Termination reason: Instruction limit
% 15.74/2.50 % (2972770)Termination phase: NewCNF
% 15.74/2.50 % (2972770)Time elapsed: 0.067 s
% 15.74/2.50 % (2972770)Peak memory usage: 23 MB
% 15.74/2.50 % (2972770)Instructions burned: 118 (million)
% 15.74/2.50 % (2972771)Instruction limit reached!
% 15.74/2.50 % (2972771)------------------------------
% 15.74/2.50 % (2972771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.74/2.50 % (2972771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/2.50 % (2972771)CaDiCaL version: 2.1.3
% 15.74/2.50 % (2972771)Termination reason: Instruction limit
% 15.74/2.50 % (2972771)Termination phase: Property scanning
% 15.74/2.50 % (2972771)Time elapsed: 0.082 s
% 15.74/2.50 % (2972771)Peak memory usage: 24 MB
% 15.74/2.50 % (2972771)Instructions burned: 133 (million)
% 15.74/2.50 % (2972780)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2724508157:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.74/2.50 % (2972781)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2266332902:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.74/2.50 % (2972772)Instruction limit reached!
% 15.74/2.50 % (2972772)------------------------------
% 15.74/2.50 % (2972772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.74/2.50 % (2972772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/2.50 % (2972772)CaDiCaL version: 2.1.3
% 15.74/2.50 % (2972772)Termination reason: Instruction limit
% 15.74/2.50 % (2972772)Termination phase: Property scanning
% 15.74/2.50 % (2972772)Time elapsed: 0.094 s
% 15.74/2.50 % (2972772)Peak memory usage: 24 MB
% 15.74/2.50 % (2972772)Instructions burned: 161 (million)
% 15.74/2.50 % (2972782)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=3601707047:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.74/2.50 % (2972785)ott-21_1_sil=16000:fs=off:random_seed=3825935284:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.74/2.50 % (2972781)Instruction limit reached!
% 15.74/2.50 % (2972781)------------------------------
% 15.74/2.50 % (2972781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.74/2.50 % (2972781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972781)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972781)Termination reason: Instruction limit
% 39.84/6.01 % (2972781)Termination phase: Property scanning
% 39.84/6.01 % (2972781)Time elapsed: 0.082 s
% 39.84/6.01 % (2972781)Peak memory usage: 24 MB
% 39.84/6.01 % (2972781)Instructions burned: 132 (million)
% 39.84/6.01 % (2972788)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1298480138:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 39.84/6.01 % (2972785)Instruction limit reached!
% 39.84/6.01 % (2972785)------------------------------
% 39.84/6.01 % (2972785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972785)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972785)Termination reason: Instruction limit
% 39.84/6.01 % (2972785)Termination phase: Function definition elimination
% 39.84/6.01 % (2972785)Time elapsed: 0.103 s
% 39.84/6.01 % (2972785)Peak memory usage: 24 MB
% 39.84/6.01 % (2972785)Instructions burned: 180 (million)
% 39.84/6.01 % (2972790)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=538801680:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 39.84/6.01 % (2972780)Instruction limit reached!
% 39.84/6.01 % (2972780)------------------------------
% 39.84/6.01 % (2972780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972780)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972780)Termination reason: Instruction limit
% 39.84/6.01 % (2972780)Termination phase: Finite model building preprocessing
% 39.84/6.01 % (2972780)Time elapsed: 0.351 s
% 39.84/6.01 % (2972780)Peak memory usage: 36 MB
% 39.84/6.01 % (2972780)Instructions burned: 715 (million)
% 39.84/6.01 % (2972782)Instruction limit reached!
% 39.84/6.01 % (2972782)------------------------------
% 39.84/6.01 % (2972782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972782)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972782)Termination reason: Instruction limit
% 39.84/6.01 % (2972782)Termination phase: Saturation
% 39.84/6.01 % (2972782)Time elapsed: 0.346 s
% 39.84/6.01 % (2972782)Peak memory usage: 31 MB
% 39.84/6.01 % (2972782)Instructions burned: 686 (million)
% 39.84/6.01 % (2972788)Instruction limit reached!
% 39.84/6.01 % (2972788)------------------------------
% 39.84/6.01 % (2972788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972788)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972788)Termination reason: Instruction limit
% 39.84/6.01 % (2972788)Termination phase: Saturation
% 39.84/6.01 % (2972788)Time elapsed: 0.262 s
% 39.84/6.01 % (2972788)Peak memory usage: 30 MB
% 39.84/6.01 % (2972788)Instructions burned: 478 (million)
% 39.84/6.01 % (2972792)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3649741829:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 39.84/6.01 % (2972793)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=519389586:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 39.84/6.01 % (2972794)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=2948918733: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)
% 39.84/6.01 % TRYING [1]
% 39.84/6.01 % (2972790)Instruction limit reached!
% 39.84/6.01 % (2972790)------------------------------
% 39.84/6.01 % (2972790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.84/6.01 % (2972790)CaDiCaL version: 2.1.3
% 39.84/6.01 % (2972790)Termination reason: Instruction limit
% 39.84/6.01 % (2972790)Termination phase: Finite model building preprocessing
% 39.84/6.01 % (2972790)Time elapsed: 0.420 s
% 39.84/6.01 % (2972790)Peak memory usage: 37 MB
% 39.84/6.01 % (2972790)Instructions burned: 867 (million)
% 39.84/6.01 % TRYING [2]
% 39.84/6.01 % (2972798)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=801855744:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 39.84/6.01 % (2972794)Instruction limit reached!
% 39.84/6.01 % (2972794)------------------------------
% 39.84/6.01 % (2972794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.84/6.01 % (2972794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972794)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972794)Termination reason: Instruction limit
% 91.22/13.19 % (2972794)Termination phase: Saturation
% 91.22/13.19 % (2972794)Time elapsed: 0.378 s
% 91.22/13.19 % (2972794)Peak memory usage: 34 MB
% 91.22/13.19 % (2972794)Instructions burned: 693 (million)
% 91.22/13.19 % TRYING [3]
% 91.22/13.19 % (2972800)fmb+10_1_sil=64000:random_seed=588017244:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 91.22/13.19 % (2972793)Instruction limit reached!
% 91.22/13.19 % (2972793)------------------------------
% 91.22/13.19 % (2972793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.22/13.19 % (2972793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972793)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972793)Termination reason: Instruction limit
% 91.22/13.19 % (2972793)Termination phase: Finite model building preprocessing
% 91.22/13.19 % (2972793)Time elapsed: 0.436 s
% 91.22/13.19 % (2972793)Peak memory usage: 38 MB
% 91.22/13.19 % (2972793)Instructions burned: 890 (million)
% 91.22/13.19 % (2972802)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=531318589:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 91.22/13.19 % (2972792)Instruction limit reached!
% 91.22/13.19 % (2972792)------------------------------
% 91.22/13.19 % (2972792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.22/13.19 % (2972792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972792)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972792)Termination reason: Instruction limit
% 91.22/13.19 % (2972792)Termination phase: Saturation
% 91.22/13.19 % (2972792)Time elapsed: 0.615 s
% 91.22/13.19 % (2972792)Peak memory usage: 39 MB
% 91.22/13.19 % (2972792)Instructions burned: 1181 (million)
% 91.22/13.19 % (2972804)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1075174966:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 91.22/13.19 % (2972798)Instruction limit reached!
% 91.22/13.19 % (2972798)------------------------------
% 91.22/13.19 % (2972798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.22/13.19 % (2972798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972798)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972798)Termination reason: Instruction limit
% 91.22/13.19 % (2972798)Termination phase: Saturation
% 91.22/13.19 % (2972798)Time elapsed: 0.417 s
% 91.22/13.19 % (2972798)Peak memory usage: 38 MB
% 91.22/13.19 % (2972798)Instructions burned: 880 (million)
% 91.22/13.19 % (2972806)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=796723917:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 91.22/13.19 % TRYING [1]
% 91.22/13.19 % (2972802)Cannot represent all propositional literals internally
% 91.22/13.19 % (2972802)Refutation not found, incomplete strategy
% 91.22/13.19 % (2972802)------------------------------
% 91.22/13.19 % (2972802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.22/13.19 % (2972802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972802)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972802)Termination reason: Refutation not found, incomplete strategy
% 91.22/13.19 % (2972802)Time elapsed: 0.577 s
% 91.22/13.19 % (2972802)Peak memory usage: 44 MB
% 91.22/13.19 % (2972802)Instructions burned: 1176 (million)
% 91.22/13.19 % (2972802)------------------------------
% 91.22/13.19 % (2972802)------------------------------
% 91.22/13.19 % TRYING [2]
% 91.22/13.19 % (2972808)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=925865454:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 91.22/13.19 % (2972804)Instruction limit reached!
% 91.22/13.19 % (2972804)------------------------------
% 91.22/13.19 % (2972804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.22/13.19 % (2972804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.19 % (2972804)CaDiCaL version: 2.1.3
% 91.22/13.19 % (2972804)Termination reason: Instruction limit
% 91.22/13.19 % (2972804)Termination phase: Finite model building preprocessing
% 91.22/13.19 % (2972804)Time elapsed: 0.449 s
% 91.22/13.19 % (2972804)Peak memory usage: 39 MB
% 91.22/13.19 % (2972804)Instructions burned: 920 (million)
% 91.22/13.19 % (2972810)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1340226184:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 91.22/13.19 % TRYING [4]
% 91.22/13.19 % (2972810)Cannot represent all propositional literals internally
% 91.22/13.19 % (2972810)Refutation not found, incomplete strategy
% 144.59/40.13 % (2972810)------------------------------
% 144.59/40.13 % (2972810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.13 % (2972810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.13 % (2972810)CaDiCaL version: 2.1.3
% 144.59/40.13 % (2972810)Termination reason: Refutation not found, incomplete strategy
% 144.59/40.13 % (2972810)Time elapsed: 0.605 s
% 144.59/40.13 % (2972810)Peak memory usage: 44 MB
% 144.59/40.13 % (2972810)Instructions burned: 1231 (million)
% 144.59/40.13 % (2972810)------------------------------
% 144.59/40.13 % (2972810)------------------------------
% 144.59/40.13 % (2972812)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2651903057:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 144.59/40.13 % (2972808)Instruction limit reached!
% 144.59/40.13 % (2972808)------------------------------
% 144.59/40.13 % (2972808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.13 % (2972808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.13 % (2972808)CaDiCaL version: 2.1.3
% 144.59/40.13 % (2972808)Termination reason: Instruction limit
% 144.59/40.13 % (2972808)Termination phase: Saturation
% 144.59/40.13 % (2972808)Time elapsed: 0.763 s
% 144.59/40.13 % (2972808)Peak memory usage: 38 MB
% 144.59/40.13 % (2972808)Instructions burned: 1472 (million)
% 144.59/40.13 % (2972814)ott-2_1_sil=16000:newcnf=on:random_seed=1333633524:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 144.59/40.13 % TRYING [3]
% 144.59/40.13 % (2972814)Instruction limit reached!
% 144.59/40.13 % (2972814)------------------------------
% 144.59/40.13 % (2972814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.13 % (2972814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.13 % (2972814)CaDiCaL version: 2.1.3
% 144.59/40.13 % (2972814)Termination reason: Instruction limit
% 144.59/40.13 % (2972814)Termination phase: Saturation
% 144.59/40.13 % (2972814)Time elapsed: 0.452 s
% 144.59/40.13 % (2972814)Peak memory usage: 35 MB
% 144.59/40.13 % (2972814)Instructions burned: 869 (million)
% 144.59/40.13 % (2972816)ott+10_1_sil=32000:tgt=ground:random_seed=3023871401:i=5114:av=off_2971 on theBenchmark for (2971ds/5114Mi)
% 144.59/40.13 % (2972812)Instruction limit reached!
% 144.59/40.13 % (2972812)------------------------------
% 144.59/40.13 % (2972812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.13 % (2972812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.13 % (2972812)CaDiCaL version: 2.1.3
% 144.59/40.13 % (2972812)Termination reason: Instruction limit
% 144.59/40.13 % (2972812)Termination phase: Finite model building preprocessing
% 144.59/40.13 % (2972812)Time elapsed: 1.059 s
% 144.59/40.13 % (2972812)Peak memory usage: 66 MB
% 144.59/40.13 % (2972812)Instructions burned: 2175 (million)
% 144.59/40.13 % (2972818)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3373236556:i=54282_2966 on theBenchmark for (2966ds/54282Mi)
% 144.59/40.13 % (2972806)Instruction limit reached!
% 144.59/40.13 % (2972806)------------------------------
% 144.59/40.13 % (2972806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.13 % (2972806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.13 % (2972806)CaDiCaL version: 2.1.3
% 144.59/40.13 % (2972806)Termination reason: Instruction limit
% 144.59/40.14 % (2972806)Termination phase: Saturation
% 144.59/40.14 % (2972806)Time elapsed: 2.743 s
% 144.59/40.14 % (2972806)Peak memory usage: 76 MB
% 144.59/40.14 % (2972806)Instructions burned: 5131 (million)
% 144.59/40.14 % (2972820)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3295155776:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 144.59/40.14 % TRYING [1]
% 144.59/40.14 % TRYING [2]
% 144.59/40.14 % TRYING [3]
% 144.59/40.14 % TRYING [4]
% 144.59/40.14 % (2972816)Instruction limit reached!
% 144.59/40.14 % (2972816)------------------------------
% 144.59/40.14 % (2972816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972816)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972816)Termination reason: Instruction limit
% 144.59/40.14 % (2972816)Termination phase: Saturation
% 144.59/40.14 % (2972816)Time elapsed: 2.717 s
% 144.59/40.14 % (2972816)Peak memory usage: 101 MB
% 144.59/40.14 % (2972816)Instructions burned: 5114 (million)
% 144.59/40.14 % (2972822)dis+21_1_sil=32000:sas=cadical:random_seed=839987430:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi)
% 144.59/40.14 % (2972820)Instruction limit reached!
% 144.59/40.14 % (2972820)------------------------------
% 144.59/40.14 % (2972820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972820)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972820)Termination reason: Instruction limit
% 144.59/40.14 % (2972820)Termination phase: Saturation
% 144.59/40.14 % (2972820)Time elapsed: 1.785 s
% 144.59/40.14 % (2972820)Peak memory usage: 47 MB
% 144.59/40.14 % (2972820)Instructions burned: 3513 (million)
% 144.59/40.14 % (2972824)ott+11_1_sil=16000:gs=on:random_seed=2619283721:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 144.59/40.14 % TRYING [5]
% 144.59/40.14 % TRYING [4]
% 144.59/40.14 % (2972824)Instruction limit reached!
% 144.59/40.14 % (2972824)------------------------------
% 144.59/40.14 % (2972824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972824)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972824)Termination reason: Instruction limit
% 144.59/40.14 % (2972824)Termination phase: Saturation
% 144.59/40.14 % (2972824)Time elapsed: 1.286 s
% 144.59/40.14 % (2972824)Peak memory usage: 102 MB
% 144.59/40.14 % (2972824)Instructions burned: 2252 (million)
% 144.59/40.14 % (2972826)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=453549799:fmbsr=1.6:i=67534_2928 on theBenchmark for (2928ds/67534Mi)
% 144.59/40.14 % (2972822)Instruction limit reached!
% 144.59/40.14 % (2972822)------------------------------
% 144.59/40.14 % (2972822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972822)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972822)Termination reason: Instruction limit
% 144.59/40.14 % (2972822)Termination phase: Saturation
% 144.59/40.14 % (2972822)Time elapsed: 1.588 s
% 144.59/40.14 % (2972822)Peak memory usage: 58 MB
% 144.59/40.14 % (2972822)Instructions burned: 3774 (million)
% 144.59/40.14 % (2972828)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3858192769:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 144.59/40.14 % (2972828)Instruction limit reached!
% 144.59/40.14 % (2972828)------------------------------
% 144.59/40.14 % (2972828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972828)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972828)Termination reason: Instruction limit
% 144.59/40.14 % (2972828)Termination phase: Saturation
% 144.59/40.14 % (2972828)Time elapsed: 1.873 s
% 144.59/40.14 % (2972828)Peak memory usage: 49 MB
% 144.59/40.14 % (2972828)Instructions burned: 4593 (million)
% 144.59/40.14 % (2972830)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=198766906:i=29340_2908 on theBenchmark for (2908ds/29340Mi)
% 144.59/40.14 % TRYING [5]
% 144.59/40.14 % (2972800)Instruction limit reached!
% 144.59/40.14 % (2972800)------------------------------
% 144.59/40.14 % (2972800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972800)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972800)Termination reason: Instruction limit
% 144.59/40.14 % (2972800)Termination phase: Finite model building SAT solving
% 144.59/40.14 % (2972800)Time elapsed: 9.654 s
% 144.59/40.14 % (2972800)Peak memory usage: 369 MB
% 144.59/40.14 % (2972800)Instructions burned: 22061 (million)
% 144.59/40.14 % (2972832)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1045338957:i=5211_2893 on theBenchmark for (2893ds/5211Mi)
% 144.59/40.14 % (2972832)Instruction limit reached!
% 144.59/40.14 % (2972832)------------------------------
% 144.59/40.14 % (2972832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972832)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972832)Termination reason: Instruction limit
% 144.59/40.14 % (2972832)Termination phase: Saturation
% 144.59/40.14 % (2972832)Time elapsed: 1.699 s
% 144.59/40.14 % (2972832)Peak memory usage: 45 MB
% 144.59/40.14 % (2972832)Instructions burned: 5213 (million)
% 144.59/40.14 % (2972834)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1444025493:i=5497:nm=2_2875 on theBenchmark for (2875ds/5497Mi)
% 144.59/40.14 % TRYING [7]
% 144.59/40.14 % (2972834)Cannot represent all propositional literals internally
% 144.59/40.14 % (2972834)Refutation not found, incomplete strategy
% 144.59/40.14 % (2972834)------------------------------
% 144.59/40.14 % (2972834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972834)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972834)Termination reason: Refutation not found, incomplete strategy
% 144.59/40.14 % (2972834)Time elapsed: 0.545 s
% 144.59/40.14 % (2972834)Peak memory usage: 43 MB
% 144.59/40.14 % (2972834)Instructions burned: 1066 (million)
% 144.59/40.14 % (2972834)------------------------------
% 144.59/40.14 % (2972834)------------------------------
% 144.59/40.14 % (2972836)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3079331153:fmbsr=2:i=46332_2870 on theBenchmark for (2870ds/46332Mi)
% 144.59/40.14 % (2972836)Cannot represent all propositional literals internally
% 144.59/40.14 % (2972836)Refutation not found, incomplete strategy
% 144.59/40.14 % (2972836)------------------------------
% 144.59/40.14 % (2972836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972836)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972836)Termination reason: Refutation not found, incomplete strategy
% 144.59/40.14 % (2972836)Time elapsed: 0.637 s
% 144.59/40.14 % (2972836)Peak memory usage: 44 MB
% 144.59/40.14 % (2972836)Instructions burned: 1365 (million)
% 144.59/40.14 % (2972836)------------------------------
% 144.59/40.14 % (2972836)------------------------------
% 144.59/40.14 % (2972907)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4116457857:i=14071_2863 on theBenchmark for (2863ds/14071Mi)
% 144.59/40.14 % TRYING [12]
% 144.59/40.14 % (2972907)Instruction limit reached!
% 144.59/40.14 % (2972907)------------------------------
% 144.59/40.14 % (2972907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972907)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972907)Termination reason: Instruction limit
% 144.59/40.14 % (2972907)Termination phase: Finite model building constraint generation
% 144.59/40.14 % (2972907)Time elapsed: 8.585 s
% 144.59/40.14 % (2972907)Peak memory usage: 760 MB
% 144.59/40.14 % (2972907)Instructions burned: 14072 (million)
% 144.59/40.14 % (2973165)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1848532311:i=22565:add=on:rawr=on_2775 on theBenchmark for (2775ds/22565Mi)
% 144.59/40.14 % (2972830)Instruction limit reached!
% 144.59/40.14 % (2972830)------------------------------
% 144.59/40.14 % (2972830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2972830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2972830)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2972830)Termination reason: Instruction limit
% 144.59/40.14 % (2972830)Termination phase: Saturation
% 144.59/40.14 % (2972830)Time elapsed: 20.276 s
% 144.59/40.14 % (2972830)Peak memory usage: 361 MB
% 144.59/40.14 % (2972830)Instructions burned: 29340 (million)
% 144.59/40.14 % (2973175)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=916229928:i=8173:av=off_2704 on theBenchmark for (2704ds/8173Mi)
% 144.59/40.14 % (2973175)Instruction limit reached!
% 144.59/40.14 % (2973175)------------------------------
% 144.59/40.14 % (2973175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.14 % (2973175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.14 % (2973175)CaDiCaL version: 2.1.3
% 144.59/40.14 % (2973175)Termination reason: Instruction limit
% 144.59/40.14 % (2973175)Termination phase: Saturation
% 144.59/40.14 % (2973175)Time elapsed: 7.851 s
% 144.59/40.14 % (2973175)Peak memory usage: 172 MB
% 144.59/40.14 % (2973175)Instructions burned: 8174 (million)
% 144.59/40.14 % (2973183)dis+10_16:1_sil=16000:random_seed=283789701:i=9155:fsr=off_2625 on theBenchmark for (2625ds/9155Mi)
% 144.59/40.14 % (2972767) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2972761-2972767"...
% 144.59/40.14 % (2972767)...printing done.
% 144.59/40.14 % (2972767)Refutation found. Thanks to Tanya!
% 144.59/40.14 % SZS status Theorem for theBenchmark
% 144.59/40.14 % SZS output start Proof for theBenchmark
% See solution above
% 144.59/40.15 % (2972767)------------------------------
% 144.59/40.15 % (2972767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.59/40.15 % (2972767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.59/40.15 % (2972767)CaDiCaL version: 2.1.3
% 144.59/40.15 % (2972767)Termination reason: Refutation
% 144.59/40.15 % (2972767)Time elapsed: 38.984 s
% 144.59/40.15 % (2972767)Peak memory usage: 227 MB
% 144.59/40.15 % (2972767)Instructions burned: 54901 (million)
% 144.59/40.15 % (2972761)Success in time 39.914 s
% 144.59/40.15 % Vampire exiting
%------------------------------------------------------------------------------