%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR115+12 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 11:19:32 AM UTC 2025
% Result : Theorem 4.84s 0.98s
% Output : CNFRefutation 4.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of formulae : 38 ( 21 unt; 0 def)
% Number of atoms : 367 ( 0 equ)
% Maximal formula atoms : 277 ( 9 avg)
% Number of connectives : 358 ( 29 ~; 26 |; 299 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 277 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-9 aty)
% Number of functors : 68 ( 68 usr; 66 con; 0-3 aty)
% Number of variables : 43 ( 3 sgn 9 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(synth_qa07_007_mira_news_1112_a19984,plain,
? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X2,X1)
& attr(X4,X5)
& has_card_leq(X6,int1994)
& obj(X3,X0)
& prop(X0,britisch__1_1)
& sub(X1,name_1_1)
& sub(X5,jahr__1_1)
& val(X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_007_mira_news_1112_a19984) ).
fof(synth_qa07_007_mira_news_1112_a19984_negated,plain,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X2,X1)
& attr(X4,X5)
& has_card_leq(X6,int1994)
& obj(X3,X0)
& prop(X0,britisch__1_1)
& sub(X1,name_1_1)
& sub(X5,jahr__1_1)
& val(X5,X6) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1112_a19984]) ).
cnf(10360,plain,
( ~ has_card_leq(X0,int1994)
| ~ sub(X1,name_1_1)
| ~ sub(X2,jahr__1_1)
| ~ obj(X3,X4)
| ~ attr(X5,X1)
| ~ attr(X6,X2)
| ~ prop(X4,britisch__1_1)
| ~ val(X2,X0) ),
inference(cnf,[status(esa)],[synth_qa07_007_mira_news_1112_a19984_negated]) ).
cnf(l0,plain,
( ~ has_card_leq(c14110,int1994)
| ~ sub(c14383,name_1_1)
| ~ sub(c14116,jahr__1_1)
| ~ obj(sK3(sK50(c14368,britisch__1_1,grossbritannien_0),c14368),c14368)
| ~ attr(c14382,c14383)
| ~ attr(c14115,c14116)
| ~ prop(c14368,britisch__1_1)
| ~ val(c14116,c14110) ),
inference(instantiation,[status(thm)],[10360]) ).
fof(ave07_era5_synth_qa07_007_mira_news_1112_a19984,plain,
( assoc(autobauer_1_1,auto__1_1)
& sub(autobauer_1_1,fabrikant_1_1)
& sub(c14109,abschlu__337_1_1)
& assoc(c14115,c14109)
& attr(c14115,c14116)
& sub(c14116,jahr__1_1)
& val(c14116,c14110)
& sub(c14120,bmw_1_1)
& sub(c14124,firmengruppe_1_1)
& attr(c14368,c14369)
& prop(c14368,britisch__1_1)
& sub(c14368,autobauer_1_1)
& sub(c14369,name_1_1)
& val(c14369,rover_0)
& pmod(c14381,erst_1_1,land_1_1)
& attr(c14382,c14383)
& sub(c14382,c14381)
& sub(c14383,name_1_1)
& val(c14383,usa_0)
& poss(c14386,c14382)
& sub(c14391,artefakt_1_1)
& attr(c14397,c14398)
& sub(c14397,stadt__1_1)
& sub(c14398,name_1_1)
& val(c14398,spartanburg_0)
& subs(c14404,betrieb_1_1)
& tupl_p9(c14579,c14115,c14120,c14124,c14368,c14382,c14391,c14397,c14404)
& sort(autobauer_1_1,d)
& sort(autobauer_1_1,io)
& card(autobauer_1_1,int1)
& etype(autobauer_1_1,int0)
& fact(autobauer_1_1,real)
& gener(autobauer_1_1,ge)
& quant(autobauer_1_1,one)
& refer(autobauer_1_1,refer_c)
& varia(autobauer_1_1,varia_c)
& sort(auto__1_1,d)
& card(auto__1_1,int1)
& etype(auto__1_1,int0)
& fact(auto__1_1,real)
& gener(auto__1_1,ge)
& quant(auto__1_1,one)
& refer(auto__1_1,refer_c)
& varia(auto__1_1,varia_c)
& sort(fabrikant_1_1,d)
& sort(fabrikant_1_1,io)
& card(fabrikant_1_1,int1)
& etype(fabrikant_1_1,int0)
& fact(fabrikant_1_1,real)
& gener(fabrikant_1_1,ge)
& quant(fabrikant_1_1,one)
& refer(fabrikant_1_1,refer_c)
& varia(fabrikant_1_1,varia_c)
& sort(c14109,ad)
& sort(c14109,io)
& card(c14109,int1)
& etype(c14109,int0)
& fact(c14109,real)
& gener(c14109,gener_c)
& quant(c14109,one)
& refer(c14109,refer_c)
& varia(c14109,varia_c)
& sort(abschlu__337_1_1,ad)
& sort(abschlu__337_1_1,io)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& sort(c14115,t)
& card(c14115,int1)
& etype(c14115,int0)
& fact(c14115,real)
& gener(c14115,sp)
& quant(c14115,one)
& refer(c14115,det)
& varia(c14115,con)
& sort(c14116,me)
& sort(c14116,oa)
& sort(c14116,ta)
& card(c14116,card_c)
& etype(c14116,etype_c)
& fact(c14116,real)
& gener(c14116,sp)
& quant(c14116,quant_c)
& refer(c14116,refer_c)
& varia(c14116,varia_c)
& sort(jahr__1_1,me)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,ta)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& sort(c14110,nu)
& card(c14110,int1994)
& sort(c14120,d)
& card(c14120,int1)
& etype(c14120,int0)
& fact(c14120,real)
& gener(c14120,sp)
& quant(c14120,one)
& refer(c14120,det)
& varia(c14120,con)
& sort(bmw_1_1,d)
& card(bmw_1_1,int1)
& etype(bmw_1_1,int0)
& fact(bmw_1_1,real)
& gener(bmw_1_1,ge)
& quant(bmw_1_1,one)
& refer(bmw_1_1,refer_c)
& varia(bmw_1_1,varia_c)
& sort(c14124,d)
& sort(c14124,io)
& card(c14124,int1)
& etype(c14124,int0)
& fact(c14124,real)
& gener(c14124,gener_c)
& quant(c14124,one)
& refer(c14124,refer_c)
& varia(c14124,varia_c)
& sort(firmengruppe_1_1,d)
& sort(firmengruppe_1_1,io)
& card(firmengruppe_1_1,int1)
& etype(firmengruppe_1_1,int0)
& fact(firmengruppe_1_1,real)
& gener(firmengruppe_1_1,ge)
& quant(firmengruppe_1_1,one)
& refer(firmengruppe_1_1,refer_c)
& varia(firmengruppe_1_1,varia_c)
& sort(c14368,d)
& sort(c14368,io)
& card(c14368,int1)
& etype(c14368,int0)
& fact(c14368,real)
& gener(c14368,sp)
& quant(c14368,one)
& refer(c14368,det)
& varia(c14368,con)
& sort(c14369,na)
& card(c14369,int1)
& etype(c14369,int0)
& fact(c14369,real)
& gener(c14369,sp)
& quant(c14369,one)
& refer(c14369,indet)
& varia(c14369,varia_c)
& sort(britisch__1_1,nq)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(rover_0,fe)
& sort(c14381,d)
& sort(c14381,io)
& card(c14381,int1)
& etype(c14381,int0)
& fact(c14381,real)
& gener(c14381,ge)
& quant(c14381,one)
& refer(c14381,refer_c)
& varia(c14381,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(c14382,d)
& sort(c14382,io)
& card(c14382,int1)
& etype(c14382,int0)
& fact(c14382,real)
& gener(c14382,sp)
& quant(c14382,one)
& refer(c14382,det)
& varia(c14382,con)
& sort(c14383,na)
& card(c14383,int1)
& etype(c14383,int0)
& fact(c14383,real)
& gener(c14383,sp)
& quant(c14383,one)
& refer(c14383,indet)
& varia(c14383,varia_c)
& sort(usa_0,fe)
& sort(c14386,o)
& card(c14386,int1)
& etype(c14386,int0)
& fact(c14386,real)
& gener(c14386,sp)
& quant(c14386,one)
& refer(c14386,det)
& varia(c14386,varia_c)
& sort(c14391,d)
& sort(c14391,io)
& card(c14391,int1)
& etype(c14391,int0)
& fact(c14391,real)
& gener(c14391,gener_c)
& quant(c14391,one)
& refer(c14391,refer_c)
& varia(c14391,varia_c)
& sort(artefakt_1_1,d)
& sort(artefakt_1_1,io)
& card(artefakt_1_1,int1)
& etype(artefakt_1_1,int0)
& fact(artefakt_1_1,real)
& gener(artefakt_1_1,ge)
& quant(artefakt_1_1,one)
& refer(artefakt_1_1,refer_c)
& varia(artefakt_1_1,varia_c)
& sort(c14397,d)
& sort(c14397,io)
& card(c14397,int1)
& etype(c14397,int0)
& fact(c14397,real)
& gener(c14397,sp)
& quant(c14397,one)
& refer(c14397,det)
& varia(c14397,con)
& sort(c14398,na)
& card(c14398,int1)
& etype(c14398,int0)
& fact(c14398,real)
& gener(c14398,sp)
& quant(c14398,one)
& refer(c14398,indet)
& varia(c14398,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(spartanburg_0,fe)
& sort(c14404,ad)
& card(c14404,int1)
& etype(c14404,int0)
& fact(c14404,real)
& gener(c14404,gener_c)
& quant(c14404,one)
& refer(c14404,refer_c)
& varia(c14404,varia_c)
& sort(betrieb_1_1,ad)
& card(betrieb_1_1,int1)
& etype(betrieb_1_1,int0)
& fact(betrieb_1_1,real)
& gener(betrieb_1_1,ge)
& quant(betrieb_1_1,one)
& refer(betrieb_1_1,refer_c)
& varia(betrieb_1_1,varia_c)
& sort(c14579,ent)
& card(c14579,card_c)
& etype(c14579,etype_c)
& fact(c14579,real)
& gener(c14579,gener_c)
& quant(c14579,quant_c)
& refer(c14579,refer_c)
& varia(c14579,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_007_mira_news_1112_a19984) ).
cnf(10376,plain,
attr(c14382,c14383),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l12,plain,
attr(c14382,c14383),
inference(instantiation,[status(thm)],[10376]) ).
cnf(10367,plain,
val(c14116,c14110),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l10,plain,
val(c14116,c14110),
inference(instantiation,[status(thm)],[10367]) ).
cnf(10365,plain,
attr(c14115,c14116),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l29,plain,
attr(c14115,c14116),
inference(instantiation,[status(thm)],[10365]) ).
cnf(10366,plain,
sub(c14116,jahr__1_1),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l1,plain,
sub(c14116,jahr__1_1),
inference(instantiation,[status(thm)],[10366]) ).
fof(has_card_eq,plain,
! [X0,X1] :
( card(X0,X1)
=> has_card_leq(X0,X1) ),
file('Axioms/CSR004+0.ax',has_card_eq) ).
cnf(19,plain,
( ~ card(X0,X1)
| has_card_leq(X0,X1) ),
inference(cnf,[status(esa)],[has_card_eq]) ).
cnf(l3,plain,
( ~ card(c14110,int1994)
| has_card_leq(c14110,int1994) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(10461,plain,
card(c14110,int1994),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l39,plain,
card(c14110,int1994),
inference(instantiation,[status(thm)],[10461]) ).
cnf(10371,plain,
prop(c14368,britisch__1_1),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l11,plain,
prop(c14368,britisch__1_1),
inference(instantiation,[status(thm)],[10371]) ).
cnf(10378,plain,
sub(c14383,name_1_1),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l8,plain,
sub(c14383,name_1_1),
inference(instantiation,[status(thm)],[10378]) ).
fof(loc__geben_1_1_loc,plain,
! [X0,X1] :
( ( has_fact_leq(X1,real)
& loc(X1,X0) )
=> ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) ) ),
file('Axioms/CSR004+0.ax',loc__geben_1_1_loc) ).
cnf(102,plain,
( ~ has_fact_leq(X0,real)
| ~ loc(X0,X1)
| obj(sK3(X1,X0),X0) ),
inference(cnf,[status(esa)],[loc__geben_1_1_loc]) ).
cnf(l14,plain,
( ~ has_fact_leq(c14368,real)
| ~ loc(c14368,sK50(c14368,britisch__1_1,grossbritannien_0))
| obj(sK3(sK50(c14368,britisch__1_1,grossbritannien_0),c14368),c14368) ),
inference(instantiation,[status(thm)],[102]) ).
fof(state_adjective__in_state,plain,
! [X0,X1,X2] :
( ( prop(X0,X1)
& state_adjective_state_binding(X1,X2) )
=> ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) ) ),
file('Axioms/CSR004+0.ax',state_adjective__in_state) ).
cnf(279,plain,
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2)
| loc(X0,sK50(X0,X1,X2)) ),
inference(cnf,[status(esa)],[state_adjective__in_state]) ).
cnf(l16,plain,
( ~ prop(c14368,britisch__1_1)
| ~ state_adjective_state_binding(britisch__1_1,grossbritannien_0)
| loc(c14368,sK50(c14368,britisch__1_1,grossbritannien_0)) ),
inference(instantiation,[status(thm)],[279]) ).
fof(has_fact_eq,plain,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('Axioms/CSR004+0.ax',has_fact_eq) ).
cnf(10,plain,
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf,[status(esa)],[has_fact_eq]) ).
cnf(l19,plain,
( ~ fact(c14368,real)
| has_fact_leq(c14368,real) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l20,plain,
prop(c14368,britisch__1_1),
inference(instantiation,[status(thm)],[10371]) ).
cnf(10500,plain,
fact(c14368,real),
inference(cnf,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1112_a19984]) ).
cnf(l35,plain,
fact(c14368,real),
inference(instantiation,[status(thm)],[10500]) ).
fof(fact_8846,plain,
state_adjective_state_binding(britisch__1_1,grossbritannien_0),
file('Axioms/CSR004+0.ax',fact_8846) ).
cnf(9199,plain,
state_adjective_state_binding(britisch__1_1,grossbritannien_0),
inference(cnf,[status(esa)],[fact_8846]) ).
cnf(l18,plain,
state_adjective_state_binding(britisch__1_1,grossbritannien_0),
inference(instantiation,[status(thm)],[9199]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l12,l10,l29,l1,l3,l39,l11,l8,l14,l16,l19,l20,l35,l18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.07 % Problem : CSR115+12 : TPTP v9.0.0. Released v4.0.0.
% 0.02/0.08 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.26 % Computer : n032.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 300
% 0.07/0.26 % DateTime : Sun Jul 20 08:16:34 EDT 2025
% 0.10/0.26 % CPUTime :
% 0.10/0.35 % launching worker at depth: 2
% 0.10/0.35 % launching worker at depth: 1
% 0.10/0.35 % launching worker at depth: 3
% 0.10/0.35 % launching worker at depth: 6
% 0.10/0.35 % launching worker at depth: 4
% 0.10/0.35 % launching worker at depth: 7
% 0.10/0.35 % launching worker at depth: 8
% 0.10/0.35 % launching worker at depth: 5
% 0.10/0.35 % launching worker at depth: 9
% 0.10/0.43 % launching worker at depth: 10
% 4.84/0.98 % SZS status Theorem for theBenchmark
% 4.84/0.98 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------