%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET992+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:57 PM UTC 2026
% Result : Theorem 8.67s 1.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET992+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:49:38 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 8.67/1.60 % Refutation found
% 8.67/1.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.67/1.60 % SZS output start CNFRefutation for theBenchmark
% 8.67/1.60 fof(f4,axiom,(
% 8.67/1.60 (! [A,B] :( B = singleton(A)<=> (! [C] :( in(C,B)<=> C = A ) )) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f5,axiom,(
% 8.67/1.60 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] :( in(D,relation_dom(A))& C = apply(A,D) ) )) )) )) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f6,axiom,(
% 8.67/1.60 (! [A] :(? [B] : element(B,A) ))),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f10,axiom,(
% 8.67/1.60 (! [A] : ~ empty(singleton(A)) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f13,axiom,(
% 8.67/1.60 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_rng(A)) ) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f14,axiom,(
% 8.67/1.60 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f25,conjecture,(
% 8.67/1.60 (! [A,B] :( ( relation(B)& function(B) )=> ( relation_dom(B) = singleton(A)=> relation_rng(B) = singleton(apply(B,A)) ) ) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f26,negated_conjecture,(
% 8.67/1.60 ~((! [A,B] :( ( relation(B)& function(B) )=> ( relation_dom(B) = singleton(A)=> relation_rng(B) = singleton(apply(B,A)) ) ) ))),
% 8.67/1.60 inference(negated_conjecture,[status(cth)],[f25])).
% 8.67/1.60 fof(f28,axiom,(
% 8.67/1.60 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 8.67/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.67/1.60 fof(f42,plain,(
% 8.67/1.60 ![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)))))),
% 8.67/1.60 inference(NNF_transformation,[status(thm)],[f4])).
% 8.67/1.60 fof(f43,plain,(
% 8.67/1.60 (![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)))))),
% 8.67/1.60 inference(miniscoping,[status(thm)],[f42])).
% 8.67/1.60 fof(f44,plain,(
% 8.67/1.60 (![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))))),
% 8.67/1.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f43])).
% 8.67/1.60 fof(f45,plain,(
% 8.67/1.60 ![X0,X1,X2]: (~X0=singleton(X1)|~in(X2,X0)|X2=X1)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f44])).
% 8.67/1.60 fof(f46,plain,(
% 8.67/1.60 ![X0,X1,X2]: (~X0=singleton(X1)|in(X2,X0)|~X2=X1)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f44])).
% 8.67/1.60 fof(f47,plain,(
% 8.67/1.60 ![X0,X1]: (X0=singleton(X1)|~in(sK0_skl(X0,X1),X0)|~sK0_skl(X0,X1)=X1)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f44])).
% 8.67/1.60 fof(f48,plain,(
% 8.67/1.60 ![X0,X1]: (X0=singleton(X1)|in(sK0_skl(X0,X1),X0)|sK0_skl(X0,X1)=X1)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f44])).
% 8.67/1.60 fof(f49,plain,(
% 8.67/1.60 ![A]: ((~relation(A)|~function(A))|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: (in(D,relation_dom(A))&C=apply(A,D))))))))),
% 8.67/1.60 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 8.67/1.60 fof(f50,plain,(
% 8.67/1.60 ![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))))))))))),
% 8.67/1.60 inference(NNF_transformation,[status(thm)],[f49])).
% 8.67/1.60 fof(f51,plain,(
% 8.67/1.60 ![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))))))))))),
% 8.67/1.60 inference(miniscoping,[status(thm)],[f50])).
% 8.67/1.60 fof(f52,plain,(
% 8.67/1.60 ![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)))))))))),
% 8.67/1.60 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])).
% 8.67/1.60 fof(f53,plain,(
% 8.67/1.60 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~X1=relation_rng(X0)|~in(X2,X1)|in(sK1_skl(X2,X1,X0),relation_dom(X0)))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f52])).
% 8.67/1.60 fof(f54,plain,(
% 8.67/1.60 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~X1=relation_rng(X0)|~in(X2,X1)|X2=apply(X0,sK1_skl(X2,X1,X0)))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f52])).
% 8.67/1.60 fof(f55,plain,(
% 8.67/1.60 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(X3,relation_dom(X0))|~X2=apply(X0,X3))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f52])).
% 8.67/1.60 fof(f59,plain,(
% 8.67/1.60 ![A]: element(sK4_skl(A),A)),
% 8.67/1.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f6])).
% 8.67/1.60 fof(f60,plain,(
% 8.67/1.60 ![X0]: (element(sK4_skl(X0),X0))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f59])).
% 8.67/1.60 fof(f66,plain,(
% 8.67/1.60 ![X0]: (~empty(singleton(X0)))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f10])).
% 8.67/1.60 fof(f71,plain,(
% 8.67/1.60 ![A]: ((empty(A)|~relation(A))|~empty(relation_rng(A)))),
% 8.67/1.60 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 8.67/1.60 fof(f72,plain,(
% 8.67/1.60 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_rng(X0)))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f71])).
% 8.67/1.60 fof(f73,plain,(
% 8.67/1.60 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 8.67/1.60 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 8.67/1.60 fof(f74,plain,(
% 8.67/1.60 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f73])).
% 8.67/1.60 fof(f104,plain,(
% 8.67/1.60 (?[A,B]: ((relation(B)&function(B))&(relation_dom(B)=singleton(A)&~relation_rng(B)=singleton(apply(B,A)))))),
% 8.67/1.60 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 8.67/1.60 fof(f105,plain,(
% 8.67/1.60 ?[B]: ((relation(B)&function(B))&(?[A]: (relation_dom(B)=singleton(A)&~relation_rng(B)=singleton(apply(B,A)))))),
% 8.67/1.60 inference(miniscoping,[status(thm)],[f104])).
% 8.67/1.60 fof(f106,plain,(
% 8.67/1.60 ((relation(sK13_skl)&function(sK13_skl))&(relation_dom(sK13_skl)=singleton(sK14_skl)&~relation_rng(sK13_skl)=singleton(apply(sK13_skl,sK14_skl))))),
% 8.67/1.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(B,sK13_skl),skolemize(A,sK14_skl)],[f105])).
% 8.67/1.60 fof(f107,plain,(
% 8.67/1.60 relation(sK13_skl)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f106])).
% 8.67/1.60 fof(f108,plain,(
% 8.67/1.60 function(sK13_skl)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f106])).
% 8.67/1.60 fof(f109,plain,(
% 8.67/1.60 relation_dom(sK13_skl)=singleton(sK14_skl)),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f106])).
% 8.67/1.60 fof(f110,plain,(
% 8.67/1.60 ~relation_rng(sK13_skl)=singleton(apply(sK13_skl,sK14_skl))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f106])).
% 8.67/1.60 fof(f113,plain,(
% 8.67/1.60 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 8.67/1.60 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 8.67/1.60 fof(f114,plain,(
% 8.67/1.60 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 8.67/1.60 inference(cnf_transformation,[status(thm)],[f113])).
% 8.67/1.60 fof(f138,plain,(
% 8.67/1.60 ![X0,X1]: (~in(X0,singleton(X1))|X0=X1)),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f45])).
% 8.67/1.60 fof(f139,plain,(
% 8.67/1.60 ![X0]: (in(X0,singleton(X0)))),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f46])).
% 8.67/1.60 fof(f140,plain,(
% 8.67/1.60 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_rng(X0))|in(sK1_skl(X1,relation_rng(X0),X0),relation_dom(X0)))),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f53])).
% 8.67/1.60 fof(f141,plain,(
% 8.67/1.60 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_rng(X0))|X1=apply(X0,sK1_skl(X1,relation_rng(X0),X0)))),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f54])).
% 8.67/1.60 fof(f142,plain,(
% 8.67/1.60 ![X0,X1]: (~relation(X0)|~function(X0)|in(apply(X0,X1),relation_rng(X0))|~in(X1,relation_dom(X0)))),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f55])).
% 8.67/1.60 fof(f150,plain,(
% 8.67/1.60 ![X0]: (~relation(sK13_skl)|~function(sK13_skl)|~in(X0,relation_rng(sK13_skl))|in(sK1_skl(X0,relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl)))),
% 8.67/1.60 inference(paramodulation,[status(thm)],[f109,f140])).
% 8.67/1.60 fof(f151,plain,(
% 8.67/1.60 ![X0]: (~function(sK13_skl)|~in(X0,relation_rng(sK13_skl))|in(sK1_skl(X0,relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl)))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f150,f107])).
% 8.67/1.60 fof(f152,plain,(
% 8.67/1.60 ![X0]: (~relation(sK13_skl)|~in(X0,relation_rng(sK13_skl))|X0=apply(sK13_skl,sK1_skl(X0,relation_rng(sK13_skl),sK13_skl)))),
% 8.67/1.60 inference(resolution,[status(thm)],[f141,f108])).
% 8.67/1.60 fof(f154,plain,(
% 8.67/1.60 ![X0]: (~in(X0,relation_rng(sK13_skl))|X0=apply(sK13_skl,sK1_skl(X0,relation_rng(sK13_skl),sK13_skl)))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f152,f107])).
% 8.67/1.60 fof(f156,plain,(
% 8.67/1.60 ![X0]: (~in(X0,relation_rng(sK13_skl))|in(sK1_skl(X0,relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl)))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f151,f108])).
% 8.67/1.60 fof(f157,plain,(
% 8.67/1.60 ![X0]: (~in(X0,relation_rng(sK13_skl))|sK1_skl(X0,relation_rng(sK13_skl),sK13_skl)=sK14_skl)),
% 8.67/1.60 inference(resolution,[status(thm)],[f156,f138])).
% 8.67/1.60 fof(f159,plain,(
% 8.67/1.60 ![X0]: (sK0_skl(relation_rng(sK13_skl),X0)=apply(sK13_skl,sK1_skl(sK0_skl(relation_rng(sK13_skl),X0),relation_rng(sK13_skl),sK13_skl))|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(resolution,[status(thm)],[f154,f48])).
% 8.67/1.60 fof(f160,plain,(
% 8.67/1.60 ![X0]: (apply(sK13_skl,X0)=apply(sK13_skl,sK1_skl(apply(sK13_skl,X0),relation_rng(sK13_skl),sK13_skl))|~relation(sK13_skl)|~function(sK13_skl)|~in(X0,relation_dom(sK13_skl)))),
% 8.67/1.60 inference(resolution,[status(thm)],[f154,f142])).
% 8.67/1.60 fof(f161,plain,(
% 8.67/1.60 ![X0]: (apply(sK13_skl,X0)=apply(sK13_skl,sK1_skl(apply(sK13_skl,X0),relation_rng(sK13_skl),sK13_skl))|~relation(sK13_skl)|~function(sK13_skl)|~in(X0,singleton(sK14_skl)))),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f109,f160])).
% 8.67/1.60 fof(f162,plain,(
% 8.67/1.60 ![X0]: (apply(sK13_skl,X0)=apply(sK13_skl,sK1_skl(apply(sK13_skl,X0),relation_rng(sK13_skl),sK13_skl))|~function(sK13_skl)|~in(X0,singleton(sK14_skl)))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f161,f107])).
% 8.67/1.60 fof(f163,plain,(
% 8.67/1.60 ~empty(sK13_skl)|empty(singleton(sK14_skl))),
% 8.67/1.60 inference(paramodulation,[status(thm)],[f109,f74])).
% 8.67/1.60 fof(f164,plain,(
% 8.67/1.60 ~empty(sK13_skl)),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f163,f66])).
% 8.67/1.60 fof(f188,plain,(
% 8.67/1.60 ![X0]: (sK1_skl(sK0_skl(relation_rng(sK13_skl),X0),relation_rng(sK13_skl),sK13_skl)=sK14_skl|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(resolution,[status(thm)],[f157,f48])).
% 8.67/1.60 fof(f247,plain,(
% 8.67/1.60 ![X0]: (apply(sK13_skl,X0)=apply(sK13_skl,sK1_skl(apply(sK13_skl,X0),relation_rng(sK13_skl),sK13_skl))|~in(X0,singleton(sK14_skl)))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f162,f108])).
% 8.67/1.60 fof(f254,plain,(
% 8.67/1.60 apply(sK13_skl,sK14_skl)=apply(sK13_skl,sK1_skl(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl),sK13_skl))),
% 8.67/1.60 inference(resolution,[status(thm)],[f247,f139])).
% 8.67/1.60 fof(f269,plain,(
% 8.67/1.60 ![X0]: (empty(X0)|in(sK4_skl(X0),X0))),
% 8.67/1.60 inference(resolution,[status(thm)],[f114,f60])).
% 8.67/1.60 fof(f468,plain,(
% 8.67/1.60 ~relation(sK13_skl)|~function(sK13_skl)|in(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl))|~in(sK1_skl(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl),sK13_skl),relation_dom(sK13_skl))),
% 8.67/1.60 inference(paramodulation,[status(thm)],[f254,f142])).
% 8.67/1.60 fof(f471,plain,(
% 8.67/1.60 ~relation(sK13_skl)|~function(sK13_skl)|in(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl))|~in(sK1_skl(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl))),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f109,f468])).
% 8.67/1.60 fof(f472,plain,(
% 8.67/1.60 ~function(sK13_skl)|in(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl))|~in(sK1_skl(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f471,f107])).
% 8.67/1.60 fof(f560,plain,(
% 8.67/1.60 empty(relation_rng(sK13_skl))|sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl)=sK14_skl),
% 8.67/1.60 inference(resolution,[status(thm)],[f269,f157])).
% 8.67/1.60 fof(f561,plain,(
% 8.67/1.60 empty(relation_rng(sK13_skl))|sK4_skl(relation_rng(sK13_skl))=apply(sK13_skl,sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl))),
% 8.67/1.60 inference(resolution,[status(thm)],[f269,f154])).
% 8.67/1.60 fof(f881,plain,(
% 8.67/1.60 ![X0]: (sK0_skl(relation_rng(sK13_skl),X0)=apply(sK13_skl,sK14_skl)|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(paramodulation,[status(thm)],[f188,f159])).
% 8.67/1.60 fof(f886,plain,(
% 8.67/1.60 ![X0]: (sK0_skl(relation_rng(sK13_skl),X0)=apply(sK13_skl,sK14_skl)|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(duplicate_literals_removal,[status(thm)],[f881])).
% 8.67/1.60 fof(f1338,plain,(
% 8.67/1.60 sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl)=sK14_skl|empty(sK13_skl)|~relation(sK13_skl)),
% 8.67/1.60 inference(resolution,[status(thm)],[f560,f72])).
% 8.67/1.60 fof(f1370,plain,(
% 8.67/1.60 sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl)=sK14_skl|~relation(sK13_skl)),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f1338,f164])).
% 8.67/1.60 fof(f1609,plain,(
% 8.67/1.60 empty(relation_rng(sK13_skl))|sK4_skl(relation_rng(sK13_skl))=apply(sK13_skl,sK14_skl)),
% 8.67/1.60 inference(backward_demodulation,[status(thm)],[f1610,f561])).
% 8.67/1.60 fof(f1610,plain,(
% 8.67/1.60 sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl)=sK14_skl),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f1370,f107])).
% 8.67/1.60 fof(f1617,plain,(
% 8.67/1.60 sK4_skl(relation_rng(sK13_skl))=apply(sK13_skl,sK14_skl)|empty(sK13_skl)|~relation(sK13_skl)),
% 8.67/1.60 inference(resolution,[status(thm)],[f1609,f72])).
% 8.67/1.60 fof(f1652,plain,(
% 8.67/1.60 sK4_skl(relation_rng(sK13_skl))=apply(sK13_skl,sK14_skl)|~relation(sK13_skl)),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f1617,f164])).
% 8.67/1.60 fof(f1876,plain,(
% 8.67/1.60 ~relation_rng(sK13_skl)=singleton(sK4_skl(relation_rng(sK13_skl)))),
% 8.67/1.60 inference(backward_demodulation,[status(thm)],[f1877,f110])).
% 8.67/1.60 fof(f1877,plain,(
% 8.67/1.60 sK4_skl(relation_rng(sK13_skl))=apply(sK13_skl,sK14_skl)),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f1652,f107])).
% 8.67/1.60 fof(f9655,plain,(
% 8.67/1.60 ~function(sK13_skl)|in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~in(sK1_skl(apply(sK13_skl,sK14_skl),relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl))),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f1877,f472])).
% 8.67/1.60 fof(f9656,plain,(
% 8.67/1.60 ~function(sK13_skl)|in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~in(sK1_skl(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl),sK13_skl),singleton(sK14_skl))),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f1877,f9655])).
% 8.67/1.60 fof(f9657,plain,(
% 8.67/1.60 ~function(sK13_skl)|in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~in(sK14_skl,singleton(sK14_skl))),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f1610,f9656])).
% 8.67/1.60 fof(f9658,plain,(
% 8.67/1.60 in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~in(sK14_skl,singleton(sK14_skl))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f9657,f108])).
% 8.67/1.60 fof(f9659,plain,(
% 8.67/1.60 in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))),
% 8.67/1.60 inference(resolution,[status(thm)],[f9658,f139])).
% 8.67/1.60 fof(f9814,plain,(
% 8.67/1.60 ![X0]: (sK0_skl(relation_rng(sK13_skl),X0)=sK4_skl(relation_rng(sK13_skl))|relation_rng(sK13_skl)=singleton(X0)|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(forward_demodulation,[status(thm)],[f1877,f886])).
% 8.67/1.60 fof(f9821,plain,(
% 8.67/1.60 ![X0]: (relation_rng(sK13_skl)=singleton(X0)|~sK4_skl(relation_rng(sK13_skl))=X0|sK0_skl(relation_rng(sK13_skl),X0)=X0)),
% 8.67/1.60 inference(equality_factoring,[status(thm)],[f9814])).
% 8.67/1.60 fof(f9830,plain,(
% 8.67/1.60 relation_rng(sK13_skl)=singleton(sK4_skl(relation_rng(sK13_skl)))|sK0_skl(relation_rng(sK13_skl),sK4_skl(relation_rng(sK13_skl)))=sK4_skl(relation_rng(sK13_skl))),
% 8.67/1.60 inference(destructive_equality_resolution,[status(thm)],[f9821])).
% 8.67/1.60 fof(f9831,plain,(
% 8.67/1.60 sK0_skl(relation_rng(sK13_skl),sK4_skl(relation_rng(sK13_skl)))=sK4_skl(relation_rng(sK13_skl))),
% 8.67/1.60 inference(forward_subsumption_resolution,[status(thm)],[f9830,f1876])).
% 8.67/1.61 fof(f10448,plain,(
% 8.67/1.61 relation_rng(sK13_skl)=singleton(sK4_skl(relation_rng(sK13_skl)))|~in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~sK0_skl(relation_rng(sK13_skl),sK4_skl(relation_rng(sK13_skl)))=sK4_skl(relation_rng(sK13_skl))),
% 8.67/1.61 inference(paramodulation,[status(thm)],[f9831,f47])).
% 8.67/1.61 fof(f10453,plain,(
% 8.67/1.61 relation_rng(sK13_skl)=singleton(sK4_skl(relation_rng(sK13_skl)))|~in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))|~sK4_skl(relation_rng(sK13_skl))=sK4_skl(relation_rng(sK13_skl))),
% 8.67/1.61 inference(forward_demodulation,[status(thm)],[f9831,f10448])).
% 8.67/1.61 fof(f10454,plain,(
% 8.67/1.61 relation_rng(sK13_skl)=singleton(sK4_skl(relation_rng(sK13_skl)))|~in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))),
% 8.67/1.61 inference(trivial_equality_resolution,[status(thm)],[f10453])).
% 8.67/1.61 fof(f10455,plain,(
% 8.67/1.61 ~in(sK4_skl(relation_rng(sK13_skl)),relation_rng(sK13_skl))),
% 8.67/1.61 inference(forward_subsumption_resolution,[status(thm)],[f10454,f1876])).
% 8.67/1.61 fof(f10472,plain,(
% 8.67/1.61 $false),
% 8.67/1.61 inference(forward_subsumption_resolution,[status(thm)],[f10455,f9659])).
% 8.67/1.61 % SZS output end CNFRefutation for theBenchmark.p
% 3.39/1.63 % Elapsed time: 1.253885 seconds
% 3.39/1.63 % CPU time: 9.594870 seconds
% 3.39/1.63 % Total memory used: 222.992 MB
% 3.39/1.63 % Net memory used: 211.235 MB
%------------------------------------------------------------------------------