%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU032+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:19:07 PM UTC 2026
% Result : Theorem 0.26s 0.77s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 14
% Syntax : Number of formulae : 64 ( 9 unt; 8 def)
% Number of atoms : 237 ( 64 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 304 ( 131 ~; 129 |; 22 &)
% ( 8 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 9 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 34 ( 33 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_dom(A) = relation_rng(function_inverse(A))
& relation_rng(A) = relation_dom(function_inverse(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ( relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A))
& relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> one_to_one(function_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( relation_composition(A,B) = identity_relation(relation_dom(A))
& relation_rng(A) = relation_dom(B)
& one_to_one(A) )
=> B = function_inverse(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> function_inverse(function_inverse(A)) = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> function_inverse(function_inverse(A)) = A ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f56,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f57,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f137,plain,
! [A] :
( ( relation_dom(A) = relation_rng(function_inverse(A))
& relation_rng(A) = relation_dom(function_inverse(A)) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f138,plain,
! [X0] :
( relation_rng(X0) = relation_dom(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0] :
( relation_dom(X0) = relation_rng(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f143,plain,
! [A] :
( ( relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A))
& relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A)) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f145,plain,
! [X0] :
( relation_composition(function_inverse(X0),X0) = identity_relation(relation_rng(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f146,plain,
! [A] :
( one_to_one(function_inverse(A))
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f147,plain,
! [X0] :
( one_to_one(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [A] :
( ! [B] :
( B = function_inverse(A)
| relation_composition(A,B) != identity_relation(relation_dom(A))
| relation_rng(A) != relation_dom(B)
| ~ one_to_one(A)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f149,plain,
! [X0,X1] :
( X1 = function_inverse(X0)
| relation_composition(X0,X1) != identity_relation(relation_dom(X0))
| relation_rng(X0) != relation_dom(X1)
| ~ one_to_one(X0)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
? [A] :
( function_inverse(function_inverse(A)) != A
& one_to_one(A)
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f151,plain,
( function_inverse(function_inverse(sK11_skl)) != sK11_skl
& one_to_one(sK11_skl)
& function(sK11_skl)
& relation(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f150]) ).
fof(f152,plain,
relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
function(sK11_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f154,plain,
one_to_one(sK11_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
function_inverse(function_inverse(sK11_skl)) != sK11_skl,
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f187,plain,
( relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f138,f154]) ).
fof(f200,definition,
( sQ3_spl
<=> relation(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( sQ3_spl
| ~ relation(sK11_skl) ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,definition,
( sQ4_spl
<=> function(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( sQ4_spl
| ~ function(sK11_skl) ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f206,definition,
( sQ5_spl
<=> relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( ~ sQ5_spl
| relation_rng(sK11_skl) = relation_dom(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f209,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f187,f200,f203,f206]) ).
fof(f211,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f205,f153]) ).
fof(f212,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f211]) ).
fof(f213,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202,f152]) ).
fof(f214,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f213]) ).
fof(f217,plain,
( relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f139,f154]) ).
fof(f224,definition,
( sQ7_spl
<=> relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( ~ sQ7_spl
| relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f227,plain,
( sQ7_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f217,f200,f203,f224]) ).
fof(f250,plain,
( relation_composition(function_inverse(sK11_skl),sK11_skl) = identity_relation(relation_rng(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f145,f154]) ).
fof(f257,definition,
( sQ11_spl
<=> relation_composition(function_inverse(sK11_skl),sK11_skl) = identity_relation(relation_rng(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( sQ11_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f250,f200,f203,f257]) ).
fof(f375,plain,
! [X0,X1] :
( ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0)
| X1 = function_inverse(function_inverse(X0))
| relation_composition(function_inverse(X0),X1) != identity_relation(relation_dom(function_inverse(X0)))
| relation_rng(function_inverse(X0)) != relation_dom(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(function_inverse(X0))
| ~ relation(function_inverse(X0)) ),
inference(resolution,[status(thm)],[f149,f147]) ).
fof(f382,plain,
! [X0,X1] :
( ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0)
| X1 = function_inverse(function_inverse(X0))
| relation_composition(function_inverse(X0),X1) != identity_relation(relation_dom(function_inverse(X0)))
| relation_rng(function_inverse(X0)) != relation_dom(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(function_inverse(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f57]) ).
fof(f776,plain,
! [X0,X1] :
( ~ one_to_one(X1)
| ~ function(X1)
| ~ relation(X1)
| X0 = function_inverse(function_inverse(X1))
| relation_composition(function_inverse(X1),X0) != identity_relation(relation_dom(function_inverse(X1)))
| relation_rng(function_inverse(X1)) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f58]) ).
fof(f1052,plain,
! [X0] :
( ~ function(sK11_skl)
| ~ relation(sK11_skl)
| X0 = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),X0) != identity_relation(relation_dom(function_inverse(sK11_skl)))
| relation_rng(function_inverse(sK11_skl)) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f154,f776]) ).
fof(f1062,definition,
! [X0] :
( sQ119_spl
<=> ( X0 = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),X0) != identity_relation(relation_dom(function_inverse(sK11_skl)))
| relation_rng(function_inverse(sK11_skl)) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1063,plain,
! [X0] :
( ~ sQ119_spl
| X0 = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),X0) != identity_relation(relation_dom(function_inverse(sK11_skl)))
| relation_rng(function_inverse(sK11_skl)) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f1062]) ).
fof(f1065,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f1052,f1062,f200,f203]) ).
fof(f3138,plain,
! [X0] :
( ~ sQ119_spl
| ~ sQ7_spl
| X0 = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),X0) != identity_relation(relation_dom(function_inverse(sK11_skl)))
| relation_dom(sK11_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f225,f1063]) ).
fof(f3139,plain,
! [X0] :
( ~ sQ119_spl
| ~ sQ7_spl
| ~ sQ5_spl
| X0 = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),X0) != identity_relation(relation_rng(sK11_skl))
| relation_dom(sK11_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f207,f3138]) ).
fof(f3141,plain,
( ~ sQ119_spl
| ~ sQ7_spl
| ~ sQ5_spl
| sK11_skl = function_inverse(function_inverse(sK11_skl))
| relation_composition(function_inverse(sK11_skl),sK11_skl) != identity_relation(relation_rng(sK11_skl))
| relation_dom(sK11_skl) != relation_dom(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f3139,f153]) ).
fof(f3158,definition,
( sQ202_spl
<=> relation_dom(sK11_skl) = relation_dom(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f3160,plain,
( sQ202_spl
| relation_dom(sK11_skl) != relation_dom(sK11_skl) ),
inference(component_clause,[status(thm)],[f3158]) ).
fof(f3161,definition,
( sQ203_spl
<=> sK11_skl = function_inverse(function_inverse(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f3162,plain,
( ~ sQ203_spl
| sK11_skl = function_inverse(function_inverse(sK11_skl)) ),
inference(component_clause,[status(thm)],[f3161]) ).
fof(f3164,plain,
( ~ sQ119_spl
| ~ sQ7_spl
| ~ sQ5_spl
| sQ203_spl
| ~ sQ11_spl
| ~ sQ202_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f3141,f200,f3158,f257,f3161,f206,f224,f1062]) ).
fof(f3189,plain,
( sQ202_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3160]) ).
fof(f3190,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f3189]) ).
fof(f3193,plain,
( ~ sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3162,f155]) ).
fof(f3194,plain,
~ sQ203_spl,
inference(contradiction_clause,[status(thm)],[f3193]) ).
fof(f3195,plain,
$false,
inference(sat_refutation,[status(thm)],[f209,f212,f214,f227,f260,f1065,f3164,f3190,f3194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU032+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n015.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 05:50:36 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 0.26/0.77 % Refutation found
% 0.26/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.26/0.82 % Elapsed time: 0.362471 seconds
% 0.26/0.82 % CPU time: 2.113535 seconds
% 0.26/0.82 % Total memory used: 109.400 MB
% 0.26/0.82 % Net memory used: 106.958 MB
%------------------------------------------------------------------------------