%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET018+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:08:53 PM UTC 2026
% Result : Theorem 1.56s 0.64s
% Output : CNFRefutation 1.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 34
% Syntax : Number of formulae : 167 ( 28 unt; 23 def)
% Number of atoms : 408 ( 61 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 414 ( 173 ~; 165 |; 43 &)
% ( 28 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 24 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 183 ( 169 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,X)
=> member(U,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [U,X,Y] :
( member(U,unordered_pair(X,Y))
<=> ( ( U = Y
| U = X )
& member(U,universal_class) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : singleton(X) = unordered_pair(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,V,X,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
<=> ( member(V,Y)
& member(U,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : ~ member(X,null_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] :
( inductive(X)
<=> ( subclass(image(successor_relation,X),X)
& member(null_class,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [X] :
( ! [Y] :
( inductive(Y)
=> subclass(X,Y) )
& inductive(X)
& member(X,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] :
( X != null_class
=> ? [U] :
( disjoint(U,X)
& member(U,X)
& member(U,universal_class) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
! [W,X,Y,Z] :
( ( member(X,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) )
=> X = Z ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
~ ! [W,X,Y,Z] :
( ( member(X,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) )
=> X = Z ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f46,plain,
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,Y)
| ~ member(U,X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f47,plain,
! [X,Y] :
( ( ? [U] :
( ~ member(U,Y)
& member(U,X) )
| subclass(X,Y) )
& ( ! [U] :
( member(U,Y)
| ~ member(U,X) )
| ~ subclass(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
( ! [X,Y] :
( ? [U] :
( ~ member(U,Y)
& member(U,X) )
| subclass(X,Y) )
& ! [X,Y] :
( ! [U] :
( member(U,Y)
| ~ member(U,X) )
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f49,plain,
( ! [X,Y] :
( ( ~ member(sK0_skl(Y,X),Y)
& member(sK0_skl(Y,X),X) )
| subclass(X,Y) )
& ! [X,Y] :
( ! [U] :
( member(U,Y)
| ~ member(U,X) )
| ~ subclass(X,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(U,sK0_skl(Y,X))],[f48]) ).
fof(f50,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f59,plain,
! [U,X,Y] :
( ( ( U != Y
& U != X )
| ~ member(U,universal_class)
| member(U,unordered_pair(X,Y)) )
& ( ( ( U = Y
| U = X )
& member(U,universal_class) )
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
( ! [U,X,Y] :
( ( U != Y
& U != X )
| ~ member(U,universal_class)
| member(U,unordered_pair(X,Y)) )
& ! [U,X,Y] :
( ( ( U = Y
| U = X )
& member(U,universal_class) )
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f62,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f64,plain,
! [X0,X1,X2] :
( X0 != X2
| ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f65,plain,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f66,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f67,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f68,plain,
! [U,V,X,Y] :
( ( ~ member(V,Y)
| ~ member(U,X)
| member(ordered_pair(U,V),cross_product(X,Y)) )
& ( ( member(V,Y)
& member(U,X) )
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f69,plain,
( ! [U,V,X,Y] :
( ~ member(V,Y)
| ~ member(U,X)
| member(ordered_pair(U,V),cross_product(X,Y)) )
& ! [U,V,X,Y] :
( ( member(V,Y)
& member(U,X) )
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1,X2,X3] :
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ member(X1,X3)
| ~ member(X0,X2)
| member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f96,plain,
! [X0] : ~ member(X0,null_class),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f130,plain,
! [X] :
( ( ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X)
| inductive(X) )
& ( ( subclass(image(successor_relation,X),X)
& member(null_class,X) )
| ~ inductive(X) ) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f131,plain,
( ! [X] :
( ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X)
| inductive(X) )
& ! [X] :
( ( subclass(image(successor_relation,X),X)
& member(null_class,X) )
| ~ inductive(X) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0] :
( member(null_class,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f135,plain,
? [X] :
( ! [Y] :
( subclass(X,Y)
| ~ inductive(Y) )
& inductive(X)
& member(X,universal_class) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f136,plain,
( ! [Y] :
( subclass(sK1_skl,Y)
| ~ inductive(Y) )
& inductive(sK1_skl)
& member(sK1_skl,universal_class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl)],[f135]) ).
fof(f138,plain,
inductive(sK1_skl),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f139,plain,
! [X0] :
( subclass(sK1_skl,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f181,plain,
! [X] :
( ? [U] :
( disjoint(U,X)
& member(U,X)
& member(U,universal_class) )
| X = null_class ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f182,plain,
! [X] :
( ( disjoint(sK5_skl(X),X)
& member(sK5_skl(X),X)
& member(sK5_skl(X),universal_class) )
| X = null_class ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(U,sK5_skl(X))],[f181]) ).
fof(f183,plain,
! [X0] :
( member(sK5_skl(X0),universal_class)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0] :
( member(sK5_skl(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f191,plain,
? [W,X,Y,Z] :
( X != Z
& member(X,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f192,plain,
? [X,Z] :
( X != Z
& member(X,universal_class)
& ? [W,Y] : ordered_pair(W,X) = ordered_pair(Y,Z) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
( sK7_skl != sK8_skl
& member(sK7_skl,universal_class)
& ordered_pair(sK9_skl,sK7_skl) = ordered_pair(sK10_skl,sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(X,sK7_skl),skolemize(Z,sK8_skl),skolemize(W,sK9_skl),skolemize(Y,sK10_skl)],[f192]) ).
fof(f194,plain,
ordered_pair(sK9_skl,sK7_skl) = ordered_pair(sK10_skl,sK8_skl),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f195,plain,
member(sK7_skl,universal_class),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f196,plain,
sK7_skl != sK8_skl,
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f199,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f200,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f64]) ).
fof(f203,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ subclass(X0,null_class) ),
inference(resolution,[status(thm)],[f96,f50]) ).
fof(f204,plain,
! [X0] : member(singleton(X0),universal_class),
inference(paramodulation,[status(thm)],[f66,f65]) ).
fof(f205,plain,
~ inductive(null_class),
inference(resolution,[status(thm)],[f132,f96]) ).
fof(f211,plain,
! [X0] :
( ~ inductive(null_class)
| ~ member(X0,sK1_skl) ),
inference(resolution,[status(thm)],[f203,f139]) ).
fof(f214,definition,
! [X0] :
( sQ0_spl
<=> ~ member(X0,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f215,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(X0,sK1_skl) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,definition,
( sQ1_spl
<=> inductive(null_class) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f211,f214,f217]) ).
fof(f221,plain,
( ~ sQ0_spl
| sK1_skl = null_class ),
inference(resolution,[status(thm)],[f215,f184]) ).
fof(f228,plain,
( ~ sQ0_spl
| inductive(null_class) ),
inference(backward_demodulation,[status(thm)],[f221,f138]) ).
fof(f232,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f228,f205]) ).
fof(f233,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f232]) ).
fof(f292,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f66,f62]) ).
fof(f293,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f292]) ).
fof(f296,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,singleton(X0)) ),
inference(paramodulation,[status(thm)],[f66,f199]) ).
fof(f298,plain,
! [X0] :
( singleton(X0) = null_class
| sK5_skl(singleton(X0)) = X0 ),
inference(resolution,[status(thm)],[f293,f184]) ).
fof(f352,plain,
! [X0,X1] :
( ~ member(unordered_pair(X0,singleton(X1)),universal_class)
| member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f67,f200]) ).
fof(f357,plain,
! [X0,X1] : member(ordered_pair(X0,X1),universal_class),
inference(paramodulation,[status(thm)],[f67,f65]) ).
fof(f359,plain,
! [X0,X1] : member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f352,f65]) ).
fof(f362,plain,
! [X0,X1] :
( member(sK10_skl,X0)
| ~ member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f194,f70]) ).
fof(f429,plain,
! [X0,X1] :
( member(sK8_skl,X1)
| ~ member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f194,f71]) ).
fof(f431,plain,
! [X0,X1,X2,X3] :
( member(X2,X3)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f72,f71]) ).
fof(f433,plain,
! [X0,X1] :
( ~ member(sK8_skl,X1)
| ~ member(sK10_skl,X0)
| member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f194,f72]) ).
fof(f435,definition,
! [X0,X1] :
( sQ14_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f436,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f435]) ).
fof(f438,definition,
! [X2,X3] :
( sQ15_spl
<=> ( member(X2,X3)
| ~ member(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f431,f435,f438]) ).
fof(f443,plain,
( ~ sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f357,f436]) ).
fof(f466,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f443]) ).
fof(f472,definition,
( sQ17_spl
<=> member(sK8_skl,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ17_spl
| ~ member(sK8_skl,universal_class) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f503,plain,
! [X0] :
( singleton(X0) = null_class
| member(X0,universal_class)
| singleton(X0) = null_class ),
inference(paramodulation,[status(thm)],[f298,f183]) ).
fof(f506,plain,
! [X0] :
( member(X0,universal_class)
| singleton(X0) = null_class ),
inference(duplicate_literals_removal,[status(thm)],[f503]) ).
fof(f649,plain,
! [X0] :
( ~ member(sK10_skl,X0)
| member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,singleton(sK8_skl)))
| ~ member(sK8_skl,universal_class) ),
inference(resolution,[status(thm)],[f296,f433]) ).
fof(f654,definition,
! [X0] :
( sQ31_spl
<=> ( ~ member(sK10_skl,X0)
| member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,singleton(sK8_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f655,plain,
! [X0] :
( ~ sQ31_spl
| ~ member(sK10_skl,X0)
| member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,singleton(sK8_skl))) ),
inference(component_clause,[status(thm)],[f654]) ).
fof(f657,plain,
( sQ31_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f649,f472,f654]) ).
fof(f658,definition,
( sQ32_spl
<=> member(sK10_skl,null_class) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( ~ sQ32_spl
| member(sK10_skl,null_class) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f662,definition,
( sQ33_spl
<=> member(sK8_skl,null_class) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f663,plain,
( ~ sQ33_spl
| member(sK8_skl,null_class) ),
inference(component_clause,[status(thm)],[f662]) ).
fof(f666,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f659,f96]) ).
fof(f667,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f666]) ).
fof(f705,plain,
! [X0,X1] :
( member(sK10_skl,X0)
| ~ member(sK7_skl,X1)
| ~ member(sK9_skl,X0) ),
inference(resolution,[status(thm)],[f72,f362]) ).
fof(f706,plain,
! [X0,X1] :
( member(sK8_skl,X1)
| ~ member(sK7_skl,X1)
| ~ member(sK9_skl,X0) ),
inference(resolution,[status(thm)],[f72,f429]) ).
fof(f707,definition,
! [X0] :
( sQ37_spl
<=> ( member(sK10_skl,X0)
| ~ member(sK9_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f710,definition,
! [X1] :
( sQ38_spl
<=> ~ member(sK7_skl,X1) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f711,plain,
! [X0] :
( ~ sQ38_spl
| ~ member(sK7_skl,X0) ),
inference(component_clause,[status(thm)],[f710]) ).
fof(f713,plain,
( sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f705,f707,f710]) ).
fof(f714,definition,
! [X0] :
( sQ39_spl
<=> ~ member(sK9_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f715,plain,
! [X0] :
( ~ sQ39_spl
| ~ member(sK9_skl,X0) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,definition,
! [X1] :
( sQ40_spl
<=> ( member(sK8_skl,X1)
| ~ member(sK7_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f718,plain,
! [X0] :
( ~ sQ40_spl
| member(sK8_skl,X0)
| ~ member(sK7_skl,X0) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,plain,
( sQ40_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f706,f714,f717]) ).
fof(f724,plain,
( ~ sQ39_spl
| singleton(sK9_skl) = null_class ),
inference(resolution,[status(thm)],[f715,f506]) ).
fof(f734,plain,
! [X0] :
( ~ sQ39_spl
| ordered_pair(sK9_skl,X0) = unordered_pair(null_class,unordered_pair(sK9_skl,singleton(X0))) ),
inference(paramodulation,[status(thm)],[f724,f67]) ).
fof(f759,plain,
( ~ sQ40_spl
| member(sK8_skl,universal_class) ),
inference(resolution,[status(thm)],[f718,f195]) ).
fof(f764,plain,
( ~ sQ40_spl
| sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f474]) ).
fof(f765,plain,
( ~ sQ40_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f764]) ).
fof(f767,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f663,f96]) ).
fof(f768,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f767]) ).
fof(f835,plain,
! [X0,X1] :
( ~ sQ39_spl
| X0 = unordered_pair(sK9_skl,singleton(X1))
| X0 = null_class
| ~ member(X0,ordered_pair(sK9_skl,X1)) ),
inference(paramodulation,[status(thm)],[f734,f62]) ).
fof(f1039,definition,
( sQ56_spl
<=> member(sK7_skl,universal_class) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( sQ56_spl
| ~ member(sK7_skl,universal_class) ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1055,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1041,f195]) ).
fof(f1056,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f1055]) ).
fof(f1081,plain,
! [X0] :
( ~ sQ31_spl
| member(sK7_skl,singleton(sK8_skl))
| ~ member(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f655,f71]) ).
fof(f1082,definition,
! [X0] :
( sQ60_spl
<=> ~ member(sK10_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1083,plain,
! [X0] :
( ~ sQ60_spl
| ~ member(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f1082]) ).
fof(f1092,definition,
( sQ62_spl
<=> member(sK7_skl,singleton(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1093,plain,
( ~ sQ62_spl
| member(sK7_skl,singleton(sK8_skl)) ),
inference(component_clause,[status(thm)],[f1092]) ).
fof(f1095,plain,
( ~ sQ31_spl
| sQ62_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1081,f1082,f1092,f654]) ).
fof(f1097,plain,
! [X0,X1] :
( ~ sQ60_spl
| ~ member(ordered_pair(sK9_skl,sK7_skl),cross_product(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f362,f1083]) ).
fof(f1171,plain,
( ~ sQ62_spl
| sK7_skl = sK8_skl ),
inference(resolution,[status(thm)],[f1093,f293]) ).
fof(f1172,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1171,f196]) ).
fof(f1173,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f1172]) ).
fof(f1421,plain,
( ~ sQ38_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f195,f711]) ).
fof(f1422,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1421]) ).
fof(f1463,plain,
! [X0,X1] :
( ~ sQ60_spl
| ~ member(sK7_skl,X1)
| ~ member(sK9_skl,X0) ),
inference(resolution,[status(thm)],[f1097,f72]) ).
fof(f1464,plain,
( ~ sQ60_spl
| sQ38_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1463,f714,f710,f1082]) ).
fof(f1690,definition,
( sQ86_spl
<=> member(null_class,null_class) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1691,plain,
( ~ sQ86_spl
| member(null_class,null_class) ),
inference(component_clause,[status(thm)],[f1690]) ).
fof(f1694,plain,
( ~ sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1691,f96]) ).
fof(f1695,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f1694]) ).
fof(f1737,plain,
member(unordered_pair(sK10_skl,singleton(sK8_skl)),ordered_pair(sK9_skl,sK7_skl)),
inference(paramodulation,[status(thm)],[f194,f359]) ).
fof(f1800,plain,
( ~ sQ39_spl
| unordered_pair(sK10_skl,singleton(sK8_skl)) = unordered_pair(sK9_skl,singleton(sK7_skl))
| unordered_pair(sK10_skl,singleton(sK8_skl)) = null_class ),
inference(resolution,[status(thm)],[f1737,f835]) ).
fof(f1801,definition,
( sQ93_spl
<=> unordered_pair(sK10_skl,singleton(sK8_skl)) = null_class ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1802,plain,
( ~ sQ93_spl
| unordered_pair(sK10_skl,singleton(sK8_skl)) = null_class ),
inference(component_clause,[status(thm)],[f1801]) ).
fof(f1804,definition,
( sQ94_spl
<=> unordered_pair(sK10_skl,singleton(sK8_skl)) = unordered_pair(sK9_skl,singleton(sK7_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1805,plain,
( ~ sQ94_spl
| unordered_pair(sK10_skl,singleton(sK8_skl)) = unordered_pair(sK9_skl,singleton(sK7_skl)) ),
inference(component_clause,[status(thm)],[f1804]) ).
fof(f1807,plain,
( ~ sQ39_spl
| sQ94_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f1800,f1801,f1804,f714]) ).
fof(f1815,plain,
( ~ sQ93_spl
| ~ member(singleton(sK8_skl),universal_class)
| member(singleton(sK8_skl),null_class) ),
inference(paramodulation,[status(thm)],[f1802,f200]) ).
fof(f1831,definition,
( sQ95_spl
<=> member(singleton(sK8_skl),null_class) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
( ~ sQ95_spl
| member(singleton(sK8_skl),null_class) ),
inference(component_clause,[status(thm)],[f1831]) ).
fof(f1834,definition,
( sQ96_spl
<=> member(singleton(sK8_skl),universal_class) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( sQ96_spl
| ~ member(singleton(sK8_skl),universal_class) ),
inference(component_clause,[status(thm)],[f1834]) ).
fof(f1837,plain,
( ~ sQ93_spl
| ~ sQ96_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f1815,f1831,f1834,f1801]) ).
fof(f1838,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1832,f96]) ).
fof(f1839,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f1838]) ).
fof(f1840,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1836,f204]) ).
fof(f1841,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f1840]) ).
fof(f1880,plain,
( ~ sQ94_spl
| ~ member(singleton(sK8_skl),universal_class)
| member(singleton(sK8_skl),unordered_pair(sK9_skl,singleton(sK7_skl))) ),
inference(paramodulation,[status(thm)],[f1805,f200]) ).
fof(f1891,definition,
( sQ98_spl
<=> member(singleton(sK8_skl),unordered_pair(sK9_skl,singleton(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1892,plain,
( ~ sQ98_spl
| member(singleton(sK8_skl),unordered_pair(sK9_skl,singleton(sK7_skl))) ),
inference(component_clause,[status(thm)],[f1891]) ).
fof(f1894,plain,
( ~ sQ94_spl
| ~ sQ96_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1880,f1891,f1834,f1804]) ).
fof(f1897,plain,
( ~ sQ98_spl
| singleton(sK8_skl) = singleton(sK7_skl)
| singleton(sK8_skl) = sK9_skl ),
inference(resolution,[status(thm)],[f1892,f62]) ).
fof(f1898,definition,
( sQ99_spl
<=> singleton(sK8_skl) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1899,plain,
( ~ sQ99_spl
| singleton(sK8_skl) = sK9_skl ),
inference(component_clause,[status(thm)],[f1898]) ).
fof(f1901,definition,
( sQ100_spl
<=> singleton(sK8_skl) = singleton(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1902,plain,
( ~ sQ100_spl
| singleton(sK8_skl) = singleton(sK7_skl) ),
inference(component_clause,[status(thm)],[f1901]) ).
fof(f1904,plain,
( ~ sQ98_spl
| sQ100_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f1897,f1898,f1901,f1891]) ).
fof(f1905,plain,
( ~ sQ98_spl
| ~ sQ99_spl
| member(sK9_skl,unordered_pair(sK9_skl,singleton(sK7_skl))) ),
inference(backward_demodulation,[status(thm)],[f1899,f1892]) ).
fof(f1910,plain,
( ~ sQ98_spl
| ~ sQ99_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1905,f715]) ).
fof(f1911,plain,
( ~ sQ98_spl
| ~ sQ99_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f1910]) ).
fof(f1929,plain,
( ~ sQ100_spl
| ~ member(sK7_skl,universal_class)
| member(sK7_skl,singleton(sK8_skl)) ),
inference(paramodulation,[status(thm)],[f1902,f296]) ).
fof(f1964,plain,
( ~ sQ100_spl
| ~ sQ56_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1929,f1092,f1039,f1901]) ).
fof(f1974,plain,
$false,
inference(sat_refutation,[status(thm)],[f220,f233,f441,f466,f657,f667,f713,f720,f765,f768,f1056,f1095,f1173,f1422,f1464,f1695,f1807,f1837,f1839,f1841,f1894,f1904,f1911,f1964]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET018+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 04:43:04 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 1.56/0.64 % Refutation found
% 1.56/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.56/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.56/0.67 % Elapsed time: 0.307740 seconds
% 1.56/0.67 % CPU time: 2.053639 seconds
% 1.56/0.67 % Total memory used: 138.689 MB
% 1.56/0.67 % Net memory used: 134.996 MB
%------------------------------------------------------------------------------