%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU208+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:59 PM UTC 2026
% Result : Theorem 0.22s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU208+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.64 % Computer : n004.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:58:05 UTC 2026
% 0.18/0.64 % CPUTime :
% 0.22/0.68 % Drodi V4.1.1
% 0.22/0.83 % Refutation found
% 0.22/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.83 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.83 fof(f7,axiom,(
% 0.22/0.83 (! [A,B] :( relation(B)=> ( B = identity_relation(A)<=> (! [C,D] :( in(ordered_pair(C,D),B)<=> ( in(C,A)& C = D ) ) )) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f11,axiom,(
% 0.22/0.83 (! [A] :( relation(A)=> (! [B,C] :( C = relation_image(A,B)<=> (! [D] :( in(D,C)<=> (? [E] :( in(ordered_pair(E,D),A)& in(E,B) ) )) )) )) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f12,axiom,(
% 0.22/0.83 (! [A] :( relation(A)=> (! [B,C] :( C = relation_inverse_image(A,B)<=> (! [D] :( in(D,C)<=> (? [E] :( in(ordered_pair(D,E),A)& in(E,B) ) )) )) )) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f13,axiom,(
% 0.22/0.83 (! [A] :( relation(A)<=> (! [B] :~ ( in(B,A)& (! [C,D] : B != ordered_pair(C,D) )) )) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f30,axiom,(
% 0.22/0.83 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f71,axiom,(
% 0.22/0.83 empty(empty_set) ),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f81,axiom,(
% 0.22/0.83 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_rng(A)) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f83,axiom,(
% 0.22/0.83 (! [A] :( empty(A)=> ( empty(relation_rng(A))& relation(relation_rng(A)) ) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f103,axiom,(
% 0.22/0.83 (? [A] :( empty(A)& relation(A) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f131,conjecture,(
% 0.22/0.83 (! [A,B,C] :( relation(C)=> ( in(A,relation_inverse_image(C,B))<=> (? [D] :( in(D,relation_rng(C))& in(ordered_pair(A,D),C)& in(D,B) ) )) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f132,negated_conjecture,(
% 0.22/0.83 ~((! [A,B,C] :( relation(C)=> ( in(A,relation_inverse_image(C,B))<=> (? [D] :( in(D,relation_rng(C))& in(ordered_pair(A,D),C)& in(D,B) ) )) ) ))),
% 0.22/0.83 inference(negated_conjecture,[status(cth)],[f131])).
% 0.22/0.83 fof(f141,lemma,(
% 0.22/0.83 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f147,lemma,(
% 0.22/0.83 (! [A] : subset(empty_set,A) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f181,lemma,(
% 0.22/0.83 ( relation_dom(empty_set) = empty_set& relation_rng(empty_set) = empty_set ) ),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f184,lemma,(
% 0.22/0.83 (! [A] :( relation(A)=> ( ( relation_dom(A) = empty_set| relation_rng(A) = empty_set )=> A = empty_set ) ) )),
% 0.22/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.83 fof(f216,plain,(
% 0.22/0.83 ![A,B]: (~relation(B)|(B=identity_relation(A)<=>(![C,D]: (in(ordered_pair(C,D),B)<=>(in(C,A)&C=D)))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.22/0.83 fof(f217,plain,(
% 0.22/0.83 ![A,B]: (~relation(B)|((~B=identity_relation(A)|(![C,D]: ((~in(ordered_pair(C,D),B)|(in(C,A)&C=D))&(in(ordered_pair(C,D),B)|(~in(C,A)|~C=D)))))&(B=identity_relation(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))&(in(ordered_pair(C,D),B)|(in(C,A)&C=D)))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f216])).
% 0.22/0.83 fof(f218,plain,(
% 0.22/0.83 ![B]: (~relation(B)|((![A]: (~B=identity_relation(A)|((![C,D]: (~in(ordered_pair(C,D),B)|(in(C,A)&C=D)))&(![C,D]: (in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))))))&(![A]: (B=identity_relation(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))&(in(ordered_pair(C,D),B)|(in(C,A)&C=D))))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f217])).
% 0.22/0.83 fof(f219,plain,(
% 0.22/0.83 ![B]: (~relation(B)|((![A]: (~B=identity_relation(A)|((![C,D]: (~in(ordered_pair(C,D),B)|(in(C,A)&C=D)))&(![C,D]: (in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))))))&(![A]: (B=identity_relation(A)|((~in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|(~in(sK0_skl(A,B),A)|~sK0_skl(A,B)=sK1_skl(A,B)))&(in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|(in(sK0_skl(A,B),A)&sK0_skl(A,B)=sK1_skl(A,B))))))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f218])).
% 0.22/0.83 fof(f223,plain,(
% 0.22/0.83 ![X0,X1]: (~relation(X0)|X0=identity_relation(X1)|~in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)|~in(sK0_skl(X1,X0),X1)|~sK0_skl(X1,X0)=sK1_skl(X1,X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f219])).
% 0.22/0.83 fof(f224,plain,(
% 0.22/0.83 ![X0,X1]: (~relation(X0)|X0=identity_relation(X1)|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)|in(sK0_skl(X1,X0),X1))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f219])).
% 0.22/0.83 fof(f225,plain,(
% 0.22/0.83 ![X0,X1]: (~relation(X0)|X0=identity_relation(X1)|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)|sK0_skl(X1,X0)=sK1_skl(X1,X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f219])).
% 0.22/0.83 fof(f251,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B,C]: (C=relation_image(A,B)<=>(![D]: (in(D,C)<=>(?[E]: (in(ordered_pair(E,D),A)&in(E,B))))))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.22/0.83 fof(f252,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B,C]: ((~C=relation_image(A,B)|(![D]: ((~in(D,C)|(?[E]: (in(ordered_pair(E,D),A)&in(E,B))))&(in(D,C)|(![E]: (~in(ordered_pair(E,D),A)|~in(E,B)))))))&(C=relation_image(A,B)|(?[D]: ((~in(D,C)|(![E]: (~in(ordered_pair(E,D),A)|~in(E,B))))&(in(D,C)|(?[E]: (in(ordered_pair(E,D),A)&in(E,B))))))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f251])).
% 0.22/0.83 fof(f253,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((![B,C]: (~C=relation_image(A,B)|((![D]: (~in(D,C)|(?[E]: (in(ordered_pair(E,D),A)&in(E,B)))))&(![D]: (in(D,C)|(![E]: (~in(ordered_pair(E,D),A)|~in(E,B))))))))&(![B,C]: (C=relation_image(A,B)|(?[D]: ((~in(D,C)|(![E]: (~in(ordered_pair(E,D),A)|~in(E,B))))&(in(D,C)|(?[E]: (in(ordered_pair(E,D),A)&in(E,B))))))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f252])).
% 0.22/0.83 fof(f254,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((![B,C]: (~C=relation_image(A,B)|((![D]: (~in(D,C)|(in(ordered_pair(sK6_skl(D,C,B,A),D),A)&in(sK6_skl(D,C,B,A),B))))&(![D]: (in(D,C)|(![E]: (~in(ordered_pair(E,D),A)|~in(E,B))))))))&(![B,C]: (C=relation_image(A,B)|((~in(sK7_skl(C,B,A),C)|(![E]: (~in(ordered_pair(E,sK7_skl(C,B,A)),A)|~in(E,B))))&(in(sK7_skl(C,B,A),C)|(in(ordered_pair(sK8_skl(C,B,A),sK7_skl(C,B,A)),A)&in(sK8_skl(C,B,A),B))))))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl]),skolemize(E,sK6_skl(D,C,B,A)),skolemize(D,sK7_skl(C,B,A)),skolemize(E,sK8_skl(C,B,A))],[f253])).
% 0.22/0.83 fof(f257,plain,(
% 0.22/0.83 ![X0,X1,X2,X3,X4]: (~relation(X0)|~X1=relation_image(X0,X2)|in(X3,X1)|~in(ordered_pair(X4,X3),X0)|~in(X4,X2))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/0.83 fof(f258,plain,(
% 0.22/0.83 ![X0,X1,X2,X3]: (~relation(X0)|X1=relation_image(X0,X2)|~in(sK7_skl(X1,X2,X0),X1)|~in(ordered_pair(X3,sK7_skl(X1,X2,X0)),X0)|~in(X3,X2))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/0.83 fof(f259,plain,(
% 0.22/0.83 ![X0,X1,X2]: (~relation(X0)|X1=relation_image(X0,X2)|in(sK7_skl(X1,X2,X0),X1)|in(ordered_pair(sK8_skl(X1,X2,X0),sK7_skl(X1,X2,X0)),X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/0.83 fof(f260,plain,(
% 0.22/0.83 ![X0,X1,X2]: (~relation(X0)|X1=relation_image(X0,X2)|in(sK7_skl(X1,X2,X0),X1)|in(sK8_skl(X1,X2,X0),X2))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/0.83 fof(f261,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B,C]: (C=relation_inverse_image(A,B)<=>(![D]: (in(D,C)<=>(?[E]: (in(ordered_pair(D,E),A)&in(E,B))))))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.22/0.83 fof(f262,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B,C]: ((~C=relation_inverse_image(A,B)|(![D]: ((~in(D,C)|(?[E]: (in(ordered_pair(D,E),A)&in(E,B))))&(in(D,C)|(![E]: (~in(ordered_pair(D,E),A)|~in(E,B)))))))&(C=relation_inverse_image(A,B)|(?[D]: ((~in(D,C)|(![E]: (~in(ordered_pair(D,E),A)|~in(E,B))))&(in(D,C)|(?[E]: (in(ordered_pair(D,E),A)&in(E,B))))))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f261])).
% 0.22/0.83 fof(f263,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((![B,C]: (~C=relation_inverse_image(A,B)|((![D]: (~in(D,C)|(?[E]: (in(ordered_pair(D,E),A)&in(E,B)))))&(![D]: (in(D,C)|(![E]: (~in(ordered_pair(D,E),A)|~in(E,B))))))))&(![B,C]: (C=relation_inverse_image(A,B)|(?[D]: ((~in(D,C)|(![E]: (~in(ordered_pair(D,E),A)|~in(E,B))))&(in(D,C)|(?[E]: (in(ordered_pair(D,E),A)&in(E,B))))))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f262])).
% 0.22/0.83 fof(f264,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((![B,C]: (~C=relation_inverse_image(A,B)|((![D]: (~in(D,C)|(in(ordered_pair(D,sK9_skl(D,C,B,A)),A)&in(sK9_skl(D,C,B,A),B))))&(![D]: (in(D,C)|(![E]: (~in(ordered_pair(D,E),A)|~in(E,B))))))))&(![B,C]: (C=relation_inverse_image(A,B)|((~in(sK10_skl(C,B,A),C)|(![E]: (~in(ordered_pair(sK10_skl(C,B,A),E),A)|~in(E,B))))&(in(sK10_skl(C,B,A),C)|(in(ordered_pair(sK10_skl(C,B,A),sK11_skl(C,B,A)),A)&in(sK11_skl(C,B,A),B))))))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(E,sK9_skl(D,C,B,A)),skolemize(D,sK10_skl(C,B,A)),skolemize(E,sK11_skl(C,B,A))],[f263])).
% 0.22/0.83 fof(f265,plain,(
% 0.22/0.83 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_inverse_image(X0,X2)|~in(X3,X1)|in(ordered_pair(X3,sK9_skl(X3,X1,X2,X0)),X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f264])).
% 0.22/0.83 fof(f266,plain,(
% 0.22/0.83 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_inverse_image(X0,X2)|~in(X3,X1)|in(sK9_skl(X3,X1,X2,X0),X2))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f264])).
% 0.22/0.83 fof(f267,plain,(
% 0.22/0.83 ![X0,X1,X2,X3,X4]: (~relation(X0)|~X1=relation_inverse_image(X0,X2)|in(X3,X1)|~in(ordered_pair(X3,X4),X0)|~in(X4,X2))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f264])).
% 0.22/0.83 fof(f271,plain,(
% 0.22/0.83 ![A]: (relation(A)<=>(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.22/0.83 fof(f272,plain,(
% 0.22/0.83 ![A]: ((~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))&(relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f271])).
% 0.22/0.83 fof(f273,plain,(
% 0.22/0.83 (![A]: (~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D))))))&(![A]: (relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f272])).
% 0.22/0.83 fof(f274,plain,(
% 0.22/0.83 (![A]: (~relation(A)|(![B]: (~in(B,A)|B=ordered_pair(sK12_skl(B,A),sK13_skl(B,A))))))&(![A]: (relation(A)|(in(sK14_skl(A),A)&(![C,D]: ~sK14_skl(A)=ordered_pair(C,D)))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(C,sK12_skl(B,A)),skolemize(D,sK13_skl(B,A)),skolemize(B,sK14_skl(A))],[f273])).
% 0.22/0.83 fof(f275,plain,(
% 0.22/0.83 ![X0,X1]: (~relation(X0)|~in(X1,X0)|X1=ordered_pair(sK12_skl(X1,X0),sK13_skl(X1,X0)))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f274])).
% 0.22/0.83 fof(f400,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.22/0.83 fof(f401,plain,(
% 0.22/0.83 ![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)))))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f400])).
% 0.22/0.83 fof(f402,plain,(
% 0.22/0.83 ![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)))))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f401])).
% 0.22/0.83 fof(f403,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK41_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK42_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK42_skl(B,A)),A)))&(in(sK42_skl(B,A),B)|in(ordered_pair(sK43_skl(B,A),sK42_skl(B,A)),A)))))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl,sK43_skl]),skolemize(D,sK41_skl(C,B,A)),skolemize(C,sK42_skl(B,A)),skolemize(D,sK43_skl(B,A))],[f402])).
% 0.22/0.83 fof(f405,plain,(
% 0.22/0.83 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f403])).
% 0.22/0.83 fof(f478,plain,(
% 0.22/0.83 empty(empty_set)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f71])).
% 0.22/0.83 fof(f496,plain,(
% 0.22/0.83 ![A]: ((empty(A)|~relation(A))|~empty(relation_rng(A)))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.22/0.83 fof(f497,plain,(
% 0.22/0.83 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_rng(X0)))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f496])).
% 0.22/0.83 fof(f501,plain,(
% 0.22/0.83 ![A]: (~empty(A)|(empty(relation_rng(A))&relation(relation_rng(A))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.22/0.83 fof(f502,plain,(
% 0.22/0.83 ![X0]: (~empty(X0)|empty(relation_rng(X0)))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f501])).
% 0.22/0.83 fof(f503,plain,(
% 0.22/0.83 ![X0]: (~empty(X0)|relation(relation_rng(X0)))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f501])).
% 0.22/0.83 fof(f555,plain,(
% 0.22/0.83 (empty(sK53_skl)&relation(sK53_skl))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl]),skolemize(A,sK53_skl)],[f103])).
% 0.22/0.83 fof(f556,plain,(
% 0.22/0.83 empty(sK53_skl)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f555])).
% 0.22/0.83 fof(f557,plain,(
% 0.22/0.83 relation(sK53_skl)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f555])).
% 0.22/0.83 fof(f644,plain,(
% 0.22/0.83 (?[A,B,C]: (relation(C)&(in(A,relation_inverse_image(C,B))<~>(?[D]: ((in(D,relation_rng(C))&in(ordered_pair(A,D),C))&in(D,B))))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f132])).
% 0.22/0.83 fof(f645,plain,(
% 0.22/0.83 ?[A,B,C]: (relation(C)&((in(A,relation_inverse_image(C,B))|(?[D]: ((in(D,relation_rng(C))&in(ordered_pair(A,D),C))&in(D,B))))&(~in(A,relation_inverse_image(C,B))|(![D]: ((~in(D,relation_rng(C))|~in(ordered_pair(A,D),C))|~in(D,B))))))),
% 0.22/0.83 inference(NNF_transformation,[status(thm)],[f644])).
% 0.22/0.83 fof(f646,plain,(
% 0.22/0.83 ?[C]: (relation(C)&(?[A,B]: ((in(A,relation_inverse_image(C,B))|(?[D]: ((in(D,relation_rng(C))&in(ordered_pair(A,D),C))&in(D,B))))&(~in(A,relation_inverse_image(C,B))|(![D]: ((~in(D,relation_rng(C))|~in(ordered_pair(A,D),C))|~in(D,B)))))))),
% 0.22/0.83 inference(miniscoping,[status(thm)],[f645])).
% 0.22/0.83 fof(f647,plain,(
% 0.22/0.83 (relation(sK61_skl)&((in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|((in(sK64_skl,relation_rng(sK61_skl))&in(ordered_pair(sK62_skl,sK64_skl),sK61_skl))&in(sK64_skl,sK63_skl)))&(~in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|(![D]: ((~in(D,relation_rng(sK61_skl))|~in(ordered_pair(sK62_skl,D),sK61_skl))|~in(D,sK63_skl))))))),
% 0.22/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK61_skl,sK62_skl,sK63_skl,sK64_skl]),skolemize(C,sK61_skl),skolemize(A,sK62_skl),skolemize(B,sK63_skl),skolemize(D,sK64_skl)],[f646])).
% 0.22/0.83 fof(f648,plain,(
% 0.22/0.83 relation(sK61_skl)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f647])).
% 0.22/0.83 fof(f650,plain,(
% 0.22/0.83 in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|in(ordered_pair(sK62_skl,sK64_skl),sK61_skl)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f647])).
% 0.22/0.83 fof(f651,plain,(
% 0.22/0.83 in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|in(sK64_skl,sK63_skl)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f647])).
% 0.22/0.83 fof(f652,plain,(
% 0.22/0.83 ![X0]: (~in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|~in(X0,relation_rng(sK61_skl))|~in(ordered_pair(sK62_skl,X0),sK61_skl)|~in(X0,sK63_skl))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f647])).
% 0.22/0.83 fof(f669,plain,(
% 0.22/0.83 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(A,B)|(subset(relation_dom(A),relation_dom(B))&subset(relation_rng(A),relation_rng(B)))))))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f141])).
% 0.22/0.83 fof(f671,plain,(
% 0.22/0.83 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(X0,X1)|subset(relation_rng(X0),relation_rng(X1)))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f669])).
% 0.22/0.83 fof(f685,plain,(
% 0.22/0.83 ![X0]: (subset(empty_set,X0))),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f147])).
% 0.22/0.83 fof(f777,plain,(
% 0.22/0.83 relation_rng(empty_set)=empty_set),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f181])).
% 0.22/0.83 fof(f783,plain,(
% 0.22/0.83 ![A]: (~relation(A)|((~relation_dom(A)=empty_set&~relation_rng(A)=empty_set)|A=empty_set))),
% 0.22/0.83 inference(pre_NNF_transformation,[status(thm)],[f184])).
% 0.22/0.83 fof(f785,plain,(
% 0.22/0.83 ![X0]: (~relation(X0)|~relation_rng(X0)=empty_set|X0=empty_set)),
% 0.22/0.83 inference(cnf_transformation,[status(thm)],[f783])).
% 0.22/0.83 fof(f862,definition,(
% 0.22/0.83 sQ0_spl <=> (in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f863,plain,(
% 0.22/0.85 in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|~sQ0_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f862])).
% 0.22/0.85 fof(f869,definition,(
% 0.22/0.85 sQ2_spl <=> (in(ordered_pair(sK62_skl,sK64_skl),sK61_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f870,plain,(
% 0.22/0.85 in(ordered_pair(sK62_skl,sK64_skl),sK61_skl)|~sQ2_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f869])).
% 0.22/0.85 fof(f872,plain,(
% 0.22/0.85 sQ0_spl|sQ2_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f650,f862,f869])).
% 0.22/0.85 fof(f873,definition,(
% 0.22/0.85 sQ3_spl <=> (in(sK64_skl,sK63_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f874,plain,(
% 0.22/0.85 in(sK64_skl,sK63_skl)|~sQ3_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f873])).
% 0.22/0.85 fof(f876,plain,(
% 0.22/0.85 sQ0_spl|sQ3_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f651,f862,f873])).
% 0.22/0.85 fof(f877,definition,(
% 0.22/0.85 ![X0]: (sQ4_spl <=> (~in(X0,relation_rng(sK61_skl))|~in(ordered_pair(sK62_skl,X0),sK61_skl)|~in(X0,sK63_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f878,plain,(
% 0.22/0.85 ![X0]: (~in(X0,relation_rng(sK61_skl))|~in(ordered_pair(sK62_skl,X0),sK61_skl)|~in(X0,sK63_skl)|~sQ4_spl)),
% 0.22/0.85 inference(component_clause,[status(thm)],[f877])).
% 0.22/0.85 fof(f880,plain,(
% 0.22/0.85 ~sQ0_spl|sQ4_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f652,f862,f877])).
% 0.22/0.85 fof(f894,plain,(
% 0.22/0.85 ![X0,X1,X2,X3]: (~relation(X0)|in(X1,relation_image(X0,X2))|~in(ordered_pair(X3,X1),X0)|~in(X3,X2))),
% 0.22/0.85 inference(destructive_equality_resolution,[status(thm)],[f257])).
% 0.22/0.85 fof(f895,plain,(
% 0.22/0.85 ![X0,X1,X2]: (~relation(X0)|~in(X1,relation_inverse_image(X0,X2))|in(ordered_pair(X1,sK9_skl(X1,relation_inverse_image(X0,X2),X2,X0)),X0))),
% 0.22/0.85 inference(destructive_equality_resolution,[status(thm)],[f265])).
% 0.22/0.85 fof(f896,plain,(
% 0.22/0.85 ![X0,X1,X2]: (~relation(X0)|~in(X1,relation_inverse_image(X0,X2))|in(sK9_skl(X1,relation_inverse_image(X0,X2),X2,X0),X2))),
% 0.22/0.85 inference(destructive_equality_resolution,[status(thm)],[f266])).
% 0.22/0.85 fof(f897,plain,(
% 0.22/0.85 ![X0,X1,X2,X3]: (~relation(X0)|in(X1,relation_inverse_image(X0,X2))|~in(ordered_pair(X1,X3),X0)|~in(X3,X2))),
% 0.22/0.85 inference(destructive_equality_resolution,[status(thm)],[f267])).
% 0.22/0.85 fof(f928,plain,(
% 0.22/0.85 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 0.22/0.85 inference(destructive_equality_resolution,[status(thm)],[f405])).
% 0.22/0.85 fof(f948,plain,(
% 0.22/0.85 ![X0]: (~relation(sK61_skl)|in(sK62_skl,relation_inverse_image(sK61_skl,X0))|~in(sK64_skl,X0)|~sQ2_spl)),
% 0.22/0.85 inference(resolution,[status(thm)],[f870,f897])).
% 0.22/0.85 fof(f950,definition,(
% 0.22/0.85 sQ5_spl <=> (relation(sK61_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f952,plain,(
% 0.22/0.85 ~relation(sK61_skl)|sQ5_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f950])).
% 0.22/0.85 fof(f953,definition,(
% 0.22/0.85 ![X0]: (sQ6_spl <=> (in(sK62_skl,relation_inverse_image(sK61_skl,X0))|~in(sK64_skl,X0)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f954,plain,(
% 0.22/0.85 ![X0]: (in(sK62_skl,relation_inverse_image(sK61_skl,X0))|~in(sK64_skl,X0)|~sQ6_spl)),
% 0.22/0.85 inference(component_clause,[status(thm)],[f953])).
% 0.22/0.85 fof(f956,plain,(
% 0.22/0.85 ~sQ5_spl|sQ6_spl|~sQ2_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f948,f950,f953,f869])).
% 0.22/0.85 fof(f961,definition,(
% 0.22/0.85 sQ8_spl <=> (relation(empty_set))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f963,plain,(
% 0.22/0.85 ~relation(empty_set)|sQ8_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f961])).
% 0.22/0.85 fof(f965,plain,(
% 0.22/0.85 relation(relation_rng(empty_set))),
% 0.22/0.85 inference(resolution,[status(thm)],[f478,f503])).
% 0.22/0.85 fof(f968,plain,(
% 0.22/0.85 relation(empty_set)),
% 0.22/0.85 inference(forward_demodulation,[status(thm)],[f777,f965])).
% 0.22/0.85 fof(f983,plain,(
% 0.22/0.85 empty(relation_rng(sK53_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f556,f502])).
% 0.22/0.85 fof(f985,plain,(
% 0.22/0.85 empty(sK53_skl)|~relation(sK53_skl)),
% 0.22/0.85 inference(resolution,[status(thm)],[f983,f497])).
% 0.22/0.85 fof(f989,definition,(
% 0.22/0.85 sQ9_spl <=> (empty(sK53_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f992,definition,(
% 0.22/0.85 sQ10_spl <=> (relation(sK53_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f994,plain,(
% 0.22/0.85 ~relation(sK53_skl)|sQ10_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f992])).
% 0.22/0.85 fof(f995,plain,(
% 0.22/0.85 sQ9_spl|~sQ10_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f985,f989,f992])).
% 0.22/0.85 fof(f998,plain,(
% 0.22/0.85 ~relation_rng(empty_set)=empty_set|empty_set=empty_set),
% 0.22/0.85 inference(resolution,[status(thm)],[f785,f968])).
% 0.22/0.85 fof(f1007,definition,(
% 0.22/0.85 sQ13_spl <=> (relation_rng(empty_set)=empty_set)),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1009,plain,(
% 0.22/0.85 ~relation_rng(empty_set)=empty_set|sQ13_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f1007])).
% 0.22/0.85 fof(f1010,definition,(
% 0.22/0.85 sQ14_spl <=> (empty_set=empty_set)),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1013,plain,(
% 0.22/0.85 ~sQ13_spl|sQ14_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f998,f1007,f1010])).
% 0.22/0.85 fof(f1021,plain,(
% 0.22/0.85 ~empty_set=empty_set|sQ13_spl),
% 0.22/0.85 inference(forward_demodulation,[status(thm)],[f777,f1009])).
% 0.22/0.85 fof(f1022,plain,(
% 0.22/0.85 $false|sQ13_spl),
% 0.22/0.85 inference(trivial_equality_resolution,[status(thm)],[f1021])).
% 0.22/0.85 fof(f1023,plain,(
% 0.22/0.85 sQ13_spl),
% 0.22/0.85 inference(contradiction_clause,[status(thm)],[f1022])).
% 0.22/0.85 fof(f1035,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|in(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl)|in(sK0_skl(X0,sK61_skl),X0))),
% 0.22/0.85 inference(resolution,[status(thm)],[f224,f648])).
% 0.22/0.85 fof(f1039,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|in(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f225,f648])).
% 0.22/0.85 fof(f1068,plain,(
% 0.22/0.85 $false|sQ10_spl),
% 0.22/0.85 inference(forward_subsumption_resolution,[status(thm)],[f994,f557])).
% 0.22/0.85 fof(f1069,plain,(
% 0.22/0.85 sQ10_spl),
% 0.22/0.85 inference(contradiction_clause,[status(thm)],[f1068])).
% 0.22/0.85 fof(f1209,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|~relation(sK61_skl)|sK61_skl=identity_relation(X0)|~in(sK0_skl(X0,sK61_skl),X0)|~sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1035,f223])).
% 0.22/0.85 fof(f1210,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|~relation(sK61_skl)|in(sK1_skl(X0,sK61_skl),relation_rng(sK61_skl)))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1035,f928])).
% 0.22/0.85 fof(f1211,plain,(
% 0.22/0.85 ![X0,X1]: (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|~relation(sK61_skl)|in(sK0_skl(X0,sK61_skl),relation_inverse_image(sK61_skl,X1))|~in(sK1_skl(X0,sK61_skl),X1))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1035,f897])).
% 0.22/0.85 fof(f1213,definition,(
% 0.22/0.85 ![X0]: (sQ36_spl <=> (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|sK61_skl=identity_relation(X0)|~in(sK0_skl(X0,sK61_skl),X0)|~sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1216,plain,(
% 0.22/0.85 sQ36_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1209,f1213,f950])).
% 0.22/0.85 fof(f1217,definition,(
% 0.22/0.85 ![X0]: (sQ37_spl <=> (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|in(sK1_skl(X0,sK61_skl),relation_rng(sK61_skl))))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1220,plain,(
% 0.22/0.85 sQ37_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1210,f1217,f950])).
% 0.22/0.85 fof(f1221,definition,(
% 0.22/0.85 ![X0,X1]: (sQ38_spl <=> (sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)|in(sK0_skl(X0,sK61_skl),relation_inverse_image(sK61_skl,X1))|~in(sK1_skl(X0,sK61_skl),X1)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1224,plain,(
% 0.22/0.85 sQ38_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1211,f1221,f950])).
% 0.22/0.85 fof(f1225,plain,(
% 0.22/0.85 $false|sQ5_spl),
% 0.22/0.85 inference(forward_subsumption_resolution,[status(thm)],[f952,f648])).
% 0.22/0.85 fof(f1226,plain,(
% 0.22/0.85 sQ5_spl),
% 0.22/0.85 inference(contradiction_clause,[status(thm)],[f1225])).
% 0.22/0.85 fof(f1227,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|~relation(sK61_skl)|sK61_skl=identity_relation(X0)|~in(sK0_skl(X0,sK61_skl),X0)|~sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1039,f223])).
% 0.22/0.85 fof(f1228,plain,(
% 0.22/0.85 ![X0]: (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|~relation(sK61_skl)|in(sK1_skl(X0,sK61_skl),relation_rng(sK61_skl)))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1039,f928])).
% 0.22/0.85 fof(f1229,plain,(
% 0.22/0.85 ![X0,X1]: (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|~relation(sK61_skl)|in(sK0_skl(X0,sK61_skl),relation_inverse_image(sK61_skl,X1))|~in(sK1_skl(X0,sK61_skl),X1))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1039,f897])).
% 0.22/0.85 fof(f1231,definition,(
% 0.22/0.85 ![X0]: (sQ39_spl <=> (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|sK61_skl=identity_relation(X0)|~in(sK0_skl(X0,sK61_skl),X0)|~sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1234,plain,(
% 0.22/0.85 sQ39_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1227,f1231,f950])).
% 0.22/0.85 fof(f1235,definition,(
% 0.22/0.85 ![X0]: (sQ40_spl <=> (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|in(sK1_skl(X0,sK61_skl),relation_rng(sK61_skl))))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1238,plain,(
% 0.22/0.85 sQ40_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1228,f1235,f950])).
% 0.22/0.85 fof(f1239,definition,(
% 0.22/0.85 ![X0,X1]: (sQ41_spl <=> (sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)|in(sK0_skl(X0,sK61_skl),relation_inverse_image(sK61_skl,X1))|~in(sK1_skl(X0,sK61_skl),X1)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1242,plain,(
% 0.22/0.85 sQ41_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1229,f1239,f950])).
% 0.22/0.85 fof(f1254,plain,(
% 0.22/0.85 ![X0,X1]: (~relation(sK61_skl)|in(sK1_skl(X0,sK61_skl),relation_image(sK61_skl,X1))|~in(sK0_skl(X0,sK61_skl),X1)|sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f894,f1039])).
% 0.22/0.85 fof(f1255,plain,(
% 0.22/0.85 ![X0,X1]: (~relation(sK61_skl)|in(sK1_skl(X0,sK61_skl),relation_image(sK61_skl,X1))|~in(sK0_skl(X0,sK61_skl),X1)|sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0))),
% 0.22/0.85 inference(resolution,[status(thm)],[f894,f1035])).
% 0.22/0.85 fof(f1256,definition,(
% 0.22/0.85 ![X0,X1]: (sQ42_spl <=> (in(sK1_skl(X0,sK61_skl),relation_image(sK61_skl,X1))|~in(sK0_skl(X0,sK61_skl),X1)|sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1259,plain,(
% 0.22/0.85 ~sQ5_spl|sQ42_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1254,f950,f1256])).
% 0.22/0.85 fof(f1260,definition,(
% 0.22/0.85 ![X0,X1]: (sQ43_spl <=> (in(sK1_skl(X0,sK61_skl),relation_image(sK61_skl,X1))|~in(sK0_skl(X0,sK61_skl),X1)|sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1263,plain,(
% 0.22/0.85 ~sQ5_spl|sQ43_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1255,f950,f1260])).
% 0.22/0.85 fof(f1295,plain,(
% 0.22/0.85 ![X0,X1]: (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|in(ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl)),sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f259,f648])).
% 0.22/0.85 fof(f1303,plain,(
% 0.22/0.85 ![X0,X1]: (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|in(sK8_skl(X0,X1,sK61_skl),X1))),
% 0.22/0.85 inference(resolution,[status(thm)],[f260,f648])).
% 0.22/0.85 fof(f1351,plain,(
% 0.22/0.85 ~relation(sK61_skl)|in(ordered_pair(sK62_skl,sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl)),sK61_skl)|~sQ0_spl),
% 0.22/0.85 inference(resolution,[status(thm)],[f895,f863])).
% 0.22/0.85 fof(f1352,definition,(
% 0.22/0.85 sQ47_spl <=> (in(ordered_pair(sK62_skl,sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl)),sK61_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1353,plain,(
% 0.22/0.85 in(ordered_pair(sK62_skl,sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl)),sK61_skl)|~sQ47_spl),
% 0.22/0.85 inference(component_clause,[status(thm)],[f1352])).
% 0.22/0.85 fof(f1355,plain,(
% 0.22/0.85 ~sQ5_spl|sQ47_spl|~sQ0_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1351,f950,f1352,f862])).
% 0.22/0.85 fof(f1356,plain,(
% 0.22/0.85 ~relation(sK61_skl)|in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),sK63_skl)|~sQ0_spl),
% 0.22/0.85 inference(resolution,[status(thm)],[f896,f863])).
% 0.22/0.85 fof(f1357,definition,(
% 0.22/0.85 sQ48_spl <=> (in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),sK63_skl))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1360,plain,(
% 0.22/0.85 ~sQ5_spl|sQ48_spl|~sQ0_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1356,f950,f1357,f862])).
% 0.22/0.85 fof(f1363,plain,(
% 0.22/0.85 ![X0,X1,X2]: (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|~relation(sK61_skl)|in(sK7_skl(X0,X1,sK61_skl),relation_image(sK61_skl,X2))|~in(sK8_skl(X0,X1,sK61_skl),X2))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1295,f894])).
% 0.22/0.85 fof(f1364,plain,(
% 0.22/0.85 ![X0,X1]: (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|~relation(sK61_skl)|in(sK7_skl(X0,X1,sK61_skl),relation_rng(sK61_skl)))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1295,f928])).
% 0.22/0.85 fof(f1365,plain,(
% 0.22/0.85 ![X0,X1,X2]: (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|~relation(sK61_skl)|in(sK8_skl(X0,X1,sK61_skl),relation_inverse_image(sK61_skl,X2))|~in(sK7_skl(X0,X1,sK61_skl),X2))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1295,f897])).
% 0.22/0.85 fof(f1367,definition,(
% 0.22/0.85 ![X0,X1,X2]: (sQ49_spl <=> (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|in(sK7_skl(X0,X1,sK61_skl),relation_image(sK61_skl,X2))|~in(sK8_skl(X0,X1,sK61_skl),X2)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1370,plain,(
% 0.22/0.85 sQ49_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1363,f1367,f950])).
% 0.22/0.85 fof(f1371,definition,(
% 0.22/0.85 ![X0,X1]: (sQ50_spl <=> (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|in(sK7_skl(X0,X1,sK61_skl),relation_rng(sK61_skl))))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1374,plain,(
% 0.22/0.85 sQ50_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1364,f1371,f950])).
% 0.22/0.85 fof(f1375,definition,(
% 0.22/0.85 ![X0,X1,X2]: (sQ51_spl <=> (X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)|in(sK8_skl(X0,X1,sK61_skl),relation_inverse_image(sK61_skl,X2))|~in(sK7_skl(X0,X1,sK61_skl),X2)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1378,plain,(
% 0.22/0.85 sQ51_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1365,f1375,f950])).
% 0.22/0.85 fof(f1379,plain,(
% 0.22/0.85 ![X0,X1,X2]: (X0=relation_image(sK61_skl,X1)|in(sK8_skl(X0,X1,sK61_skl),X1)|~relation(sK61_skl)|X0=relation_image(sK61_skl,X1)|~in(ordered_pair(X2,sK7_skl(X0,X1,sK61_skl)),sK61_skl)|~in(X2,X1))),
% 0.22/0.85 inference(resolution,[status(thm)],[f1303,f258])).
% 0.22/0.85 fof(f1392,definition,(
% 0.22/0.85 ![X0,X1,X2]: (sQ52_spl <=> (X0=relation_image(sK61_skl,X1)|in(sK8_skl(X0,X1,sK61_skl),X1)|X0=relation_image(sK61_skl,X1)|~in(ordered_pair(X2,sK7_skl(X0,X1,sK61_skl)),sK61_skl)|~in(X2,X1)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1395,plain,(
% 0.22/0.85 sQ52_spl|~sQ5_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1379,f1392,f950])).
% 0.22/0.85 fof(f1401,plain,(
% 0.22/0.85 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_rng(empty_set),relation_rng(X0)))),
% 0.22/0.85 inference(resolution,[status(thm)],[f685,f671])).
% 0.22/0.85 fof(f1402,definition,(
% 0.22/0.85 ![X0]: (sQ53_spl <=> (~relation(X0)|subset(relation_rng(empty_set),relation_rng(X0))))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1405,plain,(
% 0.22/0.85 ~sQ8_spl|sQ53_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1401,f961,f1402])).
% 0.22/0.85 fof(f1406,plain,(
% 0.22/0.85 $false|sQ8_spl),
% 0.22/0.85 inference(forward_subsumption_resolution,[status(thm)],[f963,f968])).
% 0.22/0.85 fof(f1407,plain,(
% 0.22/0.85 sQ8_spl),
% 0.22/0.85 inference(contradiction_clause,[status(thm)],[f1406])).
% 0.22/0.85 fof(f1444,plain,(
% 0.22/0.85 ![X0,X1]: (~relation(sK61_skl)|ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl)),sK61_skl))|X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0))),
% 0.22/0.85 inference(resolution,[status(thm)],[f275,f1295])).
% 0.22/0.85 fof(f1445,plain,(
% 0.22/0.85 ![X0]: (~relation(sK61_skl)|ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl))|sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl))),
% 0.22/0.85 inference(resolution,[status(thm)],[f275,f1039])).
% 0.22/0.85 fof(f1446,plain,(
% 0.22/0.85 ![X0]: (~relation(sK61_skl)|ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl))|sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0))),
% 0.22/0.85 inference(resolution,[status(thm)],[f275,f1035])).
% 0.22/0.85 fof(f1455,definition,(
% 0.22/0.85 ![X0,X1]: (sQ56_spl <=> (ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK8_skl(X0,X1,sK61_skl),sK7_skl(X0,X1,sK61_skl)),sK61_skl))|X0=relation_image(sK61_skl,X1)|in(sK7_skl(X0,X1,sK61_skl),X0)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1458,plain,(
% 0.22/0.85 ~sQ5_spl|sQ56_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1444,f950,f1455])).
% 0.22/0.85 fof(f1459,definition,(
% 0.22/0.85 ![X0]: (sQ57_spl <=> (ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl))|sK61_skl=identity_relation(X0)|sK0_skl(X0,sK61_skl)=sK1_skl(X0,sK61_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1462,plain,(
% 0.22/0.85 ~sQ5_spl|sQ57_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1445,f950,f1459])).
% 0.22/0.85 fof(f1463,definition,(
% 0.22/0.85 ![X0]: (sQ58_spl <=> (ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl))=ordered_pair(sK12_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl),sK13_skl(ordered_pair(sK0_skl(X0,sK61_skl),sK1_skl(X0,sK61_skl)),sK61_skl))|sK61_skl=identity_relation(X0)|in(sK0_skl(X0,sK61_skl),X0)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1466,plain,(
% 0.22/0.85 ~sQ5_spl|sQ58_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1446,f950,f1463])).
% 0.22/0.85 fof(f1474,plain,(
% 0.22/0.85 ~in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),relation_rng(sK61_skl))|~in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),sK63_skl)|~sQ47_spl|~sQ4_spl),
% 0.22/0.85 inference(resolution,[status(thm)],[f1353,f878])).
% 0.22/0.85 fof(f1476,plain,(
% 0.22/0.85 ~relation(sK61_skl)|in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),relation_rng(sK61_skl))|~sQ47_spl),
% 0.22/0.85 inference(resolution,[status(thm)],[f1353,f928])).
% 0.22/0.85 fof(f1480,definition,(
% 0.22/0.85 sQ61_spl <=> (in(sK9_skl(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl),sK63_skl,sK61_skl),relation_rng(sK61_skl)))),
% 0.22/0.85 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.22/0.85 fof(f1483,plain,(
% 0.22/0.85 ~sQ61_spl|~sQ48_spl|~sQ47_spl|~sQ4_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1474,f1480,f1357,f1352,f877])).
% 0.22/0.85 fof(f1488,plain,(
% 0.22/0.85 ~sQ5_spl|sQ61_spl|~sQ47_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1476,f950,f1480,f1352])).
% 0.22/0.85 fof(f1497,plain,(
% 0.22/0.85 in(sK62_skl,relation_inverse_image(sK61_skl,sK63_skl))|~sQ3_spl|~sQ6_spl),
% 0.22/0.85 inference(resolution,[status(thm)],[f874,f954])).
% 0.22/0.85 fof(f1500,plain,(
% 0.22/0.85 sQ0_spl|~sQ3_spl|~sQ6_spl),
% 0.22/0.85 inference(split_clause,[status(thm)],[f1497,f862,f873,f953])).
% 0.22/0.86 fof(f1508,plain,(
% 0.22/0.86 $false),
% 0.22/0.86 inference(sat_refutation,[status(thm)],[f872,f876,f880,f956,f995,f1013,f1023,f1069,f1216,f1220,f1224,f1226,f1234,f1238,f1242,f1259,f1263,f1355,f1360,f1370,f1374,f1378,f1395,f1405,f1407,f1458,f1462,f1466,f1483,f1488,f1500])).
% 0.22/0.86 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.87 % Elapsed time: 0.206736 seconds
% 0.22/0.87 % CPU time: 1.273080 seconds
% 0.22/0.87 % Total memory used: 128.972 MB
% 0.22/0.87 % Net memory used: 127.301 MB
%------------------------------------------------------------------------------