%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:38 PM UTC 2026
% Result : Theorem 0.11s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:43:28 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.11/0.42 % Refutation found
% 0.11/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.42 fof(f6,axiom,(
% 0.11/0.42 (! [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.11/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.42 fof(f27,axiom,(
% 0.11/0.42 (! [A,B] :( ( relation(B)& function(B) )=> ( in(A,relation_dom(B))=> relation_image(B,singleton(A)) = singleton(apply(B,A)) ) ) )),
% 0.11/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.42 fof(f28,conjecture,(
% 0.11/0.42 (! [A] :( ( relation(A)& function(A) )=> ( (! [B,C] : relation_image(A,set_difference(B,C)) = set_difference(relation_image(A,B),relation_image(A,C)))=> one_to_one(A) ) ) )),
% 0.11/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.42 fof(f29,negated_conjecture,(
% 0.11/0.42 ~((! [A] :( ( relation(A)& function(A) )=> ( (! [B,C] : relation_image(A,set_difference(B,C)) = set_difference(relation_image(A,B),relation_image(A,C)))=> one_to_one(A) ) ) ))),
% 0.11/0.42 inference(negated_conjecture,[status(cth)],[f28])).
% 0.11/0.42 fof(f31,axiom,(
% 0.11/0.42 (! [A,B] :( set_difference(singleton(A),singleton(B)) = singleton(A)<=> A != B ) )),
% 0.11/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.42 fof(f59,plain,(
% 0.11/0.42 ![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.11/0.42 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.11/0.42 fof(f60,plain,(
% 0.11/0.42 ![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.11/0.42 inference(NNF_transformation,[status(thm)],[f59])).
% 0.11/0.42 fof(f61,plain,(
% 0.11/0.42 ![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(sK1_skl(A),relation_dom(A))&in(sK2_skl(A),relation_dom(A)))&apply(A,sK1_skl(A))=apply(A,sK2_skl(A)))&~sK1_skl(A)=sK2_skl(A)))))),
% 0.11/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B,sK1_skl(A)),skolemize(C,sK2_skl(A))],[f60])).
% 0.11/0.42 fof(f63,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK1_skl(X0),relation_dom(X0)))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.11/0.42 fof(f64,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK2_skl(X0),relation_dom(X0)))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.11/0.42 fof(f65,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|apply(X0,sK1_skl(X0))=apply(X0,sK2_skl(X0)))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.11/0.42 fof(f66,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~sK1_skl(X0)=sK2_skl(X0))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.11/0.42 fof(f117,plain,(
% 0.11/0.42 ![A,B]: ((~relation(B)|~function(B))|(~in(A,relation_dom(B))|relation_image(B,singleton(A))=singleton(apply(B,A))))),
% 0.11/0.42 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.11/0.42 fof(f118,plain,(
% 0.11/0.42 ![B]: ((~relation(B)|~function(B))|(![A]: (~in(A,relation_dom(B))|relation_image(B,singleton(A))=singleton(apply(B,A)))))),
% 0.11/0.42 inference(miniscoping,[status(thm)],[f117])).
% 0.11/0.42 fof(f119,plain,(
% 0.11/0.42 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|relation_image(X0,singleton(X1))=singleton(apply(X0,X1)))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f118])).
% 0.11/0.42 fof(f120,plain,(
% 0.11/0.42 (?[A]: ((relation(A)&function(A))&((![B,C]: relation_image(A,set_difference(B,C))=set_difference(relation_image(A,B),relation_image(A,C)))&~one_to_one(A))))),
% 0.11/0.42 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.11/0.42 fof(f121,plain,(
% 0.11/0.42 ((relation(sK14_skl)&function(sK14_skl))&((![B,C]: relation_image(sK14_skl,set_difference(B,C))=set_difference(relation_image(sK14_skl,B),relation_image(sK14_skl,C)))&~one_to_one(sK14_skl)))),
% 0.11/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f120])).
% 0.11/0.42 fof(f122,plain,(
% 0.11/0.42 relation(sK14_skl)),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.42 fof(f123,plain,(
% 0.11/0.42 function(sK14_skl)),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.42 fof(f124,plain,(
% 0.11/0.42 ![X0,X1]: (relation_image(sK14_skl,set_difference(X0,X1))=set_difference(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)))),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.42 fof(f125,plain,(
% 0.11/0.42 ~one_to_one(sK14_skl)),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f121])).
% 0.11/0.42 fof(f128,plain,(
% 0.11/0.42 ![A,B]: ((~set_difference(singleton(A),singleton(B))=singleton(A)|~A=B)&(set_difference(singleton(A),singleton(B))=singleton(A)|A=B))),
% 0.11/0.42 inference(NNF_transformation,[status(thm)],[f31])).
% 0.11/0.42 fof(f129,plain,(
% 0.11/0.42 (![A,B]: (~set_difference(singleton(A),singleton(B))=singleton(A)|~A=B))&(![A,B]: (set_difference(singleton(A),singleton(B))=singleton(A)|A=B))),
% 0.11/0.42 inference(miniscoping,[status(thm)],[f128])).
% 0.11/0.42 fof(f130,plain,(
% 0.11/0.42 ![X0,X1]: (~set_difference(singleton(X0),singleton(X1))=singleton(X0)|~X0=X1)),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f129])).
% 0.11/0.42 fof(f131,plain,(
% 0.11/0.42 ![X0,X1]: (set_difference(singleton(X0),singleton(X1))=singleton(X0)|X0=X1)),
% 0.11/0.42 inference(cnf_transformation,[status(thm)],[f129])).
% 0.11/0.42 fof(f160,plain,(
% 0.11/0.42 ![X0]: (~set_difference(singleton(X0),singleton(X0))=singleton(X0))),
% 0.11/0.42 inference(destructive_equality_resolution,[status(thm)],[f130])).
% 0.11/0.42 fof(f189,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~relation(X0)|~function(X0)|relation_image(X0,singleton(sK1_skl(X0)))=singleton(apply(X0,sK1_skl(X0))))),
% 0.11/0.42 inference(resolution,[status(thm)],[f63,f119])).
% 0.11/0.42 fof(f191,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|relation_image(X0,singleton(sK1_skl(X0)))=singleton(apply(X0,sK1_skl(X0))))),
% 0.11/0.42 inference(duplicate_literals_removal,[status(thm)],[f189])).
% 0.11/0.42 fof(f192,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~relation(X0)|~function(X0)|relation_image(X0,singleton(sK2_skl(X0)))=singleton(apply(X0,sK2_skl(X0))))),
% 0.11/0.42 inference(resolution,[status(thm)],[f64,f119])).
% 0.11/0.42 fof(f194,plain,(
% 0.11/0.42 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|relation_image(X0,singleton(sK2_skl(X0)))=singleton(apply(X0,sK2_skl(X0))))),
% 0.11/0.42 inference(duplicate_literals_removal,[status(thm)],[f192])).
% 0.11/0.42 fof(f195,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|apply(sK14_skl,sK1_skl(sK14_skl))=apply(sK14_skl,sK2_skl(sK14_skl))),
% 0.11/0.42 inference(resolution,[status(thm)],[f65,f125])).
% 0.11/0.42 fof(f196,plain,(
% 0.11/0.42 ~function(sK14_skl)|apply(sK14_skl,sK1_skl(sK14_skl))=apply(sK14_skl,sK2_skl(sK14_skl))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f195,f122])).
% 0.11/0.42 fof(f197,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|~sK1_skl(sK14_skl)=sK2_skl(sK14_skl)),
% 0.11/0.42 inference(resolution,[status(thm)],[f66,f125])).
% 0.11/0.42 fof(f198,plain,(
% 0.11/0.42 ~function(sK14_skl)|~sK1_skl(sK14_skl)=sK2_skl(sK14_skl)),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f197,f122])).
% 0.11/0.42 fof(f199,plain,(
% 0.11/0.42 ~sK1_skl(sK14_skl)=sK2_skl(sK14_skl)),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f198,f123])).
% 0.11/0.42 fof(f200,plain,(
% 0.11/0.42 apply(sK14_skl,sK1_skl(sK14_skl))=apply(sK14_skl,sK2_skl(sK14_skl))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f196,f123])).
% 0.11/0.42 fof(f208,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(resolution,[status(thm)],[f191,f125])).
% 0.11/0.42 fof(f209,plain,(
% 0.11/0.42 ~function(sK14_skl)|relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f208,f122])).
% 0.11/0.42 fof(f210,plain,(
% 0.11/0.42 relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f209,f123])).
% 0.11/0.42 fof(f214,plain,(
% 0.11/0.42 ~set_difference(singleton(apply(sK14_skl,sK1_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(paramodulation,[status(thm)],[f210,f160])).
% 0.11/0.42 fof(f221,plain,(
% 0.11/0.42 ~set_difference(relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f210,f214])).
% 0.11/0.42 fof(f222,plain,(
% 0.11/0.42 ~relation_image(sK14_skl,set_difference(singleton(sK1_skl(sK14_skl)),singleton(sK1_skl(sK14_skl))))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f124,f221])).
% 0.11/0.42 fof(f223,plain,(
% 0.11/0.42 ~relation_image(sK14_skl,set_difference(singleton(sK1_skl(sK14_skl)),singleton(sK1_skl(sK14_skl))))=relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f210,f222])).
% 0.11/0.42 fof(f227,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))=singleton(apply(sK14_skl,sK2_skl(sK14_skl)))),
% 0.11/0.42 inference(resolution,[status(thm)],[f194,f125])).
% 0.11/0.42 fof(f228,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))=singleton(apply(sK14_skl,sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f200,f227])).
% 0.11/0.42 fof(f229,plain,(
% 0.11/0.42 ~relation(sK14_skl)|~function(sK14_skl)|relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))=relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f210,f228])).
% 0.11/0.42 fof(f230,plain,(
% 0.11/0.42 ~function(sK14_skl)|relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))=relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f229,f122])).
% 0.11/0.42 fof(f232,plain,(
% 0.11/0.42 relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))=relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f230,f123])).
% 0.11/0.42 fof(f235,plain,(
% 0.11/0.42 ![X0]: (relation_image(sK14_skl,set_difference(X0,singleton(sK2_skl(sK14_skl))))=set_difference(relation_image(sK14_skl,X0),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))))),
% 0.11/0.42 inference(paramodulation,[status(thm)],[f232,f124])).
% 0.11/0.42 fof(f237,plain,(
% 0.11/0.42 ![X0]: (relation_image(sK14_skl,set_difference(X0,singleton(sK2_skl(sK14_skl))))=relation_image(sK14_skl,set_difference(X0,singleton(sK1_skl(sK14_skl)))))),
% 0.11/0.42 inference(forward_demodulation,[status(thm)],[f124,f235])).
% 0.11/0.42 fof(f319,plain,(
% 0.11/0.42 ![X0]: (relation_image(sK14_skl,singleton(X0))=relation_image(sK14_skl,set_difference(singleton(X0),singleton(sK1_skl(sK14_skl))))|X0=sK2_skl(sK14_skl))),
% 0.11/0.42 inference(paramodulation,[status(thm)],[f131,f237])).
% 0.11/0.42 fof(f349,plain,(
% 0.11/0.42 sK1_skl(sK14_skl)=sK2_skl(sK14_skl)),
% 0.11/0.42 inference(resolution,[status(thm)],[f319,f223])).
% 0.11/0.42 fof(f362,plain,(
% 0.11/0.42 $false),
% 0.11/0.42 inference(forward_subsumption_resolution,[status(thm)],[f349,f199])).
% 0.11/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.44 % Elapsed time: 0.064958 seconds
% 0.11/0.44 % CPU time: 0.194280 seconds
% 0.11/0.44 % Total memory used: 104.675 MB
% 0.11/0.44 % Net memory used: 104.587 MB
%------------------------------------------------------------------------------