%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU156+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 : n002.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 0.13s 0.46s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 33
% Syntax : Number of formulae : 172 ( 35 unt; 16 def)
% Number of atoms : 451 ( 193 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 477 ( 198 ~; 218 |; 35 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 17 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 176 ( 166 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
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(f10,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(f16,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_intersection2(A,B) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B] :
( ~ empty(A)
=> ~ empty(set_union2(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,conjecture,
! [A,B,C,D] :
( ordered_pair(A,B) = ordered_pair(C,D)
=> ( B = D
& A = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,negated_conjecture,
~ ! [A,B,C,D] :
( ordered_pair(A,B) = ordered_pair(C,D)
=> ( B = D
& A = C ) ),
inference(negated_conjecture,[status(cth)],[f61]) ).
fof(f72,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,lemma,
! [A] : unordered_pair(A,A) = singleton(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f91,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f92,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f98,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)],[f7]) ).
fof(f99,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)],[f98]) ).
fof(f100,plain,
( ! [A,B] :
( ( ( sK0_skl(B,A) = A
| in(sK0_skl(B,A),B) )
& ( sK0_skl(B,A) != A
| ~ in(sK0_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,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f105,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f106,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f105]) ).
fof(f107,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))],[f106]) ).
fof(f109,plain,
! [X0] :
( in(sK1_skl(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f117,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)],[f10]) ).
fof(f118,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)],[f117]) ).
fof(f119,plain,
( ! [A,B,C] :
( ( ( sK3_skl(C,B,A) = B
| sK3_skl(C,B,A) = A
| in(sK3_skl(C,B,A),C) )
& ( ( sK3_skl(C,B,A) != B
& sK3_skl(C,B,A) != A )
| ~ in(sK3_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,[sK3_skl]),skolemize(D,sK3_skl(C,B,A))],[f118]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| X3 = X1
| ~ in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( X3 != X1
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,plain,
! [X0,X1,X2,X3] :
( X3 != X2
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f169,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f170,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)],[f17]) ).
fof(f171,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)],[f170]) ).
fof(f173,plain,
! [X0,X1] :
( set_intersection2(X0,X1) != empty_set
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f179,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f181,plain,
! [A,B] :
( ~ empty(set_union2(A,B))
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f182,plain,
! [A] :
( ! [B] : ~ empty(set_union2(A,B))
| empty(A) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ~ empty(set_union2(X0,X1))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f193,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f204,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)],[f40]) ).
fof(f205,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)],[f204]) ).
fof(f206,plain,
! [X0,X1] :
( subset(X0,X1)
| set_difference(X0,X1) != empty_set ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f234,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f244,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f254,plain,
? [A,B,C,D] :
( ( B != D
| A != C )
& ordered_pair(A,B) = ordered_pair(C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f255,plain,
( ( sK15_skl != sK17_skl
| sK14_skl != sK16_skl )
& ordered_pair(sK14_skl,sK15_skl) = ordered_pair(sK16_skl,sK17_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(A,sK14_skl),skolemize(B,sK15_skl),skolemize(C,sK16_skl),skolemize(D,sK17_skl)],[f254]) ).
fof(f256,plain,
ordered_pair(sK14_skl,sK15_skl) = ordered_pair(sK16_skl,sK17_skl),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f257,plain,
( sK15_skl != sK17_skl
| sK14_skl != sK16_skl ),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f277,plain,
! [X0] : set_difference(empty_set,X0) = empty_set,
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f288,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f312,definition,
( sQ0_spl
<=> sK14_skl = sK16_skl ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( ~ sQ0_spl
| sK14_skl = sK16_skl ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f314,plain,
( sQ0_spl
| sK14_skl != sK16_skl ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f315,definition,
( sQ1_spl
<=> sK15_skl = sK17_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f317,plain,
( sQ1_spl
| sK15_skl != sK17_skl ),
inference(component_clause,[status(thm)],[f315]) ).
fof(f318,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f257,f312,f315]) ).
fof(f321,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f101]) ).
fof(f326,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ in(X0,unordered_pair(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f120]) ).
fof(f327,plain,
! [X0,X1] : in(X0,unordered_pair(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f121]) ).
fof(f328,plain,
! [X0,X1] : in(X0,unordered_pair(X1,X0)),
inference(destructive_equality_resolution,[status(thm)],[f122]) ).
fof(f409,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,X1)),
inference(paramodulation,[status(thm)],[f169,f90]) ).
fof(f473,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X1,X0)),
inference(paramodulation,[status(thm)],[f90,f409]) ).
fof(f612,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f91,f234]) ).
fof(f771,plain,
! [X0] :
( sK1_skl(singleton(X0)) = X0
| singleton(X0) = empty_set ),
inference(resolution,[status(thm)],[f109,f321]) ).
fof(f774,plain,
! [X0] : sK1_skl(singleton(X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f771,f193]) ).
fof(f913,plain,
! [X0,X1] : in(singleton(X0),ordered_pair(X0,X1)),
inference(paramodulation,[status(thm)],[f473,f327]) ).
fof(f926,plain,
! [X0,X1] : in(unordered_pair(X0,X1),ordered_pair(X0,X1)),
inference(paramodulation,[status(thm)],[f169,f327]) ).
fof(f955,plain,
! [X0] : set_intersection2(empty_set,X0) = empty_set,
inference(paramodulation,[status(thm)],[f92,f244]) ).
fof(f986,plain,
! [X0,X1,X2] :
( X0 = singleton(X1)
| X0 = unordered_pair(X1,X2)
| ~ in(X0,ordered_pair(X1,X2)) ),
inference(paramodulation,[status(thm)],[f169,f326]) ).
fof(f1022,plain,
in(singleton(sK16_skl),ordered_pair(sK14_skl,sK15_skl)),
inference(paramodulation,[status(thm)],[f256,f913]) ).
fof(f1048,plain,
in(unordered_pair(sK16_skl,sK17_skl),ordered_pair(sK14_skl,sK15_skl)),
inference(paramodulation,[status(thm)],[f256,f926]) ).
fof(f1058,plain,
! [X0] :
( X0 = singleton(sK16_skl)
| X0 = unordered_pair(sK16_skl,sK17_skl)
| ~ in(X0,ordered_pair(sK14_skl,sK15_skl)) ),
inference(paramodulation,[status(thm)],[f256,f986]) ).
fof(f1145,plain,
( singleton(sK16_skl) = singleton(sK14_skl)
| singleton(sK16_skl) = unordered_pair(sK14_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f1022,f986]) ).
fof(f1147,definition,
( sQ4_spl
<=> singleton(sK16_skl) = unordered_pair(sK14_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1148,plain,
( ~ sQ4_spl
| singleton(sK16_skl) = unordered_pair(sK14_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f1147]) ).
fof(f1149,plain,
( sQ4_spl
| singleton(sK16_skl) != unordered_pair(sK14_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f1147]) ).
fof(f1150,definition,
( sQ5_spl
<=> singleton(sK16_skl) = singleton(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1151,plain,
( ~ sQ5_spl
| singleton(sK16_skl) = singleton(sK14_skl) ),
inference(component_clause,[status(thm)],[f1150]) ).
fof(f1153,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1145,f1147,f1150]) ).
fof(f1157,plain,
( ~ sQ4_spl
| in(sK15_skl,singleton(sK16_skl)) ),
inference(paramodulation,[status(thm)],[f1148,f328]) ).
fof(f1158,plain,
( ~ sQ4_spl
| in(sK14_skl,singleton(sK16_skl)) ),
inference(paramodulation,[status(thm)],[f1148,f327]) ).
fof(f1178,plain,
( unordered_pair(sK16_skl,sK17_skl) = singleton(sK14_skl)
| unordered_pair(sK16_skl,sK17_skl) = unordered_pair(sK14_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f1048,f986]) ).
fof(f1180,definition,
( sQ6_spl
<=> unordered_pair(sK16_skl,sK17_skl) = unordered_pair(sK14_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
( ~ sQ6_spl
| unordered_pair(sK16_skl,sK17_skl) = unordered_pair(sK14_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f1180]) ).
fof(f1183,definition,
( sQ7_spl
<=> unordered_pair(sK16_skl,sK17_skl) = singleton(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1184,plain,
( ~ sQ7_spl
| unordered_pair(sK16_skl,sK17_skl) = singleton(sK14_skl) ),
inference(component_clause,[status(thm)],[f1183]) ).
fof(f1186,plain,
( sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1178,f1180,f1183]) ).
fof(f1187,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| unordered_pair(sK16_skl,sK17_skl) = singleton(sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f1148,f1181]) ).
fof(f1188,plain,
( ~ sQ4_spl
| sK15_skl = sK16_skl ),
inference(resolution,[status(thm)],[f1157,f321]) ).
fof(f1206,plain,
( sQ0_spl
| ~ sQ4_spl
| sK14_skl != sK15_skl ),
inference(backward_demodulation,[status(thm)],[f1188,f314]) ).
fof(f1354,plain,
( ~ sQ4_spl
| in(sK14_skl,singleton(sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f1188,f1158]) ).
fof(f1355,plain,
( ~ sQ4_spl
| sK14_skl = sK15_skl ),
inference(resolution,[status(thm)],[f1354,f321]) ).
fof(f1357,plain,
( ~ sQ4_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1355,f1206]) ).
fof(f1358,plain,
( ~ sQ4_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1357]) ).
fof(f1362,plain,
( ~ sQ0_spl
| ordered_pair(sK14_skl,sK15_skl) = ordered_pair(sK14_skl,sK17_skl) ),
inference(forward_demodulation,[status(thm)],[f313,f256]) ).
fof(f1365,plain,
( ~ sQ0_spl
| in(unordered_pair(sK14_skl,sK17_skl),ordered_pair(sK14_skl,sK15_skl)) ),
inference(paramodulation,[status(thm)],[f1362,f926]) ).
fof(f1503,plain,
! [X0] :
( ~ sQ0_spl
| X0 = singleton(sK16_skl)
| X0 = unordered_pair(sK14_skl,sK17_skl)
| ~ in(X0,ordered_pair(sK14_skl,sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f313,f1058]) ).
fof(f1504,plain,
! [X0] :
( ~ sQ0_spl
| X0 = singleton(sK14_skl)
| X0 = unordered_pair(sK14_skl,sK17_skl)
| ~ in(X0,ordered_pair(sK14_skl,sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f313,f1503]) ).
fof(f1510,plain,
( ~ sQ0_spl
| unordered_pair(sK14_skl,sK15_skl) = singleton(sK14_skl)
| unordered_pair(sK14_skl,sK15_skl) = unordered_pair(sK14_skl,sK17_skl) ),
inference(resolution,[status(thm)],[f1504,f926]) ).
fof(f1516,definition,
( sQ8_spl
<=> unordered_pair(sK14_skl,sK15_skl) = unordered_pair(sK14_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1517,plain,
( ~ sQ8_spl
| unordered_pair(sK14_skl,sK15_skl) = unordered_pair(sK14_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f1516]) ).
fof(f1519,definition,
( sQ9_spl
<=> unordered_pair(sK14_skl,sK15_skl) = singleton(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1520,plain,
( ~ sQ9_spl
| unordered_pair(sK14_skl,sK15_skl) = singleton(sK14_skl) ),
inference(component_clause,[status(thm)],[f1519]) ).
fof(f1522,plain,
( ~ sQ0_spl
| sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1510,f1516,f1519,f312]) ).
fof(f1523,definition,
( sQ10_spl
<=> singleton(sK14_skl) = unordered_pair(sK14_skl,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1524,plain,
( ~ sQ10_spl
| singleton(sK14_skl) = unordered_pair(sK14_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f1523]) ).
fof(f1525,plain,
( sQ10_spl
| singleton(sK14_skl) != unordered_pair(sK14_skl,sK17_skl) ),
inference(component_clause,[status(thm)],[f1523]) ).
fof(f1544,plain,
( ~ sQ5_spl
| sK1_skl(singleton(sK14_skl)) = sK16_skl ),
inference(paramodulation,[status(thm)],[f1151,f774]) ).
fof(f1559,plain,
( ~ sQ5_spl
| sK14_skl = sK16_skl ),
inference(forward_demodulation,[status(thm)],[f774,f1544]) ).
fof(f1560,plain,
( ~ sQ5_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1559,f314]) ).
fof(f1561,plain,
( ~ sQ5_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1560]) ).
fof(f1582,plain,
( sQ1_spl
| ~ sQ4_spl
| ~ sQ0_spl
| sK14_skl != sK17_skl ),
inference(backward_demodulation,[status(thm)],[f1583,f317]) ).
fof(f1583,plain,
( ~ sQ4_spl
| ~ sQ0_spl
| sK15_skl = sK14_skl ),
inference(forward_demodulation,[status(thm)],[f313,f1188]) ).
fof(f1612,plain,
( sQ4_spl
| ~ sQ0_spl
| singleton(sK14_skl) != unordered_pair(sK14_skl,sK15_skl) ),
inference(forward_demodulation,[status(thm)],[f313,f1149]) ).
fof(f1810,plain,
( ~ sQ10_spl
| in(sK17_skl,singleton(sK14_skl)) ),
inference(paramodulation,[status(thm)],[f1524,f328]) ).
fof(f1860,plain,
( ~ sQ10_spl
| sK17_skl = sK14_skl ),
inference(resolution,[status(thm)],[f1810,f321]) ).
fof(f1866,plain,
( sQ1_spl
| ~ sQ10_spl
| sK15_skl != sK14_skl ),
inference(backward_demodulation,[status(thm)],[f1860,f317]) ).
fof(f1962,plain,
( ~ sQ7_spl
| ~ sQ0_spl
| unordered_pair(sK14_skl,sK17_skl) = singleton(sK14_skl) ),
inference(forward_demodulation,[status(thm)],[f313,f1184]) ).
fof(f2223,plain,
( ~ sQ7_spl
| ~ sQ0_spl
| in(sK17_skl,singleton(sK14_skl)) ),
inference(paramodulation,[status(thm)],[f1962,f328]) ).
fof(f2331,plain,
( ~ sQ7_spl
| ~ sQ0_spl
| sK17_skl = sK14_skl ),
inference(resolution,[status(thm)],[f2223,f321]) ).
fof(f2508,plain,
! [X0] :
( ~ empty(X0)
| empty(empty_set) ),
inference(paramodulation,[status(thm)],[f612,f183]) ).
fof(f2513,definition,
( sQ15_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f2516,definition,
! [X0] :
( sQ16_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f2517,plain,
! [X0] :
( ~ sQ16_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f2516]) ).
fof(f2519,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2508,f2513,f2516]) ).
fof(f2520,plain,
( ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f179,f2517]) ).
fof(f2521,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f2520]) ).
fof(f2538,plain,
( sQ10_spl
| ~ sQ7_spl
| ~ sQ0_spl
| singleton(sK14_skl) != unordered_pair(sK14_skl,sK14_skl) ),
inference(forward_demodulation,[status(thm)],[f2331,f1525]) ).
fof(f2539,plain,
( sQ10_spl
| ~ sQ7_spl
| ~ sQ0_spl
| singleton(sK14_skl) != singleton(sK14_skl) ),
inference(forward_demodulation,[status(thm)],[f288,f2538]) ).
fof(f2540,plain,
( sQ10_spl
| ~ sQ7_spl
| ~ sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2539]) ).
fof(f2541,plain,
( sQ10_spl
| ~ sQ7_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f2540]) ).
fof(f2571,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| ~ sQ0_spl
| unordered_pair(sK14_skl,sK17_skl) = singleton(sK16_skl) ),
inference(forward_demodulation,[status(thm)],[f313,f1187]) ).
fof(f2572,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| ~ sQ0_spl
| unordered_pair(sK14_skl,sK17_skl) = singleton(sK14_skl) ),
inference(forward_demodulation,[status(thm)],[f313,f2571]) ).
fof(f3066,plain,
! [X0] :
( empty_set != empty_set
| disjoint(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f955,f173]) ).
fof(f3067,plain,
! [X0] :
( empty_set != empty_set
| disjoint(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f244,f173]) ).
fof(f3071,definition,
! [X0] :
( sQ19_spl
<=> disjoint(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f3074,definition,
( sQ20_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f3076,plain,
( sQ20_spl
| empty_set != empty_set ),
inference(component_clause,[status(thm)],[f3074]) ).
fof(f3077,plain,
( ~ sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f3066,f3071,f3074]) ).
fof(f3078,definition,
! [X0] :
( sQ21_spl
<=> disjoint(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f3081,plain,
( ~ sQ20_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f3067,f3078,f3074]) ).
fof(f3083,plain,
( sQ20_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3076]) ).
fof(f3084,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f3083]) ).
fof(f3099,plain,
( ~ sQ0_spl
| unordered_pair(sK14_skl,sK17_skl) = singleton(sK14_skl)
| unordered_pair(sK14_skl,sK17_skl) = unordered_pair(sK14_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f1365,f986]) ).
fof(f3106,plain,
( ~ sQ0_spl
| sQ10_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f3099,f1516,f1523,f312]) ).
fof(f3124,plain,
( ~ sQ8_spl
| in(sK17_skl,unordered_pair(sK14_skl,sK15_skl)) ),
inference(paramodulation,[status(thm)],[f1517,f328]) ).
fof(f3347,plain,
( ~ sQ8_spl
| sK17_skl = sK15_skl
| sK17_skl = sK14_skl ),
inference(resolution,[status(thm)],[f3124,f326]) ).
fof(f3350,definition,
( sQ23_spl
<=> sK17_skl = sK14_skl ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f3351,plain,
( ~ sQ23_spl
| sK17_skl = sK14_skl ),
inference(component_clause,[status(thm)],[f3350]) ).
fof(f3353,plain,
( ~ sQ8_spl
| sQ1_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f3347,f3350,f315,f1516]) ).
fof(f3358,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| unordered_pair(sK14_skl,sK15_skl) = unordered_pair(sK14_skl,sK14_skl) ),
inference(backward_demodulation,[status(thm)],[f3351,f1517]) ).
fof(f3361,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| unordered_pair(sK14_skl,sK15_skl) = singleton(sK14_skl) ),
inference(forward_demodulation,[status(thm)],[f288,f3358]) ).
fof(f3362,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| sQ4_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3361,f1612]) ).
fof(f3363,plain,
( ~ sQ8_spl
| ~ sQ23_spl
| sQ4_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f3362]) ).
fof(f3369,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| ~ sQ0_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f2572,f1523,f312,f1147,f1180]) ).
fof(f3416,plain,
( sQ1_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ23_spl
| sK14_skl != sK14_skl ),
inference(forward_demodulation,[status(thm)],[f3351,f1582]) ).
fof(f3417,plain,
( sQ1_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ23_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3416]) ).
fof(f3418,plain,
( sQ1_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f3417]) ).
fof(f3419,plain,
( ~ sQ10_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f1860,f3350,f1523]) ).
fof(f3528,plain,
! [X0] :
( subset(empty_set,X0)
| empty_set != empty_set ),
inference(paramodulation,[status(thm)],[f277,f206]) ).
fof(f3530,definition,
! [X0] :
( sQ24_spl
<=> subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f3533,plain,
( sQ24_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f3528,f3074,f3530]) ).
fof(f3551,plain,
( ~ sQ9_spl
| in(sK15_skl,singleton(sK14_skl)) ),
inference(paramodulation,[status(thm)],[f1520,f328]) ).
fof(f3624,plain,
( ~ sQ9_spl
| sK15_skl = sK14_skl ),
inference(resolution,[status(thm)],[f3551,f321]) ).
fof(f3627,plain,
( ~ sQ9_spl
| sQ1_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3624,f1866]) ).
fof(f3628,plain,
( ~ sQ9_spl
| sQ1_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f3627]) ).
fof(f3629,plain,
$false,
inference(sat_refutation,[status(thm)],[f318,f1153,f1186,f1358,f1522,f1561,f2519,f2521,f2541,f3077,f3081,f3084,f3106,f3353,f3363,f3369,f3418,f3419,f3533,f3628]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU156+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 : n002.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:56:17 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.49 % Elapsed time: 0.123288 seconds
% 0.13/0.49 % CPU time: 0.658065 seconds
% 0.13/0.49 % Total memory used: 126.792 MB
% 0.13/0.49 % Net memory used: 126.181 MB
%------------------------------------------------------------------------------