%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET668+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:24 PM UTC 2026
% Result : Theorem 0.09s 0.40s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 122 ( 15 unt; 10 def)
% Number of atoms : 409 ( 22 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 485 ( 198 ~; 204 |; 30 &)
% ( 18 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 11 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-3 aty)
% Number of variables : 189 ( 184 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ( subset(C,B)
& subset(B,C) )
=> B = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ( subset(identity_relation_of(D),E)
=> ( subset(D,range(B,C,E))
& subset(D,domain(B,C,E)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( subset(B,C)
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ilf_type(C,subset_type(B))
<=> ilf_type(C,member_type(power_set(B))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(B,power_set(C))
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ( ilf_type(B,member_type(C))
<=> member(B,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> domain(B,C,D) = domain_of(D) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ilf_type(domain(B,C,D),subset_type(B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(C,B))
=> ( subset(identity_relation_of(C),D)
=> ( subset(C,range(C,B,D))
& C = domain(C,B,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(C,B))
=> ( subset(identity_relation_of(C),D)
=> ( subset(C,range(C,B,D))
& C = domain(C,B,D) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f35,plain,
! [B] :
( ! [C] :
( B = C
| ~ subset(C,B)
| ~ subset(B,C)
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f36,plain,
! [X0,X1] :
( X0 = X1
| ~ subset(X1,X0)
| ~ subset(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( subset(D,range(B,C,E))
& subset(D,domain(B,C,E)) )
| ~ subset(identity_relation_of(D),E)
| ~ ilf_type(E,relation_type(B,C)) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f38,plain,
! [X0,X1,X2,X3] :
( subset(X2,domain(X0,X1,X3))
| ~ subset(identity_relation_of(X2),X3)
| ~ ilf_type(X3,relation_type(X0,X1))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0,X1,X2,X3] :
( subset(X2,range(X0,X1,X3))
| ~ subset(identity_relation_of(X2),X3)
| ~ ilf_type(X3,relation_type(X0,X1))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f53,plain,
! [B] :
( ! [C] :
( ( subset(B,C)
<=> ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f54,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| subset(B,C) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
! [B] :
( ! [C] :
( ( ( ( ~ member(sK1_skl(C,B),C)
& member(sK1_skl(C,B),B)
& ilf_type(sK1_skl(C,B),set_type) )
| subset(B,C) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ subset(B,C) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B))],[f54]) ).
fof(f58,plain,
! [X0,X1] :
( member(sK1_skl(X1,X0),X0)
| subset(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f59,plain,
! [X0,X1] :
( ~ member(sK1_skl(X1,X0),X1)
| subset(X0,X1)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f88,plain,
! [B] :
( ! [C] :
( ( ilf_type(C,subset_type(B))
<=> ilf_type(C,member_type(power_set(B))) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f89,plain,
! [B] :
( ! [C] :
( ( ( ~ ilf_type(C,member_type(power_set(B)))
| ilf_type(C,subset_type(B)) )
& ( ilf_type(C,member_type(power_set(B)))
| ~ ilf_type(C,subset_type(B)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( ilf_type(X1,member_type(power_set(X0)))
| ~ ilf_type(X1,subset_type(X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f99,plain,
! [B] :
( ! [C] :
( ( member(B,power_set(C))
<=> ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f100,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| member(B,power_set(C)) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [B] :
( ! [C] :
( ( ( ( ~ member(sK6_skl(C,B),C)
& member(sK6_skl(C,B),B)
& ilf_type(sK6_skl(C,B),set_type) )
| member(B,power_set(C)) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(D,sK6_skl(C,B))],[f100]) ).
fof(f102,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ ilf_type(X2,set_type)
| ~ member(X0,power_set(X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f106,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f107,plain,
! [X0] :
( ~ empty(power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f109,plain,
! [B] :
( ! [C] :
( ( ilf_type(B,member_type(C))
<=> member(B,C) )
| ~ ilf_type(C,set_type)
| empty(C) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f110,plain,
! [B] :
( ! [C] :
( ( ( ~ member(B,C)
| ilf_type(B,member_type(C)) )
& ( member(B,C)
| ~ ilf_type(B,member_type(C)) ) )
| ~ ilf_type(C,set_type)
| empty(C) )
| ~ ilf_type(B,set_type) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( member(X0,X1)
| ~ ilf_type(X0,member_type(X1))
| ~ ilf_type(X1,set_type)
| empty(X1)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f135,plain,
! [B] :
( ! [C] :
( ! [D] :
( domain(B,C,D) = domain_of(D)
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f136,plain,
! [X0,X1,X2] :
( domain(X0,X1,X2) = domain_of(X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [B] :
( ! [C] :
( ! [D] :
( ilf_type(domain(B,C,D),subset_type(B))
| ~ ilf_type(D,relation_type(B,C)) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f138,plain,
! [X0,X1,X2] :
( ilf_type(domain(X0,X1,X2),subset_type(X0))
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f143,plain,
! [X0] : ilf_type(X0,set_type),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f144,plain,
? [B] :
( ? [C] :
( ? [D] :
( ( ~ subset(C,range(C,B,D))
| C != domain(C,B,D) )
& subset(identity_relation_of(C),D)
& ilf_type(D,relation_type(C,B)) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f145,plain,
( ( ~ subset(sK13_skl,range(sK13_skl,sK12_skl,sK14_skl))
| sK13_skl != domain(sK13_skl,sK12_skl,sK14_skl) )
& subset(identity_relation_of(sK13_skl),sK14_skl)
& ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl))
& ilf_type(sK13_skl,set_type)
& ilf_type(sK12_skl,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(B,sK12_skl),skolemize(C,sK13_skl),skolemize(D,sK14_skl)],[f144]) ).
fof(f148,plain,
ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl)),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f149,plain,
subset(identity_relation_of(sK13_skl),sK14_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f150,plain,
( ~ subset(sK13_skl,range(sK13_skl,sK12_skl,sK14_skl))
| sK13_skl != domain(sK13_skl,sK12_skl,sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f151,definition,
( sQ0_spl
<=> sK13_skl = domain(sK13_skl,sK12_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f154,definition,
( sQ1_spl
<=> subset(sK13_skl,range(sK13_skl,sK12_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f156,plain,
( sQ1_spl
| ~ subset(sK13_skl,range(sK13_skl,sK12_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f154]) ).
fof(f157,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f150,f151,f154]) ).
fof(f167,plain,
! [X0,X1] :
( X1 = X0
| ~ subset(X0,X1)
| ~ subset(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f36,f143]) ).
fof(f168,plain,
! [X0,X1] :
( X0 = X1
| ~ subset(X1,X0)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f167,f143]) ).
fof(f169,plain,
! [X0,X1,X2,X3] :
( subset(X1,domain(X3,X0,X2))
| ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f38,f143]) ).
fof(f170,plain,
! [X0] : ~ empty(power_set(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f107,f143]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( ~ subset(identity_relation_of(X3),X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X1,set_type)
| domain(X0,X1,X2) = X3
| ~ subset(domain(X0,X1,X2),X3) ),
inference(resolution,[status(thm)],[f168,f169]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( ~ subset(identity_relation_of(X3),X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X3,set_type)
| domain(X0,X1,X2) = X3
| ~ subset(domain(X0,X1,X2),X3) ),
inference(forward_subsumption_resolution,[status(thm)],[f172,f143]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( subset(X1,range(X3,X0,X2))
| ~ subset(identity_relation_of(X1),X2)
| ~ ilf_type(X2,relation_type(X3,X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f39,f143]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( subset(X3,range(X2,X0,X1))
| ~ subset(identity_relation_of(X3),X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f183,f143]) ).
fof(f185,plain,
! [X0,X1,X2,X3] :
( subset(X3,range(X1,X2,X0))
| ~ subset(identity_relation_of(X3),X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f184,f143]) ).
fof(f188,plain,
! [X0] :
( subset(X0,range(sK13_skl,sK12_skl,sK14_skl))
| ~ subset(identity_relation_of(X0),sK14_skl) ),
inference(resolution,[status(thm)],[f185,f148]) ).
fof(f189,plain,
subset(sK13_skl,range(sK13_skl,sK12_skl,sK14_skl)),
inference(resolution,[status(thm)],[f188,f149]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ilf_type(domain(X2,X0,X1),subset_type(X2))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f138,f143]) ).
fof(f202,plain,
! [X0,X1,X2,X3] :
( ~ subset(identity_relation_of(X3),X2)
| ~ ilf_type(X2,relation_type(X0,X1))
| domain(X0,X1,X2) = X3
| ~ subset(domain(X0,X1,X2),X3) ),
inference(forward_subsumption_resolution,[status(thm)],[f181,f143]) ).
fof(f203,plain,
! [X0] :
( ~ subset(identity_relation_of(X0),sK14_skl)
| domain(sK13_skl,sK12_skl,sK14_skl) = X0
| ~ subset(domain(sK13_skl,sK12_skl,sK14_skl),X0) ),
inference(resolution,[status(thm)],[f202,f148]) ).
fof(f204,plain,
( domain(sK13_skl,sK12_skl,sK14_skl) = sK13_skl
| ~ subset(domain(sK13_skl,sK12_skl,sK14_skl),sK13_skl) ),
inference(resolution,[status(thm)],[f203,f149]) ).
fof(f205,definition,
( sQ6_spl
<=> subset(domain(sK13_skl,sK12_skl,sK14_skl),sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ6_spl
| ~ subset(domain(sK13_skl,sK12_skl,sK14_skl),sK13_skl) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,plain,
( sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f204,f205,f151]) ).
fof(f209,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f189]) ).
fof(f210,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f209]) ).
fof(f283,plain,
! [X0,X1] :
( member(sK1_skl(X0,X1),X1)
| subset(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f58,f143]) ).
fof(f284,plain,
! [X0,X1] :
( member(sK1_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f283,f143]) ).
fof(f289,plain,
! [X0,X1] :
( ~ member(sK1_skl(X0,X1),X0)
| subset(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f59,f143]) ).
fof(f290,plain,
! [X0,X1] :
( ~ member(sK1_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f289,f143]) ).
fof(f384,plain,
! [X0,X1] :
( ilf_type(X0,member_type(power_set(X1)))
| ~ ilf_type(X0,subset_type(X1))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f90,f143]) ).
fof(f457,plain,
! [X0,X1] :
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| ~ ilf_type(X0,set_type)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f111,f143]) ).
fof(f458,plain,
! [X0,X1] :
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f457,f143]) ).
fof(f460,plain,
! [X0,X1] :
( ~ ilf_type(X1,subset_type(X0))
| ~ ilf_type(X1,set_type)
| member(X1,power_set(X0))
| empty(power_set(X0)) ),
inference(resolution,[status(thm)],[f458,f384]) ).
fof(f462,plain,
! [X0,X1] :
( ~ ilf_type(X0,subset_type(X1))
| ~ ilf_type(X0,set_type)
| member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f170]) ).
fof(f472,plain,
! [X0,X1] :
( ~ ilf_type(X0,subset_type(X1))
| member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f143]) ).
fof(f475,plain,
! [X0,X1,X2] :
( ~ ilf_type(X2,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| member(domain(X0,X1,X2),power_set(X0)) ),
inference(resolution,[status(thm)],[f472,f200]) ).
fof(f478,plain,
! [X0,X1,X2] :
( ~ ilf_type(X2,relation_type(X0,X1))
| member(domain(X0,X1,X2),power_set(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f143]) ).
fof(f486,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| ~ ilf_type(X2,set_type)
| ~ member(X1,power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f102,f143]) ).
fof(f487,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| ~ member(X1,power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[f486,f143]) ).
fof(f488,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ member(X0,power_set(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f143]) ).
fof(f491,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ member(sK1_skl(X1,X2),X0)
| ~ member(X0,power_set(X1)) ),
inference(resolution,[status(thm)],[f488,f290]) ).
fof(f593,plain,
! [X0,X1] :
( subset(X0,X1)
| subset(X0,X1)
| ~ member(X0,power_set(X1)) ),
inference(resolution,[status(thm)],[f491,f284]) ).
fof(f599,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ member(X0,power_set(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f593]) ).
fof(f824,plain,
! [X0,X1,X2] :
( domain(X2,X0,X1) = domain_of(X1)
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(forward_subsumption_resolution,[status(thm)],[f136,f143]) ).
fof(f825,plain,
! [X0,X1,X2] :
( domain(X1,X2,X0) = domain_of(X0)
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[f824,f143]) ).
fof(f845,definition,
( sQ36_spl
<=> ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f847,plain,
( sQ36_spl
| ~ ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl)) ),
inference(component_clause,[status(thm)],[f845]) ).
fof(f864,definition,
( sQ41_spl
<=> ilf_type(sK12_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( sQ41_spl
| ~ ilf_type(sK12_skl,set_type) ),
inference(component_clause,[status(thm)],[f864]) ).
fof(f871,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f847,f148]) ).
fof(f872,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f871]) ).
fof(f873,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f866,f143]) ).
fof(f874,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f873]) ).
fof(f883,definition,
( sQ44_spl
<=> ilf_type(sK13_skl,set_type) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f885,plain,
( sQ44_spl
| ~ ilf_type(sK13_skl,set_type) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f891,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f885,f143]) ).
fof(f892,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f891]) ).
fof(f963,definition,
( sQ52_spl
<=> ilf_type(ordered_pair(sK11_skl(sK13_skl),sK11_skl(sK13_skl)),set_type) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f965,plain,
( sQ52_spl
| ~ ilf_type(ordered_pair(sK11_skl(sK13_skl),sK11_skl(sK13_skl)),set_type) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f971,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f965,f143]) ).
fof(f972,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f971]) ).
fof(f977,definition,
( sQ54_spl
<=> empty(power_set(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f978,plain,
( ~ sQ54_spl
| empty(power_set(sK12_skl)) ),
inference(component_clause,[status(thm)],[f977]) ).
fof(f981,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f978,f170]) ).
fof(f982,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f981]) ).
fof(f997,plain,
domain(sK13_skl,sK12_skl,sK14_skl) = domain_of(sK14_skl),
inference(resolution,[status(thm)],[f825,f148]) ).
fof(f1002,plain,
( sQ6_spl
| ~ subset(domain_of(sK14_skl),sK13_skl) ),
inference(backward_demodulation,[status(thm)],[f997,f207]) ).
fof(f1005,plain,
( ~ ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl))
| member(domain_of(sK14_skl),power_set(sK13_skl)) ),
inference(paramodulation,[status(thm)],[f997,f478]) ).
fof(f1010,definition,
( sQ55_spl
<=> member(domain_of(sK14_skl),power_set(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
( ~ sQ55_spl
| member(domain_of(sK14_skl),power_set(sK13_skl)) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,plain,
( ~ sQ36_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1005,f1010,f845]) ).
fof(f1028,plain,
( sQ6_spl
| ~ member(domain_of(sK14_skl),power_set(sK13_skl)) ),
inference(resolution,[status(thm)],[f1002,f599]) ).
fof(f1034,definition,
( sQ60_spl
<=> ilf_type(domain_of(sK14_skl),set_type) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
( sQ60_spl
| ~ ilf_type(domain_of(sK14_skl),set_type) ),
inference(component_clause,[status(thm)],[f1034]) ).
fof(f1042,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1036,f143]) ).
fof(f1043,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f1042]) ).
fof(f1046,plain,
( sQ6_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f1011]) ).
fof(f1047,plain,
( sQ6_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f1046]) ).
fof(f1048,plain,
$false,
inference(sat_refutation,[status(thm)],[f157,f208,f210,f872,f874,f892,f972,f982,f1013,f1043,f1047]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET668+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:34:52 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.40 % Refutation found
% 0.09/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.42 % Elapsed time: 0.045740 seconds
% 0.09/0.42 % CPU time: 0.161522 seconds
% 0.09/0.42 % Total memory used: 25.868 MB
% 0.09/0.42 % Net memory used: 25.657 MB
%------------------------------------------------------------------------------