%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET793+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 : n008.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:36 PM UTC 2026
% Result : Theorem 0.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET793+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/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:39:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f2,axiom,(
% 0.12/0.43 (! [R,E] :( total_order(R,E)<=> ( order(R,E)& (! [X,Y] :( ( member(X,E)& member(Y,E) )=> ( apply(R,X,Y)| apply(R,Y,X) ) ) )) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f5,axiom,(
% 0.12/0.43 (! [R,E,M] :( greatest(M,R,E)<=> ( member(M,E)& (! [X] :( member(X,E)=> apply(R,X,M) ) )) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f7,axiom,(
% 0.12/0.43 (! [R,E,M] :( max(M,R,E)<=> ( member(M,E)& (! [X] :( ( member(X,E)& apply(R,M,X) )=> M = X ) )) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f11,conjecture,(
% 0.12/0.43 (! [R,E,M] :( ( total_order(R,E)& max(M,R,E) )=> greatest(M,R,E) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f12,negated_conjecture,(
% 0.12/0.43 ~((! [R,E,M] :( ( total_order(R,E)& max(M,R,E) )=> greatest(M,R,E) ) ))),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f11])).
% 0.12/0.43 fof(f27,plain,(
% 0.12/0.43 ![R,E]: (total_order(R,E)<=>(order(R,E)&(![X,Y]: ((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X))))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.43 fof(f28,plain,(
% 0.12/0.43 ![R,E]: ((~total_order(R,E)|(order(R,E)&(![X,Y]: ((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X))))))&(total_order(R,E)|(~order(R,E)|(?[X,Y]: ((member(X,E)&member(Y,E))&(~apply(R,X,Y)&~apply(R,Y,X)))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f27])).
% 0.12/0.43 fof(f29,plain,(
% 0.12/0.43 (![R,E]: (~total_order(R,E)|(order(R,E)&(![X,Y]: ((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X)))))))&(![R,E]: (total_order(R,E)|(~order(R,E)|(?[X,Y]: ((member(X,E)&member(Y,E))&(~apply(R,X,Y)&~apply(R,Y,X)))))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f28])).
% 0.12/0.43 fof(f30,plain,(
% 0.12/0.43 (![R,E]: (~total_order(R,E)|(order(R,E)&(![X,Y]: ((~member(X,E)|~member(Y,E))|(apply(R,X,Y)|apply(R,Y,X)))))))&(![R,E]: (total_order(R,E)|(~order(R,E)|((member(sK3_skl(E,R),E)&member(sK4_skl(E,R),E))&(~apply(R,sK3_skl(E,R),sK4_skl(E,R))&~apply(R,sK4_skl(E,R),sK3_skl(E,R)))))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(X,sK3_skl(E,R)),skolemize(Y,sK4_skl(E,R))],[f29])).
% 0.12/0.43 fof(f32,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~total_order(X0,X1)|~member(X2,X1)|~member(X3,X1)|apply(X0,X2,X3)|apply(X0,X3,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f30])).
% 0.12/0.43 fof(f51,plain,(
% 0.12/0.43 ![R,E,M]: (greatest(M,R,E)<=>(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M)))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.12/0.43 fof(f52,plain,(
% 0.12/0.43 ![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))))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f51])).
% 0.12/0.43 fof(f53,plain,(
% 0.12/0.43 (![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))))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f52])).
% 0.12/0.43 fof(f54,plain,(
% 0.12/0.43 (![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(sK7_skl(M,E,R),E)&~apply(R,sK7_skl(M,E,R),M)))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X,sK7_skl(M,E,R))],[f53])).
% 0.12/0.43 fof(f57,plain,(
% 0.12/0.43 ![X0,X1,X2]: (greatest(X0,X1,X2)|~member(X0,X2)|member(sK7_skl(X0,X2,X1),X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f54])).
% 0.12/0.43 fof(f58,plain,(
% 0.12/0.43 ![X0,X1,X2]: (greatest(X0,X1,X2)|~member(X0,X2)|~apply(X1,sK7_skl(X0,X2,X1),X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f54])).
% 0.12/0.43 fof(f67,plain,(
% 0.12/0.43 ![R,E,M]: (max(M,R,E)<=>(member(M,E)&(![X]: ((~member(X,E)|~apply(R,M,X))|M=X))))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.43 fof(f68,plain,(
% 0.12/0.43 ![R,E,M]: ((~max(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,M,X))|M=X))))&(max(M,R,E)|(~member(M,E)|(?[X]: ((member(X,E)&apply(R,M,X))&~M=X)))))),
% 0.12/0.43 inference(NNF_transformation,[status(thm)],[f67])).
% 0.12/0.43 fof(f69,plain,(
% 0.12/0.43 (![R,E,M]: (~max(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,M,X))|M=X)))))&(![R,E,M]: (max(M,R,E)|(~member(M,E)|(?[X]: ((member(X,E)&apply(R,M,X))&~M=X)))))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f68])).
% 0.12/0.43 fof(f70,plain,(
% 0.12/0.43 (![R,E,M]: (~max(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,M,X))|M=X)))))&(![R,E,M]: (max(M,R,E)|(~member(M,E)|((member(sK9_skl(M,E,R),E)&apply(R,M,sK9_skl(M,E,R)))&~M=sK9_skl(M,E,R)))))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(M,E,R))],[f69])).
% 0.12/0.43 fof(f71,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~max(X0,X1,X2)|member(X0,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.43 fof(f72,plain,(
% 0.12/0.43 ![X0,X1,X2,X3]: (~max(X0,X1,X2)|~member(X3,X2)|~apply(X1,X0,X3)|X0=X3)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.43 fof(f105,plain,(
% 0.12/0.43 (?[R,E,M]: ((total_order(R,E)&max(M,R,E))&~greatest(M,R,E)))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.12/0.43 fof(f106,plain,(
% 0.12/0.43 ((total_order(sK13_skl,sK14_skl)&max(sK15_skl,sK13_skl,sK14_skl))&~greatest(sK15_skl,sK13_skl,sK14_skl))),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(R,sK13_skl),skolemize(E,sK14_skl),skolemize(M,sK15_skl)],[f105])).
% 0.12/0.43 fof(f107,plain,(
% 0.12/0.43 total_order(sK13_skl,sK14_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f106])).
% 0.12/0.43 fof(f108,plain,(
% 0.12/0.43 max(sK15_skl,sK13_skl,sK14_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f106])).
% 0.12/0.43 fof(f109,plain,(
% 0.12/0.43 ~greatest(sK15_skl,sK13_skl,sK14_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f106])).
% 0.12/0.43 fof(f132,plain,(
% 0.12/0.43 member(sK15_skl,sK14_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f71,f108])).
% 0.12/0.43 fof(f137,plain,(
% 0.12/0.43 ![X0,X1]: (~total_order(X0,sK14_skl)|~member(X1,sK14_skl)|apply(X0,X1,sK15_skl)|apply(X0,sK15_skl,X1))),
% 0.12/0.43 inference(resolution,[status(thm)],[f132,f32])).
% 0.12/0.43 fof(f141,plain,(
% 0.12/0.43 ![X0]: (~member(X0,sK14_skl)|apply(sK13_skl,X0,sK15_skl)|apply(sK13_skl,sK15_skl,X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f137,f107])).
% 0.12/0.43 fof(f142,plain,(
% 0.12/0.43 apply(sK13_skl,sK15_skl,sK15_skl)|apply(sK13_skl,sK15_skl,sK15_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f141,f132])).
% 0.12/0.43 fof(f143,plain,(
% 0.12/0.43 apply(sK13_skl,sK15_skl,sK15_skl)),
% 0.12/0.43 inference(duplicate_literals_removal,[status(thm)],[f142])).
% 0.12/0.43 fof(f163,plain,(
% 0.12/0.43 ![X0]: (greatest(sK15_skl,X0,sK14_skl)|member(sK7_skl(sK15_skl,sK14_skl,X0),sK14_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f57,f132])).
% 0.12/0.43 fof(f164,plain,(
% 0.12/0.43 ![X0]: (greatest(sK15_skl,X0,sK14_skl)|apply(sK13_skl,sK7_skl(sK15_skl,sK14_skl,X0),sK15_skl)|apply(sK13_skl,sK15_skl,sK7_skl(sK15_skl,sK14_skl,X0)))),
% 0.12/0.43 inference(resolution,[status(thm)],[f163,f141])).
% 0.12/0.43 fof(f216,plain,(
% 0.12/0.43 greatest(sK15_skl,sK13_skl,sK14_skl)|apply(sK13_skl,sK15_skl,sK7_skl(sK15_skl,sK14_skl,sK13_skl))|greatest(sK15_skl,sK13_skl,sK14_skl)|~member(sK15_skl,sK14_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f164,f58])).
% 0.12/0.43 fof(f219,plain,(
% 0.12/0.43 greatest(sK15_skl,sK13_skl,sK14_skl)|apply(sK13_skl,sK15_skl,sK7_skl(sK15_skl,sK14_skl,sK13_skl))|~member(sK15_skl,sK14_skl)),
% 0.12/0.43 inference(duplicate_literals_removal,[status(thm)],[f216])).
% 0.12/0.43 fof(f220,plain,(
% 0.12/0.43 apply(sK13_skl,sK15_skl,sK7_skl(sK15_skl,sK14_skl,sK13_skl))|~member(sK15_skl,sK14_skl)),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f219,f109])).
% 0.12/0.43 fof(f222,plain,(
% 0.12/0.43 apply(sK13_skl,sK15_skl,sK7_skl(sK15_skl,sK14_skl,sK13_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f220,f132])).
% 0.12/0.43 fof(f226,plain,(
% 0.12/0.43 ![X0]: (~max(sK15_skl,sK13_skl,X0)|~member(sK7_skl(sK15_skl,sK14_skl,sK13_skl),X0)|sK15_skl=sK7_skl(sK15_skl,sK14_skl,sK13_skl))),
% 0.12/0.43 inference(resolution,[status(thm)],[f222,f72])).
% 0.12/0.43 fof(f244,plain,(
% 0.12/0.43 ~max(sK15_skl,sK13_skl,sK14_skl)|sK15_skl=sK7_skl(sK15_skl,sK14_skl,sK13_skl)|greatest(sK15_skl,sK13_skl,sK14_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f226,f163])).
% 0.12/0.43 fof(f245,plain,(
% 0.12/0.43 sK15_skl=sK7_skl(sK15_skl,sK14_skl,sK13_skl)|greatest(sK15_skl,sK13_skl,sK14_skl)),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f244,f108])).
% 0.12/0.43 fof(f254,plain,(
% 0.12/0.43 sK15_skl=sK7_skl(sK15_skl,sK14_skl,sK13_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f245,f109])).
% 0.12/0.43 fof(f264,plain,(
% 0.12/0.43 greatest(sK15_skl,sK13_skl,sK14_skl)|~member(sK15_skl,sK14_skl)|~apply(sK13_skl,sK15_skl,sK15_skl)),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f254,f58])).
% 0.12/0.43 fof(f268,plain,(
% 0.12/0.43 ~member(sK15_skl,sK14_skl)|~apply(sK13_skl,sK15_skl,sK15_skl)),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f264,f109])).
% 0.12/0.43 fof(f271,plain,(
% 0.12/0.43 ~apply(sK13_skl,sK15_skl,sK15_skl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f268,f132])).
% 0.12/0.43 fof(f272,plain,(
% 0.12/0.43 $false),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f271,f143])).
% 0.12/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.46 % Elapsed time: 0.080256 seconds
% 0.12/0.46 % CPU time: 0.381398 seconds
% 0.12/0.46 % Total memory used: 87.826 MB
% 0.12/0.46 % Net memory used: 87.381 MB
%------------------------------------------------------------------------------