%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR115+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:56 PM UTC 2026
% Result : Theorem 27.25s 3.98s
% Output : CNFRefutation 27.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 14
% Syntax : Number of formulae : 73 ( 18 unt; 8 def)
% Number of atoms : 428 ( 0 equ)
% Maximal formula atoms : 202 ( 5 avg)
% Number of connectives : 492 ( 137 ~; 120 |; 224 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 202 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 9 prp; 0-3 aty)
% Number of functors : 59 ( 59 usr; 58 con; 0-2 aty)
% Number of variables : 109 ( 94 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,axiom,
! [X0,X1,X2] :
( ( subs(X0,X1)
& chea(X2,X1) )
=> ? [X3] :
( subs(X3,X2)
& chea(X3,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [X0,X1,X2] :
( ( chea(X1,X0)
& agt(X0,X2) )
=> agt(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [X0,X1,X2] :
( ( obj(X0,X2)
& chea(X1,X0) )
=> obj(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8535,axiom,
chea(n374bernehmen_1_1,annahme_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( val(X1,bmw_0)
& subs(X3,n374bernehmen_1_1)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& prop(X0,britisch__1_1)
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1)
& agt(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( val(X1,bmw_0)
& subs(X3,n374bernehmen_1_1)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& prop(X0,britisch__1_1)
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1)
& agt(X3,X2) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( gener(hundertstel__1_1,ge)
& sort(hundertstel__1_1,me)
& card(c1954,int20)
& sort(c1954,nu)
& gener(abziehen_1_2,ge)
& fact(abziehen_1_2,real)
& sort(abziehen_1_2,da)
& gener(wollen_0,gener_c)
& fact(wollen_0,real)
& sort(wollen_0,md)
& varia(anteil_1_1,varia_c)
& refer(anteil_1_1,refer_c)
& quant(anteil_1_1,quant_c)
& gener(anteil_1_1,ge)
& fact(anteil_1_1,real)
& etype(anteil_1_1,etype_c)
& card(anteil_1_1,card_c)
& sort(anteil_1_1,co)
& varia(c1977,con)
& refer(c1977,refer_c)
& quant(c1977,quant_c)
& gener(c1977,gener_c)
& fact(c1977,real)
& etype(c1977,etype_c)
& card(c1977,card_c)
& sort(c1977,co)
& sort(bmw_0,fe)
& sort(bundesdeutsch_1_1,tq)
& varia(c1948,varia_c)
& refer(c1948,indet)
& quant(c1948,one)
& gener(c1948,sp)
& fact(c1948,real)
& etype(c1948,int0)
& card(c1948,int1)
& sort(c1948,na)
& sort(rover_0,fe)
& varia(firma_1_1,varia_c)
& refer(firma_1_1,refer_c)
& quant(firma_1_1,one)
& gener(firma_1_1,ge)
& fact(firma_1_1,real)
& etype(firma_1_1,int0)
& card(firma_1_1,int1)
& sort(firma_1_1,io)
& sort(firma_1_1,d)
& sort(britisch__1_1,nq)
& varia(c1854,varia_c)
& refer(c1854,indet)
& quant(c1854,one)
& gener(c1854,sp)
& fact(c1854,real)
& etype(c1854,int0)
& card(c1854,int1)
& sort(c1854,na)
& varia(annahme_1_1,varia_c)
& refer(annahme_1_1,refer_c)
& quant(annahme_1_1,one)
& gener(annahme_1_1,ge)
& fact(annahme_1_1,real)
& etype(annahme_1_1,int0)
& card(annahme_1_1,int1)
& sort(annahme_1_1,ad)
& varia(c1853,con)
& refer(c1853,det)
& quant(c1853,one)
& gener(c1853,sp)
& fact(c1853,real)
& etype(c1853,int0)
& card(c1853,int1)
& sort(c1853,io)
& sort(c1853,d)
& gener(c1957,sp)
& fact(c1957,real)
& sort(c1957,da)
& varia(c1947,con)
& refer(c1947,det)
& quant(c1947,one)
& gener(c1947,sp)
& fact(c1947,real)
& etype(c1947,int0)
& card(c1947,int1)
& sort(c1947,io)
& sort(c1947,d)
& varia(c1671,con)
& refer(c1671,det)
& quant(c1671,one)
& gener(c1671,sp)
& fact(c1671,real)
& etype(c1671,int0)
& card(c1671,int1)
& sort(c1671,ad)
& sort(honda_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)
& sort(japanisch__1_1,nq)
& varia(c1949,varia_c)
& refer(c1949,det)
& quant(c1949,quant_c)
& gener(c1949,sp)
& fact(c1949,real)
& etype(c1949,etype_c)
& card(c1949,card_c)
& sort(c1949,co)
& varia(c1666,varia_c)
& refer(c1666,indet)
& quant(c1666,one)
& gener(c1666,sp)
& fact(c1666,real)
& etype(c1666,int0)
& card(c1666,int1)
& sort(c1666,na)
& varia(c1665,con)
& refer(c1665,det)
& quant(c1665,one)
& gener(c1665,sp)
& fact(c1665,real)
& etype(c1665,int0)
& card(c1665,int1)
& sort(c1665,io)
& sort(c1665,d)
& varia(firmengruppe_1_1,varia_c)
& refer(firmengruppe_1_1,refer_c)
& quant(firmengruppe_1_1,one)
& gener(firmengruppe_1_1,ge)
& fact(firmengruppe_1_1,real)
& etype(firmengruppe_1_1,int0)
& card(firmengruppe_1_1,int1)
& sort(firmengruppe_1_1,io)
& sort(firmengruppe_1_1,d)
& varia(autokonzern_1_1,varia_c)
& refer(autokonzern_1_1,refer_c)
& quant(autokonzern_1_1,one)
& gener(autokonzern_1_1,ge)
& fact(autokonzern_1_1,real)
& etype(autokonzern_1_1,int0)
& card(autokonzern_1_1,int1)
& sort(autokonzern_1_1,io)
& sort(autokonzern_1_1,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)
& varia(auto__1_1,varia_c)
& refer(auto__1_1,refer_c)
& quant(auto__1_1,one)
& gener(auto__1_1,ge)
& fact(auto__1_1,real)
& etype(auto__1_1,int0)
& card(auto__1_1,int1)
& sort(auto__1_1,d)
& 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)
& quant_p3(c1977,c1954,hundertstel__1_1)
& subs(c1957,abziehen_1_2)
& obj(c1957,c1949)
& modl(c1957,wollen_0)
& agt(c1957,c1665)
& sub(c1949,anteil_1_1)
& attch(c1949,c1977)
& val(c1948,bmw_0)
& sub(c1948,name_1_1)
& sub(c1947,autobauer_1_1)
& prop(c1947,bundesdeutsch_1_1)
& attr(c1947,c1948)
& val(c1854,rover_0)
& sub(c1854,name_1_1)
& sub(c1853,firma_1_1)
& prop(c1853,britisch__1_1)
& attr(c1853,c1854)
& subs(c1671,annahme_1_1)
& obj(c1671,c1853)
& ante(c1671,c1957)
& agt(c1671,c1947)
& val(c1666,honda_0)
& sub(c1666,name_1_1)
& sub(c1665,autokonzern_1_1)
& prop(c1665,japanisch__1_1)
& poss(c1665,c1949)
& attr(c1665,c1666)
& sub(autokonzern_1_1,firmengruppe_1_1)
& assoc(autokonzern_1_1,auto__1_1)
& sub(autobauer_1_1,fabrikant_1_1)
& assoc(autobauer_1_1,auto__1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10373,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,X2)
& chea(X3,X0) )
| ~ subs(X0,X1)
| ~ chea(X2,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f10374,plain,
! [X0,X2] :
( ? [X3] :
( subs(X3,X2)
& chea(X3,X0) )
| ! [X1] :
( ~ subs(X0,X1)
| ~ chea(X2,X1) ) ),
inference(miniscoping,[status(thm)],[f10373]) ).
fof(f10375,plain,
! [X0,X2] :
( ( subs(sK4_skl(X2,X0),X2)
& chea(sK4_skl(X2,X0),X0) )
| ! [X1] :
( ~ subs(X0,X1)
| ~ chea(X2,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X3,sK4_skl(X2,X0))],[f10374]) ).
fof(f10376,plain,
! [X0,X1,X2] :
( chea(sK4_skl(X0,X2),X2)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10375]) ).
fof(f10377,plain,
! [X0,X1,X2] :
( subs(sK4_skl(X0,X2),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10375]) ).
fof(f10381,plain,
! [X0,X1,X2] :
( agt(X1,X2)
| ~ chea(X1,X0)
| ~ agt(X0,X2) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f10382,plain,
! [X1,X2] :
( agt(X1,X2)
| ! [X0] :
( ~ chea(X1,X0)
| ~ agt(X0,X2) ) ),
inference(miniscoping,[status(thm)],[f10381]) ).
fof(f10383,plain,
! [X0,X1,X2] :
( agt(X2,X1)
| ~ chea(X2,X0)
| ~ agt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10382]) ).
fof(f10387,plain,
! [X0,X1,X2] :
( obj(X1,X2)
| ~ obj(X0,X2)
| ~ chea(X1,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f101]) ).
fof(f10388,plain,
! [X1,X2] :
( obj(X1,X2)
| ! [X0] :
( ~ obj(X0,X2)
| ~ chea(X1,X0) ) ),
inference(miniscoping,[status(thm)],[f10387]) ).
fof(f10389,plain,
! [X0,X1,X2] :
( obj(X0,X2)
| ~ obj(X1,X2)
| ~ chea(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10388]) ).
fof(f19162,plain,
chea(n374bernehmen_1_1,annahme_1_1),
inference(cnf_transformation,[status(thm)],[f8535]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ val(X1,bmw_0)
| ~ subs(X3,n374bernehmen_1_1)
| ~ sub(X1,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ prop(X0,britisch__1_1)
| ~ obj(X3,X0)
| ~ attr(X4,X5)
| ~ attr(X2,X1)
| ~ agt(X3,X2) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X1] :
( ~ val(X1,bmw_0)
| ! [X3] :
( ~ subs(X3,n374bernehmen_1_1)
| ~ sub(X1,name_1_1)
| ! [X0] :
( ~ sub(X0,firma_1_1)
| ~ prop(X0,britisch__1_1)
| ~ obj(X3,X0)
| ! [X4,X5] : ~ attr(X4,X5)
| ! [X2] :
( ~ attr(X2,X1)
| ~ agt(X3,X2) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ sub(X5,firma_1_1)
| ~ prop(X5,britisch__1_1)
| ~ obj(X0,X5)
| ~ attr(X3,X4)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20828,plain,
agt(c1671,c1947),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20830,plain,
obj(c1671,c1853),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20831,plain,
subs(c1671,annahme_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20833,plain,
prop(c1853,britisch__1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20834,plain,
sub(c1853,firma_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20837,plain,
attr(c1947,c1948),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20840,plain,
sub(c1948,name_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20841,plain,
val(c1948,bmw_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21055,definition,
! [X0,X1,X2,X5] :
( sQ0_spl
<=> ( ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ sub(X5,firma_1_1)
| ~ prop(X5,britisch__1_1)
| ~ obj(X0,X5)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21056,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ sub(X3,firma_1_1)
| ~ prop(X3,britisch__1_1)
| ~ obj(X0,X3)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ),
inference(component_clause,[status(thm)],[f21055]) ).
fof(f21058,definition,
! [X3,X4] :
( sQ1_spl
<=> ~ attr(X3,X4) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21059,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21058]) ).
fof(f21061,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21055,f21058]) ).
fof(f21062,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ prop(c1853,britisch__1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ),
inference(resolution,[status(thm)],[f20834,f21056]) ).
fof(f21064,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f21065,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ val(X2,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ sub(X2,name_1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,X2)
| ~ agt(X0,X1) ),
inference(component_clause,[status(thm)],[f21064]) ).
fof(f21067,definition,
( sQ3_spl
<=> prop(c1853,britisch__1_1) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f21069,plain,
( sQ3_spl
| ~ prop(c1853,britisch__1_1) ),
inference(component_clause,[status(thm)],[f21067]) ).
fof(f21070,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f21062,f21064,f21067,f21055]) ).
fof(f21071,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20837,f21059]) ).
fof(f21079,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21069,f20833]) ).
fof(f21080,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f21079]) ).
fof(f21081,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f21071]) ).
fof(f21092,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ val(c1948,bmw_0)
| ~ subs(X0,n374bernehmen_1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,c1948)
| ~ agt(X0,X1) ),
inference(resolution,[status(thm)],[f20840,f21065]) ).
fof(f21095,definition,
! [X0,X1] :
( sQ4_spl
<=> ( ~ subs(X0,n374bernehmen_1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,c1948)
| ~ agt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f21096,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ subs(X0,n374bernehmen_1_1)
| ~ obj(X0,c1853)
| ~ attr(X1,c1948)
| ~ agt(X0,X1) ),
inference(component_clause,[status(thm)],[f21095]) ).
fof(f21098,definition,
( sQ5_spl
<=> val(c1948,bmw_0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f21100,plain,
( sQ5_spl
| ~ val(c1948,bmw_0) ),
inference(component_clause,[status(thm)],[f21098]) ).
fof(f21101,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f21092,f21095,f21098,f21064]) ).
fof(f21106,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21100,f20841]) ).
fof(f21107,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f21106]) ).
fof(f21111,plain,
! [X0] :
( chea(sK4_skl(n374bernehmen_1_1,X0),X0)
| ~ subs(X0,annahme_1_1) ),
inference(resolution,[status(thm)],[f10376,f19162]) ).
fof(f21112,plain,
chea(sK4_skl(n374bernehmen_1_1,c1671),c1671),
inference(resolution,[status(thm)],[f21111,f20831]) ).
fof(f21115,plain,
! [X0] :
( obj(sK4_skl(n374bernehmen_1_1,c1671),X0)
| ~ obj(c1671,X0) ),
inference(resolution,[status(thm)],[f21112,f10389]) ).
fof(f21117,plain,
! [X0] :
( agt(sK4_skl(n374bernehmen_1_1,c1671),X0)
| ~ agt(c1671,X0) ),
inference(resolution,[status(thm)],[f21112,f10383]) ).
fof(f21126,plain,
! [X0] :
( subs(sK4_skl(n374bernehmen_1_1,X0),n374bernehmen_1_1)
| ~ subs(X0,annahme_1_1) ),
inference(resolution,[status(thm)],[f10377,f19162]) ).
fof(f21127,plain,
subs(sK4_skl(n374bernehmen_1_1,c1671),n374bernehmen_1_1),
inference(resolution,[status(thm)],[f21126,f20831]) ).
fof(f21131,plain,
! [X0] :
( ~ sQ4_spl
| ~ obj(sK4_skl(n374bernehmen_1_1,c1671),c1853)
| ~ attr(X0,c1948)
| ~ agt(sK4_skl(n374bernehmen_1_1,c1671),X0) ),
inference(resolution,[status(thm)],[f21127,f21096]) ).
fof(f21134,definition,
! [X0] :
( sQ7_spl
<=> ( ~ attr(X0,c1948)
| ~ agt(sK4_skl(n374bernehmen_1_1,c1671),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f21135,plain,
! [X0] :
( ~ sQ7_spl
| ~ attr(X0,c1948)
| ~ agt(sK4_skl(n374bernehmen_1_1,c1671),X0) ),
inference(component_clause,[status(thm)],[f21134]) ).
fof(f21141,definition,
( sQ9_spl
<=> obj(sK4_skl(n374bernehmen_1_1,c1671),c1853) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f21143,plain,
( sQ9_spl
| ~ obj(sK4_skl(n374bernehmen_1_1,c1671),c1853) ),
inference(component_clause,[status(thm)],[f21141]) ).
fof(f21144,plain,
( ~ sQ4_spl
| ~ sQ9_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f21131,f21134,f21141,f21095]) ).
fof(f21160,plain,
( ~ sQ7_spl
| ~ agt(sK4_skl(n374bernehmen_1_1,c1671),c1947) ),
inference(resolution,[status(thm)],[f21135,f20837]) ).
fof(f21161,plain,
( sQ9_spl
| ~ obj(c1671,c1853) ),
inference(resolution,[status(thm)],[f21143,f21115]) ).
fof(f21162,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21161,f20830]) ).
fof(f21163,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f21162]) ).
fof(f21187,plain,
( ~ sQ7_spl
| ~ agt(c1671,c1947) ),
inference(resolution,[status(thm)],[f21160,f21117]) ).
fof(f21189,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21187,f20828]) ).
fof(f21190,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f21189]) ).
fof(f21191,plain,
$false,
inference(sat_refutation,[status(thm)],[f21061,f21070,f21080,f21081,f21101,f21107,f21144,f21163,f21190]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR115+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/0.29 % Computer : n012.cluster.edu
% 0.05/0.29 % Model : x86_64 x86_64
% 0.05/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.29 % Memory : 8046.5625MB
% 0.05/0.29 % OS : Linux 6.8.0-71-generic
% 0.05/0.29 % CPULimit : 300
% 0.05/0.29 % WCLimit : 300
% 0.05/0.29 % DateTime : Mon Sep 21 15:05:51 UTC 2026
% 0.05/0.29 % CPUTime :
% 0.10/0.42 % Drodi V4.1.1
% 27.25/3.98 % Refutation found
% 27.25/3.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.25/3.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 27.18/4.05 % Elapsed time: 3.750462 seconds
% 27.18/4.05 % CPU time: 28.283835 seconds
% 27.18/4.05 % Total memory used: 523.179 MB
% 27.18/4.05 % Net memory used: 515.175 MB
%------------------------------------------------------------------------------