%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET802+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 02:12:37 PM UTC 2026
% Result : Theorem 0.12s 6.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET802+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n015.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 05:42:11 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.12/6.06 % Refutation found
% 0.12/6.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/6.06 % SZS output start CNFRefutation for theBenchmark
% 0.12/6.06 fof(f15,axiom,(
% 0.12/6.06 (! [R,E,M] :( lower_bound(M,R,E)<=> (! [X] :( member(X,E)=> apply(R,M,X) ) )) )),
% 0.12/6.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/6.06 fof(f17,axiom,(
% 0.12/6.06 (! [R,E,M] :( least(M,R,E)<=> ( member(M,E)& (! [X] :( member(X,E)=> apply(R,M,X) ) )) ) )),
% 0.12/6.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/6.06 fof(f21,axiom,(
% 0.12/6.06 (! [A,X,R,E] :( greatest_lower_bound(A,X,R,E)<=> ( member(A,X)& lower_bound(A,R,X)& (! [M] :( ( member(M,E)& lower_bound(M,R,X) )=> apply(R,M,A) ) )) ) )),
% 0.12/6.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/6.06 fof(f22,conjecture,(
% 0.12/6.06 (! [R,E] :( order(R,E)=> (! [X] :( subset(X,E)=> (! [M] :( least(M,R,X)<=> ( member(M,X)& greatest_lower_bound(M,X,R,E) ) ) )) )) )),
% 0.12/6.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/6.06 fof(f23,negated_conjecture,(
% 0.12/6.06 ~((! [R,E] :( order(R,E)=> (! [X] :( subset(X,E)=> (! [M] :( least(M,R,X)<=> ( member(M,X)& greatest_lower_bound(M,X,R,E) ) ) )) )) ))),
% 0.12/6.06 inference(negated_conjecture,[status(cth)],[f22])).
% 0.12/6.06 fof(f109,plain,(
% 0.12/6.06 ![R,E,M]: (lower_bound(M,R,E)<=>(![X]: (~member(X,E)|apply(R,M,X))))),
% 0.12/6.06 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.12/6.06 fof(f110,plain,(
% 0.12/6.06 ![R,E,M]: ((~lower_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,M,X))))&(lower_bound(M,R,E)|(?[X]: (member(X,E)&~apply(R,M,X)))))),
% 0.12/6.06 inference(NNF_transformation,[status(thm)],[f109])).
% 0.12/6.06 fof(f111,plain,(
% 0.12/6.06 (![R,E,M]: (~lower_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,M,X)))))&(![R,E,M]: (lower_bound(M,R,E)|(?[X]: (member(X,E)&~apply(R,M,X)))))),
% 0.12/6.06 inference(miniscoping,[status(thm)],[f110])).
% 0.12/6.06 fof(f112,plain,(
% 0.12/6.06 (![R,E,M]: (~lower_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,M,X)))))&(![R,E,M]: (lower_bound(M,R,E)|(member(sK9_skl(M,E,R),E)&~apply(R,M,sK9_skl(M,E,R)))))),
% 0.12/6.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(M,E,R))],[f111])).
% 0.12/6.06 fof(f113,plain,(
% 0.12/6.06 ![X0,X1,X2,X3]: (~lower_bound(X0,X1,X2)|~member(X3,X2)|apply(X1,X0,X3))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f112])).
% 0.12/6.06 fof(f114,plain,(
% 0.12/6.06 ![X0,X1,X2]: (lower_bound(X0,X1,X2)|member(sK9_skl(X0,X2,X1),X2))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f112])).
% 0.12/6.06 fof(f115,plain,(
% 0.12/6.06 ![X0,X1,X2]: (lower_bound(X0,X1,X2)|~apply(X1,X0,sK9_skl(X0,X2,X1)))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f112])).
% 0.12/6.06 fof(f124,plain,(
% 0.12/6.06 ![R,E,M]: (least(M,R,E)<=>(member(M,E)&(![X]: (~member(X,E)|apply(R,M,X)))))),
% 0.12/6.06 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/6.06 fof(f125,plain,(
% 0.12/6.06 ![R,E,M]: ((~least(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,M,X)))))&(least(M,R,E)|(~member(M,E)|(?[X]: (member(X,E)&~apply(R,M,X))))))),
% 0.12/6.06 inference(NNF_transformation,[status(thm)],[f124])).
% 0.12/6.06 fof(f126,plain,(
% 0.12/6.06 (![R,E,M]: (~least(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,M,X))))))&(![R,E,M]: (least(M,R,E)|(~member(M,E)|(?[X]: (member(X,E)&~apply(R,M,X))))))),
% 0.12/6.06 inference(miniscoping,[status(thm)],[f125])).
% 0.12/6.06 fof(f127,plain,(
% 0.12/6.06 (![R,E,M]: (~least(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,M,X))))))&(![R,E,M]: (least(M,R,E)|(~member(M,E)|(member(sK11_skl(M,E,R),E)&~apply(R,M,sK11_skl(M,E,R))))))),
% 0.12/6.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X,sK11_skl(M,E,R))],[f126])).
% 0.12/6.06 fof(f128,plain,(
% 0.12/6.06 ![X0,X1,X2]: (~least(X0,X1,X2)|member(X0,X2))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/6.06 fof(f129,plain,(
% 0.12/6.06 ![X0,X1,X2,X3]: (~least(X0,X1,X2)|~member(X3,X2)|apply(X1,X0,X3))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/6.06 fof(f130,plain,(
% 0.12/6.06 ![X0,X1,X2]: (least(X0,X1,X2)|~member(X0,X2)|member(sK11_skl(X0,X2,X1),X2))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/6.06 fof(f131,plain,(
% 0.12/6.06 ![X0,X1,X2]: (least(X0,X1,X2)|~member(X0,X2)|~apply(X1,X0,sK11_skl(X0,X2,X1)))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/6.06 fof(f160,plain,(
% 0.12/6.06 ![A,X,R,E]: (greatest_lower_bound(A,X,R,E)<=>((member(A,X)&lower_bound(A,R,X))&(![M]: ((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A)))))),
% 0.12/6.06 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.12/6.06 fof(f161,plain,(
% 0.12/6.06 ![A,X,R,E]: ((~greatest_lower_bound(A,X,R,E)|((member(A,X)&lower_bound(A,R,X))&(![M]: ((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A)))))&(greatest_lower_bound(A,X,R,E)|((~member(A,X)|~lower_bound(A,R,X))|(?[M]: ((member(M,E)&lower_bound(M,R,X))&~apply(R,M,A))))))),
% 0.12/6.06 inference(NNF_transformation,[status(thm)],[f160])).
% 0.12/6.06 fof(f162,plain,(
% 0.12/6.06 (![A,X,R,E]: (~greatest_lower_bound(A,X,R,E)|((member(A,X)&lower_bound(A,R,X))&(![M]: ((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A))))))&(![A,X,R,E]: (greatest_lower_bound(A,X,R,E)|((~member(A,X)|~lower_bound(A,R,X))|(?[M]: ((member(M,E)&lower_bound(M,R,X))&~apply(R,M,A))))))),
% 0.12/6.06 inference(miniscoping,[status(thm)],[f161])).
% 0.12/6.06 fof(f163,plain,(
% 0.12/6.06 (![A,X,R,E]: (~greatest_lower_bound(A,X,R,E)|((member(A,X)&lower_bound(A,R,X))&(![M]: ((~member(M,E)|~lower_bound(M,R,X))|apply(R,M,A))))))&(![A,X,R,E]: (greatest_lower_bound(A,X,R,E)|((~member(A,X)|~lower_bound(A,R,X))|((member(sK15_skl(E,R,X,A),E)&lower_bound(sK15_skl(E,R,X,A),R,X))&~apply(R,sK15_skl(E,R,X,A),A)))))),
% 0.12/6.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(M,sK15_skl(E,R,X,A))],[f162])).
% 0.12/6.06 fof(f165,plain,(
% 0.12/6.06 ![X0,X1,X2,X3]: (~greatest_lower_bound(X0,X1,X2,X3)|lower_bound(X0,X2,X1))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f163])).
% 0.12/6.06 fof(f168,plain,(
% 0.12/6.06 ![X0,X1,X2,X3]: (greatest_lower_bound(X0,X1,X2,X3)|~member(X0,X1)|~lower_bound(X0,X2,X1)|lower_bound(sK15_skl(X3,X2,X1,X0),X2,X1))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f163])).
% 0.12/6.06 fof(f169,plain,(
% 0.12/6.06 ![X0,X1,X2,X3]: (greatest_lower_bound(X0,X1,X2,X3)|~member(X0,X1)|~lower_bound(X0,X2,X1)|~apply(X2,sK15_skl(X3,X2,X1,X0),X0))),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f163])).
% 0.12/6.06 fof(f170,plain,(
% 0.12/6.06 (?[R,E]: (order(R,E)&(?[X]: (subset(X,E)&(?[M]: (least(M,R,X)<~>(member(M,X)&greatest_lower_bound(M,X,R,E))))))))),
% 0.12/6.06 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.12/6.06 fof(f171,plain,(
% 0.12/6.06 ?[R,E]: (order(R,E)&(?[X]: (subset(X,E)&(?[M]: ((least(M,R,X)|(member(M,X)&greatest_lower_bound(M,X,R,E)))&(~least(M,R,X)|(~member(M,X)|~greatest_lower_bound(M,X,R,E))))))))),
% 0.12/6.06 inference(NNF_transformation,[status(thm)],[f170])).
% 0.12/6.06 fof(f172,plain,(
% 0.12/6.06 (order(sK16_skl,sK17_skl)&(subset(sK18_skl,sK17_skl)&((least(sK19_skl,sK16_skl,sK18_skl)|(member(sK19_skl,sK18_skl)&greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)))&(~least(sK19_skl,sK16_skl,sK18_skl)|(~member(sK19_skl,sK18_skl)|~greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl))))))),
% 0.12/6.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(R,sK16_skl),skolemize(E,sK17_skl),skolemize(X,sK18_skl),skolemize(M,sK19_skl)],[f171])).
% 0.12/6.06 fof(f175,plain,(
% 0.12/6.06 least(sK19_skl,sK16_skl,sK18_skl)|member(sK19_skl,sK18_skl)),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f172])).
% 0.12/6.06 fof(f176,plain,(
% 0.12/6.06 least(sK19_skl,sK16_skl,sK18_skl)|greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f172])).
% 0.12/6.06 fof(f177,plain,(
% 0.12/6.06 ~least(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)|~greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 0.12/6.06 inference(cnf_transformation,[status(thm)],[f172])).
% 0.12/6.06 fof(f198,plain,(
% 0.12/6.06 member(sK19_skl,sK18_skl)),
% 0.12/6.06 inference(forward_subsumption_resolution,[status(thm)],[f175,f128])).
% 0.12/6.06 fof(f199,plain,(
% 0.12/6.06 ~least(sK19_skl,sK16_skl,sK18_skl)|~greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 0.12/6.06 inference(forward_subsumption_resolution,[status(thm)],[f177,f198])).
% 0.12/6.06 fof(f202,plain,(
% 0.12/6.06 lower_bound(sK19_skl,sK16_skl,sK18_skl)|least(sK19_skl,sK16_skl,sK18_skl)),
% 0.12/6.06 inference(resolution,[status(thm)],[f165,f176])).
% 0.12/6.06 fof(f204,plain,(
% 0.12/6.06 ![X0]: (lower_bound(sK19_skl,sK16_skl,sK18_skl)|~member(X0,sK18_skl)|apply(sK16_skl,sK19_skl,X0))),
% 0.12/6.06 inference(resolution,[status(thm)],[f202,f129])).
% 0.12/6.06 fof(f206,plain,(
% 0.12/6.06 ![X0]: (~member(X0,sK18_skl)|apply(sK16_skl,sK19_skl,X0))),
% 0.12/6.06 inference(forward_subsumption_resolution,[status(thm)],[f204,f113])).
% 0.12/6.06 fof(f326,plain,(
% 0.12/6.06 ![X0]: (lower_bound(sK19_skl,sK16_skl,X0)|~member(sK9_skl(sK19_skl,X0,sK16_skl),sK18_skl))),
% 0.12/6.06 inference(resolution,[status(thm)],[f115,f206])).
% 0.12/6.08 fof(f330,plain,(
% 0.12/6.08 lower_bound(sK19_skl,sK16_skl,sK18_skl)|lower_bound(sK19_skl,sK16_skl,sK18_skl)),
% 0.12/6.08 inference(resolution,[status(thm)],[f326,f114])).
% 0.12/6.08 fof(f332,plain,(
% 0.12/6.08 lower_bound(sK19_skl,sK16_skl,sK18_skl)),
% 0.12/6.08 inference(duplicate_literals_removal,[status(thm)],[f330])).
% 0.12/6.08 fof(f338,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|~apply(sK16_skl,sK15_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK19_skl))),
% 0.12/6.08 inference(resolution,[status(thm)],[f332,f169])).
% 0.12/6.08 fof(f339,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|lower_bound(sK15_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK16_skl,sK18_skl))),
% 0.12/6.08 inference(resolution,[status(thm)],[f332,f168])).
% 0.12/6.08 fof(f342,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~apply(sK16_skl,sK15_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK19_skl))),
% 0.12/6.08 inference(forward_subsumption_resolution,[status(thm)],[f338,f198])).
% 0.12/6.08 fof(f343,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|lower_bound(sK15_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK16_skl,sK18_skl))),
% 0.12/6.08 inference(forward_subsumption_resolution,[status(thm)],[f339,f198])).
% 0.12/6.08 fof(f351,plain,(
% 0.12/6.08 ![X0,X1]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(X1,sK18_skl)|apply(sK16_skl,sK15_skl(X0,sK16_skl,sK18_skl,sK19_skl),X1))),
% 0.12/6.08 inference(resolution,[status(thm)],[f343,f113])).
% 0.12/6.08 fof(f360,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0))),
% 0.12/6.08 inference(resolution,[status(thm)],[f351,f342])).
% 0.12/6.08 fof(f362,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl))),
% 0.12/6.08 inference(duplicate_literals_removal,[status(thm)],[f360])).
% 0.12/6.08 fof(f363,plain,(
% 0.12/6.08 ~least(sK19_skl,sK16_skl,sK18_skl)),
% 0.12/6.08 inference(backward_subsumption_resolution,[status(thm)],[f199,f365])).
% 0.12/6.08 fof(f365,plain,(
% 0.12/6.08 ![X0]: (greatest_lower_bound(sK19_skl,sK18_skl,sK16_skl,X0))),
% 0.12/6.08 inference(forward_subsumption_resolution,[status(thm)],[f362,f198])).
% 0.12/6.08 fof(f1044,plain,(
% 0.12/6.08 ![X0]: (least(sK19_skl,sK16_skl,X0)|~member(sK19_skl,X0)|~member(sK11_skl(sK19_skl,X0,sK16_skl),sK18_skl))),
% 0.12/6.08 inference(resolution,[status(thm)],[f131,f206])).
% 0.12/6.08 fof(f1048,plain,(
% 0.12/6.08 least(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)|least(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)),
% 0.12/6.08 inference(resolution,[status(thm)],[f1044,f130])).
% 0.12/6.08 fof(f1050,plain,(
% 0.12/6.08 least(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)),
% 0.12/6.08 inference(duplicate_literals_removal,[status(thm)],[f1048])).
% 0.12/6.08 fof(f1052,plain,(
% 0.12/6.08 ~member(sK19_skl,sK18_skl)),
% 0.12/6.08 inference(forward_subsumption_resolution,[status(thm)],[f1050,f363])).
% 0.12/6.08 fof(f1053,plain,(
% 0.12/6.08 $false),
% 0.12/6.08 inference(backward_subsumption_resolution,[status(thm)],[f198,f1052])).
% 0.12/6.08 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/6.08 % Elapsed time: 0.708034 seconds
% 0.12/6.08 % CPU time: 5.331585 seconds
% 0.12/6.08 % Total memory used: 146.733 MB
% 0.12/6.08 % Net memory used: 139.371 MB
%------------------------------------------------------------------------------