%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU032+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 : n019.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.26s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU032+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n019.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 05:47:35 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.26/0.60 % Refutation found
% 0.26/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.26/0.60 fof(f5,axiom,(
% 0.26/0.60 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f36,axiom,(
% 0.26/0.60 (! [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.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f38,axiom,(
% 0.26/0.60 (! [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.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f39,axiom,(
% 0.26/0.60 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> one_to_one(function_inverse(A)) ) ) )),
% 0.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f40,axiom,(
% 0.26/0.60 (! [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.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f41,conjecture,(
% 0.26/0.60 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> function_inverse(function_inverse(A)) = A ) ) )),
% 0.26/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.60 fof(f42,negated_conjecture,(
% 0.26/0.60 ~((! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> function_inverse(function_inverse(A)) = A ) ) ))),
% 0.26/0.60 inference(negated_conjecture,[status(cth)],[f41])).
% 0.26/0.60 fof(f56,plain,(
% 0.26/0.60 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.26/0.60 fof(f57,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f56])).
% 0.26/0.60 fof(f58,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f56])).
% 0.26/0.60 fof(f137,plain,(
% 0.26/0.60 ![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.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.26/0.60 fof(f138,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f137])).
% 0.26/0.60 fof(f139,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(X0)=relation_rng(function_inverse(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f137])).
% 0.26/0.60 fof(f143,plain,(
% 0.26/0.60 ![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.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.26/0.60 fof(f145,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_composition(function_inverse(X0),X0)=identity_relation(relation_rng(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f143])).
% 0.26/0.60 fof(f146,plain,(
% 0.26/0.60 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|one_to_one(function_inverse(A))))),
% 0.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.26/0.60 fof(f147,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|one_to_one(function_inverse(X0)))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f146])).
% 0.26/0.60 fof(f148,plain,(
% 0.26/0.60 ![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.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.26/0.60 fof(f149,plain,(
% 0.26/0.60 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~one_to_one(X0)|~relation_rng(X0)=relation_dom(X1)|~relation_composition(X0,X1)=identity_relation(relation_dom(X0))|X1=function_inverse(X0))),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f148])).
% 0.26/0.60 fof(f150,plain,(
% 0.26/0.60 (?[A]: ((relation(A)&function(A))&(one_to_one(A)&~function_inverse(function_inverse(A))=A)))),
% 0.26/0.60 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.26/0.60 fof(f151,plain,(
% 0.26/0.60 ((relation(sK11_skl)&function(sK11_skl))&(one_to_one(sK11_skl)&~function_inverse(function_inverse(sK11_skl))=sK11_skl))),
% 0.26/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f150])).
% 0.26/0.60 fof(f152,plain,(
% 0.26/0.60 relation(sK11_skl)),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.26/0.60 fof(f153,plain,(
% 0.26/0.60 function(sK11_skl)),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.26/0.60 fof(f154,plain,(
% 0.26/0.60 one_to_one(sK11_skl)),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.26/0.60 fof(f155,plain,(
% 0.26/0.60 ~function_inverse(function_inverse(sK11_skl))=sK11_skl),
% 0.26/0.60 inference(cnf_transformation,[status(thm)],[f151])).
% 0.26/0.60 fof(f173,plain,(
% 0.26/0.60 ~function(sK11_skl)|relation(function_inverse(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f57,f152])).
% 0.26/0.60 fof(f174,definition,(
% 0.26/0.60 sQ2_spl <=> (function(sK11_skl))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f176,plain,(
% 0.26/0.60 ~function(sK11_skl)|sQ2_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f174])).
% 0.26/0.60 fof(f177,definition,(
% 0.26/0.60 sQ3_spl <=> (relation(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f180,plain,(
% 0.26/0.60 ~sQ2_spl|sQ3_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f173,f174,f177])).
% 0.26/0.60 fof(f181,plain,(
% 0.26/0.60 $false|sQ2_spl),
% 0.26/0.60 inference(forward_subsumption_resolution,[status(thm)],[f176,f153])).
% 0.26/0.60 fof(f182,plain,(
% 0.26/0.60 sQ2_spl),
% 0.26/0.60 inference(contradiction_clause,[status(thm)],[f181])).
% 0.26/0.60 fof(f183,plain,(
% 0.26/0.60 ~function(sK11_skl)|function(function_inverse(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f58,f152])).
% 0.26/0.60 fof(f184,definition,(
% 0.26/0.60 sQ4_spl <=> (function(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f187,plain,(
% 0.26/0.60 ~sQ2_spl|sQ4_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f183,f174,f184])).
% 0.26/0.60 fof(f188,plain,(
% 0.26/0.60 ~relation(sK11_skl)|~function(sK11_skl)|one_to_one(function_inverse(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f147,f154])).
% 0.26/0.60 fof(f189,definition,(
% 0.26/0.60 sQ5_spl <=> (relation(sK11_skl))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f191,plain,(
% 0.26/0.60 ~relation(sK11_skl)|sQ5_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f189])).
% 0.26/0.60 fof(f192,definition,(
% 0.26/0.60 sQ6_spl <=> (one_to_one(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f193,plain,(
% 0.26/0.60 one_to_one(function_inverse(sK11_skl))|~sQ6_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f192])).
% 0.26/0.60 fof(f195,plain,(
% 0.26/0.60 ~sQ5_spl|~sQ2_spl|sQ6_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f188,f189,f174,f192])).
% 0.26/0.60 fof(f196,plain,(
% 0.26/0.60 $false|sQ5_spl),
% 0.26/0.60 inference(forward_subsumption_resolution,[status(thm)],[f191,f152])).
% 0.26/0.60 fof(f197,plain,(
% 0.26/0.60 sQ5_spl),
% 0.26/0.60 inference(contradiction_clause,[status(thm)],[f196])).
% 0.26/0.60 fof(f907,plain,(
% 0.26/0.60 ~relation(sK11_skl)|~function(sK11_skl)|relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f138,f154])).
% 0.26/0.60 fof(f940,definition,(
% 0.26/0.60 sQ126_spl <=> (relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f941,plain,(
% 0.26/0.60 relation_rng(sK11_skl)=relation_dom(function_inverse(sK11_skl))|~sQ126_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f940])).
% 0.26/0.60 fof(f943,plain,(
% 0.26/0.60 ~sQ5_spl|~sQ2_spl|sQ126_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f907,f189,f174,f940])).
% 0.26/0.60 fof(f1032,plain,(
% 0.26/0.60 ~relation(sK11_skl)|~function(sK11_skl)|relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f139,f154])).
% 0.26/0.60 fof(f1070,definition,(
% 0.26/0.60 sQ150_spl <=> (relation_dom(sK11_skl)=relation_rng(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f1073,plain,(
% 0.26/0.60 ~sQ5_spl|~sQ2_spl|sQ150_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f1032,f189,f174,f1070])).
% 0.26/0.60 fof(f1138,plain,(
% 0.26/0.60 ~relation(sK11_skl)|~function(sK11_skl)|relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl))),
% 0.26/0.60 inference(resolution,[status(thm)],[f145,f154])).
% 0.26/0.60 fof(f1176,definition,(
% 0.26/0.60 sQ170_spl <=> (relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f1177,plain,(
% 0.26/0.60 relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_rng(sK11_skl))|~sQ170_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f1176])).
% 0.26/0.60 fof(f1179,plain,(
% 0.26/0.60 ~sQ5_spl|~sQ2_spl|sQ170_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f1138,f189,f174,f1176])).
% 0.26/0.60 fof(f1201,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~function(sK11_skl)|~one_to_one(X0)|~relation_rng(X0)=relation_dom(sK11_skl)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(X0))|sK11_skl=function_inverse(X0))),
% 0.26/0.60 inference(resolution,[status(thm)],[f149,f152])).
% 0.26/0.60 fof(f1277,definition,(
% 0.26/0.60 ![X0]: (sQ189_spl <=> (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation_rng(X0)=relation_dom(sK11_skl)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(X0))|sK11_skl=function_inverse(X0)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f1278,plain,(
% 0.26/0.60 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation_rng(X0)=relation_dom(sK11_skl)|~relation_composition(X0,sK11_skl)=identity_relation(relation_dom(X0))|sK11_skl=function_inverse(X0)|~sQ189_spl)),
% 0.26/0.60 inference(component_clause,[status(thm)],[f1277])).
% 0.26/0.60 fof(f1280,plain,(
% 0.26/0.60 sQ189_spl|~sQ2_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f1201,f1277,f174])).
% 0.26/0.60 fof(f1369,plain,(
% 0.26/0.60 ~relation(function_inverse(sK11_skl))|~function(function_inverse(sK11_skl))|~relation_rng(function_inverse(sK11_skl))=relation_dom(sK11_skl)|~relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_dom(function_inverse(sK11_skl)))|sK11_skl=function_inverse(function_inverse(sK11_skl))|~sQ189_spl|~sQ6_spl),
% 0.26/0.60 inference(resolution,[status(thm)],[f1278,f193])).
% 0.26/0.60 fof(f1472,definition,(
% 0.26/0.60 sQ231_spl <=> (relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_dom(function_inverse(sK11_skl))))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f1474,plain,(
% 0.26/0.60 ~relation_composition(function_inverse(sK11_skl),sK11_skl)=identity_relation(relation_dom(function_inverse(sK11_skl)))|sQ231_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f1472])).
% 0.26/0.60 fof(f1475,definition,(
% 0.26/0.60 sQ232_spl <=> (sK11_skl=function_inverse(function_inverse(sK11_skl)))),
% 0.26/0.60 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 0.26/0.60 fof(f1476,plain,(
% 0.26/0.60 sK11_skl=function_inverse(function_inverse(sK11_skl))|~sQ232_spl),
% 0.26/0.60 inference(component_clause,[status(thm)],[f1475])).
% 0.26/0.60 fof(f1478,plain,(
% 0.26/0.60 ~sQ3_spl|~sQ4_spl|~sQ150_spl|~sQ231_spl|sQ232_spl|~sQ189_spl|~sQ6_spl),
% 0.26/0.60 inference(split_clause,[status(thm)],[f1369,f177,f184,f1070,f1472,f1475,f1277,f192])).
% 0.26/0.60 fof(f1489,plain,(
% 0.26/0.60 ~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_dom(function_inverse(sK11_skl)))|~sQ170_spl|sQ231_spl),
% 0.26/0.60 inference(forward_demodulation,[status(thm)],[f1177,f1474])).
% 0.26/0.60 fof(f1490,plain,(
% 0.26/0.60 ~identity_relation(relation_rng(sK11_skl))=identity_relation(relation_rng(sK11_skl))|~sQ126_spl|~sQ170_spl|sQ231_spl),
% 0.26/0.60 inference(forward_demodulation,[status(thm)],[f941,f1489])).
% 0.26/0.60 fof(f1491,plain,(
% 0.26/0.60 $false|~sQ126_spl|~sQ170_spl|sQ231_spl),
% 0.26/0.60 inference(trivial_equality_resolution,[status(thm)],[f1490])).
% 0.26/0.60 fof(f1492,plain,(
% 0.26/0.60 ~sQ126_spl|~sQ170_spl|sQ231_spl),
% 0.26/0.60 inference(contradiction_clause,[status(thm)],[f1491])).
% 0.26/0.60 fof(f1493,plain,(
% 0.26/0.60 $false|~sQ232_spl),
% 0.26/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1476,f155])).
% 0.26/0.61 fof(f1494,plain,(
% 0.26/0.61 ~sQ232_spl),
% 0.26/0.61 inference(contradiction_clause,[status(thm)],[f1493])).
% 0.26/0.61 fof(f1495,plain,(
% 0.26/0.61 $false),
% 0.26/0.61 inference(sat_refutation,[status(thm)],[f180,f182,f187,f195,f197,f943,f1073,f1179,f1280,f1478,f1492,f1494])).
% 0.26/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.62 % Elapsed time: 0.160395 seconds
% 0.26/0.62 % CPU time: 0.903812 seconds
% 0.26/0.62 % Total memory used: 96.015 MB
% 0.26/0.62 % Net memory used: 95.174 MB
%------------------------------------------------------------------------------