%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET995+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 : n008.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:58 PM UTC 2026
% Result : Theorem 0.22s 0.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET995+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.18/0.64 % Computer : n008.cluster.edu
% 0.18/0.64 % Model : x86_64 x86_64
% 0.18/0.64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.64 % Memory : 8046.5625MB
% 0.18/0.64 % OS : Linux 6.8.0-71-generic
% 0.18/0.64 % CPULimit : 300
% 0.18/0.64 % WCLimit : 300
% 0.18/0.64 % DateTime : Mon Sep 21 05:47:09 UTC 2026
% 0.18/0.65 % CPUTime :
% 0.22/0.67 % Drodi V4.1.1
% 0.22/0.76 % Refutation found
% 0.22/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.76 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.76 fof(f4,axiom,(
% 0.22/0.76 (! [A,B] :( B = singleton(A)<=> (! [C] :( in(C,B)<=> C = A ) )) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f5,axiom,(
% 0.22/0.76 (! [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.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f25,conjecture,(
% 0.22/0.76 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( ( relation_dom(B) = relation_dom(C)& relation_rng(B) = singleton(A)& relation_rng(C) = singleton(A) )=> B = C ) ) )) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f26,negated_conjecture,(
% 0.22/0.76 ~((! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( ( relation_dom(B) = relation_dom(C)& relation_rng(B) = singleton(A)& relation_rng(C) = singleton(A) )=> B = C ) ) )) ))),
% 0.22/0.76 inference(negated_conjecture,[status(cth)],[f25])).
% 0.22/0.76 fof(f35,axiom,(
% 0.22/0.76 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( relation_dom(A) = relation_dom(B)& (! [C] :( in(C,relation_dom(A))=> apply(A,C) = apply(B,C) ) ))=> A = B ) ) )) )),
% 0.22/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.76 fof(f42,plain,(
% 0.22/0.76 ![A,B]: ((~B=singleton(A)|(![C]: ((~in(C,B)|C=A)&(in(C,B)|~C=A))))&(B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 0.22/0.76 inference(NNF_transformation,[status(thm)],[f4])).
% 0.22/0.76 fof(f43,plain,(
% 0.22/0.76 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|(?[C]: ((~in(C,B)|~C=A)&(in(C,B)|C=A)))))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f42])).
% 0.22/0.76 fof(f44,plain,(
% 0.22/0.76 (![A,B]: (~B=singleton(A)|((![C]: (~in(C,B)|C=A))&(![C]: (in(C,B)|~C=A)))))&(![A,B]: (B=singleton(A)|((~in(sK0_skl(B,A),B)|~sK0_skl(B,A)=A)&(in(sK0_skl(B,A),B)|sK0_skl(B,A)=A))))),
% 0.22/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f43])).
% 0.22/0.76 fof(f45,plain,(
% 0.22/0.76 ![X0,X1,X2]: (~X0=singleton(X1)|~in(X2,X0)|X2=X1)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f44])).
% 0.22/0.76 fof(f49,plain,(
% 0.22/0.76 ![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.22/0.76 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.22/0.76 fof(f50,plain,(
% 0.22/0.76 ![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.22/0.76 inference(NNF_transformation,[status(thm)],[f49])).
% 0.22/0.76 fof(f51,plain,(
% 0.22/0.76 ![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.22/0.76 inference(miniscoping,[status(thm)],[f50])).
% 0.22/0.76 fof(f52,plain,(
% 0.22/0.76 ![A]: ((~relation(A)|~function(A))|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(in(sK1_skl(C,B,A),relation_dom(A))&C=apply(A,sK1_skl(C,B,A)))))&(![C]: (in(C,B)|(![D]: (~in(D,relation_dom(A))|~C=apply(A,D))))))))&(![B]: (B=relation_rng(A)|((~in(sK2_skl(B,A),B)|(![D]: (~in(D,relation_dom(A))|~sK2_skl(B,A)=apply(A,D))))&(in(sK2_skl(B,A),B)|(in(sK3_skl(B,A),relation_dom(A))&sK2_skl(B,A)=apply(A,sK3_skl(B,A)))))))))),
% 0.22/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(D,sK1_skl(C,B,A)),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f51])).
% 0.22/0.76 fof(f55,plain,(
% 0.22/0.76 ![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.22/0.76 inference(cnf_transformation,[status(thm)],[f52])).
% 0.22/0.76 fof(f104,plain,(
% 0.22/0.76 (?[A,B]: ((relation(B)&function(B))&(?[C]: ((relation(C)&function(C))&(((relation_dom(B)=relation_dom(C)&relation_rng(B)=singleton(A))&relation_rng(C)=singleton(A))&~B=C)))))),
% 0.22/0.76 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.22/0.76 fof(f105,plain,(
% 0.22/0.76 ?[B]: ((relation(B)&function(B))&(?[C]: ((relation(C)&function(C))&((?[A]: ((relation_dom(B)=relation_dom(C)&relation_rng(B)=singleton(A))&relation_rng(C)=singleton(A)))&~B=C))))),
% 0.22/0.76 inference(miniscoping,[status(thm)],[f104])).
% 0.22/0.76 fof(f106,plain,(
% 0.22/0.76 ((relation(sK13_skl)&function(sK13_skl))&((relation(sK14_skl)&function(sK14_skl))&(((relation_dom(sK13_skl)=relation_dom(sK14_skl)&relation_rng(sK13_skl)=singleton(sK15_skl))&relation_rng(sK14_skl)=singleton(sK15_skl))&~sK13_skl=sK14_skl)))),
% 0.22/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(B,sK13_skl),skolemize(C,sK14_skl),skolemize(A,sK15_skl)],[f105])).
% 0.22/0.76 fof(f107,plain,(
% 0.22/0.76 relation(sK13_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f108,plain,(
% 0.22/0.76 function(sK13_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f109,plain,(
% 0.22/0.76 relation(sK14_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f110,plain,(
% 0.22/0.76 function(sK14_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f111,plain,(
% 0.22/0.76 relation_dom(sK13_skl)=relation_dom(sK14_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f112,plain,(
% 0.22/0.76 relation_rng(sK13_skl)=singleton(sK15_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f113,plain,(
% 0.22/0.76 relation_rng(sK14_skl)=singleton(sK15_skl)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f114,plain,(
% 0.22/0.76 ~sK13_skl=sK14_skl),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/0.76 fof(f137,plain,(
% 0.22/0.76 ![A]: ((~relation(A)|~function(A))|(![B]: ((~relation(B)|~function(B))|((~relation_dom(A)=relation_dom(B)|(?[C]: (in(C,relation_dom(A))&~apply(A,C)=apply(B,C))))|A=B))))),
% 0.22/0.76 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.22/0.76 fof(f138,plain,(
% 0.22/0.76 ![A]: ((~relation(A)|~function(A))|(![B]: ((~relation(B)|~function(B))|((~relation_dom(A)=relation_dom(B)|(in(sK16_skl(B,A),relation_dom(A))&~apply(A,sK16_skl(B,A))=apply(B,sK16_skl(B,A))))|A=B))))),
% 0.22/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(C,sK16_skl(B,A))],[f137])).
% 0.22/0.76 fof(f139,plain,(
% 0.22/0.76 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_dom(X0)=relation_dom(X1)|in(sK16_skl(X1,X0),relation_dom(X0))|X0=X1)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f138])).
% 0.22/0.76 fof(f140,plain,(
% 0.22/0.76 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_dom(X0)=relation_dom(X1)|~apply(X0,sK16_skl(X1,X0))=apply(X1,sK16_skl(X1,X0))|X0=X1)),
% 0.22/0.76 inference(cnf_transformation,[status(thm)],[f138])).
% 0.22/0.76 fof(f141,plain,(
% 0.22/0.76 ![X0,X1]: (~in(X0,singleton(X1))|X0=X1)),
% 0.22/0.76 inference(destructive_equality_resolution,[status(thm)],[f45])).
% 0.22/0.76 fof(f145,plain,(
% 0.22/0.76 ![X0,X1]: (~relation(X0)|~function(X0)|in(apply(X0,X1),relation_rng(X0))|~in(X1,relation_dom(X0)))),
% 0.22/0.76 inference(destructive_equality_resolution,[status(thm)],[f55])).
% 0.22/0.76 fof(f208,plain,(
% 0.22/0.76 ![X0]: (~relation(sK14_skl)|in(apply(sK14_skl,X0),relation_rng(sK14_skl))|~in(X0,relation_dom(sK14_skl)))),
% 0.22/0.76 inference(resolution,[status(thm)],[f145,f110])).
% 0.22/0.76 fof(f209,plain,(
% 0.22/0.76 ![X0]: (~relation(sK13_skl)|in(apply(sK13_skl,X0),relation_rng(sK13_skl))|~in(X0,relation_dom(sK13_skl)))),
% 0.22/0.76 inference(resolution,[status(thm)],[f145,f108])).
% 0.22/0.76 fof(f212,plain,(
% 0.22/0.76 ![X0]: (~relation(sK14_skl)|in(apply(sK14_skl,X0),singleton(sK15_skl))|~in(X0,relation_dom(sK14_skl)))),
% 0.22/0.76 inference(forward_demodulation,[status(thm)],[f113,f208])).
% 0.22/0.76 fof(f213,plain,(
% 0.22/0.76 ![X0]: (~relation(sK14_skl)|in(apply(sK14_skl,X0),singleton(sK15_skl))|~in(X0,relation_dom(sK13_skl)))),
% 0.22/0.76 inference(forward_demodulation,[status(thm)],[f111,f212])).
% 0.22/0.76 fof(f214,plain,(
% 0.22/0.76 ![X0]: (in(apply(sK14_skl,X0),singleton(sK15_skl))|~in(X0,relation_dom(sK13_skl)))),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f213,f109])).
% 0.22/0.76 fof(f215,plain,(
% 0.22/0.76 ![X0]: (~relation(sK13_skl)|in(apply(sK13_skl,X0),singleton(sK15_skl))|~in(X0,relation_dom(sK13_skl)))),
% 0.22/0.76 inference(forward_demodulation,[status(thm)],[f112,f209])).
% 0.22/0.76 fof(f216,plain,(
% 0.22/0.76 ![X0]: (in(apply(sK13_skl,X0),singleton(sK15_skl))|~in(X0,relation_dom(sK13_skl)))),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f215,f107])).
% 0.22/0.76 fof(f230,plain,(
% 0.22/0.76 ![X0]: (~in(X0,relation_dom(sK13_skl))|apply(sK14_skl,X0)=sK15_skl)),
% 0.22/0.76 inference(resolution,[status(thm)],[f214,f141])).
% 0.22/0.76 fof(f259,plain,(
% 0.22/0.76 ![X0]: (~in(X0,relation_dom(sK13_skl))|apply(sK13_skl,X0)=sK15_skl)),
% 0.22/0.76 inference(resolution,[status(thm)],[f216,f141])).
% 0.22/0.76 fof(f423,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation(sK14_skl)|~relation_dom(X0)=relation_dom(sK14_skl)|in(sK16_skl(sK14_skl,X0),relation_dom(X0))|X0=sK14_skl)),
% 0.22/0.76 inference(resolution,[status(thm)],[f139,f110])).
% 0.22/0.76 fof(f427,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation(sK14_skl)|~relation_dom(X0)=relation_dom(sK13_skl)|in(sK16_skl(sK14_skl,X0),relation_dom(X0))|X0=sK14_skl)),
% 0.22/0.76 inference(forward_demodulation,[status(thm)],[f111,f423])).
% 0.22/0.76 fof(f428,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation_dom(X0)=relation_dom(sK13_skl)|in(sK16_skl(sK14_skl,X0),relation_dom(X0))|X0=sK14_skl)),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f427,f109])).
% 0.22/0.76 fof(f432,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation(sK14_skl)|~relation_dom(X0)=relation_dom(sK14_skl)|~apply(X0,sK16_skl(sK14_skl,X0))=apply(sK14_skl,sK16_skl(sK14_skl,X0))|X0=sK14_skl)),
% 0.22/0.76 inference(resolution,[status(thm)],[f140,f110])).
% 0.22/0.76 fof(f436,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation(sK14_skl)|~relation_dom(X0)=relation_dom(sK13_skl)|~apply(X0,sK16_skl(sK14_skl,X0))=apply(sK14_skl,sK16_skl(sK14_skl,X0))|X0=sK14_skl)),
% 0.22/0.76 inference(forward_demodulation,[status(thm)],[f111,f432])).
% 0.22/0.76 fof(f437,plain,(
% 0.22/0.76 ![X0]: (~relation(X0)|~function(X0)|~relation_dom(X0)=relation_dom(sK13_skl)|~apply(X0,sK16_skl(sK14_skl,X0))=apply(sK14_skl,sK16_skl(sK14_skl,X0))|X0=sK14_skl)),
% 0.22/0.76 inference(forward_subsumption_resolution,[status(thm)],[f436,f109])).
% 0.22/0.76 fof(f451,plain,(
% 0.22/0.76 ~relation(sK13_skl)|~relation_dom(sK13_skl)=relation_dom(sK13_skl)|in(sK16_skl(sK14_skl,sK13_skl),relation_dom(sK13_skl))|sK13_skl=sK14_skl),
% 0.22/0.77 inference(resolution,[status(thm)],[f428,f108])).
% 0.22/0.77 fof(f454,plain,(
% 0.22/0.77 ~relation(sK13_skl)|in(sK16_skl(sK14_skl,sK13_skl),relation_dom(sK13_skl))|sK13_skl=sK14_skl),
% 0.22/0.77 inference(trivial_equality_resolution,[status(thm)],[f451])).
% 0.22/0.77 fof(f455,plain,(
% 0.22/0.77 in(sK16_skl(sK14_skl,sK13_skl),relation_dom(sK13_skl))|sK13_skl=sK14_skl),
% 0.22/0.77 inference(forward_subsumption_resolution,[status(thm)],[f454,f107])).
% 0.22/0.77 fof(f545,plain,(
% 0.22/0.77 sK13_skl=sK14_skl|apply(sK13_skl,sK16_skl(sK14_skl,sK13_skl))=sK15_skl),
% 0.22/0.77 inference(resolution,[status(thm)],[f455,f259])).
% 0.22/0.77 fof(f546,plain,(
% 0.22/0.77 sK13_skl=sK14_skl|apply(sK14_skl,sK16_skl(sK14_skl,sK13_skl))=sK15_skl),
% 0.22/0.77 inference(resolution,[status(thm)],[f455,f230])).
% 0.22/0.77 fof(f548,plain,(
% 0.22/0.77 apply(sK13_skl,sK16_skl(sK14_skl,sK13_skl))=sK15_skl),
% 0.22/0.77 inference(forward_subsumption_resolution,[status(thm)],[f545,f114])).
% 0.22/0.77 fof(f549,plain,(
% 0.22/0.77 apply(sK14_skl,sK16_skl(sK14_skl,sK13_skl))=sK15_skl),
% 0.22/0.77 inference(forward_subsumption_resolution,[status(thm)],[f546,f114])).
% 0.22/0.77 fof(f587,plain,(
% 0.22/0.77 ~relation(sK13_skl)|~relation_dom(sK13_skl)=relation_dom(sK13_skl)|~apply(sK13_skl,sK16_skl(sK14_skl,sK13_skl))=apply(sK14_skl,sK16_skl(sK14_skl,sK13_skl))|sK13_skl=sK14_skl),
% 0.22/0.77 inference(resolution,[status(thm)],[f437,f108])).
% 0.22/0.77 fof(f590,plain,(
% 0.22/0.77 ~relation(sK13_skl)|~relation_dom(sK13_skl)=relation_dom(sK13_skl)|~sK15_skl=apply(sK14_skl,sK16_skl(sK14_skl,sK13_skl))|sK13_skl=sK14_skl),
% 0.22/0.77 inference(forward_demodulation,[status(thm)],[f548,f587])).
% 0.22/0.77 fof(f591,plain,(
% 0.22/0.77 ~relation(sK13_skl)|~relation_dom(sK13_skl)=relation_dom(sK13_skl)|~sK15_skl=sK15_skl|sK13_skl=sK14_skl),
% 0.22/0.77 inference(forward_demodulation,[status(thm)],[f549,f590])).
% 0.22/0.77 fof(f592,plain,(
% 0.22/0.77 ~relation(sK13_skl)|sK13_skl=sK14_skl),
% 0.22/0.77 inference(trivial_equality_resolution,[status(thm)],[f591])).
% 0.22/0.77 fof(f610,plain,(
% 0.22/0.77 ~sK13_skl=sK13_skl),
% 0.22/0.77 inference(backward_demodulation,[status(thm)],[f661,f114])).
% 0.22/0.77 fof(f661,plain,(
% 0.22/0.77 sK13_skl=sK14_skl),
% 0.22/0.77 inference(forward_subsumption_resolution,[status(thm)],[f592,f107])).
% 0.22/0.78 fof(f680,plain,(
% 0.22/0.78 $false),
% 0.22/0.78 inference(trivial_equality_resolution,[status(thm)],[f610])).
% 0.22/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.80 % Elapsed time: 0.130111 seconds
% 0.22/0.80 % CPU time: 0.732764 seconds
% 0.22/0.80 % Total memory used: 113.428 MB
% 0.22/0.80 % Net memory used: 112.624 MB
%------------------------------------------------------------------------------