%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR115+48 : 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 : n012.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:26 PM UTC 2026
% Result : Theorem 242.92s 31.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR115+48 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Mon Sep 21 15:06:36 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 242.92/31.05 % Refutation found
% 242.92/31.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 242.92/31.05 % SZS output start CNFRefutation for theBenchmark
% 242.92/31.05 fof(f20,axiom,(
% 242.92/31.05 (! [X0,X1] :( card(X0,X1)=> has_card_leq(X0,X1) ) )),
% 242.92/31.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 242.92/31.05 fof(f10188,conjecture,(
% 242.92/31.05 (? [X0,X1,X2,X3,X4,X5,X6,X7] :( agt(X4,X3)& attr(X0,X1)& attr(X3,X2)& attr(X5,X6)& has_card_leq(X7,int1994)& sub(X1,name_1_1)& sub(X0,firma_1_1)& sub(X2,name_1_1)& sub(X6,jahr__1_1)& temp(X4,X5)& val(X1,bmw_0)& val(X2,bmw_0)& val(X6,X7) ) )),
% 242.92/31.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 242.92/31.05 fof(f10189,negated_conjecture,(
% 242.92/31.05 ~((? [X0,X1,X2,X3,X4,X5,X6,X7] :( agt(X4,X3)& attr(X0,X1)& attr(X3,X2)& attr(X5,X6)& has_card_leq(X7,int1994)& sub(X1,name_1_1)& sub(X0,firma_1_1)& sub(X2,name_1_1)& sub(X6,jahr__1_1)& temp(X4,X5)& val(X1,bmw_0)& val(X2,bmw_0)& val(X6,X7) ) ))),
% 242.92/31.05 inference(negated_conjecture,[status(cth)],[f10188])).
% 242.92/31.05 fof(f10190,hypothesis,(
% 242.92/31.05 ( mcont(c417,c519)& mexp(c417,c419)& subs(c417,erw__344gen_1_1)& attr(c419,c420)& sub(c419,firma_1_1)& sub(c420,name_1_1)& val(c420,bmw_0)& attr(c506,c507)& sub(c506,firma_1_1)& sub(c507,name_1_1)& val(c507,rover_0)& attr(c517,c518)& sub(c518,jahr__1_1)& val(c518,c508)& agt(c519,c419)& obj(c519,c506)& subs(c519,festigen_1_1)& temp(c519,c517)& temp(c519,schon_1_1)& sort(c417,da)& fact(c417,real)& gener(c417,sp)& sort(c519,da)& fact(c519,hypo)& gener(c519,sp)& sort(c419,d)& sort(c419,io)& card(c419,int1)& etype(c419,int0)& fact(c419,real)& gener(c419,sp)& quant(c419,one)& refer(c419,det)& varia(c419,con)& sort(erw__344gen_1_1,da)& fact(erw__344gen_1_1,real)& gener(erw__344gen_1_1,ge)& sort(c420,na)& card(c420,int1)& etype(c420,int0)& fact(c420,real)& gener(c420,sp)& quant(c420,one)& refer(c420,indet)& varia(c420,varia_c)& sort(firma_1_1,d)& sort(firma_1_1,io)& card(firma_1_1,int1)& etype(firma_1_1,int0)& fact(firma_1_1,real)& gener(firma_1_1,ge)& quant(firma_1_1,one)& refer(firma_1_1,refer_c)& varia(firma_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(bmw_0,fe)& sort(c506,d)& sort(c506,io)& card(c506,int1)& etype(c506,int0)& fact(c506,real)& gener(c506,sp)& quant(c506,one)& refer(c506,det)& varia(c506,con)& sort(c507,na)& card(c507,int1)& etype(c507,int0)& fact(c507,real)& gener(c507,sp)& quant(c507,one)& refer(c507,indet)& varia(c507,varia_c)& sort(rover_0,fe)& sort(c517,t)& card(c517,int1)& etype(c517,int0)& fact(c517,real)& gener(c517,sp)& quant(c517,one)& refer(c517,det)& varia(c517,con)& sort(c518,me)& sort(c518,oa)& sort(c518,ta)& card(c518,card_c)& etype(c518,etype_c)& fact(c518,real)& gener(c518,sp)& quant(c518,quant_c)& refer(c518,refer_c)& varia(c518,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(c508,nu)& card(c508,int1994)& sort(festigen_1_1,da)& fact(festigen_1_1,real)& gener(festigen_1_1,ge)& sort(schon_1_1,t)& card(schon_1_1,int1)& etype(schon_1_1,int0)& fact(schon_1_1,real)& gener(schon_1_1,sp)& quant(schon_1_1,one)& refer(schon_1_1,refer_c)& varia(schon_1_1,varia_c) ) ),
% 242.92/31.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 242.92/31.05 fof(f10224,plain,(
% 242.92/31.05 ![X0,X1]: (~card(X0,X1)|has_card_leq(X0,X1))),
% 242.92/31.05 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 242.92/31.05 fof(f10225,plain,(
% 242.92/31.05 ![X0,X1]: (~card(X0,X1)|has_card_leq(X0,X1))),
% 242.92/31.05 inference(cnf_transformation,[status(thm)],[f10224])).
% 242.92/31.05 fof(f20815,plain,(
% 242.92/31.05 (![X0,X1,X2,X3,X4,X5,X6,X7]: ((((((((((((~agt(X4,X3)|~attr(X0,X1))|~attr(X3,X2))|~attr(X5,X6))|~has_card_leq(X7,int1994))|~sub(X1,name_1_1))|~sub(X0,firma_1_1))|~sub(X2,name_1_1))|~sub(X6,jahr__1_1))|~temp(X4,X5))|~val(X1,bmw_0))|~val(X2,bmw_0))|~val(X6,X7)))),
% 242.92/31.05 inference(pre_NNF_transformation,[status(thm)],[f10189])).
% 242.92/31.05 fof(f20816,plain,(
% 242.92/31.05 ![X6,X7]: ((![X2]: ((![X1]: ((![X4,X5]: ((((![X0]: (((((![X3]: ((~agt(X4,X3)|~attr(X0,X1))|~attr(X3,X2)))|~attr(X5,X6))|~has_card_leq(X7,int1994))|~sub(X1,name_1_1))|~sub(X0,firma_1_1)))|~sub(X2,name_1_1))|~sub(X6,jahr__1_1))|~temp(X4,X5)))|~val(X1,bmw_0)))|~val(X2,bmw_0)))|~val(X6,X7))),
% 242.92/31.13 inference(miniscoping,[status(thm)],[f20815])).
% 242.92/31.13 fof(f20817,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~agt(X0,X1)|~attr(X2,X3)|~attr(X1,X4)|~attr(X5,X6)|~has_card_leq(X7,int1994)|~sub(X3,name_1_1)|~sub(X2,firma_1_1)|~sub(X4,name_1_1)|~sub(X6,jahr__1_1)|~temp(X0,X5)|~val(X3,bmw_0)|~val(X4,bmw_0)|~val(X6,X7))),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f20816])).
% 242.92/31.13 fof(f20821,plain,(
% 242.92/31.13 attr(c419,c420)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20822,plain,(
% 242.92/31.13 sub(c419,firma_1_1)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20823,plain,(
% 242.92/31.13 sub(c420,name_1_1)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20824,plain,(
% 242.92/31.13 val(c420,bmw_0)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20829,plain,(
% 242.92/31.13 attr(c517,c518)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20830,plain,(
% 242.92/31.13 sub(c518,jahr__1_1)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20831,plain,(
% 242.92/31.13 val(c518,c508)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20832,plain,(
% 242.92/31.13 agt(c519,c419)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20835,plain,(
% 242.92/31.13 temp(c519,c517)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20928,plain,(
% 242.92/31.13 card(c508,int1994)),
% 242.92/31.13 inference(cnf_transformation,[status(thm)],[f10190])).
% 242.92/31.13 fof(f20992,plain,(
% 242.92/31.13 has_card_leq(c508,int1994)),
% 242.92/31.13 inference(resolution,[status(thm)],[f20928,f10225])).
% 242.92/31.13 fof(f144399,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4,X5]: (~agt(X0,X1)|~attr(X2,c420)|~attr(X1,c420)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X2,firma_1_1)|~sub(X4,jahr__1_1)|~temp(X0,X3)|~val(c420,bmw_0)|~val(c420,bmw_0)|~val(X4,X5))),
% 242.92/31.13 inference(resolution,[status(thm)],[f20823,f20817])).
% 242.92/31.13 fof(f144438,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4,X5]: (~agt(X0,X1)|~attr(X2,c420)|~attr(X1,c420)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X2,firma_1_1)|~sub(X4,jahr__1_1)|~temp(X0,X3)|~val(c420,bmw_0)|~val(X4,X5))),
% 242.92/31.13 inference(duplicate_literals_removal,[status(thm)],[f144399])).
% 242.92/31.13 fof(f144439,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4,X5]: (~agt(X0,X1)|~attr(X2,c420)|~attr(X1,c420)|~attr(X3,X4)|~has_card_leq(X5,int1994)|~sub(X2,firma_1_1)|~sub(X4,jahr__1_1)|~temp(X0,X3)|~val(X4,X5))),
% 242.92/31.13 inference(forward_subsumption_resolution,[status(thm)],[f144438,f20824])).
% 242.92/31.13 fof(f144573,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4]: (~agt(X0,X1)|~attr(X1,c420)|~attr(X2,X3)|~has_card_leq(X4,int1994)|~sub(c419,firma_1_1)|~sub(X3,jahr__1_1)|~temp(X0,X2)|~val(X3,X4))),
% 242.92/31.13 inference(resolution,[status(thm)],[f144439,f20821])).
% 242.92/31.13 fof(f144574,plain,(
% 242.92/31.13 ![X0,X1,X2,X3,X4]: (~agt(X0,X1)|~attr(X1,c420)|~attr(X2,X3)|~has_card_leq(X4,int1994)|~sub(X3,jahr__1_1)|~temp(X0,X2)|~val(X3,X4))),
% 242.92/31.13 inference(forward_subsumption_resolution,[status(thm)],[f144573,f20822])).
% 242.92/31.13 fof(f144591,plain,(
% 242.92/31.13 ![X0,X1,X2,X3]: (~agt(X0,c419)|~attr(X1,X2)|~has_card_leq(X3,int1994)|~sub(X2,jahr__1_1)|~temp(X0,X1)|~val(X2,X3))),
% 242.92/31.13 inference(resolution,[status(thm)],[f144574,f20821])).
% 242.92/31.13 fof(f144592,plain,(
% 242.92/31.13 ![X0,X1,X2]: (~agt(X0,c419)|~attr(X1,X2)|~sub(X2,jahr__1_1)|~temp(X0,X1)|~val(X2,c508))),
% 242.92/31.13 inference(resolution,[status(thm)],[f144591,f20992])).
% 242.92/31.13 fof(f144611,plain,(
% 242.92/31.13 ![X0,X1]: (~agt(X0,c419)|~attr(X1,c518)|~sub(c518,jahr__1_1)|~temp(X0,X1))),
% 242.92/31.13 inference(resolution,[status(thm)],[f144592,f20831])).
% 242.92/31.13 fof(f144612,plain,(
% 242.92/31.13 ![X0,X1]: (~agt(X0,c419)|~attr(X1,c518)|~temp(X0,X1))),
% 242.92/31.13 inference(forward_subsumption_resolution,[status(thm)],[f144611,f20830])).
% 242.92/31.13 fof(f144613,plain,(
% 242.92/31.13 ![X0]: (~agt(X0,c419)|~temp(X0,c517))),
% 242.92/31.13 inference(resolution,[status(thm)],[f144612,f20829])).
% 242.92/31.13 fof(f144631,plain,(
% 242.92/31.13 ~agt(c519,c419)),
% 242.92/31.13 inference(resolution,[status(thm)],[f144613,f20835])).
% 242.92/31.13 fof(f144632,plain,(
% 242.92/31.13 $false),
% 242.92/31.13 inference(forward_subsumption_resolution,[status(thm)],[f144631,f20832])).
% 242.92/31.13 % SZS output end CNFRefutation for theBenchmark.p
% 16.85/31.35 % Elapsed time: 31.035259 seconds
% 16.85/31.35 % CPU time: 244.291303 seconds
% 16.85/31.35 % Total memory used: 1.003 GB
% 16.85/31.35 % Net memory used: 944.896 MB
%------------------------------------------------------------------------------