%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR115+50 : 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 : n008.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:44 AM UTC 2026
% Result : Theorem 0.24s 0.60s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 25 ( 11 unt; 0 def)
% Number of atoms : 246 ( 0 equ)
% Maximal formula atoms : 180 ( 9 avg)
% Number of connectives : 254 ( 33 ~; 26 |; 194 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 180 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-5 aty)
% Number of functors : 47 ( 47 usr; 46 con; 0-3 aty)
% Number of variables : 50 ( 15 sgn 15 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(chea_subs_abs__event,axiom,
! [X0,X1,X2] :
( ( subs(X0,X1)
& chea(X2,X1) )
=> ? [X3] :
( subs(X3,X2)
& chea(X3,X0) ) ),
file('theBenchmark.p',chea_subs_abs__event) ).
fof(ave07_era5_synth_qa07_007_mira_news_1295_a19984,axiom,
( sort(m__374nchen_0,fe)
& 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(c87,varia_c)
& refer(c87,indet)
& quant(c87,one)
& gener(c87,sp)
& fact(c87,real)
& etype(c87,int0)
& card(c87,int1)
& sort(c87,na)
& sort(bmw_0,fe)
& varia(firma_1_1,varia_c)
& refer(firma_1_1,refer_c)
& quant(firma_1_1,one)
& gener(firma_1_1,ge)
& fact(firma_1_1,real)
& etype(firma_1_1,int0)
& card(firma_1_1,int1)
& sort(firma_1_1,io)
& sort(firma_1_1,d)
& varia(c74,varia_c)
& refer(c74,indet)
& quant(c74,one)
& gener(c74,sp)
& fact(c74,real)
& etype(c74,int0)
& card(c74,int1)
& sort(c74,na)
& sort(rover_0,fe)
& sort(britisch__1_1,nq)
& varia(c56,varia_c)
& refer(c56,indet)
& quant(c56,one)
& gener(c56,sp)
& fact(c56,real)
& etype(c56,int0)
& card(c56,int1)
& sort(c56,na)
& varia(annahme_1_1,varia_c)
& refer(annahme_1_1,refer_c)
& quant(annahme_1_1,one)
& gener(annahme_1_1,ge)
& fact(annahme_1_1,real)
& etype(annahme_1_1,int0)
& card(annahme_1_1,int1)
& sort(annahme_1_1,ad)
& varia(c55,con)
& refer(c55,det)
& quant(c55,one)
& gener(c55,sp)
& fact(c55,real)
& etype(c55,int0)
& card(c55,int1)
& sort(c55,io)
& sort(c55,d)
& sort(eu_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(kommission_1_1,varia_c)
& refer(kommission_1_1,refer_c)
& quant(kommission_1_1,quant_c)
& gener(kommission_1_1,ge)
& fact(kommission_1_1,real)
& etype(kommission_1_1,int1)
& card(kommission_1_1,card_c)
& sort(kommission_1_1,io)
& sort(kommission_1_1,d)
& varia(c19,varia_c)
& refer(c19,det)
& quant(c19,one)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,int0)
& card(c19,int1)
& sort(c19,na)
& varia(c86,con)
& refer(c86,det)
& quant(c86,one)
& gener(c86,sp)
& fact(c86,real)
& etype(c86,int0)
& card(c86,int1)
& sort(c86,io)
& sort(c86,d)
& varia(c73,con)
& refer(c73,det)
& quant(c73,one)
& gener(c73,sp)
& fact(c73,real)
& etype(c73,int0)
& card(c73,int1)
& sort(c73,io)
& sort(c73,d)
& varia(c25,con)
& refer(c25,det)
& quant(c25,one)
& gener(c25,sp)
& fact(c25,real)
& etype(c25,int0)
& card(c25,int1)
& sort(c25,ad)
& varia(c18,varia_c)
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int1)
& card(c18,int1)
& sort(c18,io)
& sort(c18,d)
& varia(c171,varia_c)
& refer(c171,refer_c)
& quant(c171,quant_c)
& gener(c171,gener_c)
& fact(c171,real)
& etype(c171,etype_c)
& card(c171,card_c)
& sort(c171,ent)
& varia(fabrikant_1_1,varia_c)
& refer(fabrikant_1_1,refer_c)
& quant(fabrikant_1_1,one)
& gener(fabrikant_1_1,ge)
& fact(fabrikant_1_1,real)
& etype(fabrikant_1_1,int0)
& card(fabrikant_1_1,int1)
& sort(fabrikant_1_1,io)
& sort(fabrikant_1_1,d)
& varia(auto__1_1,varia_c)
& refer(auto__1_1,refer_c)
& quant(auto__1_1,one)
& gener(auto__1_1,ge)
& fact(auto__1_1,real)
& etype(auto__1_1,int0)
& card(auto__1_1,int1)
& sort(auto__1_1,d)
& varia(autobauer_1_1,varia_c)
& refer(autobauer_1_1,refer_c)
& quant(autobauer_1_1,one)
& gener(autobauer_1_1,ge)
& fact(autobauer_1_1,real)
& etype(autobauer_1_1,int0)
& card(autobauer_1_1,int1)
& sort(autobauer_1_1,io)
& sort(autobauer_1_1,d)
& val(c87,m__374nchen_0)
& sub(c87,name_1_1)
& sub(c86,stadt__1_1)
& attr(c86,c87)
& val(c74,bmw_0)
& sub(c74,name_1_1)
& sub(c73,firma_1_1)
& attr(c73,c74)
& val(c56,rover_0)
& sub(c56,name_1_1)
& sub(c55,autobauer_1_1)
& prop(c55,britisch__1_1)
& attr(c55,c56)
& subs(c25,annahme_1_1)
& obj(c25,c55)
& val(c19,eu_0)
& sub(c19,name_1_1)
& sub(c18,kommission_1_1)
& attr(c18,c19)
& tupl_p5(c171,c18,c25,c73,c86)
& sub(autobauer_1_1,fabrikant_1_1)
& assoc(autobauer_1_1,auto__1_1) ),
file('theBenchmark.p',ave07_era5_synth_qa07_007_mira_news_1295_a19984) ).
fof(synth_qa07_007_mira_news_1295_a19984,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( val(X1,bmw_0)
& subs(X3,n374bernehmen_1_1)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& attr(X4,X5)
& attr(X2,X1) ),
file('theBenchmark.p',synth_qa07_007_mira_news_1295_a19984) ).
fof(synth_qa07_007_mira_news_1295_a19984_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( val(X1,bmw_0)
& subs(X3,n374bernehmen_1_1)
& sub(X1,name_1_1)
& sub(X0,firma_1_1)
& attr(X4,X5)
& attr(X2,X1) ),
inference(assume_negation,[status(cth)],[synth_qa07_007_mira_news_1295_a19984]) ).
fof(nnf_23,plain,
! [X0,X1,X2] :
( ? [X3] :
( subs(X3,X2)
& chea(X3,X0) )
| ~ subs(X0,X1)
| ~ chea(X2,X1) ),
inference(fof_nnf,[status(thm)],[chea_subs_abs__event]) ).
fof(sk_chea_subs_abs__event_sk,plain,
! [X0,X1,X2] :
( ( subs(sK0(X0,X1,X2),X2)
& chea(sK0(X0,X1,X2),X0) )
| ~ subs(X0,X1)
| ~ chea(X2,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[nnf_23]) ).
fof(sk_chea_subs_abs__event,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subs(sK0(VAR_2,VAR_1,VAR_0),VAR_0)
| ~ subs(VAR_2,VAR_1)
| ~ chea(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( chea(sK0(VAR_2,VAR_1,VAR_0),VAR_2)
| ~ subs(VAR_2,VAR_1)
| ~ chea(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_chea_subs_abs__event_sk]) ).
cnf(c_143,plain,
( subs(sK0(C,B,A),A)
| ~ subs(C,B)
| ~ chea(A,B) ),
inference(split_conjunct,[status(thm)],[sk_chea_subs_abs__event]) ).
fof(fact_8354,axiom,
chea(n374bernehmen_1_1,annahme_1_1),
file('theBenchmark.p',fact_8354) ).
cnf(c_165,plain,
chea(n374bernehmen_1_1,annahme_1_1),
inference(clausify,[status(thm)],[fact_8354]) ).
cnf(c_175,plain,
attr(c18,c19),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_180,plain,
subs(c25,annahme_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_186,plain,
attr(c73,c74),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_187,plain,
sub(c73,firma_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_188,plain,
sub(c74,name_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_189,plain,
val(c74,bmw_0),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_news_1295_a19984]) ).
cnf(c_352,negated_conjecture,
( ~ val(B,bmw_0)
| ~ subs(F,n374bernehmen_1_1)
| ~ sub(B,name_1_1)
| ~ sub(E,firma_1_1)
| ~ attr(C,D)
| ~ attr(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_007_mira_news_1295_a19984_neg]) ).
cnf(c_557,plain,
( ~ val(B,bmw_0)
| ~ subs(D,n374bernehmen_1_1)
| ~ sub(B,name_1_1)
| ~ sub(C,firma_1_1)
| ~ attr(A,B) ),
inference(resolve,[status(thm)],[c_175,c_352]) ).
cnf(c_1345,plain,
( ~ val(c74,bmw_0)
| ~ subs(B,n374bernehmen_1_1)
| ~ sub(c74,name_1_1)
| ~ sub(A,firma_1_1) ),
inference(resolve,[status(thm)],[c_186,c_557]) ).
cnf(c_1346,plain,
( ~ val(c74,bmw_0)
| ~ subs(B,n374bernehmen_1_1)
| ~ sub(A,firma_1_1) ),
inference(resolve,[status(thm)],[c_188,c_1345]) ).
cnf(c_601,plain,
( ~ subs(B,n374bernehmen_1_1)
| ~ sub(A,firma_1_1) ),
inference(resolve,[status(thm)],[c_189,c_1346]) ).
cnf(c_604,plain,
~ subs(A,n374bernehmen_1_1),
inference(resolve,[status(thm)],[c_601,c_187]) ).
cnf(c_1347,plain,
( subs(sK0(A,annahme_1_1,n374bernehmen_1_1),n374bernehmen_1_1)
| ~ subs(A,annahme_1_1) ),
inference(resolve,[status(thm)],[c_143,c_165]) ).
cnf(c_1348,plain,
subs(sK0(c25,annahme_1_1,n374bernehmen_1_1),n374bernehmen_1_1),
inference(resolve,[status(thm)],[c_1347,c_180]) ).
cnf(c_1344,plain,
$false,
inference(resolve,[status(thm)],[c_604,c_1348]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+50 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.37 % Computer : n008.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 27 01:10:24 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.37 % Process 735175 was started by sandbox2 on n008,
% 0.13/0.37 % Sun Sep 27 01:10:24 2026
% 0.13/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.24/0.60
% 0.24/0.60 % SInE (scan): 67 to sos (tol 1.5x), 19 to usable (tol 2.0x), 10102 zapped, of 10188 axioms (depth 3).
% 0.24/0.60
% 0.24/0.60 % From the command line: assign(max_seconds, 300).
% 0.24/0.60
% 0.24/0.60 % SZS status Theorem for theBenchmark
% 0.24/0.60
% 0.24/0.60 % Proof 1 at 0.08 (+ 0.04) seconds.
% 0.24/0.60 % Length of proof is 16.
% 0.24/0.60 % Level of proof is 5.
% 0.24/0.60 % Maximum clause weight is 18.000.
% 0.24/0.60 % Given clauses 342.
% 0.24/0.60
% 0.24/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------