%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR114+17 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Thu Sep 24 12:15:20 PM UTC 2026
% Result : Theorem 46.90s 11.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR114+17 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n007.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 15:02:43 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.13/5.50 % Drodi V4.1.1
% 46.90/11.43 % Refutation found
% 46.90/11.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.90/11.43 % SZS output start CNFRefutation for theBenchmark
% 46.90/11.43 fof(f155,axiom,(
% 46.90/11.43 (! [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) ) )) )),
% 46.90/11.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.90/11.43 fof(f180,axiom,(
% 46.90/11.43 (! [X0,X1] :( loc(X0,X1)=> (? [X2] :( loc(X2,X1)& scar(X2,X0)& subs(X2,stehen_1_1) ) )) )),
% 46.90/11.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.90/11.43 fof(f9067,axiom,(
% 46.90/11.43 state_adjective_state_binding(italienisch__1_1,italien_0) ),
% 46.90/11.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.90/11.43 fof(f10188,conjecture,(
% 46.90/11.43 (? [X0,X1,X2,X3,X4] :( attr(X0,X1)& loc(X4,X2)& prop(X0,italienisch__1_1)& scar(X4,X3)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& subs(X4,stehen_1_1)& val(X1,rom_0) ) )),
% 46.90/11.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.90/11.43 fof(f10189,negated_conjecture,(
% 46.90/11.43 ~((? [X0,X1,X2,X3,X4] :( attr(X0,X1)& loc(X4,X2)& prop(X0,italienisch__1_1)& scar(X4,X3)& sub(X1,name_1_1)& sub(X0,stadt__1_1)& subs(X4,stehen_1_1)& val(X1,rom_0) ) ))),
% 46.90/11.43 inference(negated_conjecture,[status(cth)],[f10188])).
% 46.90/11.43 fof(f10190,hypothesis,(
% 46.90/11.43 ( tupl_p8(c246,c61,c67,c71,c67,c81,c85,c93)& sub(c61,palazzo_1_1)& attr(c67,c78)& prop(c67,italienisch__1_1)& sub(c67,stadt__1_1)& sub(c71,phantasieansicht_1_1)& sub(c78,name_1_1)& val(c78,rom_0)& attr(c81,c82)& sub(c82,jahr__1_1)& val(c82,c79)& sub(c85,leinwand_1_1)& quant_p3(c93,c89,cm_1_1)& assoc(phantasieansicht_1_1,phantasie_1_1)& sub(phantasieansicht_1_1,anschauung_1_1)& sort(c246,ent)& card(c246,card_c)& etype(c246,etype_c)& fact(c246,real)& gener(c246,gener_c)& quant(c246,quant_c)& refer(c246,refer_c)& varia(c246,varia_c)& sort(c61,d)& card(c61,int1)& etype(c61,int0)& fact(c61,real)& gener(c61,gener_c)& quant(c61,one)& refer(c61,refer_c)& varia(c61,varia_c)& sort(c67,d)& sort(c67,io)& card(c67,int1)& etype(c67,int0)& fact(c67,real)& gener(c67,sp)& quant(c67,one)& refer(c67,indet)& varia(c67,varia_c)& sort(c71,io)& card(c71,int1)& etype(c71,int0)& fact(c71,real)& gener(c71,gener_c)& quant(c71,one)& refer(c71,refer_c)& varia(c71,varia_c)& sort(c81,t)& card(c81,int1)& etype(c81,int0)& fact(c81,real)& gener(c81,sp)& quant(c81,one)& refer(c81,det)& varia(c81,con)& sort(c85,d)& card(c85,int1)& etype(c85,int0)& fact(c85,real)& gener(c85,gener_c)& quant(c85,one)& refer(c85,refer_c)& varia(c85,varia_c)& sort(c93,co)& sort(c93,m)& card(c93,card_c)& etype(c93,etype_c)& fact(c93,real)& gener(c93,gener_c)& quant(c93,quant_c)& refer(c93,refer_c)& varia(c93,con)& sort(palazzo_1_1,d)& card(palazzo_1_1,int1)& etype(palazzo_1_1,int0)& fact(palazzo_1_1,real)& gener(palazzo_1_1,ge)& quant(palazzo_1_1,one)& refer(palazzo_1_1,refer_c)& varia(palazzo_1_1,varia_c)& sort(c78,na)& card(c78,int1)& etype(c78,int0)& fact(c78,real)& gener(c78,sp)& quant(c78,one)& refer(c78,indet)& varia(c78,varia_c)& sort(italienisch__1_1,nq)& 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(phantasieansicht_1_1,io)& card(phantasieansicht_1_1,int1)& etype(phantasieansicht_1_1,int0)& fact(phantasieansicht_1_1,real)& gener(phantasieansicht_1_1,ge)& quant(phantasieansicht_1_1,one)& refer(phantasieansicht_1_1,refer_c)& varia(phantasieansicht_1_1,varia_c)& 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(rom_0,fe)& sort(c82,me)& sort(c82,oa)& sort(c82,ta)& card(c82,card_c)& etype(c82,etype_c)& fact(c82,real)& gener(c82,sp)& quant(c82,quant_c)& refer(c82,refer_c)& varia(c82,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(c79,nu)& card(c79,int1664)& sort(leinwand_1_1,d)& card(leinwand_1_1,int1)& etype(leinwand_1_1,int0)& fact(leinwand_1_1,real)& gener(leinwand_1_1,ge)& quant(leinwand_1_1,one)& refer(leinwand_1_1,refer_c)& varia(leinwand_1_1,varia_c)& sort(c89,nu)& card(c89,int4489)& sort(cm_1_1,me)& gener(cm_1_1,ge)& sort(phantasie_1_1,io)& card(phantasie_1_1,int1)& etype(phantasie_1_1,int0)& fact(phantasie_1_1,real)& gener(phantasie_1_1,ge)& quant(phantasie_1_1,one)& refer(phantasie_1_1,refer_c)& varia(phantasie_1_1,varia_c)& sort(anschauung_1_1,io)& card(anschauung_1_1,int1)& etype(anschauung_1_1,int0)& fact(anschauung_1_1,real)& gener(anschauung_1_1,ge)& quant(anschauung_1_1,one)& refer(anschauung_1_1,refer_c)& varia(anschauung_1_1,varia_c) ) ),
% 46.90/11.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.90/11.43 fof(f10674,plain,(
% 46.90/11.43 ![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))))),
% 46.90/11.43 inference(pre_NNF_transformation,[status(thm)],[f155])).
% 46.90/11.43 fof(f10675,plain,(
% 46.90/11.43 ![X0,X2]: ((![X1]: (~prop(X0,X1)|~state_adjective_state_binding(X1,X2)))|(?[X4]: (((?[X3]: ((?[X5]: ((in(X5,X3)&attr(X3,X4))&loc(X0,X5)))&sub(X3,land_1_1)))&sub(X4,name_1_1))&val(X4,X2))))),
% 46.90/11.43 inference(miniscoping,[status(thm)],[f10674])).
% 46.90/11.43 fof(f10676,plain,(
% 46.90/11.43 ![X0,X2]: ((![X1]: (~prop(X0,X1)|~state_adjective_state_binding(X1,X2)))|(((((in(sK49_skl(X2,X0),sK48_skl(X2,X0))&attr(sK48_skl(X2,X0),sK47_skl(X2,X0)))&loc(X0,sK49_skl(X2,X0)))&sub(sK48_skl(X2,X0),land_1_1))&sub(sK47_skl(X2,X0),name_1_1))&val(sK47_skl(X2,X0),X2)))),
% 46.90/11.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl]),skolemize(X4,sK47_skl(X2,X0)),skolemize(X3,sK48_skl(X2,X0)),skolemize(X5,sK49_skl(X2,X0))],[f10675])).
% 46.90/11.43 fof(f10679,plain,(
% 46.90/11.43 ![X0,X1,X2]: (~prop(X0,X1)|~state_adjective_state_binding(X1,X2)|loc(X0,sK49_skl(X2,X0)))),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10676])).
% 46.90/11.43 fof(f10801,plain,(
% 46.90/11.43 ![X0,X1]: (~loc(X0,X1)|(?[X2]: ((loc(X2,X1)&scar(X2,X0))&subs(X2,stehen_1_1))))),
% 46.90/11.43 inference(pre_NNF_transformation,[status(thm)],[f180])).
% 46.90/11.43 fof(f10802,plain,(
% 46.90/11.43 ![X0,X1]: (~loc(X0,X1)|((loc(sK62_skl(X1,X0),X1)&scar(sK62_skl(X1,X0),X0))&subs(sK62_skl(X1,X0),stehen_1_1)))),
% 46.90/11.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(X2,sK62_skl(X1,X0))],[f10801])).
% 46.90/11.43 fof(f10803,plain,(
% 46.90/11.43 ![X0,X1]: (~loc(X0,X1)|loc(sK62_skl(X1,X0),X1))),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10802])).
% 46.90/11.43 fof(f10804,plain,(
% 46.90/11.43 ![X0,X1]: (~loc(X0,X1)|scar(sK62_skl(X1,X0),X0))),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10802])).
% 46.90/11.43 fof(f10805,plain,(
% 46.90/11.43 ![X0,X1]: (~loc(X0,X1)|subs(sK62_skl(X1,X0),stehen_1_1))),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10802])).
% 46.90/11.43 fof(f19694,plain,(
% 46.90/11.43 state_adjective_state_binding(italienisch__1_1,italien_0)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f9067])).
% 46.90/11.43 fof(f20815,plain,(
% 46.90/11.43 (![X0,X1,X2,X3,X4]: (((((((~attr(X0,X1)|~loc(X4,X2))|~prop(X0,italienisch__1_1))|~scar(X4,X3))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1))|~subs(X4,stehen_1_1))|~val(X1,rom_0)))),
% 46.90/11.43 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 46.90/11.43 fof(f20816,plain,(
% 46.90/11.43 ![X1]: ((![X4]: ((![X0]: (((((~attr(X0,X1)|(![X2]: ~loc(X4,X2)))|~prop(X0,italienisch__1_1))|(![X3]: ~scar(X4,X3)))|~sub(X1,name_1_1))|~sub(X0,stadt__1_1)))|~subs(X4,stehen_1_1)))|~val(X1,rom_0))),
% 46.90/11.43 inference(miniscoping,[status(thm)],[f20815])).
% 46.90/11.43 fof(f20817,plain,(
% 46.90/11.43 ![X0,X1,X2,X3,X4]: (~attr(X0,X1)|~loc(X2,X3)|~prop(X0,italienisch__1_1)|~scar(X2,X4)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~subs(X2,stehen_1_1)|~val(X1,rom_0))),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f20816])).
% 46.90/11.43 fof(f20820,plain,(
% 46.90/11.43 attr(c67,c78)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.90/11.43 fof(f20821,plain,(
% 46.90/11.43 prop(c67,italienisch__1_1)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.90/11.43 fof(f20822,plain,(
% 46.90/11.43 sub(c67,stadt__1_1)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.90/11.43 fof(f20824,plain,(
% 46.90/11.43 sub(c78,name_1_1)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.90/11.43 fof(f20825,plain,(
% 46.90/11.43 val(c78,rom_0)),
% 46.90/11.43 inference(cnf_transformation,[status(thm)],[f10190])).
% 46.90/11.43 fof(f21019,definition,(
% 46.90/11.43 ![X0,X1]: (sQ0_spl <=> (~attr(X0,X1)|~prop(X0,italienisch__1_1)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~val(X1,rom_0)))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21020,plain,(
% 46.90/11.43 ![X0,X1]: (~attr(X0,X1)|~prop(X0,italienisch__1_1)|~sub(X1,name_1_1)|~sub(X0,stadt__1_1)|~val(X1,rom_0)|~sQ0_spl)),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21019])).
% 46.90/11.43 fof(f21022,definition,(
% 46.90/11.43 ![X2,X3,X4]: (sQ1_spl <=> (~loc(X2,X3)|~scar(X2,X4)|~subs(X2,stehen_1_1)))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21023,plain,(
% 46.90/11.43 ![X0,X1,X2]: (~loc(X0,X1)|~scar(X0,X2)|~subs(X0,stehen_1_1)|~sQ1_spl)),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21022])).
% 46.90/11.43 fof(f21025,plain,(
% 46.90/11.43 sQ0_spl|sQ1_spl),
% 46.90/11.43 inference(split_clause,[status(thm)],[f20817,f21019,f21022])).
% 46.90/11.43 fof(f21026,plain,(
% 46.90/11.43 ![X0]: (~attr(X0,c78)|~prop(X0,italienisch__1_1)|~sub(c78,name_1_1)|~sub(X0,stadt__1_1)|~sQ0_spl)),
% 46.90/11.43 inference(resolution,[status(thm)],[f20825,f21020])).
% 46.90/11.43 fof(f21027,definition,(
% 46.90/11.43 ![X0]: (sQ2_spl <=> (~attr(X0,c78)|~prop(X0,italienisch__1_1)|~sub(X0,stadt__1_1)))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21028,plain,(
% 46.90/11.43 ![X0]: (~attr(X0,c78)|~prop(X0,italienisch__1_1)|~sub(X0,stadt__1_1)|~sQ2_spl)),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21027])).
% 46.90/11.43 fof(f21030,definition,(
% 46.90/11.43 sQ3_spl <=> (sub(c78,name_1_1))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21032,plain,(
% 46.90/11.43 ~sub(c78,name_1_1)|sQ3_spl),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21030])).
% 46.90/11.43 fof(f21033,plain,(
% 46.90/11.43 sQ2_spl|~sQ3_spl|~sQ0_spl),
% 46.90/11.43 inference(split_clause,[status(thm)],[f21026,f21027,f21030,f21019])).
% 46.90/11.43 fof(f21038,plain,(
% 46.90/11.43 $false|sQ3_spl),
% 46.90/11.43 inference(forward_subsumption_resolution,[status(thm)],[f20824,f21032])).
% 46.90/11.43 fof(f21039,plain,(
% 46.90/11.43 sQ3_spl),
% 46.90/11.43 inference(contradiction_clause,[status(thm)],[f21038])).
% 46.90/11.43 fof(f21827,plain,(
% 46.90/11.43 ~prop(c67,italienisch__1_1)|~sub(c67,stadt__1_1)|~sQ2_spl),
% 46.90/11.43 inference(resolution,[status(thm)],[f21028,f20820])).
% 46.90/11.43 fof(f21828,definition,(
% 46.90/11.43 sQ4_spl <=> (prop(c67,italienisch__1_1))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21830,plain,(
% 46.90/11.43 ~prop(c67,italienisch__1_1)|sQ4_spl),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21828])).
% 46.90/11.43 fof(f21831,definition,(
% 46.90/11.43 sQ5_spl <=> (sub(c67,stadt__1_1))),
% 46.90/11.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 46.90/11.43 fof(f21833,plain,(
% 46.90/11.43 ~sub(c67,stadt__1_1)|sQ5_spl),
% 46.90/11.43 inference(component_clause,[status(thm)],[f21831])).
% 46.90/11.43 fof(f21834,plain,(
% 46.90/11.43 ~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 46.90/11.43 inference(split_clause,[status(thm)],[f21827,f21828,f21831,f21027])).
% 46.90/11.43 fof(f21835,plain,(
% 46.90/11.43 $false|sQ4_spl),
% 46.90/11.43 inference(forward_subsumption_resolution,[status(thm)],[f21830,f20821])).
% 46.90/11.43 fof(f21836,plain,(
% 46.90/11.43 sQ4_spl),
% 46.90/11.43 inference(contradiction_clause,[status(thm)],[f21835])).
% 46.90/11.43 fof(f21837,plain,(
% 46.90/11.43 $false|sQ5_spl),
% 46.90/11.43 inference(forward_subsumption_resolution,[status(thm)],[f21833,f20822])).
% 46.90/11.43 fof(f21838,plain,(
% 46.90/11.43 sQ5_spl),
% 46.90/11.43 inference(contradiction_clause,[status(thm)],[f21837])).
% 46.90/11.43 fof(f27380,plain,(
% 46.90/11.43 ![X0]: (~state_adjective_state_binding(italienisch__1_1,X0)|loc(c67,sK49_skl(X0,c67)))),
% 46.90/11.43 inference(resolution,[status(thm)],[f10679,f20821])).
% 46.90/11.43 fof(f27381,plain,(
% 46.90/11.43 loc(c67,sK49_skl(italien_0,c67))),
% 46.90/11.43 inference(resolution,[status(thm)],[f27380,f19694])).
% 46.90/11.43 fof(f27383,plain,(
% 46.90/11.43 scar(sK62_skl(sK49_skl(italien_0,c67),c67),c67)),
% 46.90/11.43 inference(resolution,[status(thm)],[f27381,f10804])).
% 46.90/11.43 fof(f27384,plain,(
% 46.90/11.43 loc(sK62_skl(sK49_skl(italien_0,c67),c67),sK49_skl(italien_0,c67))),
% 46.90/11.43 inference(resolution,[status(thm)],[f27381,f10803])).
% 46.90/11.43 fof(f27389,plain,(
% 46.90/11.43 subs(sK62_skl(sK49_skl(italien_0,c67),c67),stehen_1_1)),
% 46.90/11.43 inference(resolution,[status(thm)],[f27381,f10805])).
% 46.90/11.43 fof(f27430,plain,(
% 46.90/11.43 ![X0]: (~loc(sK62_skl(sK49_skl(italien_0,c67),c67),X0)|~subs(sK62_skl(sK49_skl(italien_0,c67),c67),stehen_1_1)|~sQ1_spl)),
% 46.90/11.43 inference(resolution,[status(thm)],[f27383,f21023])).
% 46.90/11.47 fof(f27431,definition,(
% 46.90/11.47 ![X0]: (sQ14_spl <=> (~loc(sK62_skl(sK49_skl(italien_0,c67),c67),X0)))),
% 46.90/11.47 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 46.90/11.47 fof(f27432,plain,(
% 46.90/11.47 ![X0]: (~loc(sK62_skl(sK49_skl(italien_0,c67),c67),X0)|~sQ14_spl)),
% 46.90/11.47 inference(component_clause,[status(thm)],[f27431])).
% 46.90/11.47 fof(f27434,definition,(
% 46.90/11.47 sQ15_spl <=> (subs(sK62_skl(sK49_skl(italien_0,c67),c67),stehen_1_1))),
% 46.90/11.47 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 46.90/11.47 fof(f27436,plain,(
% 46.90/11.47 ~subs(sK62_skl(sK49_skl(italien_0,c67),c67),stehen_1_1)|sQ15_spl),
% 46.90/11.47 inference(component_clause,[status(thm)],[f27434])).
% 46.90/11.47 fof(f27437,plain,(
% 46.90/11.47 sQ14_spl|~sQ15_spl|~sQ1_spl),
% 46.90/11.47 inference(split_clause,[status(thm)],[f27430,f27431,f27434,f21022])).
% 46.90/11.47 fof(f27446,plain,(
% 46.90/11.47 $false|~sQ14_spl),
% 46.90/11.47 inference(forward_subsumption_resolution,[status(thm)],[f27384,f27432])).
% 46.90/11.47 fof(f27447,plain,(
% 46.90/11.47 ~sQ14_spl),
% 46.90/11.47 inference(contradiction_clause,[status(thm)],[f27446])).
% 46.90/11.47 fof(f27665,plain,(
% 46.90/11.47 $false|sQ15_spl),
% 46.90/11.47 inference(forward_subsumption_resolution,[status(thm)],[f27389,f27436])).
% 46.90/11.47 fof(f27666,plain,(
% 46.90/11.47 sQ15_spl),
% 46.90/11.47 inference(contradiction_clause,[status(thm)],[f27665])).
% 46.90/11.47 fof(f27667,plain,(
% 46.90/11.47 $false),
% 46.90/11.47 inference(sat_refutation,[status(thm)],[f21025,f21033,f21039,f21834,f21836,f21838,f27437,f27447,f27666])).
% 46.90/11.47 % SZS output end CNFRefutation for theBenchmark.p
% 46.90/11.52 % Elapsed time: 6.147534 seconds
% 46.90/11.52 % CPU time: 47.344069 seconds
% 46.90/11.52 % Total memory used: 591.487 MB
% 46.90/11.52 % Net memory used: 574.883 MB
%------------------------------------------------------------------------------