%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET684+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:12:27 PM UTC 2026
% Result : Theorem 0.12s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET684+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:38:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.12/0.50 % Refutation found
% 0.12/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.50 fof(f1,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,binary_relation_type)=> (! [E] :( ilf_type(E,binary_relation_type)=> ( member(ordered_pair(B,C),compose(D,E))<=> (? [F] :( ilf_type(F,set_type)& member(ordered_pair(B,F),D)& member(ordered_pair(F,C),E) ) )) ) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f2,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,set_type)=> (! [F] :( ilf_type(F,relation_type(B,C))=> ( member(ordered_pair(D,E),F)=> ( member(D,B)& member(E,C) ) ) ) )) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f3,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,set_type)=> (! [F] :( ilf_type(F,set_type)=> ( F = ordered_pair(D,E)<=> F = unordered_pair(unordered_pair(D,E),singleton(D)) ) ) )) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f5,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( (! [D] :( ilf_type(D,subset_type(cross_product(B,C)))=> ilf_type(D,relation_type(B,C)) ))& (! [E] :( ilf_type(E,relation_type(B,C))=> ilf_type(E,subset_type(cross_product(B,C))) ) )) ) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f7,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ( ~ empty(C)& ilf_type(C,set_type) )=> ( ilf_type(B,member_type(C))<=> member(B,C) ) ) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f9,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> ( empty(B)<=> (! [C] :( ilf_type(C,set_type)=> ~ member(C,B) ) )) ) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f15,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> ( ilf_type(B,binary_relation_type)<=> ( relation_like(B)& ilf_type(B,set_type) ) ) ) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f26,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,subset_type(cross_product(B,C)))=> relation_like(D) ) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f27,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,relation_type(B,C))=> (! [F] :( ilf_type(F,relation_type(C,D))=> compose5(B,C,D,E,F) = compose(E,F) ) )) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f28,axiom,(
% 0.12/0.50 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,relation_type(B,C))=> (! [F] :( ilf_type(F,relation_type(C,D))=> ilf_type(compose5(B,C,D,E,F),relation_type(B,D)) ) )) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f29,axiom,(
% 0.12/0.50 (! [B] : ilf_type(B,set_type) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f30,conjecture,(
% 0.12/0.50 (! [B] :( ( ~ empty(B)& ilf_type(B,set_type) )=> (! [C] :( ( ~ empty(C)& ilf_type(C,set_type) )=> (! [D] :( ( ~ empty(D)& ilf_type(D,set_type) )=> (! [E] :( ilf_type(E,relation_type(B,C))=> (! [F] :( ilf_type(F,relation_type(C,D))=> (! [G] :( ilf_type(G,member_type(B))=> (! [H] :( ilf_type(H,member_type(D))=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))<=> (? [I] :( ilf_type(I,member_type(C))& member(ordered_pair(G,I),E)& member(ordered_pair(I,H),F) ) )) ) )) )) )) )) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f31,negated_conjecture,(
% 0.12/0.50 ~((! [B] :( ( ~ empty(B)& ilf_type(B,set_type) )=> (! [C] :( ( ~ empty(C)& ilf_type(C,set_type) )=> (! [D] :( ( ~ empty(D)& ilf_type(D,set_type) )=> (! [E] :( ilf_type(E,relation_type(B,C))=> (! [F] :( ilf_type(F,relation_type(C,D))=> (! [G] :( ilf_type(G,member_type(B))=> (! [H] :( ilf_type(H,member_type(D))=> ( member(ordered_pair(G,H),compose5(B,C,D,E,F))<=> (? [I] :( ilf_type(I,member_type(C))& member(ordered_pair(G,I),E)& member(ordered_pair(I,H),F) ) )) ) )) )) )) )) )) )) ))),
% 0.12/0.50 inference(negated_conjecture,[status(cth)],[f30])).
% 0.12/0.50 fof(f32,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,binary_relation_type)|(![E]: (~ilf_type(E,binary_relation_type)|(member(ordered_pair(B,C),compose(D,E))<=>(?[F]: ((ilf_type(F,set_type)&member(ordered_pair(B,F),D))&member(ordered_pair(F,C),E)))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.12/0.50 fof(f33,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,binary_relation_type)|(![E]: (~ilf_type(E,binary_relation_type)|((~member(ordered_pair(B,C),compose(D,E))|(?[F]: ((ilf_type(F,set_type)&member(ordered_pair(B,F),D))&member(ordered_pair(F,C),E))))&(member(ordered_pair(B,C),compose(D,E))|(![F]: ((~ilf_type(F,set_type)|~member(ordered_pair(B,F),D))|~member(ordered_pair(F,C),E))))))))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f32])).
% 0.12/0.50 fof(f34,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,binary_relation_type)|(![E]: (~ilf_type(E,binary_relation_type)|((~member(ordered_pair(B,C),compose(D,E))|((ilf_type(sK0_skl(E,D,C,B),set_type)&member(ordered_pair(B,sK0_skl(E,D,C,B)),D))&member(ordered_pair(sK0_skl(E,D,C,B),C),E)))&(member(ordered_pair(B,C),compose(D,E))|(![F]: ((~ilf_type(F,set_type)|~member(ordered_pair(B,F),D))|~member(ordered_pair(F,C),E))))))))))))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(F,sK0_skl(E,D,C,B))],[f33])).
% 0.12/0.50 fof(f36,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~ilf_type(X3,binary_relation_type)|~member(ordered_pair(X0,X1),compose(X2,X3))|member(ordered_pair(X0,sK0_skl(X3,X2,X1,X0)),X2))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.50 fof(f37,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~ilf_type(X3,binary_relation_type)|~member(ordered_pair(X0,X1),compose(X2,X3))|member(ordered_pair(sK0_skl(X3,X2,X1,X0),X1),X3))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.50 fof(f38,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~ilf_type(X3,binary_relation_type)|member(ordered_pair(X0,X1),compose(X2,X3))|~ilf_type(X4,set_type)|~member(ordered_pair(X0,X4),X2)|~member(ordered_pair(X4,X1),X3))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.50 fof(f39,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(![F]: (~ilf_type(F,relation_type(B,C))|(~member(ordered_pair(D,E),F)|(member(D,B)&member(E,C))))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.50 fof(f40,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|~ilf_type(X4,relation_type(X0,X1))|~member(ordered_pair(X2,X3),X4)|member(X2,X0))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.50 fof(f42,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(![F]: (~ilf_type(F,set_type)|(F=ordered_pair(D,E)<=>F=unordered_pair(unordered_pair(D,E),singleton(D))))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.12/0.50 fof(f43,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(![F]: (~ilf_type(F,set_type)|((~F=ordered_pair(D,E)|F=unordered_pair(unordered_pair(D,E),singleton(D)))&(F=ordered_pair(D,E)|~F=unordered_pair(unordered_pair(D,E),singleton(D)))))))))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f42])).
% 0.12/0.50 fof(f44,plain,(
% 0.12/0.50 (![B]: ~ilf_type(B,set_type))|((![C]: ~ilf_type(C,set_type))|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(![F]: (~ilf_type(F,set_type)|((~F=ordered_pair(D,E)|F=unordered_pair(unordered_pair(D,E),singleton(D)))&(F=ordered_pair(D,E)|~F=unordered_pair(unordered_pair(D,E),singleton(D)))))))))))),
% 0.12/0.50 inference(miniscoping,[status(thm)],[f43])).
% 0.12/0.50 fof(f45,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|~ilf_type(X4,set_type)|~X4=ordered_pair(X2,X3)|X4=unordered_pair(unordered_pair(X2,X3),singleton(X2)))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.50 fof(f46,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|~ilf_type(X4,set_type)|X4=ordered_pair(X2,X3)|~X4=unordered_pair(unordered_pair(X2,X3),singleton(X2)))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.50 fof(f49,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((![D]: (~ilf_type(D,subset_type(cross_product(B,C)))|ilf_type(D,relation_type(B,C))))&(![E]: (~ilf_type(E,relation_type(B,C))|ilf_type(E,subset_type(cross_product(B,C)))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.12/0.50 fof(f51,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|ilf_type(X2,subset_type(cross_product(X0,X1))))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.50 fof(f55,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: ((empty(C)|~ilf_type(C,set_type))|(ilf_type(B,member_type(C))<=>member(B,C)))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.50 fof(f56,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: ((empty(C)|~ilf_type(C,set_type))|((~ilf_type(B,member_type(C))|member(B,C))&(ilf_type(B,member_type(C))|~member(B,C))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f55])).
% 0.12/0.50 fof(f57,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|empty(X1)|~ilf_type(X1,set_type)|~ilf_type(X0,member_type(X1))|member(X0,X1))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.50 fof(f58,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|empty(X1)|~ilf_type(X1,set_type)|ilf_type(X0,member_type(X1))|~member(X0,X1))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.50 fof(f62,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(empty(B)<=>(![C]: (~ilf_type(C,set_type)|~member(C,B)))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.12/0.50 fof(f63,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|((~empty(B)|(![C]: (~ilf_type(C,set_type)|~member(C,B))))&(empty(B)|(?[C]: (ilf_type(C,set_type)&member(C,B))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f62])).
% 0.12/0.50 fof(f64,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|((~empty(B)|(![C]: (~ilf_type(C,set_type)|~member(C,B))))&(empty(B)|(ilf_type(sK3_skl(B),set_type)&member(sK3_skl(B),B)))))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B))],[f63])).
% 0.12/0.50 fof(f65,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|~empty(X0)|~ilf_type(X1,set_type)|~member(X1,X0))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f64])).
% 0.12/0.50 fof(f78,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.12/0.50 fof(f79,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|((~ilf_type(B,binary_relation_type)|(relation_like(B)&ilf_type(B,set_type)))&(ilf_type(B,binary_relation_type)|(~relation_like(B)|~ilf_type(B,set_type)))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f78])).
% 0.12/0.50 fof(f82,plain,(
% 0.12/0.50 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0)|~ilf_type(X0,set_type))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f79])).
% 0.12/0.50 fof(f125,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,subset_type(cross_product(B,C)))|relation_like(D))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.12/0.50 fof(f126,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,subset_type(cross_product(X0,X1)))|relation_like(X2))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f125])).
% 0.12/0.50 fof(f127,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,relation_type(B,C))|(![F]: (~ilf_type(F,relation_type(C,D))|compose5(B,C,D,E,F)=compose(E,F))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.12/0.50 fof(f128,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X0,X1))|~ilf_type(X4,relation_type(X1,X2))|compose5(X0,X1,X2,X3,X4)=compose(X3,X4))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/0.50 fof(f129,plain,(
% 0.12/0.50 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,relation_type(B,C))|(![F]: (~ilf_type(F,relation_type(C,D))|ilf_type(compose5(B,C,D,E,F),relation_type(B,D)))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.12/0.50 fof(f130,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X0,X1))|~ilf_type(X4,relation_type(X1,X2))|ilf_type(compose5(X0,X1,X2,X3,X4),relation_type(X0,X2)))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f129])).
% 0.12/0.50 fof(f131,plain,(
% 0.12/0.50 ![X0]: (ilf_type(X0,set_type))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f29])).
% 0.12/0.50 fof(f132,plain,(
% 0.12/0.50 (?[B]: ((~empty(B)&ilf_type(B,set_type))&(?[C]: ((~empty(C)&ilf_type(C,set_type))&(?[D]: ((~empty(D)&ilf_type(D,set_type))&(?[E]: (ilf_type(E,relation_type(B,C))&(?[F]: (ilf_type(F,relation_type(C,D))&(?[G]: (ilf_type(G,member_type(B))&(?[H]: (ilf_type(H,member_type(D))&(member(ordered_pair(G,H),compose5(B,C,D,E,F))<~>(?[I]: ((ilf_type(I,member_type(C))&member(ordered_pair(G,I),E))&member(ordered_pair(I,H),F))))))))))))))))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.12/0.50 fof(f133,plain,(
% 0.12/0.50 ?[B]: ((~empty(B)&ilf_type(B,set_type))&(?[C]: ((~empty(C)&ilf_type(C,set_type))&(?[D]: ((~empty(D)&ilf_type(D,set_type))&(?[E]: (ilf_type(E,relation_type(B,C))&(?[F]: (ilf_type(F,relation_type(C,D))&(?[G]: (ilf_type(G,member_type(B))&(?[H]: (ilf_type(H,member_type(D))&((member(ordered_pair(G,H),compose5(B,C,D,E,F))|(?[I]: ((ilf_type(I,member_type(C))&member(ordered_pair(G,I),E))&member(ordered_pair(I,H),F))))&(~member(ordered_pair(G,H),compose5(B,C,D,E,F))|(![I]: ((~ilf_type(I,member_type(C))|~member(ordered_pair(G,I),E))|~member(ordered_pair(I,H),F))))))))))))))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f132])).
% 0.12/0.50 fof(f134,plain,(
% 0.12/0.50 ((~empty(sK11_skl)&ilf_type(sK11_skl,set_type))&((~empty(sK12_skl)&ilf_type(sK12_skl,set_type))&((~empty(sK13_skl)&ilf_type(sK13_skl,set_type))&(ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))&(ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))&(ilf_type(sK16_skl,member_type(sK11_skl))&(ilf_type(sK17_skl,member_type(sK13_skl))&((member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|((ilf_type(sK18_skl,member_type(sK12_skl))&member(ordered_pair(sK16_skl,sK18_skl),sK14_skl))&member(ordered_pair(sK18_skl,sK17_skl),sK15_skl)))&(~member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|(![I]: ((~ilf_type(I,member_type(sK12_skl))|~member(ordered_pair(sK16_skl,I),sK14_skl))|~member(ordered_pair(I,sK17_skl),sK15_skl))))))))))))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(B,sK11_skl),skolemize(C,sK12_skl),skolemize(D,sK13_skl),skolemize(E,sK14_skl),skolemize(F,sK15_skl),skolemize(G,sK16_skl),skolemize(H,sK17_skl),skolemize(I,sK18_skl)],[f133])).
% 0.12/0.50 fof(f135,plain,(
% 0.12/0.50 ~empty(sK11_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f137,plain,(
% 0.12/0.50 ~empty(sK12_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f139,plain,(
% 0.12/0.50 ~empty(sK13_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f141,plain,(
% 0.12/0.50 ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f142,plain,(
% 0.12/0.50 ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f143,plain,(
% 0.12/0.50 ilf_type(sK16_skl,member_type(sK11_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f144,plain,(
% 0.12/0.50 ilf_type(sK17_skl,member_type(sK13_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f145,plain,(
% 0.12/0.50 member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|ilf_type(sK18_skl,member_type(sK12_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f146,plain,(
% 0.12/0.50 member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|member(ordered_pair(sK16_skl,sK18_skl),sK14_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f147,plain,(
% 0.12/0.50 member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|member(ordered_pair(sK18_skl,sK17_skl),sK15_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f148,plain,(
% 0.12/0.50 ![X0]: (~member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|~ilf_type(X0,member_type(sK12_skl))|~member(ordered_pair(sK16_skl,X0),sK14_skl)|~member(ordered_pair(X0,sK17_skl),sK15_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f134])).
% 0.12/0.50 fof(f149,definition,(
% 0.12/0.50 ![X0]: (sQ0_spl <=> (~ilf_type(X0,set_type)))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f150,plain,(
% 0.12/0.50 ![X0]: (~ilf_type(X0,set_type)|~sQ0_spl)),
% 0.12/0.50 inference(component_clause,[status(thm)],[f149])).
% 0.12/0.50 fof(f152,definition,(
% 0.12/0.50 ![X2,X3,X4]: (sQ1_spl <=> (~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|~ilf_type(X4,set_type)|~X4=ordered_pair(X2,X3)|X4=unordered_pair(unordered_pair(X2,X3),singleton(X2))))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f155,plain,(
% 0.12/0.50 sQ0_spl|sQ1_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f45,f149,f152])).
% 0.12/0.50 fof(f156,definition,(
% 0.12/0.50 ![X2,X3,X4]: (sQ2_spl <=> (~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|~ilf_type(X4,set_type)|X4=ordered_pair(X2,X3)|~X4=unordered_pair(unordered_pair(X2,X3),singleton(X2))))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f159,plain,(
% 0.12/0.50 sQ0_spl|sQ2_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f46,f149,f156])).
% 0.12/0.50 fof(f160,definition,(
% 0.12/0.50 sQ3_spl <=> (member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f161,plain,(
% 0.12/0.50 member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|~sQ3_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f160])).
% 0.12/0.50 fof(f162,plain,(
% 0.12/0.50 ~member(ordered_pair(sK16_skl,sK17_skl),compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl))|sQ3_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f160])).
% 0.12/0.50 fof(f163,definition,(
% 0.12/0.50 sQ4_spl <=> (ilf_type(sK18_skl,member_type(sK12_skl)))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f164,plain,(
% 0.12/0.50 ilf_type(sK18_skl,member_type(sK12_skl))|~sQ4_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f163])).
% 0.12/0.50 fof(f165,plain,(
% 0.12/0.50 ~ilf_type(sK18_skl,member_type(sK12_skl))|sQ4_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f163])).
% 0.12/0.50 fof(f166,plain,(
% 0.12/0.50 sQ3_spl|sQ4_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f145,f160,f163])).
% 0.12/0.50 fof(f167,definition,(
% 0.12/0.50 sQ5_spl <=> (member(ordered_pair(sK16_skl,sK18_skl),sK14_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f168,plain,(
% 0.12/0.50 member(ordered_pair(sK16_skl,sK18_skl),sK14_skl)|~sQ5_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f167])).
% 0.12/0.50 fof(f170,plain,(
% 0.12/0.50 sQ3_spl|sQ5_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f146,f160,f167])).
% 0.12/0.50 fof(f171,definition,(
% 0.12/0.50 sQ6_spl <=> (member(ordered_pair(sK18_skl,sK17_skl),sK15_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f172,plain,(
% 0.12/0.50 member(ordered_pair(sK18_skl,sK17_skl),sK15_skl)|~sQ6_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f171])).
% 0.12/0.50 fof(f174,plain,(
% 0.12/0.50 sQ3_spl|sQ6_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f147,f160,f171])).
% 0.12/0.50 fof(f175,definition,(
% 0.12/0.50 ![X0]: (sQ7_spl <=> (~ilf_type(X0,member_type(sK12_skl))|~member(ordered_pair(sK16_skl,X0),sK14_skl)|~member(ordered_pair(X0,sK17_skl),sK15_skl)))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f176,plain,(
% 0.12/0.50 ![X0]: (~ilf_type(X0,member_type(sK12_skl))|~member(ordered_pair(sK16_skl,X0),sK14_skl)|~member(ordered_pair(X0,sK17_skl),sK15_skl)|~sQ7_spl)),
% 0.12/0.50 inference(component_clause,[status(thm)],[f175])).
% 0.12/0.50 fof(f178,plain,(
% 0.12/0.50 ~sQ3_spl|sQ7_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f148,f160,f175])).
% 0.12/0.50 fof(f179,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|ilf_type(X0,member_type(X1))|~member(X0,X1))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f58,f65])).
% 0.12/0.50 fof(f180,plain,(
% 0.12/0.50 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.12/0.50 inference(duplicate_literals_removal,[status(thm)],[f82])).
% 0.12/0.50 fof(f181,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|~ilf_type(X3,relation_type(X1,X4))|ilf_type(compose5(X0,X1,X4,X2,X3),relation_type(X0,X4)))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f130,f131])).
% 0.12/0.50 fof(f182,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|~ilf_type(X3,relation_type(X1,X4))|compose5(X0,X1,X4,X2,X3)=compose(X2,X3))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f128,f131])).
% 0.12/0.50 fof(f183,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X0,X2)))|relation_like(X1))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f126,f131])).
% 0.12/0.50 fof(f197,plain,(
% 0.12/0.50 ![X0]: (ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f180,f131])).
% 0.12/0.50 fof(f203,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|empty(X1)|~ilf_type(X0,member_type(X1))|member(X0,X1))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f57,f131])).
% 0.12/0.50 fof(f205,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|ilf_type(X1,subset_type(cross_product(X0,X2))))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f51,f131])).
% 0.12/0.50 fof(f208,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,relation_type(X0,X1))|~member(ordered_pair(X2,X4),X3)|member(X2,X0))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f40,f131])).
% 0.12/0.50 fof(f209,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~ilf_type(X3,binary_relation_type)|member(ordered_pair(X0,X1),compose(X2,X3))|~member(ordered_pair(X0,X4),X2)|~member(ordered_pair(X4,X1),X3))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f38,f131])).
% 0.12/0.50 fof(f210,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~ilf_type(X2,binary_relation_type)|~member(ordered_pair(X0,X3),compose(X1,X2))|member(ordered_pair(sK0_skl(X2,X1,X3,X0),X3),X2))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f37,f131])).
% 0.12/0.50 fof(f211,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~ilf_type(X2,binary_relation_type)|~member(ordered_pair(X0,X3),compose(X1,X2))|member(ordered_pair(X0,sK0_skl(X2,X1,X3,X0)),X1))),
% 0.12/0.50 inference(backward_subsumption_resolution,[status(thm)],[f36,f131])).
% 0.12/0.50 fof(f212,plain,(
% 0.12/0.50 $false|~sQ0_spl),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f150,f131])).
% 0.12/0.50 fof(f213,plain,(
% 0.12/0.50 ~sQ0_spl),
% 0.12/0.50 inference(contradiction_clause,[status(thm)],[f212])).
% 0.12/0.50 fof(f214,plain,(
% 0.12/0.50 ![X0,X1]: (~ilf_type(X0,set_type)|ilf_type(X1,member_type(X0))|~member(X1,X0))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f179,f131])).
% 0.12/0.50 fof(f215,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X2,X0))|~ilf_type(X3,relation_type(X0,X4))|ilf_type(compose5(X2,X0,X4,X1,X3),relation_type(X2,X4)))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f181,f131])).
% 0.12/0.50 fof(f216,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X2,X0))|~ilf_type(X3,relation_type(X0,X4))|compose5(X2,X0,X4,X1,X3)=compose(X1,X3))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f182,f131])).
% 0.12/0.50 fof(f217,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,subset_type(cross_product(X1,X2)))|relation_like(X0))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f183,f131])).
% 0.12/0.50 fof(f229,plain,(
% 0.12/0.50 ![X0,X1]: (empty(X0)|~ilf_type(X1,member_type(X0))|member(X1,X0))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f203,f131])).
% 0.12/0.50 fof(f231,plain,(
% 0.12/0.50 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|ilf_type(X0,subset_type(cross_product(X1,X2))))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f205,f131])).
% 0.12/0.50 fof(f234,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X3,X0))|~member(ordered_pair(X1,X4),X2)|member(X1,X3))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f208,f131])).
% 0.12/0.50 fof(f235,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~ilf_type(X2,binary_relation_type)|member(ordered_pair(X3,X0),compose(X1,X2))|~member(ordered_pair(X3,X4),X1)|~member(ordered_pair(X4,X0),X2))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f209,f131])).
% 0.12/0.50 fof(f236,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,binary_relation_type)|~ilf_type(X1,binary_relation_type)|~member(ordered_pair(X2,X3),compose(X0,X1))|member(ordered_pair(sK0_skl(X1,X0,X3,X2),X3),X1))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f210,f131])).
% 0.12/0.50 fof(f237,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (~ilf_type(X0,binary_relation_type)|~ilf_type(X1,binary_relation_type)|~member(ordered_pair(X2,X3),compose(X0,X1))|member(ordered_pair(X2,sK0_skl(X1,X0,X3,X2)),X0))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f211,f131])).
% 0.12/0.50 fof(f242,plain,(
% 0.12/0.50 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,relation_type(X1,X2))|~ilf_type(X3,relation_type(X2,X4))|compose5(X1,X2,X4,X0,X3)=compose(X0,X3))),
% 0.12/0.50 inference(resolution,[status(thm)],[f216,f131])).
% 0.12/0.50 fof(f244,plain,(
% 0.12/0.50 empty(sK13_skl)|member(sK17_skl,sK13_skl)),
% 0.12/0.50 inference(resolution,[status(thm)],[f229,f144])).
% 0.12/0.50 fof(f245,plain,(
% 0.12/0.50 empty(sK11_skl)|member(sK16_skl,sK11_skl)),
% 0.12/0.50 inference(resolution,[status(thm)],[f229,f143])).
% 0.12/0.50 fof(f248,definition,(
% 0.12/0.50 sQ8_spl <=> (empty(sK13_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f249,plain,(
% 0.12/0.50 empty(sK13_skl)|~sQ8_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f248])).
% 0.12/0.50 fof(f251,definition,(
% 0.12/0.50 sQ9_spl <=> (member(sK17_skl,sK13_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f254,plain,(
% 0.12/0.50 sQ8_spl|sQ9_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f244,f248,f251])).
% 0.12/0.50 fof(f255,definition,(
% 0.12/0.50 sQ10_spl <=> (empty(sK11_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f256,plain,(
% 0.12/0.50 empty(sK11_skl)|~sQ10_spl),
% 0.12/0.50 inference(component_clause,[status(thm)],[f255])).
% 0.12/0.50 fof(f258,definition,(
% 0.12/0.50 sQ11_spl <=> (member(sK16_skl,sK11_skl))),
% 0.12/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.50 fof(f261,plain,(
% 0.12/0.50 sQ10_spl|sQ11_spl),
% 0.12/0.50 inference(split_clause,[status(thm)],[f245,f255,f258])).
% 0.12/0.51 fof(f262,plain,(
% 0.12/0.51 $false|~sQ10_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f256,f135])).
% 0.12/0.51 fof(f263,plain,(
% 0.12/0.51 ~sQ10_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f262])).
% 0.12/0.51 fof(f264,plain,(
% 0.12/0.51 $false|~sQ8_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f249,f139])).
% 0.12/0.51 fof(f265,plain,(
% 0.12/0.51 ~sQ8_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f264])).
% 0.12/0.51 fof(f272,plain,(
% 0.12/0.51 ![X0,X1]: (~ilf_type(X0,relation_type(X1,sK12_skl))|compose5(X1,sK12_skl,sK13_skl,X0,sK15_skl)=compose(X0,sK15_skl))),
% 0.12/0.51 inference(resolution,[status(thm)],[f242,f142])).
% 0.12/0.51 fof(f288,plain,(
% 0.12/0.51 compose5(sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl)=compose(sK14_skl,sK15_skl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f272,f141])).
% 0.12/0.51 fof(f290,plain,(
% 0.12/0.51 member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl))|~sQ3_spl),
% 0.12/0.51 inference(backward_demodulation,[status(thm)],[f288,f161])).
% 0.12/0.51 fof(f303,plain,(
% 0.12/0.51 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X2,X0))|~member(ordered_pair(X3,X4),X1)|member(X3,X2))),
% 0.12/0.51 inference(resolution,[status(thm)],[f234,f131])).
% 0.12/0.51 fof(f304,plain,(
% 0.12/0.51 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,relation_type(X1,X2))|~member(ordered_pair(X3,X4),X0)|member(X3,X1))),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f303,f131])).
% 0.12/0.51 fof(f309,plain,(
% 0.12/0.51 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|relation_like(X0))),
% 0.12/0.51 inference(resolution,[status(thm)],[f231,f217])).
% 0.12/0.51 fof(f313,plain,(
% 0.12/0.51 ![X0,X1,X2,X3,X4]: (~ilf_type(X0,binary_relation_type)|~ilf_type(X1,binary_relation_type)|member(ordered_pair(X2,X3),compose(X0,X1))|~member(ordered_pair(X2,X4),X0)|~member(ordered_pair(X4,X3),X1))),
% 0.12/0.51 inference(resolution,[status(thm)],[f235,f131])).
% 0.12/0.51 fof(f314,plain,(
% 0.12/0.51 ~ilf_type(sK14_skl,binary_relation_type)|~ilf_type(sK15_skl,binary_relation_type)|member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl)|~sQ3_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f236,f290])).
% 0.12/0.51 fof(f315,definition,(
% 0.12/0.51 sQ12_spl <=> (ilf_type(sK14_skl,binary_relation_type))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f317,plain,(
% 0.12/0.51 ~ilf_type(sK14_skl,binary_relation_type)|sQ12_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f315])).
% 0.12/0.51 fof(f318,definition,(
% 0.12/0.51 sQ13_spl <=> (ilf_type(sK15_skl,binary_relation_type))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f320,plain,(
% 0.12/0.51 ~ilf_type(sK15_skl,binary_relation_type)|sQ13_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f318])).
% 0.12/0.51 fof(f321,definition,(
% 0.12/0.51 sQ14_spl <=> (member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f322,plain,(
% 0.12/0.51 member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl)|~sQ14_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f321])).
% 0.12/0.51 fof(f324,plain,(
% 0.12/0.51 ~sQ12_spl|~sQ13_spl|sQ14_spl|~sQ3_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f314,f315,f318,f321,f160])).
% 0.12/0.51 fof(f325,plain,(
% 0.12/0.51 ~ilf_type(sK14_skl,binary_relation_type)|~ilf_type(sK15_skl,binary_relation_type)|member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl)|~sQ3_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f237,f290])).
% 0.12/0.51 fof(f326,definition,(
% 0.12/0.51 sQ15_spl <=> (member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f327,plain,(
% 0.12/0.51 member(ordered_pair(sK16_skl,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),sK14_skl)|~sQ15_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f326])).
% 0.12/0.51 fof(f329,plain,(
% 0.12/0.51 ~sQ12_spl|~sQ13_spl|sQ15_spl|~sQ3_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f325,f315,f318,f326,f160])).
% 0.12/0.51 fof(f340,plain,(
% 0.12/0.51 ~ilf_type(sK12_skl,set_type)|~member(sK18_skl,sK12_skl)|sQ4_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f165,f214])).
% 0.12/0.51 fof(f341,definition,(
% 0.12/0.51 sQ16_spl <=> (ilf_type(sK12_skl,set_type))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f343,plain,(
% 0.12/0.51 ~ilf_type(sK12_skl,set_type)|sQ16_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f341])).
% 0.12/0.51 fof(f344,definition,(
% 0.12/0.51 sQ17_spl <=> (member(sK18_skl,sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f347,plain,(
% 0.12/0.51 ~sQ16_spl|~sQ17_spl|sQ4_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f340,f341,f344,f163])).
% 0.12/0.51 fof(f349,plain,(
% 0.12/0.51 ![X0,X1,X2,X3,X4]: (relation_like(compose5(X0,X1,X2,X3,X4))|~ilf_type(X1,set_type)|~ilf_type(X3,relation_type(X0,X1))|~ilf_type(X4,relation_type(X1,X2)))),
% 0.12/0.51 inference(resolution,[status(thm)],[f309,f215])).
% 0.12/0.51 fof(f350,plain,(
% 0.12/0.51 relation_like(sK15_skl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f309,f142])).
% 0.12/0.51 fof(f351,plain,(
% 0.12/0.51 relation_like(sK14_skl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f309,f141])).
% 0.12/0.51 fof(f352,plain,(
% 0.12/0.51 ![X0,X1,X2,X3,X4]: (relation_like(compose5(X0,X1,X2,X3,X4))|~ilf_type(X3,relation_type(X0,X1))|~ilf_type(X4,relation_type(X1,X2)))),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f349,f131])).
% 0.12/0.51 fof(f358,plain,(
% 0.12/0.51 empty(sK12_skl)|member(sK18_skl,sK12_skl)|~sQ4_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f164,f229])).
% 0.12/0.51 fof(f359,definition,(
% 0.12/0.51 sQ18_spl <=> (empty(sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f360,plain,(
% 0.12/0.51 empty(sK12_skl)|~sQ18_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f359])).
% 0.12/0.51 fof(f362,plain,(
% 0.12/0.51 sQ18_spl|sQ17_spl|~sQ4_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f358,f359,f344,f163])).
% 0.12/0.51 fof(f363,plain,(
% 0.12/0.51 $false|~sQ18_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f360,f137])).
% 0.12/0.51 fof(f364,plain,(
% 0.12/0.51 ~sQ18_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f363])).
% 0.12/0.51 fof(f365,plain,(
% 0.12/0.51 $false|sQ16_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f343,f131])).
% 0.12/0.51 fof(f366,plain,(
% 0.12/0.51 sQ16_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f365])).
% 0.12/0.51 fof(f398,plain,(
% 0.12/0.51 ~relation_like(sK15_skl)|sQ13_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f320,f197])).
% 0.12/0.51 fof(f399,plain,(
% 0.12/0.51 $false|sQ13_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f398,f350])).
% 0.12/0.51 fof(f400,plain,(
% 0.12/0.51 sQ13_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f399])).
% 0.12/0.51 fof(f401,plain,(
% 0.12/0.51 ~relation_like(sK14_skl)|sQ12_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f317,f197])).
% 0.12/0.51 fof(f402,plain,(
% 0.12/0.51 $false|sQ12_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f401,f351])).
% 0.12/0.51 fof(f403,plain,(
% 0.12/0.51 sQ12_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f402])).
% 0.12/0.51 fof(f434,plain,(
% 0.12/0.51 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|~ilf_type(sK15_skl,binary_relation_type)|member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))|~member(ordered_pair(X1,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),X0)|~sQ14_spl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f322,f313])).
% 0.12/0.51 fof(f435,plain,(
% 0.12/0.51 ![X0,X1]: (~ilf_type(sK15_skl,relation_type(X0,X1))|member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),X0)|~sQ14_spl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f322,f304])).
% 0.12/0.51 fof(f437,definition,(
% 0.12/0.51 ![X0,X1]: (sQ21_spl <=> (~ilf_type(X0,binary_relation_type)|member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))|~member(ordered_pair(X1,sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl)),X0)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f440,plain,(
% 0.12/0.51 sQ21_spl|~sQ13_spl|~sQ14_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f434,f437,f318,f321])).
% 0.12/0.51 fof(f441,plain,(
% 0.12/0.51 ~member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl))|sQ3_spl),
% 0.12/0.51 inference(forward_demodulation,[status(thm)],[f288,f162])).
% 0.12/0.51 fof(f449,plain,(
% 0.12/0.51 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|~ilf_type(sK15_skl,binary_relation_type)|member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))|~member(ordered_pair(X1,sK18_skl),X0)|~sQ6_spl)),
% 0.12/0.51 inference(resolution,[status(thm)],[f172,f313])).
% 0.12/0.51 fof(f452,definition,(
% 0.12/0.51 ![X0,X1]: (sQ23_spl <=> (~ilf_type(X0,binary_relation_type)|member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))|~member(ordered_pair(X1,sK18_skl),X0)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f453,plain,(
% 0.12/0.51 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|member(ordered_pair(X1,sK17_skl),compose(X0,sK15_skl))|~member(ordered_pair(X1,sK18_skl),X0)|~sQ23_spl)),
% 0.12/0.51 inference(component_clause,[status(thm)],[f452])).
% 0.12/0.51 fof(f455,plain,(
% 0.12/0.51 sQ23_spl|~sQ13_spl|~sQ6_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f449,f452,f318,f171])).
% 0.12/0.51 fof(f548,plain,(
% 0.12/0.51 relation_like(compose(sK14_skl,sK15_skl))|~ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))|~ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))),
% 0.12/0.51 inference(paramodulation,[status(thm)],[f288,f352])).
% 0.12/0.51 fof(f549,plain,(
% 0.12/0.51 ~ilf_type(sK12_skl,set_type)|~ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))|~ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))|ilf_type(compose(sK14_skl,sK15_skl),relation_type(sK11_skl,sK13_skl))),
% 0.12/0.51 inference(paramodulation,[status(thm)],[f288,f215])).
% 0.12/0.51 fof(f550,definition,(
% 0.12/0.51 sQ24_spl <=> (relation_like(compose(sK14_skl,sK15_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f553,definition,(
% 0.12/0.51 sQ25_spl <=> (ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f555,plain,(
% 0.12/0.51 ~ilf_type(sK14_skl,relation_type(sK11_skl,sK12_skl))|sQ25_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f553])).
% 0.12/0.51 fof(f556,definition,(
% 0.12/0.51 sQ26_spl <=> (ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f558,plain,(
% 0.12/0.51 ~ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))|sQ26_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f556])).
% 0.12/0.51 fof(f559,plain,(
% 0.12/0.51 sQ24_spl|~sQ25_spl|~sQ26_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f548,f550,f553,f556])).
% 0.12/0.51 fof(f560,definition,(
% 0.12/0.51 sQ27_spl <=> (ilf_type(compose(sK14_skl,sK15_skl),relation_type(sK11_skl,sK13_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f563,plain,(
% 0.12/0.51 ~sQ16_spl|~sQ25_spl|~sQ26_spl|sQ27_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f549,f341,f553,f556,f560])).
% 0.12/0.51 fof(f564,plain,(
% 0.12/0.51 $false|sQ26_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f558,f142])).
% 0.12/0.51 fof(f565,plain,(
% 0.12/0.51 sQ26_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f564])).
% 0.12/0.51 fof(f566,plain,(
% 0.12/0.51 $false|sQ25_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f555,f141])).
% 0.12/0.51 fof(f567,plain,(
% 0.12/0.51 sQ25_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f566])).
% 0.12/0.51 fof(f569,plain,(
% 0.12/0.51 ~ilf_type(sK14_skl,binary_relation_type)|member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl))|~sQ23_spl|~sQ5_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f453,f168])).
% 0.12/0.51 fof(f571,definition,(
% 0.12/0.51 sQ28_spl <=> (member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f572,plain,(
% 0.12/0.51 member(ordered_pair(sK16_skl,sK17_skl),compose(sK14_skl,sK15_skl))|~sQ28_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f571])).
% 0.12/0.51 fof(f574,plain,(
% 0.12/0.51 ~sQ12_spl|sQ28_spl|~sQ23_spl|~sQ5_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f569,f315,f571,f452,f167])).
% 0.12/0.51 fof(f575,plain,(
% 0.12/0.51 $false|sQ3_spl|~sQ28_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f572,f441])).
% 0.12/0.51 fof(f576,plain,(
% 0.12/0.51 sQ3_spl|~sQ28_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f575])).
% 0.12/0.51 fof(f585,plain,(
% 0.12/0.51 ~ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl))|~member(ordered_pair(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK17_skl),sK15_skl)|~sQ15_spl|~sQ7_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f327,f176])).
% 0.12/0.51 fof(f590,definition,(
% 0.12/0.51 sQ29_spl <=> (ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f592,plain,(
% 0.12/0.51 ~ilf_type(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),member_type(sK12_skl))|sQ29_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f590])).
% 0.12/0.51 fof(f593,plain,(
% 0.12/0.51 ~sQ29_spl|~sQ14_spl|~sQ15_spl|~sQ7_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f585,f590,f321,f326,f175])).
% 0.12/0.51 fof(f644,plain,(
% 0.12/0.51 member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl)|~sQ14_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f435,f142])).
% 0.12/0.51 fof(f764,plain,(
% 0.12/0.51 ~ilf_type(sK12_skl,set_type)|~member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl)|sQ29_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f592,f214])).
% 0.12/0.51 fof(f765,definition,(
% 0.12/0.51 sQ38_spl <=> (member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f767,plain,(
% 0.12/0.51 ~member(sK0_skl(sK15_skl,sK14_skl,sK17_skl,sK16_skl),sK12_skl)|sQ38_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f765])).
% 0.12/0.51 fof(f768,plain,(
% 0.12/0.51 ~sQ16_spl|~sQ38_spl|sQ29_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f764,f341,f765,f590])).
% 0.12/0.51 fof(f769,plain,(
% 0.12/0.51 $false|~sQ14_spl|sQ38_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f767,f644])).
% 0.12/0.51 fof(f770,plain,(
% 0.12/0.52 ~sQ14_spl|sQ38_spl),
% 0.12/0.52 inference(contradiction_clause,[status(thm)],[f769])).
% 0.12/0.52 fof(f771,plain,(
% 0.12/0.52 $false),
% 0.12/0.52 inference(sat_refutation,[status(thm)],[f155,f159,f166,f170,f174,f178,f213,f254,f261,f263,f265,f324,f329,f347,f362,f364,f366,f400,f403,f440,f455,f559,f563,f565,f567,f574,f576,f593,f768,f770])).
% 0.12/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.54 % Elapsed time: 0.167549 seconds
% 0.23/0.54 % CPU time: 0.964627 seconds
% 0.23/0.54 % Total memory used: 104.975 MB
% 0.23/0.54 % Net memory used: 103.974 MB
%------------------------------------------------------------------------------