%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR115+33 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:13:58 PM UTC 2026
% Result : Theorem 205.23s 26.59s
% Output : CNFRefutation 206.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 31
% Syntax : Number of formulae : 117 ( 40 unt; 18 def)
% Number of atoms : 457 ( 0 equ)
% Maximal formula atoms : 199 ( 3 avg)
% Number of connectives : 474 ( 134 ~; 96 |; 224 &)
% ( 18 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 199 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 39 ( 38 usr; 19 prp; 0-6 aty)
% Number of functors : 72 ( 72 usr; 70 con; 0-2 aty)
% Number of variables : 112 ( 95 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X0,X1,X2] :
( member(X0,X2)
=> member(X0,cons(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,axiom,
! [X0,X1,X2] :
( ( sub(X0,X1)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& attr(X2,X0) )
=> ? [X3] :
( subs(X3,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9227,axiom,
sub(anf__374hrerin_1_1,an_f__374hrer_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9231,axiom,
sub(angreiferin_1_1,aggressor_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9312,axiom,
sub(begr__374nderin_1_1,be_gr__374nder_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9435,axiom,
sub(erfinderin_1_1,erfinder_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9586,axiom,
sub(herrscher__1_1,an_f__374hrer_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9658,axiom,
sub(killerin_1_1,killer_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9741,axiom,
sub(l__374gnerin_1_1,l__374gner_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10000,axiom,
sub(spielleiterin_1_1,regisseur_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( sub(X2,name_1_1)
& sub(X1,name_1_1)
& prop(X0,britisch__1_1)
& obj(X4,X0)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( sub(X2,name_1_1)
& sub(X1,name_1_1)
& prop(X0,britisch__1_1)
& obj(X4,X0)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(ordnung_1_1,varia_c)
& refer(ordnung_1_1,refer_c)
& quant(ordnung_1_1,one)
& gener(ordnung_1_1,ge)
& fact(ordnung_1_1,real)
& etype(ordnung_1_1,int0)
& card(ordnung_1_1,int1)
& sort(ordnung_1_1,io)
& sort(ordnung_1_1,as)
& varia(gr__366__337e_1_1,varia_c)
& refer(gr__366__337e_1_1,refer_c)
& quant(gr__366__337e_1_1,one)
& gener(gr__366__337e_1_1,ge)
& fact(gr__366__337e_1_1,real)
& etype(gr__366__337e_1_1,int0)
& card(gr__366__337e_1_1,int1)
& sort(gr__366__337e_1_1,oa)
& varia(c8677,varia_c)
& refer(c8677,refer_c)
& quant(c8677,quant_c)
& gener(c8677,gener_c)
& fact(c8677,real)
& etype(c8677,etype_c)
& card(c8677,card_c)
& sort(c8677,ent)
& varia(gr__366ssenordnung_1_1,varia_c)
& refer(gr__366ssenordnung_1_1,refer_c)
& quant(gr__366ssenordnung_1_1,one)
& gener(gr__366ssenordnung_1_1,ge)
& fact(gr__366ssenordnung_1_1,real)
& etype(gr__366ssenordnung_1_1,int0)
& card(gr__366ssenordnung_1_1,int1)
& sort(gr__366ssenordnung_1_1,oa)
& sort(gr__366ssenordnung_1_1,io)
& sort(neo_1_1,nq)
& varia(c7518,varia_c)
& refer(c7518,indet)
& quant(c7518,one)
& gener(c7518,sp)
& fact(c7518,real)
& etype(c7518,int0)
& card(c7518,int1)
& sort(c7518,oa)
& sort(c7518,io)
& sort(rover_0,fe)
& sort(britisch__1_1,nq)
& varia(c7514,varia_c)
& refer(c7514,indet)
& quant(c7514,one)
& gener(c7514,sp)
& fact(c7514,real)
& etype(c7514,int0)
& card(c7514,int1)
& sort(c7514,na)
& varia(c7513,con)
& refer(c7513,det)
& quant(c7513,one)
& gener(c7513,sp)
& fact(c7513,real)
& etype(c7513,int0)
& card(c7513,int1)
& sort(c7513,io)
& sort(c7513,d)
& varia(ankauf__1_1,varia_c)
& refer(ankauf__1_1,refer_c)
& quant(ankauf__1_1,one)
& gener(ankauf__1_1,ge)
& fact(ankauf__1_1,real)
& etype(ankauf__1_1,int0)
& card(ankauf__1_1,int1)
& sort(ankauf__1_1,ad)
& varia(c7474,con)
& refer(c7474,det)
& quant(c7474,one)
& gener(c7474,sp)
& fact(c7474,real)
& etype(c7474,int0)
& card(c7474,int1)
& sort(c7474,ad)
& varia(bmw_1_1,varia_c)
& refer(bmw_1_1,refer_c)
& quant(bmw_1_1,one)
& gener(bmw_1_1,ge)
& fact(bmw_1_1,real)
& etype(bmw_1_1,int0)
& card(bmw_1_1,int1)
& sort(bmw_1_1,d)
& varia(c7464,varia_c)
& refer(c7464,refer_c)
& quant(c7464,one)
& gener(c7464,gener_c)
& fact(c7464,real)
& etype(c7464,int0)
& card(c7464,int1)
& sort(c7464,d)
& sort(dpa_0,fe)
& varia(einrichtung_1_2,varia_c)
& refer(einrichtung_1_2,refer_c)
& quant(einrichtung_1_2,quant_c)
& gener(einrichtung_1_2,ge)
& fact(einrichtung_1_2,real)
& etype(einrichtung_1_2,int1)
& card(einrichtung_1_2,card_c)
& sort(einrichtung_1_2,io)
& sort(einrichtung_1_2,d)
& varia(c7462,varia_c)
& refer(c7462,indet)
& quant(c7462,one)
& gener(c7462,sp)
& fact(c7462,real)
& etype(c7462,int0)
& card(c7462,int1)
& sort(c7462,na)
& varia(c7461,con)
& refer(c7461,det)
& quant(c7461,one)
& gener(c7461,sp)
& fact(c7461,real)
& etype(c7461,int1)
& card(c7461,int1)
& sort(c7461,io)
& sort(c7461,d)
& sort(m__374nchen_0,fe)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& quant(name_1_1,one)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& etype(name_1_1,int0)
& card(name_1_1,int1)
& sort(name_1_1,na)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& quant(stadt__1_1,one)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& etype(stadt__1_1,int0)
& card(stadt__1_1,int1)
& sort(stadt__1_1,io)
& sort(stadt__1_1,d)
& varia(c7457,varia_c)
& refer(c7457,indet)
& quant(c7457,one)
& gener(c7457,sp)
& fact(c7457,real)
& etype(c7457,int0)
& card(c7457,int1)
& sort(c7457,na)
& varia(c7456,con)
& refer(c7456,det)
& quant(c7456,one)
& gener(c7456,sp)
& fact(c7456,real)
& etype(c7456,int0)
& card(c7456,int1)
& sort(c7456,io)
& sort(c7456,d)
& varia(fabrikant_1_1,varia_c)
& refer(fabrikant_1_1,refer_c)
& quant(fabrikant_1_1,one)
& gener(fabrikant_1_1,ge)
& fact(fabrikant_1_1,real)
& etype(fabrikant_1_1,int0)
& card(fabrikant_1_1,int1)
& sort(fabrikant_1_1,io)
& sort(fabrikant_1_1,d)
& sort(automobil_1_1,tq)
& varia(autobauer_1_1,varia_c)
& refer(autobauer_1_1,refer_c)
& quant(autobauer_1_1,one)
& gener(autobauer_1_1,ge)
& fact(autobauer_1_1,real)
& etype(autobauer_1_1,int0)
& card(autobauer_1_1,int1)
& sort(autobauer_1_1,io)
& sort(autobauer_1_1,d)
& sub(gr__366ssenordnung_1_1,ordnung_1_1)
& assoc(gr__366ssenordnung_1_1,gr__366__337e_1_1)
& tupl_p6(c8677,c7456,c7461,c7464,c7474,c7518)
& sub(c7518,gr__366ssenordnung_1_1)
& prop(c7518,neo_1_1)
& val(c7514,rover_0)
& sub(c7514,name_1_1)
& sub(c7513,autobauer_1_1)
& prop(c7513,britisch__1_1)
& attr(c7513,c7514)
& attch(c7513,c7474)
& subs(c7474,ankauf__1_1)
& sub(c7464,bmw_1_1)
& val(c7462,dpa_0)
& sub(c7462,name_1_1)
& sub(c7461,einrichtung_1_2)
& attr(c7461,c7462)
& val(c7457,m__374nchen_0)
& sub(c7457,name_1_1)
& sub(c7456,stadt__1_1)
& attr(c7456,c7457)
& sub(autobauer_1_1,fabrikant_1_1)
& assoc(autobauer_1_1,automobil_1_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10191,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f10192,plain,
! [X0,X1,X2] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f10193,plain,
! [X0,X2] :
( ! [X1] : member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(miniscoping,[status(thm)],[f10192]) ).
fof(f10194,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,cons(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f10193]) ).
fof(f10698,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(X3,X2) )
| ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f160]) ).
fof(f10699,plain,
! [X2] :
( ? [X3] :
( subs(X3,stehen_1_b)
& scar(X3,X2)
& obj(X3,X2)
& mcont(X3,X2) )
| ! [X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ) ),
inference(miniscoping,[status(thm)],[f10698]) ).
fof(f10700,plain,
! [X2] :
( ( subs(sK51_skl(X2),stehen_1_b)
& scar(sK51_skl(X2),X2)
& obj(sK51_skl(X2),X2)
& mcont(sK51_skl(X2),X2) )
| ! [X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl]),skolemize(X3,sK51_skl(X2))],[f10699]) ).
fof(f10702,plain,
! [X0,X1,X2] :
( ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| obj(sK51_skl(X0),X0)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10700]) ).
fof(f19854,plain,
sub(anf__374hrerin_1_1,an_f__374hrer_1_1),
inference(cnf_transformation,[status(thm)],[f9227]) ).
fof(f19858,plain,
sub(angreiferin_1_1,aggressor_1_1),
inference(cnf_transformation,[status(thm)],[f9231]) ).
fof(f19939,plain,
sub(begr__374nderin_1_1,be_gr__374nder_1_1),
inference(cnf_transformation,[status(thm)],[f9312]) ).
fof(f20062,plain,
sub(erfinderin_1_1,erfinder_1_1),
inference(cnf_transformation,[status(thm)],[f9435]) ).
fof(f20213,plain,
sub(herrscher__1_1,an_f__374hrer_1_1),
inference(cnf_transformation,[status(thm)],[f9586]) ).
fof(f20285,plain,
sub(killerin_1_1,killer_1_1),
inference(cnf_transformation,[status(thm)],[f9658]) ).
fof(f20368,plain,
sub(l__374gnerin_1_1,l__374gner_1_1),
inference(cnf_transformation,[status(thm)],[f9741]) ).
fof(f20627,plain,
sub(spielleiterin_1_1,regisseur_1_1),
inference(cnf_transformation,[status(thm)],[f10000]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sub(X2,name_1_1)
| ~ sub(X1,name_1_1)
| ~ prop(X0,britisch__1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X2] :
( ~ sub(X2,name_1_1)
| ! [X1] :
( ~ sub(X1,name_1_1)
| ! [X0] :
( ~ prop(X0,britisch__1_1)
| ! [X4] : ~ obj(X4,X0)
| ! [X5,X6] : ~ attr(X5,X6)
| ! [X3] : ~ attr(X3,X2)
| ~ attr(X0,X1) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sub(X3,name_1_1)
| ~ sub(X1,name_1_1)
| ~ prop(X0,britisch__1_1)
| ~ obj(X6,X0)
| ~ attr(X4,X5)
| ~ attr(X2,X3)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20820,plain,
attr(c7456,c7457),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20822,plain,
sub(c7457,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
sub(c7462,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20831,plain,
attr(c7513,c7514),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20832,plain,
prop(c7513,britisch__1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
sub(c7513,autobauer_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20834,plain,
sub(c7514,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21052,definition,
! [X0,X1,X6] :
( sQ0_spl
<=> ( ~ sub(X1,name_1_1)
| ~ prop(X0,britisch__1_1)
| ~ obj(X6,X0)
| ~ attr(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21053,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ sub(X2,name_1_1)
| ~ attr(X0,X2)
| ~ obj(X1,X0)
| ~ prop(X0,britisch__1_1) ),
inference(component_clause,[status(thm)],[f21052]) ).
fof(f21055,definition,
! [X2,X3] :
( sQ1_spl
<=> ( ~ sub(X3,name_1_1)
| ~ attr(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21056,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ attr(X1,X0)
| ~ sub(X0,name_1_1) ),
inference(component_clause,[status(thm)],[f21055]) ).
fof(f21058,definition,
! [X4,X5] :
( sQ2_spl
<=> ~ attr(X4,X5) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21059,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21058]) ).
fof(f21061,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21052,f21055,f21058]) ).
fof(f21075,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20820,f21059]) ).
fof(f21076,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f21075]) ).
fof(f21092,plain,
! [X0] :
( ~ sQ0_spl
| ~ prop(c7513,britisch__1_1)
| ~ sub(c7514,name_1_1)
| ~ obj(X0,c7513) ),
inference(resolution,[status(thm)],[f20831,f21053]) ).
fof(f21093,definition,
! [X0] :
( sQ5_spl
<=> ~ obj(X0,c7513) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f21094,plain,
! [X0] :
( ~ sQ5_spl
| ~ obj(X0,c7513) ),
inference(component_clause,[status(thm)],[f21093]) ).
fof(f21096,definition,
( sQ6_spl
<=> sub(c7514,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f21098,plain,
( sQ6_spl
| ~ sub(c7514,name_1_1) ),
inference(component_clause,[status(thm)],[f21096]) ).
fof(f21099,definition,
( sQ7_spl
<=> prop(c7513,britisch__1_1) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21101,plain,
( sQ7_spl
| ~ prop(c7513,britisch__1_1) ),
inference(component_clause,[status(thm)],[f21099]) ).
fof(f21102,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f21092,f21093,f21096,f21099,f21052]) ).
fof(f21103,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21101,f20832]) ).
fof(f21104,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21103]) ).
fof(f21105,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21098,f20834]) ).
fof(f21106,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f21105]) ).
fof(f21107,plain,
( ~ sQ1_spl
| ~ sub(c7514,name_1_1) ),
inference(resolution,[status(thm)],[f21056,f20831]) ).
fof(f21108,plain,
( ~ sQ1_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f21107,f21096,f21055]) ).
fof(f21156,plain,
! [X0,X1,X2] :
( obj(sK51_skl(X0),X0)
| ~ member(X2,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[f10702,f10194]) ).
fof(f22692,definition,
! [X1] :
( sQ25_spl
<=> ~ sub(c7513,X1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f22693,plain,
! [X0] :
( ~ sQ25_spl
| ~ sub(c7513,X0) ),
inference(component_clause,[status(thm)],[f22692]) ).
fof(f22703,plain,
( ~ sQ25_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20833,f22693]) ).
fof(f22714,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f22703]) ).
fof(f22931,definition,
! [X0] :
( sQ69_spl
<=> ~ sub(spielleiterin_1_1,X0) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f22932,plain,
! [X0] :
( ~ sQ69_spl
| ~ sub(spielleiterin_1_1,X0) ),
inference(component_clause,[status(thm)],[f22931]) ).
fof(f22946,plain,
( ~ sQ69_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20627,f22932]) ).
fof(f22960,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f22946]) ).
fof(f23263,definition,
! [X0] :
( sQ128_spl
<=> ~ sub(herrscher__1_1,X0) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f23264,plain,
! [X0] :
( ~ sQ128_spl
| ~ sub(herrscher__1_1,X0) ),
inference(component_clause,[status(thm)],[f23263]) ).
fof(f23327,plain,
( ~ sQ128_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20213,f23264]) ).
fof(f23345,plain,
~ sQ128_spl,
inference(contradiction_clause,[status(thm)],[f23327]) ).
fof(f23609,definition,
! [X0] :
( sQ181_spl
<=> ~ sub(anf__374hrerin_1_1,X0) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f23610,plain,
! [X0] :
( ~ sQ181_spl
| ~ sub(anf__374hrerin_1_1,X0) ),
inference(component_clause,[status(thm)],[f23609]) ).
fof(f23613,plain,
( ~ sQ181_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19854,f23610]) ).
fof(f23624,plain,
~ sQ181_spl,
inference(contradiction_clause,[status(thm)],[f23613]) ).
fof(f23636,definition,
! [X0] :
( sQ184_spl
<=> ~ sub(begr__374nderin_1_1,X0) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f23637,plain,
! [X0] :
( ~ sQ184_spl
| ~ sub(begr__374nderin_1_1,X0) ),
inference(component_clause,[status(thm)],[f23636]) ).
fof(f23640,plain,
( ~ sQ184_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19939,f23637]) ).
fof(f23651,plain,
~ sQ184_spl,
inference(contradiction_clause,[status(thm)],[f23640]) ).
fof(f23693,definition,
! [X0] :
( sQ191_spl
<=> ~ sub(angreiferin_1_1,X0) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f23694,plain,
! [X0] :
( ~ sQ191_spl
| ~ sub(angreiferin_1_1,X0) ),
inference(component_clause,[status(thm)],[f23693]) ).
fof(f23697,plain,
( ~ sQ191_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19858,f23694]) ).
fof(f23704,plain,
~ sQ191_spl,
inference(contradiction_clause,[status(thm)],[f23697]) ).
fof(f23879,definition,
! [X2] :
( sQ223_spl
<=> ~ sub(l__374gnerin_1_1,X2) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f23880,plain,
! [X0] :
( ~ sQ223_spl
| ~ sub(l__374gnerin_1_1,X0) ),
inference(component_clause,[status(thm)],[f23879]) ).
fof(f23894,plain,
( ~ sQ223_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20368,f23880]) ).
fof(f23901,plain,
~ sQ223_spl,
inference(contradiction_clause,[status(thm)],[f23894]) ).
fof(f23991,definition,
! [X2] :
( sQ244_spl
<=> ~ sub(erfinderin_1_1,X2) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f23992,plain,
! [X0] :
( ~ sQ244_spl
| ~ sub(erfinderin_1_1,X0) ),
inference(component_clause,[status(thm)],[f23991]) ).
fof(f24002,plain,
( ~ sQ244_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20062,f23992]) ).
fof(f24013,plain,
~ sQ244_spl,
inference(contradiction_clause,[status(thm)],[f24002]) ).
fof(f24174,definition,
! [X2] :
( sQ271_spl
<=> ~ sub(killerin_1_1,X2) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f24175,plain,
! [X0] :
( ~ sQ271_spl
| ~ sub(killerin_1_1,X0) ),
inference(component_clause,[status(thm)],[f24174]) ).
fof(f24193,plain,
( ~ sQ271_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20285,f24175]) ).
fof(f24205,plain,
~ sQ271_spl,
inference(contradiction_clause,[status(thm)],[f24193]) ).
fof(f24613,plain,
! [X0,X1,X2] :
( ~ attr(X0,X2)
| ~ sub(X2,X1)
| ~ member(X1,cons(name_1_1,nil))
| obj(sK51_skl(X0),X0) ),
inference(resolution,[status(thm)],[f21156,f10194]) ).
fof(f24743,plain,
! [X0,X1] :
( ~ attr(X1,X0)
| obj(sK51_skl(X1),X1)
| ~ sub(X0,name_1_1) ),
inference(resolution,[status(thm)],[f24613,f10191]) ).
fof(f24750,plain,
( obj(sK51_skl(c7513),c7513)
| ~ sub(c7514,name_1_1) ),
inference(resolution,[status(thm)],[f24743,f20831]) ).
fof(f24752,definition,
( sQ343_spl
<=> sub(c7457,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition]) ).
fof(f24754,plain,
( sQ343_spl
| ~ sub(c7457,name_1_1) ),
inference(component_clause,[status(thm)],[f24752]) ).
fof(f24761,definition,
( sQ345_spl
<=> obj(sK51_skl(c7513),c7513) ),
introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition]) ).
fof(f24762,plain,
( ~ sQ345_spl
| obj(sK51_skl(c7513),c7513) ),
inference(component_clause,[status(thm)],[f24761]) ).
fof(f24764,plain,
( sQ345_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f24750,f21096,f24761]) ).
fof(f24767,definition,
( sQ346_spl
<=> sub(c7462,name_1_1) ),
introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition]) ).
fof(f24769,plain,
( sQ346_spl
| ~ sub(c7462,name_1_1) ),
inference(component_clause,[status(thm)],[f24767]) ).
fof(f24775,plain,
( sQ343_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24754,f20822]) ).
fof(f24776,plain,
sQ343_spl,
inference(contradiction_clause,[status(thm)],[f24775]) ).
fof(f24777,plain,
( sQ346_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24769,f20826]) ).
fof(f24778,plain,
sQ346_spl,
inference(contradiction_clause,[status(thm)],[f24777]) ).
fof(f24779,plain,
( ~ sQ345_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24762,f21094]) ).
fof(f24780,plain,
( ~ sQ345_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f24779]) ).
fof(f24781,plain,
$false,
inference(sat_refutation,[status(thm)],[f21061,f21076,f21102,f21104,f21106,f21108,f22714,f22960,f23345,f23624,f23651,f23704,f23901,f24013,f24205,f24764,f24776,f24778,f24780]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR115+33 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n002.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 15:09:03 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.22/0.61 % Drodi V4.1.1
% 205.23/26.59 % Refutation found
% 205.23/26.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 205.23/26.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.40/27.11 % Elapsed time: 26.610014 seconds
% 21.40/27.11 % CPU time: 206.736909 seconds
% 21.40/27.11 % Total memory used: 717.077 MB
% 21.40/27.11 % Net memory used: 663.217 MB
%------------------------------------------------------------------------------