%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET695+4 : TPTP v9.3.1. Released v2.2.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:10:28 PM UTC 2026
% Result : Theorem 0.18s 0.87s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 44
% Syntax : Number of formulae : 236 ( 19 unt; 37 def)
% Number of atoms : 564 ( 29 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 582 ( 254 ~; 246 |; 31 &)
% ( 46 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 38 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 279 ( 269 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,A] :
( member(X,power_set(A))
<=> subset(X,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = 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,conjecture,
! [A,B,E] :
( ( subset(B,E)
& subset(A,E) )
=> ( subset(A,B)
<=> subset(difference(E,B),difference(E,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
~ ! [A,B,E] :
( ( subset(B,E)
& subset(A,E) )
=> ( subset(A,B)
<=> subset(difference(E,B),difference(E,A)) ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f14,plain,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f15,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)],[f14]) ).
fof(f16,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)],[f15]) ).
fof(f17,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))],[f16]) ).
fof(f18,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f19,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f20,plain,
! [X0,X1] :
( ~ member(sK0_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f26,plain,
! [X,A] :
( ( ~ subset(X,A)
| member(X,power_set(A)) )
& ( subset(X,A)
| ~ member(X,power_set(A)) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f27,plain,
( ! [X,A] :
( ~ subset(X,A)
| member(X,power_set(A)) )
& ! [X,A] :
( subset(X,A)
| ~ member(X,power_set(A)) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ member(X0,power_set(X1)) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| member(X0,power_set(X1)) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f40,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f41,plain,
! [B,A,E] :
( ( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f42,plain,
( ! [B,A,E] :
( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ! [B,A,E] :
( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f43,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f45,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,X1)
| member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f46,plain,
! [X,A] :
( ( X != A
| member(X,singleton(A)) )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f47,plain,
( ! [X,A] :
( X != A
| member(X,singleton(A)) )
& ! [X,A] :
( X = A
| ~ member(X,singleton(A)) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( X0 != X1
| member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f61,plain,
! [X,A] :
( member(X,product(A))
<=> ! [Y] :
( member(X,Y)
| ~ member(Y,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f62,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)],[f61]) ).
fof(f63,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)],[f62]) ).
fof(f64,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))],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X2,X1)
| ~ member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( member(sK2_skl(X1,X0),X1)
| member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [X0,X1] :
( ~ member(X0,sK2_skl(X1,X0))
| member(X0,product(X1)) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f68,plain,
? [A,B,E] :
( ( subset(A,B)
<~> subset(difference(E,B),difference(E,A)) )
& subset(B,E)
& subset(A,E) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f69,plain,
? [A,B,E] :
( ( ~ subset(difference(E,B),difference(E,A))
| ~ subset(A,B) )
& ( subset(difference(E,B),difference(E,A))
| subset(A,B) )
& subset(B,E)
& subset(A,E) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
( ( ~ subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl))
| ~ subset(sK3_skl,sK4_skl) )
& ( subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl))
| subset(sK3_skl,sK4_skl) )
& subset(sK4_skl,sK5_skl)
& subset(sK3_skl,sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK3_skl),skolemize(B,sK4_skl),skolemize(E,sK5_skl)],[f69]) ).
fof(f71,plain,
subset(sK3_skl,sK5_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f73,plain,
( subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl))
| subset(sK3_skl,sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f74,plain,
( ~ subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl))
| ~ subset(sK3_skl,sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f75,definition,
( sQ0_spl
<=> subset(sK3_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f76,plain,
( ~ sQ0_spl
| subset(sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f75]) ).
fof(f77,plain,
( sQ0_spl
| ~ subset(sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f75]) ).
fof(f78,definition,
( sQ1_spl
<=> subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f79,plain,
( ~ sQ1_spl
| subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f78]) ).
fof(f80,plain,
( sQ1_spl
| ~ subset(difference(sK5_skl,sK4_skl),difference(sK5_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f78]) ).
fof(f81,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f73,f75,f78]) ).
fof(f82,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f74,f75,f78]) ).
fof(f83,plain,
! [X0] : member(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f49]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,difference(difference(X2,X1),X3))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f44,f43]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,X2)
| ~ subset(X2,difference(X3,X1))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f44,f18]) ).
fof(f88,plain,
! [X0,X1,X2,X3,X4] :
( ~ member(X0,difference(difference(difference(X2,X1),X3),X4))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f86,f43]) ).
fof(f92,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,difference(sK5_skl,sK4_skl))
| ~ member(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f87,f79]) ).
fof(f102,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f40,f18]) ).
fof(f112,plain,
( sQ0_spl
| member(sK0_skl(sK4_skl,sK3_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f19,f77]) ).
fof(f113,plain,
! [X0,X1] :
( ~ member(X1,X0)
| member(sK0_skl(empty_set,X0),X0) ),
inference(resolution,[status(thm)],[f19,f102]) ).
fof(f118,plain,
! [X0,X1,X2] :
( member(sK0_skl(difference(X1,X2),X0),X2)
| ~ member(sK0_skl(difference(X1,X2),X0),X1)
| subset(X0,difference(X1,X2)) ),
inference(resolution,[status(thm)],[f20,f45]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ~ member(sK0_skl(X1,X0),difference(X1,X2))
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f20,f43]) ).
fof(f125,plain,
( ~ sQ1_spl
| sQ0_spl
| ~ member(sK0_skl(sK4_skl,sK3_skl),difference(sK5_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f112,f92]) ).
fof(f126,plain,
( ~ sQ1_spl
| sQ0_spl
| member(sK0_skl(sK4_skl,sK3_skl),sK4_skl)
| ~ member(sK0_skl(sK4_skl,sK3_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f125,f45]) ).
fof(f129,definition,
( sQ2_spl
<=> member(sK0_skl(sK4_skl,sK3_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f131,plain,
( sQ2_spl
| ~ member(sK0_skl(sK4_skl,sK3_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f129]) ).
fof(f132,definition,
( sQ3_spl
<=> member(sK0_skl(sK4_skl,sK3_skl),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f133,plain,
( ~ sQ3_spl
| member(sK0_skl(sK4_skl,sK3_skl),sK4_skl) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f135,plain,
( ~ sQ1_spl
| sQ0_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f126,f129,f132,f75,f78]) ).
fof(f136,plain,
( sQ1_spl
| member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),difference(sK5_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f80,f19]) ).
fof(f137,plain,
( sQ1_spl
| ~ member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK4_skl) ),
inference(resolution,[status(thm)],[f136,f44]) ).
fof(f146,plain,
( sQ1_spl
| member(sK0_skl(empty_set,difference(sK5_skl,sK4_skl)),difference(sK5_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f113,f136]) ).
fof(f147,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| member(sK0_skl(empty_set,power_set(X0)),power_set(X0)) ),
inference(resolution,[status(thm)],[f113,f29]) ).
fof(f150,plain,
! [X0] : member(sK0_skl(empty_set,singleton(X0)),singleton(X0)),
inference(resolution,[status(thm)],[f113,f83]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ~ member(X1,difference(X0,X2))
| member(sK0_skl(empty_set,X0),X0) ),
inference(resolution,[status(thm)],[f113,f43]) ).
fof(f153,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ subset(X1,X0)
| member(sK0_skl(empty_set,X0),X0) ),
inference(resolution,[status(thm)],[f113,f18]) ).
fof(f154,plain,
! [X0] : sK0_skl(empty_set,singleton(X0)) = X0,
inference(resolution,[status(thm)],[f150,f48]) ).
fof(f162,plain,
( sQ1_spl
| member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK3_skl)
| ~ member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK5_skl) ),
inference(resolution,[status(thm)],[f118,f80]) ).
fof(f166,definition,
( sQ4_spl
<=> member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f169,definition,
( sQ5_spl
<=> member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f170,plain,
( ~ sQ5_spl
| member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK3_skl) ),
inference(component_clause,[status(thm)],[f169]) ).
fof(f172,plain,
( sQ1_spl
| sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f162,f166,f169,f78]) ).
fof(f193,plain,
! [X0,X1,X2] :
( member(sK2_skl(X1,X2),X1)
| member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f65,f66]) ).
fof(f224,definition,
! [X0] :
( sQ7_spl
<=> member(sK0_skl(empty_set,difference(sK5_skl,sK4_skl)),X0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f225,plain,
! [X0] :
( ~ sQ7_spl
| member(sK0_skl(empty_set,difference(sK5_skl,sK4_skl)),X0) ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f291,plain,
( sQ1_spl
| member(sK0_skl(empty_set,sK5_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f152,f146]) ).
fof(f355,plain,
! [X0] :
( sQ2_spl
| ~ member(sK0_skl(sK4_skl,sK3_skl),X0)
| ~ subset(X0,sK5_skl) ),
inference(resolution,[status(thm)],[f131,f18]) ).
fof(f422,plain,
( sQ2_spl
| ~ member(sK0_skl(sK4_skl,sK3_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f355,f71]) ).
fof(f426,plain,
( sQ2_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f112]) ).
fof(f427,plain,
( sQ2_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f426]) ).
fof(f444,plain,
( ~ sQ7_spl
| $false ),
inference(resolution,[status(thm)],[f225,f40]) ).
fof(f469,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f444]) ).
fof(f471,plain,
( ~ sQ3_spl
| subset(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f133,f20]) ).
fof(f476,plain,
( ~ sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f471,f75,f132]) ).
fof(f530,plain,
! [X0,X1] :
( member(sK2_skl(singleton(X1),X0),singleton(X1))
| member(X0,X1) ),
inference(resolution,[status(thm)],[f193,f83]) ).
fof(f554,plain,
! [X0,X1] :
( sK2_skl(singleton(X1),X0) = X1
| member(X0,X1) ),
inference(resolution,[status(thm)],[f530,f48]) ).
fof(f578,plain,
! [X0] : sK2_skl(singleton(empty_set),X0) = empty_set,
inference(resolution,[status(thm)],[f554,f40]) ).
fof(f599,plain,
! [X0,X1] :
( member(sK0_skl(empty_set,X0),X0)
| sK2_skl(singleton(X0),X1) = X0 ),
inference(resolution,[status(thm)],[f554,f113]) ).
fof(f600,plain,
! [X0] :
( member(empty_set,singleton(empty_set))
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f578,f530]) ).
fof(f604,definition,
! [X0] :
( sQ11_spl
<=> member(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f605,plain,
! [X0] :
( ~ sQ11_spl
| member(X0,empty_set) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f607,definition,
( sQ12_spl
<=> member(empty_set,singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f610,plain,
( sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f600,f604,f607]) ).
fof(f611,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f605,f40]) ).
fof(f612,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f611]) ).
fof(f711,plain,
! [X0,X1] :
( subset(sK0_skl(empty_set,power_set(X1)),X1)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f147,f28]) ).
fof(f725,plain,
! [X0,X1] :
( ~ member(X1,sK0_skl(empty_set,power_set(empty_set)))
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f711,f102]) ).
fof(f732,definition,
! [X0] :
( sQ15_spl
<=> ~ subset(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f733,plain,
! [X0] :
( ~ sQ15_spl
| ~ subset(X0,empty_set) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f735,definition,
! [X1] :
( sQ16_spl
<=> ~ member(X1,sK0_skl(empty_set,power_set(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f736,plain,
! [X0] :
( ~ sQ16_spl
| ~ member(X0,sK0_skl(empty_set,power_set(empty_set))) ),
inference(component_clause,[status(thm)],[f735]) ).
fof(f738,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f725,f732,f735]) ).
fof(f741,plain,
! [X0] :
( ~ sQ15_spl
| member(sK0_skl(empty_set,X0),X0) ),
inference(resolution,[status(thm)],[f733,f19]) ).
fof(f742,plain,
! [X0] :
( ~ sQ15_spl
| subset(difference(empty_set,X0),empty_set) ),
inference(resolution,[status(thm)],[f741,f119]) ).
fof(f772,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f742,f733]) ).
fof(f773,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f772]) ).
fof(f793,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ member(X1,X0)
| ~ subset(X0,sK0_skl(empty_set,power_set(empty_set))) ),
inference(resolution,[status(thm)],[f736,f18]) ).
fof(f867,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ subset(X1,sK0_skl(empty_set,power_set(empty_set)))
| ~ member(X0,sK0_skl(empty_set,power_set(sK0_skl(empty_set,power_set(empty_set))))) ),
inference(resolution,[status(thm)],[f793,f711]) ).
fof(f870,definition,
! [X0] :
( sQ17_spl
<=> ~ member(X0,sK0_skl(empty_set,power_set(sK0_skl(empty_set,power_set(empty_set))))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f873,definition,
! [X1] :
( sQ18_spl
<=> ~ subset(X1,sK0_skl(empty_set,power_set(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f876,plain,
( ~ sQ16_spl
| sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f867,f870,f873,f735]) ).
fof(f916,plain,
! [X0] :
( ~ member(X0,sK3_skl)
| member(sK0_skl(empty_set,sK5_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f153,f71]) ).
fof(f929,definition,
( sQ19_spl
<=> member(sK0_skl(empty_set,sK5_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f939,definition,
! [X0] :
( sQ22_spl
<=> ~ member(X0,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f940,plain,
! [X0] :
( ~ sQ22_spl
| ~ member(X0,sK3_skl) ),
inference(component_clause,[status(thm)],[f939]) ).
fof(f943,plain,
( sQ22_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f916,f929,f939]) ).
fof(f1161,definition,
! [X0] :
( sQ26_spl
<=> sK0_skl(empty_set,sK5_skl) = X0 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1162,plain,
! [X0] :
( ~ sQ26_spl
| sK0_skl(empty_set,sK5_skl) = X0 ),
inference(component_clause,[status(thm)],[f1161]) ).
fof(f1169,plain,
! [X0,X1] :
( ~ sQ26_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f1162,f1162]) ).
fof(f1170,plain,
! [X0] :
( ~ sQ26_spl
| sQ1_spl
| member(X0,sK5_skl) ),
inference(paramodulation,[status(thm)],[f1162,f291]) ).
fof(f1182,definition,
( sQ30_spl
<=> subset(sK5_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1225,plain,
! [X0,X1] :
( ~ sQ26_spl
| sQ1_spl
| member(X0,X1) ),
inference(paramodulation,[status(thm)],[f1169,f1170]) ).
fof(f1245,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ26_spl
| sQ1_spl
| ~ member(X0,difference(difference(difference(X1,X2),X3),X4)) ),
inference(backward_subsumption_resolution,[status(thm)],[f88,f1225]) ).
fof(f1271,plain,
( ~ sQ26_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1245,f1225]) ).
fof(f1272,plain,
( ~ sQ26_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1271]) ).
fof(f1283,plain,
! [X0,X1] :
( ~ subset(power_set(X1),empty_set)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f29,f102]) ).
fof(f1308,plain,
! [X0] :
( member(X0,sK5_skl)
| ~ member(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f18,f71]) ).
fof(f1331,plain,
! [X0] :
( member(X0,sK5_skl)
| sK2_skl(singleton(sK3_skl),X0) = sK3_skl ),
inference(resolution,[status(thm)],[f554,f1308]) ).
fof(f1345,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| sK2_skl(singleton(X0),X1) = X0 ),
inference(resolution,[status(thm)],[f554,f102]) ).
fof(f1354,plain,
! [X0,X1,X2] :
( member(sK2_skl(X1,X2),X1)
| member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f65,f66]) ).
fof(f1383,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| sK2_skl(singleton(sK0_skl(empty_set,power_set(empty_set))),X0) = sK0_skl(empty_set,power_set(empty_set)) ),
inference(resolution,[status(thm)],[f1345,f711]) ).
fof(f1385,definition,
! [X0] :
( sQ34_spl
<=> sK2_skl(singleton(sK0_skl(empty_set,power_set(empty_set))),X0) = sK0_skl(empty_set,power_set(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1388,plain,
( sQ15_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f1383,f1385,f732]) ).
fof(f1486,plain,
! [X0] :
( member(sK0_skl(empty_set,sK5_skl),sK5_skl)
| sK2_skl(singleton(sK3_skl),X0) = sK3_skl ),
inference(resolution,[status(thm)],[f1331,f113]) ).
fof(f1488,plain,
! [X0] :
( ~ subset(sK5_skl,empty_set)
| sK2_skl(singleton(sK3_skl),X0) = sK3_skl ),
inference(resolution,[status(thm)],[f1331,f102]) ).
fof(f1489,definition,
! [X0] :
( sQ35_spl
<=> sK2_skl(singleton(sK3_skl),X0) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1490,plain,
! [X0] :
( ~ sQ35_spl
| sK2_skl(singleton(sK3_skl),X0) = sK3_skl ),
inference(component_clause,[status(thm)],[f1489]) ).
fof(f1492,plain,
( sQ19_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1486,f1489,f929]) ).
fof(f1493,plain,
( ~ sQ30_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1488,f1489,f1182]) ).
fof(f1495,plain,
! [X0] :
( ~ sQ35_spl
| ~ member(X0,sK3_skl)
| member(X0,product(singleton(sK3_skl))) ),
inference(paramodulation,[status(thm)],[f1490,f67]) ).
fof(f1764,definition,
! [X0,X1] :
( sQ41_spl
<=> member(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1765,plain,
! [X0,X1] :
( ~ sQ41_spl
| member(X0,X1) ),
inference(component_clause,[status(thm)],[f1764]) ).
fof(f1818,plain,
! [X0] :
( ~ sQ35_spl
| member(sK3_skl,singleton(sK3_skl))
| member(X0,sK3_skl) ),
inference(paramodulation,[status(thm)],[f1490,f530]) ).
fof(f1827,definition,
! [X0] :
( sQ43_spl
<=> member(X0,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
! [X0] :
( ~ sQ43_spl
| member(X0,sK3_skl) ),
inference(component_clause,[status(thm)],[f1827]) ).
fof(f1830,definition,
( sQ44_spl
<=> member(sK3_skl,singleton(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1833,plain,
( ~ sQ35_spl
| sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1818,f1827,f1830,f1489]) ).
fof(f1840,plain,
! [X0,X1,X2,X3] :
( ~ sQ41_spl
| ~ member(X0,difference(difference(X1,X2),X3)) ),
inference(backward_subsumption_resolution,[status(thm)],[f86,f1765]) ).
fof(f1869,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1840,f1765]) ).
fof(f1870,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1869]) ).
fof(f1871,plain,
( ~ sQ43_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1828,f940]) ).
fof(f1872,plain,
( ~ sQ43_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f1871]) ).
fof(f1887,plain,
! [X0,X1,X2] :
( subset(difference(X1,X2),X0)
| member(sK0_skl(X0,difference(X1,X2)),X1) ),
inference(resolution,[status(thm)],[f43,f19]) ).
fof(f1897,plain,
! [X0] :
( ~ sQ0_spl
| member(X0,sK4_skl)
| ~ member(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f18,f76]) ).
fof(f2030,plain,
! [X0,X1] :
( ~ sQ35_spl
| member(X0,X1)
| ~ member(X1,singleton(sK3_skl))
| ~ member(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f1495,f65]) ).
fof(f2160,plain,
! [X0,X1] :
( ~ sQ35_spl
| ~ member(X1,sK3_skl)
| member(sK0_skl(empty_set,sK3_skl),X0)
| ~ member(X0,singleton(sK3_skl)) ),
inference(resolution,[status(thm)],[f2030,f113]) ).
fof(f2164,definition,
! [X0] :
( sQ45_spl
<=> ( member(sK0_skl(empty_set,sK3_skl),X0)
| ~ member(X0,singleton(sK3_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2165,plain,
! [X0] :
( ~ sQ45_spl
| member(sK0_skl(empty_set,sK3_skl),X0)
| ~ member(X0,singleton(sK3_skl)) ),
inference(component_clause,[status(thm)],[f2164]) ).
fof(f2167,plain,
( ~ sQ35_spl
| sQ22_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f2160,f2164,f939,f1489]) ).
fof(f2323,definition,
! [X0,X1] :
( sQ46_spl
<=> ( member(X1,X0)
| ~ member(X0,singleton(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2324,plain,
! [X0,X1] :
( ~ sQ46_spl
| member(X1,X0)
| ~ member(X0,singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f2323]) ).
fof(f2336,plain,
! [X0] :
( ~ sQ46_spl
| member(X0,empty_set) ),
inference(resolution,[status(thm)],[f2324,f83]) ).
fof(f2340,definition,
! [X0] :
( sQ47_spl
<=> member(X0,sK0_skl(empty_set,singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2341,plain,
! [X0] :
( ~ sQ47_spl
| member(X0,sK0_skl(empty_set,singleton(empty_set))) ),
inference(component_clause,[status(thm)],[f2340]) ).
fof(f2347,definition,
! [X1] :
( sQ49_spl
<=> ~ member(X1,singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f2348,plain,
! [X0] :
( ~ sQ49_spl
| ~ member(X0,singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f2347]) ).
fof(f2351,plain,
( ~ sQ46_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2336,f604,f2323]) ).
fof(f2352,plain,
! [X0] :
( ~ sQ47_spl
| member(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f154,f2341]) ).
fof(f2353,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2352,f40]) ).
fof(f2354,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f2353]) ).
fof(f2364,plain,
( ~ sQ49_spl
| $false ),
inference(resolution,[status(thm)],[f2348,f83]) ).
fof(f2368,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f2364]) ).
fof(f2461,plain,
! [X0] :
( ~ sQ45_spl
| sK2_skl(singleton(singleton(sK3_skl)),X0) = singleton(sK3_skl)
| member(sK0_skl(empty_set,sK3_skl),sK0_skl(empty_set,singleton(sK3_skl))) ),
inference(resolution,[status(thm)],[f2165,f599]) ).
fof(f2467,definition,
( sQ55_spl
<=> member(sK0_skl(empty_set,sK3_skl),sK0_skl(empty_set,singleton(sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2468,plain,
( ~ sQ55_spl
| member(sK0_skl(empty_set,sK3_skl),sK0_skl(empty_set,singleton(sK3_skl))) ),
inference(component_clause,[status(thm)],[f2467]) ).
fof(f2470,definition,
! [X0] :
( sQ56_spl
<=> sK2_skl(singleton(singleton(sK3_skl)),X0) = singleton(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2471,plain,
! [X0] :
( ~ sQ56_spl
| sK2_skl(singleton(singleton(sK3_skl)),X0) = singleton(sK3_skl) ),
inference(component_clause,[status(thm)],[f2470]) ).
fof(f2473,plain,
( ~ sQ45_spl
| sQ56_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f2461,f2467,f2470,f2164]) ).
fof(f2474,definition,
! [X0] :
( sQ57_spl
<=> ~ member(X0,singleton(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2475,plain,
! [X0] :
( ~ sQ57_spl
| ~ member(X0,singleton(sK3_skl)) ),
inference(component_clause,[status(thm)],[f2474]) ).
fof(f2478,plain,
( ~ sQ55_spl
| member(sK0_skl(empty_set,sK3_skl),sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f154,f2468]) ).
fof(f2488,plain,
( ~ sQ57_spl
| $false ),
inference(resolution,[status(thm)],[f2475,f83]) ).
fof(f2491,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f2488]) ).
fof(f2511,definition,
! [X1] :
( sQ60_spl
<=> ~ member(X1,singleton(singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2512,plain,
! [X0] :
( ~ sQ60_spl
| ~ member(X0,singleton(singleton(empty_set))) ),
inference(component_clause,[status(thm)],[f2511]) ).
fof(f2527,plain,
( ~ sQ60_spl
| $false ),
inference(resolution,[status(thm)],[f2512,f83]) ).
fof(f2530,plain,
~ sQ60_spl,
inference(contradiction_clause,[status(thm)],[f2527]) ).
fof(f2533,plain,
! [X0,X1] :
( ~ sQ56_spl
| member(singleton(sK3_skl),singleton(singleton(sK3_skl)))
| member(X1,X0)
| ~ member(X0,singleton(singleton(sK3_skl))) ),
inference(paramodulation,[status(thm)],[f2471,f1354]) ).
fof(f2537,definition,
! [X0] :
( sQ62_spl
<=> X0 = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f2538,plain,
! [X0] :
( ~ sQ62_spl
| X0 = sK3_skl ),
inference(component_clause,[status(thm)],[f2537]) ).
fof(f2542,definition,
! [X0,X1] :
( sQ63_spl
<=> ( member(X1,X0)
| ~ member(X0,singleton(singleton(sK3_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f2543,plain,
! [X0,X1] :
( ~ sQ63_spl
| member(X1,X0)
| ~ member(X0,singleton(singleton(sK3_skl))) ),
inference(component_clause,[status(thm)],[f2542]) ).
fof(f2545,definition,
( sQ64_spl
<=> member(singleton(sK3_skl),singleton(singleton(sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f2548,plain,
( ~ sQ56_spl
| sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f2533,f2542,f2545,f2470]) ).
fof(f2549,plain,
! [X0,X1] :
( ~ sQ62_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f2538,f2538]) ).
fof(f2559,plain,
! [X0] :
( ~ sQ62_spl
| subset(X0,sK5_skl) ),
inference(paramodulation,[status(thm)],[f2538,f71]) ).
fof(f2577,plain,
! [X0,X1] :
( ~ sQ62_spl
| subset(X0,X1) ),
inference(paramodulation,[status(thm)],[f2549,f2559]) ).
fof(f2581,plain,
! [X0] :
( ~ sQ62_spl
| ~ subset(power_set(X0),empty_set) ),
inference(backward_subsumption_resolution,[status(thm)],[f1283,f2577]) ).
fof(f2597,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2581,f2577]) ).
fof(f2598,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f2597]) ).
fof(f2726,definition,
! [X1] :
( sQ65_spl
<=> ~ member(X1,power_set(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f2727,plain,
! [X0] :
( ~ sQ65_spl
| ~ member(X0,power_set(empty_set)) ),
inference(component_clause,[status(thm)],[f2726]) ).
fof(f2738,plain,
! [X0,X1] :
( ~ sQ63_spl
| ~ member(X1,singleton(singleton(sK3_skl)))
| member(X0,sK0_skl(empty_set,singleton(singleton(sK3_skl)))) ),
inference(resolution,[status(thm)],[f2543,f113]) ).
fof(f2742,definition,
! [X0] :
( sQ66_spl
<=> member(X0,sK0_skl(empty_set,singleton(singleton(sK3_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f2743,plain,
! [X0] :
( ~ sQ66_spl
| member(X0,sK0_skl(empty_set,singleton(singleton(sK3_skl)))) ),
inference(component_clause,[status(thm)],[f2742]) ).
fof(f2745,definition,
! [X1] :
( sQ67_spl
<=> ~ member(X1,singleton(singleton(sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f2746,plain,
! [X0] :
( ~ sQ67_spl
| ~ member(X0,singleton(singleton(sK3_skl))) ),
inference(component_clause,[status(thm)],[f2745]) ).
fof(f2748,plain,
( ~ sQ63_spl
| sQ67_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f2738,f2742,f2745,f2542]) ).
fof(f2749,plain,
! [X0] :
( ~ sQ66_spl
| member(X0,singleton(sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f154,f2743]) ).
fof(f2750,plain,
! [X0] :
( ~ sQ66_spl
| X0 = sK3_skl ),
inference(resolution,[status(thm)],[f2749,f48]) ).
fof(f2751,plain,
( ~ sQ66_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f2750,f2537,f2742]) ).
fof(f2757,plain,
( ~ sQ67_spl
| $false ),
inference(resolution,[status(thm)],[f2746,f83]) ).
fof(f2760,plain,
~ sQ67_spl,
inference(contradiction_clause,[status(thm)],[f2757]) ).
fof(f2770,plain,
! [X0] :
( ~ sQ65_spl
| ~ subset(X0,empty_set) ),
inference(resolution,[status(thm)],[f2727,f29]) ).
fof(f2773,plain,
( ~ sQ65_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2770,f732,f2726]) ).
fof(f3129,definition,
! [X0] :
( sQ79_spl
<=> ~ member(X0,singleton(power_set(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f3130,plain,
! [X0] :
( ~ sQ79_spl
| ~ member(X0,singleton(power_set(empty_set))) ),
inference(component_clause,[status(thm)],[f3129]) ).
fof(f3146,plain,
( ~ sQ79_spl
| $false ),
inference(resolution,[status(thm)],[f3130,f83]) ).
fof(f3149,plain,
~ sQ79_spl,
inference(contradiction_clause,[status(thm)],[f3146]) ).
fof(f3173,plain,
( ~ sQ5_spl
| ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f170,f940]) ).
fof(f3183,plain,
( ~ sQ5_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f3173]) ).
fof(f3419,plain,
( ~ sQ55_spl
| ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2478,f940]) ).
fof(f3430,plain,
( ~ sQ55_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f3419]) ).
fof(f3476,plain,
( sQ1_spl
| member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK5_skl) ),
inference(resolution,[status(thm)],[f1887,f80]) ).
fof(f3492,plain,
( sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3476,f166,f78]) ).
fof(f3494,plain,
( sQ1_spl
| ~ sQ0_spl
| ~ member(sK0_skl(difference(sK5_skl,sK3_skl),difference(sK5_skl,sK4_skl)),sK3_skl) ),
inference(resolution,[status(thm)],[f1897,f137]) ).
fof(f3495,plain,
( sQ1_spl
| ~ sQ0_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f3494,f169,f75,f78]) ).
fof(f3496,plain,
$false,
inference(sat_refutation,[status(thm)],[f81,f82,f135,f172,f427,f469,f476,f610,f612,f738,f773,f876,f943,f1272,f1388,f1492,f1493,f1833,f1870,f1872,f2167,f2351,f2354,f2368,f2473,f2491,f2530,f2548,f2598,f2748,f2751,f2760,f2773,f3149,f3183,f3430,f3492,f3495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET695+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n002.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 05:35:32 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.18/0.43 % Drodi V4.1.1
% 0.18/0.87 % Refutation found
% 0.18/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.26/0.92 % Elapsed time: 0.489222 seconds
% 0.26/0.92 % CPU time: 3.545870 seconds
% 0.26/0.92 % Total memory used: 112.415 MB
% 0.26/0.92 % Net memory used: 106.778 MB
%------------------------------------------------------------------------------