%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU221+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:45 PM UTC 2026
% Result : Theorem 169.97s 22.04s
% Output : CNFRefutation 53.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 17
% Syntax : Number of formulae : 81 ( 9 unt; 12 def)
% Number of atoms : 273 ( 40 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 322 ( 130 ~; 137 |; 30 &)
% ( 14 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 13 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 36 ( 33 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
<=> ! [B,C] :
( ( apply(A,B) = apply(A,C)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
=> B = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,lemma,
! [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(f205,lemma,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( ( in(A,relation_rng(B))
& one_to_one(B) )
=> ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> one_to_one(function_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> one_to_one(function_inverse(A)) ) ),
inference(negated_conjecture,[status(cth)],[f209]) ).
fof(f467,plain,
! [A] :
( ( one_to_one(A)
<=> ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f468,plain,
! [A] :
( ( ( ? [B,C] :
( B != C
& apply(A,B) = apply(A,C)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
| one_to_one(A) )
& ( ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f467]) ).
fof(f469,plain,
! [A] :
( ( ( ( sK46_skl(A) != sK47_skl(A)
& apply(A,sK46_skl(A)) = apply(A,sK47_skl(A))
& in(sK47_skl(A),relation_dom(A))
& in(sK46_skl(A),relation_dom(A)) )
| one_to_one(A) )
& ( ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46_skl,sK47_skl]),skolemize(B,sK46_skl(A)),skolemize(C,sK47_skl(A))],[f468]) ).
fof(f471,plain,
! [X0] :
( in(sK46_skl(X0),relation_dom(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f472,plain,
! [X0] :
( in(sK47_skl(X0),relation_dom(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f473,plain,
! [X0] :
( apply(X0,sK46_skl(X0)) = apply(X0,sK47_skl(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f474,plain,
! [X0] :
( sK46_skl(X0) != sK47_skl(X0)
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f469]) ).
fof(f500,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f501,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f502,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f897,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)],[f203]) ).
fof(f898,plain,
! [X0] :
( relation_rng(X0) = relation_dom(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f897]) ).
fof(f903,plain,
! [A,B] :
( ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) )
| ~ in(A,relation_rng(B))
| ~ one_to_one(B)
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f205]) ).
fof(f904,plain,
! [B] :
( ! [A] :
( ( A = apply(relation_composition(function_inverse(B),B),A)
& A = apply(B,apply(function_inverse(B),A)) )
| ~ in(A,relation_rng(B))
| ~ one_to_one(B) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f903]) ).
fof(f905,plain,
! [X0,X1] :
( X1 = apply(X0,apply(function_inverse(X0),X1))
| ~ in(X1,relation_rng(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f904]) ).
fof(f914,plain,
? [A] :
( ~ one_to_one(function_inverse(A))
& one_to_one(A)
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f210]) ).
fof(f915,plain,
( ~ one_to_one(function_inverse(sK78_skl))
& one_to_one(sK78_skl)
& function(sK78_skl)
& relation(sK78_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78_skl]),skolemize(A,sK78_skl)],[f914]) ).
fof(f916,plain,
relation(sK78_skl),
inference(cnf_transformation,[status(thm)],[f915]) ).
fof(f917,plain,
function(sK78_skl),
inference(cnf_transformation,[status(thm)],[f915]) ).
fof(f918,plain,
one_to_one(sK78_skl),
inference(cnf_transformation,[status(thm)],[f915]) ).
fof(f919,plain,
~ one_to_one(function_inverse(sK78_skl)),
inference(cnf_transformation,[status(thm)],[f915]) ).
fof(f1134,plain,
( relation_rng(sK78_skl) = relation_dom(function_inverse(sK78_skl))
| ~ function(sK78_skl)
| ~ relation(sK78_skl) ),
inference(resolution,[status(thm)],[f898,f918]) ).
fof(f1142,definition,
( sQ4_spl
<=> relation(sK78_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1144,plain,
( sQ4_spl
| ~ relation(sK78_skl) ),
inference(component_clause,[status(thm)],[f1142]) ).
fof(f1145,definition,
( sQ5_spl
<=> function(sK78_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1147,plain,
( sQ5_spl
| ~ function(sK78_skl) ),
inference(component_clause,[status(thm)],[f1145]) ).
fof(f1148,definition,
( sQ6_spl
<=> relation_rng(sK78_skl) = relation_dom(function_inverse(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1149,plain,
( ~ sQ6_spl
| relation_rng(sK78_skl) = relation_dom(function_inverse(sK78_skl)) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1151,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1134,f1142,f1145,f1148]) ).
fof(f1187,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1147,f917]) ).
fof(f1188,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1187]) ).
fof(f1189,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1144,f916]) ).
fof(f1190,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1189]) ).
fof(f1218,definition,
( sQ19_spl
<=> relation(function_inverse(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1220,plain,
( sQ19_spl
| ~ relation(function_inverse(sK78_skl)) ),
inference(component_clause,[status(thm)],[f1218]) ).
fof(f1221,definition,
( sQ20_spl
<=> function(function_inverse(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
( ~ sQ20_spl
| function(function_inverse(sK78_skl)) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1223,plain,
( sQ20_spl
| ~ function(function_inverse(sK78_skl)) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1224,definition,
( sQ21_spl
<=> one_to_one(function_inverse(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
( ~ sQ21_spl
| one_to_one(function_inverse(sK78_skl)) ),
inference(component_clause,[status(thm)],[f1224]) ).
fof(f1238,plain,
( sQ20_spl
| ~ function(sK78_skl)
| ~ relation(sK78_skl) ),
inference(resolution,[status(thm)],[f1223,f502]) ).
fof(f1240,plain,
( sQ20_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1238,f1142,f1145,f1221]) ).
fof(f1293,plain,
( sQ19_spl
| ~ function(sK78_skl)
| ~ relation(sK78_skl) ),
inference(resolution,[status(thm)],[f1220,f501]) ).
fof(f1295,plain,
( sQ19_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1293,f1142,f1145,f1218]) ).
fof(f5590,definition,
( sQ308_spl
<=> one_to_one(sK78_skl) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f5592,plain,
( sQ308_spl
| ~ one_to_one(sK78_skl) ),
inference(component_clause,[status(thm)],[f5590]) ).
fof(f5617,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5592,f918]) ).
fof(f5618,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f5617]) ).
fof(f9236,plain,
( ~ sQ6_spl
| in(sK46_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl))
| one_to_one(function_inverse(sK78_skl))
| ~ function(function_inverse(sK78_skl))
| ~ relation(function_inverse(sK78_skl)) ),
inference(paramodulation,[status(thm)],[f1149,f471]) ).
fof(f9240,definition,
( sQ498_spl
<=> in(sK46_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition]) ).
fof(f9241,plain,
( ~ sQ498_spl
| in(sK46_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl)) ),
inference(component_clause,[status(thm)],[f9240]) ).
fof(f9243,plain,
( ~ sQ6_spl
| sQ498_spl
| sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f9236,f1218,f1221,f1224,f9240,f1148]) ).
fof(f9256,plain,
( ~ sQ498_spl
| sK46_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl))))
| ~ one_to_one(sK78_skl)
| ~ function(sK78_skl)
| ~ relation(sK78_skl) ),
inference(resolution,[status(thm)],[f9241,f905]) ).
fof(f9263,definition,
( sQ502_spl
<=> sK46_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f9264,plain,
( ~ sQ502_spl
| sK46_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl)))) ),
inference(component_clause,[status(thm)],[f9263]) ).
fof(f9266,plain,
( ~ sQ498_spl
| sQ502_spl
| ~ sQ308_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f9256,f1142,f1145,f5590,f9263,f9240]) ).
fof(f9423,plain,
( ~ sQ6_spl
| in(sK47_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl))
| one_to_one(function_inverse(sK78_skl))
| ~ function(function_inverse(sK78_skl))
| ~ relation(function_inverse(sK78_skl)) ),
inference(paramodulation,[status(thm)],[f1149,f472]) ).
fof(f9427,definition,
( sQ514_spl
<=> in(sK47_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl)) ),
introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition]) ).
fof(f9428,plain,
( ~ sQ514_spl
| in(sK47_skl(function_inverse(sK78_skl)),relation_rng(sK78_skl)) ),
inference(component_clause,[status(thm)],[f9427]) ).
fof(f9430,plain,
( ~ sQ6_spl
| sQ514_spl
| sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f9423,f1218,f1221,f1224,f9427,f1148]) ).
fof(f9447,plain,
( ~ sQ20_spl
| apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl))) = apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl)))
| one_to_one(function_inverse(sK78_skl))
| ~ relation(function_inverse(sK78_skl)) ),
inference(resolution,[status(thm)],[f473,f1222]) ).
fof(f9474,definition,
( sQ522_spl
<=> apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl))) = apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl))) ),
introduced(definition,[new_symbols(definition,[sQ522_spl])],[split_symbol_definition]) ).
fof(f9475,plain,
( ~ sQ522_spl
| apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl))) = apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl))) ),
inference(component_clause,[status(thm)],[f9474]) ).
fof(f9477,plain,
( ~ sQ20_spl
| sQ522_spl
| sQ21_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f9447,f1218,f1224,f9474,f1221]) ).
fof(f10624,plain,
( ~ sQ514_spl
| sK47_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl))))
| ~ one_to_one(sK78_skl)
| ~ function(sK78_skl)
| ~ relation(sK78_skl) ),
inference(resolution,[status(thm)],[f9428,f905]) ).
fof(f10631,definition,
( sQ713_spl
<=> sK47_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f10632,plain,
( ~ sQ713_spl
| sK47_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK47_skl(function_inverse(sK78_skl)))) ),
inference(component_clause,[status(thm)],[f10631]) ).
fof(f10634,plain,
( ~ sQ514_spl
| sQ713_spl
| ~ sQ308_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f10624,f1142,f1145,f5590,f10631,f9427]) ).
fof(f10635,plain,
( ~ sQ713_spl
| ~ sQ522_spl
| sK47_skl(function_inverse(sK78_skl)) = apply(sK78_skl,apply(function_inverse(sK78_skl),sK46_skl(function_inverse(sK78_skl)))) ),
inference(forward_demodulation,[status(thm)],[f9475,f10632]) ).
fof(f10641,plain,
( ~ sQ713_spl
| ~ sQ522_spl
| ~ sQ502_spl
| sK47_skl(function_inverse(sK78_skl)) = sK46_skl(function_inverse(sK78_skl)) ),
inference(forward_demodulation,[status(thm)],[f9264,f10635]) ).
fof(f11038,plain,
( ~ sQ713_spl
| ~ sQ522_spl
| ~ sQ502_spl
| one_to_one(function_inverse(sK78_skl))
| ~ function(function_inverse(sK78_skl))
| ~ relation(function_inverse(sK78_skl)) ),
inference(resolution,[status(thm)],[f10641,f474]) ).
fof(f11041,plain,
( ~ sQ713_spl
| ~ sQ522_spl
| ~ sQ502_spl
| sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f11038,f1218,f1221,f1224,f9263,f9474,f10631]) ).
fof(f11050,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1225,f919]) ).
fof(f11051,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f11050]) ).
fof(f11052,plain,
$false,
inference(sat_refutation,[status(thm)],[f1151,f1188,f1190,f1240,f1295,f5618,f9243,f9266,f9430,f9477,f10634,f11041,f11051]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU221+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 05:57:20 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.41 % Drodi V4.1.1
% 169.97/22.04 % Refutation found
% 169.97/22.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 169.97/22.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.39/22.24 % Elapsed time: 21.850196 seconds
% 6.39/22.24 % CPU time: 171.436361 seconds
% 6.39/22.24 % Total memory used: 520.959 MB
% 6.39/22.24 % Net memory used: 466.644 MB
%------------------------------------------------------------------------------