%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET810+4 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:10:40 PM UTC 2026
% Result : Theorem 27.75s 3.96s
% Output : CNFRefutation 27.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 21
% Syntax : Number of formulae : 112 ( 19 unt; 12 def)
% Number of atoms : 418 ( 0 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 493 ( 187 ~; 173 |; 99 &)
% ( 25 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 12 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-3 aty)
% Number of variables : 240 ( 210 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(Y,A)
=> member(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( member(A,on)
<=> ( ! [X] :
( member(X,A)
=> subset(X,A) )
& strict_well_order(member_predicate,A)
& set(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [R,E] :
( strict_well_order(R,E)
<=> ( ! [A] :
( ( ? [X] : member(X,A)
& subset(A,E) )
=> ? [Y] : least(Y,R,A) )
& strict_order(R,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Y] :
( apply(member_predicate,X,Y)
<=> member(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ~ ( apply(R,Y,X)
& apply(R,X,Y) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,conjecture,
! [A,B] :
( ( member(B,on)
& member(A,on) )
=> ~ ( member(B,A)
& member(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
~ ! [A,B] :
( ( member(B,on)
& member(A,on) )
=> ~ ( member(B,A)
& member(A,B) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,plain,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f23,plain,
! [A,B] :
( ( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
( ! [A,B] :
( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f25,plain,
( ! [A,B] :
( ( ~ member(sK0_skl(B,A),B)
& member(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(B,A))],[f24]) ).
fof(f26,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f48,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f63,plain,
! [X,A] :
( ( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f64,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ( member(X,sK1_skl(A,X))
& member(sK1_skl(A,X),A) )
| ~ member(X,sum(A)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(A,X))],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( member(sK1_skl(X1,X0),X1)
| ~ member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(X,Y)
| ~ member(Y,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f70,plain,
! [X,A] :
( ( ? [Y] :
( ~ member(X,Y)
& member(Y,A) )
| member(X,product(A)) )
& ( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(NNF_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
( ! [X,A] :
( ? [Y] :
( ~ member(X,Y)
& member(Y,A) )
| member(X,product(A)) )
& ! [X,A] :
( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f72,plain,
( ! [X,A] :
( ( ~ member(X,sK2_skl(A,X))
& member(sK2_skl(A,X),A) )
| member(X,product(A)) )
& ! [X,A] :
( ! [Y] :
( member(X,Y)
| ~ member(Y,A) )
| ~ member(X,product(A)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(A,X))],[f71]) ).
fof(f74,plain,
! [X0,X1] :
( member(sK2_skl(X1,X0),X1)
| member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f76,plain,
! [A] :
( member(A,on)
<=> ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f77,plain,
! [A] :
( ( ? [X] :
( ~ subset(X,A)
& member(X,A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
( ! [A] :
( ? [X] :
( ~ subset(X,A)
& member(X,A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ! [A] :
( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
( ! [A] :
( ( ~ subset(sK3_skl(A),A)
& member(sK3_skl(A),A) )
| ~ strict_well_order(member_predicate,A)
| ~ set(A)
| member(A,on) )
& ! [A] :
( ( ! [X] :
( subset(X,A)
| ~ member(X,A) )
& strict_well_order(member_predicate,A)
& set(A) )
| ~ member(A,on) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(A))],[f78]) ).
fof(f81,plain,
! [X0] :
( strict_well_order(member_predicate,X0)
| ~ member(X0,on) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ member(X1,X0)
| ~ member(X0,on) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f85,plain,
! [R,E] :
( strict_well_order(R,E)
<=> ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f86,plain,
! [R,E] :
( ( ? [A] :
( ! [Y] : ~ least(Y,R,A)
& ? [X] : member(X,A)
& subset(A,E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ( ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
( ! [R,E] :
( ? [A] :
( ! [Y] : ~ least(Y,R,A)
& ? [X] : member(X,A)
& subset(A,E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ! [R,E] :
( ( ! [A] :
( ? [Y] : least(Y,R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
( ! [R,E] :
( ( ! [Y] : ~ least(Y,R,sK5_skl(E,R))
& member(sK6_skl(E,R),sK5_skl(E,R))
& subset(sK5_skl(E,R),E) )
| ~ strict_order(R,E)
| strict_well_order(R,E) )
& ! [R,E] :
( ( ! [A] :
( least(sK4_skl(A,E,R),R,A)
| ! [X] : ~ member(X,A)
| ~ subset(A,E) )
& strict_order(R,E) )
| ~ strict_well_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(Y,sK4_skl(A,E,R)),skolemize(A,sK5_skl(E,R)),skolemize(X,sK6_skl(E,R))],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( strict_order(X0,X1)
| ~ strict_well_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f103,plain,
! [X,Y] :
( ( ~ member(X,Y)
| apply(member_predicate,X,Y) )
& ( member(X,Y)
| ~ apply(member_predicate,X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f104,plain,
( ! [X,Y] :
( ~ member(X,Y)
| apply(member_predicate,X,Y) )
& ! [X,Y] :
( member(X,Y)
| ~ apply(member_predicate,X,Y) ) ),
inference(miniscoping,[status(thm)],[f103]) ).
fof(f106,plain,
! [X0,X1] :
( ~ member(X0,X1)
| apply(member_predicate,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f107,plain,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] :
( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f108,definition,
! [R,E,X,Y] :
( sP0_prd(Y,X,E,R)
<=> ( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f109,plain,
! [R,E] :
( strict_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) ) ),
inference(formula_renaming,[status(thm)],[f107,f108]) ).
fof(f110,plain,
! [R,E] :
( ( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X,Y] : ~ sP0_prd(Y,X,E,R)
| strict_order(R,E) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [R,E] :
( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X,Y] : ~ sP0_prd(Y,X,E,R)
| strict_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f112,plain,
( ! [R,E] :
( ( ~ apply(R,sK10_skl(E,R),sK12_skl(E,R))
& apply(R,sK11_skl(E,R),sK12_skl(E,R))
& apply(R,sK10_skl(E,R),sK11_skl(E,R))
& member(sK12_skl(E,R),E)
& member(sK11_skl(E,R),E)
& member(sK10_skl(E,R),E) )
| ~ sP0_prd(sK9_skl(E,R),sK8_skl(E,R),E,R)
| strict_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] : sP0_prd(Y,X,E,R) )
| ~ strict_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(X,sK8_skl(E,R)),skolemize(Y,sK9_skl(E,R)),skolemize(X,sK10_skl(E,R)),skolemize(Y,sK11_skl(E,R)),skolemize(Z,sK12_skl(E,R))],[f111]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X2,X3,X1,X0)
| ~ strict_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f132,plain,
? [A,B] :
( member(B,A)
& member(A,B)
& member(B,on)
& member(A,on) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f133,plain,
( member(sK14_skl,sK13_skl)
& member(sK13_skl,sK14_skl)
& member(sK14_skl,on)
& member(sK13_skl,on) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f132]) ).
fof(f134,plain,
member(sK13_skl,on),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
member(sK14_skl,on),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
member(sK13_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
member(sK14_skl,sK13_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f138,plain,
! [R,E,X,Y] :
( ( ( apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| sP0_prd(Y,X,E,R) )
& ( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E)
| ~ sP0_prd(Y,X,E,R) ) ),
inference(NNF_transformation,[status(thm)],[f108]) ).
fof(f139,plain,
( ! [R,E,X,Y] :
( ( apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| sP0_prd(Y,X,E,R) )
& ! [R,E,X,Y] :
( ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E)
| ~ sP0_prd(Y,X,E,R) ) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0,X1,X2,X3] :
( ~ apply(X3,X0,X1)
| ~ apply(X3,X1,X0)
| ~ member(X0,X2)
| ~ member(X1,X2)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f762,plain,
! [X0] : ~ member(X0,sum(empty_set)),
inference(resolution,[status(thm)],[f66,f48]) ).
fof(f849,plain,
! [X0] : subset(sum(empty_set),X0),
inference(resolution,[status(thm)],[f762,f27]) ).
fof(f2366,plain,
! [X0,X1,X2,X3] :
( ~ strict_order(X3,X1)
| ~ apply(X3,X2,X0)
| ~ apply(X3,X0,X2)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f140,f113]) ).
fof(f7123,plain,
! [X0,X1] :
( ~ strict_order(X1,sK13_skl)
| ~ apply(X1,X0,sK14_skl)
| ~ apply(X1,sK14_skl,X0)
| ~ member(X0,sK13_skl) ),
inference(resolution,[status(thm)],[f2366,f137]) ).
fof(f7364,definition,
( sQ177_spl
<=> member(sK14_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f7366,plain,
( sQ177_spl
| ~ member(sK14_skl,sK14_skl) ),
inference(component_clause,[status(thm)],[f7364]) ).
fof(f7393,plain,
! [X0] :
( sQ177_spl
| ~ member(sK14_skl,X0)
| ~ subset(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f7366,f26]) ).
fof(f7433,definition,
( sQ183_spl
<=> member(sK14_skl,on) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f7435,plain,
( sQ183_spl
| ~ member(sK14_skl,on) ),
inference(component_clause,[status(thm)],[f7433]) ).
fof(f7458,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7435,f135]) ).
fof(f7459,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f7458]) ).
fof(f7465,definition,
( sQ189_spl
<=> strict_order(member_predicate,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f7467,plain,
( sQ189_spl
| ~ strict_order(member_predicate,sK13_skl) ),
inference(component_clause,[status(thm)],[f7465]) ).
fof(f7475,plain,
( sQ189_spl
| ~ strict_well_order(member_predicate,sK13_skl) ),
inference(resolution,[status(thm)],[f7467,f89]) ).
fof(f7878,plain,
( ~ member(sK14_skl,sK14_skl)
| ~ strict_order(member_predicate,sK13_skl)
| ~ member(sK14_skl,sK13_skl) ),
inference(resolution,[status(thm)],[f7123,f106]) ).
fof(f7891,definition,
( sQ207_spl
<=> member(sK14_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f7893,plain,
( sQ207_spl
| ~ member(sK14_skl,sK13_skl) ),
inference(component_clause,[status(thm)],[f7891]) ).
fof(f7894,plain,
( ~ sQ177_spl
| ~ sQ189_spl
| ~ sQ207_spl ),
inference(split_clause,[status(thm)],[f7878,f7891,f7465,f7364]) ).
fof(f7916,plain,
( sQ207_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7893,f137]) ).
fof(f7917,plain,
sQ207_spl,
inference(contradiction_clause,[status(thm)],[f7916]) ).
fof(f7963,plain,
( sQ189_spl
| ~ member(sK13_skl,on) ),
inference(resolution,[status(thm)],[f81,f7475]) ).
fof(f7965,plain,
( sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7963,f134]) ).
fof(f7966,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f7965]) ).
fof(f8367,definition,
( sQ230_spl
<=> member(sK13_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f8369,plain,
( sQ230_spl
| ~ member(sK13_skl,sK14_skl) ),
inference(component_clause,[status(thm)],[f8367]) ).
fof(f8392,plain,
( sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8369,f136]) ).
fof(f8393,plain,
sQ230_spl,
inference(contradiction_clause,[status(thm)],[f8392]) ).
fof(f13464,definition,
! [X0] :
( sQ280_spl
<=> ~ member(X0,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f13465,plain,
! [X0] :
( ~ sQ280_spl
| ~ member(X0,sK13_skl) ),
inference(component_clause,[status(thm)],[f13464]) ).
fof(f13472,plain,
( ~ sQ280_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f137,f13465]) ).
fof(f13510,plain,
~ sQ280_spl,
inference(contradiction_clause,[status(thm)],[f13472]) ).
fof(f15744,definition,
( sQ297_spl
<=> subset(sum(empty_set),sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f15746,plain,
( sQ297_spl
| ~ subset(sum(empty_set),sK13_skl) ),
inference(component_clause,[status(thm)],[f15744]) ).
fof(f15751,plain,
( sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15746,f849]) ).
fof(f15752,plain,
sQ297_spl,
inference(contradiction_clause,[status(thm)],[f15751]) ).
fof(f15756,definition,
( sQ299_spl
<=> subset(sum(empty_set),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f15758,plain,
( sQ299_spl
| ~ subset(sum(empty_set),sK14_skl) ),
inference(component_clause,[status(thm)],[f15756]) ).
fof(f15763,plain,
( sQ299_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15758,f849]) ).
fof(f15764,plain,
sQ299_spl,
inference(contradiction_clause,[status(thm)],[f15763]) ).
fof(f15805,definition,
( sQ301_spl
<=> subset(sum(empty_set),on) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f15807,plain,
( sQ301_spl
| ~ subset(sum(empty_set),on) ),
inference(component_clause,[status(thm)],[f15805]) ).
fof(f15809,plain,
( sQ301_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15807,f849]) ).
fof(f15810,plain,
sQ301_spl,
inference(contradiction_clause,[status(thm)],[f15809]) ).
fof(f16591,definition,
! [X0] :
( sQ308_spl
<=> ~ member(X0,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f16592,plain,
! [X0] :
( ~ sQ308_spl
| ~ member(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f16591]) ).
fof(f16625,definition,
! [X0,X1] :
( sQ316_spl
<=> ~ member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f16626,plain,
! [X0,X1] :
( ~ sQ316_spl
| ~ member(X0,X1) ),
inference(component_clause,[status(thm)],[f16625]) ).
fof(f16657,plain,
( ~ sQ308_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f136,f16592]) ).
fof(f16698,plain,
~ sQ308_spl,
inference(contradiction_clause,[status(thm)],[f16657]) ).
fof(f16822,plain,
! [X0,X1] :
( ~ sQ316_spl
| member(sK2_skl(X0,X1),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f74,f16626]) ).
fof(f16849,plain,
( ~ sQ316_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16822,f16626]) ).
fof(f16850,plain,
~ sQ316_spl,
inference(contradiction_clause,[status(thm)],[f16849]) ).
fof(f20943,plain,
( sQ177_spl
| ~ subset(sK13_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f7393,f137]) ).
fof(f21026,plain,
( sQ177_spl
| ~ member(sK13_skl,sK14_skl)
| ~ member(sK14_skl,on) ),
inference(resolution,[status(thm)],[f20943,f82]) ).
fof(f21031,plain,
( sQ177_spl
| ~ sQ230_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f21026,f7433,f8367,f7364]) ).
fof(f21032,plain,
$false,
inference(sat_refutation,[status(thm)],[f7459,f7894,f7917,f7966,f8393,f13510,f15752,f15764,f15810,f16698,f16850,f21031]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET810+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:39:27 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 27.75/3.96 % Refutation found
% 27.75/3.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.75/3.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.07/4.29 % Elapsed time: 3.917460 seconds
% 2.07/4.29 % CPU time: 28.778503 seconds
% 2.07/4.29 % Total memory used: 331.505 MB
% 2.07/4.29 % Net memory used: 283.477 MB
%------------------------------------------------------------------------------