%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU048+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 : n009.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:37 PM UTC 2026
% Result : Theorem 0.11s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU048+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.11/0.36 % Computer : n009.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 05:48:27 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.11/0.45 % Refutation found
% 0.11/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.45 fof(f5,axiom,(
% 0.11/0.45 (! [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 ) )) ) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f6,axiom,(
% 0.11/0.45 (! [A,B] :( relation(B)=> relation(relation_rng_restriction(A,B)) ) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f12,axiom,(
% 0.11/0.45 (! [A,B] :( ( relation(B)& function(B) )=> ( relation(relation_rng_restriction(A,B))& function(relation_rng_restriction(A,B)) ) ) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f33,axiom,(
% 0.11/0.45 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( B = relation_rng_restriction(A,C)<=> ( (! [D] :( in(D,relation_dom(B))<=> ( in(D,relation_dom(C))& in(apply(C,D),A) ) ))& (! [D] :( in(D,relation_dom(B))=> apply(B,D) = apply(C,D) ) )) ) ) )) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f35,conjecture,(
% 0.11/0.45 (! [A,B] :( ( relation(B)& function(B) )=> ( one_to_one(B)=> one_to_one(relation_rng_restriction(A,B)) ) ) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f36,negated_conjecture,(
% 0.11/0.45 ~((! [A,B] :( ( relation(B)& function(B) )=> ( one_to_one(B)=> one_to_one(relation_rng_restriction(A,B)) ) ) ))),
% 0.11/0.45 inference(negated_conjecture,[status(cth)],[f35])).
% 0.11/0.45 fof(f47,plain,(
% 0.11/0.45 ![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))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.11/0.45 fof(f48,plain,(
% 0.11/0.45 ![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)))))),
% 0.11/0.45 inference(NNF_transformation,[status(thm)],[f47])).
% 0.11/0.45 fof(f49,plain,(
% 0.11/0.45 ![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(sK0_skl(A),relation_dom(A))&in(sK1_skl(A),relation_dom(A)))&apply(A,sK0_skl(A))=apply(A,sK1_skl(A)))&~sK0_skl(A)=sK1_skl(A)))))),
% 0.11/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(B,sK0_skl(A)),skolemize(C,sK1_skl(A))],[f48])).
% 0.11/0.45 fof(f50,plain,(
% 0.11/0.45 ![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)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.11/0.45 fof(f51,plain,(
% 0.11/0.45 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK0_skl(X0),relation_dom(X0)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.11/0.45 fof(f52,plain,(
% 0.11/0.45 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|in(sK1_skl(X0),relation_dom(X0)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.11/0.45 fof(f53,plain,(
% 0.11/0.45 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|apply(X0,sK0_skl(X0))=apply(X0,sK1_skl(X0)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.11/0.45 fof(f54,plain,(
% 0.11/0.45 ![X0]: (~relation(X0)|~function(X0)|one_to_one(X0)|~sK0_skl(X0)=sK1_skl(X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.11/0.45 fof(f55,plain,(
% 0.11/0.45 ![A,B]: (~relation(B)|relation(relation_rng_restriction(A,B)))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.11/0.45 fof(f56,plain,(
% 0.11/0.45 ![B]: (~relation(B)|(![A]: relation(relation_rng_restriction(A,B))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f55])).
% 0.11/0.45 fof(f57,plain,(
% 0.11/0.45 ![X0,X1]: (~relation(X0)|relation(relation_rng_restriction(X1,X0)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.11/0.45 fof(f67,plain,(
% 0.11/0.45 ![A,B]: ((~relation(B)|~function(B))|(relation(relation_rng_restriction(A,B))&function(relation_rng_restriction(A,B))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.11/0.45 fof(f68,plain,(
% 0.11/0.45 ![B]: ((~relation(B)|~function(B))|((![A]: relation(relation_rng_restriction(A,B)))&(![A]: function(relation_rng_restriction(A,B)))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f67])).
% 0.11/0.45 fof(f70,plain,(
% 0.11/0.45 ![X0,X1]: (~relation(X0)|~function(X0)|function(relation_rng_restriction(X1,X0)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f68])).
% 0.11/0.45 fof(f128,plain,(
% 0.11/0.45 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(B=relation_rng_restriction(A,C)<=>((![D]: (in(D,relation_dom(B))<=>(in(D,relation_dom(C))&in(apply(C,D),A))))&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.11/0.45 fof(f129,definition,(
% 0.11/0.45 ![A,C,D]: (sP0_prd(D,C,A)<=>(in(D,relation_dom(C))&in(apply(C,D),A)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.11/0.45 fof(f130,plain,(
% 0.11/0.45 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(B=relation_rng_restriction(A,C)<=>((![D]: (in(D,relation_dom(B))<=>sP0_prd(D,C,A)))&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))))),
% 0.11/0.45 inference(formula_renaming,[status(thm)],[f128,f129])).
% 0.11/0.45 fof(f131,plain,(
% 0.11/0.45 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((~B=relation_rng_restriction(A,C)|((![D]: ((~in(D,relation_dom(B))|sP0_prd(D,C,A))&(in(D,relation_dom(B))|~sP0_prd(D,C,A))))&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D)))))&(B=relation_rng_restriction(A,C)|((?[D]: ((~in(D,relation_dom(B))|~sP0_prd(D,C,A))&(in(D,relation_dom(B))|sP0_prd(D,C,A))))|(?[D]: (in(D,relation_dom(B))&~apply(B,D)=apply(C,D)))))))))),
% 0.11/0.45 inference(NNF_transformation,[status(thm)],[f130])).
% 0.11/0.45 fof(f132,plain,(
% 0.11/0.45 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~B=relation_rng_restriction(A,C)|(((![D]: (~in(D,relation_dom(B))|sP0_prd(D,C,A)))&(![D]: (in(D,relation_dom(B))|~sP0_prd(D,C,A))))&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))&(![A]: (B=relation_rng_restriction(A,C)|((?[D]: ((~in(D,relation_dom(B))|~sP0_prd(D,C,A))&(in(D,relation_dom(B))|sP0_prd(D,C,A))))|(?[D]: (in(D,relation_dom(B))&~apply(B,D)=apply(C,D))))))))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f131])).
% 0.11/0.45 fof(f133,plain,(
% 0.11/0.45 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~B=relation_rng_restriction(A,C)|(((![D]: (~in(D,relation_dom(B))|sP0_prd(D,C,A)))&(![D]: (in(D,relation_dom(B))|~sP0_prd(D,C,A))))&(![D]: (~in(D,relation_dom(B))|apply(B,D)=apply(C,D))))))&(![A]: (B=relation_rng_restriction(A,C)|(((~in(sK13_skl(A,C,B),relation_dom(B))|~sP0_prd(sK13_skl(A,C,B),C,A))&(in(sK13_skl(A,C,B),relation_dom(B))|sP0_prd(sK13_skl(A,C,B),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))))))))))),
% 0.11/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(D,sK13_skl(A,C,B)),skolemize(D,sK14_skl(A,C,B))],[f132])).
% 0.11/0.45 fof(f134,plain,(
% 0.11/0.45 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~X0=relation_rng_restriction(X2,X1)|~in(X3,relation_dom(X0))|sP0_prd(X3,X1,X2))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f133])).
% 0.11/0.45 fof(f136,plain,(
% 0.11/0.45 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~X0=relation_rng_restriction(X2,X1)|~in(X3,relation_dom(X0))|apply(X0,X3)=apply(X1,X3))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f133])).
% 0.11/0.45 fof(f144,plain,(
% 0.11/0.45 (?[A,B]: ((relation(B)&function(B))&(one_to_one(B)&~one_to_one(relation_rng_restriction(A,B)))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.11/0.45 fof(f145,plain,(
% 0.11/0.45 ?[B]: ((relation(B)&function(B))&(one_to_one(B)&(?[A]: ~one_to_one(relation_rng_restriction(A,B)))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f144])).
% 0.11/0.45 fof(f146,plain,(
% 0.11/0.45 ((relation(sK15_skl)&function(sK15_skl))&(one_to_one(sK15_skl)&~one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))))),
% 0.11/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(B,sK15_skl),skolemize(A,sK16_skl)],[f145])).
% 0.11/0.45 fof(f147,plain,(
% 0.11/0.45 relation(sK15_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f146])).
% 0.11/0.45 fof(f148,plain,(
% 0.11/0.45 function(sK15_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f146])).
% 0.11/0.45 fof(f149,plain,(
% 0.11/0.45 one_to_one(sK15_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f146])).
% 0.11/0.45 fof(f150,plain,(
% 0.11/0.45 ~one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f146])).
% 0.11/0.45 fof(f151,plain,(
% 0.11/0.45 ![A,C,D]: ((~sP0_prd(D,C,A)|(in(D,relation_dom(C))&in(apply(C,D),A)))&(sP0_prd(D,C,A)|(~in(D,relation_dom(C))|~in(apply(C,D),A))))),
% 0.11/0.45 inference(NNF_transformation,[status(thm)],[f129])).
% 0.11/0.45 fof(f152,plain,(
% 0.11/0.45 (![A,C,D]: (~sP0_prd(D,C,A)|(in(D,relation_dom(C))&in(apply(C,D),A))))&(![A,C,D]: (sP0_prd(D,C,A)|(~in(D,relation_dom(C))|~in(apply(C,D),A))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f151])).
% 0.11/0.45 fof(f153,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|in(X0,relation_dom(X1)))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f152])).
% 0.11/0.45 fof(f157,plain,(
% 0.11/0.45 ![X2,X1,X3]: (~relation(relation_rng_restriction(X2,X1))|~function(relation_rng_restriction(X2,X1))|~relation(X1)|~function(X1)|~in(X3,relation_dom(relation_rng_restriction(X2,X1)))|sP0_prd(X3,X1,X2))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f134])).
% 0.11/0.45 fof(f158,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~function(relation_rng_restriction(X0,X1))|~relation(X1)|~function(X1)|~in(X2,relation_dom(relation_rng_restriction(X0,X1)))|sP0_prd(X2,X1,X0))),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f157,f57])).
% 0.11/0.45 fof(f161,plain,(
% 0.11/0.45 ![X2,X1,X3]: (~relation(relation_rng_restriction(X2,X1))|~function(relation_rng_restriction(X2,X1))|~relation(X1)|~function(X1)|~in(X3,relation_dom(relation_rng_restriction(X2,X1)))|apply(relation_rng_restriction(X2,X1),X3)=apply(X1,X3))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f136])).
% 0.11/0.45 fof(f162,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~function(relation_rng_restriction(X0,X1))|~relation(X1)|~function(X1)|~in(X2,relation_dom(relation_rng_restriction(X0,X1)))|apply(relation_rng_restriction(X0,X1),X2)=apply(X1,X2))),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f161,f57])).
% 0.11/0.45 fof(f172,plain,(
% 0.11/0.45 ~relation(relation_rng_restriction(sK16_skl,sK15_skl))|~function(relation_rng_restriction(sK16_skl,sK15_skl))|apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(relation_rng_restriction(sK16_skl,sK15_skl),sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))),
% 0.11/0.45 inference(resolution,[status(thm)],[f53,f150])).
% 0.11/0.45 fof(f173,definition,(
% 0.11/0.45 sQ0_spl <=> (relation(relation_rng_restriction(sK16_skl,sK15_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f175,plain,(
% 0.11/0.45 ~relation(relation_rng_restriction(sK16_skl,sK15_skl))|sQ0_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f173])).
% 0.11/0.45 fof(f176,definition,(
% 0.11/0.45 sQ1_spl <=> (function(relation_rng_restriction(sK16_skl,sK15_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f177,plain,(
% 0.11/0.45 function(relation_rng_restriction(sK16_skl,sK15_skl))|~sQ1_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f176])).
% 0.11/0.45 fof(f178,plain,(
% 0.11/0.45 ~function(relation_rng_restriction(sK16_skl,sK15_skl))|sQ1_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f176])).
% 0.11/0.45 fof(f179,definition,(
% 0.11/0.45 sQ2_spl <=> (apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(relation_rng_restriction(sK16_skl,sK15_skl),sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl))))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f180,plain,(
% 0.11/0.45 apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(relation_rng_restriction(sK16_skl,sK15_skl),sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ2_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f179])).
% 0.11/0.45 fof(f182,plain,(
% 0.11/0.45 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f172,f173,f176,f179])).
% 0.11/0.45 fof(f187,definition,(
% 0.11/0.45 sQ3_spl <=> (one_to_one(relation_rng_restriction(sK16_skl,sK15_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f188,plain,(
% 0.11/0.45 one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))|~sQ3_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f187])).
% 0.11/0.45 fof(f190,definition,(
% 0.11/0.45 sQ4_spl <=> (in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl))))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f191,plain,(
% 0.11/0.45 in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ4_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f190])).
% 0.11/0.45 fof(f192,plain,(
% 0.11/0.45 ~in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|sQ4_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f190])).
% 0.11/0.45 fof(f193,definition,(
% 0.11/0.45 sQ5_spl <=> (in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl))))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f194,plain,(
% 0.11/0.45 in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ5_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f193])).
% 0.11/0.45 fof(f195,plain,(
% 0.11/0.45 ~in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|sQ5_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f193])).
% 0.11/0.45 fof(f196,definition,(
% 0.11/0.45 sQ6_spl <=> (sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl))=sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f206,plain,(
% 0.11/0.45 ~relation(sK15_skl)|~function(sK15_skl)|sQ1_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f178,f70])).
% 0.11/0.45 fof(f207,definition,(
% 0.11/0.45 sQ8_spl <=> (relation(sK15_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f209,plain,(
% 0.11/0.45 ~relation(sK15_skl)|sQ8_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f207])).
% 0.11/0.45 fof(f210,definition,(
% 0.11/0.45 sQ9_spl <=> (function(sK15_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f212,plain,(
% 0.11/0.45 ~function(sK15_skl)|sQ9_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f210])).
% 0.11/0.45 fof(f213,plain,(
% 0.11/0.45 ~sQ8_spl|~sQ9_spl|sQ1_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f206,f207,f210,f176])).
% 0.11/0.45 fof(f214,plain,(
% 0.11/0.45 $false|sQ9_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f212,f148])).
% 0.11/0.45 fof(f215,plain,(
% 0.11/0.45 sQ9_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f214])).
% 0.11/0.45 fof(f216,plain,(
% 0.11/0.45 ~relation(sK15_skl)|sQ0_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f175,f57])).
% 0.11/0.45 fof(f217,plain,(
% 0.11/0.45 $false|sQ0_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f216,f147])).
% 0.11/0.45 fof(f218,plain,(
% 0.11/0.45 sQ0_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f217])).
% 0.11/0.45 fof(f219,plain,(
% 0.11/0.45 ![X0]: (~relation(sK15_skl)|~function(sK15_skl)|~in(X0,relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|apply(relation_rng_restriction(sK16_skl,sK15_skl),X0)=apply(sK15_skl,X0)|~sQ1_spl)),
% 0.11/0.45 inference(resolution,[status(thm)],[f162,f177])).
% 0.11/0.45 fof(f221,definition,(
% 0.11/0.45 ![X0]: (sQ10_spl <=> (~in(X0,relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|apply(relation_rng_restriction(sK16_skl,sK15_skl),X0)=apply(sK15_skl,X0)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f222,plain,(
% 0.11/0.45 ![X0]: (~in(X0,relation_dom(relation_rng_restriction(sK16_skl,sK15_skl)))|apply(relation_rng_restriction(sK16_skl,sK15_skl),X0)=apply(sK15_skl,X0)|~sQ10_spl)),
% 0.11/0.45 inference(component_clause,[status(thm)],[f221])).
% 0.11/0.45 fof(f224,plain,(
% 0.11/0.45 ~sQ8_spl|~sQ9_spl|sQ10_spl|~sQ1_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f219,f207,f210,f221,f176])).
% 0.11/0.45 fof(f226,plain,(
% 0.11/0.45 $false|sQ8_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f209,f147])).
% 0.11/0.45 fof(f227,plain,(
% 0.11/0.45 sQ8_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f226])).
% 0.11/0.45 fof(f234,plain,(
% 0.11/0.45 ~relation(relation_rng_restriction(sK16_skl,sK15_skl))|~function(relation_rng_restriction(sK16_skl,sK15_skl))|~sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl))=sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl))),
% 0.11/0.45 inference(resolution,[status(thm)],[f54,f150])).
% 0.11/0.45 fof(f235,plain,(
% 0.11/0.45 ~sQ0_spl|~sQ1_spl|~sQ6_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f234,f173,f176,f196])).
% 0.11/0.45 fof(f256,plain,(
% 0.11/0.45 ~relation(relation_rng_restriction(sK16_skl,sK15_skl))|~function(relation_rng_restriction(sK16_skl,sK15_skl))|one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))|sQ5_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f195,f52])).
% 0.11/0.45 fof(f257,plain,(
% 0.11/0.45 ~sQ0_spl|~sQ1_spl|sQ3_spl|sQ5_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f256,f173,f176,f187,f193])).
% 0.11/0.45 fof(f258,plain,(
% 0.11/0.45 $false|~sQ3_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f188,f150])).
% 0.11/0.45 fof(f259,plain,(
% 0.11/0.45 ~sQ3_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f258])).
% 0.11/0.45 fof(f260,plain,(
% 0.11/0.45 ~function(relation_rng_restriction(sK16_skl,sK15_skl))|~relation(sK15_skl)|~function(sK15_skl)|sP0_prd(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl)|~sQ5_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f194,f158])).
% 0.11/0.45 fof(f262,definition,(
% 0.11/0.45 sQ13_spl <=> (sP0_prd(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f263,plain,(
% 0.11/0.45 sP0_prd(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl)|~sQ13_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f262])).
% 0.11/0.45 fof(f265,plain,(
% 0.11/0.45 ~sQ1_spl|~sQ8_spl|~sQ9_spl|sQ13_spl|~sQ5_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f260,f176,f207,f210,f262,f193])).
% 0.11/0.45 fof(f266,plain,(
% 0.11/0.45 apply(relation_rng_restriction(sK16_skl,sK15_skl),sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ10_spl|~sQ5_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f222,f194])).
% 0.11/0.45 fof(f268,plain,(
% 0.11/0.45 apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~relation(relation_rng_restriction(sK16_skl,sK15_skl))|~function(relation_rng_restriction(sK16_skl,sK15_skl))|one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))|~sQ10_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f222,f51])).
% 0.11/0.45 fof(f269,plain,(
% 0.11/0.45 apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.11/0.45 inference(backward_demodulation,[status(thm)],[f266,f180])).
% 0.11/0.45 fof(f274,definition,(
% 0.11/0.45 sQ15_spl <=> (apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl))))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f275,plain,(
% 0.11/0.45 apply(relation_rng_restriction(sK16_skl,sK15_skl),sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ15_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f274])).
% 0.11/0.45 fof(f277,plain,(
% 0.11/0.45 sQ15_spl|~sQ0_spl|~sQ1_spl|sQ3_spl|~sQ10_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f268,f274,f173,f176,f187,f221])).
% 0.11/0.45 fof(f278,plain,(
% 0.11/0.45 apply(sK15_skl,sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)))=apply(sK15_skl,sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)))|~sQ15_spl|~sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.11/0.45 inference(backward_demodulation,[status(thm)],[f275,f269])).
% 0.11/0.45 fof(f286,plain,(
% 0.11/0.45 ~relation(sK15_skl)|~function(sK15_skl)|~one_to_one(sK15_skl)|~in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|~in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl))=sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl))|~sQ15_spl|~sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.11/0.45 inference(resolution,[status(thm)],[f278,f50])).
% 0.11/0.45 fof(f290,definition,(
% 0.11/0.45 sQ16_spl <=> (one_to_one(sK15_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f292,plain,(
% 0.11/0.45 ~one_to_one(sK15_skl)|sQ16_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f290])).
% 0.11/0.46 fof(f293,definition,(
% 0.11/0.46 sQ17_spl <=> (in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl)))),
% 0.11/0.46 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.11/0.46 fof(f295,plain,(
% 0.11/0.46 ~in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|sQ17_spl),
% 0.11/0.46 inference(component_clause,[status(thm)],[f293])).
% 0.11/0.46 fof(f296,definition,(
% 0.11/0.46 sQ18_spl <=> (in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl)))),
% 0.11/0.46 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.11/0.46 fof(f298,plain,(
% 0.11/0.46 ~in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|sQ18_spl),
% 0.11/0.46 inference(component_clause,[status(thm)],[f296])).
% 0.11/0.46 fof(f299,plain,(
% 0.11/0.46 ~sQ8_spl|~sQ9_spl|~sQ16_spl|~sQ17_spl|~sQ18_spl|sQ6_spl|~sQ15_spl|~sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f286,f207,f210,f290,f293,f296,f196,f274,f221,f193,f179])).
% 0.11/0.46 fof(f344,plain,(
% 0.11/0.46 ~relation(relation_rng_restriction(sK16_skl,sK15_skl))|~function(relation_rng_restriction(sK16_skl,sK15_skl))|one_to_one(relation_rng_restriction(sK16_skl,sK15_skl))|sQ4_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f192,f51])).
% 0.11/0.46 fof(f346,plain,(
% 0.11/0.46 ~sQ0_spl|~sQ1_spl|sQ3_spl|sQ4_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f344,f173,f176,f187,f190])).
% 0.11/0.46 fof(f349,plain,(
% 0.11/0.46 ~function(relation_rng_restriction(sK16_skl,sK15_skl))|~relation(sK15_skl)|~function(sK15_skl)|sP0_prd(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl)|~sQ4_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f191,f158])).
% 0.11/0.46 fof(f352,definition,(
% 0.11/0.46 sQ23_spl <=> (sP0_prd(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl))),
% 0.11/0.46 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.11/0.46 fof(f353,plain,(
% 0.11/0.46 sP0_prd(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),sK15_skl,sK16_skl)|~sQ23_spl),
% 0.11/0.46 inference(component_clause,[status(thm)],[f352])).
% 0.11/0.46 fof(f355,plain,(
% 0.11/0.46 ~sQ1_spl|~sQ8_spl|~sQ9_spl|sQ23_spl|~sQ4_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f349,f176,f207,f210,f352,f190])).
% 0.11/0.46 fof(f545,plain,(
% 0.11/0.46 in(sK1_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|~sQ13_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f153,f263])).
% 0.11/0.46 fof(f547,plain,(
% 0.11/0.46 in(sK0_skl(relation_rng_restriction(sK16_skl,sK15_skl)),relation_dom(sK15_skl))|~sQ23_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f153,f353])).
% 0.11/0.46 fof(f549,plain,(
% 0.11/0.46 $false|sQ18_spl|~sQ13_spl),
% 0.11/0.46 inference(forward_subsumption_resolution,[status(thm)],[f545,f298])).
% 0.11/0.46 fof(f550,plain,(
% 0.11/0.46 sQ18_spl|~sQ13_spl),
% 0.11/0.46 inference(contradiction_clause,[status(thm)],[f549])).
% 0.11/0.46 fof(f553,plain,(
% 0.11/0.46 $false|sQ16_spl),
% 0.11/0.46 inference(forward_subsumption_resolution,[status(thm)],[f292,f149])).
% 0.11/0.46 fof(f554,plain,(
% 0.11/0.46 sQ16_spl),
% 0.11/0.46 inference(contradiction_clause,[status(thm)],[f553])).
% 0.11/0.46 fof(f555,plain,(
% 0.11/0.46 $false|~sQ23_spl|sQ17_spl),
% 0.11/0.46 inference(forward_subsumption_resolution,[status(thm)],[f295,f547])).
% 0.11/0.46 fof(f556,plain,(
% 0.11/0.46 ~sQ23_spl|sQ17_spl),
% 0.11/0.46 inference(contradiction_clause,[status(thm)],[f555])).
% 0.11/0.46 fof(f557,plain,(
% 0.11/0.46 $false),
% 0.11/0.46 inference(sat_refutation,[status(thm)],[f182,f213,f215,f218,f224,f227,f235,f257,f259,f265,f277,f299,f346,f355,f550,f554,f556])).
% 0.11/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.47 % Elapsed time: 0.104150 seconds
% 0.11/0.47 % CPU time: 0.563963 seconds
% 0.11/0.47 % Total memory used: 95.363 MB
% 0.11/0.47 % Net memory used: 94.715 MB
%------------------------------------------------------------------------------