%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR114+10 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 : Sun Sep 27 07:07:35 AM UTC 2026
% Result : Theorem 11.35s 2.09s
% Output : CNFRefutation 11.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 62 ( 14 unt; 0 def)
% Number of atoms : 633 ( 0 equ)
% Maximal formula atoms : 393 ( 10 avg)
% Number of connectives : 719 ( 148 ~; 131 |; 437 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 393 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 22 usr; 1 prp; 0-14 aty)
% Number of functors : 87 ( 87 usr; 82 con; 0-3 aty)
% Number of variables : 164 ( 13 sgn 45 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(in_state__state_adjective,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( val(X3,X4)
& sub(X3,name_1_1)
& sub(X2,land_1_1)
& state_adjective_state_binding(X1,X4)
& loc(X0,X5)
& attr(X2,X3)
& in(X5,X2) )
=> prop(X0,X1) ),
file('theBenchmark.p',in_state__state_adjective) ).
fof(loc__stehen_1_1_loc,axiom,
! [X0,X1] :
( loc(X0,X1)
=> ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) ) ),
file('theBenchmark.p',loc__stehen_1_1_loc) ).
fof(ave07_era5_synth_qa07_004_mira_news_613,axiom,
( varia(agentur_1_1,varia_c)
& refer(agentur_1_1,refer_c)
& quant(agentur_1_1,one)
& gener(agentur_1_1,ge)
& fact(agentur_1_1,real)
& etype(agentur_1_1,int0)
& card(agentur_1_1,int1)
& sort(agentur_1_1,io)
& sort(agentur_1_1,d)
& varia(nachricht_1_1,varia_c)
& refer(nachricht_1_1,refer_c)
& quant(nachricht_1_1,one)
& gener(nachricht_1_1,ge)
& fact(nachricht_1_1,real)
& etype(nachricht_1_1,int0)
& card(nachricht_1_1,int1)
& sort(nachricht_1_1,io)
& sort(nachricht_1_1,d)
& sort(nachricht_1_1,ad)
& varia(auff__374hrung_1_1,varia_c)
& refer(auff__374hrung_1_1,refer_c)
& quant(auff__374hrung_1_1,one)
& gener(auff__374hrung_1_1,ge)
& fact(auff__374hrung_1_1,real)
& etype(auff__374hrung_1_1,int0)
& card(auff__374hrung_1_1,int1)
& sort(auff__374hrung_1_1,ad)
& varia(ur_1_1,varia_c)
& refer(ur_1_1,refer_c)
& quant(ur_1_1,one)
& gener(ur_1_1,ge)
& fact(ur_1_1,real)
& etype(ur_1_1,int0)
& card(ur_1_1,int1)
& sort(ur_1_1,o)
& varia(c41050,varia_c)
& refer(c41050,refer_c)
& quant(c41050,quant_c)
& gener(c41050,gener_c)
& fact(c41050,real)
& etype(c41050,etype_c)
& card(c41050,card_c)
& sort(c41050,ent)
& sort(sta_0,fe)
& varia(nachrichtenagentur_1_1,varia_c)
& refer(nachrichtenagentur_1_1,refer_c)
& quant(nachrichtenagentur_1_1,one)
& gener(nachrichtenagentur_1_1,ge)
& fact(nachrichtenagentur_1_1,real)
& etype(nachrichtenagentur_1_1,int0)
& card(nachrichtenagentur_1_1,int1)
& sort(nachrichtenagentur_1_1,io)
& sort(nachrichtenagentur_1_1,d)
& varia(c41011,varia_c)
& refer(c41011,indet)
& quant(c41011,one)
& gener(c41011,sp)
& fact(c41011,real)
& etype(c41011,int0)
& card(c41011,int1)
& sort(c41011,na)
& varia(c41010,con)
& refer(c41010,det)
& quant(c41010,one)
& gener(c41010,sp)
& fact(c41010,real)
& etype(c41010,int0)
& card(c41010,int1)
& sort(c41010,io)
& sort(c41010,d)
& varia(debuet_1_1,varia_c)
& refer(debuet_1_1,refer_c)
& quant(debuet_1_1,one)
& gener(debuet_1_1,ge)
& fact(debuet_1_1,real)
& etype(debuet_1_1,int0)
& card(debuet_1_1,int1)
& sort(debuet_1_1,ad)
& varia(c40979,con)
& refer(c40979,det)
& quant(c40979,one)
& gener(c40979,sp)
& fact(c40979,real)
& etype(c40979,int0)
& card(c40979,int1)
& sort(c40979,ad)
& sort(triest_0,fe)
& varia(c40977,varia_c)
& refer(c40977,indet)
& quant(c40977,one)
& gener(c40977,sp)
& fact(c40977,real)
& etype(c40977,int0)
& card(c40977,int1)
& sort(c40977,na)
& varia(c40976,con)
& refer(c40976,det)
& quant(c40976,one)
& gener(c40976,sp)
& fact(c40976,real)
& etype(c40976,int0)
& card(c40976,int1)
& sort(c40976,io)
& sort(c40976,d)
& varia(c40970,con)
& refer(c40970,det)
& quant(c40970,one)
& gener(c40970,sp)
& fact(c40970,real)
& etype(c40970,int0)
& card(c40970,int1)
& sort(c40970,io)
& sort(c40970,d)
& varia(herstellung_1_1,varia_c)
& refer(herstellung_1_1,refer_c)
& quant(herstellung_1_1,one)
& gener(herstellung_1_1,ge)
& fact(herstellung_1_1,real)
& etype(herstellung_1_1,int0)
& card(herstellung_1_1,int1)
& sort(herstellung_1_1,ad)
& varia(c40962,varia_c)
& refer(c40962,indet)
& quant(c40962,one)
& gener(c40962,sp)
& fact(c40962,real)
& etype(c40962,int0)
& card(c40962,int1)
& sort(c40962,ad)
& varia(veroli_1_1,varia_c)
& refer(veroli_1_1,refer_c)
& quant(veroli_1_1,one)
& gener(veroli_1_1,ge)
& fact(veroli_1_1,real)
& etype(veroli_1_1,int0)
& card(veroli_1_1,int1)
& sort(veroli_1_1,o)
& varia(c40955,varia_c)
& refer(c40955,indet)
& quant(c40955,mult)
& gener(c40955,gener_c)
& fact(c40955,real)
& etype(c40955,int1)
& card(c40955,cons(x_constant,cons(int1,nil)))
& sort(c40955,o)
& sort(italienisch__1_1,nq)
& varia(c40954,con)
& refer(c40954,det)
& quant(c40954,one)
& gener(c40954,sp)
& fact(c40954,real)
& etype(c40954,int0)
& card(c40954,int1)
& sort(c40954,io)
& sort(c40954,d)
& sort(dionisya_0,fe)
& varia(schauspielhaus_1_1,varia_c)
& refer(schauspielhaus_1_1,refer_c)
& quant(schauspielhaus_1_1,one)
& gener(schauspielhaus_1_1,ge)
& fact(schauspielhaus_1_1,real)
& etype(schauspielhaus_1_1,int0)
& card(schauspielhaus_1_1,int1)
& sort(schauspielhaus_1_1,io)
& sort(schauspielhaus_1_1,d)
& sort(zeitgen__366ssisch_1_1,nq)
& varia(c40947,varia_c)
& refer(c40947,det)
& quant(c40947,one)
& gener(c40947,sp)
& fact(c40947,real)
& etype(c40947,int0)
& card(c40947,int1)
& sort(c40947,na)
& varia(c40941,varia_c)
& refer(c40941,det)
& quant(c40941,one)
& gener(c40941,sp)
& fact(c40941,real)
& etype(c40941,int0)
& card(c40941,int1)
& sort(c40941,io)
& sort(c40941,d)
& varia(festival_1_1,varia_c)
& refer(festival_1_1,refer_c)
& quant(festival_1_1,one)
& gener(festival_1_1,ge)
& fact(festival_1_1,real)
& etype(festival_1_1,int0)
& card(festival_1_1,int1)
& sort(festival_1_1,ad)
& varia(c40936,con)
& refer(c40936,det)
& quant(c40936,one)
& gener(c40936,sp)
& fact(c40936,real)
& etype(c40936,int0)
& card(c40936,int1)
& sort(c40936,ad)
& sort(jancar_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(drago_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(romanautor_1_1,varia_c)
& refer(romanautor_1_1,refer_c)
& quant(romanautor_1_1,one)
& gener(romanautor_1_1,ge)
& fact(romanautor_1_1,real)
& etype(romanautor_1_1,int0)
& card(romanautor_1_1,int1)
& sort(romanautor_1_1,d)
& varia(c40905,varia_c)
& refer(c40905,det)
& quant(c40905,one)
& gener(c40905,sp)
& fact(c40905,real)
& etype(c40905,int0)
& card(c40905,int1)
& sort(c40905,na)
& varia(c40904,varia_c)
& refer(c40904,indet)
& quant(c40904,one)
& gener(c40904,sp)
& fact(c40904,real)
& etype(c40904,int0)
& card(c40904,int1)
& sort(c40904,na)
& varia(c40903,varia_c)
& refer(c40903,det)
& quant(c40903,one)
& gener(c40903,sp)
& fact(c40903,real)
& etype(c40903,int0)
& card(c40903,int1)
& sort(c40903,d)
& varia(dramatiker_1_1,varia_c)
& refer(dramatiker_1_1,refer_c)
& quant(dramatiker_1_1,one)
& gener(dramatiker_1_1,ge)
& fact(dramatiker_1_1,real)
& etype(dramatiker_1_1,int0)
& card(dramatiker_1_1,int1)
& sort(dramatiker_1_1,d)
& sort(slowenisch__1_1,nq)
& varia(c40895,con)
& refer(c40895,det)
& quant(c40895,one)
& gener(c40895,sp)
& fact(c40895,real)
& etype(c40895,int0)
& card(c40895,int1)
& sort(c40895,d)
& varia(c40893,varia_c)
& refer(c40893,refer_c)
& quant(c40893,quant_c)
& gener(c40893,gener_c)
& fact(c40893,real)
& etype(c40893,int2)
& etype(c40893,int1)
& card(c40893,card_c)
& sort(c40893,o)
& sort(neo_1_1,nq)
& varia(st__374ck_1_1,varia_c)
& refer(st__374ck_1_1,refer_c)
& quant(st__374ck_1_1,one)
& gener(st__374ck_1_1,ge)
& fact(st__374ck_1_1,real)
& etype(st__374ck_1_1,int0)
& card(st__374ck_1_1,int1)
& sort(st__374ck_1_1,d)
& sort(c40892,tq)
& varia(c40889,con)
& refer(c40889,det)
& quant(c40889,one)
& gener(c40889,sp)
& fact(c40889,real)
& etype(c40889,int0)
& card(c40889,int1)
& sort(c40889,d)
& varia(titel_1_1,varia_c)
& refer(titel_1_1,refer_c)
& quant(titel_1_1,one)
& gener(titel_1_1,ge)
& fact(titel_1_1,real)
& etype(titel_1_1,int0)
& card(titel_1_1,int1)
& sort(titel_1_1,io)
& sort(titel_1_1,d)
& varia(c40883,con)
& refer(c40883,det)
& quant(c40883,one)
& gener(c40883,sp)
& fact(c40883,real)
& etype(c40883,int0)
& card(c40883,int1)
& sort(c40883,io)
& sort(c40883,d)
& sort(hallstatt_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(c40863,varia_c)
& refer(c40863,indet)
& quant(c40863,one)
& gener(c40863,sp)
& fact(c40863,real)
& etype(c40863,int0)
& card(c40863,int1)
& sort(c40863,na)
& varia(c40862,con)
& refer(c40862,det)
& quant(c40862,one)
& gener(c40862,sp)
& fact(c40862,real)
& etype(c40862,int0)
& card(c40862,int1)
& sort(c40862,io)
& sort(c40862,d)
& sub(nachrichtenagentur_1_1,agentur_1_1)
& assoc(nachrichtenagentur_1_1,nachricht_1_1)
& subs(debuet_1_1,auff__374hrung_1_1)
& assoc(debuet_1_1,ur_1_1)
& tupl_p14(c41050,c40862,c40883,c40892,c40903,c40862,c40936,c40941,c40954,c40955,c40962,c40976,c40979,c41010)
& val(c41011,sta_0)
& sub(c41011,name_1_1)
& sub(c41010,nachrichtenagentur_1_1)
& prop(c41010,slowenisch__1_1)
& attr(c41010,c41011)
& subs(c40979,debuet_1_1)
& val(c40977,triest_0)
& sub(c40977,name_1_1)
& sub(c40976,stadt__1_1)
& attr(c40976,c40977)
& sub(c40970,schauspielhaus_1_1)
& prop(c40970,slowenisch__1_1)
& attch(c40970,c40962)
& subs(c40962,herstellung_1_1)
& pred(c40955,veroli_1_1)
& sub(c40954,stadt__1_1)
& prop(c40954,italienisch__1_1)
& val(c40947,dionisya_0)
& sub(c40947,name_1_1)
& sub(c40941,schauspielhaus_1_1)
& prop(c40941,zeitgen__366ssisch_1_1)
& attr(c40941,c40947)
& subs(c40936,festival_1_1)
& val(c40905,jancar_0)
& sub(c40905,familiename_1_1)
& val(c40904,drago_0)
& sub(c40904,eigenname_1_1)
& sub(c40903,romanautor_1_1)
& attr(c40903,c40905)
& attr(c40903,c40904)
& sub(c40895,dramatiker_1_1)
& prop(c40895,slowenisch__1_1)
& attch(c40895,c40889)
& supl(c40892,neo_1_1,c40893)
& sub(c40889,st__374ck_1_1)
& prop(c40889,c40892)
& attch(c40889,c40883)
& sub(c40883,titel_1_1)
& val(c40863,hallstatt_0)
& sub(c40863,name_1_1)
& sub(c40862,stadt__1_1)
& attr(c40862,c40863) ),
file('theBenchmark.p',ave07_era5_synth_qa07_004_mira_news_613) ).
fof(state_adjective__in_state,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('theBenchmark.p',state_adjective__in_state) ).
fof(synth_qa07_004_mira_news_613,conjecture,
? [X0,X1,X2,X3,X4] :
( subs(X4,stehen_1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
file('theBenchmark.p',synth_qa07_004_mira_news_613) ).
fof(synth_qa07_004_mira_news_613_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( subs(X4,stehen_1_1)
& sub(X1,name_1_1)
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
inference(assume_negation,[status(cth)],[synth_qa07_004_mira_news_613]) ).
fof(nnf_60,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(fof_nnf,[status(thm)],[state_adjective__in_state]) ).
fof(sk_state_adjective__in_state_sk,plain,
! [X0,X1,X2] :
( ( val(sK2(X0,X1,X2),X2)
& sub(sK2(X0,X1,X2),name_1_1)
& sub(sK1(X0,X1,X2),land_1_1)
& loc(X0,sK0(X0,X1,X2))
& attr(sK1(X0,X1,X2),sK2(X0,X1,X2))
& in(sK0(X0,X1,X2),sK1(X0,X1,X2)) )
| ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X3,sK1(X0,X1,X2)),skolemize(X4,sK2(X0,X1,X2)),skolemize(X5,sK0(X0,X1,X2))],[nnf_60]) ).
fof(sk_state_adjective__in_state,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( val(sK2(VAR_0,VAR_1,VAR_2),VAR_2)
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sub(sK2(VAR_0,VAR_1,VAR_2),name_1_1)
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( sub(sK1(VAR_0,VAR_1,VAR_2),land_1_1)
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( loc(VAR_0,sK0(VAR_0,VAR_1,VAR_2))
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( attr(sK1(VAR_0,VAR_1,VAR_2),sK2(VAR_0,VAR_1,VAR_2))
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK0(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2))
| ~ state_adjective_state_binding(VAR_1,VAR_2)
| ~ prop(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_state_adjective__in_state_sk]) ).
cnf(c_108,plain,
( in(sK0(A,B,C),sK1(A,B,C))
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
cnf(c_109,plain,
( attr(sK1(A,B,C),sK2(A,B,C))
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
cnf(c_110,plain,
( loc(A,sK0(A,B,C))
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
cnf(c_111,plain,
( sub(sK1(A,B,C),land_1_1)
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
cnf(c_112,plain,
( sub(sK2(A,B,C),name_1_1)
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
cnf(c_113,plain,
( val(sK2(A,B,C),C)
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B) ),
inference(split_conjunct,[status(thm)],[sk_state_adjective__in_state]) ).
fof(fact_8886,axiom,
state_adjective_state_binding(italienisch__1_1,italien_0),
file('theBenchmark.p',fact_8886) ).
cnf(c_152,plain,
state_adjective_state_binding(italienisch__1_1,italien_0),
inference(clausify,[status(thm)],[fact_8886]) ).
cnf(c_222,plain,
( prop(D,E)
| ~ val(C,F)
| ~ sub(C,name_1_1)
| ~ sub(B,land_1_1)
| ~ state_adjective_state_binding(E,F)
| ~ loc(D,A)
| ~ attr(B,C)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[in_state__state_adjective]) ).
fof(nnf_42,plain,
! [X0,X1] :
( ? [X2] :
( subs(X2,stehen_1_1)
& scar(X2,X0)
& loc(X2,X1) )
| ~ loc(X0,X1) ),
inference(fof_nnf,[status(thm)],[loc__stehen_1_1_loc]) ).
fof(sk_loc__stehen_1_1_loc_sk,plain,
! [X0,X1] :
( ( subs(sK3(X0,X1),stehen_1_1)
& scar(sK3(X0,X1),X0)
& loc(sK3(X0,X1),X1) )
| ~ loc(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[nnf_42]) ).
fof(sk_loc__stehen_1_1_loc,plain,
( ! [VAR_0,VAR_1] :
( subs(sK3(VAR_0,VAR_1),stehen_1_1)
| ~ loc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( scar(sK3(VAR_0,VAR_1),VAR_0)
| ~ loc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( loc(sK3(VAR_0,VAR_1),VAR_1)
| ~ loc(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_loc__stehen_1_1_loc_sk]) ).
cnf(c_242,plain,
( loc(sK3(A,B),B)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_243,plain,
( scar(sK3(A,B),A)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_244,plain,
( subs(sK3(A,B),stehen_1_1)
| ~ loc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_loc__stehen_1_1_loc]) ).
cnf(c_278,plain,
prop(c40954,italienisch__1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_004_mira_news_613]) ).
cnf(c_646,negated_conjecture,
( ~ subs(D,stehen_1_1)
| ~ sub(C,name_1_1)
| ~ scar(D,E)
| ~ loc(D,A)
| ~ attr(B,C)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_004_mira_news_613_neg]) ).
cnf(c_648,plain,
( ~ state_adjective_state_binding(B,C)
| ~ prop(A,B)
| ~ subs(A,stehen_1_1)
| ~ sub(E,name_1_1)
| ~ scar(A,F)
| ~ attr(D,E)
| ~ in(sK0(A,B,C),D) ),
inference(resolve,[status(thm)],[c_646,c_110]) ).
cnf(c_7765,plain,
( ~ state_adjective_state_binding(B,C)
| ~ prop(A,B)
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B)
| ~ subs(A,stehen_1_1)
| ~ sub(D,name_1_1)
| ~ scar(A,E)
| ~ attr(sK1(A,B,C),D) ),
inference(resolve,[status(thm)],[c_648,c_108]) ).
cnf(c_7766,plain,
( ~ state_adjective_state_binding(B,C)
| ~ state_adjective_state_binding(B,C)
| ~ prop(A,B)
| ~ subs(A,stehen_1_1)
| ~ sub(D,name_1_1)
| ~ scar(A,E)
| ~ attr(sK1(A,B,C),D) ),
inference(copy,[status(thm)],[c_7765]) ).
cnf(c_651,plain,
( ~ state_adjective_state_binding(B,C)
| ~ prop(A,B)
| ~ subs(A,stehen_1_1)
| ~ sub(D,name_1_1)
| ~ scar(A,E)
| ~ attr(sK1(A,B,C),D) ),
inference(copy,[status(thm)],[c_7766]) ).
cnf(c_7767,plain,
( ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ sub(sK2(A,C,D),name_1_1)
| ~ scar(A,B) ),
inference(resolve,[status(thm)],[c_651,c_109]) ).
cnf(c_7768,plain,
( ~ state_adjective_state_binding(C,D)
| ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ sub(sK2(A,C,D),name_1_1)
| ~ scar(A,B) ),
inference(copy,[status(thm)],[c_7767]) ).
cnf(c_654,plain,
( ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ sub(sK2(A,C,D),name_1_1)
| ~ scar(A,B) ),
inference(copy,[status(thm)],[c_7768]) ).
cnf(c_7769,plain,
( ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ scar(A,B) ),
inference(resolve,[status(thm)],[c_654,c_112]) ).
cnf(c_7770,plain,
( ~ state_adjective_state_binding(C,D)
| ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ scar(A,B) ),
inference(copy,[status(thm)],[c_7769]) ).
cnf(c_658,plain,
( ~ state_adjective_state_binding(C,D)
| ~ prop(A,C)
| ~ subs(A,stehen_1_1)
| ~ scar(A,B) ),
inference(copy,[status(thm)],[c_7770]) ).
cnf(c_672,plain,
( ~ prop(A,italienisch__1_1)
| ~ subs(A,stehen_1_1)
| ~ scar(A,B) ),
inference(resolve,[status(thm)],[c_658,c_152]) ).
cnf(c_7771,plain,
( val(sK2(c40954,italienisch__1_1,A),A)
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_113,c_278]) ).
cnf(c_835,plain,
val(sK2(c40954,italienisch__1_1,italien_0),italien_0),
inference(resolve,[status(thm)],[c_7771,c_152]) ).
cnf(c_7772,plain,
( sub(sK2(c40954,italienisch__1_1,A),name_1_1)
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_112,c_278]) ).
cnf(c_836,plain,
sub(sK2(c40954,italienisch__1_1,italien_0),name_1_1),
inference(resolve,[status(thm)],[c_7772,c_152]) ).
cnf(c_7773,plain,
( sub(sK1(c40954,italienisch__1_1,A),land_1_1)
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_111,c_278]) ).
cnf(c_837,plain,
sub(sK1(c40954,italienisch__1_1,italien_0),land_1_1),
inference(resolve,[status(thm)],[c_7773,c_152]) ).
cnf(c_7774,plain,
( loc(c40954,sK0(c40954,italienisch__1_1,A))
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_110,c_278]) ).
cnf(c_838,plain,
loc(c40954,sK0(c40954,italienisch__1_1,italien_0)),
inference(resolve,[status(thm)],[c_7774,c_152]) ).
cnf(c_7775,plain,
( attr(sK1(c40954,italienisch__1_1,A),sK2(c40954,italienisch__1_1,A))
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_109,c_278]) ).
cnf(c_839,plain,
attr(sK1(c40954,italienisch__1_1,italien_0),sK2(c40954,italienisch__1_1,italien_0)),
inference(resolve,[status(thm)],[c_7775,c_152]) ).
cnf(c_7776,plain,
( in(sK0(c40954,italienisch__1_1,A),sK1(c40954,italienisch__1_1,A))
| ~ state_adjective_state_binding(italienisch__1_1,A) ),
inference(resolve,[status(thm)],[c_108,c_278]) ).
cnf(c_840,plain,
in(sK0(c40954,italienisch__1_1,italien_0),sK1(c40954,italienisch__1_1,italien_0)),
inference(resolve,[status(thm)],[c_7776,c_152]) ).
cnf(c_2088,plain,
( ~ prop(sK3(A,B),italienisch__1_1)
| ~ subs(sK3(A,B),stehen_1_1)
| ~ loc(A,B) ),
inference(resolve,[status(thm)],[c_243,c_672]) ).
cnf(c_7093,plain,
subs(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),stehen_1_1),
inference(resolve,[status(thm)],[c_244,c_838]) ).
cnf(c_7095,plain,
loc(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),sK0(c40954,italienisch__1_1,italien_0)),
inference(resolve,[status(thm)],[c_242,c_838]) ).
cnf(c_7777,plain,
( ~ prop(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),italienisch__1_1)
| ~ subs(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),stehen_1_1) ),
inference(resolve,[status(thm)],[c_2088,c_838]) ).
cnf(c_7742,plain,
~ prop(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),italienisch__1_1),
inference(resolve,[status(thm)],[c_7093,c_7777]) ).
cnf(c_7778,plain,
( prop(B,C)
| ~ val(A,D)
| ~ sub(A,name_1_1)
| ~ sub(sK1(c40954,italienisch__1_1,italien_0),land_1_1)
| ~ state_adjective_state_binding(C,D)
| ~ loc(B,sK0(c40954,italienisch__1_1,italien_0))
| ~ attr(sK1(c40954,italienisch__1_1,italien_0),A) ),
inference(resolve,[status(thm)],[c_222,c_840]) ).
cnf(c_7779,plain,
( prop(A,B)
| ~ val(sK2(c40954,italienisch__1_1,italien_0),C)
| ~ sub(sK2(c40954,italienisch__1_1,italien_0),name_1_1)
| ~ sub(sK1(c40954,italienisch__1_1,italien_0),land_1_1)
| ~ state_adjective_state_binding(B,C)
| ~ loc(A,sK0(c40954,italienisch__1_1,italien_0)) ),
inference(resolve,[status(thm)],[c_7778,c_839]) ).
cnf(c_7780,plain,
( prop(A,italienisch__1_1)
| ~ val(sK2(c40954,italienisch__1_1,italien_0),italien_0)
| ~ sub(sK2(c40954,italienisch__1_1,italien_0),name_1_1)
| ~ sub(sK1(c40954,italienisch__1_1,italien_0),land_1_1)
| ~ loc(A,sK0(c40954,italienisch__1_1,italien_0)) ),
inference(resolve,[status(thm)],[c_7779,c_152]) ).
cnf(c_7781,plain,
( prop(A,italienisch__1_1)
| ~ val(sK2(c40954,italienisch__1_1,italien_0),italien_0)
| ~ sub(sK2(c40954,italienisch__1_1,italien_0),name_1_1)
| ~ loc(A,sK0(c40954,italienisch__1_1,italien_0)) ),
inference(resolve,[status(thm)],[c_7780,c_837]) ).
cnf(c_7782,plain,
( prop(A,italienisch__1_1)
| ~ val(sK2(c40954,italienisch__1_1,italien_0),italien_0)
| ~ loc(A,sK0(c40954,italienisch__1_1,italien_0)) ),
inference(resolve,[status(thm)],[c_7781,c_836]) ).
cnf(c_7783,plain,
( prop(A,italienisch__1_1)
| ~ loc(A,sK0(c40954,italienisch__1_1,italien_0)) ),
inference(resolve,[status(thm)],[c_7782,c_835]) ).
cnf(c_7784,plain,
~ loc(sK3(c40954,sK0(c40954,italienisch__1_1,italien_0)),sK0(c40954,italienisch__1_1,italien_0)),
inference(resolve,[status(thm)],[c_7783,c_7742]) ).
cnf(c_7764,plain,
$false,
inference(resolve,[status(thm)],[c_7095,c_7784]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+10 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 27 01:04:40 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 428944 was started by sandbox2 on n010,
% 0.12/0.36 % Sun Sep 27 01:04:40 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 11.35/2.09
% 11.35/2.09 % SInE (scan): 82 to sos (tol 1.5x), 29 to usable (tol 2.0x), 10077 zapped, of 10188 axioms (depth 3).
% 11.35/2.09
% 11.35/2.09 % From the command line: assign(max_seconds, 300).
% 11.35/2.09
% 11.35/2.09 % given #500 (F,wt=14): 2495 -subs(herstellung_1_1,stehen_1_1) | -scar(c40962,A) | -state_adjective_state_binding(national__1_1,B) | -sub(c40970,land_1_1). [resolve(920,a,281,a)].
% 11.35/2.09
% 11.35/2.09 % given #1000 (T,wt=5): 1369 has_etype_leq(titel_1_1,int0). [ur(172,a,347,a)].
% 11.35/2.09
% 11.35/2.09 % SZS status Theorem for theBenchmark
% 11.35/2.09
% 11.35/2.09 % Proof 1 at 1.33 (+ 0.25) seconds.
% 11.35/2.09 % Length of proof is 34.
% 11.35/2.09 % Level of proof is 9.
% 11.35/2.09 % Maximum clause weight is 28.000.
% 11.35/2.09 % Given clauses 1467.
% 11.35/2.09
% 11.35/2.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------