%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU042+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 : n005.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:36 PM UTC 2026
% Result : Theorem 66.76s 8.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU042+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 : n005.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:47:32 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 66.76/8.82 % Refutation found
% 66.76/8.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.76/8.82 % SZS output start CNFRefutation for theBenchmark
% 66.76/8.82 fof(f5,axiom,(
% 66.76/8.82 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f6,axiom,(
% 66.76/8.82 (! [A,B,C] :( C = set_intersection2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& in(D,B) ) ) )) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f7,axiom,(
% 66.76/8.82 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)<=> (! [B,C] :( ( in(B,relation_dom(A))& in(C,relation_dom(A))& apply(A,B) = apply(A,C) )=> B = C ) )) ) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f8,axiom,(
% 66.76/8.82 (! [A,B] :( relation(A)=> relation(relation_dom_restriction(A,B)) ) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f15,axiom,(
% 66.76/8.82 (! [A,B] :( ( relation(A)& function(A) )=> ( relation(relation_dom_restriction(A,B))& function(relation_dom_restriction(A,B)) ) ) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f37,axiom,(
% 66.76/8.82 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( B = relation_dom_restriction(C,A)<=> ( relation_dom(B) = set_intersection2(relation_dom(C),A)& (! [D] :( in(D,relation_dom(B))=> apply(B,D) = apply(C,D) ) )) ) ) )) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f40,conjecture,(
% 66.76/8.82 (! [A,B] :( ( relation(B)& function(B) )=> ( one_to_one(B)=> one_to_one(relation_dom_restriction(B,A)) ) ) )),
% 66.76/8.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.76/8.82 fof(f41,negated_conjecture,(
% 66.76/8.82 ~((! [A,B] :( ( relation(B)& function(B) )=> ( one_to_one(B)=> one_to_one(relation_dom_restriction(B,A)) ) ) ))),
% 66.76/8.82 inference(negated_conjecture,[status(cth)],[f40])).
% 66.76/8.82 fof(f53,plain,(
% 66.76/8.82 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f5])).
% 66.76/8.82 fof(f54,plain,(
% 66.76/8.82 ![A,B,C]: ((~C=set_intersection2(A,B)|(![D]: ((~in(D,C)|(in(D,A)&in(D,B)))&(in(D,C)|(~in(D,A)|~in(D,B))))))&(C=set_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 66.76/8.82 inference(NNF_transformation,[status(thm)],[f6])).
% 66.76/8.82 fof(f55,plain,(
% 66.76/8.82 (![A,B,C]: (~C=set_intersection2(A,B)|((![D]: (~in(D,C)|(in(D,A)&in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|~in(D,B)))))))&(![A,B,C]: (C=set_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 66.76/8.82 inference(miniscoping,[status(thm)],[f54])).
% 66.76/8.82 fof(f56,plain,(
% 66.76/8.82 (![A,B,C]: (~C=set_intersection2(A,B)|((![D]: (~in(D,C)|(in(D,A)&in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|~in(D,B)))))))&(![A,B,C]: (C=set_intersection2(A,B)|((~in(sK0_skl(C,B,A),C)|(~in(sK0_skl(C,B,A),A)|~in(sK0_skl(C,B,A),B)))&(in(sK0_skl(C,B,A),C)|(in(sK0_skl(C,B,A),A)&in(sK0_skl(C,B,A),B))))))),
% 66.76/8.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B,A))],[f55])).
% 66.76/8.82 fof(f58,plain,(
% 66.76/8.82 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X2))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f56])).
% 66.76/8.82 fof(f60,plain,(
% 66.76/8.82 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|~in(sK0_skl(X0,X2,X1),X0)|~in(sK0_skl(X0,X2,X1),X1)|~in(sK0_skl(X0,X2,X1),X2))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f56])).
% 66.76/8.82 fof(f61,plain,(
% 66.76/8.82 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK0_skl(X0,X2,X1),X0)|in(sK0_skl(X0,X2,X1),X1))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f56])).
% 66.76/8.82 fof(f63,plain,(
% 66.76/8.82 ![A]: ((~relation(A)|~function(A))|(one_to_one(A)<=>(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C))))),
% 66.76/8.82 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 66.76/8.82 fof(f64,plain,(
% 66.76/8.82 ![A]: ((~relation(A)|~function(A))|((~one_to_one(A)|(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C)))&(one_to_one(A)|(?[B,C]: (((in(B,relation_dom(A))&in(C,relation_dom(A)))&apply(A,B)=apply(A,C))&~B=C)))))),
% 66.76/8.82 inference(NNF_transformation,[status(thm)],[f63])).
% 66.76/8.82 fof(f65,plain,(
% 66.76/8.82 ![A]: ((~relation(A)|~function(A))|((~one_to_one(A)|(![B,C]: (((~in(B,relation_dom(A))|~in(C,relation_dom(A)))|~apply(A,B)=apply(A,C))|B=C)))&(one_to_one(A)|(((in(sK1_skl(A),relation_dom(A))&in(sK2_skl(A),relation_dom(A)))&apply(A,sK1_skl(A))=apply(A,sK2_skl(A)))&~sK1_skl(A)=sK2_skl(A)))))),
% 66.76/8.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B,sK1_skl(A)),skolemize(C,sK2_skl(A))],[f64])).
% 66.76/8.82 fof(f66,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~in(X1,relation_dom(X0))|~in(X2,relation_dom(X0))|~apply(X0,X1)=apply(X0,X2)|X1=X2)),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f65])).
% 66.76/8.82 fof(f67,plain,(
% 66.76/8.82 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK1_skl(X0),relation_dom(X0)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f65])).
% 66.76/8.82 fof(f68,plain,(
% 66.76/8.82 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK2_skl(X0),relation_dom(X0)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f65])).
% 66.76/8.82 fof(f69,plain,(
% 66.76/8.82 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|apply(X0,sK1_skl(X0))=apply(X0,sK2_skl(X0)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f65])).
% 66.76/8.82 fof(f70,plain,(
% 66.76/8.82 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~sK1_skl(X0)=sK2_skl(X0))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f65])).
% 66.76/8.82 fof(f71,plain,(
% 66.76/8.82 ![A,B]: (~relation(A)|relation(relation_dom_restriction(A,B)))),
% 66.76/8.82 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 66.76/8.82 fof(f72,plain,(
% 66.76/8.82 ![A]: (~relation(A)|(![B]: relation(relation_dom_restriction(A,B))))),
% 66.76/8.82 inference(miniscoping,[status(thm)],[f71])).
% 66.76/8.82 fof(f73,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|relation(relation_dom_restriction(X0,X1)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f72])).
% 66.76/8.82 fof(f87,plain,(
% 66.76/8.82 ![A,B]: ((~relation(A)|~function(A))|(relation(relation_dom_restriction(A,B))&function(relation_dom_restriction(A,B))))),
% 66.76/8.82 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 66.76/8.82 fof(f88,plain,(
% 66.76/8.82 ![A]: ((~relation(A)|~function(A))|((![B]: relation(relation_dom_restriction(A,B)))&(![B]: function(relation_dom_restriction(A,B)))))),
% 66.76/8.82 inference(miniscoping,[status(thm)],[f87])).
% 66.76/8.82 fof(f90,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|~function(X0)|function(relation_dom_restriction(X0,X1)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f88])).
% 66.76/8.82 fof(f148,plain,(
% 66.76/8.82 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(B=relation_dom_restriction(C,A)<=>(relation_dom(B)=set_intersection2(relation_dom(C),A)&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))))),
% 66.76/8.82 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 66.76/8.82 fof(f149,plain,(
% 66.76/8.82 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((~B=relation_dom_restriction(C,A)|(relation_dom(B)=set_intersection2(relation_dom(C),A)&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D)))))&(B=relation_dom_restriction(C,A)|(~relation_dom(B)=set_intersection2(relation_dom(C),A)|(?[D]: (in(D,relation_dom(B))&~apply(B,D)=apply(C,D)))))))))),
% 66.76/8.82 inference(NNF_transformation,[status(thm)],[f148])).
% 66.76/8.82 fof(f150,plain,(
% 66.76/8.82 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~B=relation_dom_restriction(C,A)|(relation_dom(B)=set_intersection2(relation_dom(C),A)&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))&(![A]: (B=relation_dom_restriction(C,A)|(~relation_dom(B)=set_intersection2(relation_dom(C),A)|(?[D]: (in(D,relation_dom(B))&~apply(B,D)=apply(C,D))))))))))),
% 66.76/8.82 inference(miniscoping,[status(thm)],[f149])).
% 66.76/8.82 fof(f151,plain,(
% 66.76/8.82 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~B=relation_dom_restriction(C,A)|(relation_dom(B)=set_intersection2(relation_dom(C),A)&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))&(![A]: (B=relation_dom_restriction(C,A)|(~relation_dom(B)=set_intersection2(relation_dom(C),A)|(in(sK14_skl(A,C,B),relation_dom(B))&~apply(B,sK14_skl(A,C,B))=apply(C,sK14_skl(A,C,B))))))))))),
% 66.76/8.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(D,sK14_skl(A,C,B))],[f150])).
% 66.76/8.82 fof(f152,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~X0=relation_dom_restriction(X1,X2)|relation_dom(X0)=set_intersection2(relation_dom(X1),X2))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f151])).
% 66.76/8.82 fof(f153,plain,(
% 66.76/8.82 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~X0=relation_dom_restriction(X1,X2)|~in(X3,relation_dom(X0))|apply(X0,X3)=apply(X1,X3))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f151])).
% 66.76/8.82 fof(f155,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|X0=relation_dom_restriction(X1,X2)|~relation_dom(X0)=set_intersection2(relation_dom(X1),X2)|~apply(X0,sK14_skl(X2,X1,X0))=apply(X1,sK14_skl(X2,X1,X0)))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f151])).
% 66.76/8.82 fof(f161,plain,(
% 66.76/8.82 (?[A,B]: ((relation(B)&function(B))&(one_to_one(B)&~one_to_one(relation_dom_restriction(B,A)))))),
% 66.76/8.82 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 66.76/8.82 fof(f162,plain,(
% 66.76/8.82 ?[B]: ((relation(B)&function(B))&(one_to_one(B)&(?[A]: ~one_to_one(relation_dom_restriction(B,A)))))),
% 66.76/8.82 inference(miniscoping,[status(thm)],[f161])).
% 66.76/8.82 fof(f163,plain,(
% 66.76/8.82 ((relation(sK15_skl)&function(sK15_skl))&(one_to_one(sK15_skl)&~one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))))),
% 66.76/8.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(B,sK15_skl),skolemize(A,sK16_skl)],[f162])).
% 66.76/8.82 fof(f164,plain,(
% 66.76/8.82 relation(sK15_skl)),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f163])).
% 66.76/8.82 fof(f165,plain,(
% 66.76/8.82 function(sK15_skl)),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f163])).
% 66.76/8.82 fof(f166,plain,(
% 66.76/8.82 one_to_one(sK15_skl)),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f163])).
% 66.76/8.82 fof(f167,plain,(
% 66.76/8.82 ~one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))),
% 66.76/8.82 inference(cnf_transformation,[status(thm)],[f163])).
% 66.76/8.82 fof(f172,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X2))),
% 66.76/8.82 inference(destructive_equality_resolution,[status(thm)],[f58])).
% 66.76/8.82 fof(f174,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(relation_dom_restriction(X0,X1))|~function(relation_dom_restriction(X0,X1))|~relation(X0)|~function(X0)|relation_dom(relation_dom_restriction(X0,X1))=set_intersection2(relation_dom(X0),X1))),
% 66.76/8.82 inference(destructive_equality_resolution,[status(thm)],[f152])).
% 66.76/8.82 fof(f175,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~relation(relation_dom_restriction(X0,X1))|~function(relation_dom_restriction(X0,X1))|~relation(X0)|~function(X0)|~in(X2,relation_dom(relation_dom_restriction(X0,X1)))|apply(relation_dom_restriction(X0,X1),X2)=apply(X0,X2))),
% 66.76/8.82 inference(destructive_equality_resolution,[status(thm)],[f153])).
% 66.76/8.82 fof(f203,plain,(
% 66.76/8.82 ![X0,X1]: (~function(relation_dom_restriction(X0,X1))|~relation(X0)|~function(X0)|relation_dom(relation_dom_restriction(X0,X1))=set_intersection2(relation_dom(X0),X1))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f174,f73])).
% 66.76/8.82 fof(f204,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|~function(X0)|relation_dom(relation_dom_restriction(X0,X1))=set_intersection2(relation_dom(X0),X1)|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(resolution,[status(thm)],[f203,f90])).
% 66.76/8.82 fof(f206,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|~function(X0)|relation_dom(relation_dom_restriction(X0,X1))=set_intersection2(relation_dom(X0),X1))),
% 66.76/8.82 inference(duplicate_literals_removal,[status(thm)],[f204])).
% 66.76/8.82 fof(f209,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~relation(relation_dom_restriction(X0,X1))|relation_dom(relation_dom_restriction(relation_dom_restriction(X0,X1),X2))=set_intersection2(relation_dom(relation_dom_restriction(X0,X1)),X2)|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(resolution,[status(thm)],[f206,f90])).
% 66.76/8.82 fof(f210,plain,(
% 66.76/8.82 ![X0]: (~relation(sK15_skl)|relation_dom(relation_dom_restriction(sK15_skl,X0))=set_intersection2(relation_dom(sK15_skl),X0))),
% 66.76/8.82 inference(resolution,[status(thm)],[f206,f165])).
% 66.76/8.82 fof(f219,plain,(
% 66.76/8.82 ![X0,X1,X2]: (relation_dom(relation_dom_restriction(relation_dom_restriction(X0,X1),X2))=set_intersection2(relation_dom(relation_dom_restriction(X0,X1)),X2)|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f209,f73])).
% 66.76/8.82 fof(f220,definition,(
% 66.76/8.82 sQ6_spl <=> (relation(sK15_skl))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f222,plain,(
% 66.76/8.82 ~relation(sK15_skl)|sQ6_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f220])).
% 66.76/8.82 fof(f223,definition,(
% 66.76/8.82 ![X0]: (sQ7_spl <=> (relation_dom(relation_dom_restriction(sK15_skl,X0))=set_intersection2(relation_dom(sK15_skl),X0)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f224,plain,(
% 66.76/8.82 ![X0]: (relation_dom(relation_dom_restriction(sK15_skl,X0))=set_intersection2(relation_dom(sK15_skl),X0)|~sQ7_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f223])).
% 66.76/8.82 fof(f226,plain,(
% 66.76/8.82 ~sQ6_spl|sQ7_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f210,f220,f223])).
% 66.76/8.82 fof(f228,plain,(
% 66.76/8.82 $false|sQ6_spl),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f222,f164])).
% 66.76/8.82 fof(f229,plain,(
% 66.76/8.82 sQ6_spl),
% 66.76/8.82 inference(contradiction_clause,[status(thm)],[f228])).
% 66.76/8.82 fof(f249,plain,(
% 66.76/8.82 ![X0,X1]: (relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,X0),X1))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,X0)),X1)|~relation(sK15_skl))),
% 66.76/8.82 inference(resolution,[status(thm)],[f219,f165])).
% 66.76/8.82 fof(f260,definition,(
% 66.76/8.82 ![X0,X1]: (sQ12_spl <=> (relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,X0),X1))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,X0)),X1)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f261,plain,(
% 66.76/8.82 ![X0,X1]: (relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,X0),X1))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,X0)),X1)|~sQ12_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f260])).
% 66.76/8.82 fof(f263,plain,(
% 66.76/8.82 sQ12_spl|~sQ6_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f249,f260,f220])).
% 66.76/8.82 fof(f265,plain,(
% 66.76/8.82 ![X0,X1]: (relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,X0),X1))=set_intersection2(set_intersection2(relation_dom(sK15_skl),X0),X1)|~sQ7_spl|~sQ12_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f261])).
% 66.76/8.82 fof(f324,plain,(
% 66.76/8.82 ![X0,X1,X2]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X2)|in(sK0_skl(set_intersection2(X0,X1),X2,set_intersection2(X0,X1)),X1))),
% 66.76/8.82 inference(resolution,[status(thm)],[f61,f172])).
% 66.76/8.82 fof(f340,plain,(
% 66.76/8.82 ![X0,X1]: (X0=set_intersection2(X0,X1)|in(sK0_skl(X0,X1,X0),X0))),
% 66.76/8.82 inference(factoring,[status(thm)],[f61])).
% 66.76/8.82 fof(f397,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(relation_dom_restriction(X0,X1))|one_to_one(relation_dom_restriction(X0,X1))|in(sK1_skl(relation_dom_restriction(X0,X1)),relation_dom(relation_dom_restriction(X0,X1)))|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(resolution,[status(thm)],[f67,f90])).
% 66.76/8.82 fof(f421,plain,(
% 66.76/8.82 ![X0,X1]: (one_to_one(relation_dom_restriction(X0,X1))|in(sK1_skl(relation_dom_restriction(X0,X1)),relation_dom(relation_dom_restriction(X0,X1)))|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f397,f73])).
% 66.76/8.82 fof(f422,definition,(
% 66.76/8.82 sQ30_spl <=> (one_to_one(sK15_skl))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f424,plain,(
% 66.76/8.82 ~one_to_one(sK15_skl)|sQ30_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f422])).
% 66.76/8.82 fof(f432,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(relation_dom_restriction(X0,X1))|one_to_one(relation_dom_restriction(X0,X1))|in(sK2_skl(relation_dom_restriction(X0,X1)),relation_dom(relation_dom_restriction(X0,X1)))|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(resolution,[status(thm)],[f68,f90])).
% 66.76/8.82 fof(f447,plain,(
% 66.76/8.82 ![X0,X1]: (one_to_one(relation_dom_restriction(X0,X1))|in(sK2_skl(relation_dom_restriction(X0,X1)),relation_dom(relation_dom_restriction(X0,X1)))|~relation(X0)|~function(X0))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f432,f73])).
% 66.76/8.82 fof(f549,plain,(
% 66.76/8.82 ~relation(relation_dom_restriction(sK15_skl,sK16_skl))|~function(relation_dom_restriction(sK15_skl,sK16_skl))|apply(relation_dom_restriction(sK15_skl,sK16_skl),sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(relation_dom_restriction(sK15_skl,sK16_skl),sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))),
% 66.76/8.82 inference(resolution,[status(thm)],[f69,f167])).
% 66.76/8.82 fof(f550,definition,(
% 66.76/8.82 sQ48_spl <=> (relation(relation_dom_restriction(sK15_skl,sK16_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f552,plain,(
% 66.76/8.82 ~relation(relation_dom_restriction(sK15_skl,sK16_skl))|sQ48_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f550])).
% 66.76/8.82 fof(f553,definition,(
% 66.76/8.82 sQ49_spl <=> (function(relation_dom_restriction(sK15_skl,sK16_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f554,plain,(
% 66.76/8.82 function(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ49_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f553])).
% 66.76/8.82 fof(f555,plain,(
% 66.76/8.82 ~function(relation_dom_restriction(sK15_skl,sK16_skl))|sQ49_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f553])).
% 66.76/8.82 fof(f556,definition,(
% 66.76/8.82 sQ50_spl <=> (apply(relation_dom_restriction(sK15_skl,sK16_skl),sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(relation_dom_restriction(sK15_skl,sK16_skl),sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f557,plain,(
% 66.76/8.82 apply(relation_dom_restriction(sK15_skl,sK16_skl),sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(relation_dom_restriction(sK15_skl,sK16_skl),sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ50_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f556])).
% 66.76/8.82 fof(f559,plain,(
% 66.76/8.82 ~sQ48_spl|~sQ49_spl|sQ50_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f549,f550,f553,f556])).
% 66.76/8.82 fof(f578,definition,(
% 66.76/8.82 sQ53_spl <=> (one_to_one(relation_dom_restriction(sK15_skl,sK16_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f579,plain,(
% 66.76/8.82 one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ53_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f578])).
% 66.76/8.82 fof(f581,definition,(
% 66.76/8.82 sQ54_spl <=> (in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f582,plain,(
% 66.76/8.82 in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ54_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f581])).
% 66.76/8.82 fof(f584,definition,(
% 66.76/8.82 sQ55_spl <=> (in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f585,plain,(
% 66.76/8.82 in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ55_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f584])).
% 66.76/8.82 fof(f587,definition,(
% 66.76/8.82 sQ56_spl <=> (sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl))=sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f588,plain,(
% 66.76/8.82 sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl))=sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ56_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f587])).
% 66.76/8.82 fof(f597,plain,(
% 66.76/8.82 ~relation(sK15_skl)|~function(sK15_skl)|sQ49_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f555,f90])).
% 66.76/8.82 fof(f599,definition,(
% 66.76/8.82 sQ58_spl <=> (function(sK15_skl))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f601,plain,(
% 66.76/8.82 ~function(sK15_skl)|sQ58_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f599])).
% 66.76/8.82 fof(f602,plain,(
% 66.76/8.82 ~sQ6_spl|~sQ58_spl|sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f597,f220,f599,f553])).
% 66.76/8.82 fof(f603,plain,(
% 66.76/8.82 ~relation(sK15_skl)|sQ48_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f552,f73])).
% 66.76/8.82 fof(f605,plain,(
% 66.76/8.82 ~sQ6_spl|sQ48_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f603,f220,f550])).
% 66.76/8.82 fof(f606,plain,(
% 66.76/8.82 $false|sQ58_spl),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f601,f165])).
% 66.76/8.82 fof(f607,plain,(
% 66.76/8.82 sQ58_spl),
% 66.76/8.82 inference(contradiction_clause,[status(thm)],[f606])).
% 66.76/8.82 fof(f612,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK2_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))|~relation(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ49_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f554,f447])).
% 66.76/8.82 fof(f613,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK1_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))|~relation(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ49_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f554,f421])).
% 66.76/8.82 fof(f614,plain,(
% 66.76/8.82 ~relation(relation_dom_restriction(sK15_skl,sK16_skl))|one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))|in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ49_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f554,f68])).
% 66.76/8.82 fof(f615,plain,(
% 66.76/8.82 ~relation(relation_dom_restriction(sK15_skl,sK16_skl))|one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))|in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ49_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f554,f67])).
% 66.76/8.82 fof(f624,definition,(
% 66.76/8.82 ![X0]: (sQ60_spl <=> (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK2_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f625,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK2_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))|~sQ60_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f624])).
% 66.76/8.82 fof(f627,plain,(
% 66.76/8.82 sQ60_spl|~sQ48_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f612,f624,f550,f553])).
% 66.76/8.82 fof(f628,definition,(
% 66.76/8.82 ![X0]: (sQ61_spl <=> (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK1_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f629,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK1_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),relation_dom(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)))|~sQ61_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f628])).
% 66.76/8.82 fof(f631,plain,(
% 66.76/8.82 sQ61_spl|~sQ48_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f613,f628,f550,f553])).
% 66.76/8.82 fof(f632,plain,(
% 66.76/8.82 ~sQ48_spl|sQ53_spl|sQ55_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f614,f550,f578,f584,f553])).
% 66.76/8.82 fof(f633,plain,(
% 66.76/8.82 ~sQ48_spl|sQ53_spl|sQ54_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f615,f550,f578,f581,f553])).
% 66.76/8.82 fof(f651,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK2_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),set_intersection2(set_intersection2(relation_dom(sK15_skl),sK16_skl),X0))|~sQ7_spl|~sQ12_spl|~sQ60_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f265,f625])).
% 66.76/8.82 fof(f652,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK1_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),set_intersection2(set_intersection2(relation_dom(sK15_skl),sK16_skl),X0))|~sQ7_spl|~sQ12_spl|~sQ61_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f265,f629])).
% 66.76/8.82 fof(f658,plain,(
% 66.76/8.82 in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),set_intersection2(relation_dom(sK15_skl),sK16_skl))|~sQ7_spl|~sQ55_spl),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f585])).
% 66.76/8.82 fof(f659,plain,(
% 66.76/8.82 $false|~sQ53_spl),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f579,f167])).
% 66.76/8.82 fof(f660,plain,(
% 66.76/8.82 ~sQ53_spl),
% 66.76/8.82 inference(contradiction_clause,[status(thm)],[f659])).
% 66.76/8.82 fof(f661,plain,(
% 66.76/8.82 in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),set_intersection2(relation_dom(sK15_skl),sK16_skl))|~sQ7_spl|~sQ54_spl),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f582])).
% 66.76/8.82 fof(f971,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK2_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),X0)|~sQ7_spl|~sQ12_spl|~sQ60_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f651,f172])).
% 66.76/8.82 fof(f1038,plain,(
% 66.76/8.82 ![X0]: (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0))|in(sK1_skl(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)),X0)|~sQ7_spl|~sQ12_spl|~sQ61_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f652,f172])).
% 66.76/8.82 fof(f1173,plain,(
% 66.76/8.82 ![X0,X1,X2]: (~function(relation_dom_restriction(X0,X1))|~relation(X0)|~function(X0)|~in(X2,relation_dom(relation_dom_restriction(X0,X1)))|apply(relation_dom_restriction(X0,X1),X2)=apply(X0,X2))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f175,f73])).
% 66.76/8.82 fof(f1174,plain,(
% 66.76/8.82 ![X0]: (~relation(sK15_skl)|~function(sK15_skl)|~in(X0,relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|apply(relation_dom_restriction(sK15_skl,sK16_skl),X0)=apply(sK15_skl,X0)|~sQ49_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f1173,f554])).
% 66.76/8.82 fof(f1178,definition,(
% 66.76/8.82 ![X0]: (sQ119_spl <=> (~in(X0,relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|apply(relation_dom_restriction(sK15_skl,sK16_skl),X0)=apply(sK15_skl,X0)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f1179,plain,(
% 66.76/8.82 ![X0]: (~in(X0,relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)))|apply(relation_dom_restriction(sK15_skl,sK16_skl),X0)=apply(sK15_skl,X0)|~sQ119_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f1178])).
% 66.76/8.82 fof(f1181,plain,(
% 66.76/8.82 ~sQ6_spl|~sQ58_spl|sQ119_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f1174,f220,f599,f1178,f553])).
% 66.76/8.82 fof(f1187,plain,(
% 66.76/8.82 ![X0]: (~in(X0,set_intersection2(relation_dom(sK15_skl),sK16_skl))|apply(relation_dom_restriction(sK15_skl,sK16_skl),X0)=apply(sK15_skl,X0)|~sQ7_spl|~sQ119_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f1179])).
% 66.76/8.82 fof(f1519,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X0)|~function(X0)|X0=relation_dom_restriction(X0,X1)|~relation_dom(X0)=set_intersection2(relation_dom(X0),X1))),
% 66.76/8.82 inference(equality_resolution,[status(thm)],[f155])).
% 66.76/8.82 fof(f1520,plain,(
% 66.76/8.82 ![X0,X1]: (~relation(X0)|~function(X0)|X0=relation_dom_restriction(X0,X1)|~relation_dom(X0)=set_intersection2(relation_dom(X0),X1))),
% 66.76/8.82 inference(duplicate_literals_removal,[status(thm)],[f1519])).
% 66.76/8.82 fof(f1523,plain,(
% 66.76/8.82 apply(relation_dom_restriction(sK15_skl,sK16_skl),sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(sK15_skl,sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ119_spl|~sQ7_spl|~sQ55_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f1187,f658])).
% 66.76/8.82 fof(f1526,plain,(
% 66.76/8.82 apply(relation_dom_restriction(sK15_skl,sK16_skl),sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(sK15_skl,sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ119_spl|~sQ7_spl|~sQ54_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f1187,f661])).
% 66.76/8.82 fof(f1797,plain,(
% 66.76/8.82 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1))|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1)))),
% 66.76/8.82 inference(resolution,[status(thm)],[f324,f60])).
% 66.76/8.82 fof(f1813,plain,(
% 66.76/8.82 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1)))),
% 66.76/8.82 inference(duplicate_literals_removal,[status(thm)],[f1797])).
% 66.76/8.82 fof(f1908,plain,(
% 66.76/8.82 ~relation(relation_dom_restriction(sK15_skl,sK16_skl))|~function(relation_dom_restriction(sK15_skl,sK16_skl))|one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ56_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f588,f70])).
% 66.76/8.82 fof(f1913,plain,(
% 66.76/8.82 ~sQ48_spl|~sQ49_spl|sQ53_spl|~sQ56_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f1908,f550,f553,f578,f587])).
% 66.76/8.82 fof(f1985,plain,(
% 66.76/8.82 ![X0]: (~relation(relation_dom_restriction(sK15_skl,sK16_skl))|relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)|~relation_dom(relation_dom_restriction(sK15_skl,sK16_skl))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)),X0)|~sQ49_spl)),
% 66.76/8.82 inference(resolution,[status(thm)],[f1520,f554])).
% 66.76/8.82 fof(f2001,definition,(
% 66.76/8.82 ![X0]: (sQ197_spl <=> (relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)|~relation_dom(relation_dom_restriction(sK15_skl,sK16_skl))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)),X0)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f2002,plain,(
% 66.76/8.82 ![X0]: (relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)|~relation_dom(relation_dom_restriction(sK15_skl,sK16_skl))=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)),X0)|~sQ197_spl)),
% 66.76/8.82 inference(component_clause,[status(thm)],[f2001])).
% 66.76/8.82 fof(f2004,plain,(
% 66.76/8.82 ~sQ48_spl|sQ197_spl|~sQ49_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f1985,f550,f2001,f553])).
% 66.76/8.82 fof(f2011,plain,(
% 66.76/8.82 ![X0]: (relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)|~set_intersection2(relation_dom(sK15_skl),sK16_skl)=set_intersection2(relation_dom(relation_dom_restriction(sK15_skl,sK16_skl)),X0)|~sQ7_spl|~sQ197_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f2002])).
% 66.76/8.82 fof(f2012,plain,(
% 66.76/8.82 ![X0]: (relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),X0)|~set_intersection2(relation_dom(sK15_skl),sK16_skl)=set_intersection2(set_intersection2(relation_dom(sK15_skl),sK16_skl),X0)|~sQ7_spl|~sQ197_spl)),
% 66.76/8.82 inference(forward_demodulation,[status(thm)],[f224,f2011])).
% 66.76/8.82 fof(f5148,plain,(
% 66.76/8.82 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1))),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f1813,f340])).
% 66.76/8.82 fof(f5156,plain,(
% 66.76/8.82 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X1,X0),X1))),
% 66.76/8.82 inference(paramodulation,[status(thm)],[f53,f5148])).
% 66.76/8.82 fof(f5648,plain,(
% 66.76/8.82 relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl))|~set_intersection2(relation_dom(sK15_skl),sK16_skl)=set_intersection2(sK16_skl,relation_dom(sK15_skl))|~sQ7_spl|~sQ197_spl),
% 66.76/8.82 inference(paramodulation,[status(thm)],[f5156,f2012])).
% 66.76/8.82 fof(f5690,definition,(
% 66.76/8.82 sQ339_spl <=> (relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f5691,plain,(
% 66.76/8.82 relation_dom_restriction(sK15_skl,sK16_skl)=relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl))|~sQ339_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f5690])).
% 66.76/8.82 fof(f5693,definition,(
% 66.76/8.82 sQ340_spl <=> (set_intersection2(relation_dom(sK15_skl),sK16_skl)=set_intersection2(sK16_skl,relation_dom(sK15_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f5695,plain,(
% 66.76/8.82 ~set_intersection2(relation_dom(sK15_skl),sK16_skl)=set_intersection2(sK16_skl,relation_dom(sK15_skl))|sQ340_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f5693])).
% 66.76/8.82 fof(f5696,plain,(
% 66.76/8.82 sQ339_spl|~sQ340_spl|~sQ7_spl|~sQ197_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f5648,f5690,f5693,f223,f2001])).
% 66.76/8.82 fof(f5697,definition,(
% 66.76/8.82 sQ341_spl <=> (one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl))))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f5698,plain,(
% 66.76/8.82 one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl)))|~sQ341_spl),
% 66.76/8.82 inference(component_clause,[status(thm)],[f5697])).
% 66.76/8.82 fof(f5766,plain,(
% 66.76/8.82 $false|sQ340_spl),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f5695,f53])).
% 66.76/8.82 fof(f5767,plain,(
% 66.76/8.82 sQ340_spl),
% 66.76/8.82 inference(contradiction_clause,[status(thm)],[f5766])).
% 66.76/8.82 fof(f35743,plain,(
% 66.76/8.82 one_to_one(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ339_spl|~sQ341_spl),
% 66.76/8.82 inference(backward_demodulation,[status(thm)],[f5691,f5698])).
% 66.76/8.82 fof(f35744,plain,(
% 66.76/8.82 one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl)))|in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl))|~sQ7_spl|~sQ12_spl|~sQ61_spl|~sQ339_spl),
% 66.76/8.82 inference(paramodulation,[status(thm)],[f5691,f1038])).
% 66.76/8.82 fof(f35750,plain,(
% 66.76/8.82 one_to_one(relation_dom_restriction(relation_dom_restriction(sK15_skl,sK16_skl),relation_dom(sK15_skl)))|in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl))|~sQ7_spl|~sQ12_spl|~sQ60_spl|~sQ339_spl),
% 66.76/8.82 inference(paramodulation,[status(thm)],[f5691,f971])).
% 66.76/8.82 fof(f35769,plain,(
% 66.76/8.82 sQ53_spl|~sQ339_spl|~sQ341_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f35743,f578,f5690,f5697])).
% 66.76/8.82 fof(f35770,definition,(
% 66.76/8.82 sQ559_spl <=> (in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ559_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f35773,plain,(
% 66.76/8.82 sQ341_spl|sQ559_spl|~sQ7_spl|~sQ12_spl|~sQ61_spl|~sQ339_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f35744,f5697,f35770,f223,f260,f628,f5690])).
% 66.76/8.82 fof(f35788,definition,(
% 66.76/8.82 sQ563_spl <=> (in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl)))),
% 66.76/8.82 introduced(definition,[new_symbols(definition,[sQ563_spl])],[split_symbol_definition])).
% 66.76/8.82 fof(f35791,plain,(
% 66.76/8.82 sQ341_spl|sQ563_spl|~sQ7_spl|~sQ12_spl|~sQ60_spl|~sQ339_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f35750,f5697,f35788,f223,f260,f624,f5690])).
% 66.76/8.82 fof(f45815,plain,(
% 66.76/8.82 apply(relation_dom_restriction(sK15_skl,sK16_skl),sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(sK15_skl,sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ119_spl|~sQ7_spl|~sQ55_spl|~sQ50_spl),
% 66.76/8.82 inference(backward_demodulation,[status(thm)],[f1523,f557])).
% 66.76/8.82 fof(f46032,plain,(
% 66.76/8.82 apply(sK15_skl,sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)))=apply(sK15_skl,sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)))|~sQ54_spl|~sQ119_spl|~sQ7_spl|~sQ55_spl|~sQ50_spl),
% 66.76/8.82 inference(backward_demodulation,[status(thm)],[f1526,f45815])).
% 66.76/8.82 fof(f46971,plain,(
% 66.76/8.82 ~relation(sK15_skl)|~function(sK15_skl)|~one_to_one(sK15_skl)|~in(sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl))|~in(sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl)),relation_dom(sK15_skl))|sK1_skl(relation_dom_restriction(sK15_skl,sK16_skl))=sK2_skl(relation_dom_restriction(sK15_skl,sK16_skl))|~sQ54_spl|~sQ119_spl|~sQ7_spl|~sQ55_spl|~sQ50_spl),
% 66.76/8.82 inference(resolution,[status(thm)],[f46032,f66])).
% 66.76/8.82 fof(f46975,plain,(
% 66.76/8.82 ~sQ6_spl|~sQ58_spl|~sQ30_spl|~sQ559_spl|~sQ563_spl|sQ56_spl|~sQ54_spl|~sQ119_spl|~sQ7_spl|~sQ55_spl|~sQ50_spl),
% 66.76/8.82 inference(split_clause,[status(thm)],[f46971,f220,f599,f422,f35770,f35788,f587,f581,f1178,f223,f584,f556])).
% 66.76/8.82 fof(f46982,plain,(
% 66.76/8.82 $false|sQ30_spl),
% 66.76/8.82 inference(forward_subsumption_resolution,[status(thm)],[f424,f166])).
% 66.76/8.82 fof(f46983,plain,(
% 66.76/8.82 sQ30_spl),
% 66.76/8.82 inference(contradiction_clause,[status(thm)],[f46982])).
% 66.76/8.82 fof(f46984,plain,(
% 66.76/8.82 $false),
% 66.76/8.82 inference(sat_refutation,[status(thm)],[f226,f229,f263,f559,f602,f605,f607,f627,f631,f632,f633,f660,f1181,f1913,f2004,f5696,f5767,f35769,f35773,f35791,f46975,f46983])).
% 66.76/8.91 % SZS output end CNFRefutation for theBenchmark.p
% 66.76/8.94 % Elapsed time: 8.568380 seconds
% 66.76/8.94 % CPU time: 67.651922 seconds
% 66.76/8.94 % Total memory used: 798.375 MB
% 66.76/8.94 % Net memory used: 768.122 MB
%------------------------------------------------------------------------------