%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU203+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 : n002.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:58 PM UTC 2026
% Result : Theorem 0.14s 0.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU203+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n002.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Mon Sep 21 06:00:04 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.60 % Drodi V4.1.1
% 0.14/0.93 % Refutation found
% 0.14/0.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.93 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.93 fof(f1,axiom,(
% 0.14/0.93 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f3,axiom,(
% 0.14/0.93 (! [A] :( empty(A)=> relation(A) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f5,axiom,(
% 0.14/0.93 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f6,axiom,(
% 0.14/0.93 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f7,axiom,(
% 0.14/0.93 (! [A,B] :( relation(B)=> ( B = identity_relation(A)<=> (! [C,D] :( in(ordered_pair(C,D),B)<=> ( in(C,A)& C = D ) ) )) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f9,axiom,(
% 0.14/0.93 (! [A] :( relation(A)=> (! [B,C] :( relation(C)=> ( C = relation_dom_restriction(A,B)<=> (! [D,E] :( in(ordered_pair(D,E),C)<=> ( in(D,B)& in(ordered_pair(D,E),A) ) ) )) ) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f10,axiom,(
% 0.14/0.93 (! [A,B] :( relation(B)=> (! [C] :( relation(C)=> ( C = relation_rng_restriction(A,B)<=> (! [D,E] :( in(ordered_pair(D,E),C)<=> ( in(E,A)& in(ordered_pair(D,E),B) ) ) )) ) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f11,axiom,(
% 0.14/0.93 (! [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.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f12,axiom,(
% 0.14/0.93 (! [A] :( relation(A)<=> (! [B] :~ ( in(B,A)& (! [C,D] : B != ordered_pair(C,D) )) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f13,axiom,(
% 0.14/0.93 (! [A,B] :( ( A != empty_set=> ( B = set_meet(A)<=> (! [C] :( in(C,B)<=> (! [D] :( in(D,A)=> in(C,D) ) )) )) )& ( A = empty_set=> ( B = set_meet(A)<=> B = empty_set ) ) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f15,axiom,(
% 0.14/0.93 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f25,axiom,(
% 0.14/0.93 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f52,axiom,(
% 0.14/0.93 (! [A] :( relation(A)=> relation(relation_inverse(A)) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f57,axiom,(
% 0.14/0.93 (! [A] : relation(identity_relation(A)) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f69,axiom,(
% 0.14/0.93 empty(empty_set) ),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f76,axiom,(
% 0.14/0.93 ( empty(empty_set)& relation(empty_set) ) ),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f80,axiom,(
% 0.14/0.93 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f84,axiom,(
% 0.14/0.93 (! [A,B] : set_intersection2(A,A) = A )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f86,axiom,(
% 0.14/0.93 (! [A] :( relation(A)=> relation_inverse(relation_inverse(A)) = A ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f101,axiom,(
% 0.14/0.93 (? [A] :( empty(A)& relation(A) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f103,axiom,(
% 0.14/0.93 (? [A] : empty(A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f104,axiom,(
% 0.14/0.93 (? [A] :( ~ empty(A)& relation(A) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f105,axiom,(
% 0.14/0.93 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f124,conjecture,(
% 0.14/0.93 (! [A,B,C] :( relation(C)=> ( in(A,relation_image(C,B))<=> (? [D] :( in(D,relation_dom(C))& in(ordered_pair(D,A),C)& in(D,B) ) )) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f125,negated_conjecture,(
% 0.14/0.93 ~((! [A,B,C] :( relation(C)=> ( in(A,relation_image(C,B))<=> (? [D] :( in(D,relation_dom(C))& in(ordered_pair(D,A),C)& in(D,B) ) )) ) ))),
% 0.14/0.93 inference(negated_conjecture,[status(cth)],[f124])).
% 0.14/0.93 fof(f126,lemma,(
% 0.14/0.93 (! [A,B] : subset(set_intersection2(A,B),A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f128,axiom,(
% 0.14/0.93 (! [A] : set_union2(A,empty_set) = A )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f134,lemma,(
% 0.14/0.93 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f137,axiom,(
% 0.14/0.93 (! [A] : set_intersection2(A,empty_set) = empty_set )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f140,lemma,(
% 0.14/0.93 (! [A] : subset(empty_set,A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f144,lemma,(
% 0.14/0.93 (! [A,B] : subset(set_difference(A,B),A) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f167,axiom,(
% 0.14/0.93 (! [A] : set_difference(empty_set,A) = empty_set )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f174,lemma,(
% 0.14/0.93 ( relation_dom(empty_set) = empty_set& relation_rng(empty_set) = empty_set ) ),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f177,lemma,(
% 0.14/0.93 (! [A] :( relation(A)=> ( ( relation_dom(A) = empty_set| relation_rng(A) = empty_set )=> A = empty_set ) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f178,lemma,(
% 0.14/0.93 (! [A] :( relation(A)=> ( relation_dom(A) = empty_set<=> relation_rng(A) = empty_set ) ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f181,axiom,(
% 0.14/0.93 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f183,lemma,(
% 0.14/0.93 (! [A] :( relation_dom(identity_relation(A)) = A& relation_rng(identity_relation(A)) = A ) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f186,lemma,(
% 0.14/0.93 (! [A,B] : subset(A,set_union2(A,B)) )),
% 0.14/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.93 fof(f200,plain,(
% 0.14/0.93 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/0.93 fof(f201,plain,(
% 0.14/0.93 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/0.93 fof(f204,plain,(
% 0.14/0.93 ![A]: (~empty(A)|relation(A))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/0.93 fof(f205,plain,(
% 0.14/0.93 ![X0]: (~empty(X0)|relation(X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f204])).
% 0.14/0.93 fof(f207,plain,(
% 0.14/0.93 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.93 fof(f208,plain,(
% 0.14/0.93 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.93 fof(f209,plain,(
% 0.14/0.93 ![A,B]: (~relation(B)|(B=identity_relation(A)<=>(![C,D]: (in(ordered_pair(C,D),B)<=>(in(C,A)&C=D)))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/0.93 fof(f210,plain,(
% 0.14/0.93 ![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.14/0.93 inference(NNF_transformation,[status(thm)],[f209])).
% 0.14/0.93 fof(f211,plain,(
% 0.14/0.93 ![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.14/0.93 inference(miniscoping,[status(thm)],[f210])).
% 0.14/0.93 fof(f212,plain,(
% 0.14/0.93 ![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.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f211])).
% 0.14/0.93 fof(f217,plain,(
% 0.14/0.93 ![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.14/0.93 inference(cnf_transformation,[status(thm)],[f212])).
% 0.14/0.93 fof(f218,plain,(
% 0.14/0.93 ![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.14/0.93 inference(cnf_transformation,[status(thm)],[f212])).
% 0.14/0.93 fof(f224,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![B,C]: (~relation(C)|(C=relation_dom_restriction(A,B)<=>(![D,E]: (in(ordered_pair(D,E),C)<=>(in(D,B)&in(ordered_pair(D,E),A))))))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.93 fof(f225,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![B,C]: (~relation(C)|((~C=relation_dom_restriction(A,B)|(![D,E]: ((~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A))))))&(C=relation_dom_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))))))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f224])).
% 0.14/0.93 fof(f226,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![C]: (~relation(C)|((![B]: (~C=relation_dom_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))))))&(![B]: (C=relation_dom_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A)))))))))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f225])).
% 0.14/0.93 fof(f227,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![C]: (~relation(C)|((![B]: (~C=relation_dom_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))))))&(![B]: (C=relation_dom_restriction(A,B)|((~in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C)|(~in(sK2_skl(B,C,A),B)|~in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A)))&(in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C)|(in(sK2_skl(B,C,A),B)&in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A))))))))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(D,sK2_skl(B,C,A)),skolemize(E,sK3_skl(B,C,A))],[f226])).
% 0.14/0.93 fof(f232,plain,(
% 0.14/0.93 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|X1=relation_dom_restriction(X0,X2)|in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)|in(sK2_skl(X2,X1,X0),X2))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f227])).
% 0.14/0.93 fof(f234,plain,(
% 0.14/0.93 ![A,B]: (~relation(B)|(![C]: (~relation(C)|(C=relation_rng_restriction(A,B)<=>(![D,E]: (in(ordered_pair(D,E),C)<=>(in(E,A)&in(ordered_pair(D,E),B))))))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.14/0.93 fof(f235,plain,(
% 0.14/0.93 ![A,B]: (~relation(B)|(![C]: (~relation(C)|((~C=relation_rng_restriction(A,B)|(![D,E]: ((~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B))))))&(C=relation_rng_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))))))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f234])).
% 0.14/0.93 fof(f236,plain,(
% 0.14/0.93 ![B]: (~relation(B)|(![C]: (~relation(C)|((![A]: (~C=relation_rng_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))))))&(![A]: (C=relation_rng_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B)))))))))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f235])).
% 0.14/0.93 fof(f237,plain,(
% 0.14/0.93 ![B]: (~relation(B)|(![C]: (~relation(C)|((![A]: (~C=relation_rng_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))))))&(![A]: (C=relation_rng_restriction(A,B)|((~in(ordered_pair(sK4_skl(A,C,B),sK5_skl(A,C,B)),C)|(~in(sK5_skl(A,C,B),A)|~in(ordered_pair(sK4_skl(A,C,B),sK5_skl(A,C,B)),B)))&(in(ordered_pair(sK4_skl(A,C,B),sK5_skl(A,C,B)),C)|(in(sK5_skl(A,C,B),A)&in(ordered_pair(sK4_skl(A,C,B),sK5_skl(A,C,B)),B))))))))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(D,sK4_skl(A,C,B)),skolemize(E,sK5_skl(A,C,B))],[f236])).
% 0.14/0.93 fof(f242,plain,(
% 0.14/0.93 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|X1=relation_rng_restriction(X2,X0)|in(ordered_pair(sK4_skl(X2,X1,X0),sK5_skl(X2,X1,X0)),X1)|in(sK5_skl(X2,X1,X0),X2))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f237])).
% 0.14/0.93 fof(f244,plain,(
% 0.14/0.93 ![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.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.14/0.93 fof(f245,plain,(
% 0.14/0.93 ![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.14/0.93 inference(NNF_transformation,[status(thm)],[f244])).
% 0.14/0.93 fof(f246,plain,(
% 0.14/0.93 ![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.14/0.93 inference(miniscoping,[status(thm)],[f245])).
% 0.14/0.93 fof(f247,plain,(
% 0.14/0.93 ![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.14/0.93 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))],[f246])).
% 0.14/0.93 fof(f248,plain,(
% 0.14/0.93 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_image(X0,X2)|~in(X3,X1)|in(ordered_pair(sK6_skl(X3,X1,X2,X0),X3),X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f247])).
% 0.14/0.93 fof(f249,plain,(
% 0.14/0.93 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_image(X0,X2)|~in(X3,X1)|in(sK6_skl(X3,X1,X2,X0),X2))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f247])).
% 0.14/0.93 fof(f250,plain,(
% 0.14/0.93 ![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.14/0.93 inference(cnf_transformation,[status(thm)],[f247])).
% 0.14/0.93 fof(f252,plain,(
% 0.14/0.93 ![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.14/0.93 inference(cnf_transformation,[status(thm)],[f247])).
% 0.14/0.93 fof(f254,plain,(
% 0.14/0.93 ![A]: (relation(A)<=>(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/0.93 fof(f255,plain,(
% 0.14/0.93 ![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.14/0.93 inference(NNF_transformation,[status(thm)],[f254])).
% 0.14/0.93 fof(f256,plain,(
% 0.14/0.93 (![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.14/0.93 inference(miniscoping,[status(thm)],[f255])).
% 0.14/0.93 fof(f257,plain,(
% 0.14/0.93 (![A]: (~relation(A)|(![B]: (~in(B,A)|B=ordered_pair(sK9_skl(B,A),sK10_skl(B,A))))))&(![A]: (relation(A)|(in(sK11_skl(A),A)&(![C,D]: ~sK11_skl(A)=ordered_pair(C,D)))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(C,sK9_skl(B,A)),skolemize(D,sK10_skl(B,A)),skolemize(B,sK11_skl(A))],[f256])).
% 0.14/0.93 fof(f258,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(X0)|~in(X1,X0)|X1=ordered_pair(sK9_skl(X1,X0),sK10_skl(X1,X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f257])).
% 0.14/0.93 fof(f261,plain,(
% 0.14/0.93 ![A,B]: ((A=empty_set|(B=set_meet(A)<=>(![C]: (in(C,B)<=>(![D]: (~in(D,A)|in(C,D)))))))&(~A=empty_set|(B=set_meet(A)<=>B=empty_set)))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.14/0.93 fof(f262,plain,(
% 0.14/0.93 ![A,B]: ((A=empty_set|((~B=set_meet(A)|(![C]: ((~in(C,B)|(![D]: (~in(D,A)|in(C,D))))&(in(C,B)|(?[D]: (in(D,A)&~in(C,D)))))))&(B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))&(~A=empty_set|((~B=set_meet(A)|B=empty_set)&(B=set_meet(A)|~B=empty_set))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f261])).
% 0.14/0.93 fof(f263,plain,(
% 0.14/0.93 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(?[D]: (in(D,A)&~in(C,D))))))))&(![B]: (B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f262])).
% 0.14/0.93 fof(f264,plain,(
% 0.14/0.93 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(in(sK12_skl(C,B,A),A)&~in(C,sK12_skl(C,B,A))))))))&(![B]: (B=set_meet(A)|((~in(sK13_skl(B,A),B)|(in(sK14_skl(B,A),A)&~in(sK13_skl(B,A),sK14_skl(B,A))))&(in(sK13_skl(B,A),B)|(![D]: (~in(D,A)|in(sK13_skl(B,A),D))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(D,sK12_skl(C,B,A)),skolemize(C,sK13_skl(B,A)),skolemize(D,sK14_skl(B,A))],[f263])).
% 0.14/0.93 fof(f271,plain,(
% 0.14/0.93 ![X0,X1]: (~X0=empty_set|~X1=set_meet(X0)|X1=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f264])).
% 0.14/0.93 fof(f280,plain,(
% 0.14/0.93 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f15])).
% 0.14/0.93 fof(f281,plain,(
% 0.14/0.93 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f280])).
% 0.14/0.93 fof(f282,plain,(
% 0.14/0.93 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK16_skl(A),A)))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(B,sK16_skl(A))],[f281])).
% 0.14/0.93 fof(f283,plain,(
% 0.14/0.93 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f282])).
% 0.14/0.93 fof(f356,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.14/0.93 fof(f357,plain,(
% 0.14/0.93 ![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)))))))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f356])).
% 0.14/0.93 fof(f358,plain,(
% 0.14/0.93 ![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)))))))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f357])).
% 0.14/0.93 fof(f359,plain,(
% 0.14/0.93 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK31_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK32_skl(B,A),B)|(![D]: ~in(ordered_pair(sK32_skl(B,A),D),A)))&(in(sK32_skl(B,A),B)|in(ordered_pair(sK32_skl(B,A),sK33_skl(B,A)),A)))))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl]),skolemize(D,sK31_skl(C,B,A)),skolemize(C,sK32_skl(B,A)),skolemize(D,sK33_skl(B,A))],[f358])).
% 0.14/0.93 fof(f361,plain,(
% 0.14/0.93 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f359])).
% 0.14/0.93 fof(f434,plain,(
% 0.14/0.93 ![A]: (~relation(A)|relation(relation_inverse(A)))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.14/0.93 fof(f435,plain,(
% 0.14/0.93 ![X0]: (~relation(X0)|relation(relation_inverse(X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f434])).
% 0.14/0.93 fof(f440,plain,(
% 0.14/0.93 ![X0]: (relation(identity_relation(X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.93 fof(f461,plain,(
% 0.14/0.93 empty(empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.93 fof(f474,plain,(
% 0.14/0.93 relation(empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.93 fof(f481,plain,(
% 0.14/0.93 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 0.14/0.93 fof(f482,plain,(
% 0.14/0.93 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f481])).
% 0.14/0.93 fof(f483,plain,(
% 0.14/0.93 ![X0]: (~empty(X0)|relation(relation_dom(X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f481])).
% 0.14/0.93 fof(f492,plain,(
% 0.14/0.93 ![A]: set_intersection2(A,A)=A),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f84])).
% 0.14/0.93 fof(f493,plain,(
% 0.14/0.93 ![X0]: (set_intersection2(X0,X0)=X0)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f492])).
% 0.14/0.93 fof(f496,plain,(
% 0.14/0.93 ![A]: (~relation(A)|relation_inverse(relation_inverse(A))=A)),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.14/0.93 fof(f497,plain,(
% 0.14/0.93 ![X0]: (~relation(X0)|relation_inverse(relation_inverse(X0))=X0)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f496])).
% 0.14/0.93 fof(f538,plain,(
% 0.14/0.93 (empty(sK50_skl)&relation(sK50_skl))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(A,sK50_skl)],[f101])).
% 0.14/0.93 fof(f539,plain,(
% 0.14/0.93 empty(sK50_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f538])).
% 0.14/0.93 fof(f540,plain,(
% 0.14/0.93 relation(sK50_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f538])).
% 0.14/0.93 fof(f545,plain,(
% 0.14/0.93 empty(sK52_skl)),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl]),skolemize(A,sK52_skl)],[f103])).
% 0.14/0.93 fof(f546,plain,(
% 0.14/0.93 empty(sK52_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f545])).
% 0.14/0.93 fof(f547,plain,(
% 0.14/0.93 (~empty(sK53_skl)&relation(sK53_skl))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl]),skolemize(A,sK53_skl)],[f104])).
% 0.14/0.93 fof(f548,plain,(
% 0.14/0.93 ~empty(sK53_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f547])).
% 0.14/0.93 fof(f549,plain,(
% 0.14/0.93 relation(sK53_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f547])).
% 0.14/0.93 fof(f550,plain,(
% 0.14/0.93 ![A]: (element(sK54_skl(A),powerset(A))&empty(sK54_skl(A)))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK54_skl]),skolemize(B,sK54_skl(A))],[f105])).
% 0.14/0.93 fof(f552,plain,(
% 0.14/0.93 ![X0]: (empty(sK54_skl(X0)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f550])).
% 0.14/0.93 fof(f609,plain,(
% 0.14/0.93 (?[A,B,C]: (relation(C)&(in(A,relation_image(C,B))<~>(?[D]: ((in(D,relation_dom(C))&in(ordered_pair(D,A),C))&in(D,B))))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f125])).
% 0.14/0.93 fof(f610,plain,(
% 0.14/0.93 ?[A,B,C]: (relation(C)&((in(A,relation_image(C,B))|(?[D]: ((in(D,relation_dom(C))&in(ordered_pair(D,A),C))&in(D,B))))&(~in(A,relation_image(C,B))|(![D]: ((~in(D,relation_dom(C))|~in(ordered_pair(D,A),C))|~in(D,B))))))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f609])).
% 0.14/0.93 fof(f611,plain,(
% 0.14/0.93 ?[C]: (relation(C)&(?[A,B]: ((in(A,relation_image(C,B))|(?[D]: ((in(D,relation_dom(C))&in(ordered_pair(D,A),C))&in(D,B))))&(~in(A,relation_image(C,B))|(![D]: ((~in(D,relation_dom(C))|~in(ordered_pair(D,A),C))|~in(D,B)))))))),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f610])).
% 0.14/0.93 fof(f612,plain,(
% 0.14/0.93 (relation(sK57_skl)&((in(sK58_skl,relation_image(sK57_skl,sK59_skl))|((in(sK60_skl,relation_dom(sK57_skl))&in(ordered_pair(sK60_skl,sK58_skl),sK57_skl))&in(sK60_skl,sK59_skl)))&(~in(sK58_skl,relation_image(sK57_skl,sK59_skl))|(![D]: ((~in(D,relation_dom(sK57_skl))|~in(ordered_pair(D,sK58_skl),sK57_skl))|~in(D,sK59_skl))))))),
% 0.14/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl,sK58_skl,sK59_skl,sK60_skl]),skolemize(C,sK57_skl),skolemize(A,sK58_skl),skolemize(B,sK59_skl),skolemize(D,sK60_skl)],[f611])).
% 0.14/0.93 fof(f613,plain,(
% 0.14/0.93 relation(sK57_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f612])).
% 0.14/0.93 fof(f614,plain,(
% 0.14/0.93 in(sK58_skl,relation_image(sK57_skl,sK59_skl))|in(sK60_skl,relation_dom(sK57_skl))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f612])).
% 0.14/0.93 fof(f615,plain,(
% 0.14/0.93 in(sK58_skl,relation_image(sK57_skl,sK59_skl))|in(ordered_pair(sK60_skl,sK58_skl),sK57_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f612])).
% 0.14/0.93 fof(f616,plain,(
% 0.14/0.93 in(sK58_skl,relation_image(sK57_skl,sK59_skl))|in(sK60_skl,sK59_skl)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f612])).
% 0.14/0.93 fof(f617,plain,(
% 0.14/0.93 ![X0]: (~in(sK58_skl,relation_image(sK57_skl,sK59_skl))|~in(X0,relation_dom(sK57_skl))|~in(ordered_pair(X0,sK58_skl),sK57_skl)|~in(X0,sK59_skl))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f612])).
% 0.14/0.93 fof(f618,plain,(
% 0.14/0.93 ![X0,X1]: (subset(set_intersection2(X0,X1),X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/0.93 fof(f621,plain,(
% 0.14/0.93 ![X0]: (set_union2(X0,empty_set)=X0)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f128])).
% 0.14/0.93 fof(f634,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(A,B)|(subset(relation_dom(A),relation_dom(B))&subset(relation_rng(A),relation_rng(B)))))))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f134])).
% 0.14/0.93 fof(f635,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(X0,X1)|subset(relation_dom(X0),relation_dom(X1)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f634])).
% 0.14/0.93 fof(f642,plain,(
% 0.14/0.93 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.93 fof(f650,plain,(
% 0.14/0.93 ![X0]: (subset(empty_set,X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f140])).
% 0.14/0.93 fof(f661,plain,(
% 0.14/0.93 ![X0,X1]: (subset(set_difference(X0,X1),X0))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f144])).
% 0.14/0.93 fof(f721,plain,(
% 0.14/0.93 ![X0]: (set_difference(empty_set,X0)=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f167])).
% 0.14/0.93 fof(f741,plain,(
% 0.14/0.93 relation_dom(empty_set)=empty_set),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f174])).
% 0.14/0.93 fof(f748,plain,(
% 0.14/0.93 ![A]: (~relation(A)|((~relation_dom(A)=empty_set&~relation_rng(A)=empty_set)|A=empty_set))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f177])).
% 0.14/0.93 fof(f749,plain,(
% 0.14/0.93 ![X0]: (~relation(X0)|~relation_dom(X0)=empty_set|X0=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f748])).
% 0.14/0.93 fof(f751,plain,(
% 0.14/0.93 ![A]: (~relation(A)|(relation_dom(A)=empty_set<=>relation_rng(A)=empty_set))),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f178])).
% 0.14/0.93 fof(f752,plain,(
% 0.14/0.93 ![A]: (~relation(A)|((~relation_dom(A)=empty_set|relation_rng(A)=empty_set)&(relation_dom(A)=empty_set|~relation_rng(A)=empty_set)))),
% 0.14/0.93 inference(NNF_transformation,[status(thm)],[f751])).
% 0.14/0.93 fof(f753,plain,(
% 0.14/0.93 ![X0]: (~relation(X0)|~relation_dom(X0)=empty_set|relation_rng(X0)=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f752])).
% 0.14/0.93 fof(f754,plain,(
% 0.14/0.93 ![X0]: (~relation(X0)|relation_dom(X0)=empty_set|~relation_rng(X0)=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f752])).
% 0.14/0.93 fof(f760,plain,(
% 0.14/0.93 ![A]: (~empty(A)|A=empty_set)),
% 0.14/0.93 inference(pre_NNF_transformation,[status(thm)],[f181])).
% 0.14/0.93 fof(f761,plain,(
% 0.14/0.93 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f760])).
% 0.14/0.93 fof(f764,plain,(
% 0.14/0.93 (![A]: relation_dom(identity_relation(A))=A)&(![A]: relation_rng(identity_relation(A))=A)),
% 0.14/0.93 inference(miniscoping,[status(thm)],[f183])).
% 0.14/0.93 fof(f765,plain,(
% 0.14/0.93 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f764])).
% 0.14/0.93 fof(f766,plain,(
% 0.14/0.93 ![X0]: (relation_rng(identity_relation(X0))=X0)),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f764])).
% 0.14/0.93 fof(f776,plain,(
% 0.14/0.93 ![X0,X1]: (subset(X0,set_union2(X0,X1)))),
% 0.14/0.93 inference(cnf_transformation,[status(thm)],[f186])).
% 0.14/0.93 fof(f827,definition,(
% 0.14/0.93 sQ0_spl <=> (in(sK58_skl,relation_image(sK57_skl,sK59_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f828,plain,(
% 0.14/0.93 in(sK58_skl,relation_image(sK57_skl,sK59_skl))|~sQ0_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f827])).
% 0.14/0.93 fof(f829,plain,(
% 0.14/0.93 ~in(sK58_skl,relation_image(sK57_skl,sK59_skl))|sQ0_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f827])).
% 0.14/0.93 fof(f830,definition,(
% 0.14/0.93 sQ1_spl <=> (in(sK60_skl,relation_dom(sK57_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f831,plain,(
% 0.14/0.93 in(sK60_skl,relation_dom(sK57_skl))|~sQ1_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f830])).
% 0.14/0.93 fof(f833,plain,(
% 0.14/0.93 sQ0_spl|sQ1_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f614,f827,f830])).
% 0.14/0.93 fof(f834,definition,(
% 0.14/0.93 sQ2_spl <=> (in(ordered_pair(sK60_skl,sK58_skl),sK57_skl))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f835,plain,(
% 0.14/0.93 in(ordered_pair(sK60_skl,sK58_skl),sK57_skl)|~sQ2_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f834])).
% 0.14/0.93 fof(f837,plain,(
% 0.14/0.93 sQ0_spl|sQ2_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f615,f827,f834])).
% 0.14/0.93 fof(f838,definition,(
% 0.14/0.93 sQ3_spl <=> (in(sK60_skl,sK59_skl))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f839,plain,(
% 0.14/0.93 in(sK60_skl,sK59_skl)|~sQ3_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f838])).
% 0.14/0.93 fof(f841,plain,(
% 0.14/0.93 sQ0_spl|sQ3_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f616,f827,f838])).
% 0.14/0.93 fof(f842,definition,(
% 0.14/0.93 ![X0]: (sQ4_spl <=> (~in(X0,relation_dom(sK57_skl))|~in(ordered_pair(X0,sK58_skl),sK57_skl)|~in(X0,sK59_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f843,plain,(
% 0.14/0.93 ![X0]: (~in(X0,relation_dom(sK57_skl))|~in(ordered_pair(X0,sK58_skl),sK57_skl)|~in(X0,sK59_skl)|~sQ4_spl)),
% 0.14/0.93 inference(component_clause,[status(thm)],[f842])).
% 0.14/0.93 fof(f845,plain,(
% 0.14/0.93 ~sQ0_spl|sQ4_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f617,f827,f842])).
% 0.14/0.93 fof(f857,plain,(
% 0.14/0.93 ![X0,X1,X2]: (~relation(X0)|~in(X1,relation_image(X0,X2))|in(ordered_pair(sK6_skl(X1,relation_image(X0,X2),X2,X0),X1),X0))),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f248])).
% 0.14/0.93 fof(f858,plain,(
% 0.14/0.93 ![X0,X1,X2]: (~relation(X0)|~in(X1,relation_image(X0,X2))|in(sK6_skl(X1,relation_image(X0,X2),X2,X0),X2))),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f249])).
% 0.14/0.93 fof(f859,plain,(
% 0.14/0.93 ![X0,X1,X2,X3]: (~relation(X0)|in(X1,relation_image(X0,X2))|~in(ordered_pair(X3,X1),X0)|~in(X3,X2))),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f250])).
% 0.14/0.93 fof(f863,plain,(
% 0.14/0.93 set_meet(empty_set)=empty_set),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f271])).
% 0.14/0.93 fof(f867,plain,(
% 0.14/0.93 ![X0]: (~in(X0,empty_set))),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f283])).
% 0.14/0.93 fof(f882,plain,(
% 0.14/0.93 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f361])).
% 0.14/0.93 fof(f929,plain,(
% 0.14/0.93 ![X0,X1,X2]: (in(X0,relation_image(sK57_skl,X1))|~in(ordered_pair(X2,X0),sK57_skl)|~in(X2,X1))),
% 0.14/0.93 inference(resolution,[status(thm)],[f859,f613])).
% 0.14/0.93 fof(f930,plain,(
% 0.14/0.93 ![X0,X1]: (in(X0,relation_dom(sK57_skl))|~in(ordered_pair(X0,X1),sK57_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f882,f613])).
% 0.14/0.93 fof(f938,plain,(
% 0.14/0.93 relation(relation_dom(sK50_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f539,f483])).
% 0.14/0.93 fof(f939,plain,(
% 0.14/0.93 empty(relation_dom(sK50_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f539,f482])).
% 0.14/0.93 fof(f943,plain,(
% 0.14/0.93 empty(relation_dom(sK52_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f546,f482])).
% 0.14/0.93 fof(f944,plain,(
% 0.14/0.93 ![X0,X1]: (in(X0,relation_dom(sK53_skl))|~in(ordered_pair(X0,X1),sK53_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f549,f882])).
% 0.14/0.93 fof(f945,plain,(
% 0.14/0.93 ![X0,X1,X2]: (in(X0,relation_image(sK53_skl,X1))|~in(ordered_pair(X2,X0),sK53_skl)|~in(X2,X1))),
% 0.14/0.93 inference(resolution,[status(thm)],[f549,f859])).
% 0.14/0.93 fof(f953,plain,(
% 0.14/0.93 ![X0]: (in(sK58_skl,relation_image(sK57_skl,X0))|~in(sK60_skl,X0)|~sQ2_spl)),
% 0.14/0.93 inference(resolution,[status(thm)],[f929,f835])).
% 0.14/0.93 fof(f954,plain,(
% 0.14/0.93 ~in(sK60_skl,sK59_skl)|~sQ2_spl|sQ0_spl),
% 0.14/0.93 inference(resolution,[status(thm)],[f953,f829])).
% 0.14/0.93 fof(f956,plain,(
% 0.14/0.93 $false|~sQ3_spl|~sQ2_spl|sQ0_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f954,f839])).
% 0.14/0.93 fof(f957,plain,(
% 0.14/0.93 ~sQ3_spl|~sQ2_spl|sQ0_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f956])).
% 0.14/0.93 fof(f958,plain,(
% 0.14/0.93 ![X0]: (~in(ordered_pair(X0,sK58_skl),sK57_skl)|~in(X0,sK59_skl)|~sQ4_spl)),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f843,f930])).
% 0.14/0.93 fof(f961,plain,(
% 0.14/0.93 relation(relation_dom(relation_dom(sK50_skl)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f939,f483])).
% 0.14/0.93 fof(f965,plain,(
% 0.14/0.93 relation(relation_dom(relation_dom(sK52_skl)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f943,f483])).
% 0.14/0.93 fof(f1008,definition,(
% 0.14/0.93 sQ13_spl <=> (empty(empty_set))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1010,plain,(
% 0.14/0.93 ~empty(empty_set)|sQ13_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1008])).
% 0.14/0.93 fof(f1011,definition,(
% 0.14/0.93 sQ14_spl <=> (relation(empty_set))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1013,plain,(
% 0.14/0.93 ~relation(empty_set)|sQ14_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1011])).
% 0.14/0.93 fof(f1020,plain,(
% 0.14/0.93 ![X0]: (relation(relation_dom(sK54_skl(X0))))),
% 0.14/0.93 inference(resolution,[status(thm)],[f552,f483])).
% 0.14/0.93 fof(f1022,plain,(
% 0.14/0.93 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_dom(empty_set),relation_dom(X0)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f650,f635])).
% 0.14/0.93 fof(f1023,definition,(
% 0.14/0.93 ![X0]: (sQ15_spl <=> (~relation(X0)|subset(relation_dom(empty_set),relation_dom(X0))))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1026,plain,(
% 0.14/0.93 ~sQ14_spl|sQ15_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1022,f1011,f1023])).
% 0.14/0.93 fof(f1027,plain,(
% 0.14/0.93 $false|sQ14_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1013,f474])).
% 0.14/0.93 fof(f1028,plain,(
% 0.14/0.93 sQ14_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1027])).
% 0.14/0.93 fof(f1042,plain,(
% 0.14/0.93 ![X0]: (~relation_dom(identity_relation(X0))=empty_set|identity_relation(X0)=empty_set)),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f440])).
% 0.14/0.93 fof(f1044,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(relation_dom(sK52_skl)))=empty_set|relation_dom(relation_dom(sK52_skl))=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f965])).
% 0.14/0.93 fof(f1045,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(relation_dom(sK50_skl)))=empty_set|relation_dom(relation_dom(sK50_skl))=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f961])).
% 0.14/0.93 fof(f1047,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(sK50_skl))=empty_set|relation_dom(sK50_skl)=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f938])).
% 0.14/0.93 fof(f1050,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|empty_set=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f474])).
% 0.14/0.93 fof(f1051,plain,(
% 0.14/0.93 ~relation_dom(sK57_skl)=empty_set|sK57_skl=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f749,f613])).
% 0.14/0.93 fof(f1053,plain,(
% 0.14/0.93 ![X0]: (~X0=empty_set|identity_relation(X0)=empty_set)),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f765,f1042])).
% 0.14/0.93 fof(f1054,plain,(
% 0.14/0.93 identity_relation(empty_set)=empty_set),
% 0.14/0.93 inference(destructive_equality_resolution,[status(thm)],[f1053])).
% 0.14/0.93 fof(f1055,definition,(
% 0.14/0.93 sQ16_spl <=> (relation_dom(relation_dom(relation_dom(sK52_skl)))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1057,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(relation_dom(sK52_skl)))=empty_set|sQ16_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1055])).
% 0.14/0.93 fof(f1058,definition,(
% 0.14/0.93 sQ17_spl <=> (relation_dom(relation_dom(sK52_skl))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1061,plain,(
% 0.14/0.93 ~sQ16_spl|sQ17_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1044,f1055,f1058])).
% 0.14/0.93 fof(f1062,definition,(
% 0.14/0.93 sQ18_spl <=> (relation_dom(relation_dom(relation_dom(sK50_skl)))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1064,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(relation_dom(sK50_skl)))=empty_set|sQ18_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1062])).
% 0.14/0.93 fof(f1065,definition,(
% 0.14/0.93 sQ19_spl <=> (relation_dom(relation_dom(sK50_skl))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1068,plain,(
% 0.14/0.93 ~sQ18_spl|sQ19_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1045,f1062,f1065])).
% 0.14/0.93 fof(f1069,definition,(
% 0.14/0.93 sQ20_spl <=> (relation_dom(sK52_skl)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1070,plain,(
% 0.14/0.93 relation_dom(sK52_skl)=empty_set|~sQ20_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1069])).
% 0.14/0.93 fof(f1071,plain,(
% 0.14/0.93 ~relation_dom(sK52_skl)=empty_set|sQ20_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1069])).
% 0.14/0.93 fof(f1073,definition,(
% 0.14/0.93 sQ21_spl <=> (relation_dom(sK50_skl)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1076,plain,(
% 0.14/0.93 ~sQ19_spl|sQ21_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1047,f1065,f1073])).
% 0.14/0.93 fof(f1084,definition,(
% 0.14/0.93 sQ24_spl <=> (sK50_skl=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1085,plain,(
% 0.14/0.93 sK50_skl=empty_set|~sQ24_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1084])).
% 0.14/0.93 fof(f1086,plain,(
% 0.14/0.93 ~sK50_skl=empty_set|sQ24_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1084])).
% 0.14/0.93 fof(f1088,definition,(
% 0.14/0.93 sQ25_spl <=> (relation_dom(empty_set)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1090,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|sQ25_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1088])).
% 0.14/0.93 fof(f1091,definition,(
% 0.14/0.93 sQ26_spl <=> (empty_set=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1094,plain,(
% 0.14/0.93 ~sQ25_spl|sQ26_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1050,f1088,f1091])).
% 0.14/0.93 fof(f1095,definition,(
% 0.14/0.93 sQ27_spl <=> (relation_dom(sK57_skl)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1097,plain,(
% 0.14/0.93 ~relation_dom(sK57_skl)=empty_set|sQ27_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1095])).
% 0.14/0.93 fof(f1098,definition,(
% 0.14/0.93 sQ28_spl <=> (sK57_skl=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1099,plain,(
% 0.14/0.93 sK57_skl=empty_set|~sQ28_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1098])).
% 0.14/0.93 fof(f1101,plain,(
% 0.14/0.93 ~sQ27_spl|sQ28_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1051,f1095,f1098])).
% 0.14/0.93 fof(f1102,plain,(
% 0.14/0.93 ~empty_set=empty_set|sQ25_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1090])).
% 0.14/0.93 fof(f1103,plain,(
% 0.14/0.93 $false|sQ25_spl),
% 0.14/0.93 inference(trivial_equality_resolution,[status(thm)],[f1102])).
% 0.14/0.93 fof(f1104,plain,(
% 0.14/0.93 sQ25_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1103])).
% 0.14/0.93 fof(f1119,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(relation_dom(empty_set)))=empty_set|~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1085,f1064])).
% 0.14/0.93 fof(f1120,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(empty_set))=empty_set|~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1119])).
% 0.14/0.93 fof(f1121,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1120])).
% 0.14/0.93 fof(f1122,plain,(
% 0.14/0.93 ~empty_set=empty_set|~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1121])).
% 0.14/0.93 fof(f1123,plain,(
% 0.14/0.93 $false|~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(trivial_equality_resolution,[status(thm)],[f1122])).
% 0.14/0.93 fof(f1124,plain,(
% 0.14/0.93 ~sQ24_spl|sQ18_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1123])).
% 0.14/0.93 fof(f1135,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(empty_set))=empty_set|~sQ20_spl|sQ16_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1070,f1057])).
% 0.14/0.93 fof(f1136,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|~sQ20_spl|sQ16_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1135])).
% 0.14/0.93 fof(f1137,plain,(
% 0.14/0.93 ~empty_set=empty_set|~sQ20_spl|sQ16_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1136])).
% 0.14/0.93 fof(f1138,plain,(
% 0.14/0.93 $false|~sQ20_spl|sQ16_spl),
% 0.14/0.93 inference(trivial_equality_resolution,[status(thm)],[f1137])).
% 0.14/0.93 fof(f1139,plain,(
% 0.14/0.93 ~sQ20_spl|sQ16_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1138])).
% 0.14/0.93 fof(f1154,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(sK50_skl))=empty_set|relation_rng(relation_dom(sK50_skl))=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f753,f938])).
% 0.14/0.93 fof(f1155,plain,(
% 0.14/0.93 ![X0]: (~relation_dom(relation_dom(sK54_skl(X0)))=empty_set|relation_rng(relation_dom(sK54_skl(X0)))=empty_set)),
% 0.14/0.93 inference(resolution,[status(thm)],[f753,f1020])).
% 0.14/0.93 fof(f1157,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|relation_rng(empty_set)=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f753,f474])).
% 0.14/0.93 fof(f1161,definition,(
% 0.14/0.93 sQ29_spl <=> (relation_rng(relation_dom(sK50_skl))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1164,plain,(
% 0.14/0.93 ~sQ19_spl|sQ29_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1154,f1065,f1161])).
% 0.14/0.93 fof(f1169,definition,(
% 0.14/0.93 sQ31_spl <=> (relation_rng(empty_set)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1172,plain,(
% 0.14/0.93 ~sQ25_spl|sQ31_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1157,f1088,f1169])).
% 0.14/0.93 fof(f1177,plain,(
% 0.14/0.93 ~relation_dom(sK50_skl)=empty_set|relation_rng(sK50_skl)=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f540,f753])).
% 0.14/0.93 fof(f1181,definition,(
% 0.14/0.93 sQ33_spl <=> (relation_rng(sK50_skl)=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1184,plain,(
% 0.14/0.93 ~sQ21_spl|sQ33_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1177,f1073,f1181])).
% 0.14/0.93 fof(f1191,plain,(
% 0.14/0.93 ![X0]: (set_union2(empty_set,X0)=X0)),
% 0.14/0.93 inference(paramodulation,[status(thm)],[f207,f621])).
% 0.14/0.93 fof(f1201,plain,(
% 0.14/0.93 sK50_skl=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f761,f539])).
% 0.14/0.93 fof(f1202,plain,(
% 0.14/0.93 relation_dom(sK52_skl)=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f761,f943])).
% 0.14/0.93 fof(f1204,plain,(
% 0.14/0.93 ![X0]: (sK54_skl(X0)=empty_set)),
% 0.14/0.93 inference(resolution,[status(thm)],[f761,f552])).
% 0.14/0.93 fof(f1207,plain,(
% 0.14/0.93 $false|sQ24_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1201,f1086])).
% 0.14/0.93 fof(f1208,plain,(
% 0.14/0.93 sQ24_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1207])).
% 0.14/0.93 fof(f1209,plain,(
% 0.14/0.93 $false|sQ20_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1202,f1071])).
% 0.14/0.93 fof(f1210,plain,(
% 0.14/0.93 sQ20_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1209])).
% 0.14/0.93 fof(f1224,plain,(
% 0.14/0.93 ![X0]: (~relation_dom(relation_dom(sK54_skl(X0)))=empty_set|relation_rng(relation_dom(empty_set))=empty_set)),
% 0.14/0.93 inference(backward_demodulation,[status(thm)],[f1204,f1155])).
% 0.14/0.93 fof(f1324,definition,(
% 0.14/0.93 ![X0]: (sQ34_spl <=> (~relation_dom(relation_dom(sK54_skl(X0)))=empty_set))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1325,plain,(
% 0.14/0.93 ![X0]: (~relation_dom(relation_dom(sK54_skl(X0)))=empty_set|~sQ34_spl)),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1324])).
% 0.14/0.93 fof(f1327,definition,(
% 0.14/0.93 sQ35_spl <=> (relation_rng(relation_dom(empty_set))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1330,plain,(
% 0.14/0.93 sQ34_spl|sQ35_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1224,f1324,f1327])).
% 0.14/0.93 fof(f1371,plain,(
% 0.14/0.93 ~relation_dom(relation_dom(empty_set))=empty_set|~sQ34_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1204,f1325])).
% 0.14/0.93 fof(f1372,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|~sQ34_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1371])).
% 0.14/0.93 fof(f1373,plain,(
% 0.14/0.93 ~empty_set=empty_set|~sQ34_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1372])).
% 0.14/0.93 fof(f1374,plain,(
% 0.14/0.93 $false|~sQ34_spl),
% 0.14/0.93 inference(trivial_equality_resolution,[status(thm)],[f1373])).
% 0.14/0.93 fof(f1375,plain,(
% 0.14/0.93 ~sQ34_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1374])).
% 0.14/0.93 fof(f1377,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(sK57_skl)|sK57_skl=identity_relation(X0)|in(sK0_skl(X0,sK57_skl),X0)|in(sK1_skl(X0,sK57_skl),relation_image(sK57_skl,X1))|~in(sK0_skl(X0,sK57_skl),X1))),
% 0.14/0.93 inference(resolution,[status(thm)],[f217,f929])).
% 0.14/0.93 fof(f1378,plain,(
% 0.14/0.93 ![X0]: (~relation(sK57_skl)|sK57_skl=identity_relation(X0)|in(sK0_skl(X0,sK57_skl),X0)|in(sK0_skl(X0,sK57_skl),relation_dom(sK57_skl)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f217,f930])).
% 0.14/0.93 fof(f1379,plain,(
% 0.14/0.93 ![X0]: (~relation(empty_set)|empty_set=identity_relation(X0)|in(sK0_skl(X0,empty_set),X0))),
% 0.14/0.93 inference(resolution,[status(thm)],[f217,f867])).
% 0.14/0.93 fof(f1381,definition,(
% 0.14/0.93 sQ36_spl <=> (relation(sK57_skl))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1383,plain,(
% 0.14/0.93 ~relation(sK57_skl)|sQ36_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1381])).
% 0.14/0.93 fof(f1384,definition,(
% 0.14/0.93 ![X0,X1]: (sQ37_spl <=> (sK57_skl=identity_relation(X0)|in(sK0_skl(X0,sK57_skl),X0)|in(sK1_skl(X0,sK57_skl),relation_image(sK57_skl,X1))|~in(sK0_skl(X0,sK57_skl),X1)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1387,plain,(
% 0.14/0.93 ~sQ36_spl|sQ37_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1377,f1381,f1384])).
% 0.14/0.93 fof(f1388,definition,(
% 0.14/0.93 ![X0]: (sQ38_spl <=> (sK57_skl=identity_relation(X0)|in(sK0_skl(X0,sK57_skl),X0)|in(sK0_skl(X0,sK57_skl),relation_dom(sK57_skl))))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1389,plain,(
% 0.14/0.93 ![X0]: (sK57_skl=identity_relation(X0)|in(sK0_skl(X0,sK57_skl),X0)|in(sK0_skl(X0,sK57_skl),relation_dom(sK57_skl))|~sQ38_spl)),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1388])).
% 0.14/0.93 fof(f1391,plain,(
% 0.14/0.93 ~sQ36_spl|sQ38_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1378,f1381,f1388])).
% 0.14/0.93 fof(f1392,definition,(
% 0.14/0.93 ![X0]: (sQ39_spl <=> (empty_set=identity_relation(X0)|in(sK0_skl(X0,empty_set),X0)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1395,plain,(
% 0.14/0.93 ~sQ14_spl|sQ39_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1379,f1011,f1392])).
% 0.14/0.93 fof(f1396,plain,(
% 0.14/0.93 $false|sQ36_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1383,f613])).
% 0.14/0.93 fof(f1397,plain,(
% 0.14/0.93 sQ36_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1396])).
% 0.14/0.93 fof(f1398,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(sK57_skl)|sK57_skl=identity_relation(X0)|sK0_skl(X0,sK57_skl)=sK1_skl(X0,sK57_skl)|in(sK1_skl(X0,sK57_skl),relation_image(sK57_skl,X1))|~in(sK0_skl(X0,sK57_skl),X1))),
% 0.14/0.93 inference(resolution,[status(thm)],[f218,f929])).
% 0.14/0.93 fof(f1399,plain,(
% 0.14/0.93 ![X0]: (~relation(sK57_skl)|sK57_skl=identity_relation(X0)|sK0_skl(X0,sK57_skl)=sK1_skl(X0,sK57_skl)|in(sK0_skl(X0,sK57_skl),relation_dom(sK57_skl)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f218,f930])).
% 0.14/0.93 fof(f1400,plain,(
% 0.14/0.93 ![X0]: (~relation(empty_set)|empty_set=identity_relation(X0)|sK0_skl(X0,empty_set)=sK1_skl(X0,empty_set))),
% 0.14/0.93 inference(resolution,[status(thm)],[f218,f867])).
% 0.14/0.93 fof(f1402,definition,(
% 0.14/0.93 ![X0,X1]: (sQ40_spl <=> (sK57_skl=identity_relation(X0)|sK0_skl(X0,sK57_skl)=sK1_skl(X0,sK57_skl)|in(sK1_skl(X0,sK57_skl),relation_image(sK57_skl,X1))|~in(sK0_skl(X0,sK57_skl),X1)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1405,plain,(
% 0.14/0.93 ~sQ36_spl|sQ40_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1398,f1381,f1402])).
% 0.14/0.93 fof(f1406,definition,(
% 0.14/0.93 ![X0]: (sQ41_spl <=> (sK57_skl=identity_relation(X0)|sK0_skl(X0,sK57_skl)=sK1_skl(X0,sK57_skl)|in(sK0_skl(X0,sK57_skl),relation_dom(sK57_skl))))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1409,plain,(
% 0.14/0.93 ~sQ36_spl|sQ41_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1399,f1381,f1406])).
% 0.14/0.93 fof(f1410,definition,(
% 0.14/0.93 ![X0]: (sQ42_spl <=> (empty_set=identity_relation(X0)|sK0_skl(X0,empty_set)=sK1_skl(X0,empty_set)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1413,plain,(
% 0.14/0.93 ~sQ14_spl|sQ42_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1400,f1011,f1410])).
% 0.14/0.93 fof(f1416,plain,(
% 0.14/0.93 sK57_skl=identity_relation(empty_set)|in(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl))|~sQ38_spl),
% 0.14/0.93 inference(resolution,[status(thm)],[f1389,f867])).
% 0.14/0.93 fof(f1417,plain,(
% 0.14/0.93 sK57_skl=identity_relation(relation_dom(sK57_skl))|~in(relation_dom(sK57_skl),sK0_skl(relation_dom(sK57_skl),sK57_skl))|~sQ38_spl),
% 0.14/0.93 inference(resolution,[status(thm)],[f1389,f201])).
% 0.14/0.93 fof(f1420,plain,(
% 0.14/0.93 sK57_skl=identity_relation(relation_dom(sK57_skl))|in(sK0_skl(relation_dom(sK57_skl),sK57_skl),relation_dom(sK57_skl))|~sQ38_spl),
% 0.14/0.93 inference(factoring,[status(thm)],[f1389])).
% 0.14/0.93 fof(f1421,definition,(
% 0.14/0.93 sQ43_spl <=> (sK57_skl=identity_relation(empty_set))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1422,plain,(
% 0.14/0.93 sK57_skl=identity_relation(empty_set)|~sQ43_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1421])).
% 0.14/0.93 fof(f1424,definition,(
% 0.14/0.93 sQ44_spl <=> (in(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1425,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl))|~sQ44_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1424])).
% 0.14/0.93 fof(f1427,plain,(
% 0.14/0.93 sQ43_spl|sQ44_spl|~sQ38_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1416,f1421,f1424,f1388])).
% 0.14/0.93 fof(f1428,definition,(
% 0.14/0.93 sQ45_spl <=> (sK57_skl=identity_relation(relation_dom(sK57_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1431,definition,(
% 0.14/0.93 sQ46_spl <=> (in(relation_dom(sK57_skl),sK0_skl(relation_dom(sK57_skl),sK57_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1434,plain,(
% 0.14/0.93 sQ45_spl|~sQ46_spl|~sQ38_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1417,f1428,f1431,f1388])).
% 0.14/0.93 fof(f1435,definition,(
% 0.14/0.93 sQ47_spl <=> (in(sK0_skl(relation_dom(sK57_skl),sK57_skl),relation_dom(sK57_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1438,plain,(
% 0.14/0.93 sQ45_spl|sQ47_spl|~sQ38_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1420,f1428,f1435,f1388])).
% 0.14/0.93 fof(f1440,plain,(
% 0.14/0.93 ~relation_dom(empty_set)=empty_set|~sQ43_spl|sQ27_spl),
% 0.14/0.93 inference(backward_demodulation,[status(thm)],[f1453,f1097])).
% 0.14/0.93 fof(f1453,plain,(
% 0.14/0.93 sK57_skl=empty_set|~sQ43_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1054,f1422])).
% 0.14/0.93 fof(f1458,plain,(
% 0.14/0.93 ~sQ25_spl|~sQ43_spl|sQ27_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1440,f1088,f1421,f1095])).
% 0.14/0.93 fof(f1487,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,sK57_skl),relation_dom(empty_set))|~sQ28_spl|~sQ44_spl),
% 0.14/0.93 inference(backward_demodulation,[status(thm)],[f1099,f1425])).
% 0.14/0.93 fof(f1496,plain,(
% 0.14/0.93 in(sK58_skl,relation_image(empty_set,sK59_skl))|~sQ28_spl|~sQ0_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1099,f828])).
% 0.14/0.93 fof(f1535,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,empty_set),relation_dom(empty_set))|~sQ28_spl|~sQ44_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1099,f1487])).
% 0.14/0.93 fof(f1536,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,empty_set),empty_set)|~sQ28_spl|~sQ44_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f741,f1535])).
% 0.14/0.93 fof(f1537,plain,(
% 0.14/0.93 $false|~sQ28_spl|~sQ44_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1536,f867])).
% 0.14/0.93 fof(f1538,plain,(
% 0.14/0.93 ~sQ28_spl|~sQ44_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1537])).
% 0.14/0.93 fof(f1545,plain,(
% 0.14/0.93 ![X0]: (in(sK0_skl(X0,sK53_skl),relation_dom(sK53_skl))|~relation(sK53_skl)|sK53_skl=identity_relation(X0)|sK0_skl(X0,sK53_skl)=sK1_skl(X0,sK53_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f944,f218])).
% 0.14/0.93 fof(f1546,plain,(
% 0.14/0.93 ![X0]: (in(sK0_skl(X0,sK53_skl),relation_dom(sK53_skl))|~relation(sK53_skl)|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0))),
% 0.14/0.93 inference(resolution,[status(thm)],[f944,f217])).
% 0.14/0.93 fof(f1547,definition,(
% 0.14/0.93 ![X0]: (sQ48_spl <=> (in(sK0_skl(X0,sK53_skl),relation_dom(sK53_skl))|sK53_skl=identity_relation(X0)|sK0_skl(X0,sK53_skl)=sK1_skl(X0,sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1550,definition,(
% 0.14/0.93 sQ49_spl <=> (relation(sK53_skl))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1552,plain,(
% 0.14/0.93 ~relation(sK53_skl)|sQ49_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1550])).
% 0.14/0.93 fof(f1553,plain,(
% 0.14/0.93 sQ48_spl|~sQ49_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1545,f1547,f1550])).
% 0.14/0.93 fof(f1554,definition,(
% 0.14/0.93 ![X0]: (sQ50_spl <=> (in(sK0_skl(X0,sK53_skl),relation_dom(sK53_skl))|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1555,plain,(
% 0.14/0.93 ![X0]: (in(sK0_skl(X0,sK53_skl),relation_dom(sK53_skl))|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0)|~sQ50_spl)),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1554])).
% 0.14/0.93 fof(f1557,plain,(
% 0.14/0.93 sQ50_spl|~sQ49_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1546,f1554,f1550])).
% 0.14/0.93 fof(f1558,plain,(
% 0.14/0.93 $false|sQ49_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1552,f549])).
% 0.14/0.93 fof(f1559,plain,(
% 0.14/0.93 sQ49_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1558])).
% 0.14/0.93 fof(f1560,plain,(
% 0.14/0.93 ![X0,X1]: (in(sK1_skl(X0,sK53_skl),relation_image(sK53_skl,X1))|~in(sK0_skl(X0,sK53_skl),X1)|~relation(sK53_skl)|sK53_skl=identity_relation(X0)|sK0_skl(X0,sK53_skl)=sK1_skl(X0,sK53_skl))),
% 0.14/0.93 inference(resolution,[status(thm)],[f945,f218])).
% 0.14/0.93 fof(f1561,plain,(
% 0.14/0.93 ![X0,X1]: (in(sK1_skl(X0,sK53_skl),relation_image(sK53_skl,X1))|~in(sK0_skl(X0,sK53_skl),X1)|~relation(sK53_skl)|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0))),
% 0.14/0.93 inference(resolution,[status(thm)],[f945,f217])).
% 0.14/0.93 fof(f1562,definition,(
% 0.14/0.93 ![X0,X1]: (sQ51_spl <=> (in(sK1_skl(X0,sK53_skl),relation_image(sK53_skl,X1))|~in(sK0_skl(X0,sK53_skl),X1)|sK53_skl=identity_relation(X0)|sK0_skl(X0,sK53_skl)=sK1_skl(X0,sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1565,plain,(
% 0.14/0.93 sQ51_spl|~sQ49_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1560,f1562,f1550])).
% 0.14/0.93 fof(f1566,definition,(
% 0.14/0.93 ![X0,X1]: (sQ52_spl <=> (in(sK1_skl(X0,sK53_skl),relation_image(sK53_skl,X1))|~in(sK0_skl(X0,sK53_skl),X1)|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1567,plain,(
% 0.14/0.93 ![X0,X1]: (in(sK1_skl(X0,sK53_skl),relation_image(sK53_skl,X1))|~in(sK0_skl(X0,sK53_skl),X1)|sK53_skl=identity_relation(X0)|in(sK0_skl(X0,sK53_skl),X0)|~sQ52_spl)),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1566])).
% 0.14/0.93 fof(f1569,plain,(
% 0.14/0.93 sQ52_spl|~sQ49_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1561,f1566,f1550])).
% 0.14/0.93 fof(f1576,plain,(
% 0.14/0.93 sK53_skl=identity_relation(relation_dom(sK53_skl))|~in(relation_dom(sK53_skl),sK0_skl(relation_dom(sK53_skl),sK53_skl))|~sQ50_spl),
% 0.14/0.93 inference(resolution,[status(thm)],[f1555,f201])).
% 0.14/0.93 fof(f1578,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl))|sK53_skl=identity_relation(empty_set)|~sQ50_spl),
% 0.14/0.93 inference(resolution,[status(thm)],[f1555,f867])).
% 0.14/0.93 fof(f1580,plain,(
% 0.14/0.93 in(sK0_skl(relation_dom(sK53_skl),sK53_skl),relation_dom(sK53_skl))|sK53_skl=identity_relation(relation_dom(sK53_skl))|~sQ50_spl),
% 0.14/0.93 inference(factoring,[status(thm)],[f1555])).
% 0.14/0.93 fof(f1581,definition,(
% 0.14/0.93 sQ53_spl <=> (sK53_skl=identity_relation(relation_dom(sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1584,definition,(
% 0.14/0.93 sQ54_spl <=> (in(relation_dom(sK53_skl),sK0_skl(relation_dom(sK53_skl),sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1587,plain,(
% 0.14/0.93 sQ53_spl|~sQ54_spl|~sQ50_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1576,f1581,f1584,f1554])).
% 0.14/0.93 fof(f1588,definition,(
% 0.14/0.93 sQ55_spl <=> (in(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1589,plain,(
% 0.14/0.93 in(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl))|~sQ55_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1588])).
% 0.14/0.93 fof(f1591,definition,(
% 0.14/0.93 sQ56_spl <=> (sK53_skl=identity_relation(empty_set))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1592,plain,(
% 0.14/0.93 sK53_skl=identity_relation(empty_set)|~sQ56_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1591])).
% 0.14/0.93 fof(f1594,plain,(
% 0.14/0.93 sQ55_spl|sQ56_spl|~sQ50_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1578,f1588,f1591,f1554])).
% 0.14/0.93 fof(f1595,definition,(
% 0.14/0.93 sQ57_spl <=> (in(sK0_skl(relation_dom(sK53_skl),sK53_skl),relation_dom(sK53_skl)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1598,plain,(
% 0.14/0.93 sQ57_spl|sQ53_spl|~sQ50_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1580,f1595,f1581,f1554])).
% 0.14/0.93 fof(f1607,plain,(
% 0.14/0.93 ~relation(identity_relation(empty_set))|relation_dom(identity_relation(empty_set))=empty_set),
% 0.14/0.93 inference(resolution,[status(thm)],[f766,f754])).
% 0.14/0.93 fof(f1611,definition,(
% 0.14/0.93 sQ58_spl <=> (relation(identity_relation(empty_set)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1613,plain,(
% 0.14/0.93 ~relation(identity_relation(empty_set))|sQ58_spl),
% 0.14/0.93 inference(component_clause,[status(thm)],[f1611])).
% 0.14/0.93 fof(f1614,definition,(
% 0.14/0.93 sQ59_spl <=> (relation_dom(identity_relation(empty_set))=empty_set)),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1617,plain,(
% 0.14/0.93 ~sQ58_spl|sQ59_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1607,f1611,f1614])).
% 0.14/0.93 fof(f1618,plain,(
% 0.14/0.93 ~relation(empty_set)|sQ58_spl),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f1054,f1613])).
% 0.14/0.93 fof(f1619,plain,(
% 0.14/0.93 $false|sQ58_spl),
% 0.14/0.93 inference(forward_subsumption_resolution,[status(thm)],[f1618,f474])).
% 0.14/0.93 fof(f1620,plain,(
% 0.14/0.93 sQ58_spl),
% 0.14/0.93 inference(contradiction_clause,[status(thm)],[f1619])).
% 0.14/0.93 fof(f1638,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(set_intersection2(X0,X1))|~relation(X0)|subset(relation_dom(set_intersection2(X0,X1)),relation_dom(X0)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f618,f635])).
% 0.14/0.93 fof(f1639,plain,(
% 0.14/0.93 ![X0,X1]: (subset(set_intersection2(X0,X1),X1))),
% 0.14/0.93 inference(paramodulation,[status(thm)],[f208,f618])).
% 0.14/0.93 fof(f1642,plain,(
% 0.14/0.93 ![X0]: (set_intersection2(empty_set,X0)=empty_set)),
% 0.14/0.93 inference(paramodulation,[status(thm)],[f208,f642])).
% 0.14/0.93 fof(f1650,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(set_difference(X0,X1))|~relation(X0)|subset(relation_dom(set_difference(X0,X1)),relation_dom(X0)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f661,f635])).
% 0.14/0.93 fof(f1675,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(set_intersection2(identity_relation(X0),X1))|subset(relation_dom(set_intersection2(identity_relation(X0),X1)),relation_dom(identity_relation(X0))))),
% 0.14/0.93 inference(resolution,[status(thm)],[f1638,f440])).
% 0.14/0.93 fof(f1676,plain,(
% 0.14/0.93 ![X0]: (~relation(set_intersection2(sK53_skl,X0))|subset(relation_dom(set_intersection2(sK53_skl,X0)),relation_dom(sK53_skl)))),
% 0.14/0.93 inference(resolution,[status(thm)],[f1638,f549])).
% 0.14/0.93 fof(f1679,plain,(
% 0.14/0.93 ![X0,X1]: (~relation(set_intersection2(identity_relation(X0),X1))|subset(relation_dom(set_intersection2(identity_relation(X0),X1)),X0))),
% 0.14/0.93 inference(forward_demodulation,[status(thm)],[f765,f1675])).
% 0.14/0.93 fof(f1685,plain,(
% 0.14/0.93 ![X0]: (~relation(empty_set)|subset(relation_dom(set_intersection2(identity_relation(X0),empty_set)),X0))),
% 0.14/0.93 inference(paramodulation,[status(thm)],[f642,f1679])).
% 0.14/0.93 fof(f1691,definition,(
% 0.14/0.93 ![X0]: (sQ60_spl <=> (subset(relation_dom(set_intersection2(identity_relation(X0),empty_set)),X0)))),
% 0.14/0.93 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.93 fof(f1694,plain,(
% 0.14/0.93 ~sQ14_spl|sQ60_spl),
% 0.14/0.93 inference(split_clause,[status(thm)],[f1685,f1011,f1691])).
% 0.14/0.93 fof(f1744,plain,(
% 0.14/0.93 ![X0]: (~relation(empty_set)|~relation(empty_set)|subset(relation_dom(set_difference(empty_set,X0)),relation_dom(empty_set)))),
% 0.14/0.93 inference(paramodulation,[status(thm)],[f721,f1650])).
% 0.14/0.93 fof(f1746,definition,(
% 0.14/0.93 ![X0]: (sQ61_spl <=> (subset(relation_dom(set_difference(empty_set,X0)),relation_dom(empty_set))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1749,plain,(
% 0.14/0.94 ~sQ14_spl|sQ61_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1744,f1011,f1746])).
% 0.14/0.94 fof(f1756,plain,(
% 0.14/0.94 ~relation(empty_set)|subset(relation_dom(set_intersection2(sK53_skl,empty_set)),relation_dom(sK53_skl))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f642,f1676])).
% 0.14/0.94 fof(f1759,plain,(
% 0.14/0.94 ~relation(sK53_skl)|subset(relation_dom(set_intersection2(sK53_skl,sK53_skl)),relation_dom(sK53_skl))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f493,f1676])).
% 0.14/0.94 fof(f1760,definition,(
% 0.14/0.94 sQ62_spl <=> (subset(relation_dom(set_intersection2(sK53_skl,empty_set)),relation_dom(sK53_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1763,plain,(
% 0.14/0.94 ~sQ14_spl|sQ62_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1756,f1011,f1760])).
% 0.14/0.94 fof(f1764,definition,(
% 0.14/0.94 sQ63_spl <=> (subset(relation_dom(set_intersection2(sK53_skl,sK53_skl)),relation_dom(sK53_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1767,plain,(
% 0.14/0.94 ~sQ49_spl|sQ63_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1759,f1550,f1764])).
% 0.14/0.94 fof(f1785,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|~relation(set_union2(X0,X1))|subset(relation_dom(X0),relation_dom(set_union2(X0,X1))))),
% 0.14/0.94 inference(resolution,[status(thm)],[f776,f635])).
% 0.14/0.94 fof(f1788,plain,(
% 0.14/0.94 ![X0,X1]: (subset(X0,set_union2(X1,X0)))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f207,f776])).
% 0.14/0.94 fof(f1792,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(set_intersection2(X0,X1))|~relation(X1)|subset(relation_dom(set_intersection2(X0,X1)),relation_dom(X1)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1639,f635])).
% 0.14/0.94 fof(f1812,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|~relation(set_union2(X1,X0))|subset(relation_dom(X0),relation_dom(set_union2(X1,X0))))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1788,f635])).
% 0.14/0.94 fof(f1823,plain,(
% 0.14/0.94 relation(relation_inverse(sK53_skl))),
% 0.14/0.94 inference(resolution,[status(thm)],[f435,f549])).
% 0.14/0.94 fof(f1824,plain,(
% 0.14/0.94 relation(relation_inverse(empty_set))),
% 0.14/0.94 inference(resolution,[status(thm)],[f435,f474])).
% 0.14/0.94 fof(f1832,plain,(
% 0.14/0.94 ![X0,X1]: (in(X0,relation_dom(relation_inverse(sK53_skl)))|~in(ordered_pair(X0,X1),relation_inverse(sK53_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1823,f882])).
% 0.14/0.94 fof(f1845,plain,(
% 0.14/0.94 relation(relation_inverse(relation_inverse(empty_set)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1824,f435])).
% 0.14/0.94 fof(f1851,plain,(
% 0.14/0.94 ![X0,X1]: (in(X0,relation_dom(relation_inverse(empty_set)))|~in(ordered_pair(X0,X1),relation_inverse(empty_set)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1824,f882])).
% 0.14/0.94 fof(f1880,plain,(
% 0.14/0.94 ![X0]: (in(sK0_skl(X0,relation_inverse(sK53_skl)),relation_dom(relation_inverse(sK53_skl)))|~relation(relation_inverse(sK53_skl))|relation_inverse(sK53_skl)=identity_relation(X0)|sK0_skl(X0,relation_inverse(sK53_skl))=sK1_skl(X0,relation_inverse(sK53_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1832,f218])).
% 0.14/0.94 fof(f1881,plain,(
% 0.14/0.94 ![X0]: (in(sK0_skl(X0,relation_inverse(sK53_skl)),relation_dom(relation_inverse(sK53_skl)))|~relation(relation_inverse(sK53_skl))|relation_inverse(sK53_skl)=identity_relation(X0)|in(sK0_skl(X0,relation_inverse(sK53_skl)),X0))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1832,f217])).
% 0.14/0.94 fof(f1882,definition,(
% 0.14/0.94 ![X0]: (sQ70_spl <=> (in(sK0_skl(X0,relation_inverse(sK53_skl)),relation_dom(relation_inverse(sK53_skl)))|relation_inverse(sK53_skl)=identity_relation(X0)|sK0_skl(X0,relation_inverse(sK53_skl))=sK1_skl(X0,relation_inverse(sK53_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1885,definition,(
% 0.14/0.94 sQ71_spl <=> (relation(relation_inverse(sK53_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1887,plain,(
% 0.14/0.94 ~relation(relation_inverse(sK53_skl))|sQ71_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f1885])).
% 0.14/0.94 fof(f1888,plain,(
% 0.14/0.94 sQ70_spl|~sQ71_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1880,f1882,f1885])).
% 0.14/0.94 fof(f1889,definition,(
% 0.14/0.94 ![X0]: (sQ72_spl <=> (in(sK0_skl(X0,relation_inverse(sK53_skl)),relation_dom(relation_inverse(sK53_skl)))|relation_inverse(sK53_skl)=identity_relation(X0)|in(sK0_skl(X0,relation_inverse(sK53_skl)),X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1892,plain,(
% 0.14/0.94 sQ72_spl|~sQ71_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1881,f1889,f1885])).
% 0.14/0.94 fof(f1893,plain,(
% 0.14/0.94 $false|sQ71_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f1887,f1823])).
% 0.14/0.94 fof(f1894,plain,(
% 0.14/0.94 sQ71_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f1893])).
% 0.14/0.94 fof(f1895,plain,(
% 0.14/0.94 ![X0]: (in(sK0_skl(X0,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set)))|~relation(relation_inverse(empty_set))|relation_inverse(empty_set)=identity_relation(X0)|sK0_skl(X0,relation_inverse(empty_set))=sK1_skl(X0,relation_inverse(empty_set)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1851,f218])).
% 0.14/0.94 fof(f1896,plain,(
% 0.14/0.94 ![X0]: (in(sK0_skl(X0,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set)))|~relation(relation_inverse(empty_set))|relation_inverse(empty_set)=identity_relation(X0)|in(sK0_skl(X0,relation_inverse(empty_set)),X0))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1851,f217])).
% 0.14/0.94 fof(f1897,definition,(
% 0.14/0.94 ![X0]: (sQ73_spl <=> (in(sK0_skl(X0,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set)))|relation_inverse(empty_set)=identity_relation(X0)|sK0_skl(X0,relation_inverse(empty_set))=sK1_skl(X0,relation_inverse(empty_set))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1900,definition,(
% 0.14/0.94 sQ74_spl <=> (relation(relation_inverse(empty_set)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1902,plain,(
% 0.14/0.94 ~relation(relation_inverse(empty_set))|sQ74_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f1900])).
% 0.14/0.94 fof(f1903,plain,(
% 0.14/0.94 sQ73_spl|~sQ74_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1895,f1897,f1900])).
% 0.14/0.94 fof(f1904,definition,(
% 0.14/0.94 ![X0]: (sQ75_spl <=> (in(sK0_skl(X0,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set)))|relation_inverse(empty_set)=identity_relation(X0)|in(sK0_skl(X0,relation_inverse(empty_set)),X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1907,plain,(
% 0.14/0.94 sQ75_spl|~sQ74_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1896,f1904,f1900])).
% 0.14/0.94 fof(f1908,plain,(
% 0.14/0.94 $false|sQ74_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f1902,f1824])).
% 0.14/0.94 fof(f1909,plain,(
% 0.14/0.94 sQ74_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f1908])).
% 0.14/0.94 fof(f1910,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|subset(relation_dom(X0),relation_dom(set_union2(X0,X1)))|~empty(set_union2(X0,X1)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f1785,f205])).
% 0.14/0.94 fof(f1911,plain,(
% 0.14/0.94 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_dom(empty_set),relation_dom(set_union2(empty_set,X0))))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f1191,f1785])).
% 0.14/0.94 fof(f1916,definition,(
% 0.14/0.94 ![X0]: (sQ76_spl <=> (~relation(X0)|subset(relation_dom(empty_set),relation_dom(set_union2(empty_set,X0)))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1919,plain,(
% 0.14/0.94 ~sQ14_spl|sQ76_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1911,f1011,f1916])).
% 0.14/0.94 fof(f1941,plain,(
% 0.14/0.94 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_dom(set_intersection2(empty_set,X0)),relation_dom(X0)))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f1642,f1792])).
% 0.14/0.94 fof(f1942,plain,(
% 0.14/0.94 ![X0]: (~relation(empty_set)|~relation(empty_set)|subset(relation_dom(set_intersection2(X0,empty_set)),relation_dom(empty_set)))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f642,f1792])).
% 0.14/0.94 fof(f1946,definition,(
% 0.14/0.94 ![X0]: (sQ78_spl <=> (~relation(X0)|subset(relation_dom(set_intersection2(empty_set,X0)),relation_dom(X0))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1949,plain,(
% 0.14/0.94 ~sQ14_spl|sQ78_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1941,f1011,f1946])).
% 0.14/0.94 fof(f1950,definition,(
% 0.14/0.94 ![X0]: (sQ79_spl <=> (subset(relation_dom(set_intersection2(X0,empty_set)),relation_dom(empty_set))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1953,plain,(
% 0.14/0.94 ~sQ14_spl|sQ79_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1942,f1011,f1950])).
% 0.14/0.94 fof(f1963,plain,(
% 0.14/0.94 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_dom(empty_set),relation_dom(set_union2(X0,empty_set))))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f621,f1812])).
% 0.14/0.94 fof(f1969,definition,(
% 0.14/0.94 ![X0]: (sQ80_spl <=> (~relation(X0)|subset(relation_dom(empty_set),relation_dom(set_union2(X0,empty_set)))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1972,plain,(
% 0.14/0.94 ~sQ14_spl|sQ80_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1963,f1011,f1969])).
% 0.14/0.94 fof(f1977,plain,(
% 0.14/0.94 ![X0]: (~relation(empty_set)|subset(relation_dom(empty_set),relation_dom(set_union2(empty_set,X0)))|~empty(X0))),
% 0.14/0.94 inference(paramodulation,[status(thm)],[f1191,f1910])).
% 0.14/0.94 fof(f1982,definition,(
% 0.14/0.94 ![X0]: (sQ81_spl <=> (subset(relation_dom(empty_set),relation_dom(set_union2(empty_set,X0)))|~empty(X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f1985,plain,(
% 0.14/0.94 ~sQ14_spl|sQ81_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f1977,f1011,f1982])).
% 0.14/0.94 fof(f2002,plain,(
% 0.14/0.94 in(sK1_skl(empty_set,sK53_skl),relation_image(sK53_skl,relation_dom(sK53_skl)))|sK53_skl=identity_relation(empty_set)|in(sK0_skl(empty_set,sK53_skl),empty_set)|~sQ52_spl|~sQ55_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f1567,f1589])).
% 0.14/0.94 fof(f2017,definition,(
% 0.14/0.94 sQ83_spl <=> (in(sK1_skl(empty_set,sK53_skl),relation_image(sK53_skl,relation_dom(sK53_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2020,definition,(
% 0.14/0.94 sQ84_spl <=> (in(sK0_skl(empty_set,sK53_skl),empty_set))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2023,plain,(
% 0.14/0.94 sQ83_spl|sQ56_spl|sQ84_spl|~sQ52_spl|~sQ55_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2002,f2017,f1591,f2020,f1566,f1588])).
% 0.14/0.94 fof(f2041,plain,(
% 0.14/0.94 ~empty(empty_set)|~sQ56_spl),
% 0.14/0.94 inference(backward_demodulation,[status(thm)],[f2068,f548])).
% 0.14/0.94 fof(f2068,plain,(
% 0.14/0.94 sK53_skl=empty_set|~sQ56_spl),
% 0.14/0.94 inference(forward_demodulation,[status(thm)],[f1054,f1592])).
% 0.14/0.94 fof(f2125,plain,(
% 0.14/0.94 $false|~sQ56_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f2041,f461])).
% 0.14/0.94 fof(f2126,plain,(
% 0.14/0.94 ~sQ56_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2125])).
% 0.14/0.94 fof(f2179,plain,(
% 0.14/0.94 ~relation(empty_set)|in(ordered_pair(sK6_skl(sK58_skl,relation_image(empty_set,sK59_skl),sK59_skl,empty_set),sK58_skl),empty_set)|~sQ28_spl|~sQ0_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f857,f1496])).
% 0.14/0.94 fof(f2182,definition,(
% 0.14/0.94 sQ85_spl <=> (in(ordered_pair(sK6_skl(sK58_skl,relation_image(empty_set,sK59_skl),sK59_skl,empty_set),sK58_skl),empty_set))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2183,plain,(
% 0.14/0.94 in(ordered_pair(sK6_skl(sK58_skl,relation_image(empty_set,sK59_skl),sK59_skl,empty_set),sK58_skl),empty_set)|~sQ85_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2182])).
% 0.14/0.94 fof(f2185,plain,(
% 0.14/0.94 ~sQ14_spl|sQ85_spl|~sQ28_spl|~sQ0_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2179,f1011,f2182,f1098,f827])).
% 0.14/0.94 fof(f2186,plain,(
% 0.14/0.94 $false|~sQ85_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f2183,f867])).
% 0.14/0.94 fof(f2187,plain,(
% 0.14/0.94 ~sQ85_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2186])).
% 0.14/0.94 fof(f2192,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|sK57_skl=relation_rng_restriction(X1,X0)|in(ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0)),sK57_skl)|in(sK5_skl(X1,sK57_skl,X0),X1))),
% 0.14/0.94 inference(resolution,[status(thm)],[f613,f242])).
% 0.14/0.94 fof(f2193,plain,(
% 0.14/0.94 relation(relation_inverse(sK57_skl))),
% 0.14/0.94 inference(resolution,[status(thm)],[f613,f435])).
% 0.14/0.94 fof(f2196,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|sK57_skl=relation_dom_restriction(X0,X1)|in(ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0)),sK57_skl)|in(sK2_skl(X1,sK57_skl,X0),X1))),
% 0.14/0.94 inference(resolution,[status(thm)],[f613,f232])).
% 0.14/0.94 fof(f2205,plain,(
% 0.14/0.94 relation(relation_inverse(relation_inverse(sK57_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f2193,f435])).
% 0.14/0.94 fof(f2209,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(sK57_skl))=empty_set|relation_rng(relation_inverse(sK57_skl))=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f2193,f753])).
% 0.14/0.94 fof(f2210,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(sK57_skl))=empty_set|relation_inverse(sK57_skl)=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f2193,f749])).
% 0.14/0.94 fof(f2213,definition,(
% 0.14/0.94 sQ86_spl <=> (relation_dom(relation_inverse(sK57_skl))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2216,definition,(
% 0.14/0.94 sQ87_spl <=> (relation_rng(relation_inverse(sK57_skl))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2219,plain,(
% 0.14/0.94 ~sQ86_spl|sQ87_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2209,f2213,f2216])).
% 0.14/0.94 fof(f2220,definition,(
% 0.14/0.94 sQ88_spl <=> (relation_inverse(sK57_skl)=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2221,plain,(
% 0.14/0.94 relation_inverse(sK57_skl)=empty_set|~sQ88_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2220])).
% 0.14/0.94 fof(f2223,plain,(
% 0.14/0.94 ~sQ86_spl|sQ88_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2210,f2213,f2220])).
% 0.14/0.94 fof(f2256,plain,(
% 0.14/0.94 relation(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))),
% 0.14/0.94 inference(resolution,[status(thm)],[f2205,f435])).
% 0.14/0.94 fof(f2277,plain,(
% 0.14/0.94 ~relation(sK57_skl)|in(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl)|~sQ0_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f828,f858])).
% 0.14/0.94 fof(f2278,plain,(
% 0.14/0.94 ~relation(sK57_skl)|in(ordered_pair(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK58_skl),sK57_skl)|~sQ0_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f828,f857])).
% 0.14/0.94 fof(f2281,definition,(
% 0.14/0.94 sQ92_spl <=> (in(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2282,plain,(
% 0.14/0.94 in(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl)|~sQ92_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2281])).
% 0.14/0.94 fof(f2284,plain,(
% 0.14/0.94 ~sQ36_spl|sQ92_spl|~sQ0_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2277,f1381,f2281,f827])).
% 0.14/0.94 fof(f2285,definition,(
% 0.14/0.94 sQ93_spl <=> (in(ordered_pair(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK58_skl),sK57_skl))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2286,plain,(
% 0.14/0.94 in(ordered_pair(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK58_skl),sK57_skl)|~sQ93_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2285])).
% 0.14/0.94 fof(f2288,plain,(
% 0.14/0.94 ~sQ36_spl|sQ93_spl|~sQ0_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2278,f1381,f2285,f827])).
% 0.14/0.94 fof(f2318,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(relation_inverse(empty_set)))=empty_set|relation_rng(relation_inverse(relation_inverse(empty_set)))=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f1845,f753])).
% 0.14/0.94 fof(f2319,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(relation_inverse(empty_set)))=empty_set|relation_inverse(relation_inverse(empty_set))=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f1845,f749])).
% 0.14/0.94 fof(f2322,definition,(
% 0.14/0.94 sQ94_spl <=> (relation_dom(relation_inverse(relation_inverse(empty_set)))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2324,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(relation_inverse(empty_set)))=empty_set|sQ94_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2322])).
% 0.14/0.94 fof(f2325,definition,(
% 0.14/0.94 sQ95_spl <=> (relation_rng(relation_inverse(relation_inverse(empty_set)))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2328,plain,(
% 0.14/0.94 ~sQ94_spl|sQ95_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2318,f2322,f2325])).
% 0.14/0.94 fof(f2329,definition,(
% 0.14/0.94 sQ96_spl <=> (relation_inverse(relation_inverse(empty_set))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2332,plain,(
% 0.14/0.94 ~sQ94_spl|sQ96_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2319,f2322,f2329])).
% 0.14/0.94 fof(f2354,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(sK53_skl)|X0=relation_image(sK53_skl,X1)|in(sK7_skl(X0,X1,sK53_skl),X0)|in(sK8_skl(X0,X1,sK53_skl),relation_dom(sK53_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f252,f944])).
% 0.14/0.94 fof(f2355,plain,(
% 0.14/0.94 ![X0,X1,X2]: (~relation(sK53_skl)|X0=relation_image(sK53_skl,X1)|in(sK7_skl(X0,X1,sK53_skl),X0)|in(sK7_skl(X0,X1,sK53_skl),relation_image(sK53_skl,X2))|~in(sK8_skl(X0,X1,sK53_skl),X2))),
% 0.14/0.94 inference(resolution,[status(thm)],[f252,f945])).
% 0.14/0.94 fof(f2356,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(relation_inverse(empty_set))|X0=relation_image(relation_inverse(empty_set),X1)|in(sK7_skl(X0,X1,relation_inverse(empty_set)),X0)|in(sK8_skl(X0,X1,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set))))),
% 0.14/0.94 inference(resolution,[status(thm)],[f252,f1851])).
% 0.14/0.94 fof(f2361,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(empty_set)|X0=relation_image(empty_set,X1)|in(sK7_skl(X0,X1,empty_set),X0))),
% 0.14/0.94 inference(resolution,[status(thm)],[f252,f867])).
% 0.14/0.94 fof(f2364,definition,(
% 0.14/0.94 ![X0,X1]: (sQ100_spl <=> (X0=relation_image(sK53_skl,X1)|in(sK7_skl(X0,X1,sK53_skl),X0)|in(sK8_skl(X0,X1,sK53_skl),relation_dom(sK53_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2367,plain,(
% 0.14/0.94 ~sQ49_spl|sQ100_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2354,f1550,f2364])).
% 0.14/0.94 fof(f2368,definition,(
% 0.14/0.94 ![X0,X1,X2]: (sQ101_spl <=> (X0=relation_image(sK53_skl,X1)|in(sK7_skl(X0,X1,sK53_skl),X0)|in(sK7_skl(X0,X1,sK53_skl),relation_image(sK53_skl,X2))|~in(sK8_skl(X0,X1,sK53_skl),X2)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2371,plain,(
% 0.14/0.94 ~sQ49_spl|sQ101_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2355,f1550,f2368])).
% 0.14/0.94 fof(f2372,definition,(
% 0.14/0.94 ![X0,X1]: (sQ102_spl <=> (X0=relation_image(relation_inverse(empty_set),X1)|in(sK7_skl(X0,X1,relation_inverse(empty_set)),X0)|in(sK8_skl(X0,X1,relation_inverse(empty_set)),relation_dom(relation_inverse(empty_set)))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2375,plain,(
% 0.14/0.94 ~sQ74_spl|sQ102_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2356,f1900,f2372])).
% 0.14/0.94 fof(f2377,definition,(
% 0.14/0.94 ![X0,X1]: (sQ103_spl <=> (X0=relation_image(empty_set,X1)|in(sK7_skl(X0,X1,empty_set),X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2380,plain,(
% 0.14/0.94 ~sQ14_spl|sQ103_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2361,f1011,f2377])).
% 0.14/0.94 fof(f2393,plain,(
% 0.14/0.94 ~relation(relation_dom(sK57_skl))|sK60_skl=ordered_pair(sK9_skl(sK60_skl,relation_dom(sK57_skl)),sK10_skl(sK60_skl,relation_dom(sK57_skl)))|~sQ1_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f258,f831])).
% 0.14/0.94 fof(f2403,definition,(
% 0.14/0.94 sQ104_spl <=> (relation(relation_dom(sK57_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2406,definition,(
% 0.14/0.94 sQ105_spl <=> (sK60_skl=ordered_pair(sK9_skl(sK60_skl,relation_dom(sK57_skl)),sK10_skl(sK60_skl,relation_dom(sK57_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2409,plain,(
% 0.14/0.94 ~sQ104_spl|sQ105_spl|~sQ1_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2393,f2403,f2406,f830])).
% 0.14/0.94 fof(f2420,plain,(
% 0.14/0.94 $false|sQ13_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f1010,f461])).
% 0.14/0.94 fof(f2421,plain,(
% 0.14/0.94 sQ13_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2420])).
% 0.14/0.94 fof(f2430,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set|relation_rng(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f2256,f753])).
% 0.14/0.94 fof(f2434,definition,(
% 0.14/0.94 sQ108_spl <=> (relation_dom(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2436,plain,(
% 0.14/0.94 ~relation_dom(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set|sQ108_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2434])).
% 0.14/0.94 fof(f2437,definition,(
% 0.14/0.94 sQ109_spl <=> (relation_rng(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2438,plain,(
% 0.14/0.94 relation_rng(relation_inverse(relation_inverse(relation_inverse(sK57_skl))))=empty_set|~sQ109_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2437])).
% 0.14/0.94 fof(f2440,plain,(
% 0.14/0.94 ~sQ108_spl|sQ109_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2430,f2434,f2437])).
% 0.14/0.94 fof(f2441,definition,(
% 0.14/0.94 sQ110_spl <=> (relation_inverse(relation_inverse(relation_inverse(sK57_skl)))=empty_set)),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2442,plain,(
% 0.14/0.94 relation_inverse(relation_inverse(relation_inverse(sK57_skl)))=empty_set|~sQ110_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2441])).
% 0.14/0.94 fof(f2443,plain,(
% 0.14/0.94 ~relation_inverse(relation_inverse(relation_inverse(sK57_skl)))=empty_set|sQ110_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2441])).
% 0.14/0.94 fof(f2446,plain,(
% 0.14/0.94 ~relation_dom(empty_set)=empty_set|~sQ110_spl|sQ108_spl),
% 0.14/0.94 inference(backward_demodulation,[status(thm)],[f2442,f2436])).
% 0.14/0.94 fof(f2457,plain,(
% 0.14/0.94 ~sQ25_spl|~sQ110_spl|sQ108_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2446,f1088,f2441,f2434])).
% 0.14/0.94 fof(f2488,plain,(
% 0.14/0.94 ![X0,X1]: (in(sK8_skl(X0,X1,sK57_skl),relation_dom(sK57_skl))|~relation(sK57_skl)|X0=relation_image(sK57_skl,X1)|in(sK7_skl(X0,X1,sK57_skl),X0))),
% 0.14/0.94 inference(resolution,[status(thm)],[f930,f252])).
% 0.14/0.94 fof(f2491,definition,(
% 0.14/0.94 ![X0,X1]: (sQ111_spl <=> (in(sK8_skl(X0,X1,sK57_skl),relation_dom(sK57_skl))|X0=relation_image(sK57_skl,X1)|in(sK7_skl(X0,X1,sK57_skl),X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2494,plain,(
% 0.14/0.94 sQ111_spl|~sQ36_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2488,f2491,f1381])).
% 0.14/0.94 fof(f2497,plain,(
% 0.14/0.94 ~relation(relation_dom(sK53_skl))|sK0_skl(empty_set,sK53_skl)=ordered_pair(sK9_skl(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl)),sK10_skl(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl)))|~sQ55_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f1589,f258])).
% 0.14/0.94 fof(f2500,definition,(
% 0.14/0.94 sQ112_spl <=> (relation(relation_dom(sK53_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2503,definition,(
% 0.14/0.94 sQ113_spl <=> (sK0_skl(empty_set,sK53_skl)=ordered_pair(sK9_skl(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl)),sK10_skl(sK0_skl(empty_set,sK53_skl),relation_dom(sK53_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2506,plain,(
% 0.14/0.94 ~sQ112_spl|sQ113_spl|~sQ55_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2497,f2500,f2503,f1588])).
% 0.14/0.94 fof(f2508,plain,(
% 0.14/0.94 ![X0,X1,X2]: (in(sK7_skl(X0,X1,sK57_skl),relation_image(sK57_skl,X2))|~in(sK8_skl(X0,X1,sK57_skl),X2)|~relation(sK57_skl)|X0=relation_image(sK57_skl,X1)|in(sK7_skl(X0,X1,sK57_skl),X0))),
% 0.14/0.94 inference(resolution,[status(thm)],[f929,f252])).
% 0.14/0.94 fof(f2511,definition,(
% 0.14/0.94 ![X0,X1,X2]: (sQ114_spl <=> (in(sK7_skl(X0,X1,sK57_skl),relation_image(sK57_skl,X2))|~in(sK8_skl(X0,X1,sK57_skl),X2)|X0=relation_image(sK57_skl,X1)|in(sK7_skl(X0,X1,sK57_skl),X0)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2514,plain,(
% 0.14/0.94 sQ114_spl|~sQ36_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2508,f2511,f1381])).
% 0.14/0.94 fof(f2589,plain,(
% 0.14/0.94 relation_inverse(relation_inverse(sK57_skl))=sK57_skl),
% 0.14/0.94 inference(resolution,[status(thm)],[f497,f613])).
% 0.14/0.94 fof(f2599,plain,(
% 0.14/0.94 relation_inverse(relation_inverse(empty_set))=empty_set),
% 0.14/0.94 inference(resolution,[status(thm)],[f497,f474])).
% 0.14/0.94 fof(f2747,plain,(
% 0.14/0.94 ~relation_dom(empty_set)=empty_set|sQ94_spl),
% 0.14/0.94 inference(backward_demodulation,[status(thm)],[f2599,f2324])).
% 0.14/0.94 fof(f2784,plain,(
% 0.14/0.94 relation_rng(relation_inverse(sK57_skl))=empty_set|~sQ109_spl),
% 0.14/0.94 inference(forward_demodulation,[status(thm)],[f2589,f2438])).
% 0.14/0.94 fof(f2785,plain,(
% 0.14/0.94 ~relation_inverse(sK57_skl)=empty_set|sQ110_spl),
% 0.14/0.94 inference(forward_demodulation,[status(thm)],[f2589,f2443])).
% 0.14/0.94 fof(f2821,plain,(
% 0.14/0.94 ~sQ25_spl|sQ94_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2747,f1088,f2322])).
% 0.14/0.94 fof(f2876,definition,(
% 0.14/0.94 ![X0]: (sQ117_spl <=> (in(X0,set_meet(empty_set))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2877,plain,(
% 0.14/0.94 ![X0]: (in(X0,set_meet(empty_set))|~sQ117_spl)),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2876])).
% 0.14/0.94 fof(f2886,plain,(
% 0.14/0.94 ![X0]: (in(X0,empty_set)|~sQ117_spl)),
% 0.14/0.94 inference(forward_demodulation,[status(thm)],[f863,f2877])).
% 0.14/0.94 fof(f2887,plain,(
% 0.14/0.94 $false|~sQ117_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f2886,f867])).
% 0.14/0.94 fof(f2888,plain,(
% 0.14/0.94 ~sQ117_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2887])).
% 0.14/0.94 fof(f2889,plain,(
% 0.14/0.94 ~relation(relation_inverse(sK57_skl))|relation_dom(relation_inverse(sK57_skl))=empty_set|~sQ109_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f2784,f754])).
% 0.14/0.94 fof(f2891,definition,(
% 0.14/0.94 sQ119_spl <=> (relation(relation_inverse(sK57_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f2893,plain,(
% 0.14/0.94 ~relation(relation_inverse(sK57_skl))|sQ119_spl),
% 0.14/0.94 inference(component_clause,[status(thm)],[f2891])).
% 0.14/0.94 fof(f2894,plain,(
% 0.14/0.94 ~sQ119_spl|sQ86_spl|~sQ109_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f2889,f2891,f2213,f2437])).
% 0.14/0.94 fof(f2896,plain,(
% 0.14/0.94 $false|sQ119_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f2893,f2193])).
% 0.14/0.94 fof(f2897,plain,(
% 0.14/0.94 sQ119_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2896])).
% 0.14/0.94 fof(f2898,plain,(
% 0.14/0.94 $false|sQ110_spl|~sQ88_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f2221,f2785])).
% 0.14/0.94 fof(f2899,plain,(
% 0.14/0.94 sQ110_spl|~sQ88_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f2898])).
% 0.14/0.94 fof(f3113,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|sK57_skl=relation_rng_restriction(X1,X0)|in(sK5_skl(X1,sK57_skl,X0),X1)|~relation(sK57_skl)|ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0))=ordered_pair(sK9_skl(ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0)),sK57_skl),sK10_skl(ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0)),sK57_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f2192,f258])).
% 0.14/0.94 fof(f3116,definition,(
% 0.14/0.94 ![X0,X1]: (sQ120_spl <=> (~relation(X0)|sK57_skl=relation_rng_restriction(X1,X0)|in(sK5_skl(X1,sK57_skl,X0),X1)|ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0))=ordered_pair(sK9_skl(ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0)),sK57_skl),sK10_skl(ordered_pair(sK4_skl(X1,sK57_skl,X0),sK5_skl(X1,sK57_skl,X0)),sK57_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f3119,plain,(
% 0.14/0.94 sQ120_spl|~sQ36_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f3113,f3116,f1381])).
% 0.14/0.94 fof(f3121,plain,(
% 0.14/0.94 ~relation(relation_dom(sK57_skl))|sK0_skl(empty_set,sK57_skl)=ordered_pair(sK9_skl(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl)),sK10_skl(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl)))|~sQ44_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f1425,f258])).
% 0.14/0.94 fof(f3124,definition,(
% 0.14/0.94 sQ121_spl <=> (sK0_skl(empty_set,sK57_skl)=ordered_pair(sK9_skl(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl)),sK10_skl(sK0_skl(empty_set,sK57_skl),relation_dom(sK57_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f3127,plain,(
% 0.14/0.94 ~sQ104_spl|sQ121_spl|~sQ44_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f3121,f2403,f3124,f1424])).
% 0.14/0.94 fof(f3143,plain,(
% 0.14/0.94 ![X0,X1]: (~relation(X0)|sK57_skl=relation_dom_restriction(X0,X1)|in(sK2_skl(X1,sK57_skl,X0),X1)|~relation(sK57_skl)|ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0))=ordered_pair(sK9_skl(ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0)),sK57_skl),sK10_skl(ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0)),sK57_skl)))),
% 0.14/0.94 inference(resolution,[status(thm)],[f2196,f258])).
% 0.14/0.94 fof(f3146,definition,(
% 0.14/0.94 ![X0,X1]: (sQ122_spl <=> (~relation(X0)|sK57_skl=relation_dom_restriction(X0,X1)|in(sK2_skl(X1,sK57_skl,X0),X1)|ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0))=ordered_pair(sK9_skl(ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0)),sK57_skl),sK10_skl(ordered_pair(sK2_skl(X1,sK57_skl,X0),sK3_skl(X1,sK57_skl,X0)),sK57_skl))))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f3149,plain,(
% 0.14/0.94 sQ122_spl|~sQ36_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f3143,f3146,f1381])).
% 0.14/0.94 fof(f3359,plain,(
% 0.14/0.94 ~relation(sK59_skl)|sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl)=ordered_pair(sK9_skl(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl),sK10_skl(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl))|~sQ92_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f2282,f258])).
% 0.14/0.94 fof(f3362,definition,(
% 0.14/0.94 sQ124_spl <=> (relation(sK59_skl))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f3365,definition,(
% 0.14/0.94 sQ125_spl <=> (sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl)=ordered_pair(sK9_skl(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl),sK10_skl(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl)))),
% 0.14/0.94 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.14/0.94 fof(f3368,plain,(
% 0.14/0.94 ~sQ124_spl|sQ125_spl|~sQ92_spl),
% 0.14/0.94 inference(split_clause,[status(thm)],[f3359,f3362,f3365,f2281])).
% 0.14/0.94 fof(f3370,plain,(
% 0.14/0.94 ~in(sK6_skl(sK58_skl,relation_image(sK57_skl,sK59_skl),sK59_skl,sK57_skl),sK59_skl)|~sQ93_spl|~sQ4_spl),
% 0.14/0.94 inference(resolution,[status(thm)],[f2286,f958])).
% 0.14/0.94 fof(f3376,plain,(
% 0.14/0.94 $false|~sQ92_spl|~sQ93_spl|~sQ4_spl),
% 0.14/0.94 inference(forward_subsumption_resolution,[status(thm)],[f3370,f2282])).
% 0.14/0.94 fof(f3377,plain,(
% 0.14/0.94 ~sQ92_spl|~sQ93_spl|~sQ4_spl),
% 0.14/0.94 inference(contradiction_clause,[status(thm)],[f3376])).
% 0.14/0.94 fof(f3378,plain,(
% 0.14/0.94 $false),
% 0.14/0.94 inference(sat_refutation,[status(thm)],[f833,f837,f841,f845,f957,f1026,f1028,f1061,f1068,f1076,f1094,f1101,f1104,f1124,f1139,f1164,f1172,f1184,f1208,f1210,f1330,f1375,f1387,f1391,f1395,f1397,f1405,f1409,f1413,f1427,f1434,f1438,f1458,f1538,f1553,f1557,f1559,f1565,f1569,f1587,f1594,f1598,f1617,f1620,f1694,f1749,f1763,f1767,f1888,f1892,f1894,f1903,f1907,f1909,f1919,f1949,f1953,f1972,f1985,f2023,f2126,f2185,f2187,f2219,f2223,f2284,f2288,f2328,f2332,f2367,f2371,f2375,f2380,f2409,f2421,f2440,f2457,f2494,f2506,f2514,f2821,f2888,f2894,f2897,f2899,f3119,f3127,f3149,f3368,f3377])).
% 0.14/0.94 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.96 % Elapsed time: 0.367286 seconds
% 0.14/0.96 % CPU time: 2.636651 seconds
% 0.14/0.96 % Total memory used: 150.237 MB
% 0.14/0.96 % Net memory used: 145.426 MB
%------------------------------------------------------------------------------