%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET711+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 : n011.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 148.33s 19.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET711+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.18/0.44 % Computer : n011.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 05:33:10 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 148.33/19.30 % Refutation found
% 148.33/19.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 148.33/19.30 % SZS output start CNFRefutation for theBenchmark
% 148.33/19.30 fof(f15,axiom,(
% 148.33/19.30 (! [F,G,A,B] :( equal_maps(F,G,A,B)<=> (! [X,Y1,Y2] :( ( member(X,A)& member(Y1,B)& member(Y2,B) )=> ( ( apply(F,X,Y1)& apply(G,X,Y2) )=> Y1 = Y2 ) ) )) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f17,axiom,(
% 148.33/19.30 (! [F,A,B] :( injective(F,A,B)<=> (! [X1,X2,Y] :( ( member(X1,A)& member(X2,A)& member(Y,B) )=> ( ( apply(F,X1,Y)& apply(F,X2,Y) )=> X1 = X2 ) ) )) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f18,axiom,(
% 148.33/19.30 (! [F,A,B] :( surjective(F,A,B)<=> (! [Y] :( member(Y,B)=> (? [E] :( member(E,A)& apply(F,E,Y) ) )) )) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f19,axiom,(
% 148.33/19.30 (! [F,A,B] :( one_to_one(F,A,B)<=> ( injective(F,A,B)& surjective(F,A,B) ) ) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f20,axiom,(
% 148.33/19.30 (! [G,F,A,B] :( inverse_predicate(G,F,A,B)<=> (! [X,Y] :( ( member(X,A)& member(Y,B) )=> ( apply(F,X,Y)<=> apply(G,Y,X) ) ) )) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f29,conjecture,(
% 148.33/19.30 (! [F,G,H,A,B] :( ( maps(F,A,B)& one_to_one(F,A,B)& inverse_predicate(G,F,A,B)& inverse_predicate(H,F,A,B) )=> equal_maps(G,H,B,A) ) )),
% 148.33/19.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 148.33/19.30 fof(f30,negated_conjecture,(
% 148.33/19.30 ~((! [F,G,H,A,B] :( ( maps(F,A,B)& one_to_one(F,A,B)& inverse_predicate(G,F,A,B)& inverse_predicate(H,F,A,B) )=> equal_maps(G,H,B,A) ) ))),
% 148.33/19.30 inference(negated_conjecture,[status(cth)],[f29])).
% 148.33/19.30 fof(f119,plain,(
% 148.33/19.30 ![F,G,A,B]: (equal_maps(F,G,A,B)<=>(![X,Y1,Y2]: (((~member(X,A)|~member(Y1,B))|~member(Y2,B))|((~apply(F,X,Y1)|~apply(G,X,Y2))|Y1=Y2))))),
% 148.33/19.30 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 148.33/19.30 fof(f120,plain,(
% 148.33/19.30 ![F,G,A,B]: ((~equal_maps(F,G,A,B)|(![X,Y1,Y2]: (((~member(X,A)|~member(Y1,B))|~member(Y2,B))|((~apply(F,X,Y1)|~apply(G,X,Y2))|Y1=Y2))))&(equal_maps(F,G,A,B)|(?[X,Y1,Y2]: (((member(X,A)&member(Y1,B))&member(Y2,B))&((apply(F,X,Y1)&apply(G,X,Y2))&~Y1=Y2)))))),
% 148.33/19.30 inference(NNF_transformation,[status(thm)],[f119])).
% 148.33/19.30 fof(f121,plain,(
% 148.33/19.30 (![F,G,A,B]: (~equal_maps(F,G,A,B)|(![X,Y1,Y2]: (((~member(X,A)|~member(Y1,B))|~member(Y2,B))|((~apply(F,X,Y1)|~apply(G,X,Y2))|Y1=Y2)))))&(![F,G,A,B]: (equal_maps(F,G,A,B)|(?[X,Y1,Y2]: (((member(X,A)&member(Y1,B))&member(Y2,B))&((apply(F,X,Y1)&apply(G,X,Y2))&~Y1=Y2)))))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f120])).
% 148.33/19.30 fof(f122,plain,(
% 148.33/19.30 (![F,G,A,B]: (~equal_maps(F,G,A,B)|(![X,Y1,Y2]: (((~member(X,A)|~member(Y1,B))|~member(Y2,B))|((~apply(F,X,Y1)|~apply(G,X,Y2))|Y1=Y2)))))&(![F,G,A,B]: (equal_maps(F,G,A,B)|(((member(sK12_skl(B,A,G,F),A)&member(sK13_skl(B,A,G,F),B))&member(sK14_skl(B,A,G,F),B))&((apply(F,sK12_skl(B,A,G,F),sK13_skl(B,A,G,F))&apply(G,sK12_skl(B,A,G,F),sK14_skl(B,A,G,F)))&~sK13_skl(B,A,G,F)=sK14_skl(B,A,G,F)))))),
% 148.33/19.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X,sK12_skl(B,A,G,F)),skolemize(Y1,sK13_skl(B,A,G,F)),skolemize(Y2,sK14_skl(B,A,G,F))],[f121])).
% 148.33/19.30 fof(f124,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|member(sK12_skl(X3,X2,X1,X0),X2))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f125,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|member(sK13_skl(X3,X2,X1,X0),X3))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f126,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|member(sK14_skl(X3,X2,X1,X0),X3))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f127,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|apply(X0,sK12_skl(X3,X2,X1,X0),sK13_skl(X3,X2,X1,X0)))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f128,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|apply(X1,sK12_skl(X3,X2,X1,X0),sK14_skl(X3,X2,X1,X0)))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f129,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (equal_maps(X0,X1,X2,X3)|~sK13_skl(X3,X2,X1,X0)=sK14_skl(X3,X2,X1,X0))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f122])).
% 148.33/19.30 fof(f137,plain,(
% 148.33/19.30 ![F,A,B]: (injective(F,A,B)<=>(![X1,X2,Y]: (((~member(X1,A)|~member(X2,A))|~member(Y,B))|((~apply(F,X1,Y)|~apply(F,X2,Y))|X1=X2))))),
% 148.33/19.30 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 148.33/19.30 fof(f138,plain,(
% 148.33/19.30 ![F,A,B]: ((~injective(F,A,B)|(![X1,X2,Y]: (((~member(X1,A)|~member(X2,A))|~member(Y,B))|((~apply(F,X1,Y)|~apply(F,X2,Y))|X1=X2))))&(injective(F,A,B)|(?[X1,X2,Y]: (((member(X1,A)&member(X2,A))&member(Y,B))&((apply(F,X1,Y)&apply(F,X2,Y))&~X1=X2)))))),
% 148.33/19.30 inference(NNF_transformation,[status(thm)],[f137])).
% 148.33/19.30 fof(f139,plain,(
% 148.33/19.30 (![F,A,B]: (~injective(F,A,B)|(![X1,X2,Y]: (((~member(X1,A)|~member(X2,A))|~member(Y,B))|((~apply(F,X1,Y)|~apply(F,X2,Y))|X1=X2)))))&(![F,A,B]: (injective(F,A,B)|(?[X1,X2,Y]: (((member(X1,A)&member(X2,A))&member(Y,B))&((apply(F,X1,Y)&apply(F,X2,Y))&~X1=X2)))))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f138])).
% 148.33/19.30 fof(f140,plain,(
% 148.33/19.30 (![F,A,B]: (~injective(F,A,B)|(![X1,X2,Y]: (((~member(X1,A)|~member(X2,A))|~member(Y,B))|((~apply(F,X1,Y)|~apply(F,X2,Y))|X1=X2)))))&(![F,A,B]: (injective(F,A,B)|(((member(sK16_skl(B,A,F),A)&member(sK17_skl(B,A,F),A))&member(sK18_skl(B,A,F),B))&((apply(F,sK16_skl(B,A,F),sK18_skl(B,A,F))&apply(F,sK17_skl(B,A,F),sK18_skl(B,A,F)))&~sK16_skl(B,A,F)=sK17_skl(B,A,F)))))),
% 148.33/19.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X1,sK16_skl(B,A,F)),skolemize(X2,sK17_skl(B,A,F)),skolemize(Y,sK18_skl(B,A,F))],[f139])).
% 148.33/19.30 fof(f141,plain,(
% 148.33/19.30 ![X0,X1,X2,X3,X4,X5]: (~injective(X0,X1,X2)|~member(X3,X1)|~member(X4,X1)|~member(X5,X2)|~apply(X0,X3,X5)|~apply(X0,X4,X5)|X3=X4)),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f140])).
% 148.33/19.30 fof(f148,plain,(
% 148.33/19.30 ![F,A,B]: (surjective(F,A,B)<=>(![Y]: (~member(Y,B)|(?[E]: (member(E,A)&apply(F,E,Y))))))),
% 148.33/19.30 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 148.33/19.30 fof(f149,plain,(
% 148.33/19.30 ![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)))))))),
% 148.33/19.30 inference(NNF_transformation,[status(thm)],[f148])).
% 148.33/19.30 fof(f150,plain,(
% 148.33/19.30 (![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)))))))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f149])).
% 148.33/19.30 fof(f151,plain,(
% 148.33/19.30 (![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)))))))),
% 148.33/19.30 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])).
% 148.33/19.30 fof(f152,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (~surjective(X0,X1,X2)|~member(X3,X2)|member(sK19_skl(X3,X2,X1,X0),X1))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f151])).
% 148.33/19.30 fof(f153,plain,(
% 148.33/19.30 ![X0,X1,X2,X3]: (~surjective(X0,X1,X2)|~member(X3,X2)|apply(X0,sK19_skl(X3,X2,X1,X0),X3))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f151])).
% 148.33/19.30 fof(f156,plain,(
% 148.33/19.30 ![F,A,B]: ((~one_to_one(F,A,B)|(injective(F,A,B)&surjective(F,A,B)))&(one_to_one(F,A,B)|(~injective(F,A,B)|~surjective(F,A,B))))),
% 148.33/19.30 inference(NNF_transformation,[status(thm)],[f19])).
% 148.33/19.30 fof(f157,plain,(
% 148.33/19.30 (![F,A,B]: (~one_to_one(F,A,B)|(injective(F,A,B)&surjective(F,A,B))))&(![F,A,B]: (one_to_one(F,A,B)|(~injective(F,A,B)|~surjective(F,A,B))))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f156])).
% 148.33/19.30 fof(f158,plain,(
% 148.33/19.30 ![X0,X1,X2]: (~one_to_one(X0,X1,X2)|injective(X0,X1,X2))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f157])).
% 148.33/19.30 fof(f159,plain,(
% 148.33/19.30 ![X0,X1,X2]: (~one_to_one(X0,X1,X2)|surjective(X0,X1,X2))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f157])).
% 148.33/19.30 fof(f161,plain,(
% 148.33/19.30 ![G,F,A,B]: (inverse_predicate(G,F,A,B)<=>(![X,Y]: ((~member(X,A)|~member(Y,B))|(apply(F,X,Y)<=>apply(G,Y,X)))))),
% 148.33/19.30 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 148.33/19.30 fof(f162,plain,(
% 148.33/19.30 ![G,F,A,B]: ((~inverse_predicate(G,F,A,B)|(![X,Y]: ((~member(X,A)|~member(Y,B))|((~apply(F,X,Y)|apply(G,Y,X))&(apply(F,X,Y)|~apply(G,Y,X))))))&(inverse_predicate(G,F,A,B)|(?[X,Y]: ((member(X,A)&member(Y,B))&((~apply(F,X,Y)|~apply(G,Y,X))&(apply(F,X,Y)|apply(G,Y,X)))))))),
% 148.33/19.30 inference(NNF_transformation,[status(thm)],[f161])).
% 148.33/19.30 fof(f163,plain,(
% 148.33/19.30 (![G,F,A,B]: (~inverse_predicate(G,F,A,B)|(![X,Y]: ((~member(X,A)|~member(Y,B))|((~apply(F,X,Y)|apply(G,Y,X))&(apply(F,X,Y)|~apply(G,Y,X)))))))&(![G,F,A,B]: (inverse_predicate(G,F,A,B)|(?[X,Y]: ((member(X,A)&member(Y,B))&((~apply(F,X,Y)|~apply(G,Y,X))&(apply(F,X,Y)|apply(G,Y,X)))))))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f162])).
% 148.33/19.30 fof(f164,plain,(
% 148.33/19.30 (![G,F,A,B]: (~inverse_predicate(G,F,A,B)|(![X,Y]: ((~member(X,A)|~member(Y,B))|((~apply(F,X,Y)|apply(G,Y,X))&(apply(F,X,Y)|~apply(G,Y,X)))))))&(![G,F,A,B]: (inverse_predicate(G,F,A,B)|((member(sK21_skl(B,A,F,G),A)&member(sK22_skl(B,A,F,G),B))&((~apply(F,sK21_skl(B,A,F,G),sK22_skl(B,A,F,G))|~apply(G,sK22_skl(B,A,F,G),sK21_skl(B,A,F,G)))&(apply(F,sK21_skl(B,A,F,G),sK22_skl(B,A,F,G))|apply(G,sK22_skl(B,A,F,G),sK21_skl(B,A,F,G)))))))),
% 148.33/19.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl(B,A,F,G)),skolemize(Y,sK22_skl(B,A,F,G))],[f163])).
% 148.33/19.30 fof(f166,plain,(
% 148.33/19.30 ![X0,X1,X2,X3,X4,X5]: (~inverse_predicate(X0,X1,X2,X3)|~member(X4,X2)|~member(X5,X3)|apply(X1,X4,X5)|~apply(X0,X5,X4))),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f164])).
% 148.33/19.30 fof(f244,plain,(
% 148.33/19.30 (?[F,G,H,A,B]: ((((maps(F,A,B)&one_to_one(F,A,B))&inverse_predicate(G,F,A,B))&inverse_predicate(H,F,A,B))&~equal_maps(G,H,B,A)))),
% 148.33/19.30 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 148.33/19.30 fof(f245,plain,(
% 148.33/19.30 ?[G,H,A,B]: ((?[F]: (((maps(F,A,B)&one_to_one(F,A,B))&inverse_predicate(G,F,A,B))&inverse_predicate(H,F,A,B)))&~equal_maps(G,H,B,A))),
% 148.33/19.30 inference(miniscoping,[status(thm)],[f244])).
% 148.33/19.30 fof(f246,plain,(
% 148.33/19.30 ((((maps(sK43_skl,sK41_skl,sK42_skl)&one_to_one(sK43_skl,sK41_skl,sK42_skl))&inverse_predicate(sK39_skl,sK43_skl,sK41_skl,sK42_skl))&inverse_predicate(sK40_skl,sK43_skl,sK41_skl,sK42_skl))&~equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl))),
% 148.33/19.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl]),skolemize(G,sK39_skl),skolemize(H,sK40_skl),skolemize(A,sK41_skl),skolemize(B,sK42_skl),skolemize(F,sK43_skl)],[f245])).
% 148.33/19.30 fof(f248,plain,(
% 148.33/19.30 one_to_one(sK43_skl,sK41_skl,sK42_skl)),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f246])).
% 148.33/19.30 fof(f249,plain,(
% 148.33/19.30 inverse_predicate(sK39_skl,sK43_skl,sK41_skl,sK42_skl)),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f246])).
% 148.33/19.30 fof(f250,plain,(
% 148.33/19.30 inverse_predicate(sK40_skl,sK43_skl,sK41_skl,sK42_skl)),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f246])).
% 148.33/19.30 fof(f251,plain,(
% 148.33/19.30 ~equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl)),
% 148.33/19.30 inference(cnf_transformation,[status(thm)],[f246])).
% 148.33/19.30 fof(f270,plain,(
% 148.33/19.30 ![X0,X1]: (~member(X0,sK41_skl)|~member(X1,sK42_skl)|apply(sK43_skl,X0,X1)|~apply(sK40_skl,X1,X0))),
% 148.33/19.30 inference(resolution,[status(thm)],[f166,f250])).
% 148.33/19.30 fof(f271,plain,(
% 148.33/19.30 ![X0,X1]: (~member(X0,sK41_skl)|~member(X1,sK42_skl)|apply(sK43_skl,X0,X1)|~apply(sK39_skl,X1,X0))),
% 148.33/19.30 inference(resolution,[status(thm)],[f166,f249])).
% 148.33/19.30 fof(f292,plain,(
% 148.33/19.30 ![X0,X1,X2]: (equal_maps(sK39_skl,X0,X1,X2)|~member(sK13_skl(X2,X1,X0,sK39_skl),sK41_skl)|~member(sK12_skl(X2,X1,X0,sK39_skl),sK42_skl)|apply(sK43_skl,sK13_skl(X2,X1,X0,sK39_skl),sK12_skl(X2,X1,X0,sK39_skl)))),
% 148.33/19.30 inference(resolution,[status(thm)],[f127,f271])).
% 148.33/19.30 fof(f297,plain,(
% 148.33/19.30 ![X0,X1]: (equal_maps(sK39_skl,X0,X1,sK41_skl)|~member(sK12_skl(sK41_skl,X1,X0,sK39_skl),sK42_skl)|apply(sK43_skl,sK13_skl(sK41_skl,X1,X0,sK39_skl),sK12_skl(sK41_skl,X1,X0,sK39_skl))|equal_maps(sK39_skl,X0,X1,sK41_skl))),
% 148.33/19.30 inference(resolution,[status(thm)],[f292,f125])).
% 148.33/19.30 fof(f298,plain,(
% 148.33/19.30 ![X0,X1]: (equal_maps(sK39_skl,X0,X1,sK41_skl)|~member(sK12_skl(sK41_skl,X1,X0,sK39_skl),sK42_skl)|apply(sK43_skl,sK13_skl(sK41_skl,X1,X0,sK39_skl),sK12_skl(sK41_skl,X1,X0,sK39_skl)))),
% 148.33/19.30 inference(duplicate_literals_removal,[status(thm)],[f297])).
% 148.33/19.30 fof(f301,plain,(
% 148.33/19.30 ![X0]: (equal_maps(sK39_skl,X0,sK42_skl,sK41_skl)|apply(sK43_skl,sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK12_skl(sK41_skl,sK42_skl,X0,sK39_skl))|equal_maps(sK39_skl,X0,sK42_skl,sK41_skl))),
% 148.33/19.30 inference(resolution,[status(thm)],[f298,f124])).
% 148.33/19.31 fof(f302,plain,(
% 148.33/19.31 ![X0]: (equal_maps(sK39_skl,X0,sK42_skl,sK41_skl)|apply(sK43_skl,sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK12_skl(sK41_skl,sK42_skl,X0,sK39_skl)))),
% 148.33/19.31 inference(duplicate_literals_removal,[status(thm)],[f301])).
% 148.33/19.31 fof(f325,plain,(
% 148.33/19.31 ![X0,X1,X2]: (equal_maps(X0,sK40_skl,X1,X2)|~member(sK14_skl(X2,X1,sK40_skl,X0),sK41_skl)|~member(sK12_skl(X2,X1,sK40_skl,X0),sK42_skl)|apply(sK43_skl,sK14_skl(X2,X1,sK40_skl,X0),sK12_skl(X2,X1,sK40_skl,X0)))),
% 148.33/19.31 inference(resolution,[status(thm)],[f128,f270])).
% 148.33/19.31 fof(f417,plain,(
% 148.33/19.31 ![X0,X1]: (equal_maps(X0,sK40_skl,X1,sK41_skl)|~member(sK12_skl(sK41_skl,X1,sK40_skl,X0),sK42_skl)|apply(sK43_skl,sK14_skl(sK41_skl,X1,sK40_skl,X0),sK12_skl(sK41_skl,X1,sK40_skl,X0))|equal_maps(X0,sK40_skl,X1,sK41_skl))),
% 148.33/19.31 inference(resolution,[status(thm)],[f325,f126])).
% 148.33/19.31 fof(f418,plain,(
% 148.33/19.31 ![X0,X1]: (equal_maps(X0,sK40_skl,X1,sK41_skl)|~member(sK12_skl(sK41_skl,X1,sK40_skl,X0),sK42_skl)|apply(sK43_skl,sK14_skl(sK41_skl,X1,sK40_skl,X0),sK12_skl(sK41_skl,X1,sK40_skl,X0)))),
% 148.33/19.31 inference(duplicate_literals_removal,[status(thm)],[f417])).
% 148.33/19.31 fof(f523,plain,(
% 148.33/19.31 ![X0]: (equal_maps(X0,sK40_skl,sK42_skl,sK41_skl)|apply(sK43_skl,sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK12_skl(sK41_skl,sK42_skl,sK40_skl,X0))|equal_maps(X0,sK40_skl,sK42_skl,sK41_skl))),
% 148.33/19.31 inference(resolution,[status(thm)],[f418,f124])).
% 148.33/19.31 fof(f526,plain,(
% 148.33/19.31 ![X0]: (equal_maps(X0,sK40_skl,sK42_skl,sK41_skl)|apply(sK43_skl,sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK12_skl(sK41_skl,sK42_skl,sK40_skl,X0)))),
% 148.33/19.31 inference(duplicate_literals_removal,[status(thm)],[f523])).
% 148.33/19.31 fof(f947,plain,(
% 148.33/19.31 injective(sK43_skl,sK41_skl,sK42_skl)),
% 148.33/19.31 inference(resolution,[status(thm)],[f158,f248])).
% 148.33/19.31 fof(f1239,plain,(
% 148.33/19.31 surjective(sK43_skl,sK41_skl,sK42_skl)),
% 148.33/19.31 inference(resolution,[status(thm)],[f159,f248])).
% 148.33/19.31 fof(f1240,plain,(
% 148.33/19.31 ![X0]: (~member(X0,sK42_skl)|apply(sK43_skl,sK19_skl(X0,sK42_skl,sK41_skl,sK43_skl),X0))),
% 148.33/19.31 inference(resolution,[status(thm)],[f1239,f153])).
% 148.33/19.31 fof(f1371,plain,(
% 148.33/19.31 ![X0,X1,X2]: (apply(sK43_skl,sK19_skl(sK12_skl(X0,sK42_skl,X1,X2),sK42_skl,sK41_skl,sK43_skl),sK12_skl(X0,sK42_skl,X1,X2))|equal_maps(X2,X1,sK42_skl,X0))),
% 148.33/19.31 inference(resolution,[status(thm)],[f1240,f124])).
% 148.33/19.31 fof(f3017,plain,(
% 148.33/19.31 ![X0,X1,X2]: (~member(X0,sK41_skl)|~member(X1,sK41_skl)|~member(X2,sK42_skl)|~apply(sK43_skl,X0,X2)|~apply(sK43_skl,X1,X2)|X0=X1)),
% 148.33/19.31 inference(resolution,[status(thm)],[f141,f947])).
% 148.33/19.31 fof(f3025,plain,(
% 148.33/19.31 ![X0,X1,X2,X3]: (~member(X0,sK41_skl)|~member(sK19_skl(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl,sK41_skl,sK43_skl),sK41_skl)|~member(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl)|~apply(sK43_skl,X0,sK12_skl(X1,sK42_skl,X2,X3))|X0=sK19_skl(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X3,X2,sK42_skl,X1))),
% 148.33/19.31 inference(resolution,[status(thm)],[f3017,f1371])).
% 148.33/19.31 fof(f3057,plain,(
% 148.33/19.31 ![X0,X1,X2,X3]: (~member(X0,sK41_skl)|~member(sK19_skl(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl,sK41_skl,sK43_skl),sK41_skl)|~apply(sK43_skl,X0,sK12_skl(X1,sK42_skl,X2,X3))|X0=sK19_skl(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X3,X2,sK42_skl,X1))),
% 148.33/19.31 inference(forward_subsumption_resolution,[status(thm)],[f3025,f124])).
% 148.33/19.31 fof(f4504,plain,(
% 148.33/19.31 ![X0]: (~member(X0,sK42_skl)|member(sK19_skl(X0,sK42_skl,sK41_skl,sK43_skl),sK41_skl))),
% 148.33/19.31 inference(resolution,[status(thm)],[f152,f1239])).
% 148.33/19.31 fof(f4531,plain,(
% 148.33/19.31 ![X0,X1,X2]: (member(sK19_skl(sK12_skl(X0,sK42_skl,X1,X2),sK42_skl,sK41_skl,sK43_skl),sK41_skl)|equal_maps(X2,X1,sK42_skl,X0))),
% 148.33/19.31 inference(resolution,[status(thm)],[f4504,f124])).
% 148.33/19.31 fof(f4630,plain,(
% 148.33/19.31 ![X0,X1,X2,X3]: (~member(X0,sK41_skl)|~apply(sK43_skl,X0,sK12_skl(X1,sK42_skl,X2,X3))|X0=sK19_skl(sK12_skl(X1,sK42_skl,X2,X3),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X3,X2,sK42_skl,X1))),
% 148.33/19.31 inference(backward_subsumption_resolution,[status(thm)],[f3057,f4531])).
% 148.33/19.31 fof(f6522,plain,(
% 148.33/19.31 ![X0]: (~member(sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK41_skl)|sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X0,sK40_skl,sK42_skl,sK41_skl)|equal_maps(X0,sK40_skl,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(resolution,[status(thm)],[f4630,f526])).
% 148.33/19.34 fof(f6525,plain,(
% 148.33/19.34 ![X0]: (~member(sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK41_skl)|sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK42_skl,sK41_skl,sK43_skl)|equal_maps(sK39_skl,X0,sK42_skl,sK41_skl)|equal_maps(sK39_skl,X0,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(resolution,[status(thm)],[f4630,f302])).
% 148.33/19.34 fof(f6526,plain,(
% 148.33/19.34 ![X0]: (~member(sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK41_skl)|sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X0,sK40_skl,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(duplicate_literals_removal,[status(thm)],[f6522])).
% 148.33/19.34 fof(f6527,plain,(
% 148.33/19.34 ![X0]: (sK14_skl(sK41_skl,sK42_skl,sK40_skl,X0)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,sK40_skl,X0),sK42_skl,sK41_skl,sK43_skl)|equal_maps(X0,sK40_skl,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(forward_subsumption_resolution,[status(thm)],[f6526,f126])).
% 148.33/19.34 fof(f6532,plain,(
% 148.33/19.34 ![X0]: (~member(sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK41_skl)|sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK42_skl,sK41_skl,sK43_skl)|equal_maps(sK39_skl,X0,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(duplicate_literals_removal,[status(thm)],[f6525])).
% 148.33/19.34 fof(f6533,plain,(
% 148.33/19.34 ![X0]: (sK13_skl(sK41_skl,sK42_skl,X0,sK39_skl)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,X0,sK39_skl),sK42_skl,sK41_skl,sK43_skl)|equal_maps(sK39_skl,X0,sK42_skl,sK41_skl))),
% 148.33/19.34 inference(forward_subsumption_resolution,[status(thm)],[f6532,f125])).
% 148.33/19.34 fof(f6534,plain,(
% 148.33/19.34 sK14_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl),sK42_skl,sK41_skl,sK43_skl)),
% 148.33/19.34 inference(resolution,[status(thm)],[f6527,f251])).
% 148.33/19.34 fof(f6544,plain,(
% 148.33/19.34 sK13_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl)=sK19_skl(sK12_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl),sK42_skl,sK41_skl,sK43_skl)),
% 148.33/19.34 inference(resolution,[status(thm)],[f6533,f251])).
% 148.33/19.34 fof(f6546,plain,(
% 148.33/19.34 sK14_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl)=sK13_skl(sK41_skl,sK42_skl,sK40_skl,sK39_skl)),
% 148.33/19.34 inference(backward_demodulation,[status(thm)],[f6544,f6534])).
% 148.33/19.34 fof(f6548,plain,(
% 148.33/19.34 equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl)),
% 148.33/19.34 inference(resolution,[status(thm)],[f6546,f129])).
% 148.33/19.34 fof(f6554,plain,(
% 148.33/19.34 $false),
% 148.33/19.34 inference(forward_subsumption_resolution,[status(thm)],[f6548,f251])).
% 148.33/19.34 % SZS output end CNFRefutation for theBenchmark.p
% 15.58/19.42 % Elapsed time: 18.959072 seconds
% 15.58/19.42 % CPU time: 149.590991 seconds
% 15.58/19.42 % Total memory used: 522.708 MB
% 15.58/19.42 % Net memory used: 469.761 MB
%------------------------------------------------------------------------------