%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU290+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 : n012.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:20:02 PM UTC 2026
% Result : Theorem 166.41s 31.34s
% Output : CNFRefutation 166.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 23
% Syntax : Number of formulae : 120 ( 22 unt; 11 def)
% Number of atoms : 417 ( 133 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 461 ( 164 ~; 164 |; 91 &)
% ( 26 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 10 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-3 aty)
% Number of variables : 208 ( 182 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> ( ( B = empty_set
=> ( ( quasi_total(C,A,B)
<=> C = empty_set )
| A = empty_set ) )
& ( ( B = empty_set
=> A = empty_set )
=> ( quasi_total(C,A,B)
<=> A = relation_dom_as_subset(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,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(f120,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
? [A] :
( empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> relation_dom_as_subset(A,B,C) = relation_dom(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f216,axiom,
! [A] :
( ! [B,C,D] :
( ( ordinal(D)
& B = D
& ordinal(C)
& B = C )
=> C = D )
=> ? [B] :
! [C] :
( in(C,B)
<=> ? [D] :
( ordinal(C)
& D = C
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f356,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f357,conjecture,
! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( in(C,A)
=> ( in(apply(D,C),relation_rng(D))
| B = empty_set ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f358,negated_conjecture,
~ ! [A,B,C,D] :
( ( relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) )
=> ( in(C,A)
=> ( in(apply(D,C),relation_rng(D))
| B = empty_set ) ) ),
inference(negated_conjecture,[status(cth)],[f357]) ).
fof(f385,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f386,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f396,plain,
! [A,B,C] :
( relation(C)
| ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f397,plain,
! [C] :
( relation(C)
| ! [A,B] : ~ element(C,powerset(cartesian_product2(A,B))) ),
inference(miniscoping,[status(thm)],[f396]) ).
fof(f398,plain,
! [X0,X1,X2] :
( relation(X0)
| ~ element(X0,powerset(cartesian_product2(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f519,plain,
! [A,B,C] :
( ( ( ( quasi_total(C,A,B)
<=> C = empty_set )
| A = empty_set
| B != empty_set )
& ( ( quasi_total(C,A,B)
<=> A = relation_dom_as_subset(A,B,C) )
| ( A != empty_set
& B = empty_set ) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f520,definition,
! [A,B] :
( sP2_prd(B,A)
<=> ( A != empty_set
& B = empty_set ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f521,plain,
! [A,B,C] :
( ( ( ( quasi_total(C,A,B)
<=> C = empty_set )
| A = empty_set
| B != empty_set )
& ( ( quasi_total(C,A,B)
<=> A = relation_dom_as_subset(A,B,C) )
| sP2_prd(B,A) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(formula_renaming,[status(thm)],[f519,f520]) ).
fof(f522,plain,
! [A,B,C] :
( ( ( ( ( C != empty_set
| quasi_total(C,A,B) )
& ( C = empty_set
| ~ quasi_total(C,A,B) ) )
| A = empty_set
| B != empty_set )
& ( ( ( A != relation_dom_as_subset(A,B,C)
| quasi_total(C,A,B) )
& ( A = relation_dom_as_subset(A,B,C)
| ~ quasi_total(C,A,B) ) )
| sP2_prd(B,A) ) )
| ~ relation_of2_as_subset(C,A,B) ),
inference(NNF_transformation,[status(thm)],[f521]) ).
fof(f523,plain,
! [X0,X1,X2] :
( X1 = relation_dom_as_subset(X1,X2,X0)
| ~ quasi_total(X0,X1,X2)
| sP2_prd(X2,X1)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f522]) ).
fof(f565,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f566,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f565]) ).
fof(f567,plain,
( ! [A,B] :
( ( ( sK29_skl(B,A) = A
| in(sK29_skl(B,A),B) )
& ( sK29_skl(B,A) != A
| ~ in(sK29_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(C,sK29_skl(B,A))],[f566]) ).
fof(f569,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f567]) ).
fof(f776,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)],[f61]) ).
fof(f777,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)],[f776]) ).
fof(f778,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)],[f777]) ).
fof(f779,plain,
! [A] :
( ( ! [B] :
( ( ( ( sK68_skl(B,A) = apply(A,sK69_skl(B,A))
& in(sK69_skl(B,A),relation_dom(A)) )
| in(sK68_skl(B,A),B) )
& ( ! [D] :
( sK68_skl(B,A) != apply(A,D)
| ~ in(D,relation_dom(A)) )
| ~ in(sK68_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,sK67_skl(C,B,A))
& in(sK67_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,[sK67_skl,sK68_skl,sK69_skl]),skolemize(D,sK67_skl(C,B,A)),skolemize(C,sK68_skl(B,A)),skolemize(D,sK69_skl(B,A))],[f778]) ).
fof(f782,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)],[f779]) ).
fof(f930,plain,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
| ~ relation_of2_as_subset(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f120]) ).
fof(f931,plain,
! [X0,X1,X2] :
( element(X0,powerset(cartesian_product2(X1,X2)))
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f930]) ).
fof(f1124,plain,
( empty(sK105_skl)
& one_to_one(sK105_skl)
& function(sK105_skl)
& relation(sK105_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105_skl]),skolemize(A,sK105_skl)],[f182]) ).
fof(f1128,plain,
empty(sK105_skl),
inference(cnf_transformation,[status(thm)],[f1124]) ).
fof(f1178,plain,
! [A,B,C] :
( relation_dom_as_subset(A,B,C) = relation_dom(C)
| ~ relation_of2(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f196]) ).
fof(f1179,plain,
! [X0,X1,X2] :
( relation_dom_as_subset(X1,X2,X0) = relation_dom(X0)
| ~ relation_of2(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1178]) ).
fof(f1188,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f201]) ).
fof(f1189,plain,
( ! [A,B,C] :
( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ! [A,B,C] :
( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f1188]) ).
fof(f1190,plain,
! [X0,X1,X2] :
( relation_of2(X0,X1,X2)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1189]) ).
fof(f1309,plain,
! [A] :
( ? [B] :
! [C] :
( in(C,B)
<=> ? [D] :
( ordinal(C)
& D = C
& in(D,A) ) )
| ? [B,C,D] :
( C != D
& ordinal(D)
& B = D
& ordinal(C)
& B = C ) ),
inference(pre_NNF_transformation,[status(thm)],[f216]) ).
fof(f1310,definition,
! [B,C,D] :
( sP12_prd(D,C,B)
<=> ( C != D
& ordinal(D)
& B = D
& ordinal(C)
& B = C ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f1820,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f356]) ).
fof(f1821,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1820]) ).
fof(f1822,plain,
? [A,B,C,D] :
( ~ in(apply(D,C),relation_rng(D))
& B != empty_set
& in(C,A)
& relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) ),
inference(pre_NNF_transformation,[status(thm)],[f358]) ).
fof(f1823,plain,
? [A,B,D] :
( ? [C] :
( ~ in(apply(D,C),relation_rng(D))
& B != empty_set
& in(C,A) )
& relation_of2_as_subset(D,A,B)
& quasi_total(D,A,B)
& function(D) ),
inference(miniscoping,[status(thm)],[f1822]) ).
fof(f1824,plain,
( ~ in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl))
& sK221_skl != empty_set
& in(sK223_skl,sK220_skl)
& relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl)
& quasi_total(sK222_skl,sK220_skl,sK221_skl)
& function(sK222_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK220_skl,sK221_skl,sK222_skl,sK223_skl]),skolemize(A,sK220_skl),skolemize(B,sK221_skl),skolemize(D,sK222_skl),skolemize(C,sK223_skl)],[f1823]) ).
fof(f1825,plain,
function(sK222_skl),
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1826,plain,
quasi_total(sK222_skl,sK220_skl,sK221_skl),
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1827,plain,
relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl),
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1828,plain,
in(sK223_skl,sK220_skl),
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1829,plain,
sK221_skl != empty_set,
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1830,plain,
~ in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl)),
inference(cnf_transformation,[status(thm)],[f1824]) ).
fof(f1930,plain,
! [A,B] :
( ( A = empty_set
| B != empty_set
| sP2_prd(B,A) )
& ( ( A != empty_set
& B = empty_set )
| ~ sP2_prd(B,A) ) ),
inference(NNF_transformation,[status(thm)],[f520]) ).
fof(f1931,plain,
( ! [A,B] :
( A = empty_set
| B != empty_set
| sP2_prd(B,A) )
& ! [A,B] :
( ( A != empty_set
& B = empty_set )
| ~ sP2_prd(B,A) ) ),
inference(miniscoping,[status(thm)],[f1930]) ).
fof(f1932,plain,
! [X0,X1] :
( X0 = empty_set
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1931]) ).
fof(f2039,plain,
! [B,C,D] :
( ( C = D
| ~ ordinal(D)
| B != D
| ~ ordinal(C)
| B != C
| sP12_prd(D,C,B) )
& ( ( C != D
& ordinal(D)
& B = D
& ordinal(C)
& B = C )
| ~ sP12_prd(D,C,B) ) ),
inference(NNF_transformation,[status(thm)],[f1310]) ).
fof(f2040,plain,
( ! [B,C,D] :
( C = D
| ~ ordinal(D)
| B != D
| ~ ordinal(C)
| B != C
| sP12_prd(D,C,B) )
& ! [B,C,D] :
( ( C != D
& ordinal(D)
& B = D
& ordinal(C)
& B = C )
| ~ sP12_prd(D,C,B) ) ),
inference(miniscoping,[status(thm)],[f2039]) ).
fof(f2041,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ sP12_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2040]) ).
fof(f2043,plain,
! [X0,X1,X2] :
( X2 = X0
| ~ sP12_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2040]) ).
fof(f2045,plain,
! [X0,X1,X2] :
( X1 != X0
| ~ sP12_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2040]) ).
fof(f2122,definition,
( sQ2_spl
<=> sP12_prd(sK168_skl,sK167_skl,sK166_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2123,plain,
( ~ sQ2_spl
| sP12_prd(sK168_skl,sK167_skl,sK166_skl) ),
inference(component_clause,[status(thm)],[f2122]) ).
fof(f2176,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f569]) ).
fof(f2218,plain,
! [X0,X1] :
( ~ in(X1,relation_dom(X0))
| in(apply(X0,X1),relation_rng(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f782]) ).
fof(f2297,plain,
! [X0,X1] : ~ sP12_prd(X0,X0,X1),
inference(destructive_equality_resolution,[status(thm)],[f2045]) ).
fof(f2315,definition,
( sQ7_spl
<=> relation(sK222_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f2317,plain,
( sQ7_spl
| ~ relation(sK222_skl) ),
inference(component_clause,[status(thm)],[f2315]) ).
fof(f2328,plain,
! [X0,X1] :
( sQ7_spl
| ~ element(sK222_skl,powerset(cartesian_product2(X0,X1))) ),
inference(resolution,[status(thm)],[f2317,f398]) ).
fof(f2340,plain,
! [X0,X1] :
( sQ7_spl
| ~ relation_of2_as_subset(sK222_skl,X0,X1) ),
inference(resolution,[status(thm)],[f931,f2328]) ).
fof(f2370,plain,
( sQ7_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1827,f2340]) ).
fof(f2371,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f2370]) ).
fof(f2396,definition,
( sQ18_spl
<=> function(sK222_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f2398,plain,
( sQ18_spl
| ~ function(sK222_skl) ),
inference(component_clause,[status(thm)],[f2396]) ).
fof(f2415,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2398,f1825]) ).
fof(f2416,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f2415]) ).
fof(f2642,plain,
sK105_skl = empty_set,
inference(resolution,[status(thm)],[f1128,f1821]) ).
fof(f2838,plain,
sK221_skl != sK105_skl,
inference(backward_demodulation,[status(thm)],[f2642,f1829]) ).
fof(f3550,plain,
! [X0] : ~ in(singleton(X0),X0),
inference(resolution,[status(thm)],[f2176,f386]) ).
fof(f5098,definition,
( sQ200_spl
<=> in(sK223_skl,relation_dom(sK222_skl)) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f5099,plain,
( ~ sQ200_spl
| in(sK223_skl,relation_dom(sK222_skl)) ),
inference(component_clause,[status(thm)],[f5098]) ).
fof(f5100,plain,
( sQ200_spl
| ~ in(sK223_skl,relation_dom(sK222_skl)) ),
inference(component_clause,[status(thm)],[f5098]) ).
fof(f10362,plain,
relation_of2(sK222_skl,sK220_skl,sK221_skl),
inference(resolution,[status(thm)],[f1190,f1827]) ).
fof(f11389,plain,
! [X0,X1] :
( X0 = sK105_skl
| ~ sP2_prd(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f2642,f1932]) ).
fof(f11391,plain,
! [X0,X1,X2] :
( X2 = relation_dom_as_subset(X2,X0,X1)
| ~ quasi_total(X1,X2,X0)
| ~ relation_of2_as_subset(X1,X2,X0)
| X0 = sK105_skl ),
inference(resolution,[status(thm)],[f11389,f523]) ).
fof(f11738,plain,
( ~ sQ200_spl
| in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl))
| ~ function(sK222_skl)
| ~ relation(sK222_skl) ),
inference(resolution,[status(thm)],[f5099,f2218]) ).
fof(f11759,definition,
( sQ615_spl
<=> in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl)) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f11760,plain,
( ~ sQ615_spl
| in(apply(sK222_skl,sK223_skl),relation_rng(sK222_skl)) ),
inference(component_clause,[status(thm)],[f11759]) ).
fof(f11762,plain,
( ~ sQ200_spl
| sQ615_spl
| ~ sQ18_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f11738,f2315,f2396,f11759,f5098]) ).
fof(f11771,plain,
( ~ sQ615_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11760,f1830]) ).
fof(f11772,plain,
~ sQ615_spl,
inference(contradiction_clause,[status(thm)],[f11771]) ).
fof(f14889,definition,
( sQ711_spl
<=> relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl) = sK220_skl ),
introduced(definition,[new_symbols(definition,[sQ711_spl])],[split_symbol_definition]) ).
fof(f14890,plain,
( ~ sQ711_spl
| relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl) = sK220_skl ),
inference(component_clause,[status(thm)],[f14889]) ).
fof(f20573,definition,
( sQ901_spl
<=> sK221_skl = sK105_skl ),
introduced(definition,[new_symbols(definition,[sQ901_spl])],[split_symbol_definition]) ).
fof(f20574,plain,
( ~ sQ901_spl
| sK221_skl = sK105_skl ),
inference(component_clause,[status(thm)],[f20573]) ).
fof(f20604,plain,
( ~ sQ901_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20574,f2838]) ).
fof(f20605,plain,
~ sQ901_spl,
inference(contradiction_clause,[status(thm)],[f20604]) ).
fof(f23013,plain,
( ~ sQ2_spl
| sK166_skl = sK168_skl ),
inference(resolution,[status(thm)],[f2123,f2043]) ).
fof(f23014,plain,
( ~ sQ2_spl
| sK166_skl = sK167_skl ),
inference(resolution,[status(thm)],[f2123,f2041]) ).
fof(f23104,plain,
( ~ sQ2_spl
| sP12_prd(sK166_skl,sK167_skl,sK166_skl) ),
inference(backward_demodulation,[status(thm)],[f23013,f2123]) ).
fof(f32910,plain,
( sK220_skl = relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl)
| ~ relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl)
| sK221_skl = sK105_skl ),
inference(resolution,[status(thm)],[f11391,f1826]) ).
fof(f32913,definition,
( sQ1430_spl
<=> relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl) ),
introduced(definition,[new_symbols(definition,[sQ1430_spl])],[split_symbol_definition]) ).
fof(f32915,plain,
( sQ1430_spl
| ~ relation_of2_as_subset(sK222_skl,sK220_skl,sK221_skl) ),
inference(component_clause,[status(thm)],[f32913]) ).
fof(f32916,plain,
( sQ711_spl
| ~ sQ1430_spl
| sQ901_spl ),
inference(split_clause,[status(thm)],[f32910,f20573,f32913,f14889]) ).
fof(f32917,plain,
( sQ1430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32915,f1827]) ).
fof(f32918,plain,
sQ1430_spl,
inference(contradiction_clause,[status(thm)],[f32917]) ).
fof(f36521,definition,
! [X0] :
( sQ1563_spl
<=> in(X0,relation_dom(sK222_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1563_spl])],[split_symbol_definition]) ).
fof(f36522,plain,
! [X0] :
( ~ sQ1563_spl
| in(X0,relation_dom(sK222_skl)) ),
inference(component_clause,[status(thm)],[f36521]) ).
fof(f36545,plain,
( ~ sQ1563_spl
| $false ),
inference(resolution,[status(thm)],[f36522,f3550]) ).
fof(f36622,plain,
~ sQ1563_spl,
inference(contradiction_clause,[status(thm)],[f36545]) ).
fof(f38950,plain,
( ~ sQ2_spl
| sP12_prd(sK166_skl,sK166_skl,sK166_skl) ),
inference(forward_demodulation,[status(thm)],[f23014,f23104]) ).
fof(f38951,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38950,f2297]) ).
fof(f38952,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f38951]) ).
fof(f39716,plain,
relation_dom_as_subset(sK220_skl,sK221_skl,sK222_skl) = relation_dom(sK222_skl),
inference(resolution,[status(thm)],[f1179,f10362]) ).
fof(f39723,plain,
( ~ sQ711_spl
| sK220_skl = relation_dom(sK222_skl) ),
inference(forward_demodulation,[status(thm)],[f14890,f39716]) ).
fof(f39846,plain,
( sQ200_spl
| ~ sQ711_spl
| ~ in(sK223_skl,sK220_skl) ),
inference(backward_demodulation,[status(thm)],[f39723,f5100]) ).
fof(f39873,plain,
( sQ200_spl
| ~ sQ711_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f39846,f1828]) ).
fof(f39874,plain,
( sQ200_spl
| ~ sQ711_spl ),
inference(contradiction_clause,[status(thm)],[f39873]) ).
fof(f39875,plain,
$false,
inference(sat_refutation,[status(thm)],[f2371,f2416,f11762,f11772,f20605,f32916,f32918,f36622,f38952,f39874]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU290+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/10.35 % Computer : n012.cluster.edu
% 0.07/10.35 % Model : x86_64 x86_64
% 0.07/10.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/10.35 % Memory : 8046.5625MB
% 0.07/10.35 % OS : Linux 6.8.0-71-generic
% 0.07/10.35 % CPULimit : 300
% 0.07/10.35 % WCLimit : 300
% 0.07/10.35 % DateTime : Mon Sep 21 06:08:05 UTC 2026
% 0.07/10.35 % CPUTime :
% 0.07/10.38 % Drodi V4.1.1
% 166.41/31.34 % Refutation found
% 166.41/31.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 166.41/31.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.45/31.41 % Elapsed time: 21.038850 seconds
% 6.45/31.41 % CPU time: 167.208169 seconds
% 6.45/31.41 % Total memory used: 763.541 MB
% 6.45/31.41 % Net memory used: 665.994 MB
%------------------------------------------------------------------------------