%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR116+30 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:11:23 PM UTC 2026
% Result : Theorem 1.68s 1.39s
% Output : CNFRefutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 74 ( 7 unt; 0 def)
% Number of atoms : 791 ( 0 equ)
% Maximal formula atoms : 106 ( 10 avg)
% Number of connectives : 910 ( 193 ~; 179 |; 536 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 106 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 21 usr; 3 prp; 0-3 aty)
% Number of functors : 47 ( 47 usr; 43 con; 0-3 aty)
% Number of variables : 162 ( 0 sgn 133 !; 29 ?; 76 :)
% Comments :
%------------------------------------------------------------------------------
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/sandbox2/benchmark/Axioms/CSR004+0.ax',sub__bezeichnen_1_1_als) ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',sub__sub_0_expansion) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( subr(X3,rprs_0)
& sub(X6,name_1_1)
& sub(X4,X8)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_news_1834) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( subr(X3,rprs_0)
& sub(X6,name_1_1)
& sub(X4,X8)
& obj(X7,X0)
& attr(X5,X6)
& attr(X0,X2)
& attr(X0,X1)
& arg2(X3,X4)
& arg1(X3,X0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( varia(c47,varia_c)
& refer(c47,refer_c)
& quant(c47,quant_c)
& gener(c47,gener_c)
& fact(c47,real)
& etype(c47,etype_c)
& card(c47,card_c)
& sort(c47,ent)
& card(c17,int7)
& sort(c17,nu)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& quant(monat_1_1,quant_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& etype(monat_1_1,etype_c)
& card(monat_1_1,card_c)
& sort(monat_1_1,ta)
& sort(monat_1_1,oa)
& sort(monat_1_1,me)
& card(c16,int21)
& sort(c16,nu)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& quant(tag_1_1,quant_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& etype(tag_1_1,etype_c)
& card(tag_1_1,card_c)
& sort(tag_1_1,ta)
& sort(tag_1_1,oa)
& sort(tag_1_1,me)
& varia(c20,varia_c)
& refer(c20,refer_c)
& quant(c20,quant_c)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,etype_c)
& card(c20,card_c)
& sort(c20,ta)
& sort(c20,oa)
& sort(c20,me)
& varia(c19,varia_c)
& refer(c19,refer_c)
& quant(c19,quant_c)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,etype_c)
& card(c19,card_c)
& sort(c19,ta)
& sort(c19,oa)
& sort(c19,me)
& varia(c18,con)
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int0)
& card(c18,int1)
& sort(c18,t)
& sort(maputo_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(c12,varia_c)
& refer(c12,indet)
& quant(c12,one)
& gener(c12,sp)
& fact(c12,real)
& etype(c12,int0)
& card(c12,int1)
& sort(c12,na)
& varia(c11,con)
& refer(c11,det)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& etype(c11,int0)
& card(c11,int1)
& sort(c11,io)
& sort(c11,d)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1834) ).
fof(f10194,plain,
( varia(c47,varia_c)
& refer(c47,refer_c)
& quant(c47,quant_c)
& gener(c47,gener_c)
& fact(c47,real)
& card(c47,card_c)
& sort(c47,ent)
& card(c17,int7)
& sort(c17,nu)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& quant(monat_1_1,quant_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& card(monat_1_1,card_c)
& sort(monat_1_1,ta)
& sort(monat_1_1,oa)
& sort(monat_1_1,me)
& card(c16,int21)
& sort(c16,nu)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& quant(tag_1_1,quant_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& card(tag_1_1,card_c)
& sort(tag_1_1,ta)
& sort(tag_1_1,oa)
& sort(tag_1_1,me)
& varia(c20,varia_c)
& refer(c20,refer_c)
& quant(c20,quant_c)
& gener(c20,sp)
& fact(c20,real)
& card(c20,card_c)
& sort(c20,ta)
& sort(c20,oa)
& sort(c20,me)
& varia(c19,varia_c)
& refer(c19,refer_c)
& quant(c19,quant_c)
& gener(c19,sp)
& fact(c19,real)
& card(c19,card_c)
& sort(c19,ta)
& sort(c19,oa)
& sort(c19,me)
& varia(c18,con)
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& card(c18,int1)
& sort(c18,t)
& sort(maputo_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)
& 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)
& card(stadt__1_1,int1)
& sort(stadt__1_1,io)
& sort(stadt__1_1,d)
& varia(c12,varia_c)
& refer(c12,indet)
& quant(c12,one)
& gener(c12,sp)
& fact(c12,real)
& card(c12,int1)
& sort(c12,na)
& varia(c11,con)
& refer(c11,det)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& card(c11,int1)
& sort(c11,io)
& sort(c11,d)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10225,plain,
( varia(c47,varia_c)
& refer(c47,refer_c)
& quant(c47,quant_c)
& gener(c47,gener_c)
& fact(c47,real)
& card(c47,card_c)
& card(c17,int7)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& quant(monat_1_1,quant_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& card(monat_1_1,card_c)
& card(c16,int21)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& quant(tag_1_1,quant_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& card(tag_1_1,card_c)
& varia(c20,varia_c)
& refer(c20,refer_c)
& quant(c20,quant_c)
& gener(c20,sp)
& fact(c20,real)
& card(c20,card_c)
& varia(c19,varia_c)
& refer(c19,refer_c)
& quant(c19,quant_c)
& gener(c19,sp)
& fact(c19,real)
& card(c19,card_c)
& varia(c18,con)
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& card(c18,int1)
& 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)
& card(name_1_1,int1)
& 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)
& card(stadt__1_1,int1)
& varia(c12,varia_c)
& refer(c12,indet)
& quant(c12,one)
& gener(c12,sp)
& fact(c12,real)
& card(c12,int1)
& varia(c11,con)
& refer(c11,det)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& card(c11,int1)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10194]) ).
fof(f10228,plain,
( varia(c47,varia_c)
& refer(c47,refer_c)
& gener(c47,gener_c)
& fact(c47,real)
& card(c47,card_c)
& card(c17,int7)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& card(monat_1_1,card_c)
& card(c16,int21)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& card(tag_1_1,card_c)
& varia(c20,varia_c)
& refer(c20,refer_c)
& gener(c20,sp)
& fact(c20,real)
& card(c20,card_c)
& varia(c19,varia_c)
& refer(c19,refer_c)
& gener(c19,sp)
& fact(c19,real)
& card(c19,card_c)
& varia(c18,con)
& refer(c18,det)
& gener(c18,sp)
& fact(c18,real)
& card(c18,int1)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& card(name_1_1,int1)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& card(stadt__1_1,int1)
& varia(c12,varia_c)
& refer(c12,indet)
& gener(c12,sp)
& fact(c12,real)
& card(c12,int1)
& varia(c11,con)
& refer(c11,det)
& gener(c11,sp)
& fact(c11,real)
& card(c11,int1)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10225]) ).
fof(f10231,plain,
( varia(c47,varia_c)
& refer(c47,refer_c)
& gener(c47,gener_c)
& fact(c47,real)
& varia(monat_1_1,varia_c)
& refer(monat_1_1,refer_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& varia(tag_1_1,varia_c)
& refer(tag_1_1,refer_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& varia(c20,varia_c)
& refer(c20,refer_c)
& gener(c20,sp)
& fact(c20,real)
& varia(c19,varia_c)
& refer(c19,refer_c)
& gener(c19,sp)
& fact(c19,real)
& varia(c18,con)
& refer(c18,det)
& gener(c18,sp)
& fact(c18,real)
& varia(name_1_1,varia_c)
& refer(name_1_1,refer_c)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& varia(stadt__1_1,varia_c)
& refer(stadt__1_1,refer_c)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& varia(c12,varia_c)
& refer(c12,indet)
& gener(c12,sp)
& fact(c12,real)
& varia(c11,con)
& refer(c11,det)
& gener(c11,sp)
& fact(c11,real)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10228]) ).
fof(f10234,plain,
( varia(c47,varia_c)
& gener(c47,gener_c)
& fact(c47,real)
& varia(monat_1_1,varia_c)
& gener(monat_1_1,ge)
& fact(monat_1_1,real)
& varia(tag_1_1,varia_c)
& gener(tag_1_1,ge)
& fact(tag_1_1,real)
& varia(c20,varia_c)
& gener(c20,sp)
& fact(c20,real)
& varia(c19,varia_c)
& gener(c19,sp)
& fact(c19,real)
& varia(c18,con)
& gener(c18,sp)
& fact(c18,real)
& varia(name_1_1,varia_c)
& gener(name_1_1,ge)
& fact(name_1_1,real)
& varia(stadt__1_1,varia_c)
& gener(stadt__1_1,ge)
& fact(stadt__1_1,real)
& varia(c12,varia_c)
& gener(c12,sp)
& fact(c12,real)
& varia(c11,con)
& gener(c11,sp)
& fact(c11,real)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10231]) ).
fof(f10239,plain,
( varia(c47,varia_c)
& gener(c47,gener_c)
& varia(monat_1_1,varia_c)
& gener(monat_1_1,ge)
& varia(tag_1_1,varia_c)
& gener(tag_1_1,ge)
& varia(c20,varia_c)
& gener(c20,sp)
& varia(c19,varia_c)
& gener(c19,sp)
& varia(c18,con)
& gener(c18,sp)
& varia(name_1_1,varia_c)
& gener(name_1_1,ge)
& varia(stadt__1_1,varia_c)
& gener(stadt__1_1,ge)
& varia(c12,varia_c)
& gener(c12,sp)
& varia(c11,con)
& gener(c11,sp)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10234]) ).
fof(f10243,plain,
( gener(c47,gener_c)
& gener(monat_1_1,ge)
& gener(tag_1_1,ge)
& gener(c20,sp)
& gener(c19,sp)
& gener(c18,sp)
& gener(name_1_1,ge)
& gener(stadt__1_1,ge)
& gener(c12,sp)
& gener(c11,sp)
& tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10239]) ).
fof(f10247,plain,
( tupl(c47,c11,c18)
& val(c20,c17)
& sub(c20,monat_1_1)
& val(c19,c16)
& sub(c19,tag_1_1)
& attr(c18,c20)
& attr(c18,c19)
& val(c12,maputo_0)
& sub(c12,name_1_1)
& sub(c11,stadt__1_1)
& attr(c11,c12) ),
inference(pure_predicate_removal,[],[f10243]) ).
fof(f10250,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ subr(X3,rprs_0)
| ~ sub(X6,name_1_1)
| ~ sub(X4,X8)
| ~ obj(X7,X0)
| ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10292,plain,
! [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) ) ),
inference(ennf_transformation,[],[f162]) ).
fof(f10293,plain,
! [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) ) ),
inference(flattening,[],[f10292]) ).
fof(f10294,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| ? [X2] :
( subr(X2,sub_0)
& arg2(X2,X1)
& arg1(X2,X0) ) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10300,plain,
! [X0,X1,X2] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| ( subs(sK6(X0,X1,X2),bezeichnen_1_1)
& subr(sK7(X0,X1,X2),rprs_0)
& sub(sK8(X0,X1,X2),X2)
& obj(sK6(X0,X1,X2),X1)
& mcont(sK6(X0,X1,X2),sK7(X0,X1,X2))
& hsit(X0,sK6(X0,X1,X2))
& arg2(sK7(X0,X1,X2),sK8(X0,X1,X2))
& arg1(sK7(X0,X1,X2),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X3,sK6(X0,X1,X2)),skolemize(X4,sK7(X0,X1,X2)),skolemize(X5,sK8(X0,X1,X2))],[f10293]) ).
fof(f10301,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| ( subr(sK9(X0,X1),sub_0)
& arg2(sK9(X0,X1),X1)
& arg1(sK9(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0,X1))],[f10294]) ).
fof(f10302,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ subr(X3,rprs_0)
| ~ sub(X6,name_1_1)
| ~ sub(X4,X8)
| ~ obj(X7,X0)
| ~ attr(X5,X6)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0) ),
inference(cnf_transformation,[],[f10250]) ).
fof(f10311,plain,
sub(c12,name_1_1),
inference(cnf_transformation,[],[f10247]) ).
fof(f10312,plain,
sub(c11,stadt__1_1),
inference(cnf_transformation,[],[f10247]) ).
fof(f10313,plain,
attr(c11,c12),
inference(cnf_transformation,[],[f10247]) ).
fof(f10351,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(sK7(X0,X1,X2),rprs_0) ),
inference(cnf_transformation,[],[f10300]) ).
fof(f10352,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| sub(sK8(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f10300]) ).
fof(f10353,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| obj(sK6(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10300]) ).
fof(f10356,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| arg2(sK7(X0,X1,X2),sK8(X0,X1,X2)) ),
inference(cnf_transformation,[],[f10300]) ).
fof(f10357,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| arg1(sK7(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10300]) ).
fof(f10359,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| subr(sK9(X0,X1),sub_0) ),
inference(cnf_transformation,[],[f10301]) ).
fof(f10360,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg2(sK9(X0,X1),X1) ),
inference(cnf_transformation,[],[f10301]) ).
fof(f10361,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg1(sK9(X0,X1),X0) ),
inference(cnf_transformation,[],[f10301]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( ~ subr(X0,rprs_0)
| ~ sub(X6,name_1_1)
| ~ sub(X2,X8)
| ~ obj(X7,X1)
| ~ attr(X5,X6)
| ~ attr(X1,X4)
| ~ attr(X1,X3)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10302]) ).
tcf(c_50,plain,
attr(c11,c12),
inference(cnf_transformation,[],[f10313]) ).
tcf(c_51,plain,
sub(c11,stadt__1_1),
inference(cnf_transformation,[],[f10312]) ).
tcf(c_52,plain,
sub(c12,name_1_1),
inference(cnf_transformation,[],[f10311]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( arg1(sK7(X0,X1,X2),X1)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10357]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i] :
( arg2(sK7(X0,X1,X2),sK8(X0,X1,X2))
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10356]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( obj(sK6(X0,X1,X2),X1)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10353]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( sub(sK8(X0,X1,X2),X2)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10352]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( subr(sK7(X0,X1,X2),rprs_0)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1) ),
inference(cnf_transformation,[],[f10351]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( arg1(sK9(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10361]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] :
( arg2(sK9(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10360]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] :
( subr(sK9(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10359]) ).
tcf(c_703,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ attr(X1,X0)
| ~ sub(X0,name_1_1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_49]) ).
tcf(c_704,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ~ iPr_def_11
| ~ arg1(X0,X4)
| ~ arg2(X0,X1)
| ~ attr(X4,X6)
| ~ attr(X4,X5)
| ~ obj(X3,X4)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_49]) ).
tcf(c_705,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_49]) ).
tcf(c_708,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ sub(c12,name_1_1)
| ~ attr(X0,c12) ),
inference(instantiation,[status(thm)],[c_703]) ).
tcf(c_710,plain,
( subr(sK9(c11,stadt__1_1),sub_0)
| ~ sub(c11,stadt__1_1) ),
inference(instantiation,[status(thm)],[c_108]) ).
tcf(c_714,plain,
( arg1(sK9(c11,stadt__1_1),c11)
| ~ sub(c11,stadt__1_1) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_718,plain,
( arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ sub(c11,stadt__1_1) ),
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_747,plain,
( ~ iPr_def_10
| ~ sub(c12,name_1_1)
| ~ attr(c11,c12) ),
inference(instantiation,[status(thm)],[c_708]) ).
tcf(c_748,plain,
! [X0: $i,X1: $i] :
( arg2(sK7(sK9(c11,stadt__1_1),X0,X1),sK8(sK9(c11,stadt__1_1),X0,X1))
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),X1)
| ~ arg1(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i] :
( sub(sK8(sK9(c11,stadt__1_1),X0,X1),X1)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),X1)
| ~ arg1(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_750,plain,
! [X0: $i,X1: $i] :
( obj(sK6(sK9(c11,stadt__1_1),X0,X1),X0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),X1)
| ~ arg1(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i] :
( arg1(sK7(sK9(c11,stadt__1_1),X0,X1),X0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),X1)
| ~ arg1(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_753,plain,
! [X0: $i,X1: $i] :
( subr(sK7(sK9(c11,stadt__1_1),X0,X1),rprs_0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),X1)
| ~ arg1(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_816,plain,
! [X0: $i] :
( subr(sK7(sK9(c11,stadt__1_1),c11,X0),rprs_0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg1(sK9(c11,stadt__1_1),c11)
| ~ arg2(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_753]) ).
tcf(c_830,plain,
! [X0: $i] :
( sub(sK8(sK9(c11,stadt__1_1),c11,X0),X0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg1(sK9(c11,stadt__1_1),c11)
| ~ arg2(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_749]) ).
tcf(c_832,plain,
! [X0: $i] :
( obj(sK6(sK9(c11,stadt__1_1),c11,X0),c11)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg1(sK9(c11,stadt__1_1),c11)
| ~ arg2(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_750]) ).
tcf(c_834,plain,
! [X0: $i] :
( arg1(sK7(sK9(c11,stadt__1_1),c11,X0),c11)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg1(sK9(c11,stadt__1_1),c11)
| ~ arg2(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_751]) ).
tcf(c_854,plain,
! [X0: $i] :
( arg2(sK7(sK9(c11,stadt__1_1),c11,X0),sK8(sK9(c11,stadt__1_1),c11,X0))
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg1(sK9(c11,stadt__1_1),c11)
| ~ arg2(sK9(c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_865,plain,
( subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ arg1(sK9(c11,stadt__1_1),c11) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_872,plain,
( obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ arg1(sK9(c11,stadt__1_1),c11) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_873,plain,
( arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ arg1(sK9(c11,stadt__1_1),c11) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_880,plain,
( sub(sK8(sK9(c11,stadt__1_1),c11,stadt__1_1),stadt__1_1)
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ arg1(sK9(c11,stadt__1_1),c11) ),
inference(instantiation,[status(thm)],[c_830]) ).
tcf(c_884,plain,
( arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),sK8(sK9(c11,stadt__1_1),c11,stadt__1_1))
| ~ subr(sK9(c11,stadt__1_1),sub_0)
| ~ arg2(sK9(c11,stadt__1_1),stadt__1_1)
| ~ arg1(sK9(c11,stadt__1_1),c11) ),
inference(instantiation,[status(thm)],[c_854]) ).
tcf(c_896,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ iPr_def_11
| ~ sub(X1,X5)
| ~ obj(X4,X0)
| ~ attr(X0,X3)
| ~ attr(X0,X2)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X1)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_704]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ iPr_def_11
| ~ obj(X4,c11)
| ~ attr(c11,X3)
| ~ attr(c11,X2)
| ~ sub(X0,X1)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_1555,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_11
| ~ attr(c11,X3)
| ~ attr(c11,X2)
| ~ sub(X0,X1)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_948]) ).
tcf(c_1811,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_11
| ~ attr(c11,c12)
| ~ attr(c11,X2)
| ~ sub(X0,X1)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_1555]) ).
tcf(c_2124,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ attr(c11,c12)
| ~ sub(X0,X1)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),X0) ),
inference(instantiation,[status(thm)],[c_1811]) ).
tcf(c_2488,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ attr(c11,c12)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ sub(sK8(sK9(c11,stadt__1_1),c11,stadt__1_1),X0)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),sK8(sK9(c11,stadt__1_1),c11,stadt__1_1)) ),
inference(instantiation,[status(thm)],[c_2124]) ).
tcf(c_4224,plain,
( ~ iPr_def_11
| ~ attr(c11,c12)
| ~ subr(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),rprs_0)
| ~ sub(sK8(sK9(c11,stadt__1_1),c11,stadt__1_1),stadt__1_1)
| ~ obj(sK6(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg1(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),c11)
| ~ arg2(sK7(sK9(c11,stadt__1_1),c11,stadt__1_1),sK8(sK9(c11,stadt__1_1),c11,stadt__1_1)) ),
inference(instantiation,[status(thm)],[c_2488]) ).
tcf(c_4225,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4224,c_884,c_880,c_873,c_872,c_865,c_747,c_718,c_714,c_710,c_705,c_50,c_51,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+30 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.56 % Computer : n002.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Fri Sep 25 09:48:21 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.57 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.60 Running first-order theorem proving
% 0.09/0.60 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.61
% 0.09/0.61 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.61
% 0.09/0.62 % Detected problem language: tptp
% 0.09/0.63 % Proving...
% 1.68/1.39 % SZS status Started for theBenchmark.p
% 1.68/1.39 % SZS status Theorem for theBenchmark.p
% 1.68/1.39
% 1.68/1.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.68/1.39
% 1.68/1.39 % ------ iProver source info
% 1.68/1.39
% 1.68/1.39 % git: date: 2026-07-19 20:42:38 +0200
% 1.68/1.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.68/1.39 % git: non_committed_changes: false
% 1.68/1.39
% 1.68/1.39 % ------ Parsing...
% 1.68/1.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.68/1.39
% 1.68/1.39 % ------ Preprocessing... sf_s rm: 24 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 1.68/1.39
% 1.68/1.39 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e
% 1.68/1.39 % ------ Proving...
% 1.68/1.39 % ------ Problem Properties
% 1.68/1.39
% 1.68/1.39 %
% 1.68/1.39 % clauses 38
% 1.68/1.39 % conjectures 3
% 1.68/1.39 % EPR 15
% 1.68/1.39 % Horn 37
% 1.68/1.39 % unary 9
% 1.68/1.39 % binary 5
% 1.68/1.39 % lits 110
% 1.68/1.39 % lits eq 0
% 1.68/1.39 % fd_pure 0
% 1.68/1.39 % fd_pseudo 0
% 1.68/1.39 % fd_cond 0
% 1.68/1.39 % fd_pseudo_cond 0
% 1.68/1.39 % AC symbols 0
% 1.68/1.39
% 1.68/1.39 % ------ Schedule dynamic 5 is on
% 1.68/1.39
% 1.68/1.39 % ------ no equalities: superposition off
% 1.68/1.39
% 1.68/1.39 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.68/1.39
% 1.68/1.39
% 1.68/1.39 % ------
% 1.68/1.39 % Current options:
% 1.68/1.39 % ------
% 1.68/1.39
% 1.68/1.39
% 1.68/1.39 %
% 1.68/1.39
% 1.68/1.39 % ------ Proving...
% 1.68/1.39 %
% 1.68/1.39
% 1.68/1.39 % SZS status Theorem for theBenchmark.p
% 1.68/1.39
% 1.68/1.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.68/1.39
%------------------------------------------------------------------------------