%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU034+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 : n018.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.22s 5.53s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 53 ( 17 unt; 0 def)
% Number of atoms : 159 ( 71 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 193 ( 87 ~; 82 |; 16 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 60 ( 59 !; 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(f7,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( relation_composition(A,B) = A
& relation_rng(A) = relation_dom(B) )
=> B = identity_relation(relation_dom(B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A] : one_to_one(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,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(f40,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(f41,conjecture,
! [A] : function_inverse(identity_relation(A)) = identity_relation(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ! [A] : function_inverse(identity_relation(A)) = identity_relation(A),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f44,axiom,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f58,plain,
! [X0] :
( relation(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f62,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f76,plain,
( ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f78,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f135,plain,
! [A] :
( ! [B] :
( B = identity_relation(relation_dom(B))
| relation_composition(A,B) != A
| relation_rng(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f136,plain,
! [X0,X1] :
( X1 = identity_relation(relation_dom(X1))
| relation_composition(X0,X1) != X0
| relation_rng(X0) != relation_dom(X1)
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f140,plain,
! [X0] : one_to_one(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f141,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)],[f38]) ).
fof(f142,plain,
! [X0] :
( relation_rng(X0) = relation_dom(function_inverse(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f147,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)],[f40]) ).
fof(f148,plain,
! [X0] :
( relation_composition(X0,function_inverse(X0)) = identity_relation(relation_dom(X0))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
? [A] : function_inverse(identity_relation(A)) != identity_relation(A),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f151,plain,
function_inverse(identity_relation(sK11_skl)) != identity_relation(sK11_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f150]) ).
fof(f152,plain,
function_inverse(identity_relation(sK11_skl)) != identity_relation(sK11_skl),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
( ! [A] : relation_rng(identity_relation(A)) = A
& ! [A] : relation_dom(identity_relation(A)) = A ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f156,plain,
! [X0] : relation_dom(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [X0] : relation_rng(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f475,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| function_inverse(X1) = identity_relation(relation_dom(function_inverse(X1)))
| relation_composition(X0,function_inverse(X1)) != X0
| relation_rng(X0) != relation_dom(function_inverse(X1))
| ~ relation(function_inverse(X1))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f136,f59]) ).
fof(f517,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| function_inverse(X1) = identity_relation(relation_dom(function_inverse(X1)))
| relation_composition(X0,function_inverse(X1)) != X0
| relation_rng(X0) != relation_dom(function_inverse(X1))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f58]) ).
fof(f539,plain,
! [X0,X1] :
( ~ relation(identity_relation(X1))
| function_inverse(identity_relation(X1)) = identity_relation(relation_dom(function_inverse(identity_relation(X1))))
| relation_composition(X0,function_inverse(identity_relation(X1))) != X0
| relation_rng(X0) != relation_dom(function_inverse(identity_relation(X1)))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f517,f78]) ).
fof(f566,plain,
! [X0,X1] :
( function_inverse(identity_relation(X1)) = identity_relation(relation_dom(function_inverse(identity_relation(X1))))
| relation_composition(X0,function_inverse(identity_relation(X1))) != X0
| relation_rng(X0) != relation_dom(function_inverse(identity_relation(X1)))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f62]) ).
fof(f703,plain,
! [X0] :
( relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))) = identity_relation(relation_dom(identity_relation(X0)))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(resolution,[status(thm)],[f140,f148]) ).
fof(f705,plain,
! [X0] :
( relation_rng(identity_relation(X0)) = relation_dom(function_inverse(identity_relation(X0)))
| ~ function(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(resolution,[status(thm)],[f140,f142]) ).
fof(f707,plain,
! [X0] :
( relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))) = identity_relation(relation_dom(identity_relation(X0)))
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f703,f62]) ).
fof(f709,plain,
! [X0] :
( relation_rng(identity_relation(X0)) = relation_dom(function_inverse(identity_relation(X0)))
| ~ function(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f62]) ).
fof(f739,plain,
! [X0] :
( relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))) = identity_relation(X0)
| ~ function(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f156,f707]) ).
fof(f740,plain,
! [X0] : relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))) = identity_relation(X0),
inference(forward_subsumption_resolution,[status(thm)],[f739,f78]) ).
fof(f749,plain,
! [X0] :
( X0 = relation_dom(function_inverse(identity_relation(X0)))
| ~ function(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f157,f709]) ).
fof(f750,plain,
! [X0] : X0 = relation_dom(function_inverse(identity_relation(X0))),
inference(forward_subsumption_resolution,[status(thm)],[f749,f78]) ).
fof(f931,plain,
! [X0,X1] :
( function_inverse(identity_relation(X1)) = identity_relation(relation_dom(function_inverse(identity_relation(X1))))
| relation_composition(X0,function_inverse(identity_relation(X1))) != X0
| relation_rng(X0) != X1
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f750,f566]) ).
fof(f932,plain,
! [X0,X1] :
( function_inverse(identity_relation(X1)) = identity_relation(X1)
| relation_composition(X0,function_inverse(identity_relation(X1))) != X0
| relation_rng(X0) != X1
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f750,f931]) ).
fof(f933,plain,
! [X0] :
( function_inverse(identity_relation(relation_rng(X0))) = identity_relation(relation_rng(X0))
| relation_composition(X0,function_inverse(identity_relation(relation_rng(X0)))) != X0
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f932]) ).
fof(f938,plain,
! [X0] :
( function_inverse(identity_relation(relation_rng(identity_relation(X0)))) = identity_relation(relation_rng(identity_relation(X0)))
| relation_composition(identity_relation(X0),function_inverse(identity_relation(relation_rng(identity_relation(X0))))) != identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(resolution,[status(thm)],[f933,f78]) ).
fof(f964,plain,
! [X0] :
( function_inverse(identity_relation(relation_rng(identity_relation(X0)))) = identity_relation(relation_rng(identity_relation(X0)))
| relation_composition(identity_relation(X0),function_inverse(identity_relation(X0))) != identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f157,f938]) ).
fof(f965,plain,
! [X0] :
( function_inverse(identity_relation(relation_rng(identity_relation(X0)))) = identity_relation(relation_rng(identity_relation(X0)))
| identity_relation(X0) != identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f740,f964]) ).
fof(f966,plain,
! [X0] :
( function_inverse(identity_relation(X0)) = identity_relation(relation_rng(identity_relation(X0)))
| identity_relation(X0) != identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f157,f965]) ).
fof(f967,plain,
! [X0] :
( function_inverse(identity_relation(X0)) = identity_relation(X0)
| identity_relation(X0) != identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f157,f966]) ).
fof(f968,plain,
! [X0] :
( function_inverse(identity_relation(X0)) = identity_relation(X0)
| ~ relation(identity_relation(X0)) ),
inference(trivial_equality_resolution,[status(thm)],[f967]) ).
fof(f969,plain,
! [X0] : function_inverse(identity_relation(X0)) = identity_relation(X0),
inference(forward_subsumption_resolution,[status(thm)],[f968,f62]) ).
fof(f1069,plain,
identity_relation(sK11_skl) != identity_relation(sK11_skl),
inference(backward_demodulation,[status(thm)],[f969,f152]) ).
fof(f1076,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f1069]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU034+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.45 % Computer : n018.cluster.edu
% 0.17/5.45 % Model : x86_64 x86_64
% 0.17/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.45 % Memory : 8046.5625MB
% 0.17/5.45 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Mon Sep 21 05:49:34 UTC 2026
% 0.17/5.46 % CPUTime :
% 0.17/5.47 % Drodi V4.1.1
% 0.22/5.53 % Refutation found
% 0.22/5.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/5.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.22/5.57 % Elapsed time: 0.107955 seconds
% 0.22/5.57 % CPU time: 0.445638 seconds
% 0.22/5.57 % Total memory used: 67.462 MB
% 0.22/5.57 % Net memory used: 66.896 MB
%------------------------------------------------------------------------------