%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU030+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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.18s 0.54s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 5
% Syntax : Number of formulae : 47 ( 12 unt; 0 def)
% Number of atoms : 209 ( 75 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 281 ( 119 ~; 111 |; 36 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 41 ( 39 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ! [D] :
( ( function(D)
& relation(D) )
=> ( ( relation_composition(C,D) = identity_relation(A)
& relation_composition(B,C) = identity_relation(relation_dom(D))
& relation_rng(B) = A )
=> D = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,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/sandbox/benchmark/theBenchmark.p') ).
fof(f39,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/sandbox/benchmark/theBenchmark.p') ).
fof(f40,conjecture,
! [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/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ ! [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) ) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f55,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f56,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f92,plain,
! [A,B] :
( ! [C] :
( ! [D] :
( D = B
| relation_composition(C,D) != identity_relation(A)
| relation_composition(B,C) != identity_relation(relation_dom(D))
| relation_rng(B) != A
| ~ function(D)
| ~ relation(D) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f93,plain,
! [B] :
( ! [C] :
( ! [D] :
( D = B
| ! [A] :
( relation_composition(C,D) != identity_relation(A)
| relation_composition(B,C) != identity_relation(relation_dom(D))
| relation_rng(B) != A )
| ~ function(D)
| ~ relation(D) )
| ~ function(C)
| ~ relation(C) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( X2 = X0
| relation_composition(X1,X2) != identity_relation(X3)
| relation_composition(X0,X1) != identity_relation(relation_dom(X2))
| relation_rng(X0) != X3
| ~ function(X2)
| ~ relation(X2)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f139,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)],[f37]) ).
fof(f141,plain,
! [X0] :
( relation_dom(X0) = relation_rng(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f145,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)],[f39]) ).
fof(f147,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)],[f145]) ).
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)],[f41]) ).
fof(f149,plain,
( sK12_skl != function_inverse(sK11_skl)
& relation_composition(sK11_skl,sK12_skl) = identity_relation(relation_dom(sK11_skl))
& relation_rng(sK11_skl) = relation_dom(sK12_skl)
& one_to_one(sK11_skl)
& function(sK12_skl)
& relation(sK12_skl)
& function(sK11_skl)
& relation(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f148]) ).
fof(f150,plain,
relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
function(sK11_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f152,plain,
relation(sK12_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f153,plain,
function(sK12_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f154,plain,
one_to_one(sK11_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f155,plain,
relation_rng(sK11_skl) = relation_dom(sK12_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f156,plain,
relation_composition(sK11_skl,sK12_skl) = identity_relation(relation_dom(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f157,plain,
sK12_skl != function_inverse(sK11_skl),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f166,plain,
! [X0,X1,X2] :
( X2 = X0
| relation_composition(X1,X2) != identity_relation(relation_rng(X0))
| relation_composition(X0,X1) != identity_relation(relation_dom(X2))
| ~ function(X2)
| ~ relation(X2)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f214,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_dom(sK12_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl)
| ~ function(sK11_skl)
| ~ relation(sK11_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f156,f166]) ).
fof(f215,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl)
| ~ function(sK11_skl)
| ~ relation(sK11_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f155,f214]) ).
fof(f216,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl)
| ~ function(sK11_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f215,f150]) ).
fof(f219,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ function(sK12_skl)
| ~ relation(sK12_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f151]) ).
fof(f220,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ relation(sK12_skl)
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f219,f153]) ).
fof(f221,plain,
! [X0] :
( sK12_skl = X0
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_rng(X0))
| relation_composition(X0,sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f220,f152]) ).
fof(f233,plain,
( relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl))
| ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(resolution,[status(thm)],[f141,f154]) ).
fof(f236,plain,
( relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl))
| ~ function(sK11_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f233,f150]) ).
fof(f278,plain,
relation_dom(sK11_skl) = relation_rng(function_inverse(sK11_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f236,f151]) ).
fof(f297,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)],[f147,f154]) ).
fof(f300,plain,
( relation_composition(function_inverse(sK11_skl),sK11_skl) = identity_relation(relation_rng(sK11_skl))
| ~ function(sK11_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f297,f150]) ).
fof(f374,plain,
relation_composition(function_inverse(sK11_skl),sK11_skl) = identity_relation(relation_rng(sK11_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f300,f151]) ).
fof(f431,plain,
( sK12_skl = function_inverse(sK11_skl)
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_dom(sK11_skl))
| relation_composition(function_inverse(sK11_skl),sK11_skl) != identity_relation(relation_rng(sK11_skl))
| ~ function(function_inverse(sK11_skl))
| ~ relation(function_inverse(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f278,f221]) ).
fof(f432,plain,
( sK12_skl = function_inverse(sK11_skl)
| identity_relation(relation_dom(sK11_skl)) != identity_relation(relation_dom(sK11_skl))
| identity_relation(relation_rng(sK11_skl)) != identity_relation(relation_rng(sK11_skl))
| ~ function(function_inverse(sK11_skl))
| ~ relation(function_inverse(sK11_skl)) ),
inference(forward_demodulation,[status(thm)],[f374,f431]) ).
fof(f433,plain,
( sK12_skl = function_inverse(sK11_skl)
| ~ function(function_inverse(sK11_skl))
| ~ relation(function_inverse(sK11_skl)) ),
inference(trivial_equality_resolution,[status(thm)],[f432]) ).
fof(f434,plain,
( ~ function(function_inverse(sK11_skl))
| ~ relation(function_inverse(sK11_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f157]) ).
fof(f507,plain,
( ~ function(sK11_skl)
| ~ relation(sK11_skl)
| ~ function(function_inverse(sK11_skl)) ),
inference(resolution,[status(thm)],[f434,f56]) ).
fof(f509,plain,
( ~ function(sK11_skl)
| ~ relation(sK11_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f57]) ).
fof(f517,plain,
~ function(sK11_skl),
inference(forward_subsumption_resolution,[status(thm)],[f509,f150]) ).
fof(f518,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f151,f517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU030+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n013.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 05:46:51 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 0.18/0.54 % Refutation found
% 0.18/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.22/0.58 % Elapsed time: 0.082171 seconds
% 0.22/0.58 % CPU time: 0.145872 seconds
% 0.22/0.58 % Total memory used: 23.275 MB
% 0.22/0.58 % Net memory used: 23.182 MB
%------------------------------------------------------------------------------