%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU157+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 : n016.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:26 PM UTC 2026
% Result : Theorem 89.04s 11.65s
% Output : CNFRefutation 89.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 24
% Syntax : Number of formulae : 121 ( 15 unt; 13 def)
% Number of atoms : 323 ( 80 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 340 ( 138 ~; 134 |; 42 &)
% ( 24 <=>; 1 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 13 prp; 0-5 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-4 aty)
% Number of variables : 228 ( 204 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B,C] :
( C = cartesian_product2(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E,F] :
( D = ordered_pair(E,F)
& in(F,B)
& in(E,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_intersection2(A,B) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f61,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,lemma,
! [A,B,C,D] :
( ordered_pair(A,B) = ordered_pair(C,D)
=> ( B = D
& A = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,lemma,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f97,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f96]) ).
fof(f99,plain,
! [X0,X1] :
( subset(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f108,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f109,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f108]) ).
fof(f110,plain,
( ! [A] :
( in(sK1_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f138,definition,
! [A,B,D,E,F] :
( sP0_prd(F,E,D,B,A)
<=> ( D = ordered_pair(E,F)
& in(F,B)
& in(E,A) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f139,plain,
! [A,B,C] :
( C = cartesian_product2(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E,F] : sP0_prd(F,E,D,B,A) ) ),
inference(formula_renaming,[status(thm)],[f12,f138]) ).
fof(f140,plain,
! [A,B,C] :
( ( ? [D] :
( ( ? [E,F] : sP0_prd(F,E,D,B,A)
| in(D,C) )
& ( ! [E,F] : ~ sP0_prd(F,E,D,B,A)
| ~ in(D,C) ) )
| C = cartesian_product2(A,B) )
& ( ! [D] :
( ( ! [E,F] : ~ sP0_prd(F,E,D,B,A)
| in(D,C) )
& ( ? [E,F] : sP0_prd(F,E,D,B,A)
| ~ in(D,C) ) )
| C != cartesian_product2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
( ! [A,B,C] :
( ? [D] :
( ( ? [E,F] : sP0_prd(F,E,D,B,A)
| in(D,C) )
& ( ! [E,F] : ~ sP0_prd(F,E,D,B,A)
| ~ in(D,C) ) )
| C = cartesian_product2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ! [E,F] : ~ sP0_prd(F,E,D,B,A)
| in(D,C) )
& ! [D] :
( ? [E,F] : sP0_prd(F,E,D,B,A)
| ~ in(D,C) ) )
| C != cartesian_product2(A,B) ) ),
inference(miniscoping,[status(thm)],[f140]) ).
fof(f142,plain,
( ! [A,B,C] :
( ( ( sP0_prd(sK9_skl(C,B,A),sK8_skl(C,B,A),sK7_skl(C,B,A),B,A)
| in(sK7_skl(C,B,A),C) )
& ( ! [E,F] : ~ sP0_prd(F,E,sK7_skl(C,B,A),B,A)
| ~ in(sK7_skl(C,B,A),C) ) )
| C = cartesian_product2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ! [E,F] : ~ sP0_prd(F,E,D,B,A)
| in(D,C) )
& ! [D] :
( sP0_prd(sK6_skl(D,C,B,A),sK5_skl(D,C,B,A),D,B,A)
| ~ in(D,C) ) )
| C != cartesian_product2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(E,sK5_skl(D,C,B,A)),skolemize(F,sK6_skl(D,C,B,A)),skolemize(D,sK7_skl(C,B,A)),skolemize(E,sK8_skl(C,B,A)),skolemize(F,sK9_skl(C,B,A))],[f141]) ).
fof(f143,plain,
! [X0,X1,X2,X3] :
( sP0_prd(sK6_skl(X3,X0,X2,X1),sK5_skl(X3,X0,X2,X1),X3,X2,X1)
| ~ in(X3,X0)
| X0 != cartesian_product2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sP0_prd(X4,X5,X3,X2,X1)
| in(X3,X0)
| X0 != cartesian_product2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f182,plain,
! [A,B] :
( ( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f183,plain,
( ! [A,B] :
( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ! [A,B] :
( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f185,plain,
! [X0,X1] :
( set_intersection2(X0,X1) != empty_set
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f205,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f230,plain,
? [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<~> ( in(B,D)
& in(A,C) ) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f231,plain,
? [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(NNF_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
( ( ~ in(sK17_skl,sK19_skl)
| ~ in(sK16_skl,sK18_skl)
| ~ in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) )
& ( ( in(sK17_skl,sK19_skl)
& in(sK16_skl,sK18_skl) )
| in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl),skolemize(C,sK18_skl),skolemize(D,sK19_skl)],[f231]) ).
fof(f233,plain,
( in(sK16_skl,sK18_skl)
| in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f234,plain,
( in(sK17_skl,sK19_skl)
| in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f235,plain,
( ~ in(sK17_skl,sK19_skl)
| ~ in(sK16_skl,sK18_skl)
| ~ in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f262,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f272,plain,
! [A,B,C,D] :
( ( B = D
& A = C )
| ordered_pair(A,B) != ordered_pair(C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f65]) ).
fof(f273,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| ordered_pair(X0,X1) != ordered_pair(X2,X3) ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f274,plain,
! [X0,X1,X2,X3] :
( ordered_pair(X2,X1) != ordered_pair(X3,X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f276,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f277,plain,
( ! [A,B] :
( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ! [A,B] :
( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(miniscoping,[status(thm)],[f276]) ).
fof(f278,plain,
! [X0,X1] :
( set_difference(X0,X1) != empty_set
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f294,plain,
! [X0] : empty_set = set_difference(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f314,plain,
! [A,B] :
( ( set_difference(A,B) != A
| disjoint(A,B) )
& ( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f84]) ).
fof(f315,plain,
( ! [A,B] :
( set_difference(A,B) != A
| disjoint(A,B) )
& ! [A,B] :
( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f314]) ).
fof(f317,plain,
! [X0,X1] :
( X0 != set_difference(X0,X1)
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f329,plain,
! [A,B,D,E,F] :
( ( D != ordered_pair(E,F)
| ~ in(F,B)
| ~ in(E,A)
| sP0_prd(F,E,D,B,A) )
& ( ( D = ordered_pair(E,F)
& in(F,B)
& in(E,A) )
| ~ sP0_prd(F,E,D,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f138]) ).
fof(f330,plain,
( ! [A,B,D,E,F] :
( D != ordered_pair(E,F)
| ~ in(F,B)
| ~ in(E,A)
| sP0_prd(F,E,D,B,A) )
& ! [A,B,D,E,F] :
( ( D = ordered_pair(E,F)
& in(F,B)
& in(E,A) )
| ~ sP0_prd(F,E,D,B,A) ) ),
inference(miniscoping,[status(thm)],[f329]) ).
fof(f331,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP0_prd(X2,X0,X3,X4,X1)
| in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f332,plain,
! [X0,X1,X2,X3,X4] :
( in(X0,X3)
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f333,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP0_prd(X1,X0,X2,X3,X4)
| ordered_pair(X0,X1) = X2 ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f334,plain,
! [X0,X1,X2,X3,X4] :
( X2 != ordered_pair(X1,X0)
| ~ in(X0,X3)
| ~ in(X1,X4)
| sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f335,definition,
( sQ0_spl
<=> in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( ~ sQ0_spl
| in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f337,plain,
( sQ0_spl
| ~ in(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl)) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ1_spl
<=> in(sK16_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( ~ sQ1_spl
| in(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f340,plain,
( sQ1_spl
| ~ in(sK16_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f233,f335,f338]) ).
fof(f342,definition,
( sQ2_spl
<=> in(sK17_skl,sK19_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ2_spl
| in(sK17_skl,sK19_skl) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f344,plain,
( sQ2_spl
| ~ in(sK17_skl,sK19_skl) ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f234,f335,f342]) ).
fof(f346,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f235,f335,f338,f342]) ).
fof(f352,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f99]) ).
fof(f357,plain,
! [X0,X1,X2,X3,X4] :
( in(X2,cartesian_product2(X4,X3))
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(destructive_equality_resolution,[status(thm)],[f144]) ).
fof(f358,plain,
! [X0,X1,X2] :
( sP0_prd(sK6_skl(X0,cartesian_product2(X1,X2),X2,X1),sK5_skl(X0,cartesian_product2(X1,X2),X2,X1),X0,X2,X1)
| ~ in(X0,cartesian_product2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f143]) ).
fof(f367,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X2,X0,ordered_pair(X0,X2),X3,X1)
| ~ in(X2,X3)
| ~ in(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f334]) ).
fof(f373,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f111]) ).
fof(f656,plain,
! [X0,X1,X2] :
( sQ1_spl
| ~ sP0_prd(X0,sK16_skl,X1,X2,sK18_skl) ),
inference(resolution,[status(thm)],[f331,f340]) ).
fof(f718,plain,
( ~ sQ0_spl
| sP0_prd(sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f358,f336]) ).
fof(f979,plain,
! [X0] :
( empty_set != empty_set
| disjoint(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f294,f317]) ).
fof(f981,plain,
! [X0] :
( empty_set != empty_set
| subset(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f294,f278]) ).
fof(f983,definition,
! [X0] :
( sQ6_spl
<=> subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f986,definition,
( sQ7_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f988,plain,
( sQ7_spl
| empty_set != empty_set ),
inference(component_clause,[status(thm)],[f986]) ).
fof(f989,plain,
( ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f981,f983,f986]) ).
fof(f991,definition,
! [X0] :
( sQ8_spl
<=> disjoint(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f994,plain,
( ~ sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f979,f991,f986]) ).
fof(f995,plain,
( sQ7_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f988]) ).
fof(f996,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f995]) ).
fof(f999,plain,
( ~ sQ0_spl
| ordered_pair(sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl)) = ordered_pair(sK16_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f333,f718]) ).
fof(f1037,definition,
! [X1] :
( sQ10_spl
<=> ~ subset(cartesian_product2(sK18_skl,sK19_skl),X1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1038,plain,
! [X0] :
( ~ sQ10_spl
| ~ subset(cartesian_product2(sK18_skl,sK19_skl),X0) ),
inference(component_clause,[status(thm)],[f1037]) ).
fof(f1041,definition,
( sQ11_spl
<=> in(ordered_pair(sK16_skl,sK17_skl),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( ~ sQ11_spl
| in(ordered_pair(sK16_skl,sK17_skl),empty_set) ),
inference(component_clause,[status(thm)],[f1041]) ).
fof(f1103,plain,
( ~ sQ10_spl
| $false ),
inference(resolution,[status(thm)],[f1038,f352]) ).
fof(f1104,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1103]) ).
fof(f1141,plain,
! [X0,X1] :
( sQ0_spl
| ~ sP0_prd(X0,X1,ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f337,f357]) ).
fof(f1294,definition,
( sQ15_spl
<=> empty_set = singleton(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1295,plain,
( ~ sQ15_spl
| empty_set = singleton(sK17_skl) ),
inference(component_clause,[status(thm)],[f1294]) ).
fof(f1398,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1295,f205]) ).
fof(f1399,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1398]) ).
fof(f1426,definition,
( sQ18_spl
<=> empty_set = singleton(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( ~ sQ18_spl
| empty_set = singleton(sK16_skl) ),
inference(component_clause,[status(thm)],[f1426]) ).
fof(f1449,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1427,f205]) ).
fof(f1450,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1449]) ).
fof(f1524,plain,
! [X0] :
( empty_set != empty_set
| disjoint(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f262,f185]) ).
fof(f1529,definition,
! [X0] :
( sQ20_spl
<=> disjoint(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1532,plain,
( ~ sQ7_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1524,f1529,f986]) ).
fof(f1599,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ in(X0,X1)
| sP0_prd(sK17_skl,X0,ordered_pair(X0,sK17_skl),sK19_skl,X1) ),
inference(resolution,[status(thm)],[f367,f343]) ).
fof(f1825,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| sP0_prd(sK17_skl,sK16_skl,ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f1599,f339]) ).
fof(f1855,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1825,f1141]) ).
fof(f1856,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1855]) ).
fof(f1857,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1042,f373]) ).
fof(f1858,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1857]) ).
fof(f1885,plain,
! [X0,X1,X2] :
( sQ2_spl
| ~ sP0_prd(sK17_skl,X0,X1,sK19_skl,X2) ),
inference(resolution,[status(thm)],[f344,f332]) ).
fof(f2033,definition,
( sQ24_spl
<=> empty_set = singleton(ordered_pair(sK16_skl,sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f2034,plain,
( ~ sQ24_spl
| empty_set = singleton(ordered_pair(sK16_skl,sK17_skl)) ),
inference(component_clause,[status(thm)],[f2033]) ).
fof(f2282,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2034,f205]) ).
fof(f2283,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f2282]) ).
fof(f2517,plain,
( ~ sQ0_spl
| sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl) = sK16_skl ),
inference(resolution,[status(thm)],[f999,f273]) ).
fof(f2518,plain,
( ~ sQ0_spl
| sK17_skl = sK6_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f999,f274]) ).
fof(f2535,plain,
( ~ sQ0_spl
| sP0_prd(sK17_skl,sK5_skl(ordered_pair(sK16_skl,sK17_skl),cartesian_product2(sK18_skl,sK19_skl),sK19_skl,sK18_skl),ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl) ),
inference(backward_demodulation,[status(thm)],[f2518,f718]) ).
fof(f2571,plain,
( ~ sQ0_spl
| sP0_prd(sK17_skl,sK16_skl,ordered_pair(sK16_skl,sK17_skl),sK19_skl,sK18_skl) ),
inference(forward_demodulation,[status(thm)],[f2517,f2535]) ).
fof(f2572,plain,
( ~ sQ0_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f1885]) ).
fof(f2573,plain,
( ~ sQ0_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f2572]) ).
fof(f2574,plain,
( ~ sQ0_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2571,f656]) ).
fof(f2575,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f2574]) ).
fof(f2576,plain,
$false,
inference(sat_refutation,[status(thm)],[f341,f345,f346,f989,f994,f996,f1104,f1399,f1450,f1532,f1856,f1858,f2283,f2573,f2575]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU157+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 05:58:07 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 89.04/11.65 % Refutation found
% 89.04/11.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 89.04/11.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.51/12.52 % Elapsed time: 12.158438 seconds
% 6.51/12.52 % CPU time: 90.618817 seconds
% 6.51/12.52 % Total memory used: 768.220 MB
% 6.51/12.52 % Net memory used: 706.671 MB
%------------------------------------------------------------------------------