%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU225+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:22:03 PM UTC 2026
% Result : Theorem 0.19s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU225+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n018.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:02:43 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 0.19/0.55 % Refutation found
% 0.19/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.55 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.55 fof(f3,axiom,(
% 0.19/0.55 (! [A] :( empty(A)=> relation(A) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f7,axiom,(
% 0.19/0.55 (! [A] :( ( relation(A)& function(A) )=> (! [B,C] :( ( in(B,relation_dom(A))=> ( C = apply(A,B)<=> in(ordered_pair(B,C),A) ) )& ( ~ in(B,relation_dom(A))=> ( C = apply(A,B)<=> C = empty_set ) ) ) )) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f16,axiom,(
% 0.19/0.55 (! [A,B] :( relation(A)=> relation(relation_dom_restriction(A,B)) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f19,axiom,(
% 0.19/0.55 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f26,axiom,(
% 0.19/0.55 (! [A,B] :( ( relation(A)& function(A) )=> ( relation(relation_dom_restriction(A,B))& function(relation_dom_restriction(A,B)) ) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f31,axiom,(
% 0.19/0.55 (! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,relation_dom(relation_dom_restriction(C,A)))<=> ( in(B,relation_dom(C))& in(B,A) ) ) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f33,axiom,(
% 0.19/0.55 (? [A] :( empty(A)& relation(A) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f34,axiom,(
% 0.19/0.55 (? [A] : empty(A) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f43,axiom,(
% 0.19/0.55 (! [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) ) )) ) ) )) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f45,conjecture,(
% 0.19/0.55 (! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,A)=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) )),
% 0.19/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.55 fof(f46,negated_conjecture,(
% 0.19/0.55 ~((! [A,B,C] :( ( relation(C)& function(C) )=> ( in(B,A)=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ) ))),
% 0.19/0.55 inference(negated_conjecture,[status(cth)],[f45])).
% 0.19/0.55 fof(f53,plain,(
% 0.19/0.55 ![A]: (~empty(A)|relation(A))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.19/0.55 fof(f54,plain,(
% 0.19/0.55 ![X0]: (~empty(X0)|relation(X0))),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f53])).
% 0.19/0.55 fof(f61,plain,(
% 0.19/0.55 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|(C=apply(A,B)<=>in(ordered_pair(B,C),A)))&(in(B,relation_dom(A))|(C=apply(A,B)<=>C=empty_set)))))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.19/0.55 fof(f62,plain,(
% 0.19/0.55 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|((~C=apply(A,B)|in(ordered_pair(B,C),A))&(C=apply(A,B)|~in(ordered_pair(B,C),A))))&(in(B,relation_dom(A))|((~C=apply(A,B)|C=empty_set)&(C=apply(A,B)|~C=empty_set))))))),
% 0.19/0.55 inference(NNF_transformation,[status(thm)],[f61])).
% 0.19/0.55 fof(f63,plain,(
% 0.19/0.55 ![A]: ((~relation(A)|~function(A))|((![B]: (~in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|in(ordered_pair(B,C),A)))&(![C]: (C=apply(A,B)|~in(ordered_pair(B,C),A))))))&(![B]: (in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|C=empty_set))&(![C]: (C=apply(A,B)|~C=empty_set)))))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f62])).
% 0.19/0.55 fof(f66,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|~X2=apply(X0,X1)|X2=empty_set)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f63])).
% 0.19/0.55 fof(f69,plain,(
% 0.19/0.55 ![A,B]: (~relation(A)|relation(relation_dom_restriction(A,B)))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.19/0.55 fof(f70,plain,(
% 0.19/0.55 ![A]: (~relation(A)|(![B]: relation(relation_dom_restriction(A,B))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f69])).
% 0.19/0.55 fof(f71,plain,(
% 0.19/0.55 ![X0,X1]: (~relation(X0)|relation(relation_dom_restriction(X0,X1)))),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f70])).
% 0.19/0.55 fof(f75,plain,(
% 0.19/0.55 relation(empty_set)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f19])).
% 0.19/0.55 fof(f87,plain,(
% 0.19/0.55 ![A,B]: ((~relation(A)|~function(A))|(relation(relation_dom_restriction(A,B))&function(relation_dom_restriction(A,B))))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.19/0.55 fof(f88,plain,(
% 0.19/0.55 ![A]: ((~relation(A)|~function(A))|((![B]: relation(relation_dom_restriction(A,B)))&(![B]: function(relation_dom_restriction(A,B)))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f87])).
% 0.19/0.55 fof(f90,plain,(
% 0.19/0.55 ![X0,X1]: (~relation(X0)|~function(X0)|function(relation_dom_restriction(X0,X1)))),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f88])).
% 0.19/0.55 fof(f100,plain,(
% 0.19/0.55 ![A,B,C]: ((~relation(C)|~function(C))|(in(B,relation_dom(relation_dom_restriction(C,A)))<=>(in(B,relation_dom(C))&in(B,A))))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.19/0.55 fof(f101,plain,(
% 0.19/0.55 ![A,B,C]: ((~relation(C)|~function(C))|((~in(B,relation_dom(relation_dom_restriction(C,A)))|(in(B,relation_dom(C))&in(B,A)))&(in(B,relation_dom(relation_dom_restriction(C,A)))|(~in(B,relation_dom(C))|~in(B,A)))))),
% 0.19/0.55 inference(NNF_transformation,[status(thm)],[f100])).
% 0.19/0.55 fof(f102,plain,(
% 0.19/0.55 ![C]: ((~relation(C)|~function(C))|((![A,B]: (~in(B,relation_dom(relation_dom_restriction(C,A)))|(in(B,relation_dom(C))&in(B,A))))&(![A,B]: (in(B,relation_dom(relation_dom_restriction(C,A)))|(~in(B,relation_dom(C))|~in(B,A))))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f101])).
% 0.19/0.55 fof(f105,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(relation_dom_restriction(X0,X2)))|~in(X1,relation_dom(X0))|~in(X1,X2))),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f102])).
% 0.19/0.55 fof(f109,plain,(
% 0.19/0.55 (empty(sK2_skl)&relation(sK2_skl))),
% 0.19/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f33])).
% 0.19/0.55 fof(f111,plain,(
% 0.19/0.55 relation(sK2_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f109])).
% 0.19/0.55 fof(f112,plain,(
% 0.19/0.55 empty(sK3_skl)),
% 0.19/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f34])).
% 0.19/0.55 fof(f113,plain,(
% 0.19/0.55 empty(sK3_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f112])).
% 0.19/0.55 fof(f135,plain,(
% 0.19/0.55 ![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))))))))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.19/0.55 fof(f136,plain,(
% 0.19/0.55 ![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)))))))))),
% 0.19/0.55 inference(NNF_transformation,[status(thm)],[f135])).
% 0.19/0.55 fof(f137,plain,(
% 0.19/0.55 ![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))))))))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f136])).
% 0.19/0.55 fof(f138,plain,(
% 0.19/0.55 ![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(sK9_skl(A,C,B),relation_dom(B))&~apply(B,sK9_skl(A,C,B))=apply(C,sK9_skl(A,C,B))))))))))),
% 0.19/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(D,sK9_skl(A,C,B))],[f137])).
% 0.19/0.55 fof(f140,plain,(
% 0.19/0.55 ![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))),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f138])).
% 0.19/0.55 fof(f145,plain,(
% 0.19/0.55 (?[A,B,C]: ((relation(C)&function(C))&(in(B,A)&~apply(relation_dom_restriction(C,A),B)=apply(C,B))))),
% 0.19/0.55 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.19/0.55 fof(f146,plain,(
% 0.19/0.55 ?[C]: ((relation(C)&function(C))&(?[A,B]: (in(B,A)&~apply(relation_dom_restriction(C,A),B)=apply(C,B))))),
% 0.19/0.55 inference(miniscoping,[status(thm)],[f145])).
% 0.19/0.55 fof(f147,plain,(
% 0.19/0.55 ((relation(sK10_skl)&function(sK10_skl))&(in(sK12_skl,sK11_skl)&~apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=apply(sK10_skl,sK12_skl)))),
% 0.19/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK10_skl),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f146])).
% 0.19/0.55 fof(f148,plain,(
% 0.19/0.55 relation(sK10_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f147])).
% 0.19/0.55 fof(f149,plain,(
% 0.19/0.55 function(sK10_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f147])).
% 0.19/0.55 fof(f150,plain,(
% 0.19/0.55 in(sK12_skl,sK11_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f147])).
% 0.19/0.55 fof(f151,plain,(
% 0.19/0.55 ~apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=apply(sK10_skl,sK12_skl)),
% 0.19/0.55 inference(cnf_transformation,[status(thm)],[f147])).
% 0.19/0.55 fof(f159,plain,(
% 0.19/0.55 ![X0,X1]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|apply(X0,X1)=empty_set)),
% 0.19/0.55 inference(destructive_equality_resolution,[status(thm)],[f66])).
% 0.19/0.55 fof(f162,plain,(
% 0.19/0.55 ![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))),
% 0.19/0.55 inference(destructive_equality_resolution,[status(thm)],[f140])).
% 0.19/0.55 fof(f189,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(relation_dom_restriction(X0,X2)))|~in(X1,X2)|~relation(X0)|~function(X0)|apply(X0,X1)=empty_set)),
% 0.19/0.55 inference(resolution,[status(thm)],[f105,f159])).
% 0.19/0.55 fof(f190,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(relation_dom_restriction(X0,X2)))|~in(X1,X2)|apply(X0,X1)=empty_set)),
% 0.19/0.55 inference(duplicate_literals_removal,[status(thm)],[f189])).
% 0.19/0.55 fof(f204,definition,(
% 0.19/0.55 sQ6_spl <=> (relation(sK10_skl))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f206,plain,(
% 0.19/0.55 ~relation(sK10_skl)|sQ6_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f204])).
% 0.19/0.55 fof(f212,plain,(
% 0.19/0.55 $false|sQ6_spl),
% 0.19/0.55 inference(forward_subsumption_resolution,[status(thm)],[f206,f148])).
% 0.19/0.55 fof(f213,plain,(
% 0.19/0.55 sQ6_spl),
% 0.19/0.55 inference(contradiction_clause,[status(thm)],[f212])).
% 0.19/0.55 fof(f224,plain,(
% 0.19/0.55 ![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))),
% 0.19/0.55 inference(forward_subsumption_resolution,[status(thm)],[f162,f71])).
% 0.19/0.55 fof(f225,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(relation_dom_restriction(X0,X2)))|apply(relation_dom_restriction(X0,X2),X1)=apply(X0,X1)|~relation(X0)|~function(X0))),
% 0.19/0.55 inference(resolution,[status(thm)],[f224,f90])).
% 0.19/0.55 fof(f227,plain,(
% 0.19/0.55 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(relation_dom_restriction(X0,X2)))|apply(relation_dom_restriction(X0,X2),X1)=apply(X0,X1))),
% 0.19/0.55 inference(duplicate_literals_removal,[status(thm)],[f225])).
% 0.19/0.55 fof(f298,definition,(
% 0.19/0.55 sQ18_spl <=> (function(sK10_skl))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f300,plain,(
% 0.19/0.55 ~function(sK10_skl)|sQ18_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f298])).
% 0.19/0.55 fof(f306,plain,(
% 0.19/0.55 $false|sQ18_spl),
% 0.19/0.55 inference(forward_subsumption_resolution,[status(thm)],[f300,f149])).
% 0.19/0.55 fof(f307,plain,(
% 0.19/0.55 sQ18_spl),
% 0.19/0.55 inference(contradiction_clause,[status(thm)],[f306])).
% 0.19/0.55 fof(f344,plain,(
% 0.19/0.55 ![X0,X1]: (~relation(sK10_skl)|in(X0,relation_dom(relation_dom_restriction(sK10_skl,X1)))|~in(X0,X1)|apply(sK10_skl,X0)=empty_set)),
% 0.19/0.55 inference(resolution,[status(thm)],[f190,f149])).
% 0.19/0.55 fof(f355,definition,(
% 0.19/0.55 ![X0,X1]: (sQ25_spl <=> (in(X0,relation_dom(relation_dom_restriction(sK10_skl,X1)))|~in(X0,X1)|apply(sK10_skl,X0)=empty_set))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f356,plain,(
% 0.19/0.55 ![X0,X1]: (in(X0,relation_dom(relation_dom_restriction(sK10_skl,X1)))|~in(X0,X1)|apply(sK10_skl,X0)=empty_set|~sQ25_spl)),
% 0.19/0.55 inference(component_clause,[status(thm)],[f355])).
% 0.19/0.55 fof(f358,plain,(
% 0.19/0.55 ~sQ6_spl|sQ25_spl),
% 0.19/0.55 inference(split_clause,[status(thm)],[f344,f204,f355])).
% 0.19/0.55 fof(f432,plain,(
% 0.19/0.55 in(sK12_skl,relation_dom(relation_dom_restriction(sK10_skl,sK11_skl)))|apply(sK10_skl,sK12_skl)=empty_set|~sQ25_spl),
% 0.19/0.55 inference(resolution,[status(thm)],[f356,f150])).
% 0.19/0.55 fof(f437,definition,(
% 0.19/0.55 sQ33_spl <=> (in(sK12_skl,relation_dom(relation_dom_restriction(sK10_skl,sK11_skl))))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f438,plain,(
% 0.19/0.55 in(sK12_skl,relation_dom(relation_dom_restriction(sK10_skl,sK11_skl)))|~sQ33_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f437])).
% 0.19/0.55 fof(f439,plain,(
% 0.19/0.55 ~in(sK12_skl,relation_dom(relation_dom_restriction(sK10_skl,sK11_skl)))|sQ33_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f437])).
% 0.19/0.55 fof(f440,definition,(
% 0.19/0.55 sQ34_spl <=> (apply(sK10_skl,sK12_skl)=empty_set)),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f441,plain,(
% 0.19/0.55 apply(sK10_skl,sK12_skl)=empty_set|~sQ34_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f440])).
% 0.19/0.55 fof(f443,plain,(
% 0.19/0.55 sQ33_spl|sQ34_spl|~sQ25_spl),
% 0.19/0.55 inference(split_clause,[status(thm)],[f432,f437,f440,f355])).
% 0.19/0.55 fof(f444,plain,(
% 0.19/0.55 ~relation(sK10_skl)|~function(sK10_skl)|apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=apply(sK10_skl,sK12_skl)|~sQ33_spl),
% 0.19/0.55 inference(resolution,[status(thm)],[f438,f227])).
% 0.19/0.55 fof(f453,definition,(
% 0.19/0.55 sQ35_spl <=> (apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=apply(sK10_skl,sK12_skl))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f454,plain,(
% 0.19/0.55 apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=apply(sK10_skl,sK12_skl)|~sQ35_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f453])).
% 0.19/0.55 fof(f456,plain,(
% 0.19/0.55 ~sQ6_spl|~sQ18_spl|sQ35_spl|~sQ33_spl),
% 0.19/0.55 inference(split_clause,[status(thm)],[f444,f204,f298,f453,f437])).
% 0.19/0.55 fof(f465,definition,(
% 0.19/0.55 sQ38_spl <=> (relation(relation_dom_restriction(sK10_skl,sK11_skl)))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f467,plain,(
% 0.19/0.55 ~relation(relation_dom_restriction(sK10_skl,sK11_skl))|sQ38_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f465])).
% 0.19/0.55 fof(f468,definition,(
% 0.19/0.55 sQ39_spl <=> (function(relation_dom_restriction(sK10_skl,sK11_skl)))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f470,plain,(
% 0.19/0.55 ~function(relation_dom_restriction(sK10_skl,sK11_skl))|sQ39_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f468])).
% 0.19/0.55 fof(f487,plain,(
% 0.19/0.55 $false|~sQ35_spl),
% 0.19/0.55 inference(forward_subsumption_resolution,[status(thm)],[f454,f151])).
% 0.19/0.55 fof(f488,plain,(
% 0.19/0.55 ~sQ35_spl),
% 0.19/0.55 inference(contradiction_clause,[status(thm)],[f487])).
% 0.19/0.55 fof(f489,plain,(
% 0.19/0.55 ~apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=empty_set|~sQ34_spl),
% 0.19/0.55 inference(backward_demodulation,[status(thm)],[f441,f151])).
% 0.19/0.55 fof(f490,plain,(
% 0.19/0.55 ~relation(relation_dom_restriction(sK10_skl,sK11_skl))|~function(relation_dom_restriction(sK10_skl,sK11_skl))|apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=empty_set|sQ33_spl),
% 0.19/0.55 inference(resolution,[status(thm)],[f439,f159])).
% 0.19/0.55 fof(f493,definition,(
% 0.19/0.55 sQ44_spl <=> (apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=empty_set)),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f494,plain,(
% 0.19/0.55 apply(relation_dom_restriction(sK10_skl,sK11_skl),sK12_skl)=empty_set|~sQ44_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f493])).
% 0.19/0.55 fof(f496,plain,(
% 0.19/0.55 ~sQ38_spl|~sQ39_spl|sQ44_spl|sQ33_spl),
% 0.19/0.55 inference(split_clause,[status(thm)],[f490,f465,f468,f493,f437])).
% 0.19/0.55 fof(f501,definition,(
% 0.19/0.55 sQ45_spl <=> (relation(empty_set))),
% 0.19/0.55 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.19/0.55 fof(f503,plain,(
% 0.19/0.55 ~relation(empty_set)|sQ45_spl),
% 0.19/0.55 inference(component_clause,[status(thm)],[f501])).
% 0.19/0.55 fof(f520,plain,(
% 0.19/0.55 $false|sQ45_spl),
% 0.19/0.56 inference(forward_subsumption_resolution,[status(thm)],[f503,f75])).
% 0.19/0.56 fof(f521,plain,(
% 0.19/0.56 sQ45_spl),
% 0.19/0.56 inference(contradiction_clause,[status(thm)],[f520])).
% 0.19/0.56 fof(f526,definition,(
% 0.19/0.56 sQ50_spl <=> (relation(sK2_skl))),
% 0.19/0.56 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.19/0.56 fof(f528,plain,(
% 0.19/0.56 ~relation(sK2_skl)|sQ50_spl),
% 0.19/0.56 inference(component_clause,[status(thm)],[f526])).
% 0.19/0.56 fof(f545,plain,(
% 0.19/0.56 $false|sQ50_spl),
% 0.19/0.56 inference(forward_subsumption_resolution,[status(thm)],[f528,f111])).
% 0.19/0.56 fof(f546,plain,(
% 0.19/0.56 sQ50_spl),
% 0.19/0.56 inference(contradiction_clause,[status(thm)],[f545])).
% 0.19/0.56 fof(f551,definition,(
% 0.19/0.56 sQ55_spl <=> (relation(sK3_skl))),
% 0.19/0.56 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.19/0.56 fof(f553,plain,(
% 0.19/0.56 ~relation(sK3_skl)|sQ55_spl),
% 0.19/0.56 inference(component_clause,[status(thm)],[f551])).
% 0.19/0.56 fof(f570,plain,(
% 0.19/0.56 ~empty(sK3_skl)|sQ55_spl),
% 0.19/0.56 inference(resolution,[status(thm)],[f553,f54])).
% 0.19/0.56 fof(f571,plain,(
% 0.19/0.56 $false|sQ55_spl),
% 0.19/0.56 inference(forward_subsumption_resolution,[status(thm)],[f570,f113])).
% 0.19/0.56 fof(f572,plain,(
% 0.19/0.56 sQ55_spl),
% 0.19/0.56 inference(contradiction_clause,[status(thm)],[f571])).
% 0.19/0.56 fof(f575,plain,(
% 0.19/0.56 ~relation(sK10_skl)|~function(sK10_skl)|sQ39_spl),
% 0.19/0.56 inference(resolution,[status(thm)],[f470,f90])).
% 0.19/0.56 fof(f577,plain,(
% 0.19/0.56 ~sQ6_spl|~sQ18_spl|sQ39_spl),
% 0.19/0.56 inference(split_clause,[status(thm)],[f575,f204,f298,f468])).
% 0.19/0.56 fof(f578,plain,(
% 0.19/0.56 ~relation(sK10_skl)|sQ38_spl),
% 0.19/0.56 inference(resolution,[status(thm)],[f467,f71])).
% 0.19/0.56 fof(f580,plain,(
% 0.19/0.56 ~sQ6_spl|sQ38_spl),
% 0.19/0.56 inference(split_clause,[status(thm)],[f578,f204,f465])).
% 0.19/0.56 fof(f581,plain,(
% 0.19/0.56 $false|~sQ34_spl|~sQ44_spl),
% 0.19/0.56 inference(forward_subsumption_resolution,[status(thm)],[f494,f489])).
% 0.19/0.56 fof(f582,plain,(
% 0.19/0.56 ~sQ34_spl|~sQ44_spl),
% 0.19/0.56 inference(contradiction_clause,[status(thm)],[f581])).
% 0.19/0.56 fof(f583,plain,(
% 0.19/0.56 $false),
% 0.19/0.56 inference(sat_refutation,[status(thm)],[f213,f307,f358,f443,f456,f488,f496,f521,f546,f572,f577,f580,f582])).
% 0.19/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.60 % Elapsed time: 0.135473 seconds
% 0.27/0.60 % CPU time: 0.452315 seconds
% 0.27/0.60 % Total memory used: 54.581 MB
% 0.27/0.60 % Net memory used: 54.200 MB
%------------------------------------------------------------------------------