%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU025+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:35 PM UTC 2026
% Result : Theorem 0.28s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU025+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n020.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 05:48:32 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 0.28/0.58 % Refutation found
% 0.28/0.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.58 fof(f5,axiom,(
% 0.28/0.58 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f23,axiom,(
% 0.28/0.58 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f27,axiom,(
% 0.28/0.58 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f29,axiom,(
% 0.28/0.58 (! [A,B] : subset(A,A) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f33,axiom,(
% 0.28/0.58 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(relation_rng(A),relation_dom(B))=> relation_dom(relation_composition(A,B)) = relation_dom(A) ) ) )) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f34,axiom,(
% 0.28/0.58 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(relation_dom(A),relation_rng(B))=> relation_rng(relation_composition(B,A)) = relation_rng(A) ) ) )) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f36,axiom,(
% 0.28/0.58 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_rng(A) = relation_dom(function_inverse(A))& relation_dom(A) = relation_rng(function_inverse(A)) ) ) ) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f37,conjecture,(
% 0.28/0.58 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A)& relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ) )),
% 0.28/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.58 fof(f38,negated_conjecture,(
% 0.28/0.58 ~((! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_dom(relation_composition(A,function_inverse(A))) = relation_dom(A)& relation_rng(relation_composition(A,function_inverse(A))) = relation_dom(A) ) ) ) ))),
% 0.28/0.58 inference(negated_conjecture,[status(cth)],[f37])).
% 0.28/0.58 fof(f53,plain,(
% 0.28/0.58 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.28/0.58 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.28/0.58 fof(f54,plain,(
% 0.28/0.58 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f53])).
% 0.28/0.58 fof(f98,plain,(
% 0.28/0.58 ((relation(sK5_skl)&empty(sK5_skl))&function(sK5_skl))),
% 0.28/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f23])).
% 0.28/0.58 fof(f100,plain,(
% 0.28/0.58 empty(sK5_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f98])).
% 0.28/0.58 fof(f110,plain,(
% 0.28/0.58 ((relation(sK9_skl)&function(sK9_skl))&one_to_one(sK9_skl))),
% 0.28/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f27])).
% 0.28/0.58 fof(f111,plain,(
% 0.28/0.58 relation(sK9_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f110])).
% 0.28/0.58 fof(f112,plain,(
% 0.28/0.58 function(sK9_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f110])).
% 0.28/0.58 fof(f117,plain,(
% 0.28/0.58 ![A]: subset(A,A)),
% 0.28/0.58 inference(miniscoping,[status(thm)],[f29])).
% 0.28/0.58 fof(f118,plain,(
% 0.28/0.58 ![X0]: (subset(X0,X0))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f117])).
% 0.28/0.58 fof(f127,plain,(
% 0.28/0.58 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(relation_rng(A),relation_dom(B))|relation_dom(relation_composition(A,B))=relation_dom(A)))))),
% 0.28/0.58 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.28/0.58 fof(f128,plain,(
% 0.28/0.58 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(relation_rng(X0),relation_dom(X1))|relation_dom(relation_composition(X0,X1))=relation_dom(X0))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f127])).
% 0.28/0.58 fof(f129,plain,(
% 0.28/0.58 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(relation_dom(A),relation_rng(B))|relation_rng(relation_composition(B,A))=relation_rng(A)))))),
% 0.28/0.58 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.28/0.58 fof(f130,plain,(
% 0.28/0.58 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(relation_dom(X0),relation_rng(X1))|relation_rng(relation_composition(X1,X0))=relation_rng(X0))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f129])).
% 0.28/0.58 fof(f134,plain,(
% 0.28/0.58 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_rng(A)=relation_dom(function_inverse(A))&relation_dom(A)=relation_rng(function_inverse(A)))))),
% 0.28/0.58 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.28/0.58 fof(f135,plain,(
% 0.28/0.58 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f134])).
% 0.28/0.58 fof(f136,plain,(
% 0.28/0.58 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(X0)=relation_rng(function_inverse(X0)))),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f134])).
% 0.28/0.58 fof(f137,plain,(
% 0.28/0.58 (?[A]: ((relation(A)&function(A))&(one_to_one(A)&(~relation_dom(relation_composition(A,function_inverse(A)))=relation_dom(A)|~relation_rng(relation_composition(A,function_inverse(A)))=relation_dom(A)))))),
% 0.28/0.58 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.28/0.58 fof(f138,plain,(
% 0.28/0.58 ((relation(sK11_skl)&function(sK11_skl))&(one_to_one(sK11_skl)&(~relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl)|~relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl))))),
% 0.28/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f137])).
% 0.28/0.58 fof(f139,plain,(
% 0.28/0.58 relation(sK11_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f138])).
% 0.28/0.58 fof(f140,plain,(
% 0.28/0.58 function(sK11_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f138])).
% 0.28/0.58 fof(f141,plain,(
% 0.28/0.58 one_to_one(sK11_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f138])).
% 0.28/0.58 fof(f142,plain,(
% 0.28/0.58 ~relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl)|~relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl)),
% 0.28/0.58 inference(cnf_transformation,[status(thm)],[f138])).
% 0.28/0.58 fof(f154,definition,(
% 0.28/0.58 sQ0_spl <=> (relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f157,definition,(
% 0.28/0.58 sQ1_spl <=> (relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f160,plain,(
% 0.28/0.58 ~sQ0_spl|~sQ1_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f142,f154,f157])).
% 0.28/0.58 fof(f170,plain,(
% 0.28/0.58 ~relation(sK11_skl)|~function(sK11_skl)|relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))),
% 0.28/0.58 inference(resolution,[status(thm)],[f135,f141])).
% 0.28/0.58 fof(f172,definition,(
% 0.28/0.58 sQ2_spl <=> (relation(sK11_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f174,plain,(
% 0.28/0.58 ~relation(sK11_skl)|sQ2_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f172])).
% 0.28/0.58 fof(f175,definition,(
% 0.28/0.58 sQ3_spl <=> (function(sK11_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f177,plain,(
% 0.28/0.58 ~function(sK11_skl)|sQ3_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f175])).
% 0.28/0.58 fof(f178,definition,(
% 0.28/0.58 sQ4_spl <=> (relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl)))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f179,plain,(
% 0.28/0.58 relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))|~sQ4_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f178])).
% 0.28/0.58 fof(f181,plain,(
% 0.28/0.58 ~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f170,f172,f175,f178])).
% 0.28/0.58 fof(f194,definition,(
% 0.28/0.58 sQ7_spl <=> (relation(function_inverse(sK11_skl)))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f196,plain,(
% 0.28/0.58 ~relation(function_inverse(sK11_skl))|sQ7_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f194])).
% 0.28/0.58 fof(f202,plain,(
% 0.28/0.58 $false|sQ3_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f177,f140])).
% 0.28/0.58 fof(f203,plain,(
% 0.28/0.58 sQ3_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f202])).
% 0.28/0.58 fof(f210,plain,(
% 0.28/0.58 ~relation(sK11_skl)|~function(sK11_skl)|sQ7_spl),
% 0.28/0.58 inference(resolution,[status(thm)],[f196,f54])).
% 0.28/0.58 fof(f211,plain,(
% 0.28/0.58 ~sQ2_spl|~sQ3_spl|sQ7_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f210,f172,f175,f194])).
% 0.28/0.58 fof(f212,plain,(
% 0.28/0.58 $false|sQ2_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f174,f139])).
% 0.28/0.58 fof(f213,plain,(
% 0.28/0.58 sQ2_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f212])).
% 0.28/0.58 fof(f214,plain,(
% 0.28/0.58 ~relation(sK11_skl)|~function(sK11_skl)|relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))),
% 0.28/0.58 inference(resolution,[status(thm)],[f136,f141])).
% 0.28/0.58 fof(f216,definition,(
% 0.28/0.58 sQ9_spl <=> (relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl)))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f217,plain,(
% 0.28/0.58 relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))|~sQ9_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f216])).
% 0.28/0.58 fof(f219,plain,(
% 0.28/0.58 ~sQ2_spl|~sQ3_spl|sQ9_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f214,f172,f175,f216])).
% 0.28/0.58 fof(f231,definition,(
% 0.28/0.58 sQ11_spl <=> (empty(sK5_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f233,plain,(
% 0.28/0.58 ~empty(sK5_skl)|sQ11_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f231])).
% 0.28/0.58 fof(f269,plain,(
% 0.28/0.58 $false|sQ11_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f233,f100])).
% 0.28/0.58 fof(f270,plain,(
% 0.28/0.58 sQ11_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f269])).
% 0.28/0.58 fof(f273,definition,(
% 0.28/0.58 sQ17_spl <=> (relation(sK9_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f275,plain,(
% 0.28/0.58 ~relation(sK9_skl)|sQ17_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f273])).
% 0.28/0.58 fof(f276,definition,(
% 0.28/0.58 sQ18_spl <=> (function(sK9_skl))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f278,plain,(
% 0.28/0.58 ~function(sK9_skl)|sQ18_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f276])).
% 0.28/0.58 fof(f287,plain,(
% 0.28/0.58 $false|sQ18_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f278,f112])).
% 0.28/0.58 fof(f288,plain,(
% 0.28/0.58 sQ18_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f287])).
% 0.28/0.58 fof(f289,plain,(
% 0.28/0.58 $false|sQ17_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f275,f111])).
% 0.28/0.58 fof(f290,plain,(
% 0.28/0.58 sQ17_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f289])).
% 0.28/0.58 fof(f364,plain,(
% 0.28/0.58 ![X0]: (~relation(X0)|~relation(function_inverse(sK11_skl))|~subset(relation_rng(X0),relation_rng(sK11_skl))|relation_dom(relation_composition(X0,function_inverse(sK11_skl)))=relation_dom(X0)|~sQ4_spl)),
% 0.28/0.58 inference(paramodulation,[status(thm)],[f179,f128])).
% 0.28/0.58 fof(f377,definition,(
% 0.28/0.58 ![X0]: (sQ32_spl <=> (~relation(X0)|~subset(relation_rng(X0),relation_rng(sK11_skl))|relation_dom(relation_composition(X0,function_inverse(sK11_skl)))=relation_dom(X0)))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f378,plain,(
% 0.28/0.58 ![X0]: (~relation(X0)|~subset(relation_rng(X0),relation_rng(sK11_skl))|relation_dom(relation_composition(X0,function_inverse(sK11_skl)))=relation_dom(X0)|~sQ32_spl)),
% 0.28/0.58 inference(component_clause,[status(thm)],[f377])).
% 0.28/0.58 fof(f380,plain,(
% 0.28/0.58 sQ32_spl|~sQ7_spl|~sQ4_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f364,f377,f194,f178])).
% 0.28/0.58 fof(f383,plain,(
% 0.28/0.58 ~relation(sK11_skl)|relation_dom(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl)|~sQ32_spl),
% 0.28/0.58 inference(resolution,[status(thm)],[f378,f118])).
% 0.28/0.58 fof(f386,plain,(
% 0.28/0.58 ~sQ2_spl|sQ0_spl|~sQ32_spl),
% 0.28/0.58 inference(split_clause,[status(thm)],[f383,f172,f154,f377])).
% 0.28/0.58 fof(f460,definition,(
% 0.28/0.58 sQ47_spl <=> (subset(relation_dom(sK11_skl),relation_dom(sK11_skl)))),
% 0.28/0.58 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.28/0.58 fof(f462,plain,(
% 0.28/0.58 ~subset(relation_dom(sK11_skl),relation_dom(sK11_skl))|sQ47_spl),
% 0.28/0.58 inference(component_clause,[status(thm)],[f460])).
% 0.28/0.58 fof(f467,plain,(
% 0.28/0.58 $false|sQ47_spl),
% 0.28/0.58 inference(forward_subsumption_resolution,[status(thm)],[f462,f118])).
% 0.28/0.58 fof(f468,plain,(
% 0.28/0.58 sQ47_spl),
% 0.28/0.58 inference(contradiction_clause,[status(thm)],[f467])).
% 0.28/0.58 fof(f474,plain,(
% 0.28/0.58 ![X0]: (~relation(function_inverse(sK11_skl))|~relation(X0)|~subset(relation_rng(sK11_skl),relation_rng(X0))|relation_rng(relation_composition(X0,function_inverse(sK11_skl)))=relation_rng(function_inverse(sK11_skl))|~sQ4_spl)),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f179,f130])).
% 0.28/0.59 fof(f489,definition,(
% 0.28/0.59 ![X0]: (sQ52_spl <=> (~relation(X0)|~subset(relation_rng(sK11_skl),relation_rng(X0))|relation_rng(relation_composition(X0,function_inverse(sK11_skl)))=relation_rng(function_inverse(sK11_skl))))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f490,plain,(
% 0.28/0.59 ![X0]: (~relation(X0)|~subset(relation_rng(sK11_skl),relation_rng(X0))|relation_rng(relation_composition(X0,function_inverse(sK11_skl)))=relation_rng(function_inverse(sK11_skl))|~sQ52_spl)),
% 0.28/0.59 inference(component_clause,[status(thm)],[f489])).
% 0.28/0.59 fof(f492,plain,(
% 0.28/0.59 ~sQ7_spl|sQ52_spl|~sQ4_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f474,f194,f489,f178])).
% 0.28/0.59 fof(f501,plain,(
% 0.28/0.59 ![X0]: (~relation(X0)|~subset(relation_rng(sK11_skl),relation_rng(X0))|relation_rng(relation_composition(X0,function_inverse(sK11_skl)))=relation_dom(sK11_skl)|~sQ9_spl|~sQ52_spl)),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f217,f490])).
% 0.28/0.59 fof(f676,plain,(
% 0.28/0.59 ~relation(sK11_skl)|relation_rng(relation_composition(sK11_skl,function_inverse(sK11_skl)))=relation_dom(sK11_skl)|~sQ9_spl|~sQ52_spl),
% 0.28/0.59 inference(resolution,[status(thm)],[f501,f118])).
% 0.28/0.59 fof(f679,plain,(
% 0.28/0.59 ~sQ2_spl|sQ1_spl|~sQ9_spl|~sQ52_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f676,f172,f157,f216,f489])).
% 0.28/0.59 fof(f694,plain,(
% 0.28/0.59 $false),
% 0.28/0.59 inference(sat_refutation,[status(thm)],[f160,f181,f203,f211,f213,f219,f270,f288,f290,f380,f386,f468,f492,f679])).
% 0.28/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.61 % Elapsed time: 0.147974 seconds
% 0.28/0.61 % CPU time: 0.832869 seconds
% 0.28/0.61 % Total memory used: 93.039 MB
% 0.28/0.61 % Net memory used: 92.244 MB
%------------------------------------------------------------------------------