%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU181+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:55 PM UTC 2026
% Result : Theorem 17.29s 2.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU181+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:55:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 17.29/2.68 % Refutation found
% 17.29/2.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.29/2.68 % SZS output start CNFRefutation for theBenchmark
% 17.29/2.68 fof(f3,axiom,(
% 17.29/2.68 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f4,axiom,(
% 17.29/2.68 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f5,axiom,(
% 17.29/2.68 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f6,axiom,(
% 17.29/2.68 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f8,axiom,(
% 17.29/2.68 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( B = relation_inverse(A)<=> (! [C,D] :( in(ordered_pair(C,D),B)<=> in(ordered_pair(D,C),A) ) )) ) )) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f15,axiom,(
% 17.29/2.68 (! [A] :( relation(A)=> relation(relation_inverse(A)) ) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f24,axiom,(
% 17.29/2.68 (! [A] :( relation(A)=> relation_inverse(relation_inverse(A)) = A ) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f33,conjecture,(
% 17.29/2.68 (! [A] :( relation(A)=> ( relation_rng(A) = relation_dom(relation_inverse(A))& relation_dom(A) = relation_rng(relation_inverse(A)) ) ) )),
% 17.29/2.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.29/2.68 fof(f34,negated_conjecture,(
% 17.29/2.68 ~((! [A] :( relation(A)=> ( relation_rng(A) = relation_dom(relation_inverse(A))& relation_dom(A) = relation_rng(relation_inverse(A)) ) ) ))),
% 17.29/2.68 inference(negated_conjecture,[status(cth)],[f33])).
% 17.29/2.68 fof(f44,plain,(
% 17.29/2.68 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 17.29/2.68 inference(NNF_transformation,[status(thm)],[f3])).
% 17.29/2.68 fof(f45,plain,(
% 17.29/2.68 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 17.29/2.68 inference(miniscoping,[status(thm)],[f44])).
% 17.29/2.68 fof(f48,plain,(
% 17.29/2.68 ![X0,X1]: (X0=X1|~subset(X0,X1)|~subset(X1,X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f45])).
% 17.29/2.68 fof(f49,plain,(
% 17.29/2.68 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 17.29/2.68 fof(f50,plain,(
% 17.29/2.68 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 17.29/2.68 inference(NNF_transformation,[status(thm)],[f49])).
% 17.29/2.68 fof(f51,plain,(
% 17.29/2.68 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 17.29/2.68 inference(miniscoping,[status(thm)],[f50])).
% 17.29/2.68 fof(f52,plain,(
% 17.29/2.68 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK0_skl(B,A),A)&~in(sK0_skl(B,A),B))))),
% 17.29/2.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f51])).
% 17.29/2.68 fof(f54,plain,(
% 17.29/2.68 ![X0,X1]: (subset(X0,X1)|in(sK0_skl(X1,X0),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f52])).
% 17.29/2.68 fof(f55,plain,(
% 17.29/2.68 ![X0,X1]: (subset(X0,X1)|~in(sK0_skl(X1,X0),X1))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f52])).
% 17.29/2.68 fof(f56,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 17.29/2.68 fof(f57,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: ((~B=relation_dom(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(C,D),A)))&(in(C,B)|(![D]: ~in(ordered_pair(C,D),A))))))&(B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 17.29/2.68 inference(NNF_transformation,[status(thm)],[f56])).
% 17.29/2.68 fof(f58,plain,(
% 17.29/2.68 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(C,D),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 17.29/2.68 inference(miniscoping,[status(thm)],[f57])).
% 17.29/2.68 fof(f59,plain,(
% 17.29/2.68 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK1_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK2_skl(B,A),B)|(![D]: ~in(ordered_pair(sK2_skl(B,A),D),A)))&(in(sK2_skl(B,A),B)|in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A)))))))),
% 17.29/2.68 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))],[f58])).
% 17.29/2.68 fof(f60,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|~X1=relation_dom(X0)|~in(X2,X1)|in(ordered_pair(X2,sK1_skl(X2,X1,X0)),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f59])).
% 17.29/2.68 fof(f61,plain,(
% 17.29/2.68 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f59])).
% 17.29/2.68 fof(f64,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 17.29/2.68 fof(f65,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(D,C),A)))&(in(C,B)|(![D]: ~in(ordered_pair(D,C),A))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 17.29/2.68 inference(NNF_transformation,[status(thm)],[f64])).
% 17.29/2.68 fof(f66,plain,(
% 17.29/2.68 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(D,C),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 17.29/2.68 inference(miniscoping,[status(thm)],[f65])).
% 17.29/2.68 fof(f67,plain,(
% 17.29/2.68 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK4_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK5_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK5_skl(B,A)),A)))&(in(sK5_skl(B,A),B)|in(ordered_pair(sK6_skl(B,A),sK5_skl(B,A)),A)))))))),
% 17.29/2.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f66])).
% 17.29/2.68 fof(f68,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|~X1=relation_rng(X0)|~in(X2,X1)|in(ordered_pair(sK4_skl(X2,X1,X0),X2),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f67])).
% 17.29/2.68 fof(f69,plain,(
% 17.29/2.68 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f67])).
% 17.29/2.68 fof(f73,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (~relation(B)|(B=relation_inverse(A)<=>(![C,D]: (in(ordered_pair(C,D),B)<=>in(ordered_pair(D,C),A)))))))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 17.29/2.68 fof(f74,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (~relation(B)|((~B=relation_inverse(A)|(![C,D]: ((~in(ordered_pair(C,D),B)|in(ordered_pair(D,C),A))&(in(ordered_pair(C,D),B)|~in(ordered_pair(D,C),A)))))&(B=relation_inverse(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|~in(ordered_pair(D,C),A))&(in(ordered_pair(C,D),B)|in(ordered_pair(D,C),A)))))))))),
% 17.29/2.68 inference(NNF_transformation,[status(thm)],[f73])).
% 17.29/2.68 fof(f75,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (~relation(B)|((~B=relation_inverse(A)|((![C,D]: (~in(ordered_pair(C,D),B)|in(ordered_pair(D,C),A)))&(![C,D]: (in(ordered_pair(C,D),B)|~in(ordered_pair(D,C),A)))))&(B=relation_inverse(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|~in(ordered_pair(D,C),A))&(in(ordered_pair(C,D),B)|in(ordered_pair(D,C),A)))))))))),
% 17.29/2.68 inference(miniscoping,[status(thm)],[f74])).
% 17.29/2.68 fof(f76,plain,(
% 17.29/2.68 ![A]: (~relation(A)|(![B]: (~relation(B)|((~B=relation_inverse(A)|((![C,D]: (~in(ordered_pair(C,D),B)|in(ordered_pair(D,C),A)))&(![C,D]: (in(ordered_pair(C,D),B)|~in(ordered_pair(D,C),A)))))&(B=relation_inverse(A)|((~in(ordered_pair(sK7_skl(B,A),sK8_skl(B,A)),B)|~in(ordered_pair(sK8_skl(B,A),sK7_skl(B,A)),A))&(in(ordered_pair(sK7_skl(B,A),sK8_skl(B,A)),B)|in(ordered_pair(sK8_skl(B,A),sK7_skl(B,A)),A))))))))),
% 17.29/2.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(C,sK7_skl(B,A)),skolemize(D,sK8_skl(B,A))],[f75])).
% 17.29/2.68 fof(f77,plain,(
% 17.29/2.68 ![X0,X1,X2,X3]: (~relation(X0)|~relation(X1)|~X1=relation_inverse(X0)|~in(ordered_pair(X2,X3),X1)|in(ordered_pair(X3,X2),X0))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f76])).
% 17.29/2.68 fof(f81,plain,(
% 17.29/2.68 ![A]: (~relation(A)|relation(relation_inverse(A)))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 17.29/2.68 fof(f82,plain,(
% 17.29/2.68 ![X0]: (~relation(X0)|relation(relation_inverse(X0)))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f81])).
% 17.29/2.68 fof(f90,plain,(
% 17.29/2.68 ![A]: (~relation(A)|relation_inverse(relation_inverse(A))=A)),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 17.29/2.68 fof(f91,plain,(
% 17.29/2.68 ![X0]: (~relation(X0)|relation_inverse(relation_inverse(X0))=X0)),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f90])).
% 17.29/2.68 fof(f112,plain,(
% 17.29/2.68 (?[A]: (relation(A)&(~relation_rng(A)=relation_dom(relation_inverse(A))|~relation_dom(A)=relation_rng(relation_inverse(A)))))),
% 17.29/2.68 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 17.29/2.68 fof(f113,plain,(
% 17.29/2.68 (relation(sK15_skl)&(~relation_rng(sK15_skl)=relation_dom(relation_inverse(sK15_skl))|~relation_dom(sK15_skl)=relation_rng(relation_inverse(sK15_skl))))),
% 17.29/2.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f112])).
% 17.29/2.68 fof(f114,plain,(
% 17.29/2.68 relation(sK15_skl)),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f113])).
% 17.29/2.68 fof(f115,plain,(
% 17.29/2.68 ~relation_rng(sK15_skl)=relation_dom(relation_inverse(sK15_skl))|~relation_dom(sK15_skl)=relation_rng(relation_inverse(sK15_skl))),
% 17.29/2.68 inference(cnf_transformation,[status(thm)],[f113])).
% 17.29/2.68 fof(f136,plain,(
% 17.29/2.68 ![X0,X1]: (~relation(X0)|~in(X1,relation_dom(X0))|in(ordered_pair(X1,sK1_skl(X1,relation_dom(X0),X0)),X0))),
% 17.29/2.68 inference(destructive_equality_resolution,[status(thm)],[f60])).
% 17.29/2.68 fof(f137,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 17.29/2.68 inference(destructive_equality_resolution,[status(thm)],[f61])).
% 17.29/2.68 fof(f138,plain,(
% 17.29/2.68 ![X0,X1]: (~relation(X0)|~in(X1,relation_rng(X0))|in(ordered_pair(sK4_skl(X1,relation_rng(X0),X0),X1),X0))),
% 17.29/2.68 inference(destructive_equality_resolution,[status(thm)],[f68])).
% 17.29/2.68 fof(f139,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 17.29/2.68 inference(destructive_equality_resolution,[status(thm)],[f69])).
% 17.29/2.68 fof(f140,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|~relation(relation_inverse(X0))|~in(ordered_pair(X1,X2),relation_inverse(X0))|in(ordered_pair(X2,X1),X0))),
% 17.29/2.68 inference(destructive_equality_resolution,[status(thm)],[f77])).
% 17.29/2.68 fof(f142,plain,(
% 17.29/2.68 relation(relation_inverse(sK15_skl))),
% 17.29/2.68 inference(resolution,[status(thm)],[f82,f114])).
% 17.29/2.68 fof(f147,plain,(
% 17.29/2.68 relation_inverse(relation_inverse(sK15_skl))=sK15_skl),
% 17.29/2.68 inference(resolution,[status(thm)],[f91,f114])).
% 17.29/2.68 fof(f150,plain,(
% 17.29/2.68 ![X0,X1,X2]: (~relation(X0)|~in(ordered_pair(X1,X2),relation_inverse(X0))|in(ordered_pair(X2,X1),X0))),
% 17.29/2.68 inference(forward_subsumption_resolution,[status(thm)],[f140,f82])).
% 17.29/2.68 fof(f151,plain,(
% 17.29/2.68 ![X0,X1]: (~relation(relation_inverse(sK15_skl))|~in(ordered_pair(X0,X1),sK15_skl)|in(ordered_pair(X1,X0),relation_inverse(sK15_skl)))),
% 17.29/2.68 inference(paramodulation,[status(thm)],[f147,f150])).
% 17.29/2.68 fof(f152,plain,(
% 17.29/2.68 ![X0,X1]: (~in(ordered_pair(X0,X1),sK15_skl)|in(ordered_pair(X1,X0),relation_inverse(sK15_skl)))),
% 17.29/2.68 inference(forward_subsumption_resolution,[status(thm)],[f151,f142])).
% 17.29/2.68 fof(f753,plain,(
% 17.29/2.68 ![X0,X1]: (~relation(X0)|in(ordered_pair(sK0_skl(X1,relation_dom(X0)),sK1_skl(sK0_skl(X1,relation_dom(X0)),relation_dom(X0),X0)),X0)|subset(relation_dom(X0),X1))),
% 17.29/2.68 inference(resolution,[status(thm)],[f136,f54])).
% 17.29/2.68 fof(f805,plain,(
% 17.29/2.68 ![X0,X1]: (~relation(X0)|in(ordered_pair(sK4_skl(sK0_skl(X1,relation_rng(X0)),relation_rng(X0),X0),sK0_skl(X1,relation_rng(X0))),X0)|subset(relation_rng(X0),X1))),
% 17.29/2.68 inference(resolution,[status(thm)],[f138,f54])).
% 17.29/2.68 fof(f1152,plain,(
% 17.29/2.68 ![X0]: (in(ordered_pair(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),sK1_skl(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),relation_dom(relation_inverse(sK15_skl)),relation_inverse(sK15_skl))),relation_inverse(sK15_skl))|subset(relation_dom(relation_inverse(sK15_skl)),X0))),
% 17.29/2.68 inference(resolution,[status(thm)],[f753,f142])).
% 17.29/2.68 fof(f1153,plain,(
% 17.29/2.68 ![X0]: (in(ordered_pair(sK0_skl(X0,relation_dom(sK15_skl)),sK1_skl(sK0_skl(X0,relation_dom(sK15_skl)),relation_dom(sK15_skl),sK15_skl)),sK15_skl)|subset(relation_dom(sK15_skl),X0))),
% 17.29/2.68 inference(resolution,[status(thm)],[f753,f114])).
% 17.29/2.68 fof(f1156,plain,(
% 17.29/2.68 ![X0]: (in(ordered_pair(sK4_skl(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),relation_rng(relation_inverse(sK15_skl)),relation_inverse(sK15_skl)),sK0_skl(X0,relation_rng(relation_inverse(sK15_skl)))),relation_inverse(sK15_skl))|subset(relation_rng(relation_inverse(sK15_skl)),X0))),
% 17.29/2.68 inference(resolution,[status(thm)],[f805,f142])).
% 17.29/2.68 fof(f1157,plain,(
% 17.29/2.68 ![X0]: (in(ordered_pair(sK4_skl(sK0_skl(X0,relation_rng(sK15_skl)),relation_rng(sK15_skl),sK15_skl),sK0_skl(X0,relation_rng(sK15_skl))),sK15_skl)|subset(relation_rng(sK15_skl),X0))),
% 17.29/2.68 inference(resolution,[status(thm)],[f805,f114])).
% 17.29/2.68 fof(f1379,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(relation_inverse(sK15_skl)),X0)|~relation(sK15_skl)|in(ordered_pair(sK1_skl(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),relation_dom(relation_inverse(sK15_skl)),relation_inverse(sK15_skl)),sK0_skl(X0,relation_dom(relation_inverse(sK15_skl)))),sK15_skl))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1152,f150])).
% 17.29/2.68 fof(f1386,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(relation_inverse(sK15_skl)),X0)|in(ordered_pair(sK1_skl(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),relation_dom(relation_inverse(sK15_skl)),relation_inverse(sK15_skl)),sK0_skl(X0,relation_dom(relation_inverse(sK15_skl)))),sK15_skl))),
% 17.29/2.68 inference(forward_subsumption_resolution,[status(thm)],[f1379,f114])).
% 17.29/2.68 fof(f1390,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(sK15_skl),X0)|in(ordered_pair(sK1_skl(sK0_skl(X0,relation_dom(sK15_skl)),relation_dom(sK15_skl),sK15_skl),sK0_skl(X0,relation_dom(sK15_skl))),relation_inverse(sK15_skl)))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1153,f152])).
% 17.29/2.68 fof(f1399,plain,(
% 17.29/2.68 ![X0]: (subset(relation_rng(relation_inverse(sK15_skl)),X0)|~relation(sK15_skl)|in(ordered_pair(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),sK4_skl(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),relation_rng(relation_inverse(sK15_skl)),relation_inverse(sK15_skl))),sK15_skl))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1156,f150])).
% 17.29/2.68 fof(f1406,plain,(
% 17.29/2.68 ![X0]: (subset(relation_rng(relation_inverse(sK15_skl)),X0)|in(ordered_pair(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),sK4_skl(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),relation_rng(relation_inverse(sK15_skl)),relation_inverse(sK15_skl))),sK15_skl))),
% 17.29/2.68 inference(forward_subsumption_resolution,[status(thm)],[f1399,f114])).
% 17.29/2.68 fof(f1528,plain,(
% 17.29/2.68 ![X0]: (subset(relation_rng(sK15_skl),X0)|in(ordered_pair(sK0_skl(X0,relation_rng(sK15_skl)),sK4_skl(sK0_skl(X0,relation_rng(sK15_skl)),relation_rng(sK15_skl),sK15_skl)),relation_inverse(sK15_skl)))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1157,f152])).
% 17.29/2.68 fof(f7446,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(relation_inverse(sK15_skl)),X0)|~relation(sK15_skl)|in(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1386,f139])).
% 17.29/2.68 fof(f7451,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(relation_inverse(sK15_skl)),X0)|in(sK0_skl(X0,relation_dom(relation_inverse(sK15_skl))),relation_rng(sK15_skl)))),
% 17.29/2.68 inference(forward_subsumption_resolution,[status(thm)],[f7446,f114])).
% 17.29/2.68 fof(f7489,plain,(
% 17.29/2.68 subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))|subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),
% 17.29/2.68 inference(resolution,[status(thm)],[f7451,f55])).
% 17.29/2.68 fof(f7494,plain,(
% 17.29/2.68 subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),
% 17.29/2.68 inference(duplicate_literals_removal,[status(thm)],[f7489])).
% 17.29/2.68 fof(f8814,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(sK15_skl),X0)|~relation(relation_inverse(sK15_skl))|in(sK0_skl(X0,relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))))),
% 17.29/2.68 inference(resolution,[status(thm)],[f1390,f139])).
% 17.29/2.68 fof(f8820,plain,(
% 17.29/2.68 ![X0]: (subset(relation_dom(sK15_skl),X0)|in(sK0_skl(X0,relation_dom(sK15_skl)),relation_rng(relation_inverse(sK15_skl))))),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f8814,f142])).
% 17.29/2.70 fof(f9119,plain,(
% 17.29/2.70 subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))|subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),
% 17.29/2.70 inference(resolution,[status(thm)],[f8820,f55])).
% 17.29/2.70 fof(f9124,plain,(
% 17.29/2.70 subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),
% 17.29/2.70 inference(duplicate_literals_removal,[status(thm)],[f9119])).
% 17.29/2.70 fof(f9184,plain,(
% 17.29/2.70 ![X0]: (subset(relation_rng(relation_inverse(sK15_skl)),X0)|~relation(sK15_skl)|in(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)))),
% 17.29/2.70 inference(resolution,[status(thm)],[f1406,f137])).
% 17.29/2.70 fof(f9189,plain,(
% 17.29/2.70 ![X0]: (subset(relation_rng(relation_inverse(sK15_skl)),X0)|in(sK0_skl(X0,relation_rng(relation_inverse(sK15_skl))),relation_dom(sK15_skl)))),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f9184,f114])).
% 17.29/2.70 fof(f9423,plain,(
% 17.29/2.70 subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))|subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),
% 17.29/2.70 inference(resolution,[status(thm)],[f9189,f55])).
% 17.29/2.70 fof(f9428,plain,(
% 17.29/2.70 subset(relation_rng(relation_inverse(sK15_skl)),relation_dom(sK15_skl))),
% 17.29/2.70 inference(duplicate_literals_removal,[status(thm)],[f9423])).
% 17.29/2.70 fof(f10307,plain,(
% 17.29/2.70 ![X0]: (subset(relation_rng(sK15_skl),X0)|~relation(relation_inverse(sK15_skl))|in(sK0_skl(X0,relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))))),
% 17.29/2.70 inference(resolution,[status(thm)],[f1528,f137])).
% 17.29/2.70 fof(f10313,plain,(
% 17.29/2.70 ![X0]: (subset(relation_rng(sK15_skl),X0)|in(sK0_skl(X0,relation_rng(sK15_skl)),relation_dom(relation_inverse(sK15_skl))))),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f10307,f142])).
% 17.29/2.70 fof(f10337,plain,(
% 17.29/2.70 relation_dom(sK15_skl)=relation_rng(relation_inverse(sK15_skl))|~subset(relation_dom(sK15_skl),relation_rng(relation_inverse(sK15_skl)))),
% 17.29/2.70 inference(resolution,[status(thm)],[f9428,f48])).
% 17.29/2.70 fof(f10338,plain,(
% 17.29/2.70 relation_dom(sK15_skl)=relation_rng(relation_inverse(sK15_skl))),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f10337,f9124])).
% 17.29/2.70 fof(f10443,plain,(
% 17.29/2.70 ~relation_rng(sK15_skl)=relation_dom(relation_inverse(sK15_skl))|~relation_dom(sK15_skl)=relation_dom(sK15_skl)),
% 17.29/2.70 inference(backward_demodulation,[status(thm)],[f10338,f115])).
% 17.29/2.70 fof(f10468,plain,(
% 17.29/2.70 ~relation_rng(sK15_skl)=relation_dom(relation_inverse(sK15_skl))),
% 17.29/2.70 inference(trivial_equality_resolution,[status(thm)],[f10443])).
% 17.29/2.70 fof(f10783,plain,(
% 17.29/2.70 subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))|subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),
% 17.29/2.70 inference(resolution,[status(thm)],[f10313,f55])).
% 17.29/2.70 fof(f10788,plain,(
% 17.29/2.70 subset(relation_rng(sK15_skl),relation_dom(relation_inverse(sK15_skl)))),
% 17.29/2.70 inference(duplicate_literals_removal,[status(thm)],[f10783])).
% 17.29/2.70 fof(f12884,plain,(
% 17.29/2.70 relation_dom(relation_inverse(sK15_skl))=relation_rng(sK15_skl)|~subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),
% 17.29/2.70 inference(resolution,[status(thm)],[f10788,f48])).
% 17.29/2.70 fof(f12885,plain,(
% 17.29/2.70 ~subset(relation_dom(relation_inverse(sK15_skl)),relation_rng(sK15_skl))),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f12884,f10468])).
% 17.29/2.70 fof(f12890,plain,(
% 17.29/2.70 $false),
% 17.29/2.70 inference(forward_subsumption_resolution,[status(thm)],[f12885,f7494])).
% 17.29/2.70 % SZS output end CNFRefutation for theBenchmark.p
% 9.32/2.74 % Elapsed time: 2.359541 seconds
% 9.32/2.74 % CPU time: 18.327568 seconds
% 9.32/2.74 % Total memory used: 307.740 MB
% 9.32/2.74 % Net memory used: 294.008 MB
%------------------------------------------------------------------------------