%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+18 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:14:09 PM UTC 2026
% Result : Theorem 22.14s 3.54s
% Output : CNFRefutation 22.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 24
% Syntax : Number of formulae : 134 ( 17 unt; 18 def)
% Number of atoms : 762 ( 0 equ)
% Maximal formula atoms : 217 ( 5 avg)
% Number of connectives : 978 ( 350 ~; 306 |; 301 &)
% ( 18 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 217 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 47 ( 46 usr; 19 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 54 con; 0-3 aty)
% Number of variables : 254 ( 214 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f155,axiom,
! [X0,X1,X2] :
( ( state_adjective_state_binding(X1,X2)
& prop(X0,X1) )
=> ? [X3,X4,X5] :
( val(X4,X2)
& sub(X4,name_1_1)
& sub(X3,land_1_1)
& loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [X0,X1,X2] :
( ( subr(X0,sub_0)
& arg2(X0,X2)
& arg1(X0,X1) )
=> ? [X3,X4,X5] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( val(X7,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X7,name_1_1)
& sub(X4,X9)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X8,X0)
& attr(X6,X7)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& in(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( val(X7,s__374dafrika_0)
& val(X2,nelson_0)
& val(X1,mandela_0)
& subr(X3,rprs_0)
& sub(X7,name_1_1)
& sub(X4,X9)
& sub(X2,eigenname_1_1)
& sub(X1,familiename_1_1)
& obj(X8,X0)
& attr(X6,X7)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0)
& in(X5,X6) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,hypothesis,
( varia(depesche_1_1,varia_c)
& refer(depesche_1_1,refer_c)
& quant(depesche_1_1,one)
& gener(depesche_1_1,ge)
& fact(depesche_1_1,real)
& etype(depesche_1_1,int0)
& card(depesche_1_1,int1)
& sort(depesche_1_1,io)
& sort(depesche_1_1,d)
& varia(gl__374ckwunsch_1_1,varia_c)
& refer(gl__374ckwunsch_1_1,refer_c)
& quant(gl__374ckwunsch_1_1,one)
& gener(gl__374ckwunsch_1_1,ge)
& fact(gl__374ckwunsch_1_1,real)
& etype(gl__374ckwunsch_1_1,int0)
& card(gl__374ckwunsch_1_1,int1)
& sort(gl__374ckwunsch_1_1,io)
& sort(gl__374ckwunsch_1_1,d)
& sort(gl__374ckwunsch_1_1,ad)
& gener(senden_1_2,ge)
& fact(senden_1_2,real)
& sort(senden_1_2,da)
& gener(c8235,sp)
& fact(c8235,real)
& sort(c8235,da)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& quant(gl__374ckwunschstelegramm_1_1,one)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& fact(gl__374ckwunschstelegramm_1_1,real)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& card(gl__374ckwunschstelegramm_1_1,int1)
& sort(gl__374ckwunschstelegramm_1_1,io)
& sort(gl__374ckwunschstelegramm_1_1,d)
& varia(c13631,varia_c)
& refer(c13631,indet)
& quant(c13631,one)
& gener(c13631,sp)
& fact(c13631,real)
& etype(c13631,int0)
& card(c13631,int1)
& sort(c13631,io)
& sort(c13631,d)
& gener(stellen_1_3,ge)
& fact(stellen_1_3,real)
& sort(stellen_1_3,da)
& sort(direkt_1_1,nq)
& varia(c13605,con)
& refer(c13605,det)
& quant(c13605,one)
& gener(c13605,sp)
& fact(c13605,real)
& etype(c13605,int0)
& card(c13605,int1)
& sort(c13605,io)
& sort(c13605,d)
& sort(c13605,ad)
& varia(c13603,varia_c)
& refer(c13603,det)
& quant(c13603,one)
& gener(c13603,sp)
& fact(c13603,real)
& etype(c13603,int0)
& card(c13603,int1)
& sort(c13603,o)
& varia(wahl_1_1,varia_c)
& refer(wahl_1_1,refer_c)
& quant(wahl_1_1,one)
& gener(wahl_1_1,ge)
& fact(wahl_1_1,real)
& etype(wahl_1_1,int0)
& card(wahl_1_1,int1)
& sort(wahl_1_1,ad)
& gener(c13616,sp)
& fact(c13616,real)
& sort(c13616,da)
& varia(c13598,varia_c)
& refer(c13598,det)
& quant(c13598,one)
& gener(c13598,sp)
& fact(c13598,real)
& etype(c13598,int0)
& card(c13598,int1)
& sort(c13598,ad)
& sort(mandela_0,fe)
& varia(familiename_1_1,varia_c)
& refer(familiename_1_1,refer_c)
& quant(familiename_1_1,one)
& gener(familiename_1_1,ge)
& fact(familiename_1_1,real)
& etype(familiename_1_1,int0)
& card(familiename_1_1,int1)
& sort(familiename_1_1,na)
& sort(nelson_0,fe)
& varia(pr__344sident_1_1,varia_c)
& refer(pr__344sident_1_1,refer_c)
& quant(pr__344sident_1_1,one)
& gener(pr__344sident_1_1,ge)
& fact(pr__344sident_1_1,real)
& etype(pr__344sident_1_1,int0)
& card(pr__344sident_1_1,int1)
& sort(pr__344sident_1_1,d)
& sort(s__374dafrikanisch_1_1,nq)
& varia(c11817,varia_c)
& refer(c11817,indet)
& quant(c11817,one)
& gener(c11817,sp)
& fact(c11817,real)
& etype(c11817,int0)
& card(c11817,int1)
& sort(c11817,na)
& varia(c11816,varia_c)
& refer(c11816,indet)
& quant(c11816,one)
& gener(c11816,sp)
& fact(c11816,real)
& etype(c11816,int0)
& card(c11816,int1)
& sort(c11816,na)
& varia(c11815,con)
& refer(c11815,det)
& quant(c11815,one)
& gener(c11815,sp)
& fact(c11815,real)
& etype(c11815,int0)
& card(c11815,int1)
& sort(c11815,d)
& sort(elisabeth_0,fe)
& varia(eigenname_1_1,varia_c)
& refer(eigenname_1_1,refer_c)
& quant(eigenname_1_1,one)
& gener(eigenname_1_1,ge)
& fact(eigenname_1_1,real)
& etype(eigenname_1_1,int0)
& card(eigenname_1_1,int1)
& sort(eigenname_1_1,na)
& varia(k__366nigin_1_1,varia_c)
& refer(k__366nigin_1_1,refer_c)
& quant(k__366nigin_1_1,one)
& gener(k__366nigin_1_1,ge)
& fact(k__366nigin_1_1,real)
& etype(k__366nigin_1_1,int0)
& card(k__366nigin_1_1,int1)
& sort(k__366nigin_1_1,d)
& varia(c11806,varia_c)
& refer(c11806,det)
& quant(c11806,one)
& gener(c11806,sp)
& fact(c11806,real)
& etype(c11806,int0)
& card(c11806,int1)
& sort(c11806,na)
& varia(c11805,varia_c)
& refer(c11805,det)
& quant(c11805,one)
& gener(c11805,sp)
& fact(c11805,real)
& etype(c11805,int0)
& card(c11805,int1)
& sort(c11805,d)
& varia(antrag_1_1,varia_c)
& refer(antrag_1_1,refer_c)
& quant(antrag_1_1,one)
& gener(antrag_1_1,ge)
& fact(antrag_1_1,real)
& etype(antrag_1_1,int0)
& card(antrag_1_1,int1)
& sort(antrag_1_1,io)
& sort(antrag_1_1,d)
& sort(antrag_1_1,ad)
& varia(aufnahme_2_1,varia_c)
& refer(aufnahme_2_1,refer_c)
& quant(aufnahme_2_1,one)
& gener(aufnahme_2_1,ge)
& fact(aufnahme_2_1,real)
& etype(aufnahme_2_1,int0)
& card(aufnahme_2_1,int1)
& sort(aufnahme_2_1,ad)
& varia(aufnahmeantrag_1_1,varia_c)
& refer(aufnahmeantrag_1_1,refer_c)
& quant(aufnahmeantrag_1_1,one)
& gener(aufnahmeantrag_1_1,ge)
& fact(aufnahmeantrag_1_1,real)
& etype(aufnahmeantrag_1_1,int0)
& card(aufnahmeantrag_1_1,int1)
& sort(aufnahmeantrag_1_1,io)
& sort(aufnahmeantrag_1_1,d)
& sort(aufnahmeantrag_1_1,ad)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& subs(c8235,senden_1_2)
& ornt(c8235,c11815)
& obj(c8235,c13631)
& agt(c8235,c11805)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& subs(c13616,stellen_1_3)
& obj(c13616,c13605)
& mannr(c13616,direkt_1_1)
& agt(c13616,c11815)
& sub(c13605,aufnahmeantrag_1_1)
& attch(c13603,c13598)
& subs(c13598,wahl_1_1)
& ante(c13598,c13616)
& val(c11817,mandela_0)
& sub(c11817,familiename_1_1)
& val(c11816,nelson_0)
& sub(c11816,eigenname_1_1)
& sub(c11815,pr__344sident_1_1)
& prop(c11815,s__374dafrikanisch_1_1)
& attr(c11815,c11817)
& attr(c11815,c11816)
& val(c11806,elisabeth_0)
& sub(c11806,eigenname_1_1)
& sub(c11805,k__366nigin_1_1)
& attr(c11805,c11806)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& assoc(aufnahmeantrag_1_1,aufnahme_2_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10674,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( val(X4,X2)
& sub(X4,name_1_1)
& sub(X3,land_1_1)
& loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) )
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f10675,plain,
! [X0,X2] :
( ? [X4] :
( val(X4,X2)
& sub(X4,name_1_1)
& ? [X3] :
( sub(X3,land_1_1)
& ? [X5] :
( loc(X0,X5)
& attr(X3,X4)
& in(X5,X3) ) ) )
| ! [X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ) ),
inference(miniscoping,[status(thm)],[f10674]) ).
fof(f10676,plain,
! [X0,X2] :
( ( val(sK47_skl(X2,X0),X2)
& sub(sK47_skl(X2,X0),name_1_1)
& sub(sK48_skl(X2,X0),land_1_1)
& loc(X0,sK49_skl(X2,X0))
& attr(sK48_skl(X2,X0),sK47_skl(X2,X0))
& in(sK49_skl(X2,X0),sK48_skl(X2,X0)) )
| ! [X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl]),skolemize(X4,sK47_skl(X2,X0)),skolemize(X3,sK48_skl(X2,X0)),skolemize(X5,sK49_skl(X2,X0))],[f10675]) ).
fof(f10677,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| in(sK49_skl(X0,X1),sK48_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10678,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| attr(sK48_skl(X0,X1),sK47_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10681,plain,
! [X0,X1,X2] :
( ~ prop(X2,X0)
| sub(sK47_skl(X1,X2),name_1_1)
| ~ state_adjective_state_binding(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10682,plain,
! [X0,X1,X2] :
( val(sK47_skl(X2,X0),X2)
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10715,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f162]) ).
fof(f10716,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,bezeichnen_1_1)
& ? [X4] :
( subr(X4,rprs_0)
& ? [X5] :
( sub(X5,X2)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X5)
& arg1(X4,X1) ) ) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(miniscoping,[status(thm)],[f10715]) ).
fof(f10717,plain,
! [X0,X1,X2] :
( ( subs(sK54_skl(X2,X1,X0),bezeichnen_1_1)
& subr(sK55_skl(X2,X1,X0),rprs_0)
& sub(sK56_skl(X2,X1,X0),X2)
& obj(sK54_skl(X2,X1,X0),X1)
& mcont(sK54_skl(X2,X1,X0),sK55_skl(X2,X1,X0))
& hsit(X0,sK54_skl(X2,X1,X0))
& arg2(sK55_skl(X2,X1,X0),sK56_skl(X2,X1,X0))
& arg1(sK55_skl(X2,X1,X0),X1) )
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl,sK55_skl,sK56_skl]),skolemize(X3,sK54_skl(X2,X1,X0)),skolemize(X4,sK55_skl(X2,X1,X0)),skolemize(X5,sK56_skl(X2,X1,X0))],[f10716]) ).
fof(f10718,plain,
! [X0,X1,X2] :
( arg1(sK55_skl(X1,X2,X0),X2)
| ~ arg1(X0,X2)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10719,plain,
! [X0,X1,X2] :
( ~ arg2(X0,X2)
| arg2(sK55_skl(X2,X1,X0),sK56_skl(X2,X1,X0))
| ~ arg1(X0,X1)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10722,plain,
! [X0,X1,X2] :
( ~ arg2(X0,X2)
| obj(sK54_skl(X2,X1,X0),X1)
| ~ arg1(X0,X1)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10723,plain,
! [X0,X1,X2] :
( ~ arg2(X0,X2)
| sub(sK56_skl(X2,X1,X0),X2)
| ~ arg1(X0,X1)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10724,plain,
! [X0,X1,X2] :
( subr(sK55_skl(X1,X2,X0),rprs_0)
| ~ subr(X0,sub_0)
| ~ arg1(X0,X2)
| ~ arg2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10717]) ).
fof(f10726,plain,
! [X0,X1] :
( ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) )
| ~ sub(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f163]) ).
fof(f10727,plain,
! [X0,X1] :
( ( subr(sK57_skl(X1,X0),sub_0)
& arg2(sK57_skl(X1,X0),X1)
& arg1(sK57_skl(X1,X0),X0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl]),skolemize(X2,sK57_skl(X1,X0))],[f10726]) ).
fof(f10728,plain,
! [X0,X1] :
( ~ sub(X1,X0)
| arg1(sK57_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
fof(f10729,plain,
! [X0,X1] :
( ~ sub(X1,X0)
| arg2(sK57_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
fof(f10730,plain,
! [X0,X1] :
( ~ sub(X1,X0)
| subr(sK57_skl(X0,X1),sub_0) ),
inference(cnf_transformation,[status(thm)],[f10727]) ).
fof(f19788,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[status(thm)],[f9161]) ).
fof(f20815,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ in(X5,X6) ),
inference(pre_NNF_transformation,[status(thm)],[f10189]) ).
fof(f20816,plain,
! [X7] :
( ~ val(X7,s__374dafrika_0)
| ! [X2] :
( ~ val(X2,nelson_0)
| ! [X1] :
( ~ val(X1,mandela_0)
| ! [X3] :
( ~ subr(X3,rprs_0)
| ~ sub(X7,name_1_1)
| ! [X4] :
( ! [X9] : ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ! [X0] :
( ! [X8] : ~ obj(X8,X0)
| ! [X6] :
( ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ! [X5] : ~ in(X5,X6) ) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f20815]) ).
fof(f20817,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X6,nelson_0)
| ~ val(X5,mandela_0)
| ~ subr(X2,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X4,X9)
| ~ sub(X6,eigenname_1_1)
| ~ sub(X5,familiename_1_1)
| ~ obj(X8,X3)
| ~ attr(X1,X7)
| ~ attr(X3,X6)
| ~ attr(X3,X5)
| ~ arg2(X2,X4)
| ~ arg1(X2,X3)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20816]) ).
fof(f20824,plain,
attr(c11815,c11816),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
attr(c11815,c11817),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
prop(c11815,s__374dafrikanisch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20827,plain,
sub(c11815,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20828,plain,
sub(c11816,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20829,plain,
val(c11816,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20830,plain,
sub(c11817,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20831,plain,
val(c11817,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21070,definition,
! [X0,X1,X7] :
( sQ0_spl
<=> ( ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X1,X7)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f21071,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ val(X1,s__374dafrika_0)
| ~ in(X2,X0)
| ~ sub(X1,name_1_1)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21070]) ).
fof(f21073,definition,
! [X2,X3,X4,X5,X6,X8,X9] :
( sQ1_spl
<=> ( ~ val(X6,nelson_0)
| ~ val(X5,mandela_0)
| ~ subr(X2,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X6,eigenname_1_1)
| ~ sub(X5,familiename_1_1)
| ~ obj(X8,X3)
| ~ attr(X3,X6)
| ~ attr(X3,X5)
| ~ arg2(X2,X4)
| ~ arg1(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f21074,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ val(X2,nelson_0)
| ~ sub(X4,familiename_1_1)
| ~ arg1(X0,X3)
| ~ val(X4,mandela_0)
| ~ obj(X6,X3)
| ~ attr(X3,X2)
| ~ sub(X1,X5)
| ~ subr(X0,rprs_0)
| ~ attr(X3,X4)
| ~ sub(X2,eigenname_1_1)
| ~ arg2(X0,X1) ),
inference(component_clause,[status(thm)],[f21073]) ).
fof(f21076,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21070,f21073]) ).
fof(f21884,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ sub(sK47_skl(s__374dafrika_0,X0),name_1_1)
| ~ in(X3,X2)
| ~ attr(X2,sK47_skl(s__374dafrika_0,X0))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(X0,X1) ),
inference(resolution,[status(thm)],[f10682,f21071]) ).
fof(f21885,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ prop(X1,X2)
| ~ in(X3,X0)
| ~ state_adjective_state_binding(X2,s__374dafrika_0)
| ~ attr(X0,sK47_skl(s__374dafrika_0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f21884,f10681]) ).
fof(f22649,plain,
! [X0,X1,X2,X3] :
( ~ sQ0_spl
| ~ state_adjective_state_binding(X2,s__374dafrika_0)
| ~ prop(X1,X0)
| ~ in(X3,sK48_skl(s__374dafrika_0,X1))
| ~ prop(X1,X2)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f10678,f21885]) ).
fof(f22650,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ in(X2,sK48_skl(s__374dafrika_0,X0))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(X0,s__374dafrikanisch_1_1)
| ~ prop(X0,X1) ),
inference(resolution,[status(thm)],[f22649,f19788]) ).
fof(f22694,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ prop(c11815,X0)
| ~ in(X1,sK48_skl(s__374dafrika_0,c11815))
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(resolution,[status(thm)],[f22650,f20826]) ).
fof(f22695,definition,
! [X0] :
( sQ2_spl
<=> ( ~ prop(c11815,X0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f22696,plain,
! [X0] :
( ~ sQ2_spl
| ~ prop(c11815,X0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(component_clause,[status(thm)],[f22695]) ).
fof(f22698,definition,
! [X1] :
( sQ3_spl
<=> ~ in(X1,sK48_skl(s__374dafrika_0,c11815)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f22699,plain,
! [X0] :
( ~ sQ3_spl
| ~ in(X0,sK48_skl(s__374dafrika_0,c11815)) ),
inference(component_clause,[status(thm)],[f22698]) ).
fof(f22701,plain,
( ~ sQ0_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f22694,f22695,f22698,f21070]) ).
fof(f22702,plain,
! [X0] :
( ~ sQ3_spl
| ~ state_adjective_state_binding(X0,s__374dafrika_0)
| ~ prop(c11815,X0) ),
inference(resolution,[status(thm)],[f22699,f10677]) ).
fof(f22716,plain,
( ~ sQ3_spl
| ~ prop(c11815,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f22702,f19788]) ).
fof(f22717,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22716,f20826]) ).
fof(f22718,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f22717]) ).
fof(f22731,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1_spl
| ~ obj(X5,X2)
| ~ sub(X3,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ sub(X0,eigenname_1_1)
| ~ val(c11817,mandela_0)
| ~ attr(X2,c11817)
| ~ attr(X2,X0)
| ~ subr(X1,rprs_0)
| ~ val(X0,nelson_0) ),
inference(resolution,[status(thm)],[f21074,f20830]) ).
fof(f22732,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ4_spl
<=> ( ~ obj(X5,X2)
| ~ sub(X3,X4)
| ~ arg2(X1,X3)
| ~ arg1(X1,X2)
| ~ sub(X0,eigenname_1_1)
| ~ attr(X2,c11817)
| ~ attr(X2,X0)
| ~ subr(X1,rprs_0)
| ~ val(X0,nelson_0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f22733,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ4_spl
| ~ arg2(X2,X4)
| ~ val(X1,nelson_0)
| ~ sub(X4,X5)
| ~ subr(X2,rprs_0)
| ~ obj(X3,X0)
| ~ attr(X0,c11817)
| ~ sub(X1,eigenname_1_1)
| ~ arg1(X2,X0)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f22732]) ).
fof(f22735,definition,
( sQ5_spl
<=> val(c11817,mandela_0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f22737,plain,
( sQ5_spl
| ~ val(c11817,mandela_0) ),
inference(component_clause,[status(thm)],[f22735]) ).
fof(f22738,plain,
( ~ sQ1_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f22731,f22732,f22735,f21073]) ).
fof(f22739,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22737,f20831]) ).
fof(f22740,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f22739]) ).
fof(f22750,plain,
( ~ sQ2_spl
| ~ prop(c11815,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f22696,f19788]) ).
fof(f22751,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22750,f20826]) ).
fof(f22752,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f22751]) ).
fof(f22762,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ arg2(X1,X3)
| ~ val(X0,nelson_0)
| ~ sub(X3,X4)
| ~ subr(X1,rprs_0)
| ~ obj(X2,c11815)
| ~ sub(X0,eigenname_1_1)
| ~ arg1(X1,c11815)
| ~ attr(c11815,X0) ),
inference(resolution,[status(thm)],[f22733,f20825]) ).
fof(f22763,definition,
! [X0] :
( sQ6_spl
<=> ( ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1)
| ~ attr(c11815,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f22764,plain,
! [X0] :
( ~ sQ6_spl
| ~ val(X0,nelson_0)
| ~ attr(c11815,X0)
| ~ sub(X0,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f22763]) ).
fof(f22766,definition,
! [X1,X3,X4] :
( sQ7_spl
<=> ( ~ arg2(X1,X3)
| ~ sub(X3,X4)
| ~ subr(X1,rprs_0)
| ~ arg1(X1,c11815) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f22767,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ arg1(X0,c11815)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ subr(X0,rprs_0) ),
inference(component_clause,[status(thm)],[f22766]) ).
fof(f22769,definition,
! [X2] :
( sQ8_spl
<=> ~ obj(X2,c11815) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f22770,plain,
! [X0] :
( ~ sQ8_spl
| ~ obj(X0,c11815) ),
inference(component_clause,[status(thm)],[f22769]) ).
fof(f22772,plain,
( ~ sQ4_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f22762,f22763,f22766,f22769,f22732]) ).
fof(f22993,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| ~ arg2(X0,X1)
| ~ arg2(sK55_skl(X1,X2,X0),X3)
| ~ sub(X3,X4)
| ~ arg1(X0,X2)
| ~ arg1(sK55_skl(X1,X2,X0),c11815)
| ~ subr(X0,sub_0) ),
inference(resolution,[status(thm)],[f22767,f10724]) ).
fof(f23027,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ arg1(X2,c11815)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0)
| ~ arg1(X2,c11815)
| ~ arg2(sK55_skl(X3,c11815,X2),X0)
| ~ subr(X2,sub_0)
| ~ arg2(X2,X3)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f22993,f10718]) ).
fof(f23028,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ arg1(X1,c11815)
| ~ sub(X2,X3)
| ~ subr(X1,sub_0)
| ~ arg2(X1,X0)
| ~ arg2(sK55_skl(X0,c11815,X1),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f23027]) ).
fof(f23038,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| ~ sub(X1,X0)
| ~ arg2(sK55_skl(X4,c11815,sK57_skl(X0,X1)),X2)
| ~ arg2(sK57_skl(X0,X1),X4)
| ~ sub(X2,X3)
| ~ arg1(sK57_skl(X0,X1),c11815) ),
inference(resolution,[status(thm)],[f23028,f10730]) ).
fof(f23040,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ sub(c11815,X2)
| ~ arg2(sK55_skl(X3,c11815,sK57_skl(X2,c11815)),X0)
| ~ arg2(sK57_skl(X2,c11815),X3)
| ~ sub(c11815,X2)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f23038,f10728]) ).
fof(f23041,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ arg2(sK57_skl(X0,c11815),X1)
| ~ sub(X2,X3)
| ~ arg2(sK55_skl(X1,c11815,sK57_skl(X0,c11815)),X2)
| ~ sub(c11815,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f23040]) ).
fof(f23055,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X0)
| ~ sub(X1,X2)
| ~ arg2(sK55_skl(X0,c11815,sK57_skl(pr__344sident_1_1,c11815)),X1) ),
inference(resolution,[status(thm)],[f23041,f20827]) ).
fof(f23059,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ sub(c11815,pr__344sident_1_1)
| ~ arg2(sK55_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f23055,f10729]) ).
fof(f23060,definition,
! [X0,X1] :
( sQ11_spl
<=> ( ~ arg2(sK55_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0)
| ~ sub(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f23061,plain,
! [X0,X1] :
( ~ sQ11_spl
| ~ sub(X0,X1)
| ~ arg2(sK55_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0) ),
inference(component_clause,[status(thm)],[f23060]) ).
fof(f23063,definition,
( sQ12_spl
<=> sub(c11815,pr__344sident_1_1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f23065,plain,
( sQ12_spl
| ~ sub(c11815,pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f23063]) ).
fof(f23066,plain,
( ~ sQ7_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f23059,f23060,f23063,f22766]) ).
fof(f23067,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23065,f20827]) ).
fof(f23068,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f23067]) ).
fof(f23070,plain,
( ~ sQ6_spl
| ~ attr(c11815,c11816)
| ~ sub(c11816,eigenname_1_1) ),
inference(resolution,[status(thm)],[f22764,f20829]) ).
fof(f23071,definition,
( sQ13_spl
<=> sub(c11816,eigenname_1_1) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f23073,plain,
( sQ13_spl
| ~ sub(c11816,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f23071]) ).
fof(f23074,definition,
( sQ14_spl
<=> attr(c11815,c11816) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f23076,plain,
( sQ14_spl
| ~ attr(c11815,c11816) ),
inference(component_clause,[status(thm)],[f23074]) ).
fof(f23077,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f23070,f23071,f23074,f22763]) ).
fof(f23078,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23073,f20828]) ).
fof(f23079,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f23078]) ).
fof(f23080,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23076,f20824]) ).
fof(f23081,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f23080]) ).
fof(f23141,plain,
! [X0] :
( ~ sQ11_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),pr__344sident_1_1)
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),c11815)
| ~ subr(sK57_skl(pr__344sident_1_1,c11815),sub_0)
| ~ sub(sK56_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0) ),
inference(resolution,[status(thm)],[f23061,f10719]) ).
fof(f23142,definition,
! [X0] :
( sQ15_spl
<=> ~ sub(sK56_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f23143,plain,
! [X0] :
( ~ sQ15_spl
| ~ sub(sK56_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),X0) ),
inference(component_clause,[status(thm)],[f23142]) ).
fof(f23145,definition,
( sQ16_spl
<=> subr(sK57_skl(pr__344sident_1_1,c11815),sub_0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f23146,plain,
( ~ sQ16_spl
| subr(sK57_skl(pr__344sident_1_1,c11815),sub_0) ),
inference(component_clause,[status(thm)],[f23145]) ).
fof(f23147,plain,
( sQ16_spl
| ~ subr(sK57_skl(pr__344sident_1_1,c11815),sub_0) ),
inference(component_clause,[status(thm)],[f23145]) ).
fof(f23148,definition,
( sQ17_spl
<=> arg1(sK57_skl(pr__344sident_1_1,c11815),c11815) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f23149,plain,
( ~ sQ17_spl
| arg1(sK57_skl(pr__344sident_1_1,c11815),c11815) ),
inference(component_clause,[status(thm)],[f23148]) ).
fof(f23150,plain,
( sQ17_spl
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),c11815) ),
inference(component_clause,[status(thm)],[f23148]) ).
fof(f23151,definition,
( sQ18_spl
<=> arg2(sK57_skl(pr__344sident_1_1,c11815),pr__344sident_1_1) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f23152,plain,
( ~ sQ18_spl
| arg2(sK57_skl(pr__344sident_1_1,c11815),pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f23151]) ).
fof(f23153,plain,
( sQ18_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),pr__344sident_1_1) ),
inference(component_clause,[status(thm)],[f23151]) ).
fof(f23154,plain,
( ~ sQ11_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f23141,f23142,f23145,f23148,f23151,f23060]) ).
fof(f23157,plain,
( sQ18_spl
| ~ sub(c11815,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f23153,f10729]) ).
fof(f23158,plain,
( sQ18_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f23157,f23063,f23151]) ).
fof(f23162,plain,
( sQ17_spl
| ~ sub(c11815,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f23150,f10728]) ).
fof(f23163,plain,
( sQ17_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f23162,f23063,f23148]) ).
fof(f23220,plain,
( sQ16_spl
| ~ sub(c11815,pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f23147,f10730]) ).
fof(f23221,plain,
( sQ16_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f23220,f23063,f23145]) ).
fof(f23300,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X1)
| sub(sK56_skl(X1,X0,sK57_skl(pr__344sident_1_1,c11815)),X1)
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),X0) ),
inference(resolution,[status(thm)],[f23146,f10723]) ).
fof(f23301,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X0)
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),X1)
| obj(sK54_skl(X0,X1,sK57_skl(pr__344sident_1_1,c11815)),X1) ),
inference(resolution,[status(thm)],[f23146,f10722]) ).
fof(f23431,plain,
! [X0] :
( ~ sQ18_spl
| ~ sQ16_spl
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),X0)
| sub(sK56_skl(pr__344sident_1_1,X0,sK57_skl(pr__344sident_1_1,c11815)),pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f23300,f23152]) ).
fof(f23470,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| ~ sQ16_spl
| sub(sK56_skl(pr__344sident_1_1,c11815,sK57_skl(pr__344sident_1_1,c11815)),pr__344sident_1_1) ),
inference(resolution,[status(thm)],[f23431,f23149]) ).
fof(f23472,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| ~ sQ16_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23470,f23143]) ).
fof(f23473,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| ~ sQ16_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f23472]) ).
fof(f23481,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ8_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X0)
| ~ arg1(sK57_skl(pr__344sident_1_1,c11815),c11815) ),
inference(resolution,[status(thm)],[f22770,f23301]) ).
fof(f23573,definition,
! [X0] :
( sQ23_spl
<=> ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X0) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f23574,plain,
! [X0] :
( ~ sQ23_spl
| ~ arg2(sK57_skl(pr__344sident_1_1,c11815),X0) ),
inference(component_clause,[status(thm)],[f23573]) ).
fof(f23576,plain,
( ~ sQ16_spl
| ~ sQ8_spl
| sQ23_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f23481,f23148,f23573,f22769,f23145]) ).
fof(f23581,plain,
( ~ sQ18_spl
| ~ sQ23_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f23152,f23574]) ).
fof(f23583,plain,
( ~ sQ18_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f23581]) ).
fof(f23584,plain,
$false,
inference(sat_refutation,[status(thm)],[f21076,f22701,f22718,f22738,f22740,f22752,f22772,f23066,f23068,f23077,f23079,f23081,f23154,f23158,f23163,f23221,f23473,f23576,f23583]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR116+18 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.45 % Computer : n010.cluster.edu
% 0.16/0.45 % Model : x86_64 x86_64
% 0.16/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.45 % Memory : 8046.5625MB
% 0.16/0.45 % OS : Linux 6.8.0-71-generic
% 0.16/0.45 % CPULimit : 300
% 0.16/0.45 % WCLimit : 300
% 0.16/0.45 % DateTime : Mon Sep 21 15:09:10 UTC 2026
% 0.16/0.46 % CPUTime :
% 0.34/0.73 % Drodi V4.1.1
% 22.14/3.54 % Refutation found
% 22.14/3.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.14/3.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.85/3.71 % Elapsed time: 3.228396 seconds
% 0.85/3.71 % CPU time: 22.624806 seconds
% 0.85/3.71 % Total memory used: 488.384 MB
% 0.85/3.71 % Net memory used: 481.974 MB
%------------------------------------------------------------------------------