%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET801+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 3.93s 0.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET801+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 05:39:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 3.93/0.94 % Refutation found
% 3.93/0.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.93/0.94 % SZS output start CNFRefutation for theBenchmark
% 3.93/0.94 fof(f14,axiom,(
% 3.93/0.94 (! [R,E,M] :( upper_bound(M,R,E)<=> (! [X] :( member(X,E)=> apply(R,X,M) ) )) )),
% 3.93/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.93/0.94 fof(f16,axiom,(
% 3.93/0.94 (! [R,E,M] :( greatest(M,R,E)<=> ( member(M,E)& (! [X] :( member(X,E)=> apply(R,X,M) ) )) ) )),
% 3.93/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.93/0.94 fof(f20,axiom,(
% 3.93/0.94 (! [A,X,R,E] :( least_upper_bound(A,X,R,E)<=> ( member(A,X)& upper_bound(A,R,X)& (! [M] :( ( member(M,E)& upper_bound(M,R,X) )=> apply(R,A,M) ) )) ) )),
% 3.93/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.93/0.94 fof(f22,conjecture,(
% 3.93/0.94 (! [R,E] :( order(R,E)=> (! [X] :( subset(X,E)=> (! [M] :( greatest(M,R,X)<=> ( member(M,X)& least_upper_bound(M,X,R,E) ) ) )) )) )),
% 3.93/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.93/0.94 fof(f23,negated_conjecture,(
% 3.93/0.94 ~((! [R,E] :( order(R,E)=> (! [X] :( subset(X,E)=> (! [M] :( greatest(M,R,X)<=> ( member(M,X)& least_upper_bound(M,X,R,E) ) ) )) )) ))),
% 3.93/0.94 inference(negated_conjecture,[status(cth)],[f22])).
% 3.93/0.94 fof(f102,plain,(
% 3.93/0.94 ![R,E,M]: (upper_bound(M,R,E)<=>(![X]: (~member(X,E)|apply(R,X,M))))),
% 3.93/0.94 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 3.93/0.94 fof(f103,plain,(
% 3.93/0.94 ![R,E,M]: ((~upper_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,X,M))))&(upper_bound(M,R,E)|(?[X]: (member(X,E)&~apply(R,X,M)))))),
% 3.93/0.94 inference(NNF_transformation,[status(thm)],[f102])).
% 3.93/0.94 fof(f104,plain,(
% 3.93/0.94 (![R,E,M]: (~upper_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,X,M)))))&(![R,E,M]: (upper_bound(M,R,E)|(?[X]: (member(X,E)&~apply(R,X,M)))))),
% 3.93/0.94 inference(miniscoping,[status(thm)],[f103])).
% 3.93/0.94 fof(f105,plain,(
% 3.93/0.94 (![R,E,M]: (~upper_bound(M,R,E)|(![X]: (~member(X,E)|apply(R,X,M)))))&(![R,E,M]: (upper_bound(M,R,E)|(member(sK8_skl(M,E,R),E)&~apply(R,sK8_skl(M,E,R),M))))),
% 3.93/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X,sK8_skl(M,E,R))],[f104])).
% 3.93/0.94 fof(f106,plain,(
% 3.93/0.94 ![X0,X1,X2,X3]: (~upper_bound(X0,X1,X2)|~member(X3,X2)|apply(X1,X3,X0))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f105])).
% 3.93/0.94 fof(f107,plain,(
% 3.93/0.94 ![X0,X1,X2]: (upper_bound(X0,X1,X2)|member(sK8_skl(X0,X2,X1),X2))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f105])).
% 3.93/0.94 fof(f108,plain,(
% 3.93/0.94 ![X0,X1,X2]: (upper_bound(X0,X1,X2)|~apply(X1,sK8_skl(X0,X2,X1),X0))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f105])).
% 3.93/0.94 fof(f116,plain,(
% 3.93/0.94 ![R,E,M]: (greatest(M,R,E)<=>(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M)))))),
% 3.93/0.94 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 3.93/0.94 fof(f117,plain,(
% 3.93/0.94 ![R,E,M]: ((~greatest(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M)))))&(greatest(M,R,E)|(~member(M,E)|(?[X]: (member(X,E)&~apply(R,X,M))))))),
% 3.93/0.94 inference(NNF_transformation,[status(thm)],[f116])).
% 3.93/0.94 fof(f118,plain,(
% 3.93/0.94 (![R,E,M]: (~greatest(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M))))))&(![R,E,M]: (greatest(M,R,E)|(~member(M,E)|(?[X]: (member(X,E)&~apply(R,X,M))))))),
% 3.93/0.94 inference(miniscoping,[status(thm)],[f117])).
% 3.93/0.94 fof(f119,plain,(
% 3.93/0.94 (![R,E,M]: (~greatest(M,R,E)|(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M))))))&(![R,E,M]: (greatest(M,R,E)|(~member(M,E)|(member(sK10_skl(M,E,R),E)&~apply(R,sK10_skl(M,E,R),M)))))),
% 3.93/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(M,E,R))],[f118])).
% 3.93/0.94 fof(f120,plain,(
% 3.93/0.94 ![X0,X1,X2]: (~greatest(X0,X1,X2)|member(X0,X2))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f119])).
% 3.93/0.94 fof(f121,plain,(
% 3.93/0.94 ![X0,X1,X2,X3]: (~greatest(X0,X1,X2)|~member(X3,X2)|apply(X1,X3,X0))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f119])).
% 3.93/0.94 fof(f122,plain,(
% 3.93/0.94 ![X0,X1,X2]: (greatest(X0,X1,X2)|~member(X0,X2)|member(sK10_skl(X0,X2,X1),X2))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f119])).
% 3.93/0.94 fof(f123,plain,(
% 3.93/0.94 ![X0,X1,X2]: (greatest(X0,X1,X2)|~member(X0,X2)|~apply(X1,sK10_skl(X0,X2,X1),X0))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f119])).
% 3.93/0.94 fof(f150,plain,(
% 3.93/0.94 ![A,X,R,E]: (least_upper_bound(A,X,R,E)<=>((member(A,X)&upper_bound(A,R,X))&(![M]: ((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M)))))),
% 3.93/0.94 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 3.93/0.94 fof(f151,plain,(
% 3.93/0.94 ![A,X,R,E]: ((~least_upper_bound(A,X,R,E)|((member(A,X)&upper_bound(A,R,X))&(![M]: ((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M)))))&(least_upper_bound(A,X,R,E)|((~member(A,X)|~upper_bound(A,R,X))|(?[M]: ((member(M,E)&upper_bound(M,R,X))&~apply(R,A,M))))))),
% 3.93/0.94 inference(NNF_transformation,[status(thm)],[f150])).
% 3.93/0.94 fof(f152,plain,(
% 3.93/0.94 (![A,X,R,E]: (~least_upper_bound(A,X,R,E)|((member(A,X)&upper_bound(A,R,X))&(![M]: ((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M))))))&(![A,X,R,E]: (least_upper_bound(A,X,R,E)|((~member(A,X)|~upper_bound(A,R,X))|(?[M]: ((member(M,E)&upper_bound(M,R,X))&~apply(R,A,M))))))),
% 3.93/0.94 inference(miniscoping,[status(thm)],[f151])).
% 3.93/0.94 fof(f153,plain,(
% 3.93/0.94 (![A,X,R,E]: (~least_upper_bound(A,X,R,E)|((member(A,X)&upper_bound(A,R,X))&(![M]: ((~member(M,E)|~upper_bound(M,R,X))|apply(R,A,M))))))&(![A,X,R,E]: (least_upper_bound(A,X,R,E)|((~member(A,X)|~upper_bound(A,R,X))|((member(sK14_skl(E,R,X,A),E)&upper_bound(sK14_skl(E,R,X,A),R,X))&~apply(R,A,sK14_skl(E,R,X,A))))))),
% 3.93/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(M,sK14_skl(E,R,X,A))],[f152])).
% 3.93/0.94 fof(f155,plain,(
% 3.93/0.94 ![X0,X1,X2,X3]: (~least_upper_bound(X0,X1,X2,X3)|upper_bound(X0,X2,X1))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f153])).
% 3.93/0.94 fof(f158,plain,(
% 3.93/0.94 ![X0,X1,X2,X3]: (least_upper_bound(X0,X1,X2,X3)|~member(X0,X1)|~upper_bound(X0,X2,X1)|upper_bound(sK14_skl(X3,X2,X1,X0),X2,X1))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f153])).
% 3.93/0.94 fof(f159,plain,(
% 3.93/0.94 ![X0,X1,X2,X3]: (least_upper_bound(X0,X1,X2,X3)|~member(X0,X1)|~upper_bound(X0,X2,X1)|~apply(X2,X0,sK14_skl(X3,X2,X1,X0)))),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f153])).
% 3.93/0.94 fof(f170,plain,(
% 3.93/0.94 (?[R,E]: (order(R,E)&(?[X]: (subset(X,E)&(?[M]: (greatest(M,R,X)<~>(member(M,X)&least_upper_bound(M,X,R,E))))))))),
% 3.93/0.94 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 3.93/0.94 fof(f171,plain,(
% 3.93/0.94 ?[R,E]: (order(R,E)&(?[X]: (subset(X,E)&(?[M]: ((greatest(M,R,X)|(member(M,X)&least_upper_bound(M,X,R,E)))&(~greatest(M,R,X)|(~member(M,X)|~least_upper_bound(M,X,R,E))))))))),
% 3.93/0.94 inference(NNF_transformation,[status(thm)],[f170])).
% 3.93/0.94 fof(f172,plain,(
% 3.93/0.94 (order(sK16_skl,sK17_skl)&(subset(sK18_skl,sK17_skl)&((greatest(sK19_skl,sK16_skl,sK18_skl)|(member(sK19_skl,sK18_skl)&least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)))&(~greatest(sK19_skl,sK16_skl,sK18_skl)|(~member(sK19_skl,sK18_skl)|~least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl))))))),
% 3.93/0.94 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])).
% 3.93/0.94 fof(f175,plain,(
% 3.93/0.94 greatest(sK19_skl,sK16_skl,sK18_skl)|member(sK19_skl,sK18_skl)),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f172])).
% 3.93/0.94 fof(f176,plain,(
% 3.93/0.94 greatest(sK19_skl,sK16_skl,sK18_skl)|least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f172])).
% 3.93/0.94 fof(f177,plain,(
% 3.93/0.94 ~greatest(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)|~least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 3.93/0.94 inference(cnf_transformation,[status(thm)],[f172])).
% 3.93/0.94 fof(f198,plain,(
% 3.93/0.94 member(sK19_skl,sK18_skl)),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f175,f120])).
% 3.93/0.94 fof(f199,plain,(
% 3.93/0.94 ~greatest(sK19_skl,sK16_skl,sK18_skl)|~least_upper_bound(sK19_skl,sK18_skl,sK16_skl,sK17_skl)),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f177,f198])).
% 3.93/0.94 fof(f202,plain,(
% 3.93/0.94 upper_bound(sK19_skl,sK16_skl,sK18_skl)|greatest(sK19_skl,sK16_skl,sK18_skl)),
% 3.93/0.94 inference(resolution,[status(thm)],[f155,f176])).
% 3.93/0.94 fof(f204,plain,(
% 3.93/0.94 ![X0]: (upper_bound(sK19_skl,sK16_skl,sK18_skl)|~member(X0,sK18_skl)|apply(sK16_skl,X0,sK19_skl))),
% 3.93/0.94 inference(resolution,[status(thm)],[f202,f121])).
% 3.93/0.94 fof(f206,plain,(
% 3.93/0.94 ![X0]: (~member(X0,sK18_skl)|apply(sK16_skl,X0,sK19_skl))),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f204,f106])).
% 3.93/0.94 fof(f392,plain,(
% 3.93/0.94 ![X0]: (upper_bound(sK19_skl,sK16_skl,X0)|~member(sK8_skl(sK19_skl,X0,sK16_skl),sK18_skl))),
% 3.93/0.94 inference(resolution,[status(thm)],[f108,f206])).
% 3.93/0.94 fof(f394,plain,(
% 3.93/0.94 upper_bound(sK19_skl,sK16_skl,sK18_skl)|upper_bound(sK19_skl,sK16_skl,sK18_skl)),
% 3.93/0.94 inference(resolution,[status(thm)],[f392,f107])).
% 3.93/0.94 fof(f396,plain,(
% 3.93/0.94 upper_bound(sK19_skl,sK16_skl,sK18_skl)),
% 3.93/0.94 inference(duplicate_literals_removal,[status(thm)],[f394])).
% 3.93/0.94 fof(f397,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|~apply(sK16_skl,sK19_skl,sK14_skl(X0,sK16_skl,sK18_skl,sK19_skl)))),
% 3.93/0.94 inference(resolution,[status(thm)],[f396,f159])).
% 3.93/0.94 fof(f398,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|upper_bound(sK14_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK16_skl,sK18_skl))),
% 3.93/0.94 inference(resolution,[status(thm)],[f396,f158])).
% 3.93/0.94 fof(f401,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~apply(sK16_skl,sK19_skl,sK14_skl(X0,sK16_skl,sK18_skl,sK19_skl)))),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f397,f198])).
% 3.93/0.94 fof(f402,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|upper_bound(sK14_skl(X0,sK16_skl,sK18_skl,sK19_skl),sK16_skl,sK18_skl))),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f398,f198])).
% 3.93/0.94 fof(f406,plain,(
% 3.93/0.94 ![X0,X1]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(X1,sK18_skl)|apply(sK16_skl,X1,sK14_skl(X0,sK16_skl,sK18_skl,sK19_skl)))),
% 3.93/0.94 inference(resolution,[status(thm)],[f402,f106])).
% 3.93/0.94 fof(f408,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl)|least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0))),
% 3.93/0.94 inference(resolution,[status(thm)],[f406,f401])).
% 3.93/0.94 fof(f410,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0)|~member(sK19_skl,sK18_skl))),
% 3.93/0.94 inference(duplicate_literals_removal,[status(thm)],[f408])).
% 3.93/0.94 fof(f411,plain,(
% 3.93/0.94 ~greatest(sK19_skl,sK16_skl,sK18_skl)),
% 3.93/0.94 inference(backward_subsumption_resolution,[status(thm)],[f199,f412])).
% 3.93/0.94 fof(f412,plain,(
% 3.93/0.94 ![X0]: (least_upper_bound(sK19_skl,sK18_skl,sK16_skl,X0))),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f410,f198])).
% 3.93/0.94 fof(f895,plain,(
% 3.93/0.94 ![X0]: (greatest(sK19_skl,sK16_skl,X0)|~member(sK19_skl,X0)|~member(sK10_skl(sK19_skl,X0,sK16_skl),sK18_skl))),
% 3.93/0.94 inference(resolution,[status(thm)],[f123,f206])).
% 3.93/0.94 fof(f897,plain,(
% 3.93/0.94 greatest(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)|greatest(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)),
% 3.93/0.94 inference(resolution,[status(thm)],[f895,f122])).
% 3.93/0.94 fof(f902,plain,(
% 3.93/0.94 greatest(sK19_skl,sK16_skl,sK18_skl)|~member(sK19_skl,sK18_skl)),
% 3.93/0.94 inference(duplicate_literals_removal,[status(thm)],[f897])).
% 3.93/0.94 fof(f904,plain,(
% 3.93/0.94 ~member(sK19_skl,sK18_skl)),
% 3.93/0.94 inference(forward_subsumption_resolution,[status(thm)],[f902,f411])).
% 3.93/0.94 fof(f905,plain,(
% 3.93/0.94 $false),
% 3.93/0.94 inference(backward_subsumption_resolution,[status(thm)],[f198,f904])).
% 3.93/0.94 % SZS output end CNFRefutation for theBenchmark.p
% 3.93/0.96 % Elapsed time: 0.573135 seconds
% 3.93/0.96 % CPU time: 4.241413 seconds
% 3.93/0.96 % Total memory used: 138.459 MB
% 3.93/0.96 % Net memory used: 132.284 MB
%------------------------------------------------------------------------------