%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET803+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 : n010.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.09s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET803+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n010.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 05:39:10 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 0.09/0.60 % Refutation found
% 0.09/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.60 fof(f5,axiom,(
% 0.09/0.60 (! [R,E,M] :( greatest(M,R,E)<=> ( member(M,E)& (! [X] :( member(X,E)=> apply(R,X,M) ) )) ) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f7,axiom,(
% 0.09/0.60 (! [R,E,M] :( max(M,R,E)<=> ( member(M,E)& (! [X] :( ( member(X,E)& apply(R,M,X) )=> M = X ) )) ) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f11,conjecture,(
% 0.09/0.60 (! [R,E] :( order(R,E)=> (! [M1,M2] :( ( max(M1,R,E)& max(M2,R,E)& M1 != M2 )=> ~ (? [M] : greatest(M,R,E) )) )) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f12,negated_conjecture,(
% 0.09/0.60 ~((! [R,E] :( order(R,E)=> (! [M1,M2] :( ( max(M1,R,E)& max(M2,R,E)& M1 != M2 )=> ~ (? [M] : greatest(M,R,E) )) )) ))),
% 0.09/0.60 inference(negated_conjecture,[status(cth)],[f11])).
% 0.09/0.60 fof(f51,plain,(
% 0.09/0.60 ![R,E,M]: (greatest(M,R,E)<=>(member(M,E)&(![X]: (~member(X,E)|apply(R,X,M)))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.09/0.60 fof(f52,plain,(
% 0.09/0.60 ![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.09/0.60 inference(NNF_transformation,[status(thm)],[f51])).
% 0.09/0.60 fof(f53,plain,(
% 0.09/0.60 (![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.09/0.60 inference(miniscoping,[status(thm)],[f52])).
% 0.09/0.60 fof(f54,plain,(
% 0.09/0.60 (![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.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X,sK7_skl(M,E,R))],[f53])).
% 0.09/0.60 fof(f55,plain,(
% 0.09/0.60 ![X0,X1,X2]: (~greatest(X0,X1,X2)|member(X0,X2))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f54])).
% 0.09/0.60 fof(f56,plain,(
% 0.09/0.60 ![X0,X1,X2,X3]: (~greatest(X0,X1,X2)|~member(X3,X2)|apply(X1,X3,X0))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f54])).
% 0.09/0.60 fof(f67,plain,(
% 0.09/0.60 ![R,E,M]: (max(M,R,E)<=>(member(M,E)&(![X]: ((~member(X,E)|~apply(R,M,X))|M=X))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.09/0.60 fof(f68,plain,(
% 0.09/0.60 ![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.09/0.60 inference(NNF_transformation,[status(thm)],[f67])).
% 0.09/0.60 fof(f69,plain,(
% 0.09/0.60 (![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.09/0.60 inference(miniscoping,[status(thm)],[f68])).
% 0.09/0.60 fof(f70,plain,(
% 0.09/0.60 (![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.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl(M,E,R))],[f69])).
% 0.09/0.60 fof(f71,plain,(
% 0.09/0.60 ![X0,X1,X2]: (~max(X0,X1,X2)|member(X0,X2))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f70])).
% 0.09/0.60 fof(f72,plain,(
% 0.09/0.60 ![X0,X1,X2,X3]: (~max(X0,X1,X2)|~member(X3,X2)|~apply(X1,X0,X3)|X0=X3)),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f70])).
% 0.09/0.60 fof(f105,plain,(
% 0.09/0.60 (?[R,E]: (order(R,E)&(?[M1,M2]: (((max(M1,R,E)&max(M2,R,E))&~M1=M2)&(?[M]: greatest(M,R,E))))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.09/0.60 fof(f106,plain,(
% 0.09/0.60 ?[R,E]: (order(R,E)&((?[M1,M2]: ((max(M1,R,E)&max(M2,R,E))&~M1=M2))&(?[M]: greatest(M,R,E))))),
% 0.09/0.60 inference(miniscoping,[status(thm)],[f105])).
% 0.09/0.60 fof(f107,plain,(
% 0.09/0.60 (order(sK13_skl,sK14_skl)&(((max(sK15_skl,sK13_skl,sK14_skl)&max(sK16_skl,sK13_skl,sK14_skl))&~sK15_skl=sK16_skl)&greatest(sK17_skl,sK13_skl,sK14_skl)))),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(R,sK13_skl),skolemize(E,sK14_skl),skolemize(M1,sK15_skl),skolemize(M2,sK16_skl),skolemize(M,sK17_skl)],[f106])).
% 0.09/0.60 fof(f109,plain,(
% 0.09/0.60 max(sK15_skl,sK13_skl,sK14_skl)),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f107])).
% 0.09/0.61 fof(f110,plain,(
% 0.09/0.61 max(sK16_skl,sK13_skl,sK14_skl)),
% 0.09/0.61 inference(cnf_transformation,[status(thm)],[f107])).
% 0.09/0.61 fof(f111,plain,(
% 0.09/0.61 ~sK15_skl=sK16_skl),
% 0.09/0.61 inference(cnf_transformation,[status(thm)],[f107])).
% 0.09/0.61 fof(f112,plain,(
% 0.09/0.61 greatest(sK17_skl,sK13_skl,sK14_skl)),
% 0.09/0.61 inference(cnf_transformation,[status(thm)],[f107])).
% 0.09/0.61 fof(f131,plain,(
% 0.09/0.61 member(sK17_skl,sK14_skl)),
% 0.09/0.61 inference(resolution,[status(thm)],[f55,f112])).
% 0.09/0.61 fof(f135,plain,(
% 0.09/0.61 ![X0,X1,X2,X3,X4]: (~max(X0,X1,X2)|~member(X3,X2)|X0=X3|~greatest(X3,X1,X4)|~member(X0,X4))),
% 0.09/0.61 inference(resolution,[status(thm)],[f72,f56])).
% 0.09/0.61 fof(f136,plain,(
% 0.09/0.61 ![X0,X1]: (~max(X0,sK13_skl,X1)|~member(sK17_skl,X1)|X0=sK17_skl|~member(X0,sK14_skl))),
% 0.09/0.61 inference(resolution,[status(thm)],[f135,f112])).
% 0.09/0.61 fof(f137,plain,(
% 0.09/0.61 ![X0]: (~max(X0,sK13_skl,sK14_skl)|X0=sK17_skl|~member(X0,sK14_skl))),
% 0.09/0.61 inference(resolution,[status(thm)],[f136,f131])).
% 0.09/0.61 fof(f138,plain,(
% 0.09/0.61 ![X0]: (~max(X0,sK13_skl,sK14_skl)|X0=sK17_skl)),
% 0.09/0.61 inference(forward_subsumption_resolution,[status(thm)],[f137,f71])).
% 0.09/0.61 fof(f139,plain,(
% 0.09/0.61 sK16_skl=sK17_skl),
% 0.09/0.61 inference(resolution,[status(thm)],[f138,f110])).
% 0.09/0.61 fof(f140,plain,(
% 0.09/0.61 sK15_skl=sK17_skl),
% 0.09/0.61 inference(resolution,[status(thm)],[f138,f109])).
% 0.09/0.61 fof(f143,plain,(
% 0.09/0.61 ~sK15_skl=sK17_skl),
% 0.09/0.61 inference(backward_demodulation,[status(thm)],[f139,f111])).
% 0.09/0.61 fof(f146,plain,(
% 0.09/0.61 ~sK17_skl=sK17_skl),
% 0.09/0.61 inference(forward_demodulation,[status(thm)],[f140,f143])).
% 0.09/0.61 fof(f147,plain,(
% 0.09/0.61 $false),
% 0.09/0.61 inference(trivial_equality_resolution,[status(thm)],[f146])).
% 0.09/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.63 % Elapsed time: 0.054594 seconds
% 0.12/0.63 % CPU time: 0.150937 seconds
% 0.12/0.63 % Total memory used: 82.647 MB
% 0.12/0.63 % Net memory used: 82.535 MB
%------------------------------------------------------------------------------