%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU031+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 : n003.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 0.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU031+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.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 05:49:01 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f5,axiom,(
% 0.14/0.42 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f21,axiom,(
% 0.14/0.42 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> (! [D] :( ( relation(D)& function(D) )=> ( ( relation_rng(B) = A& relation_composition(B,C) = identity_relation(relation_dom(D))& relation_composition(C,D) = identity_relation(A) )=> D = B ) ) )) )) )),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f37,axiom,(
% 0.14/0.42 (! [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.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f39,axiom,(
% 0.14/0.42 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A))& relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A)) ) ) ) )),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f40,conjecture,(
% 0.14/0.42 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( one_to_one(A)& relation_rng(B) = relation_dom(A)& relation_composition(B,A) = identity_relation(relation_rng(A)) )=> B = function_inverse(A) ) ) )) )),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f41,negated_conjecture,(
% 0.14/0.42 ~((! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( one_to_one(A)& relation_rng(B) = relation_dom(A)& relation_composition(B,A) = identity_relation(relation_rng(A)) )=> B = function_inverse(A) ) ) )) ))),
% 0.14/0.42 inference(negated_conjecture,[status(cth)],[f40])).
% 0.14/0.42 fof(f55,plain,(
% 0.14/0.42 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.42 fof(f56,plain,(
% 0.14/0.42 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/0.42 fof(f57,plain,(
% 0.14/0.42 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/0.42 fof(f92,plain,(
% 0.14/0.42 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(![D]: ((~relation(D)|~function(D))|(((~relation_rng(B)=A|~relation_composition(B,C)=identity_relation(relation_dom(D)))|~relation_composition(C,D)=identity_relation(A))|D=B))))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.14/0.42 fof(f93,plain,(
% 0.14/0.42 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(![D]: ((~relation(D)|~function(D))|((![A]: ((~relation_rng(B)=A|~relation_composition(B,C)=identity_relation(relation_dom(D)))|~relation_composition(C,D)=identity_relation(A)))|D=B))))))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f92])).
% 0.14/0.42 fof(f94,plain,(
% 0.14/0.42 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation(X2)|~function(X2)|~relation_rng(X0)=X3|~relation_composition(X0,X1)=identity_relation(relation_dom(X2))|~relation_composition(X1,X2)=identity_relation(X3)|X2=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f93])).
% 0.14/0.42 fof(f139,plain,(
% 0.14/0.42 ![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.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.14/0.42 fof(f140,plain,(
% 0.14/0.42 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f139])).
% 0.14/0.42 fof(f145,plain,(
% 0.14/0.42 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_composition(A,function_inverse(A))=identity_relation(relation_dom(A))&relation_composition(function_inverse(A),A)=identity_relation(relation_rng(A)))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.14/0.42 fof(f146,plain,(
% 0.14/0.42 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_composition(X0,function_inverse(X0))=identity_relation(relation_dom(X0)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f145])).
% 0.14/0.43 fof(f148,plain,(
% 0.14/0.43 (?[A]: ((relation(A)&function(A))&(?[B]: ((relation(B)&function(B))&(((one_to_one(A)&relation_rng(B)=relation_dom(A))&relation_composition(B,A)=identity_relation(relation_rng(A)))&~B=function_inverse(A))))))),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.14/0.43 fof(f149,plain,(
% 0.14/0.43 ((relation(sK11_skl)&function(sK11_skl))&((relation(sK12_skl)&function(sK12_skl))&(((one_to_one(sK11_skl)&relation_rng(sK12_skl)=relation_dom(sK11_skl))&relation_composition(sK12_skl,sK11_skl)=identity_relation(relation_rng(sK11_skl)))&~sK12_skl=function_inverse(sK11_skl))))),
% 0.14/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f148])).
% 0.14/0.43 fof(f150,plain,(
% 0.14/0.43 relation(sK11_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f151,plain,(
% 0.14/0.43 function(sK11_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f152,plain,(
% 0.14/0.43 relation(sK12_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f153,plain,(
% 0.14/0.43 function(sK12_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f154,plain,(
% 0.14/0.43 one_to_one(sK11_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f155,plain,(
% 0.14/0.43 relation_rng(sK12_skl)=relation_dom(sK11_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f156,plain,(
% 0.14/0.43 relation_composition(sK12_skl,sK11_skl)=identity_relation(relation_rng(sK11_skl))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f157,plain,(
% 0.14/0.43 ~sK12_skl=function_inverse(sK11_skl)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f149])).
% 0.14/0.43 fof(f166,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation(X2)|~function(X2)|~relation_composition(X0,X1)=identity_relation(relation_dom(X2))|~relation_composition(X1,X2)=identity_relation(relation_rng(X0))|X2=X0)),
% 0.14/0.43 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 0.14/0.43 fof(f188,definition,(
% 0.14/0.43 sQ4_spl <=> (relation(sK12_skl))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f190,plain,(
% 0.14/0.43 ~relation(sK12_skl)|sQ4_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f188])).
% 0.14/0.43 fof(f191,definition,(
% 0.14/0.43 sQ5_spl <=> (relation(sK11_skl))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f193,plain,(
% 0.14/0.43 ~relation(sK11_skl)|sQ5_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f191])).
% 0.14/0.43 fof(f212,plain,(
% 0.14/0.43 $false|sQ4_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f190,f152])).
% 0.14/0.43 fof(f213,plain,(
% 0.14/0.43 sQ4_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f212])).
% 0.14/0.43 fof(f214,plain,(
% 0.14/0.43 $false|sQ5_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f193,f150])).
% 0.14/0.43 fof(f215,plain,(
% 0.14/0.43 sQ5_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f214])).
% 0.14/0.43 fof(f221,definition,(
% 0.14/0.43 sQ9_spl <=> (function(sK12_skl))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f223,plain,(
% 0.14/0.43 ~function(sK12_skl)|sQ9_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f221])).
% 0.14/0.43 fof(f224,definition,(
% 0.14/0.43 sQ10_spl <=> (function(sK11_skl))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f226,plain,(
% 0.14/0.43 ~function(sK11_skl)|sQ10_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f224])).
% 0.14/0.43 fof(f267,plain,(
% 0.14/0.43 ![X0]: (~relation(sK12_skl)|~function(sK12_skl)|~relation(sK11_skl)|~function(sK11_skl)|~relation(X0)|~function(X0)|~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_dom(X0))|~relation_composition(sK11_skl,X0)=identity_relation(relation_rng(sK12_skl))|X0=sK12_skl)),
% 0.14/0.43 inference(paramodulation,[status(thm)],[f156,f166])).
% 0.14/0.43 fof(f268,definition,(
% 0.14/0.43 ![X0]: (sQ15_spl <=> (~relation(X0)|~function(X0)|~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_dom(X0))|~relation_composition(sK11_skl,X0)=identity_relation(relation_rng(sK12_skl))|X0=sK12_skl))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f269,plain,(
% 0.14/0.43 ![X0]: (~relation(X0)|~function(X0)|~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_dom(X0))|~relation_composition(sK11_skl,X0)=identity_relation(relation_rng(sK12_skl))|X0=sK12_skl|~sQ15_spl)),
% 0.14/0.43 inference(component_clause,[status(thm)],[f268])).
% 0.14/0.43 fof(f271,plain,(
% 0.14/0.43 ~sQ4_spl|~sQ9_spl|~sQ5_spl|~sQ10_spl|sQ15_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f267,f188,f221,f191,f224,f268])).
% 0.14/0.43 fof(f272,plain,(
% 0.14/0.43 $false|sQ10_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f226,f151])).
% 0.14/0.43 fof(f273,plain,(
% 0.14/0.43 sQ10_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f272])).
% 0.14/0.43 fof(f274,plain,(
% 0.14/0.43 $false|sQ9_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f223,f153])).
% 0.14/0.43 fof(f275,plain,(
% 0.14/0.43 sQ9_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f274])).
% 0.14/0.43 fof(f276,plain,(
% 0.14/0.43 ![X0]: (~relation(X0)|~function(X0)|~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_dom(X0))|~relation_composition(sK11_skl,X0)=identity_relation(relation_dom(sK11_skl))|X0=sK12_skl|~sQ15_spl)),
% 0.14/0.43 inference(forward_demodulation,[status(thm)],[f155,f269])).
% 0.14/0.43 fof(f294,plain,(
% 0.14/0.43 ~relation(sK11_skl)|~function(sK11_skl)|relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))),
% 0.14/0.43 inference(resolution,[status(thm)],[f140,f154])).
% 0.14/0.43 fof(f352,definition,(
% 0.14/0.43 sQ32_spl <=> (relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f353,plain,(
% 0.14/0.43 relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))|~sQ32_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f352])).
% 0.14/0.43 fof(f355,plain,(
% 0.14/0.43 ~sQ5_spl|~sQ10_spl|sQ32_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f294,f191,f224,f352])).
% 0.14/0.43 fof(f499,plain,(
% 0.14/0.43 ~relation(sK11_skl)|~function(sK11_skl)|relation_composition(sK11_skl,function_inverse(sK11_skl))=identity_relation(relation_dom(sK11_skl))),
% 0.14/0.43 inference(resolution,[status(thm)],[f146,f154])).
% 0.14/0.43 fof(f503,definition,(
% 0.14/0.43 sQ42_spl <=> (relation_composition(sK11_skl,function_inverse(sK11_skl))=identity_relation(relation_dom(sK11_skl)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f506,plain,(
% 0.14/0.43 ~sQ5_spl|~sQ10_spl|sQ42_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f499,f191,f224,f503])).
% 0.14/0.43 fof(f610,definition,(
% 0.14/0.43 sQ53_spl <=> (relation(function_inverse(sK11_skl)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f612,plain,(
% 0.14/0.43 ~relation(function_inverse(sK11_skl))|sQ53_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f610])).
% 0.14/0.43 fof(f613,definition,(
% 0.14/0.43 sQ54_spl <=> (function(function_inverse(sK11_skl)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f615,plain,(
% 0.14/0.43 ~function(function_inverse(sK11_skl))|sQ54_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f613])).
% 0.14/0.43 fof(f626,plain,(
% 0.14/0.43 ~relation(sK11_skl)|~function(sK11_skl)|sQ53_spl),
% 0.14/0.43 inference(resolution,[status(thm)],[f612,f56])).
% 0.14/0.43 fof(f628,plain,(
% 0.14/0.43 ~sQ5_spl|~sQ10_spl|sQ53_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f626,f191,f224,f610])).
% 0.14/0.43 fof(f629,plain,(
% 0.14/0.43 ~relation(function_inverse(sK11_skl))|~function(function_inverse(sK11_skl))|~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_rng(sK11_skl))|~relation_composition(sK11_skl,function_inverse(sK11_skl))=identity_relation(relation_dom(sK11_skl))|function_inverse(sK11_skl)=sK12_skl|~sQ15_spl|~sQ32_spl),
% 0.14/0.43 inference(paramodulation,[status(thm)],[f353,f276])).
% 0.14/0.43 fof(f630,definition,(
% 0.14/0.43 sQ57_spl <=> (identity_relation(relation_rng(sK11_skl))=identity_relation(relation_rng(sK11_skl)))),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f632,plain,(
% 0.14/0.43 ~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_rng(sK11_skl))|sQ57_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f630])).
% 0.14/0.43 fof(f633,definition,(
% 0.14/0.43 sQ58_spl <=> (function_inverse(sK11_skl)=sK12_skl)),
% 0.14/0.43 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/0.43 fof(f634,plain,(
% 0.14/0.43 function_inverse(sK11_skl)=sK12_skl|~sQ58_spl),
% 0.14/0.43 inference(component_clause,[status(thm)],[f633])).
% 0.14/0.43 fof(f636,plain,(
% 0.14/0.43 ~sQ53_spl|~sQ54_spl|~sQ57_spl|~sQ42_spl|sQ58_spl|~sQ15_spl|~sQ32_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f629,f610,f613,f630,f503,f633,f268,f352])).
% 0.14/0.43 fof(f876,plain,(
% 0.14/0.43 $false|~sQ58_spl),
% 0.14/0.43 inference(forward_subsumption_resolution,[status(thm)],[f634,f157])).
% 0.14/0.43 fof(f877,plain,(
% 0.14/0.43 ~sQ58_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f876])).
% 0.14/0.43 fof(f879,plain,(
% 0.14/0.43 ~relation(sK11_skl)|~function(sK11_skl)|sQ54_spl),
% 0.14/0.43 inference(resolution,[status(thm)],[f615,f57])).
% 0.14/0.43 fof(f880,plain,(
% 0.14/0.43 ~sQ5_spl|~sQ10_spl|sQ54_spl),
% 0.14/0.43 inference(split_clause,[status(thm)],[f879,f191,f224,f613])).
% 0.14/0.43 fof(f881,plain,(
% 0.14/0.43 $false|sQ57_spl),
% 0.14/0.43 inference(trivial_equality_resolution,[status(thm)],[f632])).
% 0.14/0.43 fof(f882,plain,(
% 0.14/0.43 sQ57_spl),
% 0.14/0.43 inference(contradiction_clause,[status(thm)],[f881])).
% 0.14/0.43 fof(f883,plain,(
% 0.14/0.43 $false),
% 0.14/0.43 inference(sat_refutation,[status(thm)],[f213,f215,f271,f273,f275,f355,f506,f628,f636,f877,f880,f882])).
% 0.14/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.45 % Elapsed time: 0.086167 seconds
% 0.14/0.45 % CPU time: 0.360368 seconds
% 0.14/0.45 % Total memory used: 108.988 MB
% 0.14/0.45 % Net memory used: 108.577 MB
%------------------------------------------------------------------------------