%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU307+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:20:07 PM UTC 2026
% Result : Theorem 66.59s 9.06s
% Output : CNFRefutation 66.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 109
% Syntax : Number of formulae : 508 ( 160 unt; 66 def)
% Number of atoms : 1243 ( 200 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 1203 ( 468 ~; 427 |; 194 &)
% ( 89 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 96 ( 94 usr; 67 prp; 0-3 aty)
% Number of functors : 54 ( 54 usr; 12 con; 0-3 aty)
% Number of variables : 421 ( 393 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] : succ(A) = set_union2(A,singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = B
| D = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B,C] :
( C = set_union2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
| in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A] : cast_to_subset(A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A] :
( A = omega
<=> ( ! [B] :
( ordinal(B)
=> ( ( being_limit_ordinal(B)
& in(empty_set,B) )
=> subset(A,B) ) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [A] :
( relation(A)
=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [A] :
( one_sorted_str(A)
=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [A] : element(cast_to_subset(A),powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,axiom,
! [A] :
( meet_semilatt_str(A)
=> ( relation_of2_as_subset(the_L_meet(A),cartesian_product2(the_carrier(A),the_carrier(A)),the_carrier(A))
& quasi_total(the_L_meet(A),cartesian_product2(the_carrier(A),the_carrier(A)),the_carrier(A))
& function(the_L_meet(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
? [A] : meet_semilatt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
? [A] : join_semilatt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,axiom,
? [A] : latt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,axiom,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,lemma,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( in(C,B)
=> in(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f259,axiom,
? [A] :
( being_limit_ordinal(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,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/sandbox/benchmark/theBenchmark.p') ).
fof(f266,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,axiom,
! [A,B,C] :
( ( element(C,powerset(A))
& element(B,powerset(A)) )
=> subset_intersection2(A,B,C) = set_intersection2(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f347,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_intersection2(the_carrier(A),B,cast_as_carrier_subset(A)) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f348,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_intersection2(the_carrier(A),B,cast_as_carrier_subset(A)) = B ) ),
inference(negated_conjecture,[status(cth)],[f347]) ).
fof(f363,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f364,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f392,lemma,
! [A,B] :
( subset(A,B)
=> set_intersection2(A,B) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f453,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f462,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f491,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f492,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f593,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f613,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f614,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)],[f613]) ).
fof(f615,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f614]) ).
fof(f733,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f752,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f753,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f752]) ).
fof(f754,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f753]) ).
fof(f755,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK28_skl(B,A),D)
| ~ in(D,A) )
| in(sK28_skl(B,A),B) )
& ( ( ~ in(sK28_skl(B,A),sK29_skl(B,A))
& in(sK29_skl(B,A),A) )
| ~ in(sK28_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK27_skl(C,B,A))
& in(sK27_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl,sK29_skl]),skolemize(D,sK27_skl(C,B,A)),skolemize(C,sK28_skl(B,A)),skolemize(D,sK29_skl(B,A))],[f754]) ).
fof(f762,plain,
! [X0,X1] :
( X1 = empty_set
| X1 != set_meet(X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f755]) ).
fof(f792,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f64]) ).
fof(f793,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f792]) ).
fof(f794,plain,
( ! [A] :
( in(sK34_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(B,sK34_skl(A))],[f793]) ).
fof(f795,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f794]) ).
fof(f797,plain,
! [A,B] :
( ( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ( ! [C] :
( ( ~ subset(C,A)
| in(C,B) )
& ( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f798,plain,
( ! [A,B] :
( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(miniscoping,[status(thm)],[f797]) ).
fof(f799,plain,
( ! [A,B] :
( ( ( subset(sK35_skl(B,A),A)
| in(sK35_skl(B,A),B) )
& ( ~ subset(sK35_skl(B,A),A)
| ~ in(sK35_skl(B,A),B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(C,sK35_skl(B,A))],[f798]) ).
fof(f800,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f799]) ).
fof(f801,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f799]) ).
fof(f828,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f829,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f828]) ).
fof(f830,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f829]) ).
fof(f831,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f830]) ).
fof(f835,plain,
! [A,B,C] :
( ( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ( ! [D] :
( ( ( D != B
& D != A )
| in(D,C) )
& ( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f836,plain,
( ! [A,B,C] :
( ? [D] :
( ( D = B
| D = A
| in(D,C) )
& ( ( D != B
& D != A )
| ~ in(D,C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(miniscoping,[status(thm)],[f835]) ).
fof(f837,plain,
( ! [A,B,C] :
( ( ( sK41_skl(C,B,A) = B
| sK41_skl(C,B,A) = A
| in(sK41_skl(C,B,A),C) )
& ( ( sK41_skl(C,B,A) != B
& sK41_skl(C,B,A) != A )
| ~ in(sK41_skl(C,B,A),C) ) )
| C = unordered_pair(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( D != B
& D != A )
| in(D,C) )
& ! [D] :
( D = B
| D = A
| ~ in(D,C) ) )
| C != unordered_pair(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(D,sK41_skl(C,B,A))],[f836]) ).
fof(f839,plain,
! [X0,X1,X2,X3] :
( X3 != X1
| in(X3,X0)
| X0 != unordered_pair(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f837]) ).
fof(f852,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_union2(A,B) )
& ( ! [D] :
( ( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f73]) ).
fof(f853,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_union2(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_union2(A,B) ) ),
inference(miniscoping,[status(thm)],[f852]) ).
fof(f854,plain,
( ! [A,B,C] :
( ( ( in(sK44_skl(C,B,A),B)
| in(sK44_skl(C,B,A),A)
| in(sK44_skl(C,B,A),C) )
& ( ( ~ in(sK44_skl(C,B,A),B)
& ~ in(sK44_skl(C,B,A),A) )
| ~ in(sK44_skl(C,B,A),C) ) )
| C = set_union2(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_union2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl]),skolemize(D,sK44_skl(C,B,A))],[f853]) ).
fof(f856,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X1)
| in(X3,X0)
| X0 != set_union2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f854]) ).
fof(f884,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f885,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f884]) ).
fof(f947,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f974,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_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f90]) ).
fof(f975,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_difference(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_difference(A,B) ) ),
inference(miniscoping,[status(thm)],[f974]) ).
fof(f976,plain,
( ! [A,B,C] :
( ( ( ( ~ in(sK67_skl(C,B,A),B)
& in(sK67_skl(C,B,A),A) )
| in(sK67_skl(C,B,A),C) )
& ( in(sK67_skl(C,B,A),B)
| ~ in(sK67_skl(C,B,A),A)
| ~ in(sK67_skl(C,B,A),C) ) )
| C = set_difference(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_difference(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(D,sK67_skl(C,B,A))],[f975]) ).
fof(f978,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f976]) ).
fof(f993,plain,
! [A] :
( A = omega
<=> ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f994,plain,
! [A] :
( ( ? [B] :
( ~ subset(A,B)
& being_limit_ordinal(B)
& in(empty_set,B)
& ordinal(B) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(NNF_transformation,[status(thm)],[f993]) ).
fof(f995,plain,
( ! [A] :
( ? [B] :
( ~ subset(A,B)
& being_limit_ordinal(B)
& in(empty_set,B)
& ordinal(B) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ! [A] :
( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(miniscoping,[status(thm)],[f994]) ).
fof(f996,plain,
( ! [A] :
( ( ~ subset(A,sK71_skl(A))
& being_limit_ordinal(sK71_skl(A))
& in(empty_set,sK71_skl(A))
& ordinal(sK71_skl(A)) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ! [A] :
( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71_skl]),skolemize(B,sK71_skl(A))],[f995]) ).
fof(f997,plain,
! [X0] :
( in(empty_set,X0)
| X0 != omega ),
inference(cnf_transformation,[status(thm)],[f996]) ).
fof(f999,plain,
! [X0] :
( ordinal(X0)
| X0 != omega ),
inference(cnf_transformation,[status(thm)],[f996]) ).
fof(f1013,plain,
! [A,B] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f1014,plain,
! [X0,X1] :
( subset_complement(X1,X0) = set_difference(X1,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1013]) ).
fof(f1029,plain,
! [A] :
( relation_field(A) = set_union2(relation_dom(A),relation_rng(A))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f1030,plain,
! [X0] :
( relation_field(X0) = set_union2(relation_dom(X0),relation_rng(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1029]) ).
fof(f1133,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f130]) ).
fof(f1134,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1133]) ).
fof(f1135,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f1141,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f139]) ).
fof(f1142,plain,
! [X0,X1] :
( element(subset_complement(X1,X0),powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1141]) ).
fof(f1174,plain,
! [A] :
( ( join_semilatt_str(A)
& meet_semilatt_str(A) )
| ~ latt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f162]) ).
fof(f1175,plain,
! [X0] :
( meet_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1176,plain,
! [X0] :
( join_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1179,plain,
! [A] :
( ( relation_of2_as_subset(the_L_meet(A),cartesian_product2(the_carrier(A),the_carrier(A)),the_carrier(A))
& quasi_total(the_L_meet(A),cartesian_product2(the_carrier(A),the_carrier(A)),the_carrier(A))
& function(the_L_meet(A)) )
| ~ meet_semilatt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f166]) ).
fof(f1180,plain,
! [X0] :
( function(the_L_meet(X0))
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f1187,plain,
meet_semilatt_str(sK93_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(A,sK93_skl)],[f169]) ).
fof(f1188,plain,
meet_semilatt_str(sK93_skl),
inference(cnf_transformation,[status(thm)],[f1187]) ).
fof(f1191,plain,
join_semilatt_str(sK95_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95_skl]),skolemize(A,sK95_skl)],[f171]) ).
fof(f1192,plain,
join_semilatt_str(sK95_skl),
inference(cnf_transformation,[status(thm)],[f1191]) ).
fof(f1193,plain,
latt_str(sK96_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96_skl]),skolemize(A,sK96_skl)],[f172]) ).
fof(f1194,plain,
latt_str(sK96_skl),
inference(cnf_transformation,[status(thm)],[f1193]) ).
fof(f1225,plain,
( ! [A] : finite(singleton(A))
& ! [A] : ~ empty(singleton(A)) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f1227,plain,
! [X0] : finite(singleton(X0)),
inference(cnf_transformation,[status(thm)],[f1225]) ).
fof(f1228,plain,
( ! [A] : preboolean(powerset(A))
& ! [A] : diff_closed(powerset(A))
& ! [A] : cup_closed(powerset(A))
& ! [A] : ~ empty(powerset(A)) ),
inference(miniscoping,[status(thm)],[f185]) ).
fof(f1229,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f1228]) ).
fof(f1237,plain,
epsilon_transitive(omega),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f1240,plain,
~ empty(omega),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f1354,plain,
v1_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1355,plain,
v2_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1356,plain,
v3_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1357,plain,
v4_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1358,plain,
v5_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1393,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f1420,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f243]) ).
fof(f1421,plain,
( ! [A,B] :
( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ! [A,B] :
( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(miniscoping,[status(thm)],[f1420]) ).
fof(f1423,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ),
inference(cnf_transformation,[status(thm)],[f1421]) ).
fof(f1424,plain,
! [A,B] :
( ! [C] :
( in(C,A)
| ~ in(C,B) )
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f244]) ).
fof(f1425,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1424]) ).
fof(f1495,plain,
( being_limit_ordinal(sK116_skl)
& ordinal(sK116_skl)
& epsilon_connected(sK116_skl)
& epsilon_transitive(sK116_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl]),skolemize(A,sK116_skl)],[f259]) ).
fof(f1496,plain,
epsilon_transitive(sK116_skl),
inference(cnf_transformation,[status(thm)],[f1495]) ).
fof(f1498,plain,
ordinal(sK116_skl),
inference(cnf_transformation,[status(thm)],[f1495]) ).
fof(f1514,plain,
! [A] :
( finite(sK121_skl(A))
& natural(sK121_skl(A))
& ordinal(sK121_skl(A))
& epsilon_connected(sK121_skl(A))
& epsilon_transitive(sK121_skl(A))
& one_to_one(sK121_skl(A))
& function(sK121_skl(A))
& relation(sK121_skl(A))
& empty(sK121_skl(A))
& element(sK121_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK121_skl]),skolemize(B,sK121_skl(A))],[f264]) ).
fof(f1516,plain,
! [X0] : empty(sK121_skl(X0)),
inference(cnf_transformation,[status(thm)],[f1514]) ).
fof(f1524,plain,
! [X0] : finite(sK121_skl(X0)),
inference(cnf_transformation,[status(thm)],[f1514]) ).
fof(f1529,plain,
( ordinal(sK123_skl)
& epsilon_connected(sK123_skl)
& epsilon_transitive(sK123_skl)
& empty(sK123_skl)
& one_to_one(sK123_skl)
& function(sK123_skl)
& relation(sK123_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(A,sK123_skl)],[f266]) ).
fof(f1530,plain,
relation(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1531,plain,
function(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1532,plain,
one_to_one(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1533,plain,
empty(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1536,plain,
ordinal(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1554,plain,
( one_to_one(sK129_skl)
& function(sK129_skl)
& relation(sK129_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK129_skl]),skolemize(A,sK129_skl)],[f272]) ).
fof(f1556,plain,
function(sK129_skl),
inference(cnf_transformation,[status(thm)],[f1554]) ).
fof(f1566,plain,
( ~ empty_carrier(sK132_skl)
& one_sorted_str(sK132_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132_skl]),skolemize(A,sK132_skl)],[f275]) ).
fof(f1568,plain,
~ empty_carrier(sK132_skl),
inference(cnf_transformation,[status(thm)],[f1566]) ).
fof(f1589,plain,
! [A,B,C] :
( subset_intersection2(A,B,C) = set_intersection2(B,C)
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f284]) ).
fof(f1590,plain,
! [X0,X1,X2] :
( subset_intersection2(X1,X0,X2) = set_intersection2(X0,X2)
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1589]) ).
fof(f2001,plain,
? [A] :
( ? [B] :
( subset_intersection2(the_carrier(A),B,cast_as_carrier_subset(A)) != B
& element(B,powerset(the_carrier(A))) )
& one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f348]) ).
fof(f2002,plain,
( subset_intersection2(the_carrier(sK251_skl),sK252_skl,cast_as_carrier_subset(sK251_skl)) != sK252_skl
& element(sK252_skl,powerset(the_carrier(sK251_skl)))
& one_sorted_str(sK251_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251_skl,sK252_skl]),skolemize(A,sK251_skl),skolemize(B,sK252_skl)],[f2001]) ).
fof(f2003,plain,
one_sorted_str(sK251_skl),
inference(cnf_transformation,[status(thm)],[f2002]) ).
fof(f2004,plain,
element(sK252_skl,powerset(the_carrier(sK251_skl))),
inference(cnf_transformation,[status(thm)],[f2002]) ).
fof(f2005,plain,
subset_intersection2(the_carrier(sK251_skl),sK252_skl,cast_as_carrier_subset(sK251_skl)) != sK252_skl,
inference(cnf_transformation,[status(thm)],[f2002]) ).
fof(f2054,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f2055,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f364]) ).
fof(f2056,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2055]) ).
fof(f2147,plain,
! [A,B] :
( set_intersection2(A,B) = A
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f392]) ).
fof(f2148,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2147]) ).
fof(f2341,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f2342,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f2370,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f462]) ).
fof(f2371,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f2370]) ).
fof(f2810,definition,
! [X1] :
( sQ1_spl
<=> ~ ordinal(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f2811,plain,
! [X0] :
( ~ sQ1_spl
| ~ ordinal(X0) ),
inference(component_clause,[status(thm)],[f2810]) ).
fof(f2936,definition,
( sQ31_spl
<=> in(empty_set,omega) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f2938,plain,
( sQ31_spl
| ~ in(empty_set,omega) ),
inference(component_clause,[status(thm)],[f2936]) ).
fof(f3059,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f615]) ).
fof(f3089,plain,
set_meet(empty_set) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f762]) ).
fof(f3103,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f795]) ).
fof(f3104,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f800]) ).
fof(f3105,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f801]) ).
fof(f3110,plain,
! [X0,X1] : in(X0,unordered_pair(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f839]) ).
fof(f3113,plain,
! [X0,X1,X2] :
( ~ in(X0,X1)
| in(X0,set_union2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f856]) ).
fof(f3130,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| ~ in(X0,set_difference(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f978]) ).
fof(f3135,plain,
in(empty_set,omega),
inference(destructive_equality_resolution,[status(thm)],[f997]) ).
fof(f3137,plain,
ordinal(omega),
inference(destructive_equality_resolution,[status(thm)],[f999]) ).
fof(f3254,plain,
cast_as_carrier_subset(sK251_skl) = the_carrier(sK251_skl),
inference(resolution,[status(thm)],[f885,f2003]) ).
fof(f3257,plain,
subset_intersection2(the_carrier(sK251_skl),sK252_skl,the_carrier(sK251_skl)) != sK252_skl,
inference(backward_demodulation,[status(thm)],[f3254,f2005]) ).
fof(f3259,definition,
( sQ57_spl
<=> one_sorted_str(sK251_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f3261,plain,
( sQ57_spl
| ~ one_sorted_str(sK251_skl) ),
inference(component_clause,[status(thm)],[f3259]) ).
fof(f3266,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3261,f2003]) ).
fof(f3267,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f3266]) ).
fof(f3299,plain,
! [X0,X1] :
( ~ one_sorted_str(X1)
| subset_intersection2(the_carrier(X1),X0,cast_as_carrier_subset(X1)) = set_intersection2(X0,cast_as_carrier_subset(X1))
| ~ element(X0,powerset(the_carrier(X1))) ),
inference(resolution,[status(thm)],[f1590,f1134]) ).
fof(f3385,plain,
( ~ one_sorted_str(sK251_skl)
| subset_intersection2(the_carrier(sK251_skl),sK252_skl,cast_as_carrier_subset(sK251_skl)) = set_intersection2(sK252_skl,cast_as_carrier_subset(sK251_skl)) ),
inference(resolution,[status(thm)],[f3299,f2004]) ).
fof(f3392,definition,
( sQ70_spl
<=> subset_intersection2(the_carrier(sK251_skl),sK252_skl,cast_as_carrier_subset(sK251_skl)) = set_intersection2(sK252_skl,cast_as_carrier_subset(sK251_skl)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3393,plain,
( ~ sQ70_spl
| subset_intersection2(the_carrier(sK251_skl),sK252_skl,cast_as_carrier_subset(sK251_skl)) = set_intersection2(sK252_skl,cast_as_carrier_subset(sK251_skl)) ),
inference(component_clause,[status(thm)],[f3392]) ).
fof(f3395,plain,
( ~ sQ57_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f3385,f3392,f3259]) ).
fof(f3399,plain,
( ~ sQ70_spl
| subset_intersection2(the_carrier(sK251_skl),sK252_skl,the_carrier(sK251_skl)) = set_intersection2(sK252_skl,cast_as_carrier_subset(sK251_skl)) ),
inference(forward_demodulation,[status(thm)],[f3254,f3393]) ).
fof(f3400,plain,
( ~ sQ70_spl
| subset_intersection2(the_carrier(sK251_skl),sK252_skl,the_carrier(sK251_skl)) = set_intersection2(sK252_skl,the_carrier(sK251_skl)) ),
inference(forward_demodulation,[status(thm)],[f3254,f3399]) ).
fof(f3657,plain,
( ~ sQ70_spl
| set_intersection2(sK252_skl,the_carrier(sK251_skl)) != sK252_skl ),
inference(backward_demodulation,[status(thm)],[f3400,f3257]) ).
fof(f8327,plain,
! [X0] :
( in(empty_set,X0)
| ~ element(omega,powerset(X0)) ),
inference(resolution,[status(thm)],[f3135,f1425]) ).
fof(f8379,plain,
meet_semilatt_str(sK96_skl),
inference(resolution,[status(thm)],[f1175,f1194]) ).
fof(f8514,plain,
join_semilatt_str(sK96_skl),
inference(resolution,[status(thm)],[f1176,f1194]) ).
fof(f8850,definition,
! [X0] :
( sQ211_spl
<=> ( in(sK27_skl(X0,set_meet(empty_set),empty_set),empty_set)
| in(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f8851,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,set_meet(empty_set),empty_set),empty_set)
| in(X0,empty_set) ),
inference(component_clause,[status(thm)],[f8850]) ).
fof(f9606,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f593,f2054]) ).
fof(f10916,plain,
! [X0] : sK121_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f2371,f1516]) ).
fof(f10917,plain,
sK123_skl = empty_set,
inference(resolution,[status(thm)],[f2371,f1533]) ).
fof(f10925,plain,
relation_rng(empty_set) = sK123_skl,
inference(backward_demodulation,[status(thm)],[f10917,f2342]) ).
fof(f10926,plain,
relation_dom(empty_set) = sK123_skl,
inference(backward_demodulation,[status(thm)],[f10917,f2341]) ).
fof(f10933,plain,
! [X0] :
( in(sK123_skl,X0)
| ~ element(omega,powerset(X0)) ),
inference(backward_demodulation,[status(thm)],[f10917,f8327]) ).
fof(f10942,plain,
set_meet(empty_set) = sK123_skl,
inference(backward_demodulation,[status(thm)],[f10917,f3089]) ).
fof(f10948,plain,
! [X0] : singleton(X0) != sK123_skl,
inference(backward_demodulation,[status(thm)],[f10917,f1393]) ).
fof(f10949,plain,
! [X0] : ~ in(X0,sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f3103]) ).
fof(f10951,plain,
v5_membered(sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f1358]) ).
fof(f10952,plain,
v4_membered(sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f1357]) ).
fof(f10953,plain,
v3_membered(sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f1356]) ).
fof(f10954,plain,
v2_membered(sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f1355]) ).
fof(f10955,plain,
v1_membered(sK123_skl),
inference(backward_demodulation,[status(thm)],[f10917,f1354]) ).
fof(f10964,plain,
relation_rng(sK123_skl) = sK123_skl,
inference(forward_demodulation,[status(thm)],[f10917,f10925]) ).
fof(f10965,plain,
relation_dom(sK123_skl) = sK123_skl,
inference(forward_demodulation,[status(thm)],[f10917,f10926]) ).
fof(f10966,plain,
set_meet(sK123_skl) = sK123_skl,
inference(forward_demodulation,[status(thm)],[f10917,f10942]) ).
fof(f10980,plain,
! [X0] : in(X0,powerset(X0)),
inference(resolution,[status(thm)],[f3105,f3059]) ).
fof(f11573,definition,
( sQ298_spl
<=> meet_semilatt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f11575,plain,
( sQ298_spl
| ~ meet_semilatt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f11573]) ).
fof(f11588,definition,
( sQ302_spl
<=> join_semilatt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f11590,plain,
( sQ302_spl
| ~ join_semilatt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f11588]) ).
fof(f11611,definition,
( sQ308_spl
<=> empty(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f11613,plain,
( sQ308_spl
| ~ empty(sK123_skl) ),
inference(component_clause,[status(thm)],[f11611]) ).
fof(f11790,plain,
( in(sK252_skl,powerset(the_carrier(sK251_skl)))
| empty(powerset(the_carrier(sK251_skl))) ),
inference(resolution,[status(thm)],[f831,f2004]) ).
fof(f11799,definition,
( sQ313_spl
<=> empty(powerset(the_carrier(sK251_skl))) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f11800,plain,
( ~ sQ313_spl
| empty(powerset(the_carrier(sK251_skl))) ),
inference(component_clause,[status(thm)],[f11799]) ).
fof(f11802,definition,
( sQ314_spl
<=> in(sK252_skl,powerset(the_carrier(sK251_skl))) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f11803,plain,
( ~ sQ314_spl
| in(sK252_skl,powerset(the_carrier(sK251_skl))) ),
inference(component_clause,[status(thm)],[f11802]) ).
fof(f11805,plain,
( sQ314_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f11790,f11799,f11802]) ).
fof(f11808,plain,
( ~ sQ313_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11800,f1229]) ).
fof(f11809,plain,
~ sQ313_spl,
inference(contradiction_clause,[status(thm)],[f11808]) ).
fof(f11826,plain,
finite(sK123_skl),
inference(backward_demodulation,[status(thm)],[f11835,f1524]) ).
fof(f11835,plain,
! [X0] : sK121_skl(X0) = sK123_skl,
inference(forward_demodulation,[status(thm)],[f10917,f10916]) ).
fof(f11844,plain,
( ~ sQ314_spl
| subset(sK252_skl,the_carrier(sK251_skl)) ),
inference(resolution,[status(thm)],[f11803,f3104]) ).
fof(f11962,definition,
( sQ320_spl
<=> in(sK34_skl(sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f11963,plain,
( ~ sQ320_spl
| in(sK34_skl(sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f11962]) ).
fof(f11970,definition,
( sQ322_spl
<=> empty(powerset(sK123_skl)) ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f11971,plain,
( ~ sQ322_spl
| empty(powerset(sK123_skl)) ),
inference(component_clause,[status(thm)],[f11970]) ).
fof(f11977,plain,
( ~ sQ322_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11971,f1229]) ).
fof(f11978,plain,
~ sQ322_spl,
inference(contradiction_clause,[status(thm)],[f11977]) ).
fof(f12013,plain,
! [X0,X1] : ~ in(unordered_pair(X0,X1),X0),
inference(resolution,[status(thm)],[f3110,f492]) ).
fof(f12583,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11590,f8514]) ).
fof(f12584,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f12583]) ).
fof(f12585,plain,
( sQ298_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11575,f8379]) ).
fof(f12586,plain,
sQ298_spl,
inference(contradiction_clause,[status(thm)],[f12585]) ).
fof(f13008,plain,
in(sK123_skl,omega),
inference(forward_demodulation,[status(thm)],[f10917,f3135]) ).
fof(f13073,plain,
! [X0] : set_union2(sK123_skl,X0) = X0,
inference(forward_demodulation,[status(thm)],[f10917,f9606]) ).
fof(f13164,definition,
( sQ352_spl
<=> function(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f13166,plain,
( sQ352_spl
| ~ function(sK123_skl) ),
inference(component_clause,[status(thm)],[f13164]) ).
fof(f13195,plain,
( sQ352_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13166,f1531]) ).
fof(f13196,plain,
sQ352_spl,
inference(contradiction_clause,[status(thm)],[f13195]) ).
fof(f13298,definition,
! [X0,X1] :
( sQ363_spl
<=> ( in(X0,X1)
| ~ element(sK123_skl,powerset(X1))
| in(sK27_skl(X0,set_meet(sK123_skl),sK123_skl),sK123_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f13299,plain,
! [X0,X1] :
( ~ sQ363_spl
| in(X0,X1)
| ~ element(sK123_skl,powerset(X1))
| in(sK27_skl(X0,set_meet(sK123_skl),sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f13298]) ).
fof(f13302,plain,
! [X0,X1] :
( ~ sQ363_spl
| in(X0,X1)
| ~ element(sK123_skl,powerset(X1))
| in(sK27_skl(X0,sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10966,f13299]) ).
fof(f13303,plain,
! [X0,X1] :
( ~ sQ363_spl
| in(X1,X0)
| ~ element(sK123_skl,powerset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f13302,f10949]) ).
fof(f13620,plain,
( ~ sQ320_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11963,f10949]) ).
fof(f13621,plain,
~ sQ320_spl,
inference(contradiction_clause,[status(thm)],[f13620]) ).
fof(f13624,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11613,f1533]) ).
fof(f13625,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f13624]) ).
fof(f13707,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,set_meet(empty_set),empty_set),empty_set)
| in(X0,sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10917,f8851]) ).
fof(f13708,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,set_meet(sK123_skl),empty_set),empty_set)
| in(X0,sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10917,f13707]) ).
fof(f13709,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,sK123_skl,empty_set),empty_set)
| in(X0,sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10966,f13708]) ).
fof(f13710,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,sK123_skl,sK123_skl),empty_set)
| in(X0,sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10917,f13709]) ).
fof(f13711,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,sK123_skl,sK123_skl),sK123_skl)
| in(X0,sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10917,f13710]) ).
fof(f13712,plain,
! [X0] :
( ~ sQ211_spl
| in(sK27_skl(X0,sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f13711,f10949]) ).
fof(f13746,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3137,f2811]) ).
fof(f13870,definition,
( sQ375_spl
<=> empty_carrier(sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition]) ).
fof(f13871,plain,
( ~ sQ375_spl
| empty_carrier(sK132_skl) ),
inference(component_clause,[status(thm)],[f13870]) ).
fof(f13874,plain,
( ~ sQ375_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13871,f1568]) ).
fof(f13875,plain,
~ sQ375_spl,
inference(contradiction_clause,[status(thm)],[f13874]) ).
fof(f14202,definition,
( sQ390_spl
<=> function(sK129_skl) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f14204,plain,
( sQ390_spl
| ~ function(sK129_skl) ),
inference(component_clause,[status(thm)],[f14202]) ).
fof(f14214,plain,
( sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14204,f1556]) ).
fof(f14215,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f14214]) ).
fof(f14645,definition,
( sQ401_spl
<=> ordinal(omega) ),
introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition]) ).
fof(f14647,plain,
( sQ401_spl
| ~ ordinal(omega) ),
inference(component_clause,[status(thm)],[f14645]) ).
fof(f14655,definition,
( sQ404_spl
<=> ordinal(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f14657,plain,
( sQ404_spl
| ~ ordinal(sK116_skl) ),
inference(component_clause,[status(thm)],[f14655]) ).
fof(f14665,plain,
( sQ404_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14657,f1498]) ).
fof(f14666,plain,
sQ404_spl,
inference(contradiction_clause,[status(thm)],[f14665]) ).
fof(f14669,plain,
( sQ401_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14647,f3137]) ).
fof(f14670,plain,
sQ401_spl,
inference(contradiction_clause,[status(thm)],[f14669]) ).
fof(f14671,plain,
( sQ31_spl
| ~ in(sK123_skl,omega) ),
inference(forward_demodulation,[status(thm)],[f10917,f2938]) ).
fof(f14826,plain,
subset_complement(the_carrier(sK251_skl),sK252_skl) = set_difference(the_carrier(sK251_skl),sK252_skl),
inference(resolution,[status(thm)],[f1014,f2004]) ).
fof(f14831,plain,
! [X0,X1] :
( ~ in(X1,powerset(X0))
| subset_complement(X0,X1) = set_difference(X0,X1) ),
inference(resolution,[status(thm)],[f1014,f2056]) ).
fof(f14886,plain,
relation_field(sK123_skl) = set_union2(relation_dom(sK123_skl),relation_rng(sK123_skl)),
inference(resolution,[status(thm)],[f1030,f1530]) ).
fof(f14897,plain,
relation_field(sK123_skl) = set_union2(sK123_skl,relation_rng(sK123_skl)),
inference(forward_demodulation,[status(thm)],[f10965,f14886]) ).
fof(f14898,plain,
relation_field(sK123_skl) = relation_rng(sK123_skl),
inference(forward_demodulation,[status(thm)],[f13073,f14897]) ).
fof(f14899,plain,
relation_field(sK123_skl) = sK123_skl,
inference(forward_demodulation,[status(thm)],[f10964,f14898]) ).
fof(f14978,plain,
! [X0] : subset_complement(X0,X0) = set_difference(X0,X0),
inference(resolution,[status(thm)],[f14831,f10980]) ).
fof(f15025,definition,
! [X0] :
( sQ419_spl
<=> in(sK25_skl(sK252_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition]) ).
fof(f15026,plain,
! [X0] :
( ~ sQ419_spl
| in(sK25_skl(sK252_skl),X0) ),
inference(component_clause,[status(thm)],[f15025]) ).
fof(f15044,plain,
! [X0] :
( ~ sQ419_spl
| ~ in(sK25_skl(sK252_skl),X0) ),
inference(resolution,[status(thm)],[f15026,f3130]) ).
fof(f15098,plain,
( ~ sQ419_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15044,f15026]) ).
fof(f15099,plain,
~ sQ419_spl,
inference(contradiction_clause,[status(thm)],[f15098]) ).
fof(f15163,definition,
( sQ423_spl
<=> powerset(sK123_skl) = sK123_skl ),
introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition]) ).
fof(f15164,plain,
( ~ sQ423_spl
| powerset(sK123_skl) = sK123_skl ),
inference(component_clause,[status(thm)],[f15163]) ).
fof(f15214,plain,
( ~ sQ423_spl
| in(sK123_skl,sK123_skl) ),
inference(paramodulation,[status(thm)],[f15164,f10980]) ).
fof(f15336,definition,
! [X0] :
( sQ428_spl
<=> ( in(relation_dom(sK17_skl(X0)),sK123_skl)
| ~ finite(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f15337,plain,
! [X0] :
( ~ sQ428_spl
| in(relation_dom(sK17_skl(X0)),sK123_skl)
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f15336]) ).
fof(f15345,definition,
( sQ430_spl
<=> in(sK123_skl,sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f15346,plain,
( ~ sQ430_spl
| in(sK123_skl,sK123_skl) ),
inference(component_clause,[status(thm)],[f15345]) ).
fof(f15356,definition,
( sQ432_spl
<=> in(sK252_skl,sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f15357,plain,
( ~ sQ432_spl
| in(sK252_skl,sK123_skl) ),
inference(component_clause,[status(thm)],[f15356]) ).
fof(f15380,plain,
( ~ sQ423_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15214,f10949]) ).
fof(f15381,plain,
~ sQ423_spl,
inference(contradiction_clause,[status(thm)],[f15380]) ).
fof(f15382,plain,
( ~ sQ432_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15357,f10949]) ).
fof(f15383,plain,
~ sQ432_spl,
inference(contradiction_clause,[status(thm)],[f15382]) ).
fof(f15384,plain,
( ~ sQ430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15346,f10949]) ).
fof(f15385,plain,
~ sQ430_spl,
inference(contradiction_clause,[status(thm)],[f15384]) ).
fof(f15386,plain,
! [X0] :
( ~ sQ428_spl
| ~ finite(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15337,f10949]) ).
fof(f15387,plain,
( ~ sQ428_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f11826,f15386]) ).
fof(f15391,plain,
~ sQ428_spl,
inference(contradiction_clause,[status(thm)],[f15387]) ).
fof(f15796,definition,
( sQ439_spl
<=> empty(powerset(the_carrier(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f15797,plain,
( ~ sQ439_spl
| empty(powerset(the_carrier(sK132_skl))) ),
inference(component_clause,[status(thm)],[f15796]) ).
fof(f15805,plain,
( ~ sQ439_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15797,f1229]) ).
fof(f15806,plain,
~ sQ439_spl,
inference(contradiction_clause,[status(thm)],[f15805]) ).
fof(f15819,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14671,f13008]) ).
fof(f15820,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f15819]) ).
fof(f16091,definition,
( sQ466_spl
<=> in(sK33_skl(relation_field(sK123_skl),sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition]) ).
fof(f16092,plain,
( ~ sQ466_spl
| in(sK33_skl(relation_field(sK123_skl),sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f16091]) ).
fof(f16095,definition,
( sQ467_spl
<=> in(sK33_skl(sK123_skl,sK123_skl),relation_field(sK123_skl)) ),
introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition]) ).
fof(f16096,plain,
( ~ sQ467_spl
| in(sK33_skl(sK123_skl,sK123_skl),relation_field(sK123_skl)) ),
inference(component_clause,[status(thm)],[f16095]) ).
fof(f16099,definition,
( sQ468_spl
<=> in(sK32_skl(relation_field(sK123_skl),sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition]) ).
fof(f16100,plain,
( ~ sQ468_spl
| in(sK32_skl(relation_field(sK123_skl),sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f16099]) ).
fof(f16103,definition,
( sQ469_spl
<=> in(sK32_skl(sK123_skl,sK123_skl),relation_field(sK123_skl)) ),
introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition]) ).
fof(f16104,plain,
( ~ sQ469_spl
| in(sK32_skl(sK123_skl,sK123_skl),relation_field(sK123_skl)) ),
inference(component_clause,[status(thm)],[f16103]) ).
fof(f16129,plain,
( ~ sQ469_spl
| in(sK32_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f14899,f16104]) ).
fof(f16130,plain,
( ~ sQ469_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16129,f10949]) ).
fof(f16131,plain,
~ sQ469_spl,
inference(contradiction_clause,[status(thm)],[f16130]) ).
fof(f16132,plain,
( ~ sQ468_spl
| in(sK32_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f14899,f16100]) ).
fof(f16133,plain,
( ~ sQ468_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16132,f10949]) ).
fof(f16134,plain,
~ sQ468_spl,
inference(contradiction_clause,[status(thm)],[f16133]) ).
fof(f16135,plain,
( ~ sQ467_spl
| in(sK33_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f14899,f16096]) ).
fof(f16136,plain,
( ~ sQ467_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16135,f10949]) ).
fof(f16137,plain,
~ sQ467_spl,
inference(contradiction_clause,[status(thm)],[f16136]) ).
fof(f16138,plain,
( ~ sQ466_spl
| in(sK33_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f14899,f16092]) ).
fof(f16139,plain,
( ~ sQ466_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16138,f10949]) ).
fof(f16140,plain,
~ sQ466_spl,
inference(contradiction_clause,[status(thm)],[f16139]) ).
fof(f16179,definition,
( sQ480_spl
<=> empty(omega) ),
introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition]) ).
fof(f16180,plain,
( ~ sQ480_spl
| empty(omega) ),
inference(component_clause,[status(thm)],[f16179]) ).
fof(f16183,plain,
( ~ sQ480_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16180,f1240]) ).
fof(f16184,plain,
~ sQ480_spl,
inference(contradiction_clause,[status(thm)],[f16183]) ).
fof(f16583,definition,
( sQ487_spl
<=> empty(powerset(the_carrier(sK94_skl))) ),
introduced(definition,[new_symbols(definition,[sQ487_spl])],[split_symbol_definition]) ).
fof(f16584,plain,
( ~ sQ487_spl
| empty(powerset(the_carrier(sK94_skl))) ),
inference(component_clause,[status(thm)],[f16583]) ).
fof(f16592,plain,
( ~ sQ487_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16584,f1229]) ).
fof(f16593,plain,
~ sQ487_spl,
inference(contradiction_clause,[status(thm)],[f16592]) ).
fof(f16668,definition,
( sQ497_spl
<=> latt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition]) ).
fof(f16670,plain,
( sQ497_spl
| ~ latt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f16668]) ).
fof(f16677,plain,
( sQ497_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16670,f1194]) ).
fof(f16678,plain,
sQ497_spl,
inference(contradiction_clause,[status(thm)],[f16677]) ).
fof(f16735,definition,
( sQ506_spl
<=> epsilon_transitive(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f16737,plain,
( sQ506_spl
| ~ epsilon_transitive(sK116_skl) ),
inference(component_clause,[status(thm)],[f16735]) ).
fof(f16742,plain,
( sQ506_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16737,f1496]) ).
fof(f16743,plain,
sQ506_spl,
inference(contradiction_clause,[status(thm)],[f16742]) ).
fof(f17123,definition,
( sQ536_spl
<=> element(sK123_skl,powerset(the_carrier(sK251_skl))) ),
introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition]) ).
fof(f17125,plain,
( sQ536_spl
| ~ element(sK123_skl,powerset(the_carrier(sK251_skl))) ),
inference(component_clause,[status(thm)],[f17123]) ).
fof(f17174,definition,
( sQ542_spl
<=> join_semilatt_str(sK95_skl) ),
introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition]) ).
fof(f17176,plain,
( sQ542_spl
| ~ join_semilatt_str(sK95_skl) ),
inference(component_clause,[status(thm)],[f17174]) ).
fof(f17202,plain,
( sQ542_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17176,f1192]) ).
fof(f17203,plain,
sQ542_spl,
inference(contradiction_clause,[status(thm)],[f17202]) ).
fof(f17658,definition,
( sQ570_spl
<=> meet_semilatt_str(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition]) ).
fof(f17660,plain,
( sQ570_spl
| ~ meet_semilatt_str(sK93_skl) ),
inference(component_clause,[status(thm)],[f17658]) ).
fof(f17701,plain,
( sQ570_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17660,f1188]) ).
fof(f17702,plain,
sQ570_spl,
inference(contradiction_clause,[status(thm)],[f17701]) ).
fof(f17782,plain,
( ~ sQ211_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13712,f10949]) ).
fof(f17783,plain,
~ sQ211_spl,
inference(contradiction_clause,[status(thm)],[f17782]) ).
fof(f17786,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f947,f1135]) ).
fof(f17787,plain,
in(sK123_skl,omega),
inference(resolution,[status(thm)],[f17786,f10933]) ).
fof(f18274,plain,
element(subset_complement(the_carrier(sK251_skl),sK252_skl),powerset(the_carrier(sK251_skl))),
inference(resolution,[status(thm)],[f1142,f2004]) ).
fof(f18278,plain,
! [X0] : element(subset_complement(X0,X0),powerset(X0)),
inference(resolution,[status(thm)],[f1142,f17786]) ).
fof(f18280,plain,
element(set_difference(the_carrier(sK251_skl),sK252_skl),powerset(the_carrier(sK251_skl))),
inference(forward_demodulation,[status(thm)],[f14826,f18274]) ).
fof(f18281,plain,
! [X0] : element(set_difference(X0,X0),powerset(X0)),
inference(forward_demodulation,[status(thm)],[f14978,f18278]) ).
fof(f18608,plain,
! [X0] : in(sK123_skl,set_union2(omega,X0)),
inference(resolution,[status(thm)],[f17787,f3113]) ).
fof(f18880,plain,
function(the_L_meet(sK93_skl)),
inference(resolution,[status(thm)],[f1180,f1188]) ).
fof(f19059,definition,
( sQ594_spl
<=> in(ordered_pair(sK91_skl(sK123_skl,sK123_skl),sK90_skl(sK123_skl,sK123_skl)),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition]) ).
fof(f19060,plain,
( ~ sQ594_spl
| in(ordered_pair(sK91_skl(sK123_skl,sK123_skl),sK90_skl(sK123_skl,sK123_skl)),sK123_skl) ),
inference(component_clause,[status(thm)],[f19059]) ).
fof(f19063,definition,
( sQ595_spl
<=> in(ordered_pair(sK89_skl(sK123_skl,sK123_skl),sK91_skl(sK123_skl,sK123_skl)),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition]) ).
fof(f19064,plain,
( ~ sQ595_spl
| in(ordered_pair(sK89_skl(sK123_skl,sK123_skl),sK91_skl(sK123_skl,sK123_skl)),sK123_skl) ),
inference(component_clause,[status(thm)],[f19063]) ).
fof(f19067,definition,
( sQ596_spl
<=> in(sK90_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f19068,plain,
( ~ sQ596_spl
| in(sK90_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19067]) ).
fof(f19071,definition,
( sQ597_spl
<=> in(sK91_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ597_spl])],[split_symbol_definition]) ).
fof(f19072,plain,
( ~ sQ597_spl
| in(sK91_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19071]) ).
fof(f19075,definition,
( sQ598_spl
<=> in(sK89_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ598_spl])],[split_symbol_definition]) ).
fof(f19076,plain,
( ~ sQ598_spl
| in(sK89_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19075]) ).
fof(f19083,plain,
( ~ sQ598_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19076,f10949]) ).
fof(f19084,plain,
~ sQ598_spl,
inference(contradiction_clause,[status(thm)],[f19083]) ).
fof(f19085,plain,
( ~ sQ597_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19072,f10949]) ).
fof(f19086,plain,
~ sQ597_spl,
inference(contradiction_clause,[status(thm)],[f19085]) ).
fof(f19087,plain,
( ~ sQ596_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19068,f10949]) ).
fof(f19088,plain,
~ sQ596_spl,
inference(contradiction_clause,[status(thm)],[f19087]) ).
fof(f19089,plain,
( ~ sQ595_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19064,f10949]) ).
fof(f19090,plain,
~ sQ595_spl,
inference(contradiction_clause,[status(thm)],[f19089]) ).
fof(f19091,plain,
( ~ sQ594_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19060,f10949]) ).
fof(f19092,plain,
~ sQ594_spl,
inference(contradiction_clause,[status(thm)],[f19091]) ).
fof(f19097,definition,
( sQ600_spl
<=> in(sK76_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f19098,plain,
( ~ sQ600_spl
| in(sK76_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19097]) ).
fof(f19101,definition,
( sQ601_spl
<=> in(sK75_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f19102,plain,
( ~ sQ601_spl
| in(sK75_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19101]) ).
fof(f19106,plain,
( ~ sQ600_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19098,f10949]) ).
fof(f19107,plain,
~ sQ600_spl,
inference(contradiction_clause,[status(thm)],[f19106]) ).
fof(f19108,plain,
( ~ sQ601_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19102,f10949]) ).
fof(f19109,plain,
~ sQ601_spl,
inference(contradiction_clause,[status(thm)],[f19108]) ).
fof(f19168,definition,
( sQ602_spl
<=> in(ordered_pair(sK62_skl(sK123_skl,sK123_skl),sK61_skl(sK123_skl,sK123_skl)),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition]) ).
fof(f19169,plain,
( ~ sQ602_spl
| in(ordered_pair(sK62_skl(sK123_skl,sK123_skl),sK61_skl(sK123_skl,sK123_skl)),sK123_skl) ),
inference(component_clause,[status(thm)],[f19168]) ).
fof(f19172,definition,
( sQ603_spl
<=> in(ordered_pair(sK61_skl(sK123_skl,sK123_skl),sK62_skl(sK123_skl,sK123_skl)),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ603_spl])],[split_symbol_definition]) ).
fof(f19173,plain,
( ~ sQ603_spl
| in(ordered_pair(sK61_skl(sK123_skl,sK123_skl),sK62_skl(sK123_skl,sK123_skl)),sK123_skl) ),
inference(component_clause,[status(thm)],[f19172]) ).
fof(f19176,definition,
( sQ604_spl
<=> in(sK62_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition]) ).
fof(f19177,plain,
( ~ sQ604_spl
| in(sK62_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19176]) ).
fof(f19180,definition,
( sQ605_spl
<=> in(sK61_skl(sK123_skl,sK123_skl),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition]) ).
fof(f19181,plain,
( ~ sQ605_spl
| in(sK61_skl(sK123_skl,sK123_skl),sK123_skl) ),
inference(component_clause,[status(thm)],[f19180]) ).
fof(f19184,plain,
( ~ sQ605_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19181,f10949]) ).
fof(f19185,plain,
~ sQ605_spl,
inference(contradiction_clause,[status(thm)],[f19184]) ).
fof(f19186,plain,
( ~ sQ604_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19177,f10949]) ).
fof(f19187,plain,
~ sQ604_spl,
inference(contradiction_clause,[status(thm)],[f19186]) ).
fof(f19188,plain,
( ~ sQ603_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19173,f10949]) ).
fof(f19189,plain,
~ sQ603_spl,
inference(contradiction_clause,[status(thm)],[f19188]) ).
fof(f19190,plain,
( ~ sQ602_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19169,f10949]) ).
fof(f19191,plain,
~ sQ602_spl,
inference(contradiction_clause,[status(thm)],[f19190]) ).
fof(f19246,definition,
( sQ607_spl
<=> epsilon_transitive(omega) ),
introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition]) ).
fof(f19248,plain,
( sQ607_spl
| ~ epsilon_transitive(omega) ),
inference(component_clause,[status(thm)],[f19246]) ).
fof(f19253,plain,
( sQ607_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19248,f1237]) ).
fof(f19254,plain,
sQ607_spl,
inference(contradiction_clause,[status(thm)],[f19253]) ).
fof(f19836,definition,
! [X0] :
( sQ617_spl
<=> ~ v1_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f19837,plain,
! [X0] :
( ~ sQ617_spl
| ~ v1_membered(X0) ),
inference(component_clause,[status(thm)],[f19836]) ).
fof(f19892,plain,
( ~ sQ617_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f10955,f19837]) ).
fof(f19900,plain,
~ sQ617_spl,
inference(contradiction_clause,[status(thm)],[f19892]) ).
fof(f19905,definition,
! [X0] :
( sQ620_spl
<=> ~ v2_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f19906,plain,
! [X0] :
( ~ sQ620_spl
| ~ v2_membered(X0) ),
inference(component_clause,[status(thm)],[f19905]) ).
fof(f19938,definition,
( sQ623_spl
<=> function(the_L_meet(sK93_skl)) ),
introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition]) ).
fof(f19940,plain,
( sQ623_spl
| ~ function(the_L_meet(sK93_skl)) ),
inference(component_clause,[status(thm)],[f19938]) ).
fof(f19964,plain,
( ~ sQ620_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f10954,f19906]) ).
fof(f19971,plain,
~ sQ620_spl,
inference(contradiction_clause,[status(thm)],[f19964]) ).
fof(f20095,definition,
! [X0] :
( sQ637_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition]) ).
fof(f20096,plain,
! [X0] :
( ~ sQ637_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f20095]) ).
fof(f20187,definition,
! [X0] :
( sQ638_spl
<=> ~ v3_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f20188,plain,
! [X0] :
( ~ sQ638_spl
| ~ v3_membered(X0) ),
inference(component_clause,[status(thm)],[f20187]) ).
fof(f20334,plain,
( ~ sQ638_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f10953,f20188]) ).
fof(f20340,plain,
~ sQ638_spl,
inference(contradiction_clause,[status(thm)],[f20334]) ).
fof(f20351,definition,
! [X0] :
( sQ645_spl
<=> ~ v4_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition]) ).
fof(f20352,plain,
! [X0] :
( ~ sQ645_spl
| ~ v4_membered(X0) ),
inference(component_clause,[status(thm)],[f20351]) ).
fof(f20455,definition,
( sQ652_spl
<=> one_to_one(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition]) ).
fof(f20457,plain,
( sQ652_spl
| ~ one_to_one(sK123_skl) ),
inference(component_clause,[status(thm)],[f20455]) ).
fof(f20462,plain,
( sQ652_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20457,f1532]) ).
fof(f20463,plain,
sQ652_spl,
inference(contradiction_clause,[status(thm)],[f20462]) ).
fof(f20481,definition,
( sQ656_spl
<=> v4_membered(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f20483,plain,
( sQ656_spl
| ~ v4_membered(sK123_skl) ),
inference(component_clause,[status(thm)],[f20481]) ).
fof(f20485,plain,
( sQ656_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20483,f10952]) ).
fof(f20486,plain,
sQ656_spl,
inference(contradiction_clause,[status(thm)],[f20485]) ).
fof(f21113,plain,
in(sK123_skl,succ(omega)),
inference(paramodulation,[status(thm)],[f733,f18608]) ).
fof(f21767,plain,
( ~ sQ645_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f10952,f20352]) ).
fof(f21772,plain,
~ sQ645_spl,
inference(contradiction_clause,[status(thm)],[f21767]) ).
fof(f22274,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_difference(X0,X1) = sK123_skl ),
inference(forward_demodulation,[status(thm)],[f10917,f1423]) ).
fof(f22289,plain,
! [X0] : set_difference(X0,X0) = sK123_skl,
inference(resolution,[status(thm)],[f22274,f3059]) ).
fof(f22640,plain,
! [X0] : element(sK123_skl,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f22289,f18281]) ).
fof(f22874,definition,
! [X0] :
( sQ702_spl
<=> in(sK34_skl(sK123_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f22875,plain,
! [X0] :
( ~ sQ702_spl
| in(sK34_skl(sK123_skl),X0) ),
inference(component_clause,[status(thm)],[f22874]) ).
fof(f22897,definition,
! [X0] :
( sQ704_spl
<=> sK123_skl = singleton(X0) ),
introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition]) ).
fof(f22898,plain,
! [X0] :
( ~ sQ704_spl
| sK123_skl = singleton(X0) ),
inference(component_clause,[status(thm)],[f22897]) ).
fof(f22901,plain,
( ~ sQ704_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22898,f10948]) ).
fof(f22902,plain,
~ sQ704_spl,
inference(contradiction_clause,[status(thm)],[f22901]) ).
fof(f23068,definition,
! [X0,X1] :
( sQ730_spl
<=> ~ in(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition]) ).
fof(f23069,plain,
! [X0,X1] :
( ~ sQ730_spl
| ~ in(X0,X1) ),
inference(component_clause,[status(thm)],[f23068]) ).
fof(f23297,plain,
( ~ sQ730_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f21113,f23069]) ).
fof(f23320,definition,
! [X0] :
( sQ734_spl
<=> ~ finite(X0) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f23321,plain,
! [X0] :
( ~ sQ734_spl
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f23320]) ).
fof(f23323,definition,
! [X1] :
( sQ735_spl
<=> ~ element(omega,powerset(X1)) ),
introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition]) ).
fof(f23324,plain,
! [X0] :
( ~ sQ735_spl
| ~ element(omega,powerset(X0)) ),
inference(component_clause,[status(thm)],[f23323]) ).
fof(f23357,plain,
~ sQ730_spl,
inference(contradiction_clause,[status(thm)],[f23297]) ).
fof(f23358,plain,
( ~ sQ734_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1227,f23321]) ).
fof(f23362,plain,
~ sQ734_spl,
inference(contradiction_clause,[status(thm)],[f23358]) ).
fof(f23598,plain,
( ~ sQ702_spl
| $false ),
inference(resolution,[status(thm)],[f22875,f10949]) ).
fof(f23606,plain,
~ sQ702_spl,
inference(contradiction_clause,[status(thm)],[f23598]) ).
fof(f23607,plain,
( ~ sQ735_spl
| $false ),
inference(resolution,[status(thm)],[f23324,f17786]) ).
fof(f23608,plain,
~ sQ735_spl,
inference(contradiction_clause,[status(thm)],[f23607]) ).
fof(f23689,plain,
( sQ536_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17125,f22640]) ).
fof(f23690,plain,
sQ536_spl,
inference(contradiction_clause,[status(thm)],[f23689]) ).
fof(f23990,definition,
( sQ772_spl
<=> ordinal(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ772_spl])],[split_symbol_definition]) ).
fof(f23992,plain,
( sQ772_spl
| ~ ordinal(sK123_skl) ),
inference(component_clause,[status(thm)],[f23990]) ).
fof(f24012,plain,
( sQ772_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23992,f1536]) ).
fof(f24013,plain,
sQ772_spl,
inference(contradiction_clause,[status(thm)],[f24012]) ).
fof(f24022,definition,
( sQ778_spl
<=> element(set_difference(the_carrier(sK251_skl),sK252_skl),powerset(the_carrier(sK251_skl))) ),
introduced(definition,[new_symbols(definition,[sQ778_spl])],[split_symbol_definition]) ).
fof(f24024,plain,
( sQ778_spl
| ~ element(set_difference(the_carrier(sK251_skl),sK252_skl),powerset(the_carrier(sK251_skl))) ),
inference(component_clause,[status(thm)],[f24022]) ).
fof(f24034,plain,
( sQ778_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24024,f18280]) ).
fof(f24035,plain,
sQ778_spl,
inference(contradiction_clause,[status(thm)],[f24034]) ).
fof(f25083,plain,
! [X0,X1] :
( ~ sQ363_spl
| in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f13303,f22640]) ).
fof(f25107,plain,
( ~ sQ363_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f12013,f25083]) ).
fof(f25155,plain,
~ sQ363_spl,
inference(contradiction_clause,[status(thm)],[f25107]) ).
fof(f25280,definition,
! [X0] :
( sQ803_spl
<=> ~ v5_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ803_spl])],[split_symbol_definition]) ).
fof(f25281,plain,
! [X0] :
( ~ sQ803_spl
| ~ v5_membered(X0) ),
inference(component_clause,[status(thm)],[f25280]) ).
fof(f25324,plain,
( ~ sQ803_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f10951,f25281]) ).
fof(f25327,plain,
~ sQ803_spl,
inference(contradiction_clause,[status(thm)],[f25324]) ).
fof(f25422,plain,
( ~ sQ637_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1533,f20096]) ).
fof(f25423,plain,
~ sQ637_spl,
inference(contradiction_clause,[status(thm)],[f25422]) ).
fof(f25429,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f13746]) ).
fof(f26333,definition,
! [X0] :
( sQ838_spl
<=> ( in(sK254_skl(sK123_skl,X0),sK123_skl)
| ~ finite(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ838_spl])],[split_symbol_definition]) ).
fof(f26334,plain,
! [X0] :
( ~ sQ838_spl
| in(sK254_skl(sK123_skl,X0),sK123_skl)
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f26333]) ).
fof(f26337,plain,
! [X0] :
( ~ sQ838_spl
| ~ finite(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f26334,f10949]) ).
fof(f26350,plain,
( ~ sQ838_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1227,f26337]) ).
fof(f26354,plain,
~ sQ838_spl,
inference(contradiction_clause,[status(thm)],[f26350]) ).
fof(f26530,plain,
( sQ623_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19940,f18880]) ).
fof(f26531,plain,
sQ623_spl,
inference(contradiction_clause,[status(thm)],[f26530]) ).
fof(f26758,definition,
( sQ851_spl
<=> in(sK257_skl(the_L_meet(sK93_skl),sK123_skl,cartesian_product2(sK123_skl,sK123_skl)),sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ851_spl])],[split_symbol_definition]) ).
fof(f26759,plain,
( ~ sQ851_spl
| in(sK257_skl(the_L_meet(sK93_skl),sK123_skl,cartesian_product2(sK123_skl,sK123_skl)),sK123_skl) ),
inference(component_clause,[status(thm)],[f26758]) ).
fof(f26765,plain,
( ~ sQ851_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26759,f10949]) ).
fof(f26766,plain,
~ sQ851_spl,
inference(contradiction_clause,[status(thm)],[f26765]) ).
fof(f26984,definition,
( sQ859_spl
<=> finite(relation_dom(sK123_skl)) ),
introduced(definition,[new_symbols(definition,[sQ859_spl])],[split_symbol_definition]) ).
fof(f26986,plain,
( sQ859_spl
| ~ finite(relation_dom(sK123_skl)) ),
inference(component_clause,[status(thm)],[f26984]) ).
fof(f26988,plain,
( sQ859_spl
| ~ finite(sK123_skl) ),
inference(forward_demodulation,[status(thm)],[f10965,f26986]) ).
fof(f26989,plain,
( sQ859_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26988,f11826]) ).
fof(f26990,plain,
sQ859_spl,
inference(contradiction_clause,[status(thm)],[f26989]) ).
fof(f27063,plain,
( ~ sQ314_spl
| set_intersection2(sK252_skl,the_carrier(sK251_skl)) = sK252_skl ),
inference(resolution,[status(thm)],[f2148,f11844]) ).
fof(f27089,plain,
( ~ sQ314_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27063,f3657]) ).
fof(f27090,plain,
( ~ sQ314_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f27089]) ).
fof(f27091,plain,
$false,
inference(sat_refutation,[status(thm)],[f3267,f3395,f11805,f11809,f11978,f12584,f12586,f13196,f13621,f13625,f13875,f14215,f14666,f14670,f15099,f15381,f15383,f15385,f15391,f15806,f15820,f16131,f16134,f16137,f16140,f16184,f16593,f16678,f16743,f17203,f17702,f17783,f19084,f19086,f19088,f19090,f19092,f19107,f19109,f19185,f19187,f19189,f19191,f19254,f19900,f19971,f20340,f20463,f20486,f21772,f22902,f23357,f23362,f23606,f23608,f23690,f24013,f24035,f25155,f25327,f25423,f25429,f26354,f26531,f26766,f26990,f27090]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU307+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n026.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 06:12:38 UTC 2026
% 0.18/0.47 % CPUTime :
% 0.21/0.56 % Drodi V4.1.1
% 66.59/9.06 % Refutation found
% 66.59/9.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.59/9.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.46/9.12 % Elapsed time: 8.643509 seconds
% 12.46/9.12 % CPU time: 67.319671 seconds
% 12.46/9.12 % Total memory used: 474.092 MB
% 12.46/9.12 % Net memory used: 430.648 MB
%------------------------------------------------------------------------------