%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR115+83 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:48 AM UTC 2026
% Result : Theorem 18.82s 2.99s
% Output : CNFRefutation 18.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 6
% Syntax : Number of formulae : 46 ( 16 unt; 0 def)
% Number of atoms : 389 ( 0 equ)
% Maximal formula atoms : 211 ( 8 avg)
% Number of connectives : 460 ( 117 ~; 100 |; 240 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 211 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-3 aty)
% Number of functors : 67 ( 67 usr; 66 con; 0-3 aty)
% Number of variables : 105 ( 8 sgn 20 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(has_card_eq,axiom,
! [X0,X1] :
( card(X0,X1)
=> has_card_leq(X0,X1) ),
file('theBenchmark.p',has_card_eq) ).
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(chea_agt_abs__event,axiom,
! [X0,X1,X2] :
( ( chea(X1,X0)
& agt(X0,X2) )
=> agt(X1,X2) ),
file('theBenchmark.p',chea_agt_abs__event) ).
fof(ave07_era5_synth_qa07_007_mira_wp_499,axiom,
( gener(prop_0,gener_c)
& fact(prop_0,real)
& sort(prop_0,st)
& gener(werden_1_1,ge)
& fact(werden_1_1,real)
& sort(werden_1_1,dn)
& sort(besonders_1_1,lg)
& 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(c1798,varia_c)
& refer(c1798,indet)
& quant(c1798,one)
& gener(c1798,sp)
& fact(c1798,real)
& etype(c1798,int0)
& card(c1798,int1)
& sort(c1798,na)
& sort(rover_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)
& sort(britisch__1_1,nq)
& varia(c1786,varia_c)
& refer(c1786,indet)
& quant(c1786,one)
& gener(c1786,sp)
& fact(c1786,real)
& etype(c1786,int0)
& card(c1786,int1)
& sort(c1786,na)
& gener(einf__344deln_1_1,ge)
& fact(einf__344deln_1_1,real)
& sort(einf__344deln_1_1,da)
& gener(c1751,sp)
& fact(c1751,real)
& sort(c1751,da)
& 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)
& sort(c2,tq)
& varia(c1785,con)
& refer(c1785,det)
& quant(c1785,one)
& gener(c1785,sp)
& fact(c1785,real)
& etype(c1785,int0)
& card(c1785,int1)
& sort(c1785,io)
& sort(c1785,d)
& varia(c1797,con)
& refer(c1797,det)
& quant(c1797,one)
& gener(c1797,sp)
& fact(c1797,real)
& etype(c1797,int0)
& card(c1797,int1)
& sort(c1797,io)
& sort(c1797,d)
& card(c1744,int1994)
& sort(c1744,nu)
& varia(jahr__1_1,varia_c)
& refer(jahr__1_1,refer_c)
& quant(jahr__1_1,quant_c)
& gener(jahr__1_1,ge)
& fact(jahr__1_1,real)
& etype(jahr__1_1,etype_c)
& card(jahr__1_1,card_c)
& sort(jahr__1_1,ta)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,me)
& varia(c1748,varia_c)
& refer(c1748,refer_c)
& quant(c1748,quant_c)
& gener(c1748,sp)
& fact(c1748,real)
& etype(c1748,etype_c)
& card(c1748,card_c)
& sort(c1748,ta)
& sort(c1748,oa)
& sort(c1748,me)
& varia(c1747,con)
& refer(c1747,det)
& quant(c1747,one)
& gener(c1747,sp)
& fact(c1747,real)
& etype(c1747,int0)
& card(c1747,int1)
& sort(c1747,t)
& sort(pischetsrieder_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)
& varia(mensch_1_1,varia_c)
& refer(mensch_1_1,refer_c)
& quant(mensch_1_1,one)
& gener(mensch_1_1,ge)
& fact(mensch_1_1,real)
& etype(mensch_1_1,int0)
& card(mensch_1_1,int1)
& sort(mensch_1_1,d)
& sort(bekannt_1_1,nq)
& varia(c1736,varia_c)
& refer(c1736,indet)
& quant(c1736,one)
& gener(c1736,sp)
& fact(c1736,real)
& etype(c1736,int0)
& card(c1736,int1)
& sort(c1736,na)
& varia(c1735,con)
& refer(c1735,det)
& quant(c1735,one)
& gener(c1735,sp)
& fact(c1735,real)
& etype(c1735,int0)
& card(c1735,int1)
& sort(c1735,d)
& gener(c1800,sp)
& fact(c1800,real)
& sort(c1800,dn)
& gener(c1801,sp)
& fact(c1801,real)
& sort(c1801,st)
& varia(c1750,con)
& refer(c1750,det)
& quant(c1750,one)
& gener(c1750,sp)
& fact(c1750,real)
& etype(c1750,int0)
& card(c1750,int1)
& sort(c1750,ad)
& gener(c1731,sp)
& fact(c1731,real)
& sort(c1731,dn)
& 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)
& sort(automobil_1_1,tq)
& 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)
& chsp2(einf__344deln_1_1,c2)
& subr(c1801,prop_0)
& arg2(c1801,bekannt_1_1)
& arg1(c1801,c1735)
& mods(c1800,besonders_1_1,werden_1_1)
& val(c1798,bmw_0)
& sub(c1798,name_1_1)
& sub(c1797,firma_1_1)
& attr(c1797,c1798)
& val(c1786,rover_0)
& sub(c1786,name_1_1)
& sub(c1785,autobauer_1_1)
& prop(c1785,britisch__1_1)
& attr(c1785,c1786)
& temp(c1751,c1747)
& subs(c1751,einf__344deln_1_1)
& obj(c1751,c1750)
& agt(c1751,c1735)
& subs(c1750,annahme_1_1)
& prop(c1750,c2)
& obj(c1750,c1785)
& agt(c1750,c1797)
& val(c1748,c1744)
& sub(c1748,jahr__1_1)
& attr(c1747,c1748)
& val(c1736,pischetsrieder_0)
& sub(c1736,familiename_1_1)
& sub(c1735,mensch_1_1)
& prop(c1735,bekannt_1_1)
& attr(c1735,c1736)
& subs(c1731,c1800)
& rslt(c1731,c1801)
& cstr(c1731,c1750)
& sub(autobauer_1_1,fabrikant_1_1)
& assoc(autobauer_1_1,automobil_1_1) ),
file('theBenchmark.p',ave07_era5_synth_qa07_007_mira_wp_499) ).
fof(synth_qa07_007_mira_wp_499,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,bmw_0)
& val(X1,bmw_0)
& subs(X4,n374bernehmen_1_1)
& sub(X6,jahr__1_1)
& sub(X2,name_1_1)
& sub(X0,firma_1_1)
& sub(X1,name_1_1)
& has_card_leq(X7,int1994)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
file('theBenchmark.p',synth_qa07_007_mira_wp_499) ).
fof(synth_qa07_007_mira_wp_499_neg,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,bmw_0)
& val(X1,bmw_0)
& subs(X4,n374bernehmen_1_1)
& sub(X6,jahr__1_1)
& sub(X2,name_1_1)
& sub(X0,firma_1_1)
& sub(X1,name_1_1)
& has_card_leq(X7,int1994)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
inference(assume_negation,[status(cth)],[synth_qa07_007_mira_wp_499]) ).
cnf(c_185,plain,
( has_card_leq(A,B)
| ~ card(A,B) ),
inference(clausify,[status(thm)],[has_card_eq]) ).
fof(nnf_29,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_29]) ).
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_231,plain,
( chea(sK0(C,B,A),C)
| ~ subs(C,B)
| ~ chea(A,B) ),
inference(split_conjunct,[status(thm)],[sk_chea_subs_abs__event]) ).
cnf(c_232,plain,
( subs(sK0(C,B,A),A)
| ~ subs(C,B)
| ~ chea(A,B) ),
inference(split_conjunct,[status(thm)],[sk_chea_subs_abs__event]) ).
cnf(c_234,plain,
( agt(C,B)
| ~ chea(C,A)
| ~ agt(A,B) ),
inference(clausify,[status(thm)],[chea_agt_abs__event]) ).
fof(fact_8354,axiom,
chea(n374bernehmen_1_1,annahme_1_1),
file('theBenchmark.p',fact_8354) ).
cnf(c_263,plain,
chea(n374bernehmen_1_1,annahme_1_1),
inference(clausify,[status(thm)],[fact_8354]) ).
cnf(c_280,plain,
attr(c1747,c1748),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_281,plain,
sub(c1748,jahr__1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_282,plain,
val(c1748,c1744),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_283,plain,
agt(c1750,c1797),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_286,plain,
subs(c1750,annahme_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_296,plain,
attr(c1797,c1798),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_297,plain,
sub(c1797,firma_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_298,plain,
sub(c1798,name_1_1),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_299,plain,
val(c1798,bmw_0),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_404,plain,
card(c1744,int1994),
inference(clausify,[status(thm)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c_481,negated_conjecture,
( ~ val(V6,V7)
| ~ val(E,bmw_0)
| ~ val(D,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(V6,jahr__1_1)
| ~ sub(E,name_1_1)
| ~ sub(C,firma_1_1)
| ~ sub(D,name_1_1)
| ~ has_card_leq(V7,int1994)
| ~ attr(F,V6)
| ~ attr(B,E)
| ~ attr(C,D)
| ~ agt(A,B) ),
inference(clausify,[status(thm)],[synth_qa07_007_mira_wp_499_neg]) ).
cnf(c_8045,negated_conjecture,
( ~ val(E,F)
| ~ val(C,bmw_0)
| ~ val(c1798,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(E,jahr__1_1)
| ~ sub(C,name_1_1)
| ~ sub(c1797,firma_1_1)
| ~ sub(c1798,name_1_1)
| ~ has_card_leq(F,int1994)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_296,c_481]) ).
cnf(c_8046,negated_conjecture,
( ~ val(E,F)
| ~ val(C,bmw_0)
| ~ val(c1798,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(E,jahr__1_1)
| ~ sub(C,name_1_1)
| ~ sub(c1797,firma_1_1)
| ~ has_card_leq(F,int1994)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_298,c_8045]) ).
cnf(c_8047,negated_conjecture,
( ~ val(E,F)
| ~ val(C,bmw_0)
| ~ val(c1798,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(E,jahr__1_1)
| ~ sub(C,name_1_1)
| ~ has_card_leq(F,int1994)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_297,c_8046]) ).
cnf(c_515,negated_conjecture,
( ~ val(E,F)
| ~ val(C,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(E,jahr__1_1)
| ~ sub(C,name_1_1)
| ~ has_card_leq(F,int1994)
| ~ attr(D,E)
| ~ attr(B,C)
| ~ agt(A,B) ),
inference(resolve,[status(thm)],[c_299,c_8047]) ).
cnf(c_8048,plain,
( ~ val(C,D)
| ~ val(c1798,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,jahr__1_1)
| ~ sub(c1798,name_1_1)
| ~ has_card_leq(D,int1994)
| ~ attr(B,C)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_515,c_296]) ).
cnf(c_8049,plain,
( ~ val(C,D)
| ~ val(c1798,bmw_0)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,jahr__1_1)
| ~ has_card_leq(D,int1994)
| ~ attr(B,C)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_298,c_8048]) ).
cnf(c_520,plain,
( ~ val(C,D)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(C,jahr__1_1)
| ~ has_card_leq(D,int1994)
| ~ attr(B,C)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_299,c_8049]) ).
cnf(c_8050,plain,
( ~ val(c1748,B)
| ~ subs(A,n374bernehmen_1_1)
| ~ sub(c1748,jahr__1_1)
| ~ has_card_leq(B,int1994)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_520,c_280]) ).
cnf(c_537,plain,
( ~ val(c1748,B)
| ~ subs(A,n374bernehmen_1_1)
| ~ has_card_leq(B,int1994)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_281,c_8050]) ).
cnf(c_555,plain,
( ~ subs(A,n374bernehmen_1_1)
| ~ has_card_leq(c1744,int1994)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_537,c_282]) ).
cnf(c_8051,plain,
( ~ card(c1744,int1994)
| ~ subs(A,n374bernehmen_1_1)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_555,c_185]) ).
cnf(c_567,plain,
( ~ subs(A,n374bernehmen_1_1)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_404,c_8051]) ).
cnf(c_8052,plain,
( chea(sK0(A,annahme_1_1,n374bernehmen_1_1),A)
| ~ subs(A,annahme_1_1) ),
inference(resolve,[status(thm)],[c_231,c_263]) ).
cnf(c_882,plain,
chea(sK0(c1750,annahme_1_1,n374bernehmen_1_1),c1750),
inference(resolve,[status(thm)],[c_8052,c_286]) ).
cnf(c_8053,plain,
( subs(sK0(A,annahme_1_1,n374bernehmen_1_1),n374bernehmen_1_1)
| ~ subs(A,annahme_1_1) ),
inference(resolve,[status(thm)],[c_232,c_263]) ).
cnf(c_902,plain,
subs(sK0(c1750,annahme_1_1,n374bernehmen_1_1),n374bernehmen_1_1),
inference(resolve,[status(thm)],[c_8053,c_286]) ).
cnf(c_948,plain,
( ~ subs(B,n374bernehmen_1_1)
| ~ chea(B,A)
| ~ agt(A,c1797) ),
inference(resolve,[status(thm)],[c_234,c_567]) ).
cnf(c_1101,plain,
( ~ subs(A,n374bernehmen_1_1)
| ~ chea(A,c1750) ),
inference(resolve,[status(thm)],[c_948,c_283]) ).
cnf(c_8054,plain,
~ subs(sK0(c1750,annahme_1_1,n374bernehmen_1_1),n374bernehmen_1_1),
inference(resolve,[status(thm)],[c_882,c_1101]) ).
cnf(c_8044,plain,
$false,
inference(resolve,[status(thm)],[c_902,c_8054]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR115+83 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n009.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sun Sep 27 01:12:14 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.46 % Process 1530748 was started by sandbox on n009,
% 0.19/0.46 % Sun Sep 27 01:12:14 2026
% 0.19/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 18.82/2.99
% 18.82/2.99 % SInE (scan): 94 to sos (tol 1.5x), 30 to usable (tol 2.0x), 10064 zapped, of 10188 axioms (depth 3).
% 18.82/2.99
% 18.82/2.99 % From the command line: assign(max_seconds, 300).
% 18.82/2.99
% 18.82/2.99 % given #500 (F,wt=14): 906 -agtrel(n374bernehmen_1_1,A) | -attch(c1797,B) | -sub(firma_1_1,C) | -sub(C,A). [resolve(855,c,218,c)].
% 18.82/2.99
% 18.82/2.99 % given #1000 (T,wt=5): 1719 has_quant_leq(c1786,quant_c). [ur(72,a,443,a)].
% 18.82/2.99
% 18.82/2.99 % SZS status Theorem for theBenchmark
% 18.82/2.99
% 18.82/2.99 % Proof 1 at 1.91 (+ 0.41) seconds.
% 18.82/2.99 % Length of proof is 31.
% 18.82/2.99 % Level of proof is 9.
% 18.82/2.99 % Maximum clause weight is 41.000.
% 18.82/2.99 % Given clauses 1485.
% 18.82/2.99
% 18.82/2.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------