%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR116+28 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:11 PM UTC 2026
% Result : Theorem 78.39s 10.50s
% Output : CNFRefutation 41.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 27
% Syntax : Number of formulae : 142 ( 24 unt; 18 def)
% Number of atoms : 811 ( 0 equ)
% Maximal formula atoms : 253 ( 5 avg)
% Number of connectives : 1011 ( 342 ~; 302 |; 344 &)
% ( 18 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 253 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 50 ( 49 usr; 19 prp; 0-2 aty)
% Number of functors : 71 ( 71 usr; 63 con; 0-3 aty)
% Number of variables : 270 ( 230 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [X0,X1] :
( ( loc(X1,X0)
& has_fact_leq(X1,real) )
=> ? [X2] :
( subs(X2,geben_1_1)
& obj(X2,X1)
& loc(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,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,hei__337en_1_1)
& arg2(X3,X2)
& arg1(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( subs(X0,hei__337en_1_1)
& arg2(X0,X2)
& arg1(X0,X1) )
=> ? [X3,X4] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/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/sandbox2/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(orden_1_1,varia_c)
& refer(orden_1_1,refer_c)
& quant(orden_1_1,quant_c)
& gener(orden_1_1,ge)
& fact(orden_1_1,real)
& etype(orden_1_1,int1)
& card(orden_1_1,card_c)
& sort(orden_1_1,io)
& sort(orden_1_1,d)
& varia(verdienst_2_1,varia_c)
& refer(verdienst_2_1,refer_c)
& quant(verdienst_2_1,one)
& gener(verdienst_2_1,ge)
& fact(verdienst_2_1,real)
& etype(verdienst_2_1,int0)
& card(verdienst_2_1,int1)
& sort(verdienst_2_1,io)
& sort(verdienst_2_1,as)
& varia(an_f__374hrer_1_1,varia_c)
& refer(an_f__374hrer_1_1,refer_c)
& quant(an_f__374hrer_1_1,one)
& gener(an_f__374hrer_1_1,ge)
& fact(an_f__374hrer_1_1,real)
& etype(an_f__374hrer_1_1,int0)
& card(an_f__374hrer_1_1,int1)
& sort(an_f__374hrer_1_1,d)
& varia(residenz__1_1,varia_c)
& refer(residenz__1_1,refer_c)
& quant(residenz__1_1,one)
& gener(residenz__1_1,ge)
& fact(residenz__1_1,real)
& etype(residenz__1_1,int0)
& card(residenz__1_1,int1)
& sort(residenz__1_1,d)
& sort(s__374dafrika_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(land_1_1,varia_c)
& refer(land_1_1,refer_c)
& quant(land_1_1,one)
& gener(land_1_1,ge)
& fact(land_1_1,real)
& etype(land_1_1,int0)
& card(land_1_1,int1)
& sort(land_1_1,io)
& sort(land_1_1,d)
& varia(c32,varia_c)
& refer(c32,indet)
& quant(c32,one)
& gener(c32,sp)
& fact(c32,real)
& etype(c32,int0)
& card(c32,int1)
& sort(c32,na)
& varia(c31,con)
& refer(c31,det)
& quant(c31,one)
& gener(c31,sp)
& fact(c31,real)
& etype(c31,int0)
& card(c31,int1)
& sort(c31,io)
& sort(c31,d)
& varia(landesvater_1_1,varia_c)
& refer(landesvater_1_1,refer_c)
& quant(landesvater_1_1,one)
& gener(landesvater_1_1,ge)
& fact(landesvater_1_1,real)
& etype(landesvater_1_1,int0)
& card(landesvater_1_1,int1)
& sort(landesvater_1_1,d)
& varia(c287,varia_c)
& refer(c287,indet)
& quant(c287,mult)
& gener(c287,sp)
& fact(c287,real)
& etype(c287,int1)
& card(c287,cons(x_constant,cons(int1,nil)))
& sort(c287,l)
& gener(auszeichnen_1_1,ge)
& fact(auszeichnen_1_1,real)
& sort(auszeichnen_1_1,da)
& varia(c29,varia_c)
& refer(c29,refer_c)
& quant(c29,one)
& gener(c29,sp)
& fact(c29,real)
& etype(c29,int0)
& card(c29,int1)
& sort(c29,d)
& varia(c288,con)
& refer(c288,det)
& quant(c288,one)
& gener(c288,sp)
& fact(c288,real)
& etype(c288,int0)
& card(c288,int1)
& sort(c288,l)
& gener(c284,sp)
& fact(c284,real)
& sort(c284,da)
& varia(verdienstorden_1_1,varia_c)
& refer(verdienstorden_1_1,refer_c)
& quant(verdienstorden_1_1,quant_c)
& gener(verdienstorden_1_1,ge)
& fact(verdienstorden_1_1,real)
& etype(verdienstorden_1_1,int1)
& card(verdienstorden_1_1,card_c)
& sort(verdienstorden_1_1,io)
& sort(verdienstorden_1_1,d)
& varia(c277,con)
& refer(c277,det)
& quant(c277,one)
& gener(c277,sp)
& fact(c277,real)
& etype(c277,int1)
& card(c277,int1)
& sort(c277,io)
& sort(c277,d)
& 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(c26,con)
& refer(c26,det)
& quant(c26,one)
& gener(c26,sp)
& fact(c26,real)
& etype(c26,int0)
& card(c26,int1)
& sort(c26,d)
& varia(tuinhuys_1_1,varia_c)
& refer(tuinhuys_1_1,refer_c)
& quant(tuinhuys_1_1,one)
& gener(tuinhuys_1_1,ge)
& fact(tuinhuys_1_1,real)
& etype(tuinhuys_1_1,int0)
& card(tuinhuys_1_1,int1)
& sort(tuinhuys_1_1,o)
& varia(c21,varia_c)
& refer(c21,indet)
& quant(c21,mult)
& gener(c21,sp)
& fact(c21,real)
& etype(c21,int1)
& card(c21,cons(x_constant,cons(int1,nil)))
& sort(c21,o)
& 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(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(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(c19,varia_c)
& refer(c19,indet)
& quant(c19,one)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,int0)
& card(c19,int1)
& sort(c19,na)
& varia(c18,varia_c)
& refer(c18,indet)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int0)
& card(c18,int1)
& sort(c18,na)
& varia(c8,con)
& refer(c8,det)
& quant(c8,one)
& gener(c8,sp)
& fact(c8,real)
& etype(c8,int0)
& card(c8,int1)
& sort(c8,d)
& varia(c17,con)
& refer(c17,det)
& quant(c17,one)
& gener(c17,sp)
& fact(c17,real)
& etype(c17,int0)
& card(c17,int1)
& sort(c17,d)
& sort(c0,tq)
& gener(anschlie__337en_1_1,ge)
& fact(anschlie__337en_1_1,real)
& sort(anschlie__337en_1_1,da)
& sub(verdienstorden_1_1,orden_1_1)
& assoc(verdienstorden_1_1,verdienst_2_1)
& sub(landesvater_1_1,an_f__374hrer_1_1)
& assoc(landesvater_1_1,land_1_1)
& sub(c8,residenz__1_1)
& loc(c8,c287)
& val(c32,s__374dafrika_0)
& sub(c32,name_1_1)
& sub(c31,land_1_1)
& attr(c31,c32)
& attch(c31,c26)
& sub(c29,landesvater_1_1)
& in(c288,c8)
& in(c287,c21)
& subs(c284,auszeichnen_1_1)
& ornt(c284,c29)
& mannr(c284,c0)
& loc(c284,c288)
& assoc(c284,c277)
& agt(c284,c26)
& sub(c277,verdienstorden_1_1)
& sub(c26,k__366nigin_1_1)
& pred(c21,tuinhuys_1_1)
& val(c19,mandela_0)
& sub(c19,familiename_1_1)
& val(c18,nelson_0)
& sub(c18,eigenname_1_1)
& sub(c17,pr__344sident_1_1)
& prop(c17,s__374dafrikanisch_1_1)
& attr(c17,c19)
& attr(c17,c18)
& attch(c17,c8)
& chsp1(anschlie__337en_1_1,c0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10191,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f10209,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f10210,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10209]) ).
fof(f10363,plain,
! [X0,X1] :
( ? [X2] :
( subs(X2,geben_1_1)
& obj(X2,X1)
& loc(X2,X0) )
| ~ loc(X1,X0)
| ~ has_fact_leq(X1,real) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f10364,plain,
! [X0,X1] :
( ( subs(sK2_skl(X1,X0),geben_1_1)
& obj(sK2_skl(X1,X0),X1)
& loc(sK2_skl(X1,X0),X0) )
| ~ loc(X1,X0)
| ~ has_fact_leq(X1,real) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X2,sK2_skl(X1,X0))],[f10363]) ).
fof(f10366,plain,
! [X0,X1] :
( ~ loc(X0,X1)
| obj(sK2_skl(X0,X1),X0)
| ~ has_fact_leq(X0,real) ),
inference(cnf_transformation,[status(thm)],[f10364]) ).
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] :
( in(sK49_skl(X2,X0),sK48_skl(X2,X0))
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10678,plain,
! [X0,X1,X2] :
( attr(sK48_skl(X2,X0),sK47_skl(X2,X0))
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10679,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X1,X2)
| loc(X0,sK49_skl(X2,X0))
| ~ prop(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10676]) ).
fof(f10681,plain,
! [X0,X1,X2] :
( ~ state_adjective_state_binding(X2,X0)
| ~ prop(X1,X2)
| sub(sK47_skl(X0,X1),name_1_1) ),
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(f10692,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,hei__337en_1_1)
& arg2(X3,X2)
& arg1(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)],[f159]) ).
fof(f10693,plain,
! [X2] :
( ? [X3] :
( subs(X3,hei__337en_1_1)
& arg2(X3,X2)
& arg1(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)],[f10692]) ).
fof(f10694,plain,
! [X2] :
( ( subs(sK50_skl(X2),hei__337en_1_1)
& arg2(sK50_skl(X2),X2)
& arg1(sK50_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,[sK50_skl]),skolemize(X3,sK50_skl(X2))],[f10693]) ).
fof(f10695,plain,
! [X0,X1,X2] :
( ~ sub(X2,X0)
| ~ attr(X1,X2)
| arg1(sK50_skl(X1),X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10696,plain,
! [X0,X1,X2] :
( ~ sub(X2,X0)
| arg2(sK50_skl(X1),X1)
| ~ attr(X1,X2)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10697,plain,
! [X0,X1,X2] :
( ~ sub(X2,X0)
| subs(sK50_skl(X1),hei__337en_1_1)
| ~ attr(X1,X2)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(cnf_transformation,[status(thm)],[f10694]) ).
fof(f10705,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( subs(X3,bezeichnen_1_1)
& subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f161]) ).
fof(f10706,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,bezeichnen_1_1)
& ? [X4] :
( subr(X4,rprs_0)
& obj(X3,X1)
& mcont(X3,X4)
& hsit(X0,X3)
& arg2(X4,X2)
& arg1(X4,X1) ) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(miniscoping,[status(thm)],[f10705]) ).
fof(f10707,plain,
! [X0,X1,X2] :
( ( subs(sK52_skl(X2,X1,X0),bezeichnen_1_1)
& subr(sK53_skl(X2,X1,X0),rprs_0)
& obj(sK52_skl(X2,X1,X0),X1)
& mcont(sK52_skl(X2,X1,X0),sK53_skl(X2,X1,X0))
& hsit(X0,sK52_skl(X2,X1,X0))
& arg2(sK53_skl(X2,X1,X0),X2)
& arg1(sK53_skl(X2,X1,X0),X1) )
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl]),skolemize(X3,sK52_skl(X2,X1,X0)),skolemize(X4,sK53_skl(X2,X1,X0))],[f10706]) ).
fof(f10708,plain,
! [X0,X1,X2] :
( ~ subs(X2,hei__337en_1_1)
| ~ arg2(X2,X0)
| ~ arg1(X2,X1)
| arg1(sK53_skl(X0,X1,X2),X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10709,plain,
! [X0,X1,X2] :
( ~ subs(X2,hei__337en_1_1)
| ~ arg1(X2,X1)
| ~ arg2(X2,X0)
| arg2(sK53_skl(X0,X1,X2),X0) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
fof(f10713,plain,
! [X0,X1,X2] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X2)
| subr(sK53_skl(X1,X2,X0),rprs_0)
| ~ arg2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f10707]) ).
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(f20820,plain,
attr(c17,c18),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20821,plain,
attr(c17,c19),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20822,plain,
prop(c17,s__374dafrikanisch_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20823,plain,
sub(c17,pr__344sident_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20824,plain,
sub(c18,eigenname_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20825,plain,
val(c18,nelson_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20826,plain,
sub(c19,familiename_1_1),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20827,plain,
val(c19,mandela_0),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f20858,plain,
fact(c17,real),
inference(cnf_transformation,[status(thm)],[f10190]) ).
fof(f21106,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(f21107,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ sub(X1,name_1_1)
| ~ val(X1,s__374dafrika_0)
| ~ in(X2,X0)
| ~ attr(X0,X1) ),
inference(component_clause,[status(thm)],[f21106]) ).
fof(f21109,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(f21110,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ1_spl
| ~ arg1(X6,X3)
| ~ val(X4,nelson_0)
| ~ sub(X5,familiename_1_1)
| ~ sub(X4,eigenname_1_1)
| ~ subr(X6,rprs_0)
| ~ arg2(X6,X0)
| ~ attr(X3,X5)
| ~ val(X5,mandela_0)
| ~ attr(X3,X4)
| ~ obj(X2,X3)
| ~ sub(X0,X1) ),
inference(component_clause,[status(thm)],[f21109]) ).
fof(f21112,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20817,f21106,f21109]) ).
fof(f21126,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1_spl
| ~ arg2(X0,X4)
| ~ val(X2,mandela_0)
| ~ sub(X4,X5)
| ~ subr(X0,rprs_0)
| ~ attr(X1,c18)
| ~ sub(X2,familiename_1_1)
| ~ sub(c18,eigenname_1_1)
| ~ obj(X3,X1)
| ~ attr(X1,X2)
| ~ arg1(X0,X1) ),
inference(resolution,[status(thm)],[f20825,f21110]) ).
fof(f21127,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ4_spl
<=> ( ~ arg2(X0,X4)
| ~ val(X2,mandela_0)
| ~ sub(X4,X5)
| ~ subr(X0,rprs_0)
| ~ attr(X1,c18)
| ~ sub(X2,familiename_1_1)
| ~ obj(X3,X1)
| ~ attr(X1,X2)
| ~ arg1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f21128,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ4_spl
| ~ arg1(X0,X1)
| ~ obj(X5,X1)
| ~ arg2(X0,X2)
| ~ attr(X1,X4)
| ~ val(X4,mandela_0)
| ~ sub(X4,familiename_1_1)
| ~ sub(X2,X3)
| ~ attr(X1,c18)
| ~ subr(X0,rprs_0) ),
inference(component_clause,[status(thm)],[f21127]) ).
fof(f21130,definition,
( sQ5_spl
<=> sub(c18,eigenname_1_1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f21131,plain,
( ~ sQ5_spl
| sub(c18,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f21130]) ).
fof(f21132,plain,
( sQ5_spl
| ~ sub(c18,eigenname_1_1) ),
inference(component_clause,[status(thm)],[f21130]) ).
fof(f21133,plain,
( ~ sQ1_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f21126,f21127,f21130,f21109]) ).
fof(f22132,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20824,f21132]) ).
fof(f22133,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f22132]) ).
fof(f22859,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ arg1(X0,c17)
| ~ obj(X4,c17)
| ~ arg2(X0,X1)
| ~ attr(c17,X3)
| ~ val(X3,mandela_0)
| ~ sub(X3,familiename_1_1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0) ),
inference(resolution,[status(thm)],[f20820,f21128]) ).
fof(f22860,definition,
! [X0,X1,X2] :
( sQ310_spl
<=> ( ~ arg1(X0,c17)
| ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0) ) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f22861,plain,
! [X0,X1,X2] :
( ~ sQ310_spl
| ~ arg1(X2,c17)
| ~ arg2(X2,X0)
| ~ subr(X2,rprs_0)
| ~ sub(X0,X1) ),
inference(component_clause,[status(thm)],[f22860]) ).
fof(f22863,definition,
! [X3] :
( sQ311_spl
<=> ( ~ attr(c17,X3)
| ~ val(X3,mandela_0)
| ~ sub(X3,familiename_1_1) ) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f22864,plain,
! [X0] :
( ~ sQ311_spl
| ~ attr(c17,X0)
| ~ val(X0,mandela_0)
| ~ sub(X0,familiename_1_1) ),
inference(component_clause,[status(thm)],[f22863]) ).
fof(f22866,definition,
! [X4] :
( sQ312_spl
<=> ~ obj(X4,c17) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f22867,plain,
! [X0] :
( ~ sQ312_spl
| ~ obj(X0,c17) ),
inference(component_clause,[status(thm)],[f22866]) ).
fof(f22869,plain,
( ~ sQ4_spl
| sQ312_spl
| sQ311_spl
| sQ310_spl ),
inference(split_clause,[status(thm)],[f22859,f22860,f22863,f22866,f21127]) ).
fof(f22943,plain,
( ~ sQ311_spl
| ~ attr(c17,c19)
| ~ val(c19,mandela_0) ),
inference(resolution,[status(thm)],[f22864,f20826]) ).
fof(f22944,definition,
( sQ327_spl
<=> val(c19,mandela_0) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f22946,plain,
( sQ327_spl
| ~ val(c19,mandela_0) ),
inference(component_clause,[status(thm)],[f22944]) ).
fof(f22947,definition,
( sQ328_spl
<=> attr(c17,c19) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f22949,plain,
( sQ328_spl
| ~ attr(c17,c19) ),
inference(component_clause,[status(thm)],[f22947]) ).
fof(f22950,plain,
( ~ sQ311_spl
| ~ sQ328_spl
| ~ sQ327_spl ),
inference(split_clause,[status(thm)],[f22943,f22944,f22947,f22863]) ).
fof(f22951,plain,
( sQ328_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22949,f20821]) ).
fof(f22952,plain,
sQ328_spl,
inference(contradiction_clause,[status(thm)],[f22951]) ).
fof(f22953,plain,
( sQ327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22946,f20827]) ).
fof(f22954,plain,
sQ327_spl,
inference(contradiction_clause,[status(thm)],[f22953]) ).
fof(f24884,definition,
! [X0,X1] :
( sQ663_spl
<=> ( ~ sub(X1,X0)
| ~ attr(c17,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ) ),
introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition]) ).
fof(f24885,plain,
! [X0,X1] :
( ~ sQ663_spl
| ~ sub(X1,X0)
| ~ attr(c17,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(component_clause,[status(thm)],[f24884]) ).
fof(f24887,definition,
! [X2,X3] :
( sQ664_spl
<=> ( ~ sub(X2,X3)
| ~ arg2(sK50_skl(c17),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition]) ).
fof(f24888,plain,
! [X0,X1] :
( ~ sQ664_spl
| ~ arg2(sK50_skl(c17),X0)
| ~ sub(X0,X1) ),
inference(component_clause,[status(thm)],[f24887]) ).
fof(f25081,plain,
! [X0] :
( ~ sQ663_spl
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(c18,X0) ),
inference(resolution,[status(thm)],[f24885,f20820]) ).
fof(f25117,plain,
( ~ sQ5_spl
| ~ sQ663_spl
| ~ member(eigenname_1_1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(resolution,[status(thm)],[f25081,f21131]) ).
fof(f25118,plain,
( ~ sQ5_spl
| ~ sQ663_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25117,f10191]) ).
fof(f25119,plain,
( ~ sQ5_spl
| ~ sQ663_spl ),
inference(contradiction_clause,[status(thm)],[f25118]) ).
fof(f25222,plain,
! [X0,X1,X2] :
( ~ sQ664_spl
| ~ sub(c17,X2)
| ~ sub(X1,X0)
| ~ attr(c17,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ),
inference(resolution,[status(thm)],[f10696,f24888]) ).
fof(f25223,definition,
! [X2] :
( sQ709_spl
<=> ~ sub(c17,X2) ),
introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition]) ).
fof(f25224,plain,
! [X0] :
( ~ sQ709_spl
| ~ sub(c17,X0) ),
inference(component_clause,[status(thm)],[f25223]) ).
fof(f25226,plain,
( ~ sQ664_spl
| sQ709_spl
| sQ663_spl ),
inference(split_clause,[status(thm)],[f25222,f24884,f25223,f24887]) ).
fof(f25227,plain,
( ~ sQ709_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20823,f25224]) ).
fof(f25228,plain,
~ sQ709_spl,
inference(contradiction_clause,[status(thm)],[f25227]) ).
fof(f27643,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK49_skl(s__374dafrika_0,X0),sK48_skl(s__374dafrika_0,X0)) ),
inference(resolution,[status(thm)],[f10677,f19788]) ).
fof(f28290,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| sub(sK47_skl(s__374dafrika_0,X0),name_1_1) ),
inference(resolution,[status(thm)],[f10681,f19788]) ).
fof(f29159,plain,
! [X0] :
( loc(X0,sK49_skl(s__374dafrika_0,X0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f10679,f19788]) ).
fof(f30137,plain,
sub(sK47_skl(s__374dafrika_0,c17),name_1_1),
inference(resolution,[status(thm)],[f28290,f20822]) ).
fof(f31826,plain,
loc(c17,sK49_skl(s__374dafrika_0,c17)),
inference(resolution,[status(thm)],[f29159,f20822]) ).
fof(f33393,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ val(sK47_skl(s__374dafrika_0,c17),s__374dafrika_0)
| ~ in(X1,X0)
| ~ attr(X0,sK47_skl(s__374dafrika_0,c17)) ),
inference(resolution,[status(thm)],[f30137,f21107]) ).
fof(f33407,definition,
! [X0,X1] :
( sQ1890_spl
<=> ( ~ in(X1,X0)
| ~ attr(X0,sK47_skl(s__374dafrika_0,c17)) ) ),
introduced(definition,[new_symbols(definition,[sQ1890_spl])],[split_symbol_definition]) ).
fof(f33408,plain,
! [X0,X1] :
( ~ sQ1890_spl
| ~ in(X1,X0)
| ~ attr(X0,sK47_skl(s__374dafrika_0,c17)) ),
inference(component_clause,[status(thm)],[f33407]) ).
fof(f33410,definition,
( sQ1891_spl
<=> val(sK47_skl(s__374dafrika_0,c17),s__374dafrika_0) ),
introduced(definition,[new_symbols(definition,[sQ1891_spl])],[split_symbol_definition]) ).
fof(f33412,plain,
( sQ1891_spl
| ~ val(sK47_skl(s__374dafrika_0,c17),s__374dafrika_0) ),
inference(component_clause,[status(thm)],[f33410]) ).
fof(f33413,plain,
( ~ sQ0_spl
| ~ sQ1891_spl
| sQ1890_spl ),
inference(split_clause,[status(thm)],[f33393,f33407,f33410,f21106]) ).
fof(f33471,plain,
! [X0,X1] :
( ~ sQ1890_spl
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(c17,X1)
| ~ in(X0,sK48_skl(s__374dafrika_0,c17)) ),
inference(resolution,[status(thm)],[f33408,f10678]) ).
fof(f33472,definition,
! [X0] :
( sQ1896_spl
<=> ~ in(X0,sK48_skl(s__374dafrika_0,c17)) ),
introduced(definition,[new_symbols(definition,[sQ1896_spl])],[split_symbol_definition]) ).
fof(f33473,plain,
! [X0] :
( ~ sQ1896_spl
| ~ in(X0,sK48_skl(s__374dafrika_0,c17)) ),
inference(component_clause,[status(thm)],[f33472]) ).
fof(f33475,definition,
! [X1] :
( sQ1897_spl
<=> ( ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(c17,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ1897_spl])],[split_symbol_definition]) ).
fof(f33476,plain,
! [X0] :
( ~ sQ1897_spl
| ~ prop(c17,X0)
| ~ state_adjective_state_binding(X0,s__374dafrika_0) ),
inference(component_clause,[status(thm)],[f33475]) ).
fof(f33478,plain,
( ~ sQ1890_spl
| sQ1897_spl
| sQ1896_spl ),
inference(split_clause,[status(thm)],[f33471,f33472,f33475,f33407]) ).
fof(f33479,plain,
( ~ sQ1896_spl
| ~ prop(c17,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f33473,f27643]) ).
fof(f33480,plain,
( ~ sQ1896_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33479,f20822]) ).
fof(f33481,plain,
~ sQ1896_spl,
inference(contradiction_clause,[status(thm)],[f33480]) ).
fof(f33482,plain,
! [X0] :
( sQ1891_spl
| ~ state_adjective_state_binding(X0,s__374dafrika_0)
| ~ prop(c17,X0) ),
inference(resolution,[status(thm)],[f33412,f10682]) ).
fof(f33505,plain,
( ~ sQ1897_spl
| ~ prop(c17,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f33476,f19788]) ).
fof(f33506,plain,
( ~ sQ1897_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33505,f20822]) ).
fof(f33507,plain,
~ sQ1897_spl,
inference(contradiction_clause,[status(thm)],[f33506]) ).
fof(f33540,plain,
( sQ1891_spl
| ~ prop(c17,s__374dafrikanisch_1_1) ),
inference(resolution,[status(thm)],[f33482,f19788]) ).
fof(f33541,plain,
( sQ1891_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33540,f20822]) ).
fof(f33542,plain,
sQ1891_spl,
inference(contradiction_clause,[status(thm)],[f33541]) ).
fof(f37453,plain,
( obj(sK2_skl(c17,sK49_skl(s__374dafrika_0,c17)),c17)
| ~ has_fact_leq(c17,real) ),
inference(resolution,[status(thm)],[f31826,f10366]) ).
fof(f37466,definition,
( sQ2473_spl
<=> has_fact_leq(c17,real) ),
introduced(definition,[new_symbols(definition,[sQ2473_spl])],[split_symbol_definition]) ).
fof(f37468,plain,
( sQ2473_spl
| ~ has_fact_leq(c17,real) ),
inference(component_clause,[status(thm)],[f37466]) ).
fof(f37469,definition,
( sQ2474_spl
<=> obj(sK2_skl(c17,sK49_skl(s__374dafrika_0,c17)),c17) ),
introduced(definition,[new_symbols(definition,[sQ2474_spl])],[split_symbol_definition]) ).
fof(f37470,plain,
( ~ sQ2474_spl
| obj(sK2_skl(c17,sK49_skl(s__374dafrika_0,c17)),c17) ),
inference(component_clause,[status(thm)],[f37469]) ).
fof(f37472,plain,
( sQ2474_spl
| ~ sQ2473_spl ),
inference(split_clause,[status(thm)],[f37453,f37466,f37469]) ).
fof(f37484,plain,
( ~ sQ2474_spl
| ~ sQ312_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37470,f22867]) ).
fof(f37485,plain,
( ~ sQ2474_spl
| ~ sQ312_spl ),
inference(contradiction_clause,[status(thm)],[f37484]) ).
fof(f37517,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ310_spl
| ~ arg2(X0,X4)
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(sK53_skl(X4,X1,X0),c17)
| ~ arg2(sK53_skl(X4,X1,X0),X2)
| ~ sub(X2,X3)
| ~ arg1(X0,X1) ),
inference(resolution,[status(thm)],[f22861,f10713]) ).
fof(f37540,plain,
( sQ2473_spl
| ~ fact(c17,real) ),
inference(resolution,[status(thm)],[f37468,f10210]) ).
fof(f37541,plain,
( sQ2473_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37540,f20858]) ).
fof(f37542,plain,
sQ2473_spl,
inference(contradiction_clause,[status(thm)],[f37541]) ).
fof(f37600,plain,
! [X0,X1,X2,X3] :
( ~ sQ310_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X3)
| ~ arg1(X0,c17)
| ~ arg2(X0,X3)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(sK53_skl(X3,c17,X0),X1)
| ~ sub(X1,X2)
| ~ arg1(X0,c17) ),
inference(resolution,[status(thm)],[f37517,f10708]) ).
fof(f37601,plain,
! [X0,X1,X2,X3] :
( ~ sQ310_spl
| ~ arg1(X0,c17)
| ~ arg2(X0,X1)
| ~ sub(X2,X3)
| ~ arg2(sK53_skl(X1,c17,X0),X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(duplicate_literals_removal,[status(thm)],[f37600]) ).
fof(f37646,plain,
! [X0,X1,X2] :
( ~ sQ310_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,c17)
| ~ arg2(X0,X1)
| ~ arg1(X0,c17)
| ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(resolution,[status(thm)],[f37601,f10709]) ).
fof(f37647,plain,
! [X0,X1,X2] :
( ~ sQ310_spl
| ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,c17)
| ~ sub(X1,X2)
| ~ arg2(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f37646]) ).
fof(f37671,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ310_spl
| ~ arg2(sK50_skl(X0),X3)
| ~ attr(X0,X1)
| ~ sub(X3,X4)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| ~ arg1(sK50_skl(X0),c17) ),
inference(resolution,[status(thm)],[f37647,f10697]) ).
fof(f38180,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ310_spl
| ~ sub(X5,X4)
| ~ attr(c17,X5)
| ~ member(X4,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ arg2(sK50_skl(c17),X2)
| ~ attr(c17,X0)
| ~ sub(X2,X3)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[f37671,f10695]) ).
fof(f38181,plain,
( ~ sQ310_spl
| sQ664_spl
| sQ663_spl ),
inference(split_clause,[status(thm)],[f38180,f24884,f24887,f22860]) ).
fof(f38182,plain,
$false,
inference(sat_refutation,[status(thm)],[f21112,f21133,f22133,f22869,f22950,f22952,f22954,f25119,f25226,f25228,f33413,f33478,f33481,f33507,f33542,f37472,f37485,f37542,f38181]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+28 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 15:12:37 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.23/0.50 % Drodi V4.1.1
% 78.39/10.50 % Refutation found
% 78.39/10.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 78.39/10.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 41.89/10.70 % Elapsed time: 10.306986 seconds
% 41.89/10.70 % CPU time: 79.457307 seconds
% 41.89/10.70 % Total memory used: 632.342 MB
% 41.89/10.70 % Net memory used: 601.313 MB
%------------------------------------------------------------------------------