%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET722+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 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:30 PM UTC 2026
% Result : Theorem 159.40s 20.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET722+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n019.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:34:05 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 159.40/20.68 % Refutation found
% 159.40/20.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 159.40/20.68 % SZS output start CNFRefutation for theBenchmark
% 159.40/20.68 fof(f14,axiom,(
% 159.40/20.68 (! [G,F,A,B,C,X,Z] :( ( member(X,A)& member(Z,C) )=> ( apply(compose_function(G,F,A,B,C),X,Z)<=> (? [Y] :( member(Y,B)& apply(F,X,Y)& apply(G,Y,Z) ) )) ) )),
% 159.40/20.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 159.40/20.68 fof(f18,axiom,(
% 159.40/20.68 (! [F,A,B] :( surjective(F,A,B)<=> (! [Y] :( member(Y,B)=> (? [E] :( member(E,A)& apply(F,E,Y) ) )) )) )),
% 159.40/20.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 159.40/20.68 fof(f29,conjecture,(
% 159.40/20.68 (! [F,G,A,B,C] :( ( maps(F,A,B)& maps(G,B,C)& surjective(compose_function(G,F,A,B,C),A,C) )=> surjective(G,B,C) ) )),
% 159.40/20.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 159.40/20.68 fof(f30,negated_conjecture,(
% 159.40/20.68 ~((! [F,G,A,B,C] :( ( maps(F,A,B)& maps(G,B,C)& surjective(compose_function(G,F,A,B,C),A,C) )=> surjective(G,B,C) ) ))),
% 159.40/20.68 inference(negated_conjecture,[status(cth)],[f29])).
% 159.40/20.68 fof(f111,plain,(
% 159.40/20.68 ![G,F,A,B,C,X,Z]: ((~member(X,A)|~member(Z,C))|(apply(compose_function(G,F,A,B,C),X,Z)<=>(?[Y]: ((member(Y,B)&apply(F,X,Y))&apply(G,Y,Z)))))),
% 159.40/20.68 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 159.40/20.68 fof(f112,plain,(
% 159.40/20.68 ![G,F,A,B,C,X,Z]: ((~member(X,A)|~member(Z,C))|((~apply(compose_function(G,F,A,B,C),X,Z)|(?[Y]: ((member(Y,B)&apply(F,X,Y))&apply(G,Y,Z))))&(apply(compose_function(G,F,A,B,C),X,Z)|(![Y]: ((~member(Y,B)|~apply(F,X,Y))|~apply(G,Y,Z))))))),
% 159.40/20.68 inference(NNF_transformation,[status(thm)],[f111])).
% 159.40/20.68 fof(f113,plain,(
% 159.40/20.68 ![A,C,X,Z]: ((~member(X,A)|~member(Z,C))|((![G,F,B]: (~apply(compose_function(G,F,A,B,C),X,Z)|(?[Y]: ((member(Y,B)&apply(F,X,Y))&apply(G,Y,Z)))))&(![G,F,B]: (apply(compose_function(G,F,A,B,C),X,Z)|(![Y]: ((~member(Y,B)|~apply(F,X,Y))|~apply(G,Y,Z)))))))),
% 159.40/20.68 inference(miniscoping,[status(thm)],[f112])).
% 159.40/20.68 fof(f114,plain,(
% 159.40/20.68 ![A,C,X,Z]: ((~member(X,A)|~member(Z,C))|((![G,F,B]: (~apply(compose_function(G,F,A,B,C),X,Z)|((member(sK11_skl(B,F,G,Z,X,C,A),B)&apply(F,X,sK11_skl(B,F,G,Z,X,C,A)))&apply(G,sK11_skl(B,F,G,Z,X,C,A),Z))))&(![G,F,B]: (apply(compose_function(G,F,A,B,C),X,Z)|(![Y]: ((~member(Y,B)|~apply(F,X,Y))|~apply(G,Y,Z)))))))),
% 159.40/20.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Y,sK11_skl(B,F,G,Z,X,C,A))],[f113])).
% 159.40/20.68 fof(f115,plain,(
% 159.40/20.68 ![X0,X1,X2,X3,X4,X5,X6]: (~member(X0,X1)|~member(X2,X3)|~apply(compose_function(X4,X5,X1,X6,X3),X0,X2)|member(sK11_skl(X6,X5,X4,X2,X0,X3,X1),X6))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f114])).
% 159.40/20.68 fof(f117,plain,(
% 159.40/20.68 ![X0,X1,X2,X3,X4,X5,X6]: (~member(X0,X1)|~member(X2,X3)|~apply(compose_function(X4,X5,X1,X6,X3),X0,X2)|apply(X4,sK11_skl(X6,X5,X4,X2,X0,X3,X1),X2))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f114])).
% 159.40/20.68 fof(f148,plain,(
% 159.40/20.68 ![F,A,B]: (surjective(F,A,B)<=>(![Y]: (~member(Y,B)|(?[E]: (member(E,A)&apply(F,E,Y))))))),
% 159.40/20.68 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 159.40/20.68 fof(f149,plain,(
% 159.40/20.68 ![F,A,B]: ((~surjective(F,A,B)|(![Y]: (~member(Y,B)|(?[E]: (member(E,A)&apply(F,E,Y))))))&(surjective(F,A,B)|(?[Y]: (member(Y,B)&(![E]: (~member(E,A)|~apply(F,E,Y)))))))),
% 159.40/20.68 inference(NNF_transformation,[status(thm)],[f148])).
% 159.40/20.68 fof(f150,plain,(
% 159.40/20.68 (![F,A,B]: (~surjective(F,A,B)|(![Y]: (~member(Y,B)|(?[E]: (member(E,A)&apply(F,E,Y)))))))&(![F,A,B]: (surjective(F,A,B)|(?[Y]: (member(Y,B)&(![E]: (~member(E,A)|~apply(F,E,Y)))))))),
% 159.40/20.68 inference(miniscoping,[status(thm)],[f149])).
% 159.40/20.68 fof(f151,plain,(
% 159.40/20.68 (![F,A,B]: (~surjective(F,A,B)|(![Y]: (~member(Y,B)|(member(sK19_skl(Y,B,A,F),A)&apply(F,sK19_skl(Y,B,A,F),Y))))))&(![F,A,B]: (surjective(F,A,B)|(member(sK20_skl(B,A,F),B)&(![E]: (~member(E,A)|~apply(F,E,sK20_skl(B,A,F)))))))),
% 159.40/20.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(E,sK19_skl(Y,B,A,F)),skolemize(Y,sK20_skl(B,A,F))],[f150])).
% 159.40/20.68 fof(f152,plain,(
% 159.40/20.68 ![X0,X1,X2,X3]: (~surjective(X0,X1,X2)|~member(X3,X2)|member(sK19_skl(X3,X2,X1,X0),X1))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f151])).
% 159.40/20.68 fof(f153,plain,(
% 159.40/20.68 ![X0,X1,X2,X3]: (~surjective(X0,X1,X2)|~member(X3,X2)|apply(X0,sK19_skl(X3,X2,X1,X0),X3))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f151])).
% 159.40/20.68 fof(f154,plain,(
% 159.40/20.68 ![X0,X1,X2]: (surjective(X0,X1,X2)|member(sK20_skl(X2,X1,X0),X2))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f151])).
% 159.40/20.68 fof(f155,plain,(
% 159.40/20.68 ![X0,X1,X2,X3]: (surjective(X0,X1,X2)|~member(X3,X1)|~apply(X0,X3,sK20_skl(X2,X1,X0)))),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f151])).
% 159.40/20.68 fof(f244,plain,(
% 159.40/20.68 (?[F,G,A,B,C]: (((maps(F,A,B)&maps(G,B,C))&surjective(compose_function(G,F,A,B,C),A,C))&~surjective(G,B,C)))),
% 159.40/20.68 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 159.40/20.68 fof(f245,plain,(
% 159.40/20.68 ?[G,B,C]: ((?[F,A]: ((maps(F,A,B)&maps(G,B,C))&surjective(compose_function(G,F,A,B,C),A,C)))&~surjective(G,B,C))),
% 159.40/20.68 inference(miniscoping,[status(thm)],[f244])).
% 159.40/20.68 fof(f246,plain,(
% 159.40/20.68 (((maps(sK42_skl,sK43_skl,sK40_skl)&maps(sK39_skl,sK40_skl,sK41_skl))&surjective(compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl),sK43_skl,sK41_skl))&~surjective(sK39_skl,sK40_skl,sK41_skl))),
% 159.40/20.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl]),skolemize(G,sK39_skl),skolemize(B,sK40_skl),skolemize(C,sK41_skl),skolemize(F,sK42_skl),skolemize(A,sK43_skl)],[f245])).
% 159.40/20.68 fof(f249,plain,(
% 159.40/20.68 surjective(compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl),sK43_skl,sK41_skl)),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f246])).
% 159.40/20.68 fof(f250,plain,(
% 159.40/20.68 ~surjective(sK39_skl,sK40_skl,sK41_skl)),
% 159.40/20.68 inference(cnf_transformation,[status(thm)],[f246])).
% 159.40/20.68 fof(f341,plain,(
% 159.40/20.68 ![X0]: (~member(X0,sK41_skl)|member(sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK43_skl))),
% 159.40/20.68 inference(resolution,[status(thm)],[f152,f249])).
% 159.40/20.68 fof(f344,plain,(
% 159.40/20.68 ![X0]: (~member(X0,sK41_skl)|apply(compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl),sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),X0))),
% 159.40/20.68 inference(resolution,[status(thm)],[f153,f249])).
% 159.40/20.68 fof(f434,plain,(
% 159.40/20.68 ![X0]: (~member(sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK43_skl)|~member(X0,sK41_skl)|member(sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),sK40_skl)|~member(X0,sK41_skl))),
% 159.40/20.68 inference(resolution,[status(thm)],[f115,f344])).
% 159.40/20.68 fof(f436,plain,(
% 159.40/20.68 ![X0]: (~member(sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK43_skl)|~member(X0,sK41_skl)|member(sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),sK40_skl))),
% 159.40/20.68 inference(duplicate_literals_removal,[status(thm)],[f434])).
% 159.40/20.68 fof(f437,plain,(
% 159.40/20.68 ![X0]: (~member(X0,sK41_skl)|member(sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),sK40_skl))),
% 159.40/20.68 inference(forward_subsumption_resolution,[status(thm)],[f436,f341])).
% 159.40/20.68 fof(f1812,plain,(
% 159.40/20.68 ![X0]: (~member(sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK43_skl)|~member(X0,sK41_skl)|apply(sK39_skl,sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),X0)|~member(X0,sK41_skl))),
% 159.40/20.68 inference(resolution,[status(thm)],[f117,f344])).
% 159.40/20.68 fof(f1814,plain,(
% 159.40/20.68 ![X0]: (~member(sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK43_skl)|~member(X0,sK41_skl)|apply(sK39_skl,sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),X0))),
% 159.40/20.68 inference(duplicate_literals_removal,[status(thm)],[f1812])).
% 159.40/20.68 fof(f1815,plain,(
% 159.40/20.68 ![X0]: (~member(X0,sK41_skl)|apply(sK39_skl,sK11_skl(sK40_skl,sK42_skl,sK39_skl,X0,sK19_skl(X0,sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),X0))),
% 159.40/20.68 inference(forward_subsumption_resolution,[status(thm)],[f1814,f341])).
% 159.40/20.68 fof(f1829,plain,(
% 125.36/20.75 ![X0,X1]: (apply(sK39_skl,sK11_skl(sK40_skl,sK42_skl,sK39_skl,sK20_skl(sK41_skl,X0,X1),sK19_skl(sK20_skl(sK41_skl,X0,X1),sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),sK20_skl(sK41_skl,X0,X1))|surjective(X1,X0,sK41_skl))),
% 125.36/20.75 inference(resolution,[status(thm)],[f1815,f154])).
% 125.36/20.75 fof(f3504,plain,(
% 125.36/20.75 ![X0]: (surjective(sK39_skl,X0,sK41_skl)|~member(sK11_skl(sK40_skl,sK42_skl,sK39_skl,sK20_skl(sK41_skl,X0,sK39_skl),sK19_skl(sK20_skl(sK41_skl,X0,sK39_skl),sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),X0)|surjective(sK39_skl,X0,sK41_skl))),
% 125.36/20.75 inference(resolution,[status(thm)],[f155,f1829])).
% 125.36/20.75 fof(f3506,plain,(
% 125.36/20.75 ![X0]: (surjective(sK39_skl,X0,sK41_skl)|~member(sK11_skl(sK40_skl,sK42_skl,sK39_skl,sK20_skl(sK41_skl,X0,sK39_skl),sK19_skl(sK20_skl(sK41_skl,X0,sK39_skl),sK41_skl,sK43_skl,compose_function(sK39_skl,sK42_skl,sK43_skl,sK40_skl,sK41_skl)),sK41_skl,sK43_skl),X0))),
% 125.36/20.75 inference(duplicate_literals_removal,[status(thm)],[f3504])).
% 125.36/20.75 fof(f3535,plain,(
% 125.36/20.75 surjective(sK39_skl,sK40_skl,sK41_skl)|~member(sK20_skl(sK41_skl,sK40_skl,sK39_skl),sK41_skl)),
% 125.36/20.75 inference(resolution,[status(thm)],[f3506,f437])).
% 125.36/20.75 fof(f3559,plain,(
% 125.36/20.75 ~member(sK20_skl(sK41_skl,sK40_skl,sK39_skl),sK41_skl)),
% 125.36/20.75 inference(forward_subsumption_resolution,[status(thm)],[f3535,f250])).
% 125.36/20.75 fof(f3560,plain,(
% 125.36/20.75 surjective(sK39_skl,sK40_skl,sK41_skl)),
% 125.36/20.75 inference(resolution,[status(thm)],[f3559,f154])).
% 125.36/20.75 fof(f3561,plain,(
% 125.36/20.75 $false),
% 125.36/20.75 inference(forward_subsumption_resolution,[status(thm)],[f3560,f250])).
% 125.36/20.75 % SZS output end CNFRefutation for theBenchmark.p
% 125.36/20.77 % Elapsed time: 20.313041 seconds
% 125.36/20.77 % CPU time: 160.417071 seconds
% 125.36/20.77 % Total memory used: 492.759 MB
% 125.36/20.77 % Net memory used: 426.871 MB
%------------------------------------------------------------------------------