%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU221+3 : 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 : n005.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:22:02 PM UTC 2026
% Result : Theorem 0.22s 5.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU221+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.48 % Computer : n005.cluster.edu
% 0.17/5.48 % Model : x86_64 x86_64
% 0.17/5.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.48 % Memory : 8046.5625MB
% 0.17/5.48 % OS : Linux 6.8.0-71-generic
% 0.17/5.48 % CPULimit : 300
% 0.17/5.48 % WCLimit : 300
% 0.17/5.48 % DateTime : Mon Sep 21 05:59:53 UTC 2026
% 0.17/5.49 % CPUTime :
% 0.22/5.51 % Drodi V4.1.1
% 0.22/5.59 % Refutation found
% 0.22/5.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/5.59 % SZS output start CNFRefutation for theBenchmark
% 0.22/5.59 fof(f5,axiom,(
% 0.22/5.59 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)<=> (! [B,C] :( ( in(B,relation_dom(A))& in(C,relation_dom(A))& apply(A,B) = apply(A,C) )=> B = C ) )) ) )),
% 0.22/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/5.59 fof(f6,axiom,(
% 0.22/5.59 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.22/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/5.59 fof(f35,axiom,(
% 0.22/5.59 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> (! [B] :( ( relation(B)& function(B) )=> ( B = function_inverse(A)<=> ( relation_dom(B) = relation_rng(A)& (! [C,D] :( ( ( in(C,relation_rng(A))& D = apply(B,C) )=> ( in(D,relation_dom(A))& C = apply(A,D) ) )& ( ( in(D,relation_dom(A))& C = apply(A,D) )=> ( in(C,relation_rng(A))& D = apply(B,C) ) ) ) )) ) ) )) ) )),
% 0.22/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/5.59 fof(f36,axiom,(
% 0.22/5.59 (! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_rng(B)) )=> ( A = apply(B,apply(function_inverse(B),A))& A = apply(relation_composition(function_inverse(B),B),A) ) ) ) )),
% 0.22/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/5.59 fof(f38,conjecture,(
% 0.22/5.59 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> one_to_one(function_inverse(A)) ) ) )),
% 0.22/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/5.59 fof(f39,negated_conjecture,(
% 0.22/5.59 ~((! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> one_to_one(function_inverse(A)) ) ) ))),
% 0.22/5.59 inference(negated_conjecture,[status(cth)],[f38])).
% 0.22/5.59 fof(f53,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(one_to_one(A)<=>(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C))))),
% 0.22/5.59 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.22/5.59 fof(f54,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|((~one_to_one(A)|(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C)))&(one_to_one(A)|(?[B,C]: (((in(B,relation_dom(A))&in(C,relation_dom(A)))&apply(A,B)=apply(A,C))&~B=C)))))),
% 0.22/5.59 inference(NNF_transformation,[status(thm)],[f53])).
% 0.22/5.59 fof(f55,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|((~one_to_one(A)|(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C)))&(one_to_one(A)|(((in(sK0_skl(A),relation_dom(A))&in(sK1_skl(A),relation_dom(A)))&apply(A,sK0_skl(A))=apply(A,sK1_skl(A)))&~sK0_skl(A)=sK1_skl(A)))))),
% 0.22/5.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(B,sK0_skl(A)),skolemize(C,sK1_skl(A))],[f54])).
% 0.22/5.59 fof(f57,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK0_skl(X0),relation_dom(X0)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/5.59 fof(f58,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK1_skl(X0),relation_dom(X0)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/5.59 fof(f59,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|apply(X0,sK0_skl(X0))=apply(X0,sK1_skl(X0)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/5.59 fof(f60,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~sK0_skl(X0)=sK1_skl(X0))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f55])).
% 0.22/5.59 fof(f61,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.22/5.59 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.22/5.59 fof(f62,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f61])).
% 0.22/5.59 fof(f63,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f61])).
% 0.22/5.59 fof(f138,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|(B=function_inverse(A)<=>(relation_dom(B)=relation_rng(A)&(![C,D]: (((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D)))&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))))))),
% 0.22/5.59 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.22/5.59 fof(f139,definition,(
% 0.22/5.59 ![A,B,C,D]: (sP0_prd(D,C,B,A)<=>((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D))))),
% 0.22/5.59 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.22/5.59 fof(f140,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|(B=function_inverse(A)<=>(relation_dom(B)=relation_rng(A)&(![C,D]: (sP0_prd(D,C,B,A)&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))))))),
% 0.22/5.59 inference(formula_renaming,[status(thm)],[f138,f139])).
% 0.22/5.59 fof(f141,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&(![C,D]: (sP0_prd(D,C,B,A)&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|(?[C,D]: (~sP0_prd(D,C,B,A)|((in(D,relation_dom(A))&C=apply(A,D))&(~in(C,relation_rng(A))|~D=apply(B,C))))))))))))),
% 0.22/5.59 inference(NNF_transformation,[status(thm)],[f140])).
% 0.22/5.59 fof(f142,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&((![C,D]: sP0_prd(D,C,B,A))&(![C,D]: ((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|((?[C,D]: ~sP0_prd(D,C,B,A))|(?[C,D]: ((in(D,relation_dom(A))&C=apply(A,D))&(~in(C,relation_rng(A))|~D=apply(B,C))))))))))))),
% 0.22/5.59 inference(miniscoping,[status(thm)],[f141])).
% 0.22/5.59 fof(f143,plain,(
% 0.22/5.59 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&((![C,D]: sP0_prd(D,C,B,A))&(![C,D]: ((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|(~sP0_prd(sK14_skl(B,A),sK13_skl(B,A),B,A)|((in(sK16_skl(B,A),relation_dom(A))&sK15_skl(B,A)=apply(A,sK16_skl(B,A)))&(~in(sK15_skl(B,A),relation_rng(A))|~sK16_skl(B,A)=apply(B,sK15_skl(B,A))))))))))))),
% 0.22/5.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl,sK16_skl]),skolemize(C,sK13_skl(B,A)),skolemize(D,sK14_skl(B,A)),skolemize(C,sK15_skl(B,A)),skolemize(D,sK16_skl(B,A))],[f142])).
% 0.22/5.59 fof(f144,plain,(
% 0.22/5.59 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(X1)|~function(X1)|~X1=function_inverse(X0)|relation_dom(X1)=relation_rng(X0))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f143])).
% 0.22/5.59 fof(f151,plain,(
% 0.22/5.59 ![A,B]: ((~relation(B)|~function(B))|((~one_to_one(B)|~in(A,relation_rng(B)))|(A=apply(B,apply(function_inverse(B),A))&A=apply(relation_composition(function_inverse(B),B),A))))),
% 0.22/5.59 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.22/5.59 fof(f152,plain,(
% 0.22/5.59 ![B]: ((~relation(B)|~function(B))|(![A]: ((~one_to_one(B)|~in(A,relation_rng(B)))|(A=apply(B,apply(function_inverse(B),A))&A=apply(relation_composition(function_inverse(B),B),A)))))),
% 0.22/5.59 inference(miniscoping,[status(thm)],[f151])).
% 0.22/5.59 fof(f153,plain,(
% 0.22/5.59 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_rng(X0))|X1=apply(X0,apply(function_inverse(X0),X1)))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f152])).
% 0.22/5.59 fof(f158,plain,(
% 0.22/5.59 (?[A]: ((relation(A)&function(A))&(one_to_one(A)&~one_to_one(function_inverse(A)))))),
% 0.22/5.59 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.22/5.59 fof(f159,plain,(
% 0.22/5.59 ((relation(sK17_skl)&function(sK17_skl))&(one_to_one(sK17_skl)&~one_to_one(function_inverse(sK17_skl))))),
% 0.22/5.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f158])).
% 0.22/5.59 fof(f160,plain,(
% 0.22/5.59 relation(sK17_skl)),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f159])).
% 0.22/5.59 fof(f161,plain,(
% 0.22/5.59 function(sK17_skl)),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f159])).
% 0.22/5.59 fof(f162,plain,(
% 0.22/5.59 one_to_one(sK17_skl)),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f159])).
% 0.22/5.59 fof(f163,plain,(
% 0.22/5.59 ~one_to_one(function_inverse(sK17_skl))),
% 0.22/5.59 inference(cnf_transformation,[status(thm)],[f159])).
% 0.22/5.59 fof(f180,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(function_inverse(X0))|~function(function_inverse(X0))|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 0.22/5.59 inference(destructive_equality_resolution,[status(thm)],[f144])).
% 0.22/5.59 fof(f181,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~function(function_inverse(X0))|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f180,f62])).
% 0.22/5.59 fof(f191,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(function_inverse(X0))=relation_rng(X0)|~relation(X0)|~function(X0))),
% 0.22/5.59 inference(resolution,[status(thm)],[f181,f63])).
% 0.22/5.59 fof(f192,plain,(
% 0.22/5.59 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 0.22/5.59 inference(duplicate_literals_removal,[status(thm)],[f191])).
% 0.22/5.59 fof(f193,plain,(
% 0.22/5.59 ~relation(sK17_skl)|~function(sK17_skl)|relation_dom(function_inverse(sK17_skl))=relation_rng(sK17_skl)),
% 0.22/5.59 inference(resolution,[status(thm)],[f192,f162])).
% 0.22/5.59 fof(f194,plain,(
% 0.22/5.59 ~function(sK17_skl)|relation_dom(function_inverse(sK17_skl))=relation_rng(sK17_skl)),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f193,f160])).
% 0.22/5.59 fof(f195,plain,(
% 0.22/5.59 relation_dom(function_inverse(sK17_skl))=relation_rng(sK17_skl)),
% 0.22/5.59 inference(resolution,[status(thm)],[f194,f161])).
% 0.22/5.59 fof(f258,plain,(
% 0.22/5.59 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))|one_to_one(function_inverse(sK17_skl))|in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.59 inference(paramodulation,[status(thm)],[f195,f57])).
% 0.22/5.59 fof(f260,plain,(
% 0.22/5.59 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))|in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f258,f163])).
% 0.22/5.59 fof(f266,plain,(
% 0.22/5.59 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))|one_to_one(function_inverse(sK17_skl))|in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.59 inference(paramodulation,[status(thm)],[f195,f58])).
% 0.22/5.59 fof(f268,plain,(
% 0.22/5.59 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))|in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f266,f163])).
% 0.22/5.59 fof(f275,plain,(
% 0.22/5.59 ![X0]: (~relation(function_inverse(X0))|one_to_one(function_inverse(X0))|apply(function_inverse(X0),sK0_skl(function_inverse(X0)))=apply(function_inverse(X0),sK1_skl(function_inverse(X0)))|~relation(X0)|~function(X0))),
% 0.22/5.59 inference(resolution,[status(thm)],[f59,f63])).
% 0.22/5.59 fof(f278,plain,(
% 0.22/5.59 ![X0]: (one_to_one(function_inverse(X0))|apply(function_inverse(X0),sK0_skl(function_inverse(X0)))=apply(function_inverse(X0),sK1_skl(function_inverse(X0)))|~relation(X0)|~function(X0))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f275,f62])).
% 0.22/5.59 fof(f279,plain,(
% 0.22/5.59 ~relation(function_inverse(sK17_skl))|in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.59 inference(resolution,[status(thm)],[f260,f63])).
% 0.22/5.59 fof(f280,plain,(
% 0.22/5.59 in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f279,f62])).
% 0.22/5.59 fof(f281,plain,(
% 0.22/5.59 in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)),
% 0.22/5.59 inference(resolution,[status(thm)],[f280,f161])).
% 0.22/5.59 fof(f282,plain,(
% 0.22/5.59 in(sK0_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f281,f160])).
% 0.22/5.59 fof(f283,plain,(
% 0.22/5.59 ~relation(sK17_skl)|~function(sK17_skl)|~one_to_one(sK17_skl)|sK0_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK0_skl(function_inverse(sK17_skl))))),
% 0.22/5.59 inference(resolution,[status(thm)],[f282,f153])).
% 0.22/5.59 fof(f285,plain,(
% 0.22/5.59 ~function(sK17_skl)|~one_to_one(sK17_skl)|sK0_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK0_skl(function_inverse(sK17_skl))))),
% 0.22/5.59 inference(forward_subsumption_resolution,[status(thm)],[f283,f160])).
% 0.22/5.61 fof(f286,plain,(
% 0.22/5.61 ~relation(function_inverse(sK17_skl))|in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.61 inference(resolution,[status(thm)],[f268,f63])).
% 0.22/5.61 fof(f287,plain,(
% 0.22/5.61 in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f286,f62])).
% 0.22/5.61 fof(f322,plain,(
% 0.22/5.61 apply(function_inverse(sK17_skl),sK0_skl(function_inverse(sK17_skl)))=apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl)))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.61 inference(resolution,[status(thm)],[f278,f163])).
% 0.22/5.61 fof(f326,plain,(
% 0.22/5.61 apply(function_inverse(sK17_skl),sK0_skl(function_inverse(sK17_skl)))=apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl)))|~function(sK17_skl)),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f322,f160])).
% 0.22/5.61 fof(f479,plain,(
% 0.22/5.61 in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))|~relation(sK17_skl)),
% 0.22/5.61 inference(resolution,[status(thm)],[f287,f161])).
% 0.22/5.61 fof(f480,plain,(
% 0.22/5.61 in(sK1_skl(function_inverse(sK17_skl)),relation_rng(sK17_skl))),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f479,f160])).
% 0.22/5.61 fof(f481,plain,(
% 0.22/5.61 ~relation(sK17_skl)|~function(sK17_skl)|~one_to_one(sK17_skl)|sK1_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl))))),
% 0.22/5.61 inference(resolution,[status(thm)],[f480,f153])).
% 0.22/5.61 fof(f483,plain,(
% 0.22/5.61 ~function(sK17_skl)|~one_to_one(sK17_skl)|sK1_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl))))),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f481,f160])).
% 0.22/5.61 fof(f484,plain,(
% 0.22/5.61 apply(function_inverse(sK17_skl),sK0_skl(function_inverse(sK17_skl)))=apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl)))),
% 0.22/5.61 inference(resolution,[status(thm)],[f326,f161])).
% 0.22/5.61 fof(f486,plain,(
% 0.22/5.61 ~function(sK17_skl)|~one_to_one(sK17_skl)|sK0_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl))))),
% 0.22/5.61 inference(backward_demodulation,[status(thm)],[f484,f285])).
% 0.22/5.61 fof(f487,plain,(
% 0.22/5.61 ~one_to_one(sK17_skl)|sK0_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl))))),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f486,f161])).
% 0.22/5.61 fof(f493,plain,(
% 0.22/5.61 sK0_skl(function_inverse(sK17_skl))=apply(sK17_skl,apply(function_inverse(sK17_skl),sK1_skl(function_inverse(sK17_skl))))),
% 0.22/5.61 inference(resolution,[status(thm)],[f487,f162])).
% 0.22/5.61 fof(f495,plain,(
% 0.22/5.61 ~function(sK17_skl)|~one_to_one(sK17_skl)|sK1_skl(function_inverse(sK17_skl))=sK0_skl(function_inverse(sK17_skl))),
% 0.22/5.61 inference(backward_demodulation,[status(thm)],[f493,f483])).
% 0.22/5.61 fof(f496,plain,(
% 0.22/5.61 ~one_to_one(sK17_skl)|sK1_skl(function_inverse(sK17_skl))=sK0_skl(function_inverse(sK17_skl))),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f495,f161])).
% 0.22/5.61 fof(f497,plain,(
% 0.22/5.61 sK1_skl(function_inverse(sK17_skl))=sK0_skl(function_inverse(sK17_skl))),
% 0.22/5.61 inference(resolution,[status(thm)],[f496,f162])).
% 0.22/5.61 fof(f503,plain,(
% 0.22/5.61 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))|one_to_one(function_inverse(sK17_skl))),
% 0.22/5.61 inference(resolution,[status(thm)],[f497,f60])).
% 0.22/5.61 fof(f506,plain,(
% 0.22/5.61 ~relation(function_inverse(sK17_skl))|~function(function_inverse(sK17_skl))),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f503,f163])).
% 0.22/5.61 fof(f509,plain,(
% 0.22/5.61 ~relation(function_inverse(sK17_skl))|~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.61 inference(resolution,[status(thm)],[f506,f63])).
% 0.22/5.61 fof(f510,plain,(
% 0.22/5.61 ~relation(sK17_skl)|~function(sK17_skl)),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f509,f62])).
% 0.22/5.61 fof(f511,plain,(
% 0.22/5.61 ~relation(sK17_skl)),
% 0.22/5.61 inference(resolution,[status(thm)],[f510,f161])).
% 0.22/5.61 fof(f512,plain,(
% 0.22/5.61 $false),
% 0.22/5.61 inference(forward_subsumption_resolution,[status(thm)],[f511,f160])).
% 0.22/5.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/5.61 % Elapsed time: 0.118698 seconds
% 0.22/5.61 % CPU time: 0.401215 seconds
% 0.22/5.61 % Total memory used: 41.823 MB
% 0.22/5.61 % Net memory used: 41.280 MB
%------------------------------------------------------------------------------