%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU111+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:14 PM UTC 2026
% Result : Theorem 69.98s 9.42s
% Output : CNFRefutation 70.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 62
% Syntax : Number of formulae : 265 ( 61 unt; 37 def)
% Number of atoms : 652 ( 48 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 649 ( 262 ~; 237 |; 95 &)
% ( 47 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 38 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 236 ( 220 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [A,B] :
( element(B,finite_subsets(A))
=> finite(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( preboolean(B)
=> ( B = finite_subsets(A)
<=> ! [C] :
( in(C,B)
<=> ( finite(C)
& subset(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : preboolean(finite_subsets(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( preboolean(finite_subsets(A))
& diff_closed(finite_subsets(A))
& cup_closed(finite_subsets(A))
& ~ empty(finite_subsets(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] : set_intersection2(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
? [A] :
( preboolean(A)
& diff_closed(A)
& cap_closed(A)
& cup_closed(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
? [B] :
( finite(B)
& natural(B)
& ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B)
& one_to_one(B)
& function(B)
& relation(B)
& empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A,B] : subset(set_intersection2(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A,B,C] :
( ( subset(A,C)
& subset(A,B) )
=> subset(A,set_intersection2(B,C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( subset(A,B)
=> subset(finite_subsets(A),finite_subsets(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,conjecture,
! [A,B] : finite_subsets(set_intersection2(A,B)) = set_intersection2(finite_subsets(A),finite_subsets(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
~ ! [A,B] : finite_subsets(set_intersection2(A,B)) = set_intersection2(finite_subsets(A),finite_subsets(B)),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,plain,
! [A,B] :
( finite(B)
| ~ element(B,finite_subsets(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f57,plain,
! [B] :
( finite(B)
| ! [A] : ~ element(B,finite_subsets(A)) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( finite(X0)
| ~ element(X0,finite_subsets(X1)) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f60,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f61,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f66,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f66]) ).
fof(f68,plain,
( ! [A,B] :
( ( ~ in(sK0_skl(B,A),B)
& in(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f67]) ).
fof(f69,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f72,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f73,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( in(D,B)
& in(D,A) )
| in(D,C) )
& ( ~ in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
( ! [A,B,C] :
( ( ( ( in(sK1_skl(C,B,A),B)
& in(sK1_skl(C,B,A),A) )
| in(sK1_skl(C,B,A),C) )
& ( ~ in(sK1_skl(C,B,A),B)
| ~ in(sK1_skl(C,B,A),A)
| ~ in(sK1_skl(C,B,A),C) ) )
| C = set_intersection2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f73]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ in(sK1_skl(X0,X2,X1),X2)
| ~ in(sK1_skl(X0,X2,X1),X1)
| ~ in(sK1_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f79,plain,
! [X0,X1,X2] :
( in(sK1_skl(X0,X2,X1),X1)
| in(sK1_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f80,plain,
! [X0,X1,X2] :
( in(sK1_skl(X0,X2,X1),X2)
| in(sK1_skl(X0,X2,X1),X0)
| X0 = set_intersection2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f81,plain,
! [A,B] :
( ( B = finite_subsets(A)
<=> ! [C] :
( in(C,B)
<=> ( finite(C)
& subset(C,A) ) ) )
| ~ preboolean(B) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f82,plain,
! [A,B] :
( ( ( ? [C] :
( ( ( finite(C)
& subset(C,A) )
| in(C,B) )
& ( ~ finite(C)
| ~ subset(C,A)
| ~ in(C,B) ) )
| B = finite_subsets(A) )
& ( ! [C] :
( ( ~ finite(C)
| ~ subset(C,A)
| in(C,B) )
& ( ( finite(C)
& subset(C,A) )
| ~ in(C,B) ) )
| B != finite_subsets(A) ) )
| ~ preboolean(B) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [B] :
( ( ! [A] :
( ? [C] :
( ( ( finite(C)
& subset(C,A) )
| in(C,B) )
& ( ~ finite(C)
| ~ subset(C,A)
| ~ in(C,B) ) )
| B = finite_subsets(A) )
& ! [A] :
( ( ! [C] :
( ~ finite(C)
| ~ subset(C,A)
| in(C,B) )
& ! [C] :
( ( finite(C)
& subset(C,A) )
| ~ in(C,B) ) )
| B != finite_subsets(A) ) )
| ~ preboolean(B) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f84,plain,
! [B] :
( ( ! [A] :
( ( ( ( finite(sK2_skl(A,B))
& subset(sK2_skl(A,B),A) )
| in(sK2_skl(A,B),B) )
& ( ~ finite(sK2_skl(A,B))
| ~ subset(sK2_skl(A,B),A)
| ~ in(sK2_skl(A,B),B) ) )
| B = finite_subsets(A) )
& ! [A] :
( ( ! [C] :
( ~ finite(C)
| ~ subset(C,A)
| in(C,B) )
& ! [C] :
( ( finite(C)
& subset(C,A) )
| ~ in(C,B) ) )
| B != finite_subsets(A) ) )
| ~ preboolean(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(A,B))],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != finite_subsets(X1)
| ~ preboolean(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ~ finite(X2)
| ~ subset(X2,X1)
| in(X2,X0)
| X0 != finite_subsets(X1)
| ~ preboolean(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f91,plain,
! [X0] : preboolean(finite_subsets(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f92,plain,
! [A] : element(sK3_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f13]) ).
fof(f93,plain,
! [X0] : element(sK3_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f100,plain,
( ! [A] : preboolean(powerset(A))
& ! [A] : diff_closed(powerset(A))
& ! [A] : cup_closed(powerset(A))
& ! [A] : ~ empty(powerset(A)) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f101,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f107,plain,
( ! [A] : preboolean(finite_subsets(A))
& ! [A] : diff_closed(finite_subsets(A))
& ! [A] : cup_closed(finite_subsets(A))
& ! [A] : ~ empty(finite_subsets(A)) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f108,plain,
! [X0] : ~ empty(finite_subsets(X0)),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f112,plain,
! [A] : set_intersection2(A,A) = A,
inference(miniscoping,[status(thm)],[f20]) ).
fof(f113,plain,
! [X0] : set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
( finite(sK4_skl)
& ~ empty(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f21]) ).
fof(f115,plain,
~ empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f117,plain,
( preboolean(sK5_skl)
& diff_closed(sK5_skl)
& cap_closed(sK5_skl)
& cup_closed(sK5_skl)
& ~ empty(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f22]) ).
fof(f118,plain,
~ empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f129,plain,
! [A] :
( finite(sK8_skl(A))
& natural(sK8_skl(A))
& ordinal(sK8_skl(A))
& epsilon_connected(sK8_skl(A))
& epsilon_transitive(sK8_skl(A))
& one_to_one(sK8_skl(A))
& function(sK8_skl(A))
& relation(sK8_skl(A))
& empty(sK8_skl(A))
& element(sK8_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f25]) ).
fof(f139,plain,
! [X0] : finite(sK8_skl(X0)),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f140,plain,
! [A] :
( empty(sK9_skl(A))
& element(sK9_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f26]) ).
fof(f142,plain,
! [X0] : empty(sK9_skl(X0)),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f143,plain,
~ empty(sK10_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f27]) ).
fof(f144,plain,
~ empty(sK10_skl),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
! [A] :
( ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f146,plain,
! [A] :
( ( finite(sK11_skl(A))
& ~ empty(sK11_skl(A))
& element(sK11_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(B,sK11_skl(A))],[f145]) ).
fof(f149,plain,
! [X0] :
( finite(sK11_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f157,plain,
! [X0,X1] : subset(set_intersection2(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f158,plain,
! [A,B,C] :
( subset(A,set_intersection2(B,C))
| ~ subset(A,C)
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f159,plain,
! [X0,X1,X2] :
( subset(X0,set_intersection2(X1,X2))
| ~ subset(X0,X2)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f161,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
! [A,B] :
( subset(finite_subsets(A),finite_subsets(B))
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f163,plain,
! [X0,X1] :
( subset(finite_subsets(X0),finite_subsets(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
? [A,B] : finite_subsets(set_intersection2(A,B)) != set_intersection2(finite_subsets(A),finite_subsets(B)),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f165,plain,
finite_subsets(set_intersection2(sK13_skl,sK14_skl)) != set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f164]) ).
fof(f166,plain,
finite_subsets(set_intersection2(sK13_skl,sK14_skl)) != set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f168,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f169,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f170,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f171,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f173,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f188,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f62]) ).
fof(f193,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ in(X1,finite_subsets(X0))
| ~ preboolean(finite_subsets(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f85]) ).
fof(f195,plain,
! [X0,X1] :
( ~ finite(X1)
| ~ subset(X1,X0)
| in(X1,finite_subsets(X0))
| ~ preboolean(finite_subsets(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f87]) ).
fof(f196,plain,
! [X0,X1] :
( ~ finite(X0)
| ~ subset(X0,X1)
| in(X0,finite_subsets(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f195,f91]) ).
fof(f198,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,finite_subsets(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f193,f91]) ).
fof(f228,plain,
! [X0,X1] : subset(set_intersection2(X0,X1),X1),
inference(paramodulation,[status(thm)],[f59,f157]) ).
fof(f1902,definition,
( sQ2_spl
<=> subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1904,plain,
( sQ2_spl
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f1902]) ).
fof(f1905,definition,
( sQ3_spl
<=> subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1907,plain,
( sQ3_spl
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl)) ),
inference(component_clause,[status(thm)],[f1905]) ).
fof(f1911,plain,
( sQ3_spl
| ~ subset(set_intersection2(sK13_skl,sK14_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f1907,f163]) ).
fof(f1912,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1911,f228]) ).
fof(f1913,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1912]) ).
fof(f1914,plain,
( sQ2_spl
| ~ subset(set_intersection2(sK13_skl,sK14_skl),sK13_skl) ),
inference(resolution,[status(thm)],[f1904,f163]) ).
fof(f1915,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1914,f157]) ).
fof(f1916,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1915]) ).
fof(f2073,plain,
( ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK14_skl))
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl))
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(resolution,[status(thm)],[f78,f166]) ).
fof(f2077,definition,
( sQ4_spl
<=> in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2079,plain,
( sQ4_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f2077]) ).
fof(f2080,definition,
( sQ5_spl
<=> in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f2082,plain,
( sQ5_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2080]) ).
fof(f2083,definition,
( sQ6_spl
<=> in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
( sQ6_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK14_skl)) ),
inference(component_clause,[status(thm)],[f2083]) ).
fof(f2086,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f2073,f2077,f2080,f2083]) ).
fof(f2115,plain,
! [X0] :
( sQ6_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),X0)
| ~ subset(X0,finite_subsets(sK14_skl)) ),
inference(resolution,[status(thm)],[f2085,f69]) ).
fof(f2119,definition,
( sQ13_spl
<=> finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( ~ sQ13_spl
| finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) ),
inference(component_clause,[status(thm)],[f2119]) ).
fof(f2135,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2120,f166]) ).
fof(f2136,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f2135]) ).
fof(f2271,definition,
( sQ39_spl
<=> empty(finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f2272,plain,
( ~ sQ39_spl
| empty(finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f2271]) ).
fof(f2275,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2272,f108]) ).
fof(f2276,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f2275]) ).
fof(f2293,definition,
! [X0] :
( sQ41_spl
<=> ~ in(finite_subsets(sK13_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f2294,plain,
! [X0] :
( ~ sQ41_spl
| ~ in(finite_subsets(sK13_skl),X0) ),
inference(component_clause,[status(thm)],[f2293]) ).
fof(f2301,plain,
! [X0] :
( sQ5_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),X0)
| ~ subset(X0,finite_subsets(sK13_skl)) ),
inference(resolution,[status(thm)],[f2082,f69]) ).
fof(f2306,definition,
( sQ43_spl
<=> element(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2307,plain,
( ~ sQ43_spl
| element(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2306]) ).
fof(f2308,plain,
( sQ43_spl
| ~ element(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2306]) ).
fof(f2309,definition,
( sQ44_spl
<=> empty(finite_subsets(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f2310,plain,
( ~ sQ44_spl
| empty(finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2309]) ).
fof(f2313,plain,
( ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2310,f108]) ).
fof(f2314,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f2313]) ).
fof(f2343,plain,
! [X0] :
( ~ sQ41_spl
| empty(X0)
| ~ element(finite_subsets(sK13_skl),X0) ),
inference(resolution,[status(thm)],[f2294,f169]) ).
fof(f2359,definition,
! [X0] :
( sQ47_spl
<=> ~ in(finite_subsets(sK14_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2360,plain,
! [X0] :
( ~ sQ47_spl
| ~ in(finite_subsets(sK14_skl),X0) ),
inference(component_clause,[status(thm)],[f2359]) ).
fof(f2368,plain,
! [X0] :
( ~ sQ47_spl
| empty(X0)
| ~ element(finite_subsets(sK14_skl),X0) ),
inference(resolution,[status(thm)],[f2360,f169]) ).
fof(f2439,definition,
( sQ57_spl
<=> subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2441,plain,
( sQ57_spl
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f2439]) ).
fof(f2444,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2441,f188]) ).
fof(f2445,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f2444]) ).
fof(f2541,plain,
! [X0] :
( ~ sQ47_spl
| ~ element(finite_subsets(sK14_skl),powerset(X0)) ),
inference(resolution,[status(thm)],[f101,f2368]) ).
fof(f2542,plain,
! [X0] :
( ~ sQ41_spl
| ~ element(finite_subsets(sK13_skl),powerset(X0)) ),
inference(resolution,[status(thm)],[f101,f2343]) ).
fof(f2547,definition,
( sQ66_spl
<=> subset(sK13_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f2549,plain,
( sQ66_spl
| ~ subset(sK13_skl,sK13_skl) ),
inference(component_clause,[status(thm)],[f2547]) ).
fof(f2554,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2549,f188]) ).
fof(f2555,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f2554]) ).
fof(f2573,definition,
( sQ68_spl
<=> set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) = set_intersection2(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f2574,plain,
( ~ sQ68_spl
| set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) = set_intersection2(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f2573]) ).
fof(f2589,plain,
( ~ sQ68_spl
| set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) = finite_subsets(set_intersection2(sK13_skl,sK14_skl)) ),
inference(forward_demodulation,[status(thm)],[f113,f2574]) ).
fof(f2590,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2589,f166]) ).
fof(f2591,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f2590]) ).
fof(f2599,definition,
( sQ72_spl
<=> finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f2600,plain,
( ~ sQ72_spl
| finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
inference(component_clause,[status(thm)],[f2599]) ).
fof(f2608,plain,
( ~ sQ72_spl
| finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)) ),
inference(forward_demodulation,[status(thm)],[f113,f2600]) ).
fof(f2609,plain,
( ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2608,f166]) ).
fof(f2610,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f2609]) ).
fof(f2873,definition,
( sQ102_spl
<=> subset(sK14_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2875,plain,
( sQ102_spl
| ~ subset(sK14_skl,sK14_skl) ),
inference(component_clause,[status(thm)],[f2873]) ).
fof(f2877,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2875,f188]) ).
fof(f2878,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f2877]) ).
fof(f3235,definition,
( sQ120_spl
<=> subset(set_intersection2(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f3237,plain,
( sQ120_spl
| ~ subset(set_intersection2(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(component_clause,[status(thm)],[f3235]) ).
fof(f3267,plain,
( sQ120_spl
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(set_intersection2(sK13_skl,sK14_skl))) ),
inference(forward_demodulation,[status(thm)],[f113,f3237]) ).
fof(f3268,plain,
( sQ120_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3267,f188]) ).
fof(f3269,plain,
sQ120_spl,
inference(contradiction_clause,[status(thm)],[f3268]) ).
fof(f3296,plain,
( sQ5_spl
| in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl))
| finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK13_skl)) ),
inference(resolution,[status(thm)],[f2301,f79]) ).
fof(f3307,definition,
( sQ126_spl
<=> subset(finite_subsets(sK13_skl),finite_subsets(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f3309,plain,
( sQ126_spl
| ~ subset(finite_subsets(sK13_skl),finite_subsets(sK13_skl)) ),
inference(component_clause,[status(thm)],[f3307]) ).
fof(f3312,plain,
( sQ5_spl
| sQ13_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f3296,f1902,f2119,f2080]) ).
fof(f3313,plain,
( sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3309,f188]) ).
fof(f3314,plain,
sQ126_spl,
inference(contradiction_clause,[status(thm)],[f3313]) ).
fof(f3328,plain,
( sQ6_spl
| in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK14_skl))
| finite_subsets(set_intersection2(sK13_skl,sK14_skl)) = set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))
| ~ subset(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl)) ),
inference(resolution,[status(thm)],[f2115,f80]) ).
fof(f3336,definition,
( sQ127_spl
<=> subset(finite_subsets(sK14_skl),finite_subsets(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f3338,plain,
( sQ127_spl
| ~ subset(finite_subsets(sK14_skl),finite_subsets(sK14_skl)) ),
inference(component_clause,[status(thm)],[f3336]) ).
fof(f3344,plain,
( sQ6_spl
| sQ13_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f3328,f1905,f2119,f2083]) ).
fof(f3346,plain,
( sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3338,f188]) ).
fof(f3347,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f3346]) ).
fof(f3859,definition,
( sQ137_spl
<=> subset(set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f3861,plain,
( sQ137_spl
| ~ subset(set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl)),set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
inference(component_clause,[status(thm)],[f3859]) ).
fof(f3864,plain,
( sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3861,f188]) ).
fof(f3865,plain,
sQ137_spl,
inference(contradiction_clause,[status(thm)],[f3864]) ).
fof(f4782,plain,
( sQ43_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
inference(resolution,[status(thm)],[f161,f2308]) ).
fof(f4809,plain,
( sQ43_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f4782,f2080,f2306]) ).
fof(f5046,plain,
! [X0] : subset(empty_set,X0),
inference(paramodulation,[status(thm)],[f167,f157]) ).
fof(f5742,definition,
! [X0] :
( sQ196_spl
<=> ~ element(X0,set_intersection2(X0,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f5743,plain,
! [X0] :
( ~ sQ196_spl
| ~ element(X0,set_intersection2(X0,empty_set)) ),
inference(component_clause,[status(thm)],[f5742]) ).
fof(f5799,definition,
! [X0] :
( sQ198_spl
<=> ~ finite(X0) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f5800,plain,
! [X0] :
( ~ sQ198_spl
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f5799]) ).
fof(f5809,plain,
( ~ sQ198_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f139,f5800]) ).
fof(f5846,plain,
! [X0] :
( ~ sQ196_spl
| ~ element(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f167,f5743]) ).
fof(f5867,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f5809]) ).
fof(f6554,plain,
! [X0] :
( ~ sQ47_spl
| ~ subset(finite_subsets(sK14_skl),X0) ),
inference(resolution,[status(thm)],[f173,f2541]) ).
fof(f6555,plain,
! [X0] :
( ~ sQ41_spl
| ~ subset(finite_subsets(sK13_skl),X0) ),
inference(resolution,[status(thm)],[f173,f2542]) ).
fof(f6787,plain,
( ~ sQ47_spl
| $false ),
inference(resolution,[status(thm)],[f6554,f188]) ).
fof(f6788,definition,
! [X0] :
( sQ219_spl
<=> ~ subset(finite_subsets(sK14_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f6789,plain,
! [X0] :
( ~ sQ219_spl
| ~ subset(finite_subsets(sK14_skl),X0) ),
inference(component_clause,[status(thm)],[f6788]) ).
fof(f6792,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f6787]) ).
fof(f6811,plain,
( ~ sQ41_spl
| $false ),
inference(resolution,[status(thm)],[f6555,f188]) ).
fof(f6812,definition,
! [X0] :
( sQ220_spl
<=> ~ subset(finite_subsets(sK13_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f6813,plain,
! [X0] :
( ~ sQ220_spl
| ~ subset(finite_subsets(sK13_skl),X0) ),
inference(component_clause,[status(thm)],[f6812]) ).
fof(f6816,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f6811]) ).
fof(f6835,plain,
( ~ sQ219_spl
| $false ),
inference(resolution,[status(thm)],[f6789,f188]) ).
fof(f6837,plain,
~ sQ219_spl,
inference(contradiction_clause,[status(thm)],[f6835]) ).
fof(f6844,plain,
( ~ sQ220_spl
| $false ),
inference(resolution,[status(thm)],[f6813,f188]) ).
fof(f6846,plain,
~ sQ220_spl,
inference(contradiction_clause,[status(thm)],[f6844]) ).
fof(f6906,definition,
( sQ226_spl
<=> empty(powerset(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f6907,plain,
( ~ sQ226_spl
| empty(powerset(sK13_skl)) ),
inference(component_clause,[status(thm)],[f6906]) ).
fof(f6910,plain,
( ~ sQ226_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6907,f101]) ).
fof(f6911,plain,
~ sQ226_spl,
inference(contradiction_clause,[status(thm)],[f6910]) ).
fof(f6919,definition,
( sQ228_spl
<=> empty(powerset(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f6920,plain,
( ~ sQ228_spl
| empty(powerset(sK14_skl)) ),
inference(component_clause,[status(thm)],[f6919]) ).
fof(f6923,plain,
( ~ sQ228_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6920,f101]) ).
fof(f6924,plain,
~ sQ228_spl,
inference(contradiction_clause,[status(thm)],[f6923]) ).
fof(f7224,definition,
! [X0] :
( sQ246_spl
<=> ~ element(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f7225,plain,
! [X0] :
( ~ sQ246_spl
| ~ element(X0,empty_set) ),
inference(component_clause,[status(thm)],[f7224]) ).
fof(f8213,plain,
( ~ sQ196_spl
| $false ),
inference(resolution,[status(thm)],[f5846,f93]) ).
fof(f8216,plain,
~ sQ196_spl,
inference(contradiction_clause,[status(thm)],[f8213]) ).
fof(f8746,definition,
( sQ265_spl
<=> subset(empty_set,set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f8748,plain,
( sQ265_spl
| ~ subset(empty_set,set_intersection2(finite_subsets(sK13_skl),finite_subsets(sK14_skl))) ),
inference(component_clause,[status(thm)],[f8746]) ).
fof(f8757,plain,
( sQ265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8748,f5046]) ).
fof(f8758,plain,
sQ265_spl,
inference(contradiction_clause,[status(thm)],[f8757]) ).
fof(f8821,plain,
( ~ sQ246_spl
| $false ),
inference(resolution,[status(thm)],[f7225,f93]) ).
fof(f8824,plain,
~ sQ246_spl,
inference(contradiction_clause,[status(thm)],[f8821]) ).
fof(f9289,plain,
( sQ4_spl
| ~ finite(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)))
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),set_intersection2(sK13_skl,sK14_skl)) ),
inference(resolution,[status(thm)],[f196,f2079]) ).
fof(f9333,definition,
! [X0] :
( sQ280_spl
<=> ~ subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f9334,plain,
! [X0] :
( ~ sQ280_spl
| ~ subset(empty_set,X0) ),
inference(component_clause,[status(thm)],[f9333]) ).
fof(f9377,definition,
( sQ292_spl
<=> subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),set_intersection2(sK13_skl,sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f9379,plain,
( sQ292_spl
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),set_intersection2(sK13_skl,sK14_skl)) ),
inference(component_clause,[status(thm)],[f9377]) ).
fof(f9380,definition,
( sQ293_spl
<=> finite(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f9382,plain,
( sQ293_spl
| ~ finite(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl))) ),
inference(component_clause,[status(thm)],[f9380]) ).
fof(f9383,plain,
( sQ4_spl
| ~ sQ293_spl
| ~ sQ292_spl ),
inference(split_clause,[status(thm)],[f9289,f9377,f9380,f2077]) ).
fof(f9460,plain,
( ~ sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9334,f5046]) ).
fof(f9461,plain,
~ sQ280_spl,
inference(contradiction_clause,[status(thm)],[f9460]) ).
fof(f9474,plain,
! [X0] :
( sQ293_spl
| ~ element(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(X0)) ),
inference(resolution,[status(thm)],[f9382,f58]) ).
fof(f9476,plain,
( ~ sQ43_spl
| sQ293_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2307,f9474]) ).
fof(f9478,plain,
( ~ sQ43_spl
| sQ293_spl ),
inference(contradiction_clause,[status(thm)],[f9476]) ).
fof(f9479,plain,
( sQ292_spl
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK14_skl)
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK13_skl) ),
inference(resolution,[status(thm)],[f9379,f159]) ).
fof(f9483,definition,
( sQ305_spl
<=> subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition]) ).
fof(f9485,plain,
( sQ305_spl
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK13_skl) ),
inference(component_clause,[status(thm)],[f9483]) ).
fof(f9486,definition,
( sQ306_spl
<=> subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f9488,plain,
( sQ306_spl
| ~ subset(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),sK14_skl) ),
inference(component_clause,[status(thm)],[f9486]) ).
fof(f9489,plain,
( sQ292_spl
| ~ sQ306_spl
| ~ sQ305_spl ),
inference(split_clause,[status(thm)],[f9479,f9483,f9486,f9377]) ).
fof(f10205,definition,
! [X0] :
( sQ320_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f10206,plain,
! [X0] :
( ~ sQ320_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f10205]) ).
fof(f10216,plain,
( ~ sQ320_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f142,f10206]) ).
fof(f10321,plain,
~ sQ320_spl,
inference(contradiction_clause,[status(thm)],[f10216]) ).
fof(f10878,definition,
( sQ331_spl
<=> finite(sK11_skl(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f10880,plain,
( sQ331_spl
| ~ finite(sK11_skl(sK10_skl)) ),
inference(component_clause,[status(thm)],[f10878]) ).
fof(f10886,plain,
( sQ331_spl
| empty(sK10_skl) ),
inference(resolution,[status(thm)],[f10880,f149]) ).
fof(f10890,plain,
( sQ331_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10886,f144]) ).
fof(f10891,plain,
sQ331_spl,
inference(contradiction_clause,[status(thm)],[f10890]) ).
fof(f10897,definition,
( sQ333_spl
<=> finite(sK11_skl(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition]) ).
fof(f10899,plain,
( sQ333_spl
| ~ finite(sK11_skl(sK5_skl)) ),
inference(component_clause,[status(thm)],[f10897]) ).
fof(f10910,definition,
( sQ335_spl
<=> finite(sK11_skl(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f10912,plain,
( sQ335_spl
| ~ finite(sK11_skl(sK4_skl)) ),
inference(component_clause,[status(thm)],[f10910]) ).
fof(f11665,plain,
( sQ333_spl
| empty(sK5_skl) ),
inference(resolution,[status(thm)],[f10899,f149]) ).
fof(f11669,plain,
( sQ333_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11665,f118]) ).
fof(f11670,plain,
sQ333_spl,
inference(contradiction_clause,[status(thm)],[f11669]) ).
fof(f11720,plain,
( sQ335_spl
| empty(sK4_skl) ),
inference(resolution,[status(thm)],[f10912,f149]) ).
fof(f11724,plain,
( sQ335_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11720,f115]) ).
fof(f11725,plain,
sQ335_spl,
inference(contradiction_clause,[status(thm)],[f11724]) ).
fof(f11736,plain,
( sQ305_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK13_skl)) ),
inference(resolution,[status(thm)],[f9485,f198]) ).
fof(f11739,plain,
( sQ305_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f11736,f2080,f9483]) ).
fof(f11740,plain,
( sQ306_spl
| ~ in(sK1_skl(finite_subsets(set_intersection2(sK13_skl,sK14_skl)),finite_subsets(sK14_skl),finite_subsets(sK13_skl)),finite_subsets(sK14_skl)) ),
inference(resolution,[status(thm)],[f9488,f198]) ).
fof(f11743,plain,
( sQ306_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f11740,f2083,f9486]) ).
fof(f11744,plain,
$false,
inference(sat_refutation,[status(thm)],[f1913,f1916,f2086,f2136,f2276,f2314,f2445,f2555,f2591,f2610,f2878,f3269,f3312,f3314,f3344,f3347,f3865,f4809,f5867,f6792,f6816,f6837,f6846,f6911,f6924,f8216,f8758,f8824,f9383,f9461,f9478,f9489,f10321,f10891,f11670,f11725,f11739,f11743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU111+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n016.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Mon Sep 21 05:55:24 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.43 % Drodi V4.1.1
% 69.98/9.42 % Refutation found
% 69.98/9.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 69.98/9.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 70.85/9.52 % Elapsed time: 9.084307 seconds
% 70.85/9.52 % CPU time: 71.344302 seconds
% 70.85/9.52 % Total memory used: 413.252 MB
% 70.85/9.52 % Net memory used: 370.245 MB
%------------------------------------------------------------------------------