%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU009+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:34 PM UTC 2026
% Result : Theorem 0.12s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU009+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:46:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.45 fof(f1,axiom,(
% 0.12/0.45 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f2,axiom,(
% 0.12/0.45 (! [A] :( empty(A)=> function(A) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f4,axiom,(
% 0.12/0.45 (! [A,B] :( ( relation(A)& relation(B) )=> relation(relation_composition(A,B)) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f5,axiom,(
% 0.12/0.45 (! [A] : relation(identity_relation(A)) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f6,axiom,(
% 0.12/0.45 (! [A] :(? [B] : element(B,A) ))),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f7,axiom,(
% 0.12/0.45 (! [A,B] :( ( empty(A)& relation(B) )=> ( empty(relation_composition(B,A))& relation(relation_composition(B,A)) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f8,axiom,(
% 0.12/0.45 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f9,axiom,(
% 0.12/0.45 (! [A,B] :( ( relation(A)& function(A)& relation(B)& function(B) )=> ( relation(relation_composition(A,B))& function(relation_composition(A,B)) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f10,axiom,(
% 0.12/0.45 (! [A] : ~ empty(powerset(A)) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f12,axiom,(
% 0.12/0.45 (! [A] :( relation(identity_relation(A))& function(identity_relation(A)) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f14,axiom,(
% 0.12/0.45 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_dom(A)) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f15,axiom,(
% 0.12/0.45 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f16,axiom,(
% 0.12/0.45 (! [A,B] :( ( empty(A)& relation(B) )=> ( empty(relation_composition(A,B))& relation(relation_composition(A,B)) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f17,axiom,(
% 0.12/0.45 (? [A] :( relation(A)& function(A) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f19,axiom,(
% 0.12/0.45 (! [A] :( ~ empty(A)=> (? [B] :( element(B,powerset(A))& ~ empty(B) ) )) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f20,axiom,(
% 0.12/0.45 (? [A] : empty(A) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f21,axiom,(
% 0.12/0.45 (? [A] :( ~ empty(A)& relation(A) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f22,axiom,(
% 0.12/0.45 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f24,axiom,(
% 0.12/0.45 (? [A] :( relation(A)& relation_empty_yielding(A) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f27,axiom,(
% 0.12/0.45 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( in(A,relation_dom(relation_composition(C,B)))<=> ( in(A,relation_dom(C))& in(apply(C,A),relation_dom(B)) ) ) ) )) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f28,axiom,(
% 0.12/0.45 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f29,axiom,(
% 0.12/0.45 (! [A,B] :( ( relation(B)& function(B) )=> ( B = identity_relation(A)<=> ( relation_dom(B) = A& (! [C] :( in(C,A)=> apply(B,C) = C ) )) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f30,axiom,(
% 0.12/0.45 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f31,conjecture,(
% 0.12/0.45 (! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,relation_dom(relation_composition(C,identity_relation(A))))<=> ( in(B,relation_dom(C))& in(apply(C,B),A) ) ) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f32,negated_conjecture,(
% 0.12/0.45 ~((! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,relation_dom(relation_composition(C,identity_relation(A))))<=> ( in(B,relation_dom(C))& in(apply(C,B),A) ) ) ) ))),
% 0.12/0.45 inference(negated_conjecture,[status(cth)],[f31])).
% 0.12/0.45 fof(f34,axiom,(
% 0.12/0.45 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f35,axiom,(
% 0.12/0.45 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f36,axiom,(
% 0.12/0.45 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 0.12/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.45 fof(f38,plain,(
% 0.12/0.45 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.12/0.45 fof(f39,plain,(
% 0.12/0.45 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f38])).
% 0.12/0.45 fof(f40,plain,(
% 0.12/0.45 ![A]: (~empty(A)|function(A))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.45 fof(f41,plain,(
% 0.12/0.45 ![X0]: (~empty(X0)|function(X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f40])).
% 0.12/0.45 fof(f44,plain,(
% 0.12/0.45 ![A,B]: ((~relation(A)|~relation(B))|relation(relation_composition(A,B)))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.12/0.45 fof(f45,plain,(
% 0.12/0.45 ![X0,X1]: (~relation(X0)|~relation(X1)|relation(relation_composition(X0,X1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.45 fof(f46,plain,(
% 0.12/0.45 ![X0]: (relation(identity_relation(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.45 fof(f47,plain,(
% 0.12/0.45 ![A]: element(sK0_skl(A),A)),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f6])).
% 0.12/0.45 fof(f48,plain,(
% 0.12/0.45 ![X0]: (element(sK0_skl(X0),X0))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/0.45 fof(f49,plain,(
% 0.12/0.45 ![A,B]: ((~empty(A)|~relation(B))|(empty(relation_composition(B,A))&relation(relation_composition(B,A))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.45 fof(f50,plain,(
% 0.12/0.45 ![X0,X1]: (~empty(X0)|~relation(X1)|empty(relation_composition(X1,X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.45 fof(f52,plain,(
% 0.12/0.45 empty(empty_set)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.45 fof(f53,plain,(
% 0.12/0.45 relation(empty_set)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.45 fof(f55,plain,(
% 0.12/0.45 ![A,B]: ((((~relation(A)|~function(A))|~relation(B))|~function(B))|(relation(relation_composition(A,B))&function(relation_composition(A,B))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.12/0.45 fof(f57,plain,(
% 0.12/0.45 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|function(relation_composition(X0,X1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f55])).
% 0.12/0.45 fof(f58,plain,(
% 0.12/0.45 ![X0]: (~empty(powerset(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.45 fof(f60,plain,(
% 0.12/0.45 (![A]: relation(identity_relation(A)))&(![A]: function(identity_relation(A)))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f12])).
% 0.12/0.45 fof(f62,plain,(
% 0.12/0.45 ![X0]: (function(identity_relation(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f60])).
% 0.12/0.45 fof(f65,plain,(
% 0.12/0.45 ![A]: ((empty(A)|~relation(A))|~empty(relation_dom(A)))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.12/0.45 fof(f66,plain,(
% 0.12/0.45 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_dom(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f65])).
% 0.12/0.45 fof(f67,plain,(
% 0.12/0.45 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.12/0.45 fof(f68,plain,(
% 0.12/0.45 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/0.45 fof(f69,plain,(
% 0.12/0.45 ![X0]: (~empty(X0)|relation(relation_dom(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/0.45 fof(f70,plain,(
% 0.12/0.45 ![A,B]: ((~empty(A)|~relation(B))|(empty(relation_composition(A,B))&relation(relation_composition(A,B))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.45 fof(f71,plain,(
% 0.12/0.45 ![X0,X1]: (~empty(X0)|~relation(X1)|empty(relation_composition(X0,X1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/0.45 fof(f73,plain,(
% 0.12/0.45 (relation(sK1_skl)&function(sK1_skl))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f17])).
% 0.12/0.45 fof(f74,plain,(
% 0.12/0.45 relation(sK1_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/0.45 fof(f75,plain,(
% 0.12/0.45 function(sK1_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/0.45 fof(f79,plain,(
% 0.12/0.45 ![A]: (empty(A)|(?[B]: (element(B,powerset(A))&~empty(B))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.45 fof(f80,plain,(
% 0.12/0.45 ![A]: (empty(A)|(element(sK3_skl(A),powerset(A))&~empty(sK3_skl(A))))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f79])).
% 0.12/0.45 fof(f81,plain,(
% 0.12/0.45 ![X0]: (empty(X0)|element(sK3_skl(X0),powerset(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.12/0.45 fof(f83,plain,(
% 0.12/0.45 empty(sK4_skl)),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f20])).
% 0.12/0.45 fof(f84,plain,(
% 0.12/0.45 empty(sK4_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f83])).
% 0.12/0.45 fof(f85,plain,(
% 0.12/0.45 (~empty(sK5_skl)&relation(sK5_skl))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f21])).
% 0.12/0.45 fof(f87,plain,(
% 0.12/0.45 relation(sK5_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f85])).
% 0.12/0.45 fof(f88,plain,(
% 0.12/0.45 ![A]: (element(sK6_skl(A),powerset(A))&empty(sK6_skl(A)))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f22])).
% 0.12/0.45 fof(f89,plain,(
% 0.12/0.45 ![X0]: (element(sK6_skl(X0),powerset(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f88])).
% 0.12/0.45 fof(f90,plain,(
% 0.12/0.45 ![X0]: (empty(sK6_skl(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f88])).
% 0.12/0.45 fof(f93,plain,(
% 0.12/0.45 (relation(sK8_skl)&relation_empty_yielding(sK8_skl))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f24])).
% 0.12/0.45 fof(f94,plain,(
% 0.12/0.45 relation(sK8_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.45 fof(f100,plain,(
% 0.12/0.45 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(in(A,relation_dom(relation_composition(C,B)))<=>(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B)))))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.12/0.45 fof(f101,plain,(
% 0.12/0.45 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((~in(A,relation_dom(relation_composition(C,B)))|(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B))))&(in(A,relation_dom(relation_composition(C,B)))|(~in(A,relation_dom(C))|~in(apply(C,A),relation_dom(B))))))))),
% 0.12/0.45 inference(NNF_transformation,[status(thm)],[f100])).
% 0.12/0.45 fof(f102,plain,(
% 0.12/0.45 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~in(A,relation_dom(relation_composition(C,B)))|(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B)))))&(![A]: (in(A,relation_dom(relation_composition(C,B)))|(~in(A,relation_dom(C))|~in(apply(C,A),relation_dom(B)))))))))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f101])).
% 0.12/0.45 fof(f103,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~in(X2,relation_dom(relation_composition(X1,X0)))|in(X2,relation_dom(X1)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f102])).
% 0.12/0.45 fof(f104,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~in(X2,relation_dom(relation_composition(X1,X0)))|in(apply(X1,X2),relation_dom(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f102])).
% 0.12/0.45 fof(f105,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,X0)))|~in(X2,relation_dom(X1))|~in(apply(X1,X2),relation_dom(X0)))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f102])).
% 0.12/0.45 fof(f106,plain,(
% 0.12/0.45 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.12/0.45 fof(f107,plain,(
% 0.12/0.45 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f106])).
% 0.12/0.45 fof(f108,plain,(
% 0.12/0.45 ![A,B]: ((~relation(B)|~function(B))|(B=identity_relation(A)<=>(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.12/0.45 fof(f109,plain,(
% 0.12/0.45 ![A,B]: ((~relation(B)|~function(B))|((~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C))))&(B=identity_relation(A)|(~relation_dom(B)=A|(?[C]: (in(C,A)&~apply(B,C)=C))))))),
% 0.12/0.45 inference(NNF_transformation,[status(thm)],[f108])).
% 0.12/0.45 fof(f110,plain,(
% 0.12/0.45 ![B]: ((~relation(B)|~function(B))|((![A]: (~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))&(![A]: (B=identity_relation(A)|(~relation_dom(B)=A|(?[C]: (in(C,A)&~apply(B,C)=C)))))))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f109])).
% 0.12/0.45 fof(f111,plain,(
% 0.12/0.45 ![B]: ((~relation(B)|~function(B))|((![A]: (~B=identity_relation(A)|(relation_dom(B)=A&(![C]: (~in(C,A)|apply(B,C)=C)))))&(![A]: (B=identity_relation(A)|(~relation_dom(B)=A|(in(sK9_skl(A,B),A)&~apply(B,sK9_skl(A,B))=sK9_skl(A,B)))))))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(A,B))],[f110])).
% 0.12/0.45 fof(f112,plain,(
% 0.12/0.45 ![X0,X1]: (~relation(X0)|~function(X0)|~X0=identity_relation(X1)|relation_dom(X0)=X1)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f111])).
% 0.12/0.45 fof(f113,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~X0=identity_relation(X1)|~in(X2,X1)|apply(X0,X2)=X2)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f111])).
% 0.12/0.45 fof(f114,plain,(
% 0.12/0.45 ![X0,X1]: (~relation(X0)|~function(X0)|X0=identity_relation(X1)|~relation_dom(X0)=X1|in(sK9_skl(X1,X0),X1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f111])).
% 0.12/0.45 fof(f116,plain,(
% 0.12/0.45 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 0.12/0.45 inference(NNF_transformation,[status(thm)],[f30])).
% 0.12/0.45 fof(f117,plain,(
% 0.12/0.45 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f116])).
% 0.12/0.45 fof(f119,plain,(
% 0.12/0.45 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f117])).
% 0.12/0.45 fof(f120,plain,(
% 0.12/0.45 (?[A,B,C]: ((relation(C)&function(C))&(in(B,relation_dom(relation_composition(C,identity_relation(A))))<~>(in(B,relation_dom(C))&in(apply(C,B),A)))))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.12/0.45 fof(f121,plain,(
% 0.12/0.45 ?[A,B,C]: ((relation(C)&function(C))&((in(B,relation_dom(relation_composition(C,identity_relation(A))))|(in(B,relation_dom(C))&in(apply(C,B),A)))&(~in(B,relation_dom(relation_composition(C,identity_relation(A))))|(~in(B,relation_dom(C))|~in(apply(C,B),A)))))),
% 0.12/0.45 inference(NNF_transformation,[status(thm)],[f120])).
% 0.12/0.45 fof(f122,plain,(
% 0.12/0.45 ?[C]: ((relation(C)&function(C))&(?[A,B]: ((in(B,relation_dom(relation_composition(C,identity_relation(A))))|(in(B,relation_dom(C))&in(apply(C,B),A)))&(~in(B,relation_dom(relation_composition(C,identity_relation(A))))|(~in(B,relation_dom(C))|~in(apply(C,B),A))))))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f121])).
% 0.12/0.45 fof(f123,plain,(
% 0.12/0.45 ((relation(sK10_skl)&function(sK10_skl))&((in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|(in(sK12_skl,relation_dom(sK10_skl))&in(apply(sK10_skl,sK12_skl),sK11_skl)))&(~in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|(~in(sK12_skl,relation_dom(sK10_skl))|~in(apply(sK10_skl,sK12_skl),sK11_skl)))))),
% 0.12/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK10_skl),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f122])).
% 0.12/0.45 fof(f124,plain,(
% 0.12/0.45 relation(sK10_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.45 fof(f125,plain,(
% 0.12/0.45 function(sK10_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.45 fof(f126,plain,(
% 0.12/0.45 in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|in(sK12_skl,relation_dom(sK10_skl))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.45 fof(f127,plain,(
% 0.12/0.45 in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|in(apply(sK10_skl,sK12_skl),sK11_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.45 fof(f128,plain,(
% 0.12/0.45 ~in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|~in(sK12_skl,relation_dom(sK10_skl))|~in(apply(sK10_skl,sK12_skl),sK11_skl)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.45 fof(f132,plain,(
% 0.12/0.45 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.12/0.45 fof(f133,plain,(
% 0.12/0.45 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f132])).
% 0.12/0.45 fof(f134,plain,(
% 0.12/0.45 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f133])).
% 0.12/0.45 fof(f135,plain,(
% 0.12/0.45 ![A]: (~empty(A)|A=empty_set)),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.12/0.45 fof(f136,plain,(
% 0.12/0.45 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/0.45 fof(f137,plain,(
% 0.12/0.45 ![A,B]: (~in(A,B)|~empty(B))),
% 0.12/0.45 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.12/0.45 fof(f138,plain,(
% 0.12/0.45 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 0.12/0.45 inference(miniscoping,[status(thm)],[f137])).
% 0.12/0.45 fof(f139,plain,(
% 0.12/0.45 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 0.12/0.45 inference(cnf_transformation,[status(thm)],[f138])).
% 0.12/0.45 fof(f143,definition,(
% 0.12/0.45 sQ0_spl <=> (in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl)))))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f144,plain,(
% 0.12/0.45 in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|~sQ0_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f143])).
% 0.12/0.45 fof(f146,definition,(
% 0.12/0.45 sQ1_spl <=> (in(sK12_skl,relation_dom(sK10_skl)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f147,plain,(
% 0.12/0.45 in(sK12_skl,relation_dom(sK10_skl))|~sQ1_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f146])).
% 0.12/0.45 fof(f149,plain,(
% 0.12/0.45 sQ0_spl|sQ1_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f126,f143,f146])).
% 0.12/0.45 fof(f150,definition,(
% 0.12/0.45 sQ2_spl <=> (in(apply(sK10_skl,sK12_skl),sK11_skl))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f151,plain,(
% 0.12/0.45 in(apply(sK10_skl,sK12_skl),sK11_skl)|~sQ2_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f150])).
% 0.12/0.45 fof(f152,plain,(
% 0.12/0.45 ~in(apply(sK10_skl,sK12_skl),sK11_skl)|sQ2_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f150])).
% 0.12/0.45 fof(f153,plain,(
% 0.12/0.45 sQ0_spl|sQ2_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f127,f143,f150])).
% 0.12/0.45 fof(f154,plain,(
% 0.12/0.45 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f128,f143,f146,f150])).
% 0.12/0.45 fof(f155,plain,(
% 0.12/0.45 ![X0]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|relation_dom(identity_relation(X0))=X0)),
% 0.12/0.45 inference(destructive_equality_resolution,[status(thm)],[f112])).
% 0.12/0.45 fof(f156,plain,(
% 0.12/0.45 ![X0,X1]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,X0)|apply(identity_relation(X0),X1)=X1)),
% 0.12/0.45 inference(destructive_equality_resolution,[status(thm)],[f113])).
% 0.12/0.45 fof(f157,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|~function(X0)|X0=identity_relation(relation_dom(X0))|in(sK9_skl(relation_dom(X0),X0),relation_dom(X0)))),
% 0.12/0.45 inference(destructive_equality_resolution,[status(thm)],[f114])).
% 0.12/0.45 fof(f163,plain,(
% 0.12/0.45 function(sK4_skl)),
% 0.12/0.45 inference(resolution,[status(thm)],[f84,f41])).
% 0.12/0.45 fof(f167,plain,(
% 0.12/0.45 empty(relation_dom(empty_set))),
% 0.12/0.45 inference(resolution,[status(thm)],[f68,f52])).
% 0.12/0.45 fof(f171,plain,(
% 0.12/0.45 empty(relation_dom(relation_dom(empty_set)))),
% 0.12/0.45 inference(resolution,[status(thm)],[f167,f68])).
% 0.12/0.45 fof(f182,plain,(
% 0.12/0.45 empty(relation_dom(relation_dom(relation_dom(empty_set))))),
% 0.12/0.45 inference(resolution,[status(thm)],[f171,f68])).
% 0.12/0.45 fof(f193,plain,(
% 0.12/0.45 empty(relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))),
% 0.12/0.45 inference(resolution,[status(thm)],[f182,f68])).
% 0.12/0.45 fof(f205,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|empty(relation_composition(X0,relation_dom(relation_dom(relation_dom(relation_dom(empty_set)))))))),
% 0.12/0.45 inference(resolution,[status(thm)],[f193,f50])).
% 0.12/0.45 fof(f217,plain,(
% 0.12/0.45 ![X0,X1]: (relation_composition(X0,X1)=empty_set|~empty(X0)|~relation(X1))),
% 0.12/0.45 inference(resolution,[status(thm)],[f136,f71])).
% 0.12/0.45 fof(f219,plain,(
% 0.12/0.45 relation_dom(relation_dom(relation_dom(empty_set)))=empty_set),
% 0.12/0.45 inference(resolution,[status(thm)],[f136,f182])).
% 0.12/0.45 fof(f220,plain,(
% 0.12/0.45 relation_dom(relation_dom(empty_set))=empty_set),
% 0.12/0.45 inference(resolution,[status(thm)],[f136,f171])).
% 0.12/0.45 fof(f223,plain,(
% 0.12/0.45 sK4_skl=empty_set),
% 0.12/0.45 inference(resolution,[status(thm)],[f136,f84])).
% 0.12/0.45 fof(f225,plain,(
% 0.12/0.45 ![X0]: (~empty(X0)|X0=sK4_skl)),
% 0.12/0.45 inference(backward_demodulation,[status(thm)],[f223,f136])).
% 0.12/0.45 fof(f235,plain,(
% 0.12/0.45 relation(sK4_skl)),
% 0.12/0.45 inference(backward_demodulation,[status(thm)],[f223,f53])).
% 0.12/0.45 fof(f242,plain,(
% 0.12/0.45 relation_dom(relation_dom(sK4_skl))=empty_set),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f223,f220])).
% 0.12/0.45 fof(f243,plain,(
% 0.12/0.45 relation_dom(relation_dom(sK4_skl))=sK4_skl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f223,f242])).
% 0.12/0.45 fof(f244,plain,(
% 0.12/0.45 ~empty(relation_dom(sK4_skl))|relation(sK4_skl)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f243,f69])).
% 0.12/0.45 fof(f245,plain,(
% 0.12/0.45 empty(relation_dom(sK4_skl))|~relation(relation_dom(sK4_skl))|~empty(sK4_skl)),
% 0.12/0.45 inference(paramodulation,[status(thm)],[f243,f66])).
% 0.12/0.45 fof(f246,definition,(
% 0.12/0.45 sQ11_spl <=> (empty(relation_dom(sK4_skl)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f249,definition,(
% 0.12/0.45 sQ12_spl <=> (relation(sK4_skl))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f252,plain,(
% 0.12/0.45 ~sQ11_spl|sQ12_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f244,f246,f249])).
% 0.12/0.45 fof(f253,definition,(
% 0.12/0.45 sQ13_spl <=> (relation(relation_dom(sK4_skl)))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f255,plain,(
% 0.12/0.45 ~relation(relation_dom(sK4_skl))|sQ13_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f253])).
% 0.12/0.45 fof(f256,definition,(
% 0.12/0.45 sQ14_spl <=> (empty(sK4_skl))),
% 0.12/0.45 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.45 fof(f258,plain,(
% 0.12/0.45 ~empty(sK4_skl)|sQ14_spl),
% 0.12/0.45 inference(component_clause,[status(thm)],[f256])).
% 0.12/0.45 fof(f259,plain,(
% 0.12/0.45 sQ11_spl|~sQ13_spl|~sQ14_spl),
% 0.12/0.45 inference(split_clause,[status(thm)],[f245,f246,f253,f256])).
% 0.12/0.45 fof(f260,plain,(
% 0.12/0.45 $false|sQ14_spl),
% 0.12/0.45 inference(forward_subsumption_resolution,[status(thm)],[f258,f84])).
% 0.12/0.45 fof(f261,plain,(
% 0.12/0.45 sQ14_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f260])).
% 0.12/0.45 fof(f264,plain,(
% 0.12/0.45 relation_dom(relation_dom(relation_dom(sK4_skl)))=empty_set),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f223,f219])).
% 0.12/0.45 fof(f265,plain,(
% 0.12/0.45 relation_dom(sK4_skl)=empty_set),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f243,f264])).
% 0.12/0.45 fof(f267,plain,(
% 0.12/0.45 relation_dom(sK4_skl)=sK4_skl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f223,f265])).
% 0.12/0.45 fof(f272,plain,(
% 0.12/0.45 ![X0]: (empty(X0)|in(sK0_skl(X0),X0))),
% 0.12/0.45 inference(resolution,[status(thm)],[f107,f48])).
% 0.12/0.45 fof(f292,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|empty(relation_composition(X0,relation_dom(relation_dom(relation_dom(relation_dom(sK4_skl)))))))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f223,f205])).
% 0.12/0.45 fof(f293,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|empty(relation_composition(X0,relation_dom(relation_dom(relation_dom(sK4_skl))))))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f267,f292])).
% 0.12/0.45 fof(f294,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|empty(relation_composition(X0,relation_dom(relation_dom(sK4_skl)))))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f267,f293])).
% 0.12/0.45 fof(f295,plain,(
% 0.12/0.45 ![X0]: (~relation(X0)|empty(relation_composition(X0,relation_dom(sK4_skl))))),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f267,f294])).
% 0.12/0.46 fof(f296,plain,(
% 0.12/0.46 ![X0]: (~relation(X0)|empty(relation_composition(X0,sK4_skl)))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f267,f295])).
% 0.12/0.46 fof(f297,plain,(
% 0.12/0.46 ![X0]: (~relation(X0)|relation_composition(X0,sK4_skl)=sK4_skl)),
% 0.12/0.46 inference(resolution,[status(thm)],[f296,f225])).
% 0.12/0.46 fof(f308,plain,(
% 0.12/0.46 ~relation(sK4_skl)|sQ13_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f267,f255])).
% 0.12/0.46 fof(f309,plain,(
% 0.12/0.46 $false|sQ13_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f308,f235])).
% 0.12/0.46 fof(f310,plain,(
% 0.12/0.46 sQ13_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f309])).
% 0.12/0.46 fof(f318,plain,(
% 0.12/0.46 ~relation(identity_relation(sK11_skl))|~function(identity_relation(sK11_skl))|~relation(sK10_skl)|~function(sK10_skl)|in(sK12_skl,relation_dom(sK10_skl))|~sQ0_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f103,f144])).
% 0.12/0.46 fof(f319,definition,(
% 0.12/0.46 sQ15_spl <=> (relation(identity_relation(sK11_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f321,plain,(
% 0.12/0.46 ~relation(identity_relation(sK11_skl))|sQ15_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f319])).
% 0.12/0.46 fof(f322,definition,(
% 0.12/0.46 sQ16_spl <=> (function(identity_relation(sK11_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f324,plain,(
% 0.12/0.46 ~function(identity_relation(sK11_skl))|sQ16_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f322])).
% 0.12/0.46 fof(f325,definition,(
% 0.12/0.46 sQ17_spl <=> (relation(sK10_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f327,plain,(
% 0.12/0.46 ~relation(sK10_skl)|sQ17_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f325])).
% 0.12/0.46 fof(f328,definition,(
% 0.12/0.46 sQ18_spl <=> (function(sK10_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f330,plain,(
% 0.12/0.46 ~function(sK10_skl)|sQ18_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f328])).
% 0.12/0.46 fof(f331,plain,(
% 0.12/0.46 ~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|sQ1_spl|~sQ0_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f318,f319,f322,f325,f328,f146,f143])).
% 0.12/0.46 fof(f335,plain,(
% 0.12/0.46 ![X0]: (sK6_skl(X0)=sK4_skl)),
% 0.12/0.46 inference(resolution,[status(thm)],[f90,f225])).
% 0.12/0.46 fof(f344,plain,(
% 0.12/0.46 ![X0]: (empty(X0)|empty(powerset(X0))|in(sK3_skl(X0),powerset(X0)))),
% 0.12/0.46 inference(resolution,[status(thm)],[f81,f107])).
% 0.12/0.46 fof(f345,plain,(
% 0.12/0.46 ![X0]: (empty(X0)|in(sK3_skl(X0),powerset(X0)))),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f344,f58])).
% 0.12/0.46 fof(f346,plain,(
% 0.12/0.46 ![X0]: (element(sK4_skl,powerset(X0)))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f335,f89])).
% 0.12/0.46 fof(f348,plain,(
% 0.12/0.46 ![X0]: (empty(powerset(X0))|in(sK4_skl,powerset(X0)))),
% 0.12/0.46 inference(resolution,[status(thm)],[f346,f107])).
% 0.12/0.46 fof(f349,plain,(
% 0.12/0.46 ![X0]: (in(sK4_skl,powerset(X0)))),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f348,f58])).
% 0.12/0.46 fof(f352,plain,(
% 0.12/0.46 ~empty(relation_dom(sK10_skl))|~sQ1_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f147,f139])).
% 0.12/0.46 fof(f355,definition,(
% 0.12/0.46 sQ19_spl <=> (empty(relation_dom(sK10_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f356,plain,(
% 0.12/0.46 empty(relation_dom(sK10_skl))|~sQ19_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f355])).
% 0.12/0.46 fof(f371,plain,(
% 0.12/0.46 relation_composition(sK4_skl,sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f235])).
% 0.12/0.46 fof(f373,plain,(
% 0.12/0.46 relation_composition(sK8_skl,sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f94])).
% 0.12/0.46 fof(f374,plain,(
% 0.12/0.46 relation_composition(sK5_skl,sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f87])).
% 0.12/0.46 fof(f375,plain,(
% 0.12/0.46 relation_composition(sK1_skl,sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f74])).
% 0.12/0.46 fof(f376,plain,(
% 0.12/0.46 ![X0]: (relation_composition(identity_relation(X0),sK4_skl)=sK4_skl)),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f46])).
% 0.12/0.46 fof(f380,plain,(
% 0.12/0.46 relation_composition(sK10_skl,sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f297,f124])).
% 0.12/0.46 fof(f383,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f371,f104])).
% 0.12/0.46 fof(f384,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f371,f103])).
% 0.12/0.46 fof(f391,definition,(
% 0.12/0.46 sQ21_spl <=> (function(sK4_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f393,plain,(
% 0.12/0.46 ~function(sK4_skl)|sQ21_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f391])).
% 0.12/0.46 fof(f394,definition,(
% 0.12/0.46 ![X0]: (sQ22_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f397,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|sQ22_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f383,f249,f391,f394])).
% 0.12/0.46 fof(f398,definition,(
% 0.12/0.46 ![X0]: (sQ23_spl <=> (~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f401,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|sQ23_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f384,f249,f391,f398])).
% 0.12/0.46 fof(f407,plain,(
% 0.12/0.46 $false|sQ21_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f393,f163])).
% 0.12/0.46 fof(f408,plain,(
% 0.12/0.46 sQ21_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f407])).
% 0.12/0.46 fof(f412,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK8_skl)|~function(sK8_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK8_skl,X0),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f373,f104])).
% 0.12/0.46 fof(f413,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK8_skl)|~function(sK8_skl)|~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK8_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f373,f103])).
% 0.12/0.46 fof(f419,definition,(
% 0.12/0.46 sQ24_spl <=> (relation(sK8_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f421,plain,(
% 0.12/0.46 ~relation(sK8_skl)|sQ24_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f419])).
% 0.12/0.46 fof(f423,definition,(
% 0.12/0.46 sQ25_spl <=> (function(sK8_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f426,definition,(
% 0.12/0.46 ![X0]: (sQ26_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK8_skl,X0),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f429,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ24_spl|~sQ25_spl|sQ26_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f412,f249,f391,f419,f423,f426])).
% 0.12/0.46 fof(f430,definition,(
% 0.12/0.46 ![X0]: (sQ27_spl <=> (~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK8_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f433,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ24_spl|~sQ25_spl|sQ27_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f413,f249,f391,f419,f423,f430])).
% 0.12/0.46 fof(f442,plain,(
% 0.12/0.46 $false|sQ24_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f421,f94])).
% 0.12/0.46 fof(f443,plain,(
% 0.12/0.46 sQ24_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f442])).
% 0.12/0.46 fof(f444,plain,(
% 0.12/0.46 ![X0,X1]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(X0)|~function(X0)|in(X1,relation_dom(relation_composition(X0,sK4_skl)))|~in(X1,relation_dom(X0))|~in(apply(X0,X1),sK4_skl))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f267,f105])).
% 0.12/0.46 fof(f445,definition,(
% 0.12/0.46 ![X0,X1]: (sQ29_spl <=> (~relation(X0)|~function(X0)|in(X1,relation_dom(relation_composition(X0,sK4_skl)))|~in(X1,relation_dom(X0))|~in(apply(X0,X1),sK4_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f448,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|sQ29_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f444,f249,f391,f445])).
% 0.12/0.46 fof(f449,plain,(
% 0.12/0.46 ![X0]: (~function(identity_relation(X0))|relation_dom(identity_relation(X0))=X0)),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f155,f46])).
% 0.12/0.46 fof(f450,plain,(
% 0.12/0.46 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 0.12/0.46 inference(resolution,[status(thm)],[f449,f62])).
% 0.12/0.46 fof(f452,plain,(
% 0.12/0.46 ![X0,X1,X2]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,identity_relation(X0))))|~in(X2,relation_dom(X1))|~in(apply(X1,X2),X0))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f450,f105])).
% 0.12/0.46 fof(f454,plain,(
% 0.12/0.46 ![X0]: (empty(identity_relation(X0))|~relation(identity_relation(X0))|~empty(X0))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f450,f66])).
% 0.12/0.46 fof(f455,plain,(
% 0.12/0.46 ![X0,X1,X2]: (~function(identity_relation(X0))|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,identity_relation(X0))))|~in(X2,relation_dom(X1))|~in(apply(X1,X2),X0))),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f452,f46])).
% 0.12/0.46 fof(f456,plain,(
% 0.12/0.46 ![X0]: (empty(identity_relation(X0))|~empty(X0))),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f454,f46])).
% 0.12/0.46 fof(f464,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK5_skl)|~function(sK5_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK5_skl,X0),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f374,f104])).
% 0.12/0.46 fof(f465,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK5_skl)|~function(sK5_skl)|~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK5_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f374,f103])).
% 0.12/0.46 fof(f471,definition,(
% 0.12/0.46 sQ30_spl <=> (relation(sK5_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f473,plain,(
% 0.12/0.46 ~relation(sK5_skl)|sQ30_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f471])).
% 0.12/0.46 fof(f475,definition,(
% 0.12/0.46 sQ31_spl <=> (function(sK5_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f478,definition,(
% 0.12/0.46 ![X0]: (sQ32_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK5_skl,X0),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f481,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ30_spl|~sQ31_spl|sQ32_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f464,f249,f391,f471,f475,f478])).
% 0.12/0.46 fof(f482,definition,(
% 0.12/0.46 ![X0]: (sQ33_spl <=> (~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK5_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f485,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ30_spl|~sQ31_spl|sQ33_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f465,f249,f391,f471,f475,f482])).
% 0.12/0.46 fof(f494,plain,(
% 0.12/0.46 $false|sQ30_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f473,f87])).
% 0.12/0.46 fof(f495,plain,(
% 0.12/0.46 sQ30_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f494])).
% 0.12/0.46 fof(f497,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK1_skl)|~function(sK1_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK1_skl,X0),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f375,f104])).
% 0.12/0.46 fof(f498,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK1_skl)|~function(sK1_skl)|~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK1_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f375,f103])).
% 0.12/0.46 fof(f504,definition,(
% 0.12/0.46 sQ35_spl <=> (relation(sK1_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f506,plain,(
% 0.12/0.46 ~relation(sK1_skl)|sQ35_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f504])).
% 0.12/0.46 fof(f508,definition,(
% 0.12/0.46 sQ36_spl <=> (function(sK1_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f510,plain,(
% 0.12/0.46 ~function(sK1_skl)|sQ36_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f508])).
% 0.12/0.46 fof(f511,definition,(
% 0.12/0.46 ![X0]: (sQ37_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK1_skl,X0),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f514,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ35_spl|~sQ36_spl|sQ37_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f497,f249,f391,f504,f508,f511])).
% 0.12/0.46 fof(f515,definition,(
% 0.12/0.46 ![X0]: (sQ38_spl <=> (~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK1_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f518,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ35_spl|~sQ36_spl|sQ38_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f498,f249,f391,f504,f508,f515])).
% 0.12/0.46 fof(f527,plain,(
% 0.12/0.46 $false|sQ35_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f506,f74])).
% 0.12/0.46 fof(f528,plain,(
% 0.12/0.46 sQ35_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f527])).
% 0.12/0.46 fof(f529,plain,(
% 0.12/0.46 $false|sQ36_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f510,f75])).
% 0.12/0.46 fof(f530,plain,(
% 0.12/0.46 sQ36_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f529])).
% 0.12/0.46 fof(f535,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK10_skl)|~function(sK10_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK10_skl,X0),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f380,f104])).
% 0.12/0.46 fof(f536,plain,(
% 0.12/0.46 ![X0]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(sK10_skl)|~function(sK10_skl)|~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK10_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f380,f103])).
% 0.12/0.46 fof(f543,definition,(
% 0.12/0.46 ![X0]: (sQ40_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK10_skl,X0),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f546,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ17_spl|~sQ18_spl|sQ40_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f535,f249,f391,f325,f328,f543])).
% 0.12/0.46 fof(f547,definition,(
% 0.12/0.46 ![X0]: (sQ41_spl <=> (~in(X0,relation_dom(sK4_skl))|in(X0,relation_dom(sK10_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f550,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|~sQ17_spl|~sQ18_spl|sQ41_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f536,f249,f391,f325,f328,f547])).
% 0.12/0.46 fof(f559,plain,(
% 0.12/0.46 $false|sQ17_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f327,f124])).
% 0.12/0.46 fof(f560,plain,(
% 0.12/0.46 sQ17_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f559])).
% 0.12/0.46 fof(f561,plain,(
% 0.12/0.46 $false|sQ18_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f330,f125])).
% 0.12/0.46 fof(f562,plain,(
% 0.12/0.46 sQ18_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f561])).
% 0.12/0.46 fof(f566,plain,(
% 0.12/0.46 ![X0,X1]: (~function(identity_relation(X0))|~in(X1,X0)|apply(identity_relation(X0),X1)=X1)),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f156,f46])).
% 0.12/0.46 fof(f567,plain,(
% 0.12/0.46 ![X0,X1]: (~in(X0,X1)|apply(identity_relation(X1),X0)=X0)),
% 0.12/0.46 inference(resolution,[status(thm)],[f566,f62])).
% 0.12/0.46 fof(f568,plain,(
% 0.12/0.46 ~relation(sK4_skl)|sK4_skl=identity_relation(relation_dom(sK4_skl))|in(sK9_skl(relation_dom(sK4_skl),sK4_skl),relation_dom(sK4_skl))),
% 0.12/0.46 inference(resolution,[status(thm)],[f157,f163])).
% 0.12/0.46 fof(f571,plain,(
% 0.12/0.46 ![X0,X1]: (~relation(relation_composition(X0,X1))|relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|in(sK9_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 0.12/0.46 inference(resolution,[status(thm)],[f157,f57])).
% 0.12/0.46 fof(f573,definition,(
% 0.12/0.46 sQ43_spl <=> (sK4_skl=identity_relation(relation_dom(sK4_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f574,plain,(
% 0.12/0.46 sK4_skl=identity_relation(relation_dom(sK4_skl))|~sQ43_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f573])).
% 0.12/0.46 fof(f576,definition,(
% 0.12/0.46 sQ44_spl <=> (in(sK9_skl(relation_dom(sK4_skl),sK4_skl),relation_dom(sK4_skl)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f577,plain,(
% 0.12/0.46 in(sK9_skl(relation_dom(sK4_skl),sK4_skl),relation_dom(sK4_skl))|~sQ44_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f576])).
% 0.12/0.46 fof(f579,plain,(
% 0.12/0.46 ~sQ12_spl|sQ43_spl|sQ44_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f568,f249,f573,f576])).
% 0.12/0.46 fof(f587,plain,(
% 0.12/0.46 ![X0,X1]: (relation_composition(X0,X1)=identity_relation(relation_dom(relation_composition(X0,X1)))|in(sK9_skl(relation_dom(relation_composition(X0,X1)),relation_composition(X0,X1)),relation_dom(relation_composition(X0,X1)))|~relation(X0)|~function(X0)|~relation(X1)|~function(X1))),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f571,f45])).
% 0.12/0.46 fof(f595,plain,(
% 0.12/0.46 sK4_skl=identity_relation(sK4_skl)|~sQ43_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f267,f574])).
% 0.12/0.46 fof(f625,plain,(
% 0.12/0.46 $false|sQ15_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f321,f46])).
% 0.12/0.46 fof(f626,plain,(
% 0.12/0.46 sQ15_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f625])).
% 0.12/0.46 fof(f627,plain,(
% 0.12/0.46 $false|sQ16_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f324,f62])).
% 0.12/0.46 fof(f628,plain,(
% 0.12/0.46 sQ16_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f627])).
% 0.12/0.46 fof(f630,definition,(
% 0.12/0.46 sQ53_spl <=> (in(sK12_skl,sK11_skl))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f631,plain,(
% 0.12/0.46 in(sK12_skl,sK11_skl)|~sQ53_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f630])).
% 0.12/0.46 fof(f634,plain,(
% 0.12/0.46 ![X0]: (~function(sK4_skl)|~in(X0,sK4_skl)|apply(identity_relation(sK4_skl),X0)=X0|~sQ43_spl)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f595,f566])).
% 0.12/0.46 fof(f639,definition,(
% 0.12/0.46 ![X0]: (sQ54_spl <=> (~in(X0,sK4_skl)|apply(identity_relation(sK4_skl),X0)=X0))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f642,plain,(
% 0.12/0.46 ~sQ21_spl|sQ54_spl|~sQ43_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f634,f391,f639,f573])).
% 0.12/0.46 fof(f647,plain,(
% 0.12/0.46 empty(identity_relation(sK4_skl))),
% 0.12/0.46 inference(resolution,[status(thm)],[f456,f84])).
% 0.12/0.46 fof(f655,plain,(
% 0.12/0.46 ~relation(identity_relation(sK11_skl))|~function(identity_relation(sK11_skl))|~relation(sK10_skl)|~function(sK10_skl)|in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl)))|~sQ0_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f144,f104])).
% 0.12/0.46 fof(f660,definition,(
% 0.12/0.46 sQ55_spl <=> (in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f661,plain,(
% 0.12/0.46 in(apply(sK10_skl,sK12_skl),relation_dom(identity_relation(sK11_skl)))|~sQ55_spl),
% 0.12/0.46 inference(component_clause,[status(thm)],[f660])).
% 0.12/0.46 fof(f663,plain,(
% 0.12/0.46 ~sQ15_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|sQ55_spl|~sQ0_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f655,f319,f322,f325,f328,f660,f143])).
% 0.12/0.46 fof(f683,plain,(
% 0.12/0.46 in(apply(sK10_skl,sK12_skl),sK11_skl)|~sQ55_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f450,f661])).
% 0.12/0.46 fof(f687,plain,(
% 0.12/0.46 $false|~sQ55_spl|sQ2_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f152,f683])).
% 0.12/0.46 fof(f688,plain,(
% 0.12/0.46 ~sQ55_spl|sQ2_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f687])).
% 0.12/0.46 fof(f700,plain,(
% 0.12/0.46 ![X0,X1,X2,X3]: (~in(X0,X1)|~element(X1,powerset(relation_composition(X2,X3)))|~empty(X2)|~relation(X3))),
% 0.12/0.46 inference(resolution,[status(thm)],[f134,f71])).
% 0.12/0.46 fof(f701,plain,(
% 0.12/0.46 ![X0,X1]: (~in(X0,X1)|~element(X1,powerset(sK4_skl)))),
% 0.12/0.46 inference(resolution,[status(thm)],[f134,f84])).
% 0.12/0.46 fof(f703,plain,(
% 0.12/0.46 ![X0,X1,X2,X3,X4]: (~in(X0,X1)|~element(X1,powerset(relation_composition(relation_composition(X2,X3),X4)))|~relation(X4)|~empty(X2)|~relation(X3))),
% 0.12/0.46 inference(resolution,[status(thm)],[f700,f71])).
% 0.12/0.46 fof(f738,plain,(
% 0.12/0.46 ![X0]: (empty(X0)|~in(X0,sK0_skl(X0)))),
% 0.12/0.46 inference(resolution,[status(thm)],[f272,f39])).
% 0.12/0.46 fof(f747,plain,(
% 0.12/0.46 $false|~sQ1_spl|~sQ19_spl),
% 0.12/0.46 inference(forward_subsumption_resolution,[status(thm)],[f356,f352])).
% 0.12/0.46 fof(f748,plain,(
% 0.12/0.46 ~sQ1_spl|~sQ19_spl),
% 0.12/0.46 inference(contradiction_clause,[status(thm)],[f747])).
% 0.12/0.46 fof(f753,plain,(
% 0.12/0.46 ![X0,X1]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,relation_dom(sK4_skl))|in(apply(identity_relation(X0),X1),relation_dom(sK4_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f376,f104])).
% 0.12/0.46 fof(f754,plain,(
% 0.12/0.46 ![X0,X1]: (~relation(sK4_skl)|~function(sK4_skl)|~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,relation_dom(sK4_skl))|in(X1,relation_dom(identity_relation(X0))))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f376,f103])).
% 0.12/0.46 fof(f760,definition,(
% 0.12/0.46 ![X0]: (sQ60_spl <=> (~relation(identity_relation(X0))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f761,plain,(
% 0.12/0.46 ![X0]: (~relation(identity_relation(X0))|~sQ60_spl)),
% 0.12/0.46 inference(component_clause,[status(thm)],[f760])).
% 0.12/0.46 fof(f764,definition,(
% 0.12/0.46 ![X0,X1]: (sQ61_spl <=> (~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,relation_dom(sK4_skl))|in(apply(identity_relation(X0),X1),relation_dom(sK4_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f767,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|sQ61_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f753,f249,f391,f764])).
% 0.12/0.46 fof(f768,definition,(
% 0.12/0.46 ![X0,X1]: (sQ62_spl <=> (~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,relation_dom(sK4_skl))|in(X1,relation_dom(identity_relation(X0)))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f771,plain,(
% 0.12/0.46 ~sQ12_spl|~sQ21_spl|sQ62_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f754,f249,f391,f768])).
% 0.12/0.46 fof(f813,plain,(
% 0.12/0.46 apply(identity_relation(sK11_skl),sK12_skl)=sK12_skl|~sQ53_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f567,f631])).
% 0.12/0.46 fof(f820,plain,(
% 0.12/0.46 ![X0,X1]: (relation_composition(X0,X1)=sK4_skl|~empty(X0)|~relation(X1))),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f223,f217])).
% 0.12/0.46 fof(f823,plain,(
% 0.12/0.46 ![X0]: (relation_composition(sK4_skl,X0)=sK4_skl|~relation(X0))),
% 0.12/0.46 inference(resolution,[status(thm)],[f820,f84])).
% 0.12/0.46 fof(f824,plain,(
% 0.12/0.46 ![X0]: (~relation(X0)|~function(X0)|~relation(identity_relation(sK11_skl))|~function(identity_relation(sK11_skl))|in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),X0)))|~in(sK12_skl,relation_dom(identity_relation(sK11_skl)))|~in(sK12_skl,relation_dom(X0))|~sQ53_spl)),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f813,f105])).
% 0.12/0.46 fof(f825,definition,(
% 0.12/0.46 ![X0]: (sQ65_spl <=> (~relation(X0)|~function(X0)|in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),X0)))|~in(sK12_skl,relation_dom(X0))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f826,plain,(
% 0.12/0.46 ![X0]: (~relation(X0)|~function(X0)|in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),X0)))|~in(sK12_skl,relation_dom(X0))|~sQ65_spl)),
% 0.12/0.46 inference(component_clause,[status(thm)],[f825])).
% 0.12/0.46 fof(f828,definition,(
% 0.12/0.46 sQ66_spl <=> (in(sK12_skl,relation_dom(identity_relation(sK11_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f831,plain,(
% 0.12/0.46 sQ65_spl|~sQ15_spl|~sQ16_spl|~sQ66_spl|~sQ53_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f824,f825,f319,f322,f828,f630])).
% 0.12/0.46 fof(f862,plain,(
% 0.12/0.46 ~relation(sK10_skl)|~function(sK10_skl)|in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),sK10_skl)))|~sQ65_spl|~sQ1_spl),
% 0.12/0.46 inference(resolution,[status(thm)],[f826,f147])).
% 0.12/0.46 fof(f865,definition,(
% 0.12/0.46 sQ73_spl <=> (in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),sK10_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f868,plain,(
% 0.12/0.46 ~sQ17_spl|~sQ18_spl|sQ73_spl|~sQ65_spl|~sQ1_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f862,f325,f328,f865,f825,f146])).
% 0.12/0.46 fof(f879,plain,(
% 0.12/0.46 relation_composition(sK4_skl,sK8_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f823,f94])).
% 0.12/0.46 fof(f880,plain,(
% 0.12/0.46 relation_composition(sK4_skl,sK5_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f823,f87])).
% 0.12/0.46 fof(f881,plain,(
% 0.12/0.46 relation_composition(sK4_skl,sK1_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f823,f74])).
% 0.12/0.46 fof(f882,plain,(
% 0.12/0.46 ![X0]: (relation_composition(sK4_skl,identity_relation(X0))=sK4_skl)),
% 0.12/0.46 inference(resolution,[status(thm)],[f823,f46])).
% 0.12/0.46 fof(f886,plain,(
% 0.12/0.46 relation_composition(sK4_skl,sK10_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f823,f124])).
% 0.12/0.46 fof(f889,plain,(
% 0.12/0.46 ![X0]: (~relation(sK8_skl)|~function(sK8_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK8_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f879,f104])).
% 0.12/0.46 fof(f897,definition,(
% 0.12/0.46 ![X0]: (sQ75_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK8_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f900,plain,(
% 0.12/0.46 ~sQ24_spl|~sQ25_spl|~sQ12_spl|~sQ21_spl|sQ75_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f889,f419,f423,f249,f391,f897])).
% 0.12/0.46 fof(f908,plain,(
% 0.12/0.46 ![X0]: (~relation(sK5_skl)|~function(sK5_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK5_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f880,f104])).
% 0.12/0.46 fof(f916,definition,(
% 0.12/0.46 ![X0]: (sQ76_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK5_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f919,plain,(
% 0.12/0.46 ~sQ30_spl|~sQ31_spl|~sQ12_spl|~sQ21_spl|sQ76_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f908,f471,f475,f249,f391,f916])).
% 0.12/0.46 fof(f927,plain,(
% 0.12/0.46 ![X0]: (~relation(sK1_skl)|~function(sK1_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK1_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f881,f104])).
% 0.12/0.46 fof(f935,definition,(
% 0.12/0.46 ![X0]: (sQ77_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK1_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f938,plain,(
% 0.12/0.46 ~sQ35_spl|~sQ36_spl|~sQ12_spl|~sQ21_spl|sQ77_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f927,f504,f508,f249,f391,f935])).
% 0.12/0.46 fof(f947,plain,(
% 0.12/0.46 ![X0]: (~relation(sK10_skl)|~function(sK10_skl)|~relation(sK4_skl)|~function(sK4_skl)|~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK10_skl)))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f886,f104])).
% 0.12/0.46 fof(f955,definition,(
% 0.12/0.46 ![X0]: (sQ78_spl <=> (~in(X0,relation_dom(sK4_skl))|in(apply(sK4_skl,X0),relation_dom(sK10_skl))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f958,plain,(
% 0.12/0.46 ~sQ17_spl|~sQ18_spl|~sQ12_spl|~sQ21_spl|sQ78_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f947,f325,f328,f249,f391,f955])).
% 0.12/0.46 fof(f970,plain,(
% 0.12/0.46 ![X0,X1]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|~relation(sK4_skl)|~function(sK4_skl)|~in(X1,relation_dom(sK4_skl))|in(apply(sK4_skl,X1),relation_dom(identity_relation(X0))))),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f882,f104])).
% 0.12/0.46 fof(f978,definition,(
% 0.12/0.46 ![X0,X1]: (sQ79_spl <=> (~relation(identity_relation(X0))|~function(identity_relation(X0))|~in(X1,relation_dom(sK4_skl))|in(apply(sK4_skl,X1),relation_dom(identity_relation(X0)))))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f981,plain,(
% 0.12/0.46 sQ79_spl|~sQ12_spl|~sQ21_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f970,f978,f249,f391])).
% 0.12/0.46 fof(f994,plain,(
% 0.12/0.46 ![X0]: (relation_composition(X0,sK4_skl)=identity_relation(relation_dom(relation_composition(X0,sK4_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK4_skl)),relation_composition(X0,sK4_skl)),relation_dom(relation_composition(X0,sK4_skl)))|~relation(X0)|~function(X0)|~relation(sK4_skl))),
% 0.12/0.46 inference(resolution,[status(thm)],[f587,f163])).
% 0.12/0.46 fof(f995,plain,(
% 0.12/0.46 ![X0]: (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)),relation_dom(relation_composition(X0,sK1_skl)))|~relation(X0)|~function(X0)|~relation(sK1_skl))),
% 0.12/0.46 inference(resolution,[status(thm)],[f587,f75])).
% 0.12/0.46 fof(f1000,plain,(
% 0.12/0.46 ![X0]: (relation_composition(X0,sK10_skl)=identity_relation(relation_dom(relation_composition(X0,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK10_skl)),relation_composition(X0,sK10_skl)),relation_dom(relation_composition(X0,sK10_skl)))|~relation(X0)|~function(X0)|~relation(sK10_skl))),
% 0.12/0.46 inference(resolution,[status(thm)],[f587,f125])).
% 0.12/0.46 fof(f1001,definition,(
% 0.12/0.46 ![X0]: (sQ80_spl <=> (relation_composition(X0,sK4_skl)=identity_relation(relation_dom(relation_composition(X0,sK4_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK4_skl)),relation_composition(X0,sK4_skl)),relation_dom(relation_composition(X0,sK4_skl)))|~relation(X0)|~function(X0)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f1004,plain,(
% 0.12/0.46 sQ80_spl|~sQ12_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f994,f1001,f249])).
% 0.12/0.46 fof(f1005,definition,(
% 0.12/0.46 ![X0]: (sQ81_spl <=> (relation_composition(X0,sK1_skl)=identity_relation(relation_dom(relation_composition(X0,sK1_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK1_skl)),relation_composition(X0,sK1_skl)),relation_dom(relation_composition(X0,sK1_skl)))|~relation(X0)|~function(X0)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f1008,plain,(
% 0.12/0.46 sQ81_spl|~sQ35_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f995,f1005,f504])).
% 0.12/0.46 fof(f1011,definition,(
% 0.12/0.46 ![X0]: (sQ82_spl <=> (relation_composition(X0,sK10_skl)=identity_relation(relation_dom(relation_composition(X0,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK10_skl)),relation_composition(X0,sK10_skl)),relation_dom(relation_composition(X0,sK10_skl)))|~relation(X0)|~function(X0)))),
% 0.12/0.46 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.12/0.46 fof(f1012,plain,(
% 0.12/0.46 ![X0]: (relation_composition(X0,sK10_skl)=identity_relation(relation_dom(relation_composition(X0,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(X0,sK10_skl)),relation_composition(X0,sK10_skl)),relation_dom(relation_composition(X0,sK10_skl)))|~relation(X0)|~function(X0)|~sQ82_spl)),
% 0.12/0.46 inference(component_clause,[status(thm)],[f1011])).
% 0.12/0.46 fof(f1014,plain,(
% 0.12/0.46 sQ82_spl|~sQ17_spl),
% 0.12/0.46 inference(split_clause,[status(thm)],[f1000,f1011,f325])).
% 0.12/0.46 fof(f1023,plain,(
% 0.12/0.46 in(sK9_skl(sK4_skl,sK4_skl),relation_dom(sK4_skl))|~sQ44_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f267,f577])).
% 0.12/0.46 fof(f1024,plain,(
% 0.12/0.46 in(sK9_skl(sK4_skl,sK4_skl),sK4_skl)|~sQ44_spl),
% 0.12/0.46 inference(forward_demodulation,[status(thm)],[f267,f1023])).
% 0.12/0.46 fof(f1034,plain,(
% 0.12/0.46 ![X0,X1,X2,X3]: (~in(X0,X1)|~element(X1,powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X2),X3)))|~relation(X3)|~relation(X2))),
% 0.12/0.46 inference(resolution,[status(thm)],[f647,f703])).
% 0.12/0.46 fof(f1035,plain,(
% 0.12/0.46 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(relation_composition(identity_relation(sK4_skl),X2)))|~relation(X2))),
% 0.12/0.46 inference(resolution,[status(thm)],[f647,f700])).
% 0.12/0.46 fof(f1039,plain,(
% 0.12/0.46 identity_relation(sK4_skl)=sK4_skl),
% 0.12/0.46 inference(resolution,[status(thm)],[f647,f225])).
% 0.12/0.46 fof(f1045,plain,(
% 0.12/0.46 ![X0,X1]: (~element(X0,powerset(relation_composition(identity_relation(sK4_skl),X1)))|~relation(X1)|empty(X0))),
% 0.12/0.46 inference(resolution,[status(thm)],[f1035,f272])).
% 0.12/0.46 fof(f1046,plain,(
% 0.12/0.46 ![X0]: (~element(sK11_skl,powerset(relation_composition(identity_relation(sK4_skl),X0)))|~relation(X0)|~sQ53_spl)),
% 0.12/0.46 inference(resolution,[status(thm)],[f1035,f631])).
% 0.12/0.46 fof(f1051,plain,(
% 0.12/0.46 ~element(sK11_skl,powerset(sK4_skl))|~relation(sK4_skl)|~sQ53_spl),
% 0.12/0.46 inference(paramodulation,[status(thm)],[f376,f1046])).
% 0.12/0.47 fof(f1052,definition,(
% 0.12/0.47 sQ84_spl <=> (element(sK11_skl,powerset(sK4_skl)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1055,plain,(
% 0.12/0.47 ~sQ84_spl|~sQ12_spl|~sQ53_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1051,f1052,f249,f630])).
% 0.12/0.47 fof(f1061,plain,(
% 0.12/0.47 ![X0]: (~element(X0,powerset(sK4_skl))|~relation(sK4_skl)|empty(X0))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1045])).
% 0.12/0.47 fof(f1067,definition,(
% 0.12/0.47 ![X0]: (sQ86_spl <=> (~element(X0,powerset(sK4_skl))|empty(X0)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1068,plain,(
% 0.12/0.47 ![X0]: (~element(X0,powerset(sK4_skl))|empty(X0)|~sQ86_spl)),
% 0.12/0.47 inference(component_clause,[status(thm)],[f1067])).
% 0.12/0.47 fof(f1070,plain,(
% 0.12/0.47 sQ86_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1061,f1067,f249])).
% 0.12/0.47 fof(f1073,plain,(
% 0.12/0.47 empty(sK0_skl(powerset(sK4_skl)))|~sQ86_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f1068,f48])).
% 0.12/0.47 fof(f1080,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~element(powerset(X0),powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X1),X2)))|~relation(X2)|~relation(X1)|empty(X0))),
% 0.12/0.47 inference(resolution,[status(thm)],[f1034,f345])).
% 0.12/0.47 fof(f1081,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~element(X0,powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X1),X2)))|~relation(X2)|~relation(X1)|empty(X0))),
% 0.12/0.47 inference(resolution,[status(thm)],[f1034,f272])).
% 0.12/0.47 fof(f1082,plain,(
% 0.12/0.47 ![X0,X1]: (~element(sK11_skl,powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X0),X1)))|~relation(X1)|~relation(X0)|~sQ53_spl)),
% 0.12/0.47 inference(resolution,[status(thm)],[f1034,f631])).
% 0.12/0.47 fof(f1084,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~element(powerset(X0),powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X1),X2)))|~relation(X2)|~relation(X1))),
% 0.12/0.47 inference(resolution,[status(thm)],[f1034,f349])).
% 0.12/0.47 fof(f1087,plain,(
% 0.12/0.47 ![X0]: (~element(sK11_skl,powerset(relation_composition(sK4_skl,X0)))|~relation(X0)|~relation(sK4_skl)|~sQ53_spl)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1082])).
% 0.12/0.47 fof(f1088,definition,(
% 0.12/0.47 ![X0]: (sQ88_spl <=> (~element(sK11_skl,powerset(relation_composition(sK4_skl,X0)))|~relation(X0)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1091,plain,(
% 0.12/0.47 sQ88_spl|~sQ12_spl|~sQ53_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1087,f1088,f249,f630])).
% 0.12/0.47 fof(f1092,plain,(
% 0.12/0.47 $false|~sQ60_spl),
% 0.12/0.47 inference(forward_subsumption_resolution,[status(thm)],[f761,f46])).
% 0.12/0.47 fof(f1093,plain,(
% 0.12/0.47 ~sQ60_spl),
% 0.12/0.47 inference(contradiction_clause,[status(thm)],[f1092])).
% 0.12/0.47 fof(f1094,plain,(
% 0.12/0.47 ![X0,X1]: (~element(sK11_skl,powerset(relation_composition(relation_composition(identity_relation(sK4_skl),X0),X1)))|~relation(X1)|~relation(X0)|~sQ2_spl)),
% 0.12/0.47 inference(resolution,[status(thm)],[f151,f1034])).
% 0.12/0.47 fof(f1095,plain,(
% 0.12/0.47 ![X0]: (~element(sK11_skl,powerset(relation_composition(identity_relation(sK4_skl),X0)))|~relation(X0)|~sQ2_spl)),
% 0.12/0.47 inference(resolution,[status(thm)],[f151,f1035])).
% 0.12/0.47 fof(f1114,plain,(
% 0.12/0.47 ~element(sK11_skl,powerset(sK4_skl))|~relation(sK4_skl)|~sQ2_spl),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1095])).
% 0.12/0.47 fof(f1115,plain,(
% 0.12/0.47 ~sQ84_spl|~sQ12_spl|~sQ2_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1114,f1052,f249,f150])).
% 0.12/0.47 fof(f1116,plain,(
% 0.12/0.47 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(sK11_skl,relation_composition(relation_composition(identity_relation(sK4_skl),X1),X0))|~sQ2_spl)),
% 0.12/0.47 inference(resolution,[status(thm)],[f1094,f119])).
% 0.12/0.47 fof(f1118,plain,(
% 0.12/0.47 ![X0]: (~element(sK11_skl,powerset(relation_composition(sK4_skl,X0)))|~relation(X0)|~relation(sK4_skl)|~sQ2_spl)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1094])).
% 0.12/0.47 fof(f1119,plain,(
% 0.12/0.47 sQ88_spl|~sQ12_spl|~sQ2_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1118,f1088,f249,f150])).
% 0.12/0.47 fof(f1131,plain,(
% 0.12/0.47 ![X0]: (~relation(X0)|~relation(sK4_skl)|~subset(sK11_skl,relation_composition(sK4_skl,X0))|~sQ2_spl)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1116])).
% 0.12/0.47 fof(f1132,definition,(
% 0.12/0.47 ![X0]: (sQ89_spl <=> (~relation(X0)|~subset(sK11_skl,relation_composition(sK4_skl,X0))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1135,plain,(
% 0.12/0.47 sQ89_spl|~sQ12_spl|~sQ2_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1131,f1132,f249,f150])).
% 0.12/0.47 fof(f1136,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~subset(powerset(X2),relation_composition(relation_composition(identity_relation(sK4_skl),X1),X0)))),
% 0.12/0.47 inference(resolution,[status(thm)],[f1084,f119])).
% 0.12/0.47 fof(f1138,plain,(
% 0.12/0.47 ![X0,X1]: (~element(powerset(X0),powerset(relation_composition(sK4_skl,X1)))|~relation(X1)|~relation(sK4_skl))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1084])).
% 0.12/0.47 fof(f1139,definition,(
% 0.12/0.47 ![X0,X1]: (sQ90_spl <=> (~element(powerset(X0),powerset(relation_composition(sK4_skl,X1)))|~relation(X1)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1142,plain,(
% 0.12/0.47 sQ90_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1138,f1139,f249])).
% 0.12/0.47 fof(f1144,plain,(
% 0.12/0.47 ![X0,X1]: (~relation(X0)|~relation(sK4_skl)|~subset(powerset(X1),relation_composition(sK4_skl,X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1136])).
% 0.12/0.47 fof(f1145,definition,(
% 0.12/0.47 ![X0,X1]: (sQ91_spl <=> (~relation(X0)|~subset(powerset(X1),relation_composition(sK4_skl,X0))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1148,plain,(
% 0.12/0.47 sQ91_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1144,f1145,f249])).
% 0.12/0.47 fof(f1152,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|empty(X2)|~subset(X2,relation_composition(relation_composition(identity_relation(sK4_skl),X1),X0)))),
% 0.12/0.47 inference(resolution,[status(thm)],[f1081,f119])).
% 0.12/0.47 fof(f1154,plain,(
% 0.12/0.47 ![X0,X1]: (~element(X0,powerset(relation_composition(sK4_skl,X1)))|~relation(X1)|~relation(sK4_skl)|empty(X0))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1081])).
% 0.12/0.47 fof(f1157,definition,(
% 0.12/0.47 ![X0,X1]: (sQ92_spl <=> (~element(X0,powerset(relation_composition(sK4_skl,X1)))|~relation(X1)|empty(X0)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1160,plain,(
% 0.12/0.47 sQ92_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1154,f1157,f249])).
% 0.12/0.47 fof(f1168,plain,(
% 0.12/0.47 ![X0,X1]: (~relation(X0)|~relation(sK4_skl)|empty(X1)|~subset(X1,relation_composition(sK4_skl,X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f376,f1152])).
% 0.12/0.47 fof(f1171,definition,(
% 0.12/0.47 ![X0,X1]: (sQ93_spl <=> (~relation(X0)|empty(X1)|~subset(X1,relation_composition(sK4_skl,X0))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1174,plain,(
% 0.12/0.47 sQ93_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1168,f1171,f249])).
% 0.12/0.47 fof(f1201,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~element(powerset(X0),powerset(relation_composition(relation_composition(sK4_skl,X1),X2)))|~relation(X2)|~relation(X1)|empty(X0))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f1039,f1080])).
% 0.12/0.47 fof(f1209,plain,(
% 0.12/0.47 ![X0,X1]: (~element(powerset(X0),powerset(relation_composition(sK4_skl,X1)))|~relation(X1)|~relation(sK4_skl)|empty(X0))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f371,f1201])).
% 0.12/0.47 fof(f1210,definition,(
% 0.12/0.47 ![X0,X1]: (sQ94_spl <=> (~element(powerset(X0),powerset(relation_composition(sK4_skl,X1)))|~relation(X1)|empty(X0)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1218,plain,(
% 0.12/0.47 sQ94_spl|~sQ12_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1209,f1210,f249])).
% 0.12/0.47 fof(f1224,plain,(
% 0.12/0.47 ![X0]: (~in(X0,sK4_skl))),
% 0.12/0.47 inference(resolution,[status(thm)],[f701,f346])).
% 0.12/0.47 fof(f1249,plain,(
% 0.12/0.47 relation_composition(sK4_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK4_skl,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(sK4_skl,sK10_skl)),relation_composition(sK4_skl,sK10_skl)),relation_dom(relation_composition(sK4_skl,sK10_skl)))|~relation(sK4_skl)|~sQ82_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f1012,f163])).
% 0.12/0.47 fof(f1250,plain,(
% 0.12/0.47 relation_composition(sK1_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK1_skl,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(sK1_skl,sK10_skl)),relation_composition(sK1_skl,sK10_skl)),relation_dom(relation_composition(sK1_skl,sK10_skl)))|~relation(sK1_skl)|~sQ82_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f1012,f75])).
% 0.12/0.47 fof(f1255,plain,(
% 0.12/0.47 relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl)))|in(sK9_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl)))|~relation(sK10_skl)|~sQ82_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f1012,f125])).
% 0.12/0.47 fof(f1256,definition,(
% 0.12/0.47 sQ96_spl <=> (relation_composition(sK4_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK4_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1259,definition,(
% 0.12/0.47 sQ97_spl <=> (in(sK9_skl(relation_dom(relation_composition(sK4_skl,sK10_skl)),relation_composition(sK4_skl,sK10_skl)),relation_dom(relation_composition(sK4_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1262,plain,(
% 0.12/0.47 sQ96_spl|sQ97_spl|~sQ12_spl|~sQ82_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1249,f1256,f1259,f249,f1011])).
% 0.12/0.47 fof(f1263,definition,(
% 0.12/0.47 sQ98_spl <=> (relation_composition(sK1_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK1_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1266,definition,(
% 0.12/0.47 sQ99_spl <=> (in(sK9_skl(relation_dom(relation_composition(sK1_skl,sK10_skl)),relation_composition(sK1_skl,sK10_skl)),relation_dom(relation_composition(sK1_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1269,plain,(
% 0.12/0.47 sQ98_spl|sQ99_spl|~sQ35_spl|~sQ82_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1250,f1263,f1266,f504,f1011])).
% 0.12/0.47 fof(f1272,definition,(
% 0.12/0.47 sQ100_spl <=> (relation_composition(sK10_skl,sK10_skl)=identity_relation(relation_dom(relation_composition(sK10_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1275,definition,(
% 0.12/0.47 sQ101_spl <=> (in(sK9_skl(relation_dom(relation_composition(sK10_skl,sK10_skl)),relation_composition(sK10_skl,sK10_skl)),relation_dom(relation_composition(sK10_skl,sK10_skl))))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1278,plain,(
% 0.12/0.47 sQ100_spl|sQ101_spl|~sQ17_spl|~sQ82_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1255,f1272,f1275,f325,f1011])).
% 0.12/0.47 fof(f1294,plain,(
% 0.12/0.47 sK0_skl(powerset(sK4_skl))=sK4_skl|~sQ86_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f1073,f225])).
% 0.12/0.47 fof(f1300,plain,(
% 0.12/0.47 empty(powerset(sK4_skl))|~in(powerset(sK4_skl),sK4_skl)|~sQ86_spl),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f1294,f738])).
% 0.12/0.47 fof(f1301,plain,(
% 0.12/0.47 empty(powerset(sK4_skl))|in(sK4_skl,powerset(sK4_skl))|~sQ86_spl),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f1294,f272])).
% 0.12/0.47 fof(f1303,definition,(
% 0.12/0.47 sQ102_spl <=> (empty(powerset(sK4_skl)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1304,plain,(
% 0.12/0.47 empty(powerset(sK4_skl))|~sQ102_spl),
% 0.12/0.47 inference(component_clause,[status(thm)],[f1303])).
% 0.12/0.47 fof(f1306,definition,(
% 0.12/0.47 sQ103_spl <=> (in(powerset(sK4_skl),sK4_skl))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1309,plain,(
% 0.12/0.47 sQ102_spl|~sQ103_spl|~sQ86_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1300,f1303,f1306,f1067])).
% 0.12/0.47 fof(f1310,definition,(
% 0.12/0.47 sQ104_spl <=> (in(sK4_skl,powerset(sK4_skl)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1313,plain,(
% 0.12/0.47 sQ102_spl|sQ104_spl|~sQ86_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1301,f1303,f1310,f1067])).
% 0.12/0.47 fof(f1314,plain,(
% 0.12/0.47 $false|~sQ102_spl),
% 0.12/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1304,f58])).
% 0.12/0.47 fof(f1315,plain,(
% 0.12/0.47 ~sQ102_spl),
% 0.12/0.47 inference(contradiction_clause,[status(thm)],[f1314])).
% 0.12/0.47 fof(f1332,plain,(
% 0.12/0.47 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(relation_composition(X0,identity_relation(X2))))|~in(X1,relation_dom(X0))|~in(apply(X0,X1),X2))),
% 0.12/0.47 inference(forward_subsumption_resolution,[status(thm)],[f455,f62])).
% 0.12/0.47 fof(f1354,plain,(
% 0.12/0.47 $false|~sQ44_spl),
% 0.12/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1024,f1224])).
% 0.12/0.47 fof(f1355,plain,(
% 0.12/0.47 ~sQ44_spl),
% 0.12/0.47 inference(contradiction_clause,[status(thm)],[f1354])).
% 0.12/0.47 fof(f1363,plain,(
% 0.12/0.47 ![X0]: (~relation(identity_relation(sK11_skl))|~function(identity_relation(sK11_skl))|in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),identity_relation(X0))))|~in(sK12_skl,relation_dom(identity_relation(sK11_skl)))|~in(sK12_skl,X0)|~sQ53_spl)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f813,f1332])).
% 0.12/0.47 fof(f1365,definition,(
% 0.12/0.47 ![X0]: (sQ106_spl <=> (in(sK12_skl,relation_dom(relation_composition(identity_relation(sK11_skl),identity_relation(X0))))|~in(sK12_skl,X0)))),
% 0.12/0.47 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.12/0.47 fof(f1368,plain,(
% 0.12/0.47 ~sQ15_spl|~sQ16_spl|sQ106_spl|~sQ66_spl|~sQ53_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1363,f319,f322,f1365,f828,f630])).
% 0.12/0.47 fof(f1371,plain,(
% 0.12/0.47 ~relation(sK10_skl)|~function(sK10_skl)|in(sK12_skl,relation_dom(relation_composition(sK10_skl,identity_relation(sK11_skl))))|~in(sK12_skl,relation_dom(sK10_skl))|~sQ2_spl),
% 0.12/0.47 inference(resolution,[status(thm)],[f151,f1332])).
% 0.12/0.47 fof(f1376,plain,(
% 0.12/0.47 ~sQ17_spl|~sQ18_spl|sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.12/0.47 inference(split_clause,[status(thm)],[f1371,f325,f328,f143,f146,f150])).
% 0.12/0.47 fof(f1377,plain,(
% 0.12/0.47 $false),
% 0.12/0.47 inference(sat_refutation,[status(thm)],[f149,f153,f154,f252,f259,f261,f310,f331,f397,f401,f408,f429,f433,f443,f448,f481,f485,f495,f514,f518,f528,f530,f546,f550,f560,f562,f579,f626,f628,f642,f663,f688,f748,f767,f771,f831,f868,f900,f919,f938,f958,f981,f1004,f1008,f1014,f1055,f1070,f1091,f1093,f1115,f1119,f1135,f1142,f1148,f1160,f1174,f1218,f1262,f1269,f1278,f1309,f1313,f1315,f1355,f1368,f1376])).
% 0.12/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.50 % Elapsed time: 0.132415 seconds
% 0.12/0.50 % CPU time: 0.698211 seconds
% 0.12/0.50 % Total memory used: 92.426 MB
% 0.12/0.50 % Net memory used: 91.648 MB
%------------------------------------------------------------------------------