%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET776+4 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:34 PM UTC 2026
% Result : Theorem 0.16s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET776+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n008.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 05:37:54 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.54 % Refutation found
% 0.16/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.54 fof(f16,axiom,(
% 0.16/0.54 (! [R,E] :( pre_order(R,E)<=> ( (! [X] :( member(X,E)=> apply(R,X,X) ))& (! [X,Y,Z] :( ( member(X,E)& member(Y,E)& member(Z,E) )=> ( ( apply(R,X,Y)& apply(R,Y,Z) )=> apply(R,X,Z) ) ) )) ) )),
% 0.16/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.54 fof(f17,conjecture,(
% 0.16/0.54 (! [E,P,R] :( ( pre_order(P,E)& (! [A,B] :( ( member(A,E)& member(B,E) )=> ( apply(R,A,B)<=> ( apply(P,A,B)& apply(P,B,A) ) ) ) ))=> (! [X1,X2,Y1,Y2] :( ( member(X1,E)& member(X2,E)& member(Y1,E)& member(Y2,E) )=> ( ( apply(R,X1,Y1)& apply(R,X2,Y2)& apply(P,X1,X2) )=> apply(P,Y1,Y2) ) ) )) )),
% 0.16/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.54 fof(f18,negated_conjecture,(
% 0.16/0.54 ~((! [E,P,R] :( ( pre_order(P,E)& (! [A,B] :( ( member(A,E)& member(B,E) )=> ( apply(R,A,B)<=> ( apply(P,A,B)& apply(P,B,A) ) ) ) ))=> (! [X1,X2,Y1,Y2] :( ( member(X1,E)& member(X2,E)& member(Y1,E)& member(Y2,E) )=> ( ( apply(R,X1,Y1)& apply(R,X2,Y2)& apply(P,X1,X2) )=> apply(P,Y1,Y2) ) ) )) ))),
% 0.16/0.54 inference(negated_conjecture,[status(cth)],[f17])).
% 0.16/0.54 fof(f112,plain,(
% 0.16/0.54 ![R,E]: (pre_order(R,E)<=>((![X]: (~member(X,E)|apply(R,X,X)))&(![X,Y,Z]: (((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))),
% 0.16/0.54 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.16/0.54 fof(f113,definition,(
% 0.16/0.54 ![R,E,X]: (sP2_prd(X,E,R)<=>(~member(X,E)|apply(R,X,X)))),
% 0.16/0.54 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.16/0.54 fof(f114,plain,(
% 0.16/0.54 ![R,E]: (pre_order(R,E)<=>((![X]: sP2_prd(X,E,R))&(![X,Y,Z]: (((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))),
% 0.16/0.54 inference(formula_renaming,[status(thm)],[f112,f113])).
% 0.16/0.54 fof(f115,plain,(
% 0.16/0.54 ![R,E]: ((~pre_order(R,E)|((![X]: sP2_prd(X,E,R))&(![X,Y,Z]: (((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))&(pre_order(R,E)|((?[X]: ~sP2_prd(X,E,R))|(?[X,Y,Z]: (((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))),
% 0.16/0.54 inference(NNF_transformation,[status(thm)],[f114])).
% 0.16/0.54 fof(f116,plain,(
% 0.16/0.54 (![R,E]: (~pre_order(R,E)|((![X]: sP2_prd(X,E,R))&(![X,Y,Z]: (((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z)))))))&(![R,E]: (pre_order(R,E)|((?[X]: ~sP2_prd(X,E,R))|(?[X,Y,Z]: (((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))),
% 0.16/0.54 inference(miniscoping,[status(thm)],[f115])).
% 0.16/0.54 fof(f117,plain,(
% 0.16/0.54 (![R,E]: (~pre_order(R,E)|((![X]: sP2_prd(X,E,R))&(![X,Y,Z]: (((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z)))))))&(![R,E]: (pre_order(R,E)|(~sP2_prd(sK10_skl(E,R),E,R)|(((member(sK11_skl(E,R),E)&member(sK12_skl(E,R),E))&member(sK13_skl(E,R),E))&((apply(R,sK11_skl(E,R),sK12_skl(E,R))&apply(R,sK12_skl(E,R),sK13_skl(E,R)))&~apply(R,sK11_skl(E,R),sK13_skl(E,R)))))))),
% 0.16/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(X,sK10_skl(E,R)),skolemize(X,sK11_skl(E,R)),skolemize(Y,sK12_skl(E,R)),skolemize(Z,sK13_skl(E,R))],[f116])).
% 0.16/0.54 fof(f119,plain,(
% 0.16/0.54 ![X0,X1,X2,X3,X4]: (~pre_order(X0,X1)|~member(X2,X1)|~member(X3,X1)|~member(X4,X1)|~apply(X0,X2,X3)|~apply(X0,X3,X4)|apply(X0,X2,X4))),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f117])).
% 0.16/0.54 fof(f126,plain,(
% 0.16/0.54 (?[E,P,R]: ((pre_order(P,E)&(![A,B]: ((~member(A,E)|~member(B,E))|(apply(R,A,B)<=>(apply(P,A,B)&apply(P,B,A))))))&(?[X1,X2,Y1,Y2]: ((((member(X1,E)&member(X2,E))&member(Y1,E))&member(Y2,E))&(((apply(R,X1,Y1)&apply(R,X2,Y2))&apply(P,X1,X2))&~apply(P,Y1,Y2))))))),
% 0.16/0.54 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.16/0.54 fof(f127,plain,(
% 0.16/0.54 ?[E,P,R]: ((pre_order(P,E)&(![A,B]: ((~member(A,E)|~member(B,E))|((~apply(R,A,B)|(apply(P,A,B)&apply(P,B,A)))&(apply(R,A,B)|(~apply(P,A,B)|~apply(P,B,A)))))))&(?[X1,X2,Y1,Y2]: ((((member(X1,E)&member(X2,E))&member(Y1,E))&member(Y2,E))&(((apply(R,X1,Y1)&apply(R,X2,Y2))&apply(P,X1,X2))&~apply(P,Y1,Y2)))))),
% 0.16/0.54 inference(NNF_transformation,[status(thm)],[f126])).
% 0.16/0.54 fof(f128,plain,(
% 0.16/0.54 ((pre_order(sK15_skl,sK14_skl)&(![A,B]: ((~member(A,sK14_skl)|~member(B,sK14_skl))|((~apply(sK16_skl,A,B)|(apply(sK15_skl,A,B)&apply(sK15_skl,B,A)))&(apply(sK16_skl,A,B)|(~apply(sK15_skl,A,B)|~apply(sK15_skl,B,A)))))))&((((member(sK17_skl,sK14_skl)&member(sK18_skl,sK14_skl))&member(sK19_skl,sK14_skl))&member(sK20_skl,sK14_skl))&(((apply(sK16_skl,sK17_skl,sK19_skl)&apply(sK16_skl,sK18_skl,sK20_skl))&apply(sK15_skl,sK17_skl,sK18_skl))&~apply(sK15_skl,sK19_skl,sK20_skl))))),
% 0.16/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl]),skolemize(E,sK14_skl),skolemize(P,sK15_skl),skolemize(R,sK16_skl),skolemize(X1,sK17_skl),skolemize(X2,sK18_skl),skolemize(Y1,sK19_skl),skolemize(Y2,sK20_skl)],[f127])).
% 0.16/0.54 fof(f129,plain,(
% 0.16/0.54 pre_order(sK15_skl,sK14_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f130,plain,(
% 0.16/0.54 ![X0,X1]: (~member(X0,sK14_skl)|~member(X1,sK14_skl)|~apply(sK16_skl,X0,X1)|apply(sK15_skl,X0,X1))),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f131,plain,(
% 0.16/0.54 ![X0,X1]: (~member(X0,sK14_skl)|~member(X1,sK14_skl)|~apply(sK16_skl,X0,X1)|apply(sK15_skl,X1,X0))),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f133,plain,(
% 0.16/0.54 member(sK17_skl,sK14_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f134,plain,(
% 0.16/0.54 member(sK18_skl,sK14_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f135,plain,(
% 0.16/0.54 member(sK19_skl,sK14_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f136,plain,(
% 0.16/0.54 member(sK20_skl,sK14_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f137,plain,(
% 0.16/0.54 apply(sK16_skl,sK17_skl,sK19_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f138,plain,(
% 0.16/0.54 apply(sK16_skl,sK18_skl,sK20_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f139,plain,(
% 0.16/0.54 apply(sK15_skl,sK17_skl,sK18_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f140,plain,(
% 0.16/0.54 ~apply(sK15_skl,sK19_skl,sK20_skl)),
% 0.16/0.54 inference(cnf_transformation,[status(thm)],[f128])).
% 0.16/0.54 fof(f177,plain,(
% 0.16/0.54 ~member(sK18_skl,sK14_skl)|~member(sK20_skl,sK14_skl)|apply(sK15_skl,sK18_skl,sK20_skl)),
% 0.16/0.54 inference(resolution,[status(thm)],[f138,f130])).
% 0.16/0.54 fof(f178,plain,(
% 0.16/0.54 ~member(sK20_skl,sK14_skl)|apply(sK15_skl,sK18_skl,sK20_skl)),
% 0.16/0.54 inference(forward_subsumption_resolution,[status(thm)],[f177,f134])).
% 0.16/0.54 fof(f179,plain,(
% 0.16/0.54 ![X0,X1,X2]: (~member(X0,sK14_skl)|~member(X1,sK14_skl)|~member(X2,sK14_skl)|~apply(sK15_skl,X0,X1)|~apply(sK15_skl,X1,X2)|apply(sK15_skl,X0,X2))),
% 0.16/0.54 inference(resolution,[status(thm)],[f119,f129])).
% 0.16/0.54 fof(f181,plain,(
% 0.16/0.54 ~member(sK17_skl,sK14_skl)|~member(sK19_skl,sK14_skl)|apply(sK15_skl,sK19_skl,sK17_skl)),
% 0.16/0.54 inference(resolution,[status(thm)],[f131,f137])).
% 0.16/0.54 fof(f183,plain,(
% 0.16/0.54 ~member(sK19_skl,sK14_skl)|apply(sK15_skl,sK19_skl,sK17_skl)),
% 0.16/0.54 inference(forward_subsumption_resolution,[status(thm)],[f181,f133])).
% 0.16/0.54 fof(f191,plain,(
% 0.16/0.54 ![X0]: (~member(sK19_skl,sK14_skl)|~member(X0,sK14_skl)|~member(sK20_skl,sK14_skl)|~apply(sK15_skl,sK19_skl,X0)|~apply(sK15_skl,X0,sK20_skl))),
% 0.16/0.54 inference(resolution,[status(thm)],[f179,f140])).
% 0.16/0.54 fof(f192,plain,(
% 0.16/0.54 ![X0]: (~member(X0,sK14_skl)|~member(sK20_skl,sK14_skl)|~apply(sK15_skl,sK19_skl,X0)|~apply(sK15_skl,X0,sK20_skl))),
% 0.16/0.54 inference(forward_subsumption_resolution,[status(thm)],[f191,f135])).
% 0.16/0.54 fof(f193,plain,(
% 0.16/0.54 ![X0]: (~member(X0,sK14_skl)|~apply(sK15_skl,sK19_skl,X0)|~apply(sK15_skl,X0,sK20_skl))),
% 0.16/0.54 inference(resolution,[status(thm)],[f192,f136])).
% 0.16/0.54 fof(f195,plain,(
% 0.16/0.54 ![X0,X1]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~member(sK19_skl,sK14_skl)|~member(X1,sK14_skl)|~member(X0,sK14_skl)|~apply(sK15_skl,sK19_skl,X1)|~apply(sK15_skl,X1,X0))),
% 0.16/0.54 inference(resolution,[status(thm)],[f193,f179])).
% 0.16/0.54 fof(f197,plain,(
% 0.16/0.54 ![X0,X1]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~member(sK19_skl,sK14_skl)|~member(X1,sK14_skl)|~apply(sK15_skl,sK19_skl,X1)|~apply(sK15_skl,X1,X0))),
% 0.16/0.54 inference(duplicate_literals_removal,[status(thm)],[f195])).
% 0.16/0.54 fof(f198,plain,(
% 0.16/0.54 ![X0,X1]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~member(X1,sK14_skl)|~apply(sK15_skl,sK19_skl,X1)|~apply(sK15_skl,X1,X0))),
% 0.16/0.55 inference(forward_subsumption_resolution,[status(thm)],[f197,f135])).
% 0.16/0.55 fof(f201,plain,(
% 0.16/0.55 ![X0]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~member(sK17_skl,sK14_skl)|~apply(sK15_skl,sK17_skl,X0)|~member(sK19_skl,sK14_skl))),
% 0.16/0.55 inference(resolution,[status(thm)],[f198,f183])).
% 0.16/0.55 fof(f203,plain,(
% 0.16/0.55 ![X0]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~apply(sK15_skl,sK17_skl,X0)|~member(sK19_skl,sK14_skl))),
% 0.16/0.55 inference(forward_subsumption_resolution,[status(thm)],[f201,f133])).
% 0.16/0.55 fof(f206,plain,(
% 0.16/0.55 ![X0]: (~member(X0,sK14_skl)|~apply(sK15_skl,X0,sK20_skl)|~apply(sK15_skl,sK17_skl,X0))),
% 0.16/0.55 inference(resolution,[status(thm)],[f203,f135])).
% 0.16/0.55 fof(f207,plain,(
% 0.16/0.55 ~member(sK18_skl,sK14_skl)|~apply(sK15_skl,sK17_skl,sK18_skl)|~member(sK20_skl,sK14_skl)),
% 0.16/0.55 inference(resolution,[status(thm)],[f206,f178])).
% 0.16/0.55 fof(f209,plain,(
% 0.16/0.55 ~apply(sK15_skl,sK17_skl,sK18_skl)|~member(sK20_skl,sK14_skl)),
% 0.16/0.55 inference(forward_subsumption_resolution,[status(thm)],[f207,f134])).
% 0.16/0.55 fof(f212,plain,(
% 0.16/0.55 ~apply(sK15_skl,sK17_skl,sK18_skl)),
% 0.16/0.55 inference(resolution,[status(thm)],[f209,f136])).
% 0.16/0.55 fof(f213,plain,(
% 0.16/0.55 $false),
% 0.16/0.55 inference(forward_subsumption_resolution,[status(thm)],[f212,f139])).
% 0.16/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.56 % Elapsed time: 0.117659 seconds
% 0.16/0.56 % CPU time: 0.432913 seconds
% 0.16/0.56 % Total memory used: 69.010 MB
% 0.16/0.56 % Net memory used: 68.643 MB
%------------------------------------------------------------------------------