%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET804+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:37 PM UTC 2026
% Result : Theorem 0.02s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET804+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 05:39:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.02/0.39 % Drodi V4.1.1
% 0.02/0.41 % Refutation found
% 0.02/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.41 fof(f6,axiom,(
% 0.02/0.41 (! [R,E,M] :( least(M,R,E)<=> ( member(M,E)& (! [X] :( member(X,E)=> apply(R,M,X) ) )) ) )),
% 0.02/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.41 fof(f8,axiom,(
% 0.02/0.41 (! [R,E,M] :( min(M,R,E)<=> ( member(M,E)& (! [X] :( ( member(X,E)& apply(R,X,M) )=> M = X ) )) ) )),
% 0.02/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.41 fof(f11,conjecture,(
% 0.02/0.41 (! [R,E] :( order(R,E)=> (! [M1,M2] :( ( min(M1,R,E)& min(M2,R,E)& M1 != M2 )=> ~ (? [M] : least(M,R,E) )) )) )),
% 0.02/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.41 fof(f12,negated_conjecture,(
% 0.02/0.41 ~((! [R,E] :( order(R,E)=> (! [M1,M2] :( ( min(M1,R,E)& min(M2,R,E)& M1 != M2 )=> ~ (? [M] : least(M,R,E) )) )) ))),
% 0.02/0.41 inference(negated_conjecture,[status(cth)],[f11])).
% 0.02/0.41 fof(f59,plain,(
% 0.02/0.41 ![R,E,M]: (least(M,R,E)<=>(member(M,E)&(![X]: (~member(X,E)|apply(R,M,X)))))),
% 0.02/0.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.02/0.41 fof(f60,plain,(
% 0.02/0.41 ![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.02/0.41 inference(NNF_transformation,[status(thm)],[f59])).
% 0.02/0.41 fof(f61,plain,(
% 0.02/0.41 (![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.02/0.41 inference(miniscoping,[status(thm)],[f60])).
% 0.02/0.41 fof(f62,plain,(
% 0.02/0.41 (![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(sK8_skl(M,E,R),E)&~apply(R,M,sK8_skl(M,E,R))))))),
% 0.02/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X,sK8_skl(M,E,R))],[f61])).
% 0.02/0.41 fof(f63,plain,(
% 0.02/0.41 ![X0,X1,X2]: (~least(X0,X1,X2)|member(X0,X2))),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f62])).
% 0.02/0.41 fof(f64,plain,(
% 0.02/0.41 ![X0,X1,X2,X3]: (~least(X0,X1,X2)|~member(X3,X2)|apply(X1,X0,X3))),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f62])).
% 0.02/0.41 fof(f76,plain,(
% 0.02/0.41 ![R,E,M]: (min(M,R,E)<=>(member(M,E)&(![X]: ((~member(X,E)|~apply(R,X,M))|M=X))))),
% 0.02/0.41 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.02/0.41 fof(f77,plain,(
% 0.02/0.41 ![R,E,M]: ((~min(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,X,M))|M=X))))&(min(M,R,E)|(~member(M,E)|(?[X]: ((member(X,E)&apply(R,X,M))&~M=X)))))),
% 0.02/0.41 inference(NNF_transformation,[status(thm)],[f76])).
% 0.02/0.41 fof(f78,plain,(
% 0.02/0.41 (![R,E,M]: (~min(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,X,M))|M=X)))))&(![R,E,M]: (min(M,R,E)|(~member(M,E)|(?[X]: ((member(X,E)&apply(R,X,M))&~M=X)))))),
% 0.02/0.41 inference(miniscoping,[status(thm)],[f77])).
% 0.02/0.41 fof(f79,plain,(
% 0.02/0.41 (![R,E,M]: (~min(M,R,E)|(member(M,E)&(![X]: ((~member(X,E)|~apply(R,X,M))|M=X)))))&(![R,E,M]: (min(M,R,E)|(~member(M,E)|((member(sK10_skl(M,E,R),E)&apply(R,sK10_skl(M,E,R),M))&~M=sK10_skl(M,E,R)))))),
% 0.02/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(M,E,R))],[f78])).
% 0.02/0.41 fof(f80,plain,(
% 0.02/0.41 ![X0,X1,X2]: (~min(X0,X1,X2)|member(X0,X2))),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f79])).
% 0.02/0.41 fof(f81,plain,(
% 0.02/0.41 ![X0,X1,X2,X3]: (~min(X0,X1,X2)|~member(X3,X2)|~apply(X1,X3,X0)|X0=X3)),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f79])).
% 0.02/0.41 fof(f105,plain,(
% 0.02/0.41 (?[R,E]: (order(R,E)&(?[M1,M2]: (((min(M1,R,E)&min(M2,R,E))&~M1=M2)&(?[M]: least(M,R,E))))))),
% 0.02/0.41 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.02/0.41 fof(f106,plain,(
% 0.02/0.41 ?[R,E]: (order(R,E)&((?[M1,M2]: ((min(M1,R,E)&min(M2,R,E))&~M1=M2))&(?[M]: least(M,R,E))))),
% 0.02/0.41 inference(miniscoping,[status(thm)],[f105])).
% 0.02/0.41 fof(f107,plain,(
% 0.02/0.41 (order(sK13_skl,sK14_skl)&(((min(sK15_skl,sK13_skl,sK14_skl)&min(sK16_skl,sK13_skl,sK14_skl))&~sK15_skl=sK16_skl)&least(sK17_skl,sK13_skl,sK14_skl)))),
% 0.02/0.41 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.02/0.41 fof(f109,plain,(
% 0.02/0.41 min(sK15_skl,sK13_skl,sK14_skl)),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.02/0.41 fof(f110,plain,(
% 0.02/0.41 min(sK16_skl,sK13_skl,sK14_skl)),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.02/0.41 fof(f111,plain,(
% 0.02/0.41 ~sK15_skl=sK16_skl),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.02/0.41 fof(f112,plain,(
% 0.02/0.41 least(sK17_skl,sK13_skl,sK14_skl)),
% 0.02/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.02/0.41 fof(f131,plain,(
% 0.02/0.41 member(sK17_skl,sK14_skl)),
% 0.02/0.41 inference(resolution,[status(thm)],[f63,f112])).
% 0.02/0.41 fof(f135,plain,(
% 0.02/0.41 ![X0,X1,X2,X3,X4]: (~min(X0,X1,X2)|~member(X3,X2)|X0=X3|~least(X3,X1,X4)|~member(X0,X4))),
% 0.02/0.41 inference(resolution,[status(thm)],[f81,f64])).
% 0.02/0.41 fof(f136,plain,(
% 0.02/0.41 ![X0,X1]: (~min(X0,sK13_skl,X1)|~member(sK17_skl,X1)|X0=sK17_skl|~member(X0,sK14_skl))),
% 0.02/0.41 inference(resolution,[status(thm)],[f135,f112])).
% 0.02/0.41 fof(f137,plain,(
% 0.02/0.41 ![X0]: (~min(X0,sK13_skl,sK14_skl)|X0=sK17_skl|~member(X0,sK14_skl))),
% 0.02/0.41 inference(resolution,[status(thm)],[f136,f131])).
% 0.02/0.41 fof(f138,plain,(
% 0.02/0.41 ![X0]: (~min(X0,sK13_skl,sK14_skl)|X0=sK17_skl)),
% 0.02/0.41 inference(forward_subsumption_resolution,[status(thm)],[f137,f80])).
% 0.02/0.41 fof(f139,plain,(
% 0.02/0.41 sK16_skl=sK17_skl),
% 0.02/0.41 inference(resolution,[status(thm)],[f138,f110])).
% 0.02/0.41 fof(f140,plain,(
% 0.02/0.41 sK15_skl=sK17_skl),
% 0.02/0.41 inference(resolution,[status(thm)],[f138,f109])).
% 0.02/0.41 fof(f143,plain,(
% 0.02/0.41 ~sK15_skl=sK17_skl),
% 0.02/0.41 inference(backward_demodulation,[status(thm)],[f139,f111])).
% 0.02/0.41 fof(f146,plain,(
% 0.02/0.41 ~sK17_skl=sK17_skl),
% 0.02/0.41 inference(forward_demodulation,[status(thm)],[f140,f143])).
% 0.02/0.41 fof(f147,plain,(
% 0.02/0.41 $false),
% 0.02/0.41 inference(trivial_equality_resolution,[status(thm)],[f146])).
% 0.02/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.44 % Elapsed time: 0.053370 seconds
% 0.02/0.44 % CPU time: 0.160644 seconds
% 0.02/0.44 % Total memory used: 82.604 MB
% 0.02/0.44 % Net memory used: 82.492 MB
%------------------------------------------------------------------------------