%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU072+1 : 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 : n018.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:21:39 PM UTC 2026
% Result : Theorem 0.23s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU072+1 : 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.20/0.45 % Computer : n018.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 05:51:14 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 0.23/0.73 % Refutation found
% 0.23/0.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.73 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.73 fof(f5,axiom,(
% 0.23/0.73 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] :( in(D,relation_dom(A))& C = apply(A,D) ) )) )) )) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f6,axiom,(
% 0.23/0.73 (! [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.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f21,axiom,(
% 0.23/0.73 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f27,axiom,(
% 0.23/0.73 (! [A,B] : subset(A,A) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f28,axiom,(
% 0.23/0.73 (! [A,B] :( ( relation(B)& function(B) )=> ( in(A,relation_dom(B))=> relation_image(B,singleton(A)) = singleton(apply(B,A)) ) ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f29,axiom,(
% 0.23/0.73 (! [A,B] :( relation(B)=> ( in(A,relation_rng(B))<=> relation_inverse_image(B,singleton(A)) != empty_set ) ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f30,conjecture,(
% 0.23/0.73 (! [A] :( ( relation(A)& function(A) )=> ( (! [B] : subset(relation_inverse_image(A,relation_image(A,B)),B))=> one_to_one(A) ) ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f31,negated_conjecture,(
% 0.23/0.73 ~((! [A] :( ( relation(A)& function(A) )=> ( (! [B] : subset(relation_inverse_image(A,relation_image(A,B)),B))=> one_to_one(A) ) ) ))),
% 0.23/0.73 inference(negated_conjecture,[status(cth)],[f30])).
% 0.23/0.73 fof(f34,axiom,(
% 0.23/0.73 (! [A,B] :( subset(A,singleton(B))<=> ( A = empty_set| A = singleton(B) ) ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f38,axiom,(
% 0.23/0.73 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f39,axiom,(
% 0.23/0.73 (! [A,B] :( subset(singleton(A),singleton(B))=> A = B ) )),
% 0.23/0.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.73 fof(f52,plain,(
% 0.23/0.73 ![A]: ((~relation(A)|~function(A))|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.23/0.73 fof(f53,plain,(
% 0.23/0.73 ![A]: ((~relation(A)|~function(A))|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))&(in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D)))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))&(in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))))),
% 0.23/0.73 inference(NNF_transformation,[status(thm)],[f52])).
% 0.23/0.73 fof(f54,plain,(
% 0.23/0.73 ![A]: ((~relation(A)|~function(A))|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D)))))&(![C]: (in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))&(in(C,B)|(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))))),
% 0.23/0.73 inference(miniscoping,[status(thm)],[f53])).
% 0.23/0.73 fof(f55,plain,(
% 0.23/0.73 ![A]: ((~relation(A)|~function(A))|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(in(sK0_skl(C,B,A),relation_dom(A))&C=apply(A,sK0_skl(C,B,A)))))&(![C]: (in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))))))&(![B]: (B=relation_rng(A)|((~in(sK1_skl(B,A),B)|(![D]: (~in(D,relation_dom(A))|~sK1_skl(B,A)=apply(A,D))))&(in(sK1_skl(B,A),B)|(in(sK2_skl(B,A),relation_dom(A))&sK1_skl(B,A)=apply(A,sK2_skl(B,A)))))))))),
% 0.23/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(C,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f54])).
% 0.23/0.73 fof(f58,plain,(
% 0.23/0.73 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(X3,relation_dom(X0))|~X2=apply(X0,X3))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f55])).
% 0.23/0.73 fof(f62,plain,(
% 0.23/0.73 ![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.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.23/0.73 fof(f63,plain,(
% 0.23/0.73 ![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.23/0.73 inference(NNF_transformation,[status(thm)],[f62])).
% 0.23/0.73 fof(f64,plain,(
% 0.23/0.73 ![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(sK3_skl(A),relation_dom(A))&in(sK4_skl(A),relation_dom(A)))&apply(A,sK3_skl(A))=apply(A,sK4_skl(A)))&~sK3_skl(A)=sK4_skl(A)))))),
% 0.23/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(B,sK3_skl(A)),skolemize(C,sK4_skl(A))],[f63])).
% 0.23/0.73 fof(f66,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK3_skl(X0),relation_dom(X0)))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f64])).
% 0.23/0.73 fof(f67,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK4_skl(X0),relation_dom(X0)))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f64])).
% 0.23/0.73 fof(f68,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|apply(X0,sK3_skl(X0))=apply(X0,sK4_skl(X0)))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f64])).
% 0.23/0.73 fof(f69,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~sK3_skl(X0)=sK4_skl(X0))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f64])).
% 0.23/0.73 fof(f102,plain,(
% 0.23/0.73 ((relation(sK10_skl)&empty(sK10_skl))&function(sK10_skl))),
% 0.23/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f21])).
% 0.23/0.73 fof(f104,plain,(
% 0.23/0.73 empty(sK10_skl)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f102])).
% 0.23/0.73 fof(f121,plain,(
% 0.23/0.73 ![A]: subset(A,A)),
% 0.23/0.73 inference(miniscoping,[status(thm)],[f27])).
% 0.23/0.73 fof(f122,plain,(
% 0.23/0.73 ![X0]: (subset(X0,X0))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f121])).
% 0.23/0.73 fof(f123,plain,(
% 0.23/0.73 ![A,B]: ((~relation(B)|~function(B))|(~in(A,relation_dom(B))|relation_image(B,singleton(A))=singleton(apply(B,A))))),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.23/0.73 fof(f124,plain,(
% 0.23/0.73 ![B]: ((~relation(B)|~function(B))|(![A]: (~in(A,relation_dom(B))|relation_image(B,singleton(A))=singleton(apply(B,A)))))),
% 0.23/0.73 inference(miniscoping,[status(thm)],[f123])).
% 0.23/0.73 fof(f125,plain,(
% 0.23/0.73 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|relation_image(X0,singleton(X1))=singleton(apply(X0,X1)))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f124])).
% 0.23/0.73 fof(f126,plain,(
% 0.23/0.73 ![A,B]: (~relation(B)|(in(A,relation_rng(B))<=>~relation_inverse_image(B,singleton(A))=empty_set))),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.23/0.73 fof(f127,plain,(
% 0.23/0.73 ![A,B]: (~relation(B)|((~in(A,relation_rng(B))|~relation_inverse_image(B,singleton(A))=empty_set)&(in(A,relation_rng(B))|relation_inverse_image(B,singleton(A))=empty_set)))),
% 0.23/0.73 inference(NNF_transformation,[status(thm)],[f126])).
% 0.23/0.73 fof(f128,plain,(
% 0.23/0.73 ![B]: (~relation(B)|((![A]: (~in(A,relation_rng(B))|~relation_inverse_image(B,singleton(A))=empty_set))&(![A]: (in(A,relation_rng(B))|relation_inverse_image(B,singleton(A))=empty_set))))),
% 0.23/0.73 inference(miniscoping,[status(thm)],[f127])).
% 0.23/0.73 fof(f129,plain,(
% 0.23/0.73 ![X0,X1]: (~relation(X0)|~in(X1,relation_rng(X0))|~relation_inverse_image(X0,singleton(X1))=empty_set)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f128])).
% 0.23/0.73 fof(f131,plain,(
% 0.23/0.73 (?[A]: ((relation(A)&function(A))&((![B]: subset(relation_inverse_image(A,relation_image(A,B)),B))&~one_to_one(A))))),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.23/0.73 fof(f132,plain,(
% 0.23/0.73 ((relation(sK16_skl)&function(sK16_skl))&((![B]: subset(relation_inverse_image(sK16_skl,relation_image(sK16_skl,B)),B))&~one_to_one(sK16_skl)))),
% 0.23/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f131])).
% 0.23/0.73 fof(f133,plain,(
% 0.23/0.73 relation(sK16_skl)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.73 fof(f134,plain,(
% 0.23/0.73 function(sK16_skl)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.73 fof(f135,plain,(
% 0.23/0.73 ![X0]: (subset(relation_inverse_image(sK16_skl,relation_image(sK16_skl,X0)),X0))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.73 fof(f136,plain,(
% 0.23/0.73 ~one_to_one(sK16_skl)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.73 fof(f141,plain,(
% 0.23/0.73 ![A,B]: ((~subset(A,singleton(B))|(A=empty_set|A=singleton(B)))&(subset(A,singleton(B))|(~A=empty_set&~A=singleton(B))))),
% 0.23/0.73 inference(NNF_transformation,[status(thm)],[f34])).
% 0.23/0.73 fof(f142,plain,(
% 0.23/0.73 (![A,B]: (~subset(A,singleton(B))|(A=empty_set|A=singleton(B))))&(![A,B]: (subset(A,singleton(B))|(~A=empty_set&~A=singleton(B))))),
% 0.23/0.73 inference(miniscoping,[status(thm)],[f141])).
% 0.23/0.73 fof(f143,plain,(
% 0.23/0.73 ![X0,X1]: (~subset(X0,singleton(X1))|X0=empty_set|X0=singleton(X1))),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f142])).
% 0.23/0.73 fof(f156,plain,(
% 0.23/0.73 ![A]: (~empty(A)|A=empty_set)),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.23/0.73 fof(f157,plain,(
% 0.23/0.73 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f156])).
% 0.23/0.73 fof(f158,plain,(
% 0.23/0.73 ![A,B]: (~subset(singleton(A),singleton(B))|A=B)),
% 0.23/0.73 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.23/0.73 fof(f159,plain,(
% 0.23/0.73 ![X0,X1]: (~subset(singleton(X0),singleton(X1))|X0=X1)),
% 0.23/0.73 inference(cnf_transformation,[status(thm)],[f158])).
% 0.23/0.73 fof(f169,plain,(
% 0.23/0.73 ![X0,X1]: (~relation(X0)|~function(X0)|in(apply(X0,X1),relation_rng(X0))|~in(X1,relation_dom(X0)))),
% 0.23/0.73 inference(destructive_equality_resolution,[status(thm)],[f58])).
% 0.23/0.73 fof(f174,plain,(
% 0.23/0.73 ![X0]: (relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=empty_set|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=singleton(X0))),
% 0.23/0.73 inference(resolution,[status(thm)],[f143,f135])).
% 0.23/0.73 fof(f207,plain,(
% 0.23/0.73 ![X0]: (~singleton(X0)=empty_set|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=empty_set)),
% 0.23/0.73 inference(equality_factoring,[status(thm)],[f174])).
% 0.23/0.73 fof(f323,plain,(
% 0.23/0.73 sK10_skl=empty_set),
% 0.23/0.73 inference(resolution,[status(thm)],[f157,f104])).
% 0.23/0.73 fof(f347,plain,(
% 0.23/0.73 ![X0]: (~singleton(X0)=empty_set|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=sK10_skl)),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f323,f207])).
% 0.23/0.73 fof(f352,plain,(
% 0.23/0.73 ![X0]: (relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=sK10_skl|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=singleton(X0))),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f323,f174])).
% 0.23/0.73 fof(f360,plain,(
% 0.23/0.73 ![X0,X1]: (~relation(X0)|~in(X1,relation_rng(X0))|~relation_inverse_image(X0,singleton(X1))=sK10_skl)),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f323,f129])).
% 0.23/0.73 fof(f443,plain,(
% 0.23/0.73 ![X0]: (~singleton(X0)=sK10_skl|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(X0)))=sK10_skl)),
% 0.23/0.73 inference(forward_demodulation,[status(thm)],[f323,f347])).
% 0.23/0.73 fof(f543,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~relation(X0)|~function(X0)|in(apply(X0,sK3_skl(X0)),relation_rng(X0)))),
% 0.23/0.73 inference(resolution,[status(thm)],[f66,f169])).
% 0.23/0.73 fof(f544,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~relation(X0)|~function(X0)|relation_image(X0,singleton(sK3_skl(X0)))=singleton(apply(X0,sK3_skl(X0))))),
% 0.23/0.73 inference(resolution,[status(thm)],[f66,f125])).
% 0.23/0.73 fof(f547,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(apply(X0,sK3_skl(X0)),relation_rng(X0)))),
% 0.23/0.73 inference(duplicate_literals_removal,[status(thm)],[f543])).
% 0.23/0.73 fof(f548,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|relation_image(X0,singleton(sK3_skl(X0)))=singleton(apply(X0,sK3_skl(X0))))),
% 0.23/0.73 inference(duplicate_literals_removal,[status(thm)],[f544])).
% 0.23/0.73 fof(f551,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~relation(X0)|~function(X0)|relation_image(X0,singleton(sK4_skl(X0)))=singleton(apply(X0,sK4_skl(X0))))),
% 0.23/0.73 inference(resolution,[status(thm)],[f67,f125])).
% 0.23/0.73 fof(f555,plain,(
% 0.23/0.73 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|relation_image(X0,singleton(sK4_skl(X0)))=singleton(apply(X0,sK4_skl(X0))))),
% 0.23/0.73 inference(duplicate_literals_removal,[status(thm)],[f551])).
% 0.23/0.73 fof(f672,plain,(
% 0.23/0.73 ~relation(sK16_skl)|one_to_one(sK16_skl)|apply(sK16_skl,sK3_skl(sK16_skl))=apply(sK16_skl,sK4_skl(sK16_skl))),
% 0.23/0.73 inference(resolution,[status(thm)],[f68,f134])).
% 0.23/0.73 fof(f674,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|apply(sK16_skl,sK3_skl(sK16_skl))=apply(sK16_skl,sK4_skl(sK16_skl))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f672,f133])).
% 0.23/0.73 fof(f724,plain,(
% 0.23/0.73 ~relation(sK16_skl)|one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))=singleton(apply(sK16_skl,sK3_skl(sK16_skl)))),
% 0.23/0.73 inference(resolution,[status(thm)],[f548,f134])).
% 0.23/0.73 fof(f726,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))=singleton(apply(sK16_skl,sK3_skl(sK16_skl)))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f724,f133])).
% 0.23/0.73 fof(f730,plain,(
% 0.23/0.73 ~relation(sK16_skl)|one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK4_skl(sK16_skl)))=singleton(apply(sK16_skl,sK4_skl(sK16_skl)))),
% 0.23/0.73 inference(resolution,[status(thm)],[f555,f134])).
% 0.23/0.73 fof(f732,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK4_skl(sK16_skl)))=singleton(apply(sK16_skl,sK4_skl(sK16_skl)))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f730,f133])).
% 0.23/0.73 fof(f797,plain,(
% 0.23/0.73 apply(sK16_skl,sK3_skl(sK16_skl))=apply(sK16_skl,sK4_skl(sK16_skl))),
% 0.23/0.73 inference(resolution,[status(thm)],[f674,f136])).
% 0.23/0.73 fof(f799,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))=singleton(apply(sK16_skl,sK4_skl(sK16_skl)))),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f797,f726])).
% 0.23/0.73 fof(f800,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|relation_image(sK16_skl,singleton(sK4_skl(sK16_skl)))=relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f801,f732])).
% 0.23/0.73 fof(f801,plain,(
% 0.23/0.73 relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))=singleton(apply(sK16_skl,sK4_skl(sK16_skl)))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f799,f136])).
% 0.23/0.73 fof(f802,plain,(
% 0.23/0.73 relation_image(sK16_skl,singleton(sK4_skl(sK16_skl)))=singleton(apply(sK16_skl,sK4_skl(sK16_skl)))),
% 0.23/0.73 inference(backward_demodulation,[status(thm)],[f803,f801])).
% 0.23/0.73 fof(f803,plain,(
% 0.23/0.73 relation_image(sK16_skl,singleton(sK4_skl(sK16_skl)))=relation_image(sK16_skl,singleton(sK3_skl(sK16_skl)))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f800,f136])).
% 0.23/0.73 fof(f956,plain,(
% 0.23/0.73 relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK3_skl(sK16_skl))))=sK10_skl|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=singleton(sK3_skl(sK16_skl))),
% 0.23/0.73 inference(paramodulation,[status(thm)],[f803,f352])).
% 0.23/0.73 fof(f957,plain,(
% 0.23/0.73 ~singleton(sK3_skl(sK16_skl))=sK10_skl|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.73 inference(paramodulation,[status(thm)],[f803,f443])).
% 0.23/0.73 fof(f962,plain,(
% 0.23/0.73 relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=singleton(sK3_skl(sK16_skl))),
% 0.23/0.73 inference(forward_demodulation,[status(thm)],[f803,f956])).
% 0.23/0.73 fof(f1124,plain,(
% 0.23/0.73 ~relation(sK16_skl)|one_to_one(sK16_skl)|in(apply(sK16_skl,sK3_skl(sK16_skl)),relation_rng(sK16_skl))),
% 0.23/0.73 inference(resolution,[status(thm)],[f547,f134])).
% 0.23/0.73 fof(f1127,plain,(
% 0.23/0.73 ~relation(sK16_skl)|one_to_one(sK16_skl)|in(apply(sK16_skl,sK4_skl(sK16_skl)),relation_rng(sK16_skl))),
% 0.23/0.73 inference(forward_demodulation,[status(thm)],[f797,f1124])).
% 0.23/0.73 fof(f1128,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|in(apply(sK16_skl,sK4_skl(sK16_skl)),relation_rng(sK16_skl))),
% 0.23/0.73 inference(forward_subsumption_resolution,[status(thm)],[f1127,f133])).
% 0.23/0.73 fof(f1142,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|~relation(sK16_skl)|~relation_inverse_image(sK16_skl,singleton(apply(sK16_skl,sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.73 inference(resolution,[status(thm)],[f1128,f360])).
% 0.23/0.73 fof(f1147,plain,(
% 0.23/0.73 one_to_one(sK16_skl)|~relation(sK16_skl)|~relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.73 inference(forward_demodulation,[status(thm)],[f802,f1142])).
% 0.23/0.73 fof(f1148,plain,(
% 0.23/0.73 ~relation(sK16_skl)|~relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1147,f136])).
% 0.23/0.74 fof(f1178,plain,(
% 0.23/0.74 ~relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.74 inference(resolution,[status(thm)],[f1148,f133])).
% 0.23/0.74 fof(f1179,plain,(
% 0.23/0.74 ~singleton(sK3_skl(sK16_skl))=sK10_skl),
% 0.23/0.74 inference(backward_subsumption_resolution,[status(thm)],[f957,f1178])).
% 0.23/0.74 fof(f1180,plain,(
% 0.23/0.74 relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=singleton(sK3_skl(sK16_skl))),
% 0.23/0.74 inference(backward_subsumption_resolution,[status(thm)],[f962,f1178])).
% 0.23/0.74 fof(f1527,plain,(
% 0.23/0.74 singleton(sK4_skl(sK16_skl))=singleton(sK3_skl(sK16_skl))|relation_inverse_image(sK16_skl,relation_image(sK16_skl,singleton(sK4_skl(sK16_skl))))=sK10_skl),
% 0.23/0.74 inference(paramodulation,[status(thm)],[f352,f1180])).
% 0.23/0.74 fof(f1535,plain,(
% 0.23/0.74 singleton(sK4_skl(sK16_skl))=singleton(sK3_skl(sK16_skl))|singleton(sK3_skl(sK16_skl))=sK10_skl),
% 0.23/0.74 inference(forward_demodulation,[status(thm)],[f1180,f1527])).
% 0.23/0.74 fof(f1539,plain,(
% 0.23/0.74 singleton(sK4_skl(sK16_skl))=singleton(sK3_skl(sK16_skl))),
% 0.23/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1535,f1179])).
% 0.23/0.74 fof(f1555,plain,(
% 0.23/0.74 ![X0]: (~subset(singleton(X0),singleton(sK4_skl(sK16_skl)))|X0=sK3_skl(sK16_skl))),
% 0.23/0.74 inference(paramodulation,[status(thm)],[f1539,f159])).
% 0.23/0.74 fof(f1569,plain,(
% 0.23/0.74 sK4_skl(sK16_skl)=sK3_skl(sK16_skl)),
% 0.23/0.74 inference(resolution,[status(thm)],[f1555,f122])).
% 0.23/0.74 fof(f1590,plain,(
% 0.23/0.74 ~relation(sK16_skl)|~function(sK16_skl)|one_to_one(sK16_skl)),
% 0.23/0.74 inference(resolution,[status(thm)],[f1569,f69])).
% 0.23/0.74 fof(f1595,plain,(
% 0.23/0.74 ~function(sK16_skl)|one_to_one(sK16_skl)),
% 0.23/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1590,f133])).
% 0.23/0.74 fof(f1597,plain,(
% 0.23/0.74 one_to_one(sK16_skl)),
% 0.23/0.74 inference(resolution,[status(thm)],[f1595,f134])).
% 0.23/0.74 fof(f1598,plain,(
% 0.23/0.74 $false),
% 0.23/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1597,f136])).
% 0.23/0.74 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.76 % Elapsed time: 0.275912 seconds
% 0.23/0.76 % CPU time: 1.751478 seconds
% 0.23/0.76 % Total memory used: 105.983 MB
% 0.23/0.76 % Net memory used: 104.361 MB
%------------------------------------------------------------------------------