%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU030+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 : n026.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.19s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU030+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n026.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:50:09 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 0.19/0.50 % Refutation found
% 0.19/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.50 fof(f5,axiom,(
% 0.19/0.50 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.19/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f21,axiom,(
% 0.19/0.50 (! [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.19/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f37,axiom,(
% 0.19/0.50 (! [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.19/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f39,axiom,(
% 0.19/0.50 (! [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.19/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f40,conjecture,(
% 0.19/0.50 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( one_to_one(A)& relation_rng(A) = relation_dom(B)& relation_composition(A,B) = identity_relation(relation_dom(A)) )=> B = function_inverse(A) ) ) )) )),
% 0.19/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.50 fof(f41,negated_conjecture,(
% 0.19/0.50 ~((! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( one_to_one(A)& relation_rng(A) = relation_dom(B)& relation_composition(A,B) = identity_relation(relation_dom(A)) )=> B = function_inverse(A) ) ) )) ))),
% 0.19/0.50 inference(negated_conjecture,[status(cth)],[f40])).
% 0.19/0.50 fof(f55,plain,(
% 0.19/0.50 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.19/0.50 fof(f56,plain,(
% 0.19/0.50 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f55])).
% 0.19/0.50 fof(f57,plain,(
% 0.19/0.50 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f55])).
% 0.19/0.50 fof(f92,plain,(
% 0.19/0.50 ![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.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.19/0.50 fof(f93,plain,(
% 0.19/0.50 ![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.19/0.50 inference(miniscoping,[status(thm)],[f92])).
% 0.19/0.50 fof(f94,plain,(
% 0.19/0.50 ![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.19/0.50 inference(cnf_transformation,[status(thm)],[f93])).
% 0.19/0.50 fof(f139,plain,(
% 0.19/0.50 ![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.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.19/0.50 fof(f141,plain,(
% 0.19/0.50 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(X0)=relation_rng(function_inverse(X0)))),
% 0.19/0.50 inference(cnf_transformation,[status(thm)],[f139])).
% 0.19/0.50 fof(f145,plain,(
% 0.19/0.50 ![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.19/0.50 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.19/0.50 fof(f147,plain,(
% 0.19/0.50 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_composition(function_inverse(X0),X0)=identity_relation(relation_rng(X0)))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f145])).
% 0.19/0.51 fof(f148,plain,(
% 0.19/0.51 (?[A]: ((relation(A)&function(A))&(?[B]: ((relation(B)&function(B))&(((one_to_one(A)&relation_rng(A)=relation_dom(B))&relation_composition(A,B)=identity_relation(relation_dom(A)))&~B=function_inverse(A))))))),
% 0.19/0.51 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.19/0.51 fof(f149,plain,(
% 0.19/0.51 ((relation(sK11_skl)&function(sK11_skl))&((relation(sK12_skl)&function(sK12_skl))&(((one_to_one(sK11_skl)&relation_rng(sK11_skl)=relation_dom(sK12_skl))&relation_composition(sK11_skl,sK12_skl)=identity_relation(relation_dom(sK11_skl)))&~sK12_skl=function_inverse(sK11_skl))))),
% 0.19/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f148])).
% 0.19/0.51 fof(f150,plain,(
% 0.19/0.51 relation(sK11_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f151,plain,(
% 0.19/0.51 function(sK11_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f152,plain,(
% 0.19/0.51 relation(sK12_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f153,plain,(
% 0.19/0.51 function(sK12_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f154,plain,(
% 0.19/0.51 one_to_one(sK11_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f155,plain,(
% 0.19/0.51 relation_rng(sK11_skl)=relation_dom(sK12_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f156,plain,(
% 0.19/0.51 relation_composition(sK11_skl,sK12_skl)=identity_relation(relation_dom(sK11_skl))),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f157,plain,(
% 0.19/0.51 ~sK12_skl=function_inverse(sK11_skl)),
% 0.19/0.51 inference(cnf_transformation,[status(thm)],[f149])).
% 0.19/0.51 fof(f166,plain,(
% 0.19/0.51 ![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.19/0.51 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 0.19/0.51 fof(f188,definition,(
% 0.19/0.51 sQ4_spl <=> (relation(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f190,plain,(
% 0.19/0.51 ~relation(sK11_skl)|sQ4_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f188])).
% 0.19/0.51 fof(f191,definition,(
% 0.19/0.51 sQ5_spl <=> (relation(sK12_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f193,plain,(
% 0.19/0.51 ~relation(sK12_skl)|sQ5_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f191])).
% 0.19/0.51 fof(f212,plain,(
% 0.19/0.51 $false|sQ4_spl),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f190,f150])).
% 0.19/0.51 fof(f213,plain,(
% 0.19/0.51 sQ4_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f212])).
% 0.19/0.51 fof(f214,plain,(
% 0.19/0.51 $false|sQ5_spl),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f193,f152])).
% 0.19/0.51 fof(f215,plain,(
% 0.19/0.51 sQ5_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f214])).
% 0.19/0.51 fof(f221,definition,(
% 0.19/0.51 sQ9_spl <=> (function(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f223,plain,(
% 0.19/0.51 ~function(sK11_skl)|sQ9_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f221])).
% 0.19/0.51 fof(f224,definition,(
% 0.19/0.51 sQ10_spl <=> (function(sK12_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f226,plain,(
% 0.19/0.51 ~function(sK12_skl)|sQ10_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f224])).
% 0.19/0.51 fof(f268,plain,(
% 0.19/0.51 ![X0]: (~relation(X0)|~function(X0)|~relation(sK11_skl)|~function(sK11_skl)|~relation(sK12_skl)|~function(sK12_skl)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(sK12_skl))|~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_rng(X0))|sK12_skl=X0)),
% 0.19/0.51 inference(paramodulation,[status(thm)],[f156,f166])).
% 0.19/0.51 fof(f269,definition,(
% 0.19/0.51 ![X0]: (sQ15_spl <=> (~relation(X0)|~function(X0)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(sK12_skl))|~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_rng(X0))|sK12_skl=X0))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f270,plain,(
% 0.19/0.51 ![X0]: (~relation(X0)|~function(X0)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(sK12_skl))|~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_rng(X0))|sK12_skl=X0|~sQ15_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f269])).
% 0.19/0.51 fof(f272,plain,(
% 0.19/0.51 sQ15_spl|~sQ4_spl|~sQ9_spl|~sQ5_spl|~sQ10_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f268,f269,f188,f221,f191,f224])).
% 0.19/0.51 fof(f273,plain,(
% 0.19/0.51 $false|sQ10_spl),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f226,f153])).
% 0.19/0.51 fof(f274,plain,(
% 0.19/0.51 sQ10_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f273])).
% 0.19/0.51 fof(f275,plain,(
% 0.19/0.51 $false|sQ9_spl),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f223,f151])).
% 0.19/0.51 fof(f276,plain,(
% 0.19/0.51 sQ9_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f275])).
% 0.19/0.51 fof(f277,plain,(
% 0.19/0.51 ![X0]: (~relation(X0)|~function(X0)|~relation_composition(X0,sK11_skl)=identity_relation(relation_rng(sK11_skl))|~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_rng(X0))|sK12_skl=X0|~sQ15_spl)),
% 0.19/0.51 inference(forward_demodulation,[status(thm)],[f155,f270])).
% 0.19/0.51 fof(f368,plain,(
% 0.19/0.51 ~relation(sK11_skl)|~function(sK11_skl)|relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))),
% 0.19/0.51 inference(resolution,[status(thm)],[f141,f154])).
% 0.19/0.51 fof(f392,definition,(
% 0.19/0.51 sQ37_spl <=> (relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f393,plain,(
% 0.19/0.51 relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))|~sQ37_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f392])).
% 0.19/0.51 fof(f395,plain,(
% 0.19/0.51 ~sQ4_spl|~sQ9_spl|sQ37_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f368,f188,f221,f392])).
% 0.19/0.51 fof(f440,definition,(
% 0.19/0.51 sQ39_spl <=> (relation(function_inverse(sK11_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f442,plain,(
% 0.19/0.51 ~relation(function_inverse(sK11_skl))|sQ39_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f440])).
% 0.19/0.51 fof(f444,plain,(
% 0.19/0.51 ~relation(sK11_skl)|~function(sK11_skl)|sQ39_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f442,f56])).
% 0.19/0.51 fof(f446,plain,(
% 0.19/0.51 ~sQ4_spl|~sQ9_spl|sQ39_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f444,f188,f221,f440])).
% 0.19/0.51 fof(f500,plain,(
% 0.19/0.51 ~relation(sK11_skl)|~function(sK11_skl)|relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl))),
% 0.19/0.51 inference(resolution,[status(thm)],[f147,f154])).
% 0.19/0.51 fof(f515,definition,(
% 0.19/0.51 sQ49_spl <=> (relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f518,plain,(
% 0.19/0.51 ~sQ4_spl|~sQ9_spl|sQ49_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f500,f188,f221,f515])).
% 0.19/0.51 fof(f696,definition,(
% 0.19/0.51 sQ58_spl <=> (function(function_inverse(sK11_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f698,plain,(
% 0.19/0.51 ~function(function_inverse(sK11_skl))|sQ58_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f696])).
% 0.19/0.51 fof(f712,plain,(
% 0.19/0.51 ~relation(sK11_skl)|~function(sK11_skl)|sQ58_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f698,f57])).
% 0.19/0.51 fof(f713,plain,(
% 0.19/0.51 ~sQ4_spl|~sQ9_spl|sQ58_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f712,f188,f221,f696])).
% 0.19/0.51 fof(f1145,plain,(
% 0.19/0.51 ~relation(function_inverse(sK11_skl))|~function(function_inverse(sK11_skl))|~relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl))|~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_dom(sK11_skl))|sK12_skl=function_inverse(sK11_skl)|~sQ15_spl|~sQ37_spl),
% 0.19/0.51 inference(paramodulation,[status(thm)],[f393,f277])).
% 0.19/0.51 fof(f1146,definition,(
% 0.19/0.51 sQ107_spl <=> (identity_relation(relation_dom(sK11_skl))=identity_relation(relation_dom(sK11_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f1148,plain,(
% 0.19/0.51 ~identity_relation(relation_dom(sK11_skl))=identity_relation(relation_dom(sK11_skl))|sQ107_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f1146])).
% 0.19/0.51 fof(f1149,definition,(
% 0.19/0.51 sQ108_spl <=> (sK12_skl=function_inverse(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f1150,plain,(
% 0.19/0.51 sK12_skl=function_inverse(sK11_skl)|~sQ108_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f1149])).
% 0.19/0.51 fof(f1152,plain,(
% 0.19/0.51 ~sQ39_spl|~sQ58_spl|~sQ49_spl|~sQ107_spl|sQ108_spl|~sQ15_spl|~sQ37_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f1145,f440,f696,f515,f1146,f1149,f269,f392])).
% 0.19/0.51 fof(f1153,plain,(
% 0.19/0.51 $false|sQ107_spl),
% 0.19/0.51 inference(trivial_equality_resolution,[status(thm)],[f1148])).
% 0.19/0.51 fof(f1154,plain,(
% 0.19/0.51 sQ107_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f1153])).
% 0.19/0.51 fof(f1155,plain,(
% 0.19/0.51 $false|~sQ108_spl),
% 0.19/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1150,f157])).
% 0.19/0.51 fof(f1156,plain,(
% 0.19/0.51 ~sQ108_spl),
% 0.19/0.51 inference(contradiction_clause,[status(thm)],[f1155])).
% 0.19/0.51 fof(f1157,plain,(
% 0.19/0.51 $false),
% 0.19/0.51 inference(sat_refutation,[status(thm)],[f213,f215,f272,f274,f276,f395,f446,f518,f713,f1152,f1154,f1156])).
% 0.19/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.53 % Elapsed time: 0.076452 seconds
% 0.19/0.53 % CPU time: 0.324135 seconds
% 0.19/0.53 % Total memory used: 74.435 MB
% 0.19/0.53 % Net memory used: 74.180 MB
%------------------------------------------------------------------------------