%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU027+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:06 PM UTC 2026
% Result : Theorem 169.81s 21.93s
% Output : CNFRefutation 169.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 6
% Syntax : Number of formulae : 85 ( 17 unt; 1 def)
% Number of atoms : 473 ( 173 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 645 ( 257 ~; 260 |; 98 &)
% ( 11 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 144 ( 125 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( function(function_inverse(A))
& relation(function_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( B = function_inverse(A)
<=> ( ! [C,D] :
( ( ( C = apply(A,D)
& in(D,relation_dom(A)) )
=> ( D = apply(B,C)
& in(C,relation_rng(A)) ) )
& ( ( D = apply(B,C)
& in(C,relation_rng(A)) )
=> ( C = apply(A,D)
& in(D,relation_dom(A)) ) ) )
& relation_dom(B) = relation_rng(A) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C,D] :
( ( in(D,relation_dom(B))
& in(C,relation_dom(A)) )
=> ( apply(A,C) = D
<=> apply(B,D) = C ) )
& relation_rng(A) = relation_dom(B)
& relation_dom(A) = relation_rng(B)
& one_to_one(A) )
=> B = function_inverse(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C,D] :
( ( in(D,relation_dom(B))
& in(C,relation_dom(A)) )
=> ( apply(A,C) = D
<=> apply(B,D) = C ) )
& relation_rng(A) = relation_dom(B)
& relation_dom(A) = relation_rng(B)
& one_to_one(A) )
=> B = function_inverse(A) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f38,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C] :
( in(C,relation_dom(A))
=> apply(A,C) = apply(B,C) )
& relation_dom(A) = relation_dom(B) )
=> A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,plain,
! [A] :
( ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f50,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| in(C,B) )
& ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ( ! [C] :
( ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| in(C,B) )
& ( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ! [C] :
( ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f52,plain,
! [A] :
( ( ! [B] :
( ( ( ( sK1_skl(B,A) = apply(A,sK2_skl(B,A))
& in(sK2_skl(B,A),relation_dom(A)) )
| in(sK1_skl(B,A),B) )
& ( ! [D] :
( sK1_skl(B,A) != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(sK1_skl(B,A),B) ) )
| B = relation_rng(A) )
& ! [B] :
( ( ! [C] :
( ! [D] :
( C != apply(A,D)
| ~ in(D,relation_dom(A)) )
| in(C,B) )
& ! [C] :
( ( C = apply(A,sK0_skl(C,B,A))
& in(sK0_skl(C,B,A),relation_dom(A)) )
| ~ in(C,B) ) )
| B != relation_rng(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(D,sK0_skl(C,B,A)),skolemize(C,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f51]) ).
fof(f55,plain,
! [X0,X1,X2,X3] :
( X2 != apply(X0,X3)
| ~ in(X3,relation_dom(X0))
| in(X2,X1)
| X1 != relation_rng(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f59,plain,
! [A] :
( ( function(function_inverse(A))
& relation(function_inverse(A)) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f60,plain,
! [X0] :
( ~ relation(X0)
| ~ function(X0)
| relation(function_inverse(X0)) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [X0] :
( function(function_inverse(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f125,plain,
! [A] :
( ! [B] :
( ( B = function_inverse(A)
<=> ( ! [C,D] :
( ( ( D = apply(B,C)
& in(C,relation_rng(A)) )
| C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& ( ( C = apply(A,D)
& in(D,relation_dom(A)) )
| D != apply(B,C)
| ~ in(C,relation_rng(A)) ) )
& relation_dom(B) = relation_rng(A) ) )
| ~ function(B)
| ~ relation(B) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f126,definition,
! [A,B,C,D] :
( sP0_prd(D,C,B,A)
<=> ( ( C = apply(A,D)
& in(D,relation_dom(A)) )
| D != apply(B,C)
| ~ in(C,relation_rng(A)) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f127,plain,
! [A] :
( ! [B] :
( ( B = function_inverse(A)
<=> ( ! [C,D] :
( ( ( D = apply(B,C)
& in(C,relation_rng(A)) )
| C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& sP0_prd(D,C,B,A) )
& relation_dom(B) = relation_rng(A) ) )
| ~ function(B)
| ~ relation(B) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(formula_renaming,[status(thm)],[f125,f126]) ).
fof(f128,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( ( D != apply(B,C)
| ~ in(C,relation_rng(A)) )
& C = apply(A,D)
& in(D,relation_dom(A)) )
| ~ sP0_prd(D,C,B,A) )
| relation_dom(B) != relation_rng(A)
| B = function_inverse(A) )
& ( ( ! [C,D] :
( ( ( D = apply(B,C)
& in(C,relation_rng(A)) )
| C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& sP0_prd(D,C,B,A) )
& relation_dom(B) = relation_rng(A) )
| B != function_inverse(A) ) )
| ~ function(B)
| ~ relation(B) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [A] :
( ! [B] :
( ( ( ? [C,D] :
( ( D != apply(B,C)
| ~ in(C,relation_rng(A)) )
& C = apply(A,D)
& in(D,relation_dom(A)) )
| ? [C,D] : ~ sP0_prd(D,C,B,A)
| relation_dom(B) != relation_rng(A)
| B = function_inverse(A) )
& ( ( ! [C,D] :
( ( D = apply(B,C)
& in(C,relation_rng(A)) )
| C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& ! [C,D] : sP0_prd(D,C,B,A)
& relation_dom(B) = relation_rng(A) )
| B != function_inverse(A) ) )
| ~ function(B)
| ~ relation(B) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f128]) ).
fof(f130,plain,
! [A] :
( ! [B] :
( ( ( ( ( sK17_skl(B,A) != apply(B,sK16_skl(B,A))
| ~ in(sK16_skl(B,A),relation_rng(A)) )
& sK16_skl(B,A) = apply(A,sK17_skl(B,A))
& in(sK17_skl(B,A),relation_dom(A)) )
| ~ sP0_prd(sK15_skl(B,A),sK14_skl(B,A),B,A)
| relation_dom(B) != relation_rng(A)
| B = function_inverse(A) )
& ( ( ! [C,D] :
( ( D = apply(B,C)
& in(C,relation_rng(A)) )
| C != apply(A,D)
| ~ in(D,relation_dom(A)) )
& ! [C,D] : sP0_prd(D,C,B,A)
& relation_dom(B) = relation_rng(A) )
| B != function_inverse(A) ) )
| ~ function(B)
| ~ relation(B) )
| ~ one_to_one(A)
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(C,sK14_skl(B,A)),skolemize(D,sK15_skl(B,A)),skolemize(C,sK16_skl(B,A)),skolemize(D,sK17_skl(B,A))],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( relation_dom(X1) = relation_rng(X0)
| X1 != function_inverse(X0)
| ~ function(X1)
| ~ relation(X1)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f134,plain,
! [X0,X1,X2,X3] :
( X2 = apply(X1,X3)
| X3 != apply(X0,X2)
| ~ in(X2,relation_dom(X0))
| X1 != function_inverse(X0)
| ~ function(X1)
| ~ relation(X1)
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f141,plain,
? [A] :
( ? [B] :
( B != function_inverse(A)
& ! [C,D] :
( ( apply(A,C) = D
<=> apply(B,D) = C )
| ~ in(D,relation_dom(B))
| ~ in(C,relation_dom(A)) )
& relation_rng(A) = relation_dom(B)
& relation_dom(A) = relation_rng(B)
& one_to_one(A)
& function(B)
& relation(B) )
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f142,plain,
? [A] :
( ? [B] :
( B != function_inverse(A)
& ! [C,D] :
( ( ( apply(B,D) != C
| apply(A,C) = D )
& ( apply(B,D) = C
| apply(A,C) != D ) )
| ~ in(D,relation_dom(B))
| ~ in(C,relation_dom(A)) )
& relation_rng(A) = relation_dom(B)
& relation_dom(A) = relation_rng(B)
& one_to_one(A)
& function(B)
& relation(B) )
& function(A)
& relation(A) ),
inference(NNF_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
( sK19_skl != function_inverse(sK18_skl)
& ! [C,D] :
( ( ( apply(sK19_skl,D) != C
| apply(sK18_skl,C) = D )
& ( apply(sK19_skl,D) = C
| apply(sK18_skl,C) != D ) )
| ~ in(D,relation_dom(sK19_skl))
| ~ in(C,relation_dom(sK18_skl)) )
& relation_rng(sK18_skl) = relation_dom(sK19_skl)
& relation_dom(sK18_skl) = relation_rng(sK19_skl)
& one_to_one(sK18_skl)
& function(sK19_skl)
& relation(sK19_skl)
& function(sK18_skl)
& relation(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl]),skolemize(A,sK18_skl),skolemize(B,sK19_skl)],[f142]) ).
fof(f144,plain,
relation(sK18_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
function(sK18_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f146,plain,
relation(sK19_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f147,plain,
function(sK19_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f148,plain,
one_to_one(sK18_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f149,plain,
relation_rng(sK19_skl) = relation_dom(sK18_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f150,plain,
relation_rng(sK18_skl) = relation_dom(sK19_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f152,plain,
! [X0,X1] :
( apply(sK19_skl,X1) != X0
| apply(sK18_skl,X0) = X1
| ~ in(X1,relation_dom(sK19_skl))
| ~ in(X0,relation_dom(sK18_skl)) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f153,plain,
function_inverse(sK18_skl) != sK19_skl,
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f162,plain,
! [A] :
( ! [B] :
( A = B
| ? [C] :
( apply(A,C) != apply(B,C)
& in(C,relation_dom(A)) )
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f163,plain,
! [A] :
( ! [B] :
( A = B
| ( apply(A,sK20_skl(B,A)) != apply(B,sK20_skl(B,A))
& in(sK20_skl(B,A),relation_dom(A)) )
| relation_dom(A) != relation_dom(B)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(C,sK20_skl(B,A))],[f162]) ).
fof(f164,plain,
! [X0,X1] :
( relation_dom(X1) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1)
| in(sK20_skl(X0,X1),relation_dom(X1))
| X1 = X0
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( X0 = X1
| ~ relation(X0)
| relation_dom(X1) != relation_dom(X0)
| apply(X0,sK20_skl(X1,X0)) != apply(X1,sK20_skl(X1,X0))
| ~ function(X1)
| ~ relation(X1)
| ~ function(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f173,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| X1 = apply(function_inverse(X0),apply(X0,X1))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ relation(function_inverse(X0))
| ~ function(function_inverse(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f134]) ).
fof(f174,plain,
! [X0] :
( ~ function(function_inverse(X0))
| relation_dom(function_inverse(X0)) = relation_rng(X0)
| ~ one_to_one(X0)
| ~ relation(X0)
| ~ function(X0)
| ~ relation(function_inverse(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f131]) ).
fof(f175,plain,
! [X0,X1] :
( in(apply(X1,X0),relation_rng(X1))
| ~ relation(X1)
| ~ function(X1)
| ~ in(X0,relation_dom(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f55]) ).
fof(f182,plain,
! [X0] :
( ~ function(function_inverse(X0))
| relation_dom(function_inverse(X0)) = relation_rng(X0)
| ~ one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f174,f60]) ).
fof(f183,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| X1 = apply(function_inverse(X0),apply(X0,X1))
| ~ one_to_one(X0)
| ~ function(X0)
| ~ function(function_inverse(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f173,f60]) ).
fof(f189,plain,
! [X0,X1] :
( apply(sK19_skl,X1) != X0
| apply(sK18_skl,X0) = X1
| ~ in(X1,relation_dom(sK19_skl))
| ~ in(X0,relation_rng(sK19_skl)) ),
inference(forward_demodulation,[status(thm)],[f149,f152]) ).
fof(f190,plain,
! [X0,X1] :
( apply(sK19_skl,X1) != X0
| apply(sK18_skl,X0) = X1
| ~ in(X1,relation_rng(sK18_skl))
| ~ in(X0,relation_rng(sK19_skl)) ),
inference(forward_demodulation,[status(thm)],[f150,f189]) ).
fof(f191,plain,
! [X0] :
( ~ in(X0,relation_rng(sK18_skl))
| X0 = apply(sK18_skl,apply(sK19_skl,X0))
| ~ in(apply(sK19_skl,X0),relation_rng(sK19_skl)) ),
inference(destructive_equality_resolution,[status(thm)],[f190]) ).
fof(f192,plain,
! [X0] :
( ~ one_to_one(X0)
| ~ relation(X0)
| ~ function(X0)
| relation_rng(X0) = relation_dom(function_inverse(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f182,f61]) ).
fof(f194,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| ~ one_to_one(X0)
| X1 = apply(function_inverse(X0),apply(X0,X1))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f61]) ).
fof(f200,plain,
! [X0] :
( in(apply(sK19_skl,X0),relation_rng(sK19_skl))
| ~ relation(sK19_skl)
| ~ function(sK19_skl)
| ~ in(X0,relation_rng(sK18_skl)) ),
inference(paramodulation,[status(thm)],[f150,f175]) ).
fof(f201,plain,
! [X0] :
( ~ relation(sK19_skl)
| ~ in(X0,relation_rng(sK18_skl))
| in(apply(sK19_skl,X0),relation_rng(sK19_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f200,f147]) ).
fof(f235,plain,
( ~ relation(sK18_skl)
| relation(function_inverse(sK18_skl)) ),
inference(resolution,[status(thm)],[f60,f145]) ).
fof(f238,plain,
relation(function_inverse(sK18_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f235,f144]) ).
fof(f291,plain,
! [X0] :
( sK19_skl = X0
| ~ relation(sK19_skl)
| relation_dom(X0) != relation_dom(sK19_skl)
| apply(sK19_skl,sK20_skl(X0,sK19_skl)) != apply(X0,sK20_skl(X0,sK19_skl))
| ~ function(X0)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f165,f147]) ).
fof(f298,plain,
! [X0] :
( sK19_skl = X0
| ~ relation(sK19_skl)
| relation_dom(X0) != relation_rng(sK18_skl)
| apply(sK19_skl,sK20_skl(X0,sK19_skl)) != apply(X0,sK20_skl(X0,sK19_skl))
| ~ function(X0)
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f150,f291]) ).
fof(f299,plain,
! [X0] :
( X0 = sK19_skl
| relation_rng(sK18_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(X0)
| apply(sK19_skl,sK20_skl(X0,sK19_skl)) != apply(X0,sK20_skl(X0,sK19_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f146]) ).
fof(f304,plain,
( function(function_inverse(sK18_skl))
| ~ relation(sK18_skl) ),
inference(resolution,[status(thm)],[f61,f145]) ).
fof(f308,plain,
function(function_inverse(sK18_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f304,f144]) ).
fof(f335,plain,
( ~ relation(sK18_skl)
| ~ function(sK18_skl)
| relation_rng(sK18_skl) = relation_dom(function_inverse(sK18_skl)) ),
inference(resolution,[status(thm)],[f192,f148]) ).
fof(f336,plain,
( relation_dom(function_inverse(sK18_skl)) = relation_rng(sK18_skl)
| ~ relation(sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f335,f145]) ).
fof(f386,plain,
( function_inverse(sK18_skl) = sK19_skl
| relation_rng(sK18_skl) != relation_dom(function_inverse(sK18_skl))
| ~ relation(function_inverse(sK18_skl))
| apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) != apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl)) ),
inference(resolution,[status(thm)],[f299,f308]) ).
fof(f400,plain,
( relation_dom(function_inverse(sK18_skl)) != relation_rng(sK18_skl)
| apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) != apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl))
| function_inverse(sK18_skl) = sK19_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f238]) ).
fof(f477,plain,
! [X0] :
( ~ in(X0,relation_rng(sK19_skl))
| ~ one_to_one(sK18_skl)
| X0 = apply(function_inverse(sK18_skl),apply(sK18_skl,X0))
| ~ function(sK18_skl)
| ~ relation(sK18_skl) ),
inference(paramodulation,[status(thm)],[f149,f194]) ).
fof(f479,plain,
! [X0] :
( ~ one_to_one(sK18_skl)
| ~ function(sK18_skl)
| apply(function_inverse(sK18_skl),apply(sK18_skl,X0)) = X0
| ~ in(X0,relation_rng(sK19_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f144]) ).
fof(f492,plain,
relation_rng(sK18_skl) = relation_dom(function_inverse(sK18_skl)),
inference(resolution,[status(thm)],[f336,f144]) ).
fof(f494,plain,
( relation_rng(sK18_skl) != relation_rng(sK18_skl)
| apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) != apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl))
| function_inverse(sK18_skl) = sK19_skl ),
inference(backward_demodulation,[status(thm)],[f492,f400]) ).
fof(f498,plain,
( apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) != apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl))
| function_inverse(sK18_skl) = sK19_skl ),
inference(trivial_equality_resolution,[status(thm)],[f494]) ).
fof(f499,plain,
apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) != apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f498,f153]) ).
fof(f1115,plain,
! [X0] :
( relation_dom(sK19_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(sK19_skl)
| in(sK20_skl(X0,sK19_skl),relation_dom(sK19_skl))
| sK19_skl = X0
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f164,f147]) ).
fof(f1134,plain,
! [X0] :
( relation_dom(sK19_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(sK19_skl)
| in(sK20_skl(X0,sK19_skl),relation_rng(sK18_skl))
| sK19_skl = X0
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f150,f1115]) ).
fof(f1135,plain,
! [X0] :
( relation_rng(sK18_skl) != relation_dom(X0)
| ~ function(X0)
| ~ relation(sK19_skl)
| in(sK20_skl(X0,sK19_skl),relation_rng(sK18_skl))
| sK19_skl = X0
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f150,f1134]) ).
fof(f1136,plain,
! [X0] :
( in(sK20_skl(X0,sK19_skl),relation_rng(sK18_skl))
| ~ function(X0)
| ~ relation(X0)
| relation_dom(X0) != relation_rng(sK18_skl)
| X0 = sK19_skl ),
inference(forward_subsumption_resolution,[status(thm)],[f1135,f146]) ).
fof(f1336,plain,
( in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl))
| ~ relation(function_inverse(sK18_skl))
| relation_dom(function_inverse(sK18_skl)) != relation_rng(sK18_skl)
| function_inverse(sK18_skl) = sK19_skl ),
inference(resolution,[status(thm)],[f1136,f308]) ).
fof(f1353,plain,
( in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl))
| ~ relation(function_inverse(sK18_skl))
| relation_rng(sK18_skl) != relation_rng(sK18_skl)
| function_inverse(sK18_skl) = sK19_skl ),
inference(forward_demodulation,[status(thm)],[f492,f1336]) ).
fof(f1354,plain,
( in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl))
| ~ relation(function_inverse(sK18_skl))
| function_inverse(sK18_skl) = sK19_skl ),
inference(trivial_equality_resolution,[status(thm)],[f1353]) ).
fof(f1355,plain,
( ~ relation(function_inverse(sK18_skl))
| in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1354,f153]) ).
fof(f3789,plain,
in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl)),
inference(resolution,[status(thm)],[f1355,f238]) ).
fof(f3794,plain,
( ~ relation(sK19_skl)
| in(apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)),relation_rng(sK19_skl)) ),
inference(resolution,[status(thm)],[f3789,f201]) ).
fof(f3803,plain,
in(apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)),relation_rng(sK19_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3794,f146]) ).
fof(f3994,plain,
( ~ in(sK20_skl(function_inverse(sK18_skl),sK19_skl),relation_rng(sK18_skl))
| sK20_skl(function_inverse(sK18_skl),sK19_skl) = apply(sK18_skl,apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl))) ),
inference(resolution,[status(thm)],[f3803,f191]) ).
fof(f3996,plain,
( ~ one_to_one(sK18_skl)
| ~ function(sK18_skl)
| apply(function_inverse(sK18_skl),apply(sK18_skl,apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)))) = apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) ),
inference(resolution,[status(thm)],[f3803,f479]) ).
fof(f4007,plain,
apply(sK18_skl,apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl))) = sK20_skl(function_inverse(sK18_skl),sK19_skl),
inference(forward_subsumption_resolution,[status(thm)],[f3994,f3789]) ).
fof(f4011,plain,
( ~ one_to_one(sK18_skl)
| ~ function(sK18_skl)
| apply(function_inverse(sK18_skl),sK20_skl(function_inverse(sK18_skl),sK19_skl)) = apply(sK19_skl,sK20_skl(function_inverse(sK18_skl),sK19_skl)) ),
inference(forward_demodulation,[status(thm)],[f4007,f3996]) ).
fof(f4012,plain,
( ~ one_to_one(sK18_skl)
| ~ function(sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4011,f499]) ).
fof(f4062,plain,
~ function(sK18_skl),
inference(resolution,[status(thm)],[f4012,f148]) ).
fof(f4063,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4062,f145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU027+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/0.44 % Computer : n018.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:49:43 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 169.81/21.93 % Refutation found
% 169.81/21.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 169.81/21.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.33/22.41 % Elapsed time: 21.943722 seconds
% 16.33/22.41 % CPU time: 170.919252 seconds
% 16.33/22.41 % Total memory used: 528.962 MB
% 16.33/22.41 % Net memory used: 481.446 MB
%------------------------------------------------------------------------------