%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU303+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 : n003.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:05 PM UTC 2026
% Result : Theorem 70.52s 9.51s
% Output : CNFRefutation 69.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 31
% Syntax : Number of formulae : 138 ( 39 unt; 14 def)
% Number of atoms : 357 ( 93 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 360 ( 141 ~; 132 |; 52 &)
% ( 23 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 14 prp; 0-4 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-4 aty)
% Number of variables : 186 ( 177 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( empty(A)
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B,C,D] :
( D = unordered_triple(A,B,C)
<=> ! [E] :
( in(E,D)
<=> ~ ( E != C
& E != B
& E != A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,axiom,
! [A] :
( empty(A)
=> ( relation(relation_inverse(A))
& empty(relation_inverse(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [A,B] :
( ( finite(B)
& function(A)
& relation(A) )
=> finite(relation_image(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,lemma,
! [A] :
( relation(A)
=> relation_image(A,relation_dom(A)) = relation_rng(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
=> finite(relation_rng(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f319,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( finite(relation_dom(A))
=> finite(relation_rng(A)) ) ),
inference(negated_conjecture,[status(cth)],[f318]) ).
fof(f328,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f384,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f393,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f422,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f423,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f430,plain,
! [A] :
( finite(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f431,plain,
! [X0] :
( finite(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f430]) ).
fof(f447,plain,
! [A] :
( ! [B] :
( finite(B)
| ~ element(B,powerset(A)) )
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f448,plain,
! [X0,X1] :
( finite(X1)
| ~ element(X1,powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f556,plain,
! [A,B,C,D] :
( D = unordered_triple(A,B,C)
<=> ! [E] :
( in(E,D)
<=> ( E = C
| E = B
| E = A ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f557,definition,
! [A,B,C,E] :
( sP1_prd(E,C,B,A)
<=> ( E = C
| E = B
| E = A ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f558,plain,
! [A,B,C,D] :
( D = unordered_triple(A,B,C)
<=> ! [E] :
( in(E,D)
<=> sP1_prd(E,C,B,A) ) ),
inference(formula_renaming,[status(thm)],[f556,f557]) ).
fof(f559,plain,
! [A,B,C,D] :
( ( ? [E] :
( ( sP1_prd(E,C,B,A)
| in(E,D) )
& ( ~ sP1_prd(E,C,B,A)
| ~ in(E,D) ) )
| D = unordered_triple(A,B,C) )
& ( ! [E] :
( ( ~ sP1_prd(E,C,B,A)
| in(E,D) )
& ( sP1_prd(E,C,B,A)
| ~ in(E,D) ) )
| D != unordered_triple(A,B,C) ) ),
inference(NNF_transformation,[status(thm)],[f558]) ).
fof(f560,plain,
( ! [A,B,C,D] :
( ? [E] :
( ( sP1_prd(E,C,B,A)
| in(E,D) )
& ( ~ sP1_prd(E,C,B,A)
| ~ in(E,D) ) )
| D = unordered_triple(A,B,C) )
& ! [A,B,C,D] :
( ( ! [E] :
( ~ sP1_prd(E,C,B,A)
| in(E,D) )
& ! [E] :
( sP1_prd(E,C,B,A)
| ~ in(E,D) ) )
| D != unordered_triple(A,B,C) ) ),
inference(miniscoping,[status(thm)],[f559]) ).
fof(f561,plain,
( ! [A,B,C,D] :
( ( ( sP1_prd(sK16_skl(D,C,B,A),C,B,A)
| in(sK16_skl(D,C,B,A),D) )
& ( ~ sP1_prd(sK16_skl(D,C,B,A),C,B,A)
| ~ in(sK16_skl(D,C,B,A),D) ) )
| D = unordered_triple(A,B,C) )
& ! [A,B,C,D] :
( ( ! [E] :
( ~ sP1_prd(E,C,B,A)
| in(E,D) )
& ! [E] :
( sP1_prd(E,C,B,A)
| ~ in(E,D) ) )
| D != unordered_triple(A,B,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(E,sK16_skl(D,C,B,A))],[f560]) ).
fof(f563,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP1_prd(X4,X3,X2,X1)
| in(X4,X0)
| X0 != unordered_triple(X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f561]) ).
fof(f656,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f657,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f656]) ).
fof(f658,plain,
( ! [A] :
( in(sK34_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(B,sK34_skl(A))],[f657]) ).
fof(f659,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f658]) ).
fof(f697,plain,
! [A,B,C] :
( ( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ( ! [D] :
( ( ( D != B
& D != A )
| in(D,C) )
& ( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f698,plain,
( ! [A,B,C] :
( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(miniscoping,[status(thm)],[f697]) ).
fof(f699,plain,
( ! [A,B,C] :
( ( ( sK41_skl(C,B,A) = B
| sK41_skl(C,B,A) = A
| in(sK41_skl(C,B,A),C) )
& ( ( sK41_skl(C,B,A) != B
& sK41_skl(C,B,A) != A )
| ~ in(sK41_skl(C,B,A),C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(D,sK41_skl(C,B,A))],[f698]) ).
fof(f702,plain,
! [X0,X1,X2,X3] :
( X3 != X2
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f871,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f1009,plain,
! [A] : element(sK92_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92_skl]),skolemize(B,sK92_skl(A))],[f130]) ).
fof(f1010,plain,
! [X0] : element(sK92_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f1009]) ).
fof(f1022,plain,
! [A] :
( ( relation(relation_inverse(A))
& empty(relation_inverse(A)) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f135]) ).
fof(f1023,plain,
! [X0] :
( empty(relation_inverse(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1022]) ).
fof(f1028,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f1029,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f1031,plain,
! [A,B] :
( finite(relation_image(A,B))
| ~ finite(B)
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f1032,plain,
! [X0,X1] :
( finite(relation_image(X0,X1))
| ~ finite(X1)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1031]) ).
fof(f1219,plain,
( finite(sK105_skl)
& ~ empty(sK105_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105_skl]),skolemize(A,sK105_skl)],[f196]) ).
fof(f1221,plain,
finite(sK105_skl),
inference(cnf_transformation,[status(thm)],[f1219]) ).
fof(f1712,plain,
! [A] :
( relation_image(A,relation_dom(A)) = relation_rng(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f277]) ).
fof(f1713,plain,
! [X0] :
( relation_image(X0,relation_dom(X0)) = relation_rng(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1712]) ).
fof(f1844,plain,
? [A] :
( ~ finite(relation_rng(A))
& finite(relation_dom(A))
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f319]) ).
fof(f1845,plain,
( ~ finite(relation_rng(sK248_skl))
& finite(relation_dom(sK248_skl))
& function(sK248_skl)
& relation(sK248_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK248_skl]),skolemize(A,sK248_skl)],[f1844]) ).
fof(f1846,plain,
relation(sK248_skl),
inference(cnf_transformation,[status(thm)],[f1845]) ).
fof(f1847,plain,
function(sK248_skl),
inference(cnf_transformation,[status(thm)],[f1845]) ).
fof(f1848,plain,
finite(relation_dom(sK248_skl)),
inference(cnf_transformation,[status(thm)],[f1845]) ).
fof(f1849,plain,
~ finite(relation_rng(sK248_skl)),
inference(cnf_transformation,[status(thm)],[f1845]) ).
fof(f1875,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f2059,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f2087,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f393]) ).
fof(f2088,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f2087]) ).
fof(f2192,plain,
! [A,B,C,E] :
( ( ( E != C
& E != B
& E != A )
| sP1_prd(E,C,B,A) )
& ( E = C
| E = B
| E = A
| ~ sP1_prd(E,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f557]) ).
fof(f2193,plain,
( ! [A,B,C,E] :
( ( E != C
& E != B
& E != A )
| sP1_prd(E,C,B,A) )
& ! [A,B,C,E] :
( E = C
| E = B
| E = A
| ~ sP1_prd(E,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f2192]) ).
fof(f2197,plain,
! [X0,X1,X2,X3] :
( X0 != X1
| sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f2193]) ).
fof(f2796,plain,
! [X0,X1,X2,X3] :
( ~ sP1_prd(X0,X3,X2,X1)
| in(X0,unordered_triple(X1,X2,X3)) ),
inference(destructive_equality_resolution,[status(thm)],[f563]) ).
fof(f2820,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f659]) ).
fof(f2828,plain,
! [X0,X1] : in(X0,unordered_pair(X1,X0)),
inference(destructive_equality_resolution,[status(thm)],[f702]) ).
fof(f2922,plain,
! [X0,X1,X2] : sP1_prd(X0,X0,X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f2197]) ).
fof(f2986,plain,
finite(empty_set),
inference(resolution,[status(thm)],[f1028,f431]) ).
fof(f5105,plain,
! [X0,X1,X2] : in(X0,unordered_triple(X1,X2,X0)),
inference(resolution,[status(thm)],[f2796,f2922]) ).
fof(f5163,plain,
empty(relation_inverse(empty_set)),
inference(resolution,[status(thm)],[f1023,f1028]) ).
fof(f5172,plain,
relation_inverse(empty_set) = empty_set,
inference(resolution,[status(thm)],[f5163,f2088]) ).
fof(f5195,definition,
( sQ183_spl
<=> relation_rng(relation_rng(relation_inverse(empty_set))) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f5197,plain,
( sQ183_spl
| relation_rng(relation_rng(relation_inverse(empty_set))) != empty_set ),
inference(component_clause,[status(thm)],[f5195]) ).
fof(f5263,definition,
( sQ195_spl
<=> relation(sK248_skl) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f5265,plain,
( sQ195_spl
| ~ relation(sK248_skl) ),
inference(component_clause,[status(thm)],[f5263]) ).
fof(f5421,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5265,f1846]) ).
fof(f5422,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f5421]) ).
fof(f6188,plain,
! [X0,X1,X2] : ~ in(unordered_triple(X0,X1,X2),X2),
inference(resolution,[status(thm)],[f5105,f423]) ).
fof(f9735,plain,
! [X0] :
( finite(X0)
| ~ element(X0,powerset(sK105_skl)) ),
inference(resolution,[status(thm)],[f448,f1221]) ).
fof(f11838,definition,
( sQ630_spl
<=> finite(relation_dom(sK248_skl)) ),
introduced(definition,[new_symbols(definition,[sQ630_spl])],[split_symbol_definition]) ).
fof(f11840,plain,
( sQ630_spl
| ~ finite(relation_dom(sK248_skl)) ),
inference(component_clause,[status(thm)],[f11838]) ).
fof(f16659,plain,
! [X0,X1] : in(singleton(X0),ordered_pair(X0,X1)),
inference(paramodulation,[status(thm)],[f871,f2828]) ).
fof(f17328,plain,
finite(sK92_skl(powerset(sK105_skl))),
inference(resolution,[status(thm)],[f9735,f1010]) ).
fof(f21653,definition,
( sQ1349_spl
<=> finite(relation_rng(sK248_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1349_spl])],[split_symbol_definition]) ).
fof(f21654,plain,
( ~ sQ1349_spl
| finite(relation_rng(sK248_skl)) ),
inference(component_clause,[status(thm)],[f21653]) ).
fof(f21658,plain,
( ~ sQ1349_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21654,f1849]) ).
fof(f21659,plain,
~ sQ1349_spl,
inference(contradiction_clause,[status(thm)],[f21658]) ).
fof(f23181,plain,
! [X0] :
( finite(relation_image(sK248_skl,X0))
| ~ finite(X0)
| ~ relation(sK248_skl) ),
inference(resolution,[status(thm)],[f1032,f1847]) ).
fof(f23195,definition,
! [X0] :
( sQ1408_spl
<=> ( finite(relation_image(sK248_skl,X0))
| ~ finite(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1408_spl])],[split_symbol_definition]) ).
fof(f23196,plain,
! [X0] :
( ~ sQ1408_spl
| finite(relation_image(sK248_skl,X0))
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f23195]) ).
fof(f23198,plain,
( sQ1408_spl
| ~ sQ195_spl ),
inference(split_clause,[status(thm)],[f23181,f5263,f23195]) ).
fof(f27391,definition,
! [X0,X1] :
( sQ1675_spl
<=> ~ in(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ1675_spl])],[split_symbol_definition]) ).
fof(f27392,plain,
! [X0,X1] :
( ~ sQ1675_spl
| ~ in(X0,X1) ),
inference(component_clause,[status(thm)],[f27391]) ).
fof(f27423,plain,
( sQ630_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11840,f1848]) ).
fof(f27424,plain,
sQ630_spl,
inference(contradiction_clause,[status(thm)],[f27423]) ).
fof(f27623,plain,
( ~ sQ1675_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f16659,f27392]) ).
fof(f27664,plain,
~ sQ1675_spl,
inference(contradiction_clause,[status(thm)],[f27623]) ).
fof(f28338,definition,
( sQ1722_spl
<=> finite(sK92_skl(powerset(sK105_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1722_spl])],[split_symbol_definition]) ).
fof(f28340,plain,
( sQ1722_spl
| ~ finite(sK92_skl(powerset(sK105_skl))) ),
inference(component_clause,[status(thm)],[f28338]) ).
fof(f28344,plain,
( sQ1722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28340,f17328]) ).
fof(f28345,plain,
sQ1722_spl,
inference(contradiction_clause,[status(thm)],[f28344]) ).
fof(f28631,definition,
! [X0] :
( sQ1735_spl
<=> ( ~ finite(X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1735_spl])],[split_symbol_definition]) ).
fof(f28632,plain,
! [X0] :
( ~ sQ1735_spl
| ~ finite(X0)
| ~ relation(X0) ),
inference(component_clause,[status(thm)],[f28631]) ).
fof(f28650,definition,
( sQ1740_spl
<=> in(apply(sK109_skl,sK34_skl(relation_dom(sK109_skl))),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1740_spl])],[split_symbol_definition]) ).
fof(f28651,plain,
( ~ sQ1740_spl
| in(apply(sK109_skl,sK34_skl(relation_dom(sK109_skl))),empty_set) ),
inference(component_clause,[status(thm)],[f28650]) ).
fof(f28666,definition,
! [X0] :
( sQ1744_spl
<=> ( in(apply(sK109_skl,sK27_skl(X0,set_meet(relation_dom(sK109_skl)),relation_dom(sK109_skl))),empty_set)
| in(X0,set_meet(relation_dom(sK109_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ1744_spl])],[split_symbol_definition]) ).
fof(f28667,plain,
! [X0] :
( ~ sQ1744_spl
| in(apply(sK109_skl,sK27_skl(X0,set_meet(relation_dom(sK109_skl)),relation_dom(sK109_skl))),empty_set)
| in(X0,set_meet(relation_dom(sK109_skl))) ),
inference(component_clause,[status(thm)],[f28666]) ).
fof(f28670,definition,
( sQ1745_spl
<=> in(apply(sK109_skl,sK25_skl(relation_dom(sK109_skl))),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1745_spl])],[split_symbol_definition]) ).
fof(f28671,plain,
( ~ sQ1745_spl
| in(apply(sK109_skl,sK25_skl(relation_dom(sK109_skl))),empty_set) ),
inference(component_clause,[status(thm)],[f28670]) ).
fof(f28753,plain,
( ~ sQ1745_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28671,f2820]) ).
fof(f28754,plain,
~ sQ1745_spl,
inference(contradiction_clause,[status(thm)],[f28753]) ).
fof(f28755,plain,
! [X0] :
( ~ sQ1744_spl
| in(X0,set_meet(relation_dom(sK109_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f28667,f2820]) ).
fof(f28759,plain,
( ~ sQ1740_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28651,f2820]) ).
fof(f28760,plain,
~ sQ1740_spl,
inference(contradiction_clause,[status(thm)],[f28759]) ).
fof(f28809,plain,
( ~ sQ1735_spl
| ~ finite(empty_set) ),
inference(resolution,[status(thm)],[f28632,f1029]) ).
fof(f28811,plain,
( ~ sQ1735_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28809,f2986]) ).
fof(f28812,plain,
~ sQ1735_spl,
inference(contradiction_clause,[status(thm)],[f28811]) ).
fof(f29141,plain,
( ~ sQ1744_spl
| $false ),
inference(resolution,[status(thm)],[f28755,f6188]) ).
fof(f29168,plain,
~ sQ1744_spl,
inference(contradiction_clause,[status(thm)],[f29141]) ).
fof(f30911,definition,
( sQ1812_spl
<=> subset(empty_set,sK248_skl) ),
introduced(definition,[new_symbols(definition,[sQ1812_spl])],[split_symbol_definition]) ).
fof(f30913,plain,
( sQ1812_spl
| ~ subset(empty_set,sK248_skl) ),
inference(component_clause,[status(thm)],[f30911]) ).
fof(f30918,plain,
( sQ1812_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30913,f1875]) ).
fof(f30919,plain,
sQ1812_spl,
inference(contradiction_clause,[status(thm)],[f30918]) ).
fof(f31209,plain,
( sQ183_spl
| relation_rng(relation_rng(empty_set)) != empty_set ),
inference(forward_demodulation,[status(thm)],[f5172,f5197]) ).
fof(f31210,plain,
( sQ183_spl
| relation_rng(empty_set) != empty_set ),
inference(forward_demodulation,[status(thm)],[f2059,f31209]) ).
fof(f31211,plain,
( sQ183_spl
| empty_set != empty_set ),
inference(forward_demodulation,[status(thm)],[f2059,f31210]) ).
fof(f31212,plain,
( sQ183_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f31211]) ).
fof(f31213,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f31212]) ).
fof(f36063,definition,
( sQ1983_spl
<=> subset(empty_set,relation_dom(sK118_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1983_spl])],[split_symbol_definition]) ).
fof(f36065,plain,
( sQ1983_spl
| ~ subset(empty_set,relation_dom(sK118_skl)) ),
inference(component_clause,[status(thm)],[f36063]) ).
fof(f36075,plain,
( sQ1983_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36065,f1875]) ).
fof(f36076,plain,
sQ1983_spl,
inference(contradiction_clause,[status(thm)],[f36075]) ).
fof(f36115,plain,
relation_image(sK248_skl,relation_dom(sK248_skl)) = relation_rng(sK248_skl),
inference(resolution,[status(thm)],[f1713,f1846]) ).
fof(f36180,plain,
( ~ sQ1408_spl
| finite(relation_rng(sK248_skl))
| ~ finite(relation_dom(sK248_skl)) ),
inference(paramodulation,[status(thm)],[f36115,f23196]) ).
fof(f36186,plain,
( ~ sQ1408_spl
| sQ1349_spl
| ~ sQ630_spl ),
inference(split_clause,[status(thm)],[f36180,f11838,f21653,f23195]) ).
fof(f36201,plain,
$false,
inference(sat_refutation,[status(thm)],[f5422,f21659,f23198,f27424,f27664,f28345,f28754,f28760,f28812,f29168,f30919,f31213,f36076,f36186]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU303+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.43 % Computer : n003.cluster.edu
% 0.14/0.43 % Model : x86_64 x86_64
% 0.14/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.43 % Memory : 8046.5625MB
% 0.14/0.43 % OS : Linux 6.8.0-71-generic
% 0.14/0.43 % CPULimit : 300
% 0.14/0.43 % WCLimit : 300
% 0.14/0.43 % DateTime : Mon Sep 21 06:11:15 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.48 % Drodi V4.1.1
% 70.52/9.51 % Refutation found
% 70.52/9.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 70.52/9.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 69.09/9.57 % Elapsed time: 9.125827 seconds
% 69.09/9.57 % CPU time: 71.641344 seconds
% 69.09/9.57 % Total memory used: 413.959 MB
% 69.09/9.57 % Net memory used: 371.146 MB
%------------------------------------------------------------------------------