%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU383+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:22 PM UTC 2026
% Result : Theorem 111.41s 14.67s
% Output : CNFRefutation 67.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 344
% Syntax : Number of formulae : 1363 ( 305 unt; 252 def)
% Number of atoms : 4158 ( 75 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 4491 (1696 ~;1687 |; 744 &)
% ( 270 <=>; 93 =>; 0 <=; 1 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 311 ( 309 usr; 253 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 21 con; 0-2 aty)
% Number of variables : 707 ( 678 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( v1_membered(A)
=> ! [B] :
( element(B,A)
=> v1_xcmplx_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( rel_str(A)
=> ( ( complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( join_complete_relstr(A)
& up_complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A] :
( v2_membered(A)
=> ! [B] :
( element(B,A)
=> ( v1_xreal_0(B)
& v1_xcmplx_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
( rel_str(A)
=> ( ( join_complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( lower_bounded_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] :
( v3_membered(A)
=> ! [B] :
( element(B,A)
=> ( v1_rat_1(B)
& v1_xreal_0(B)
& v1_xcmplx_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( v4_membered(A)
=> ! [B] :
( element(B,A)
=> ( v1_rat_1(B)
& v1_int_1(B)
& v1_xreal_0(B)
& v1_xcmplx_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( rel_str(A)
=> ( ( join_complete_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( with_infima_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( v5_membered(A)
=> ! [B] :
( element(B,A)
=> ( v1_rat_1(B)
& v1_int_1(B)
& v1_xreal_0(B)
& natural(B)
& v1_xcmplx_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( rel_str(A)
=> ( ( join_complete_relstr(A)
& upper_bounded_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( empty(A)
=> ( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( v1_membered(A)
=> ! [B] :
( element(B,powerset(A))
=> v1_membered(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( v2_membered(A)
=> ! [B] :
( element(B,powerset(A))
=> ( v2_membered(B)
& v1_membered(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( v3_membered(A)
=> ! [B] :
( element(B,powerset(A))
=> ( v3_membered(B)
& v2_membered(B)
& v1_membered(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( v4_membered(A)
=> ! [B] :
( element(B,powerset(A))
=> ( v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( ordinal(A)
=> ! [B] :
( element(B,A)
=> ( ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A] :
( rel_str(A)
=> ( ( join_complete_relstr(A)
& up_complete_relstr(A)
& upper_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( rel_str(A)
=> ( with_infima_relstr(A)
=> ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( rel_str(A)
=> ( ( up_complete_relstr(A)
& connected_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( join_complete_relstr(A)
& up_complete_relstr(A)
& connected_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A] :
( rel_str(A)
=> ( ( reflexive_relstr(A)
& trivial_carrier(A)
& ~ empty_carrier(A) )
=> ( v2_waybel_3(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( rel_str(A)
=> ( ( reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( ~ v1_yellow_3(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A] :
( rel_str(A)
=> ( ( v3_waybel_3(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( v2_waybel_3(A)
& up_complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( rel_str(A)
=> ( ( with_infima_relstr(A)
& with_suprema_relstr(A)
& v3_waybel_3(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A) )
=> ( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& v2_waybel_2(A)
& v1_waybel_2(A)
& ~ v1_yellow_3(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A] :
( rel_str(A)
=> ( ( trivial_carrier(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( connected_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A] :
( rel_str(A)
=> ( ( v2_waybel_3(A)
& up_complete_relstr(A)
& lower_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A) )
=> ( v3_waybel_3(A)
& lower_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A] :
( rel_str(A)
=> ( ( upper_bounded_relstr(A)
& lower_bounded_relstr(A) )
=> bounded_relstr(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A] :
( rel_str(A)
=> ( ( connected_relstr(A)
& complete_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( v2_waybel_3(A)
& connected_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [A] :
( rel_str(A)
=> ( ( complemented_relstr(A)
& distributive_relstr(A)
& bounded_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( boolean_relstr(A)
& complemented_relstr(A)
& distributive_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( upper_relstr_subset(B,A)
<=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& in(C,B) )
=> in(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
! [A] : cast_to_subset(A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,axiom,
! [A] : element(cast_to_subset(A),powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,axiom,
! [A] :
( rel_str(A)
=> element(bottom_of_relstr(A),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f351,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f377,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f391,axiom,
! [A,B] :
( v5_membered(A)
=> ( v5_membered(set_intersection2(A,B))
& v4_membered(set_intersection2(A,B))
& v3_membered(set_intersection2(A,B))
& v2_membered(set_intersection2(A,B))
& v1_membered(set_intersection2(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f393,axiom,
! [A,B] :
( v1_membered(A)
=> v1_membered(set_difference(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f394,axiom,
! [A,B] :
( v2_membered(A)
=> ( v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f395,axiom,
! [A,B] :
( v3_membered(A)
=> ( v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f407,axiom,
! [A,B] :
( v4_membered(A)
=> ( v4_membered(set_difference(A,B))
& v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [A,B] :
( v5_membered(A)
=> ( v5_membered(set_difference(A,B))
& v4_membered(set_difference(A,B))
& v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f458,lemma,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( in(C,B)
=> in(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f472,axiom,
? [A] :
( connected_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f474,axiom,
? [A] :
( join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f479,axiom,
? [A] :
( complete_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f480,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f484,axiom,
? [A] :
( empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f490,axiom,
? [A] :
( join_complete_relstr(A)
& up_complete_relstr(A)
& connected_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f491,axiom,
? [A] :
( v3_waybel_3(A)
& v2_waybel_3(A)
& distributive_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f492,axiom,
? [A] :
( with_infima_relstr(A)
& with_suprema_relstr(A)
& boolean_relstr(A)
& complemented_relstr(A)
& heyting_relstr(A)
& distributive_relstr(A)
& ~ v1_yellow_3(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ trivial_carrier(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f494,axiom,
? [A] :
( trivial_carrier(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f495,axiom,
? [A] :
( ~ v1_yellow_3(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f499,axiom,
? [A] :
( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f500,axiom,
? [A] :
( antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f504,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f508,axiom,
? [A] :
( v3_waybel_3(A)
& v2_waybel_3(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f511,axiom,
? [A] :
( bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f523,axiom,
? [A] :
( boolean_relstr(A)
& complemented_relstr(A)
& heyting_relstr(A)
& distributive_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f525,axiom,
? [A] :
( heyting_relstr(A)
& distributive_relstr(A)
& upper_bounded_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f612,axiom,
! [A,B] :
( disjoint(A,B)
=> disjoint(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f663,lemma,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f669,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f705,lemma,
! [A,B] :
( subset(A,B)
=> set_intersection2(A,B) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f710,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f715,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f742,lemma,
! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f744,axiom,
! [A] : set_difference(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f747,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f751,lemma,
! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f760,lemma,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f775,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f776,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f777,lemma,
! [A] : the_carrier(boole_POSet(A)) = powerset(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f794,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f795,lemma,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f802,lemma,
! [A] :
( rel_str(A)
=> ! [B] :
( ( subrelstr(B,A)
& full_subrelstr(B,A) )
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( in(F,the_carrier(B))
& in(E,the_carrier(B))
& related(A,C,D)
& F = D
& E = C )
=> related(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f820,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f825,lemma,
! [A,B] : subset(A,set_union2(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f826,lemma,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f832,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f833,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f832]) ).
fof(f852,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f853,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f852]) ).
fof(f856,plain,
! [A] :
( ! [B] :
( v1_xcmplx_0(B)
| ~ element(B,A) )
| ~ v1_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f857,plain,
! [X0,X1] :
( v1_xcmplx_0(X1)
| ~ element(X1,X0)
| ~ v1_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f856]) ).
fof(f858,plain,
! [A] :
( ( join_complete_relstr(A)
& up_complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ complete_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f861,plain,
! [X0] :
( up_complete_relstr(X0)
| ~ complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f858]) ).
fof(f862,plain,
! [X0] :
( join_complete_relstr(X0)
| ~ complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f858]) ).
fof(f873,plain,
! [A] :
( ! [B] :
( ( v1_xreal_0(B)
& v1_xcmplx_0(B) )
| ~ element(B,A) )
| ~ v2_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f875,plain,
! [X0,X1] :
( v1_xreal_0(X1)
| ~ element(X1,X0)
| ~ v2_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f873]) ).
fof(f876,plain,
! [A] :
( ( lower_bounded_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ join_complete_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f879,plain,
! [X0] :
( lower_bounded_relstr(X0)
| ~ join_complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f876]) ).
fof(f880,plain,
! [A] :
( ! [B] :
( ( v1_rat_1(B)
& v1_xreal_0(B)
& v1_xcmplx_0(B) )
| ~ element(B,A) )
| ~ v3_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f883,plain,
! [X0,X1] :
( v1_rat_1(X1)
| ~ element(X1,X0)
| ~ v3_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f880]) ).
fof(f895,plain,
! [A] :
( ! [B] :
( ( v1_rat_1(B)
& v1_int_1(B)
& v1_xreal_0(B)
& v1_xcmplx_0(B) )
| ~ element(B,A) )
| ~ v4_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f898,plain,
! [X0,X1] :
( v1_int_1(X1)
| ~ element(X1,X0)
| ~ v4_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f895]) ).
fof(f900,plain,
! [A] :
( ( with_infima_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ join_complete_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f904,plain,
! [X0] :
( with_infima_relstr(X0)
| ~ join_complete_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f900]) ).
fof(f905,plain,
! [A] :
( ! [B] :
( ( v1_rat_1(B)
& v1_int_1(B)
& v1_xreal_0(B)
& natural(B)
& v1_xcmplx_0(B) )
| ~ element(B,A) )
| ~ v5_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f907,plain,
! [X0,X1] :
( natural(X1)
| ~ element(X1,X0)
| ~ v5_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f905]) ).
fof(f911,plain,
! [A] :
( ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ join_complete_relstr(A)
| ~ upper_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f915,plain,
! [X0] :
( with_suprema_relstr(X0)
| ~ join_complete_relstr(X0)
| ~ upper_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f911]) ).
fof(f917,plain,
! [A] :
( ( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f918,plain,
! [X0] :
( v1_membered(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f919,plain,
! [X0] :
( v2_membered(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f920,plain,
! [X0] :
( v3_membered(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f921,plain,
! [X0] :
( v4_membered(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f922,plain,
! [X0] :
( v5_membered(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f923,plain,
! [A] :
( ! [B] :
( v1_membered(B)
| ~ element(B,powerset(A)) )
| ~ v1_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f924,plain,
! [X0,X1] :
( v1_membered(X1)
| ~ element(X1,powerset(X0))
| ~ v1_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f923]) ).
fof(f925,plain,
! [A] :
( ! [B] :
( ( v2_membered(B)
& v1_membered(B) )
| ~ element(B,powerset(A)) )
| ~ v2_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f927,plain,
! [X0,X1] :
( v2_membered(X1)
| ~ element(X1,powerset(X0))
| ~ v2_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f925]) ).
fof(f928,plain,
! [A] :
( ! [B] :
( ( v3_membered(B)
& v2_membered(B)
& v1_membered(B) )
| ~ element(B,powerset(A)) )
| ~ v3_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f931,plain,
! [X0,X1] :
( v3_membered(X1)
| ~ element(X1,powerset(X0))
| ~ v3_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f928]) ).
fof(f932,plain,
! [A] :
( ! [B] :
( ( v4_membered(B)
& v3_membered(B)
& v2_membered(B)
& v1_membered(B) )
| ~ element(B,powerset(A)) )
| ~ v4_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f936,plain,
! [X0,X1] :
( v4_membered(X1)
| ~ element(X1,powerset(X0))
| ~ v4_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f932]) ).
fof(f937,plain,
! [A] :
( ! [B] :
( ( ordinal(B)
& epsilon_connected(B)
& epsilon_transitive(B) )
| ~ element(B,A) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f938,plain,
! [X0,X1] :
( epsilon_transitive(X1)
| ~ element(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f937]) ).
fof(f939,plain,
! [X0,X1] :
( epsilon_connected(X1)
| ~ element(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f937]) ).
fof(f940,plain,
! [X0,X1] :
( ordinal(X1)
| ~ element(X1,X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f937]) ).
fof(f981,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f982,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f981]) ).
fof(f993,plain,
! [A] :
( ( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ join_complete_relstr(A)
| ~ up_complete_relstr(A)
| ~ upper_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f1000,plain,
! [X0] :
( bounded_relstr(X0)
| ~ join_complete_relstr(X0)
| ~ up_complete_relstr(X0)
| ~ upper_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f993]) ).
fof(f1023,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f1026,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1023]) ).
fof(f1032,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_infima_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f1033,plain,
! [X0] :
( ~ empty_carrier(X0)
| ~ with_infima_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1032]) ).
fof(f1041,plain,
! [A] :
( ( join_complete_relstr(A)
& up_complete_relstr(A)
& connected_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ up_complete_relstr(A)
| ~ connected_relstr(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f1046,plain,
! [X0] :
( with_suprema_relstr(X0)
| ~ up_complete_relstr(X0)
| ~ connected_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1041]) ).
fof(f1051,plain,
! [X0] :
( bounded_relstr(X0)
| ~ up_complete_relstr(X0)
| ~ connected_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1041]) ).
fof(f1077,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f1080,plain,
! [X0] :
( ordinal(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1077]) ).
fof(f1081,plain,
! [A] :
( ( v2_waybel_3(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ reflexive_relstr(A)
| ~ trivial_carrier(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f1084,plain,
! [X0] :
( v2_waybel_3(X0)
| ~ reflexive_relstr(X0)
| ~ trivial_carrier(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1081]) ).
fof(f1088,plain,
! [A] :
( ( ~ v1_yellow_3(A)
& ~ empty_carrier(A) )
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f1090,plain,
! [X0] :
( ~ v1_yellow_3(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1088]) ).
fof(f1103,plain,
! [A] :
( ( v2_waybel_3(A)
& up_complete_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ v3_waybel_3(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f1107,plain,
! [X0] :
( v2_waybel_3(X0)
| ~ v3_waybel_3(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1108,plain,
! [A] :
( ( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& v2_waybel_2(A)
& v1_waybel_2(A)
& ~ v1_yellow_3(A)
& join_complete_relstr(A)
& up_complete_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ with_infima_relstr(A)
| ~ with_suprema_relstr(A)
| ~ v3_waybel_3(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f1114,plain,
! [X0] :
( upper_bounded_relstr(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1115,plain,
! [X0] :
( bounded_relstr(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1116,plain,
! [X0] :
( up_complete_relstr(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1118,plain,
! [X0] :
( ~ v1_yellow_3(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1119,plain,
! [X0] :
( v1_waybel_2(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1120,plain,
! [X0] :
( v2_waybel_2(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ v3_waybel_3(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1108]) ).
fof(f1139,plain,
! [A] :
( ( connected_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ trivial_carrier(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f1142,plain,
! [X0] :
( connected_relstr(X0)
| ~ trivial_carrier(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1139]) ).
fof(f1150,plain,
! [A] :
( ( v3_waybel_3(A)
& lower_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ v2_waybel_3(A)
| ~ up_complete_relstr(A)
| ~ lower_bounded_relstr(A)
| ~ with_suprema_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f1157,plain,
! [X0] :
( v3_waybel_3(X0)
| ~ v2_waybel_3(X0)
| ~ up_complete_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1150]) ).
fof(f1158,plain,
! [A] :
( bounded_relstr(A)
| ~ upper_bounded_relstr(A)
| ~ lower_bounded_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f1159,plain,
! [X0] :
( bounded_relstr(X0)
| ~ upper_bounded_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1158]) ).
fof(f1171,plain,
! [A] :
( ( v2_waybel_3(A)
& connected_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ connected_relstr(A)
| ~ complete_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f1177,plain,
! [X0] :
( v2_waybel_3(X0)
| ~ connected_relstr(X0)
| ~ complete_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1171]) ).
fof(f1211,plain,
! [A] :
( ( boolean_relstr(A)
& complemented_relstr(A)
& distributive_relstr(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ complemented_relstr(A)
| ~ distributive_relstr(A)
| ~ bounded_relstr(A)
| ~ with_infima_relstr(A)
| ~ with_suprema_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f1223,plain,
! [X0] :
( boolean_relstr(X0)
| ~ complemented_relstr(X0)
| ~ distributive_relstr(X0)
| ~ bounded_relstr(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1211]) ).
fof(f1227,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f1230,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f1249,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f92]) ).
fof(f1250,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)],[f1249]) ).
fof(f1251,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f1250]) ).
fof(f1253,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f1250]) ).
fof(f1603,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f139]) ).
fof(f1604,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f1603]) ).
fof(f1605,plain,
( ! [A] :
( in(sK63_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63_skl]),skolemize(B,sK63_skl(A))],[f1604]) ).
fof(f1606,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f1605]) ).
fof(f1609,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)],[f141]) ).
fof(f1610,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)],[f1609]) ).
fof(f1611,plain,
( ! [A,B] :
( ( ( subset(sK64_skl(B,A),A)
| in(sK64_skl(B,A),B) )
& ( ~ subset(sK64_skl(B,A),A)
| ~ in(sK64_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,[sK64_skl]),skolemize(C,sK64_skl(B,A))],[f1610]) ).
fof(f1612,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f1611]) ).
fof(f1616,plain,
! [A] :
( ! [B] :
( ( upper_relstr_subset(B,A)
<=> ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f142]) ).
fof(f1617,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ~ in(D,B)
& related(A,C,D)
& in(C,B)
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f1616]) ).
fof(f1618,plain,
! [A] :
( ! [B] :
( ( ( ( ~ in(sK66_skl(B,A),B)
& related(A,sK65_skl(B,A),sK66_skl(B,A))
& in(sK65_skl(B,A),B)
& element(sK66_skl(B,A),the_carrier(A))
& element(sK65_skl(B,A),the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65_skl,sK66_skl]),skolemize(C,sK65_skl(B,A)),skolemize(D,sK66_skl(B,A))],[f1617]) ).
fof(f1619,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1618]) ).
fof(f1674,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f152]) ).
fof(f1675,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)],[f1674]) ).
fof(f1676,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)],[f1675]) ).
fof(f1677,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1676]) ).
fof(f1679,plain,
! [X0,X1] :
( empty(X1)
| ~ element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1676]) ).
fof(f1680,plain,
! [X0,X1] :
( ~ empty(X1)
| element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1676]) ).
fof(f1773,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f167]) ).
fof(f1774,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)],[f1773]) ).
fof(f1775,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)],[f1774]) ).
fof(f1776,plain,
( ! [A,B] :
( ( ~ in(sK93_skl(B,A),B)
& in(sK93_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,[sK93_skl]),skolemize(C,sK93_skl(B,A))],[f1775]) ).
fof(f1778,plain,
! [X0,X1] :
( in(sK93_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1776]) ).
fof(f1779,plain,
! [X0,X1] :
( ~ in(sK93_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1776]) ).
fof(f1830,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f2191,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f2213,plain,
! [A] :
( element(bottom_of_relstr(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f270]) ).
fof(f2214,plain,
! [X0] :
( element(bottom_of_relstr(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f2213]) ).
fof(f2215,plain,
( ! [A] : rel_str(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f271]) ).
fof(f2217,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f2215]) ).
fof(f2287,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f305]) ).
fof(f2288,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f2287]) ).
fof(f2375,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f2402,plain,
( ! [A] : preboolean(powerset(A))
& ! [A] : diff_closed(powerset(A))
& ! [A] : cup_closed(powerset(A))
& ! [A] : ~ empty(powerset(A)) ),
inference(miniscoping,[status(thm)],[f351]) ).
fof(f2403,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f2402]) ).
fof(f2545,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f2623,plain,
! [A,B] :
( ( v5_membered(set_intersection2(A,B))
& v4_membered(set_intersection2(A,B))
& v3_membered(set_intersection2(A,B))
& v2_membered(set_intersection2(A,B))
& v1_membered(set_intersection2(A,B)) )
| ~ v5_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f391]) ).
fof(f2624,plain,
! [A] :
( ( ! [B] : v5_membered(set_intersection2(A,B))
& ! [B] : v4_membered(set_intersection2(A,B))
& ! [B] : v3_membered(set_intersection2(A,B))
& ! [B] : v2_membered(set_intersection2(A,B))
& ! [B] : v1_membered(set_intersection2(A,B)) )
| ~ v5_membered(A) ),
inference(miniscoping,[status(thm)],[f2623]) ).
fof(f2629,plain,
! [X0,X1] :
( v5_membered(set_intersection2(X0,X1))
| ~ v5_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2624]) ).
fof(f2637,plain,
! [A,B] :
( v1_membered(set_difference(A,B))
| ~ v1_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f393]) ).
fof(f2638,plain,
! [A] :
( ! [B] : v1_membered(set_difference(A,B))
| ~ v1_membered(A) ),
inference(miniscoping,[status(thm)],[f2637]) ).
fof(f2639,plain,
! [X0,X1] :
( v1_membered(set_difference(X0,X1))
| ~ v1_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2638]) ).
fof(f2640,plain,
! [A,B] :
( ( v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) )
| ~ v2_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f394]) ).
fof(f2641,plain,
! [A] :
( ( ! [B] : v2_membered(set_difference(A,B))
& ! [B] : v1_membered(set_difference(A,B)) )
| ~ v2_membered(A) ),
inference(miniscoping,[status(thm)],[f2640]) ).
fof(f2643,plain,
! [X0,X1] :
( v2_membered(set_difference(X0,X1))
| ~ v2_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2641]) ).
fof(f2644,plain,
! [A,B] :
( ( v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) )
| ~ v3_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f395]) ).
fof(f2645,plain,
! [A] :
( ( ! [B] : v3_membered(set_difference(A,B))
& ! [B] : v2_membered(set_difference(A,B))
& ! [B] : v1_membered(set_difference(A,B)) )
| ~ v3_membered(A) ),
inference(miniscoping,[status(thm)],[f2644]) ).
fof(f2648,plain,
! [X0,X1] :
( v3_membered(set_difference(X0,X1))
| ~ v3_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2645]) ).
fof(f2705,plain,
! [A,B] :
( ( v4_membered(set_difference(A,B))
& v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) )
| ~ v4_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f407]) ).
fof(f2706,plain,
! [A] :
( ( ! [B] : v4_membered(set_difference(A,B))
& ! [B] : v3_membered(set_difference(A,B))
& ! [B] : v2_membered(set_difference(A,B))
& ! [B] : v1_membered(set_difference(A,B)) )
| ~ v4_membered(A) ),
inference(miniscoping,[status(thm)],[f2705]) ).
fof(f2710,plain,
! [X0,X1] :
( v4_membered(set_difference(X0,X1))
| ~ v4_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2706]) ).
fof(f2711,plain,
! [A,B] :
( ( v5_membered(set_difference(A,B))
& v4_membered(set_difference(A,B))
& v3_membered(set_difference(A,B))
& v2_membered(set_difference(A,B))
& v1_membered(set_difference(A,B)) )
| ~ v5_membered(A) ),
inference(pre_NNF_transformation,[status(thm)],[f408]) ).
fof(f2712,plain,
! [A] :
( ( ! [B] : v5_membered(set_difference(A,B))
& ! [B] : v4_membered(set_difference(A,B))
& ! [B] : v3_membered(set_difference(A,B))
& ! [B] : v2_membered(set_difference(A,B))
& ! [B] : v1_membered(set_difference(A,B)) )
| ~ v5_membered(A) ),
inference(miniscoping,[status(thm)],[f2711]) ).
fof(f2717,plain,
! [X0,X1] :
( v5_membered(set_difference(X0,X1))
| ~ v5_membered(X0) ),
inference(cnf_transformation,[status(thm)],[f2712]) ).
fof(f2931,plain,
! [A,B] :
( ! [C] :
( in(C,A)
| ~ in(C,B) )
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f458]) ).
fof(f2932,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f2931]) ).
fof(f3028,plain,
( connected_relstr(sK179_skl)
& antisymmetric_relstr(sK179_skl)
& transitive_relstr(sK179_skl)
& reflexive_relstr(sK179_skl)
& ~ empty_carrier(sK179_skl)
& rel_str(sK179_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK179_skl]),skolemize(A,sK179_skl)],[f472]) ).
fof(f3029,plain,
rel_str(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3030,plain,
~ empty_carrier(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3031,plain,
reflexive_relstr(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3032,plain,
transitive_relstr(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3033,plain,
antisymmetric_relstr(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3034,plain,
connected_relstr(sK179_skl),
inference(cnf_transformation,[status(thm)],[f3028]) ).
fof(f3052,plain,
( join_complete_relstr(sK181_skl)
& up_complete_relstr(sK181_skl)
& bounded_relstr(sK181_skl)
& upper_bounded_relstr(sK181_skl)
& lower_bounded_relstr(sK181_skl)
& complete_relstr(sK181_skl)
& with_infima_relstr(sK181_skl)
& with_suprema_relstr(sK181_skl)
& antisymmetric_relstr(sK181_skl)
& transitive_relstr(sK181_skl)
& reflexive_relstr(sK181_skl)
& strict_rel_str(sK181_skl)
& ~ empty_carrier(sK181_skl)
& rel_str(sK181_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK181_skl]),skolemize(A,sK181_skl)],[f474]) ).
fof(f3053,plain,
rel_str(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3054,plain,
~ empty_carrier(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3056,plain,
reflexive_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3057,plain,
transitive_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3058,plain,
antisymmetric_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3061,plain,
complete_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3062,plain,
lower_bounded_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3063,plain,
upper_bounded_relstr(sK181_skl),
inference(cnf_transformation,[status(thm)],[f3052]) ).
fof(f3084,plain,
( complete_relstr(sK186_skl)
& antisymmetric_relstr(sK186_skl)
& transitive_relstr(sK186_skl)
& reflexive_relstr(sK186_skl)
& strict_rel_str(sK186_skl)
& ~ empty_carrier(sK186_skl)
& rel_str(sK186_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK186_skl]),skolemize(A,sK186_skl)],[f479]) ).
fof(f3085,plain,
rel_str(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3086,plain,
~ empty_carrier(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3088,plain,
reflexive_relstr(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3089,plain,
transitive_relstr(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3090,plain,
antisymmetric_relstr(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3091,plain,
complete_relstr(sK186_skl),
inference(cnf_transformation,[status(thm)],[f3084]) ).
fof(f3092,plain,
( v5_membered(sK187_skl)
& v4_membered(sK187_skl)
& v3_membered(sK187_skl)
& v2_membered(sK187_skl)
& v1_membered(sK187_skl)
& ~ empty(sK187_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK187_skl]),skolemize(A,sK187_skl)],[f480]) ).
fof(f3094,plain,
v1_membered(sK187_skl),
inference(cnf_transformation,[status(thm)],[f3092]) ).
fof(f3095,plain,
v2_membered(sK187_skl),
inference(cnf_transformation,[status(thm)],[f3092]) ).
fof(f3096,plain,
v3_membered(sK187_skl),
inference(cnf_transformation,[status(thm)],[f3092]) ).
fof(f3097,plain,
v4_membered(sK187_skl),
inference(cnf_transformation,[status(thm)],[f3092]) ).
fof(f3098,plain,
v5_membered(sK187_skl),
inference(cnf_transformation,[status(thm)],[f3092]) ).
fof(f3111,plain,
( empty(sK191_skl)
& one_to_one(sK191_skl)
& function(sK191_skl)
& relation(sK191_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK191_skl]),skolemize(A,sK191_skl)],[f484]) ).
fof(f3115,plain,
empty(sK191_skl),
inference(cnf_transformation,[status(thm)],[f3111]) ).
fof(f3136,plain,
( join_complete_relstr(sK197_skl)
& up_complete_relstr(sK197_skl)
& connected_relstr(sK197_skl)
& bounded_relstr(sK197_skl)
& upper_bounded_relstr(sK197_skl)
& lower_bounded_relstr(sK197_skl)
& complete_relstr(sK197_skl)
& with_infima_relstr(sK197_skl)
& with_suprema_relstr(sK197_skl)
& antisymmetric_relstr(sK197_skl)
& transitive_relstr(sK197_skl)
& reflexive_relstr(sK197_skl)
& ~ empty_carrier(sK197_skl)
& rel_str(sK197_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK197_skl]),skolemize(A,sK197_skl)],[f490]) ).
fof(f3137,plain,
rel_str(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3138,plain,
~ empty_carrier(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3139,plain,
reflexive_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3140,plain,
transitive_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3141,plain,
antisymmetric_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3144,plain,
complete_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3146,plain,
upper_bounded_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3148,plain,
connected_relstr(sK197_skl),
inference(cnf_transformation,[status(thm)],[f3136]) ).
fof(f3151,plain,
( v3_waybel_3(sK198_skl)
& v2_waybel_3(sK198_skl)
& distributive_relstr(sK198_skl)
& complete_relstr(sK198_skl)
& with_infima_relstr(sK198_skl)
& with_suprema_relstr(sK198_skl)
& join_complete_relstr(sK198_skl)
& up_complete_relstr(sK198_skl)
& bounded_relstr(sK198_skl)
& upper_bounded_relstr(sK198_skl)
& lower_bounded_relstr(sK198_skl)
& antisymmetric_relstr(sK198_skl)
& transitive_relstr(sK198_skl)
& reflexive_relstr(sK198_skl)
& strict_rel_str(sK198_skl)
& ~ empty_carrier(sK198_skl)
& rel_str(sK198_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK198_skl]),skolemize(A,sK198_skl)],[f491]) ).
fof(f3152,plain,
rel_str(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3153,plain,
~ empty_carrier(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3155,plain,
reflexive_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3156,plain,
transitive_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3157,plain,
antisymmetric_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3159,plain,
upper_bounded_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3165,plain,
complete_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3166,plain,
distributive_relstr(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3168,plain,
v3_waybel_3(sK198_skl),
inference(cnf_transformation,[status(thm)],[f3151]) ).
fof(f3169,plain,
( with_infima_relstr(sK199_skl)
& with_suprema_relstr(sK199_skl)
& boolean_relstr(sK199_skl)
& complemented_relstr(sK199_skl)
& heyting_relstr(sK199_skl)
& distributive_relstr(sK199_skl)
& ~ v1_yellow_3(sK199_skl)
& bounded_relstr(sK199_skl)
& upper_bounded_relstr(sK199_skl)
& lower_bounded_relstr(sK199_skl)
& antisymmetric_relstr(sK199_skl)
& transitive_relstr(sK199_skl)
& reflexive_relstr(sK199_skl)
& strict_rel_str(sK199_skl)
& ~ trivial_carrier(sK199_skl)
& ~ empty_carrier(sK199_skl)
& rel_str(sK199_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl]),skolemize(A,sK199_skl)],[f492]) ).
fof(f3170,plain,
rel_str(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3171,plain,
~ empty_carrier(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3174,plain,
reflexive_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3175,plain,
transitive_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3176,plain,
antisymmetric_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3177,plain,
lower_bounded_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3178,plain,
upper_bounded_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3181,plain,
distributive_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3183,plain,
complemented_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3185,plain,
with_suprema_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3186,plain,
with_infima_relstr(sK199_skl),
inference(cnf_transformation,[status(thm)],[f3169]) ).
fof(f3189,plain,
( trivial_carrier(sK201_skl)
& complete_relstr(sK201_skl)
& with_infima_relstr(sK201_skl)
& with_suprema_relstr(sK201_skl)
& antisymmetric_relstr(sK201_skl)
& transitive_relstr(sK201_skl)
& reflexive_relstr(sK201_skl)
& strict_rel_str(sK201_skl)
& ~ empty_carrier(sK201_skl)
& rel_str(sK201_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK201_skl]),skolemize(A,sK201_skl)],[f494]) ).
fof(f3190,plain,
rel_str(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3191,plain,
~ empty_carrier(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3193,plain,
reflexive_relstr(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3194,plain,
transitive_relstr(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3195,plain,
antisymmetric_relstr(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3198,plain,
complete_relstr(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3199,plain,
trivial_carrier(sK201_skl),
inference(cnf_transformation,[status(thm)],[f3189]) ).
fof(f3200,plain,
( ~ v1_yellow_3(sK202_skl)
& antisymmetric_relstr(sK202_skl)
& transitive_relstr(sK202_skl)
& reflexive_relstr(sK202_skl)
& strict_rel_str(sK202_skl)
& ~ empty_carrier(sK202_skl)
& rel_str(sK202_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK202_skl]),skolemize(A,sK202_skl)],[f495]) ).
fof(f3201,plain,
rel_str(sK202_skl),
inference(cnf_transformation,[status(thm)],[f3200]) ).
fof(f3202,plain,
~ empty_carrier(sK202_skl),
inference(cnf_transformation,[status(thm)],[f3200]) ).
fof(f3204,plain,
reflexive_relstr(sK202_skl),
inference(cnf_transformation,[status(thm)],[f3200]) ).
fof(f3205,plain,
transitive_relstr(sK202_skl),
inference(cnf_transformation,[status(thm)],[f3200]) ).
fof(f3206,plain,
antisymmetric_relstr(sK202_skl),
inference(cnf_transformation,[status(thm)],[f3200]) ).
fof(f3231,plain,
( complete_relstr(sK206_skl)
& with_infima_relstr(sK206_skl)
& with_suprema_relstr(sK206_skl)
& antisymmetric_relstr(sK206_skl)
& transitive_relstr(sK206_skl)
& reflexive_relstr(sK206_skl)
& strict_rel_str(sK206_skl)
& ~ empty_carrier(sK206_skl)
& rel_str(sK206_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK206_skl]),skolemize(A,sK206_skl)],[f499]) ).
fof(f3232,plain,
rel_str(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3233,plain,
~ empty_carrier(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3235,plain,
reflexive_relstr(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3236,plain,
transitive_relstr(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3237,plain,
antisymmetric_relstr(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3240,plain,
complete_relstr(sK206_skl),
inference(cnf_transformation,[status(thm)],[f3231]) ).
fof(f3241,plain,
( antisymmetric_relstr(sK207_skl)
& transitive_relstr(sK207_skl)
& reflexive_relstr(sK207_skl)
& strict_rel_str(sK207_skl)
& ~ empty_carrier(sK207_skl)
& rel_str(sK207_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK207_skl]),skolemize(A,sK207_skl)],[f500]) ).
fof(f3242,plain,
rel_str(sK207_skl),
inference(cnf_transformation,[status(thm)],[f3241]) ).
fof(f3243,plain,
~ empty_carrier(sK207_skl),
inference(cnf_transformation,[status(thm)],[f3241]) ).
fof(f3245,plain,
reflexive_relstr(sK207_skl),
inference(cnf_transformation,[status(thm)],[f3241]) ).
fof(f3246,plain,
transitive_relstr(sK207_skl),
inference(cnf_transformation,[status(thm)],[f3241]) ).
fof(f3247,plain,
antisymmetric_relstr(sK207_skl),
inference(cnf_transformation,[status(thm)],[f3241]) ).
fof(f3263,plain,
! [A] :
( empty(sK211_skl(A))
& element(sK211_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK211_skl]),skolemize(B,sK211_skl(A))],[f504]) ).
fof(f3265,plain,
! [X0] : empty(sK211_skl(X0)),
inference(cnf_transformation,[status(thm)],[f3263]) ).
fof(f3281,plain,
( v3_waybel_3(sK215_skl)
& v2_waybel_3(sK215_skl)
& join_complete_relstr(sK215_skl)
& up_complete_relstr(sK215_skl)
& bounded_relstr(sK215_skl)
& upper_bounded_relstr(sK215_skl)
& lower_bounded_relstr(sK215_skl)
& complete_relstr(sK215_skl)
& with_infima_relstr(sK215_skl)
& with_suprema_relstr(sK215_skl)
& antisymmetric_relstr(sK215_skl)
& transitive_relstr(sK215_skl)
& reflexive_relstr(sK215_skl)
& strict_rel_str(sK215_skl)
& ~ empty_carrier(sK215_skl)
& rel_str(sK215_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK215_skl]),skolemize(A,sK215_skl)],[f508]) ).
fof(f3282,plain,
rel_str(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3283,plain,
~ empty_carrier(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3285,plain,
reflexive_relstr(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3286,plain,
transitive_relstr(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3287,plain,
antisymmetric_relstr(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3290,plain,
complete_relstr(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3292,plain,
upper_bounded_relstr(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3297,plain,
v3_waybel_3(sK215_skl),
inference(cnf_transformation,[status(thm)],[f3281]) ).
fof(f3304,plain,
( bounded_relstr(sK218_skl)
& upper_bounded_relstr(sK218_skl)
& lower_bounded_relstr(sK218_skl)
& complete_relstr(sK218_skl)
& with_infima_relstr(sK218_skl)
& with_suprema_relstr(sK218_skl)
& antisymmetric_relstr(sK218_skl)
& transitive_relstr(sK218_skl)
& reflexive_relstr(sK218_skl)
& ~ empty_carrier(sK218_skl)
& rel_str(sK218_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK218_skl]),skolemize(A,sK218_skl)],[f511]) ).
fof(f3305,plain,
rel_str(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3306,plain,
~ empty_carrier(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3307,plain,
reflexive_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3308,plain,
transitive_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3309,plain,
antisymmetric_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3312,plain,
complete_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3313,plain,
lower_bounded_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3314,plain,
upper_bounded_relstr(sK218_skl),
inference(cnf_transformation,[status(thm)],[f3304]) ).
fof(f3365,plain,
( boolean_relstr(sK230_skl)
& complemented_relstr(sK230_skl)
& heyting_relstr(sK230_skl)
& distributive_relstr(sK230_skl)
& bounded_relstr(sK230_skl)
& upper_bounded_relstr(sK230_skl)
& lower_bounded_relstr(sK230_skl)
& with_infima_relstr(sK230_skl)
& with_suprema_relstr(sK230_skl)
& antisymmetric_relstr(sK230_skl)
& transitive_relstr(sK230_skl)
& reflexive_relstr(sK230_skl)
& strict_rel_str(sK230_skl)
& ~ empty_carrier(sK230_skl)
& rel_str(sK230_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK230_skl]),skolemize(A,sK230_skl)],[f523]) ).
fof(f3366,plain,
rel_str(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3367,plain,
~ empty_carrier(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3369,plain,
reflexive_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3370,plain,
transitive_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3371,plain,
antisymmetric_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3372,plain,
with_suprema_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3373,plain,
with_infima_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3374,plain,
lower_bounded_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3375,plain,
upper_bounded_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3377,plain,
distributive_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3379,plain,
complemented_relstr(sK230_skl),
inference(cnf_transformation,[status(thm)],[f3365]) ).
fof(f3385,plain,
( heyting_relstr(sK232_skl)
& distributive_relstr(sK232_skl)
& upper_bounded_relstr(sK232_skl)
& with_infima_relstr(sK232_skl)
& with_suprema_relstr(sK232_skl)
& antisymmetric_relstr(sK232_skl)
& transitive_relstr(sK232_skl)
& reflexive_relstr(sK232_skl)
& strict_rel_str(sK232_skl)
& ~ empty_carrier(sK232_skl)
& rel_str(sK232_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK232_skl]),skolemize(A,sK232_skl)],[f525]) ).
fof(f3386,plain,
rel_str(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3387,plain,
~ empty_carrier(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3389,plain,
reflexive_relstr(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3390,plain,
transitive_relstr(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3391,plain,
antisymmetric_relstr(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3394,plain,
upper_bounded_relstr(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f3395,plain,
distributive_relstr(sK232_skl),
inference(cnf_transformation,[status(thm)],[f3385]) ).
fof(f4016,plain,
! [A,B] :
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f612]) ).
fof(f4017,plain,
! [X0,X1] :
( disjoint(X1,X0)
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4016]) ).
fof(f4206,plain,
! [X0] : bottom_of_relstr(boole_POSet(X0)) = empty_set,
inference(cnf_transformation,[status(thm)],[f663]) ).
fof(f4219,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f669]) ).
fof(f4220,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4219]) ).
fof(f4340,plain,
! [A,B] :
( set_intersection2(A,B) = A
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f705]) ).
fof(f4341,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4340]) ).
fof(f4357,plain,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f710]) ).
fof(f4370,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f715]) ).
fof(f4479,plain,
! [X0,X1] : set_union2(X0,set_difference(X1,X0)) = set_union2(X0,X1),
inference(cnf_transformation,[status(thm)],[f742]) ).
fof(f4485,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f744]) ).
fof(f4492,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f747]) ).
fof(f4493,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f4492]) ).
fof(f4495,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f4493]) ).
fof(f4505,plain,
! [X0,X1] : set_difference(set_union2(X0,X1),X1) = set_difference(X0,X1),
inference(cnf_transformation,[status(thm)],[f751]) ).
fof(f4536,plain,
! [A] :
( ! [B] :
( related(A,bottom_of_relstr(A),B)
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f760]) ).
fof(f4537,plain,
! [X0,X1] :
( related(X0,bottom_of_relstr(X0),X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f4536]) ).
fof(f4581,plain,
! [X0] : set_difference(empty_set,X0) = empty_set,
inference(cnf_transformation,[status(thm)],[f775]) ).
fof(f4582,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f776]) ).
fof(f4583,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f4582]) ).
fof(f4584,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4583]) ).
fof(f4585,plain,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
inference(cnf_transformation,[status(thm)],[f777]) ).
fof(f4646,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f794]) ).
fof(f4647,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f4646]) ).
fof(f4648,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4647]) ).
fof(f4649,plain,
! [A,B] :
( ( proper_element(B,powerset(A))
<=> B != A )
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f795]) ).
fof(f4650,plain,
! [A,B] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(NNF_transformation,[status(thm)],[f4649]) ).
fof(f4651,plain,
! [X0,X1] :
( X0 != X1
| ~ proper_element(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f4650]) ).
fof(f4652,plain,
! [X0,X1] :
( X0 = X1
| proper_element(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f4650]) ).
fof(f4666,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( related(B,E,F)
| ~ in(F,the_carrier(B))
| ~ in(E,the_carrier(B))
| ~ related(A,C,D)
| F != D
| E != C
| ~ element(F,the_carrier(B)) )
| ~ element(E,the_carrier(B)) )
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ subrelstr(B,A)
| ~ full_subrelstr(B,A) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f802]) ).
fof(f4667,plain,
! [X0,X1,X2,X3,X4,X5] :
( related(X1,X4,X5)
| ~ in(X5,the_carrier(X1))
| ~ in(X4,the_carrier(X1))
| ~ related(X0,X2,X3)
| X5 != X3
| X4 != X2
| ~ element(X5,the_carrier(X1))
| ~ element(X4,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f4666]) ).
fof(f4726,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f820]) ).
fof(f4727,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f4726]) ).
fof(f4728,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4727]) ).
fof(f4743,plain,
! [X0,X1] : subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[status(thm)],[f825]) ).
fof(f4744,plain,
! [A,B] :
( ( set_difference(A,B) != A
| disjoint(A,B) )
& ( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f826]) ).
fof(f4745,plain,
( ! [A,B] :
( set_difference(A,B) != A
| disjoint(A,B) )
& ! [A,B] :
( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f4744]) ).
fof(f4747,plain,
! [X0,X1] :
( set_difference(X0,X1) != X0
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4745]) ).
fof(f4769,plain,
? [A] :
( ? [B] :
( ( proper_element(B,powerset(the_carrier(A)))
<~> ~ in(bottom_of_relstr(A),B) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f833]) ).
fof(f4770,plain,
? [A] :
( ? [B] :
( ( in(bottom_of_relstr(A),B)
| ~ proper_element(B,powerset(the_carrier(A))) )
& ( ~ in(bottom_of_relstr(A),B)
| proper_element(B,powerset(the_carrier(A))) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f4769]) ).
fof(f4771,plain,
( ( in(bottom_of_relstr(sK473_skl),sK474_skl)
| ~ proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) )
& ( ~ in(bottom_of_relstr(sK473_skl),sK474_skl)
| proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) )
& element(sK474_skl,powerset(the_carrier(sK473_skl)))
& upper_relstr_subset(sK474_skl,sK473_skl)
& filtered_subset(sK474_skl,sK473_skl)
& ~ empty(sK474_skl)
& rel_str(sK473_skl)
& lower_bounded_relstr(sK473_skl)
& antisymmetric_relstr(sK473_skl)
& transitive_relstr(sK473_skl)
& reflexive_relstr(sK473_skl)
& ~ empty_carrier(sK473_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK473_skl,sK474_skl]),skolemize(A,sK473_skl),skolemize(B,sK474_skl)],[f4770]) ).
fof(f4772,plain,
~ empty_carrier(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4773,plain,
reflexive_relstr(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4774,plain,
transitive_relstr(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4775,plain,
antisymmetric_relstr(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4776,plain,
lower_bounded_relstr(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4777,plain,
rel_str(sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4778,plain,
~ empty(sK474_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4780,plain,
upper_relstr_subset(sK474_skl,sK473_skl),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4781,plain,
element(sK474_skl,powerset(the_carrier(sK473_skl))),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4782,plain,
( ~ in(bottom_of_relstr(sK473_skl),sK474_skl)
| proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) ),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f4783,plain,
( in(bottom_of_relstr(sK473_skl),sK474_skl)
| ~ proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) ),
inference(cnf_transformation,[status(thm)],[f4771]) ).
fof(f5537,definition,
( sQ35_spl
<=> proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f5538,plain,
( ~ sQ35_spl
| proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) ),
inference(component_clause,[status(thm)],[f5537]) ).
fof(f5540,definition,
( sQ36_spl
<=> in(bottom_of_relstr(sK473_skl),sK474_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f5543,plain,
( ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f4782,f5537,f5540]) ).
fof(f5544,plain,
( sQ36_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f4783,f5537,f5540]) ).
fof(f5669,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1026,f982]) ).
fof(f5675,plain,
! [X0] :
( boolean_relstr(X0)
| ~ complemented_relstr(X0)
| ~ distributive_relstr(X0)
| ~ bounded_relstr(X0)
| ~ with_infima_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f1033]) ).
fof(f5679,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1251]) ).
fof(f5739,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f1606]) ).
fof(f5740,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f1612]) ).
fof(f5811,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f1830,f2191]) ).
fof(f5998,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1619,f4584]) ).
fof(f6022,plain,
! [X1] :
( ~ proper_element(X1,powerset(X1))
| ~ element(X1,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f4651]) ).
fof(f6023,plain,
! [X0] : ~ proper_element(X0,powerset(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f6022,f5811]) ).
fof(f6026,plain,
! [X0,X1,X2,X3] :
( related(X1,X2,X3)
| ~ in(X3,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f4667]) ).
fof(f6027,plain,
! [X0,X1,X2,X3] :
( related(X1,X2,X3)
| ~ in(X3,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6026,f4220]) ).
fof(f6219,definition,
( sQ63_spl
<=> empty_carrier(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f6220,plain,
( ~ sQ63_spl
| empty_carrier(sK473_skl) ),
inference(component_clause,[status(thm)],[f6219]) ).
fof(f6225,definition,
( sQ65_spl
<=> rel_str(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f6227,plain,
( sQ65_spl
| ~ rel_str(sK473_skl) ),
inference(component_clause,[status(thm)],[f6225]) ).
fof(f6238,plain,
( empty(sK474_skl)
| ~ empty(powerset(the_carrier(sK473_skl))) ),
inference(resolution,[status(thm)],[f1679,f4781]) ).
fof(f6239,definition,
( sQ67_spl
<=> empty(sK474_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f6240,plain,
( ~ sQ67_spl
| empty(sK474_skl) ),
inference(component_clause,[status(thm)],[f6239]) ).
fof(f6246,definition,
( sQ69_spl
<=> empty(powerset(the_carrier(sK473_skl))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f6249,plain,
( sQ67_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f6238,f6246,f6239]) ).
fof(f6255,plain,
( one_to_one(empty_set)
| ~ empty(empty_set) ),
inference(resolution,[status(thm)],[f5669,f2545]) ).
fof(f6256,definition,
( sQ70_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f6258,plain,
( sQ70_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f6256]) ).
fof(f6259,definition,
( sQ71_spl
<=> one_to_one(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f6262,plain,
( sQ71_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f6255,f6256,f6259]) ).
fof(f6263,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6258,f2375]) ).
fof(f6264,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f6263]) ).
fof(f6281,plain,
( up_complete_relstr(sK181_skl)
| ~ complete_relstr(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f861,f3056]) ).
fof(f6284,definition,
( sQ76_spl
<=> rel_str(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f6286,plain,
( sQ76_spl
| ~ rel_str(sK181_skl) ),
inference(component_clause,[status(thm)],[f6284]) ).
fof(f6287,definition,
( sQ77_spl
<=> empty_carrier(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f6288,plain,
( ~ sQ77_spl
| empty_carrier(sK181_skl) ),
inference(component_clause,[status(thm)],[f6287]) ).
fof(f6290,definition,
( sQ78_spl
<=> complete_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f6292,plain,
( sQ78_spl
| ~ complete_relstr(sK181_skl) ),
inference(component_clause,[status(thm)],[f6290]) ).
fof(f6293,definition,
( sQ79_spl
<=> up_complete_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f6296,plain,
( sQ79_spl
| ~ sQ78_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f6281,f6284,f6287,f6290,f6293]) ).
fof(f6297,definition,
( sQ80_spl
<=> rel_str(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f6299,plain,
( sQ80_spl
| ~ rel_str(sK179_skl) ),
inference(component_clause,[status(thm)],[f6297]) ).
fof(f6300,definition,
( sQ81_spl
<=> empty_carrier(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f6301,plain,
( ~ sQ81_spl
| empty_carrier(sK179_skl) ),
inference(component_clause,[status(thm)],[f6300]) ).
fof(f6317,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6220,f4772]) ).
fof(f6318,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f6317]) ).
fof(f6319,plain,
( sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6227,f4777]) ).
fof(f6320,plain,
sQ65_spl,
inference(contradiction_clause,[status(thm)],[f6319]) ).
fof(f6321,plain,
( ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6301,f3030]) ).
fof(f6322,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f6321]) ).
fof(f6323,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6299,f3029]) ).
fof(f6324,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f6323]) ).
fof(f6326,plain,
! [X0,X1] :
( v1_xcmplx_0(X1)
| ~ v1_membered(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f857]) ).
fof(f6327,plain,
! [X0,X1] :
( empty(X1)
| ~ empty(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f1679]) ).
fof(f6328,definition,
! [X0] :
( sQ86_spl
<=> ( ~ v1_membered(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f6329,plain,
! [X0] :
( ~ sQ86_spl
| ~ v1_membered(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f6328]) ).
fof(f6331,definition,
! [X1] :
( sQ87_spl
<=> ( v1_xcmplx_0(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f6334,plain,
( sQ87_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f6326,f6328,f6331]) ).
fof(f6335,definition,
! [X0] :
( sQ88_spl
<=> ( ~ empty(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f6336,plain,
! [X0] :
( ~ sQ88_spl
| ~ empty(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f6335]) ).
fof(f6338,definition,
! [X1] :
( sQ89_spl
<=> ( empty(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f6341,plain,
( sQ89_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f6327,f6335,f6338]) ).
fof(f6342,plain,
( ~ sQ88_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f6410]) ).
fof(f6410,plain,
! [X0] :
( ~ sQ88_spl
| ~ empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f6336]) ).
fof(f6411,plain,
~ sQ88_spl,
inference(contradiction_clause,[status(thm)],[f6342]) ).
fof(f6415,plain,
( ~ sQ86_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3115,f6481]) ).
fof(f6481,plain,
! [X0] :
( ~ sQ86_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6329,f918]) ).
fof(f6532,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f6415]) ).
fof(f6550,plain,
( up_complete_relstr(sK186_skl)
| ~ complete_relstr(sK186_skl)
| empty_carrier(sK186_skl)
| ~ rel_str(sK186_skl) ),
inference(resolution,[status(thm)],[f3088,f861]) ).
fof(f6551,definition,
( sQ90_spl
<=> rel_str(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f6553,plain,
( sQ90_spl
| ~ rel_str(sK186_skl) ),
inference(component_clause,[status(thm)],[f6551]) ).
fof(f6554,definition,
( sQ91_spl
<=> empty_carrier(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f6555,plain,
( ~ sQ91_spl
| empty_carrier(sK186_skl) ),
inference(component_clause,[status(thm)],[f6554]) ).
fof(f6557,definition,
( sQ92_spl
<=> complete_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f6559,plain,
( sQ92_spl
| ~ complete_relstr(sK186_skl) ),
inference(component_clause,[status(thm)],[f6557]) ).
fof(f6560,definition,
( sQ93_spl
<=> up_complete_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f6563,plain,
( sQ93_spl
| ~ sQ92_spl
| sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f6550,f6551,f6554,f6557,f6560]) ).
fof(f6564,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6559,f3091]) ).
fof(f6565,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f6564]) ).
fof(f6566,plain,
( ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6555,f3086]) ).
fof(f6567,plain,
~ sQ91_spl,
inference(contradiction_clause,[status(thm)],[f6566]) ).
fof(f6568,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6553,f3085]) ).
fof(f6569,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f6568]) ).
fof(f6570,plain,
( join_complete_relstr(sK186_skl)
| ~ complete_relstr(sK186_skl)
| empty_carrier(sK186_skl)
| ~ rel_str(sK186_skl) ),
inference(resolution,[status(thm)],[f862,f3088]) ).
fof(f6571,plain,
( join_complete_relstr(sK181_skl)
| ~ complete_relstr(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f862,f3056]) ).
fof(f6574,definition,
( sQ94_spl
<=> join_complete_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f6577,plain,
( sQ94_spl
| ~ sQ92_spl
| sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f6570,f6551,f6554,f6557,f6574]) ).
fof(f6578,definition,
( sQ95_spl
<=> join_complete_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f6581,plain,
( sQ95_spl
| ~ sQ78_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f6571,f6284,f6287,f6290,f6578]) ).
fof(f6590,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6292,f3061]) ).
fof(f6591,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f6590]) ).
fof(f6592,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6288,f3054]) ).
fof(f6593,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f6592]) ).
fof(f6594,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6286,f3053]) ).
fof(f6595,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f6594]) ).
fof(f6615,plain,
! [X0] :
( in(X0,the_carrier(sK473_skl))
| ~ in(X0,sK474_skl) ),
inference(resolution,[status(thm)],[f2932,f4781]) ).
fof(f6616,plain,
( join_complete_relstr(sK197_skl)
| ~ complete_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f3139,f862]) ).
fof(f6617,plain,
( up_complete_relstr(sK197_skl)
| ~ complete_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f3139,f861]) ).
fof(f6618,definition,
( sQ99_spl
<=> rel_str(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f6620,plain,
( sQ99_spl
| ~ rel_str(sK197_skl) ),
inference(component_clause,[status(thm)],[f6618]) ).
fof(f6621,definition,
( sQ100_spl
<=> empty_carrier(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f6622,plain,
( ~ sQ100_spl
| empty_carrier(sK197_skl) ),
inference(component_clause,[status(thm)],[f6621]) ).
fof(f6624,definition,
( sQ101_spl
<=> complete_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f6626,plain,
( sQ101_spl
| ~ complete_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f6624]) ).
fof(f6627,definition,
( sQ102_spl
<=> join_complete_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f6630,plain,
( sQ102_spl
| ~ sQ101_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f6616,f6618,f6621,f6624,f6627]) ).
fof(f6631,definition,
( sQ103_spl
<=> up_complete_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f6634,plain,
( sQ103_spl
| ~ sQ101_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f6617,f6618,f6621,f6624,f6631]) ).
fof(f6635,plain,
( sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6626,f3144]) ).
fof(f6636,plain,
sQ101_spl,
inference(contradiction_clause,[status(thm)],[f6635]) ).
fof(f6637,plain,
( ~ sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6622,f3138]) ).
fof(f6638,plain,
~ sQ100_spl,
inference(contradiction_clause,[status(thm)],[f6637]) ).
fof(f6639,plain,
( sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6620,f3137]) ).
fof(f6640,plain,
sQ99_spl,
inference(contradiction_clause,[status(thm)],[f6639]) ).
fof(f6641,plain,
( join_complete_relstr(sK198_skl)
| ~ complete_relstr(sK198_skl)
| empty_carrier(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f3155,f862]) ).
fof(f6643,definition,
( sQ104_spl
<=> rel_str(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f6645,plain,
( sQ104_spl
| ~ rel_str(sK198_skl) ),
inference(component_clause,[status(thm)],[f6643]) ).
fof(f6646,definition,
( sQ105_spl
<=> empty_carrier(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f6647,plain,
( ~ sQ105_spl
| empty_carrier(sK198_skl) ),
inference(component_clause,[status(thm)],[f6646]) ).
fof(f6649,definition,
( sQ106_spl
<=> complete_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f6651,plain,
( sQ106_spl
| ~ complete_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f6649]) ).
fof(f6652,definition,
( sQ107_spl
<=> join_complete_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f6655,plain,
( sQ107_spl
| ~ sQ106_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f6641,f6643,f6646,f6649,f6652]) ).
fof(f6656,definition,
( sQ108_spl
<=> up_complete_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f6660,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6651,f3165]) ).
fof(f6661,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f6660]) ).
fof(f6662,plain,
( ~ sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6647,f3153]) ).
fof(f6663,plain,
~ sQ105_spl,
inference(contradiction_clause,[status(thm)],[f6662]) ).
fof(f6664,plain,
( sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6645,f3152]) ).
fof(f6665,plain,
sQ104_spl,
inference(contradiction_clause,[status(thm)],[f6664]) ).
fof(f6668,definition,
( sQ109_spl
<=> rel_str(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f6670,plain,
( sQ109_spl
| ~ rel_str(sK199_skl) ),
inference(component_clause,[status(thm)],[f6668]) ).
fof(f6671,definition,
( sQ110_spl
<=> empty_carrier(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f6672,plain,
( ~ sQ110_spl
| empty_carrier(sK199_skl) ),
inference(component_clause,[status(thm)],[f6671]) ).
fof(f6710,definition,
( sQ118_spl
<=> element(bottom_of_relstr(sK473_skl),sK474_skl) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f6711,plain,
( ~ sQ118_spl
| element(bottom_of_relstr(sK473_skl),sK474_skl) ),
inference(component_clause,[status(thm)],[f6710]) ).
fof(f6762,plain,
! [X0] :
( element(empty_set,the_carrier(boole_POSet(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f4206,f2214]) ).
fof(f6763,plain,
! [X0] :
( element(empty_set,powerset(X0))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f4585,f6762]) ).
fof(f6766,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f6763,f2217]) ).
fof(f6767,plain,
( join_complete_relstr(sK201_skl)
| ~ complete_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f3193,f862]) ).
fof(f6768,plain,
( up_complete_relstr(sK201_skl)
| ~ complete_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f3193,f861]) ).
fof(f6769,definition,
( sQ125_spl
<=> rel_str(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f6771,plain,
( sQ125_spl
| ~ rel_str(sK201_skl) ),
inference(component_clause,[status(thm)],[f6769]) ).
fof(f6772,definition,
( sQ126_spl
<=> empty_carrier(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f6773,plain,
( ~ sQ126_spl
| empty_carrier(sK201_skl) ),
inference(component_clause,[status(thm)],[f6772]) ).
fof(f6775,definition,
( sQ127_spl
<=> complete_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f6777,plain,
( sQ127_spl
| ~ complete_relstr(sK201_skl) ),
inference(component_clause,[status(thm)],[f6775]) ).
fof(f6778,definition,
( sQ128_spl
<=> join_complete_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f6781,plain,
( sQ128_spl
| ~ sQ127_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f6767,f6769,f6772,f6775,f6778]) ).
fof(f6782,definition,
( sQ129_spl
<=> up_complete_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f6785,plain,
( sQ129_spl
| ~ sQ127_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f6768,f6769,f6772,f6775,f6782]) ).
fof(f6786,plain,
( sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6777,f3198]) ).
fof(f6787,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f6786]) ).
fof(f6788,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6773,f3191]) ).
fof(f6789,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f6788]) ).
fof(f6790,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6771,f3190]) ).
fof(f6791,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f6790]) ).
fof(f6794,definition,
( sQ130_spl
<=> rel_str(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f6796,plain,
( sQ130_spl
| ~ rel_str(sK202_skl) ),
inference(component_clause,[status(thm)],[f6794]) ).
fof(f6797,definition,
( sQ131_spl
<=> empty_carrier(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f6798,plain,
( ~ sQ131_spl
| empty_carrier(sK202_skl) ),
inference(component_clause,[status(thm)],[f6797]) ).
fof(f6811,plain,
( ~ sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6798,f3202]) ).
fof(f6812,plain,
~ sQ131_spl,
inference(contradiction_clause,[status(thm)],[f6811]) ).
fof(f6813,plain,
( sQ130_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6796,f3201]) ).
fof(f6814,plain,
sQ130_spl,
inference(contradiction_clause,[status(thm)],[f6813]) ).
fof(f6816,plain,
! [X0] :
( element(X0,the_carrier(sK473_skl))
| ~ in(X0,sK474_skl) ),
inference(resolution,[status(thm)],[f6615,f4220]) ).
fof(f6817,plain,
! [X0] :
( ~ in(the_carrier(sK473_skl),X0)
| ~ in(X0,sK474_skl) ),
inference(resolution,[status(thm)],[f6615,f853]) ).
fof(f6856,plain,
( in(sK474_skl,powerset(the_carrier(sK473_skl)))
| empty(powerset(the_carrier(sK473_skl))) ),
inference(resolution,[status(thm)],[f1677,f4781]) ).
fof(f6861,definition,
( sQ140_spl
<=> in(sK474_skl,powerset(the_carrier(sK473_skl))) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f6862,plain,
( ~ sQ140_spl
| in(sK474_skl,powerset(the_carrier(sK473_skl))) ),
inference(component_clause,[status(thm)],[f6861]) ).
fof(f6864,plain,
( sQ140_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f6856,f6246,f6861]) ).
fof(f6881,plain,
( join_complete_relstr(sK206_skl)
| ~ complete_relstr(sK206_skl)
| empty_carrier(sK206_skl)
| ~ rel_str(sK206_skl) ),
inference(resolution,[status(thm)],[f3235,f862]) ).
fof(f6882,plain,
( up_complete_relstr(sK206_skl)
| ~ complete_relstr(sK206_skl)
| empty_carrier(sK206_skl)
| ~ rel_str(sK206_skl) ),
inference(resolution,[status(thm)],[f3235,f861]) ).
fof(f6883,definition,
( sQ141_spl
<=> rel_str(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f6885,plain,
( sQ141_spl
| ~ rel_str(sK206_skl) ),
inference(component_clause,[status(thm)],[f6883]) ).
fof(f6886,definition,
( sQ142_spl
<=> empty_carrier(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f6887,plain,
( ~ sQ142_spl
| empty_carrier(sK206_skl) ),
inference(component_clause,[status(thm)],[f6886]) ).
fof(f6889,definition,
( sQ143_spl
<=> complete_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f6891,plain,
( sQ143_spl
| ~ complete_relstr(sK206_skl) ),
inference(component_clause,[status(thm)],[f6889]) ).
fof(f6892,definition,
( sQ144_spl
<=> join_complete_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f6895,plain,
( sQ144_spl
| ~ sQ143_spl
| sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f6881,f6883,f6886,f6889,f6892]) ).
fof(f6896,definition,
( sQ145_spl
<=> up_complete_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f6899,plain,
( sQ145_spl
| ~ sQ143_spl
| sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f6882,f6883,f6886,f6889,f6896]) ).
fof(f6900,plain,
( sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6891,f3240]) ).
fof(f6901,plain,
sQ143_spl,
inference(contradiction_clause,[status(thm)],[f6900]) ).
fof(f6902,plain,
( ~ sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6887,f3233]) ).
fof(f6903,plain,
~ sQ142_spl,
inference(contradiction_clause,[status(thm)],[f6902]) ).
fof(f6904,plain,
( sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6885,f3232]) ).
fof(f6905,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f6904]) ).
fof(f6908,definition,
( sQ146_spl
<=> rel_str(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f6910,plain,
( sQ146_spl
| ~ rel_str(sK207_skl) ),
inference(component_clause,[status(thm)],[f6908]) ).
fof(f6911,definition,
( sQ147_spl
<=> empty_carrier(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f6912,plain,
( ~ sQ147_spl
| empty_carrier(sK207_skl) ),
inference(component_clause,[status(thm)],[f6911]) ).
fof(f6925,plain,
( ~ sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6912,f3243]) ).
fof(f6926,plain,
~ sQ147_spl,
inference(contradiction_clause,[status(thm)],[f6925]) ).
fof(f6927,plain,
( sQ146_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6910,f3242]) ).
fof(f6928,plain,
sQ146_spl,
inference(contradiction_clause,[status(thm)],[f6927]) ).
fof(f6946,definition,
! [X0] :
( sQ154_spl
<=> ( ~ empty(X0)
| ~ v2_membered(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f6947,plain,
! [X0] :
( ~ sQ154_spl
| ~ empty(X0)
| ~ v2_membered(X0) ),
inference(component_clause,[status(thm)],[f6946]) ).
fof(f6954,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ empty(X0)
| v1_xreal_0(X1)
| ~ v2_membered(X0) ),
inference(resolution,[status(thm)],[f875,f1680]) ).
fof(f6967,definition,
! [X1] :
( sQ158_spl
<=> ( ~ empty(X1)
| v1_xreal_0(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f6970,plain,
( sQ158_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f6954,f6946,f6967]) ).
fof(f6973,plain,
( ~ sQ154_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f7041]) ).
fof(f7041,plain,
! [X0] :
( ~ sQ154_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6947,f919]) ).
fof(f7044,plain,
! [X0,X1,X2,X3] :
( related(X1,X2,X3)
| ~ in(X3,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ full_subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6027,f4220]) ).
fof(f7046,plain,
( lower_bounded_relstr(sK206_skl)
| ~ join_complete_relstr(sK206_skl)
| empty_carrier(sK206_skl)
| ~ rel_str(sK206_skl) ),
inference(resolution,[status(thm)],[f879,f3235]) ).
fof(f7048,plain,
( lower_bounded_relstr(sK201_skl)
| ~ join_complete_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f879,f3193]) ).
fof(f7050,plain,
( lower_bounded_relstr(sK198_skl)
| ~ join_complete_relstr(sK198_skl)
| empty_carrier(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f879,f3155]) ).
fof(f7051,plain,
( lower_bounded_relstr(sK197_skl)
| ~ join_complete_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f879,f3139]) ).
fof(f7052,plain,
( lower_bounded_relstr(sK186_skl)
| ~ join_complete_relstr(sK186_skl)
| empty_carrier(sK186_skl)
| ~ rel_str(sK186_skl) ),
inference(resolution,[status(thm)],[f879,f3088]) ).
fof(f7053,plain,
( lower_bounded_relstr(sK181_skl)
| ~ join_complete_relstr(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f879,f3056]) ).
fof(f7060,definition,
( sQ160_spl
<=> lower_bounded_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f7063,plain,
( sQ160_spl
| ~ sQ144_spl
| sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f7046,f6883,f6886,f6892,f7060]) ).
fof(f7068,definition,
( sQ162_spl
<=> lower_bounded_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f7071,plain,
( sQ162_spl
| ~ sQ128_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f7048,f6769,f6772,f6778,f7068]) ).
fof(f7072,definition,
( sQ163_spl
<=> lower_bounded_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f7074,plain,
( sQ163_spl
| ~ lower_bounded_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f7072]) ).
fof(f7076,definition,
( sQ164_spl
<=> lower_bounded_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f7079,plain,
( sQ164_spl
| ~ sQ107_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f7050,f6643,f6646,f6652,f7076]) ).
fof(f7080,definition,
( sQ165_spl
<=> lower_bounded_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f7083,plain,
( sQ165_spl
| ~ sQ102_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f7051,f6618,f6621,f6627,f7080]) ).
fof(f7084,definition,
( sQ166_spl
<=> lower_bounded_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f7087,plain,
( sQ166_spl
| ~ sQ94_spl
| sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f7052,f6551,f6554,f6574,f7084]) ).
fof(f7088,definition,
( sQ167_spl
<=> lower_bounded_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f7091,plain,
( sQ167_spl
| ~ sQ95_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f7053,f6284,f6287,f6578,f7088]) ).
fof(f7096,definition,
( sQ169_spl
<=> lower_bounded_relstr(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f7098,plain,
( sQ169_spl
| ~ lower_bounded_relstr(sK473_skl) ),
inference(component_clause,[status(thm)],[f7096]) ).
fof(f7100,plain,
( ~ sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6672,f3171]) ).
fof(f7101,plain,
~ sQ110_spl,
inference(contradiction_clause,[status(thm)],[f7100]) ).
fof(f7102,plain,
~ sQ154_spl,
inference(contradiction_clause,[status(thm)],[f6973]) ).
fof(f7103,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6670,f3170]) ).
fof(f7104,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f7103]) ).
fof(f7111,definition,
( sQ170_spl
<=> in(the_carrier(sK473_skl),sK474_skl) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f7147,plain,
( sK474_skl = the_carrier(sK473_skl)
| proper_element(sK474_skl,powerset(the_carrier(sK473_skl))) ),
inference(resolution,[status(thm)],[f4652,f4781]) ).
fof(f7148,definition,
( sQ176_spl
<=> sK474_skl = the_carrier(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f7149,plain,
( ~ sQ176_spl
| sK474_skl = the_carrier(sK473_skl) ),
inference(component_clause,[status(thm)],[f7148]) ).
fof(f7151,plain,
( sQ176_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f7147,f5537,f7148]) ).
fof(f7152,plain,
( lower_bounded_relstr(sK215_skl)
| ~ join_complete_relstr(sK215_skl)
| empty_carrier(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f3285,f879]) ).
fof(f7153,plain,
( join_complete_relstr(sK215_skl)
| ~ complete_relstr(sK215_skl)
| empty_carrier(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f3285,f862]) ).
fof(f7155,definition,
( sQ177_spl
<=> rel_str(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f7157,plain,
( sQ177_spl
| ~ rel_str(sK215_skl) ),
inference(component_clause,[status(thm)],[f7155]) ).
fof(f7158,definition,
( sQ178_spl
<=> empty_carrier(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f7159,plain,
( ~ sQ178_spl
| empty_carrier(sK215_skl) ),
inference(component_clause,[status(thm)],[f7158]) ).
fof(f7161,definition,
( sQ179_spl
<=> join_complete_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f7164,definition,
( sQ180_spl
<=> lower_bounded_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f7167,plain,
( sQ180_spl
| ~ sQ179_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f7152,f7155,f7158,f7161,f7164]) ).
fof(f7168,definition,
( sQ181_spl
<=> complete_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f7170,plain,
( sQ181_spl
| ~ complete_relstr(sK215_skl) ),
inference(component_clause,[status(thm)],[f7168]) ).
fof(f7171,plain,
( sQ179_spl
| ~ sQ181_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f7153,f7155,f7158,f7168,f7161]) ).
fof(f7172,definition,
( sQ182_spl
<=> up_complete_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f7176,plain,
( ~ sQ178_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7159,f3283]) ).
fof(f7177,plain,
~ sQ178_spl,
inference(contradiction_clause,[status(thm)],[f7176]) ).
fof(f7178,plain,
( sQ177_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7157,f3282]) ).
fof(f7179,plain,
sQ177_spl,
inference(contradiction_clause,[status(thm)],[f7178]) ).
fof(f7180,plain,
( sQ181_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7170,f3290]) ).
fof(f7181,plain,
sQ181_spl,
inference(contradiction_clause,[status(thm)],[f7180]) ).
fof(f7182,plain,
( lower_bounded_relstr(sK218_skl)
| ~ join_complete_relstr(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f3307,f879]) ).
fof(f7183,plain,
( join_complete_relstr(sK218_skl)
| ~ complete_relstr(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f3307,f862]) ).
fof(f7184,plain,
( up_complete_relstr(sK218_skl)
| ~ complete_relstr(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f3307,f861]) ).
fof(f7185,definition,
( sQ183_spl
<=> rel_str(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f7187,plain,
( sQ183_spl
| ~ rel_str(sK218_skl) ),
inference(component_clause,[status(thm)],[f7185]) ).
fof(f7188,definition,
( sQ184_spl
<=> empty_carrier(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f7189,plain,
( ~ sQ184_spl
| empty_carrier(sK218_skl) ),
inference(component_clause,[status(thm)],[f7188]) ).
fof(f7191,definition,
( sQ185_spl
<=> join_complete_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f7194,definition,
( sQ186_spl
<=> lower_bounded_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f7197,plain,
( sQ186_spl
| ~ sQ185_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7182,f7185,f7188,f7191,f7194]) ).
fof(f7198,definition,
( sQ187_spl
<=> complete_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f7200,plain,
( sQ187_spl
| ~ complete_relstr(sK218_skl) ),
inference(component_clause,[status(thm)],[f7198]) ).
fof(f7201,plain,
( sQ185_spl
| ~ sQ187_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7183,f7185,f7188,f7198,f7191]) ).
fof(f7202,definition,
( sQ188_spl
<=> up_complete_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f7205,plain,
( sQ188_spl
| ~ sQ187_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7184,f7185,f7188,f7198,f7202]) ).
fof(f7206,plain,
( ~ sQ184_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7189,f3306]) ).
fof(f7207,plain,
~ sQ184_spl,
inference(contradiction_clause,[status(thm)],[f7206]) ).
fof(f7208,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7187,f3305]) ).
fof(f7209,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f7208]) ).
fof(f7210,plain,
( sQ187_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7200,f3312]) ).
fof(f7211,plain,
sQ187_spl,
inference(contradiction_clause,[status(thm)],[f7210]) ).
fof(f7263,plain,
( ~ in(the_carrier(sK473_skl),sK474_skl)
| ~ in(the_carrier(sK473_skl),sK474_skl) ),
inference(resolution,[status(thm)],[f6817,f6615]) ).
fof(f7264,plain,
~ sQ170_spl,
inference(split_clause,[status(thm)],[f7263,f7111]) ).
fof(f7276,plain,
! [X0,X1] :
( v1_rat_1(X1)
| ~ v3_membered(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f883]) ).
fof(f7283,definition,
! [X0] :
( sQ197_spl
<=> ( ~ v3_membered(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f7284,plain,
! [X0] :
( ~ sQ197_spl
| ~ v3_membered(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f7283]) ).
fof(f7286,definition,
! [X1] :
( sQ198_spl
<=> ( v1_rat_1(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f7289,plain,
( sQ198_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f7276,f7283,f7286]) ).
fof(f7295,plain,
( ~ sQ197_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f7364]) ).
fof(f7364,plain,
! [X0] :
( ~ sQ197_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7284,f920]) ).
fof(f7365,plain,
~ sQ197_spl,
inference(contradiction_clause,[status(thm)],[f7295]) ).
fof(f7370,definition,
( sQ199_spl
<=> rel_str(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f7372,plain,
( sQ199_spl
| ~ rel_str(sK230_skl) ),
inference(component_clause,[status(thm)],[f7370]) ).
fof(f7373,definition,
( sQ200_spl
<=> empty_carrier(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f7374,plain,
( ~ sQ200_spl
| empty_carrier(sK230_skl) ),
inference(component_clause,[status(thm)],[f7373]) ).
fof(f7379,definition,
( sQ202_spl
<=> lower_bounded_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f7381,plain,
( sQ202_spl
| ~ lower_bounded_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7379]) ).
fof(f7391,plain,
( ~ sQ200_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7374,f3367]) ).
fof(f7392,plain,
~ sQ200_spl,
inference(contradiction_clause,[status(thm)],[f7391]) ).
fof(f7393,plain,
( sQ199_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7372,f3366]) ).
fof(f7394,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f7393]) ).
fof(f7398,definition,
( sQ205_spl
<=> rel_str(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f7400,plain,
( sQ205_spl
| ~ rel_str(sK232_skl) ),
inference(component_clause,[status(thm)],[f7398]) ).
fof(f7401,definition,
( sQ206_spl
<=> empty_carrier(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f7402,plain,
( ~ sQ206_spl
| empty_carrier(sK232_skl) ),
inference(component_clause,[status(thm)],[f7401]) ).
fof(f7419,plain,
( ~ sQ206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7402,f3387]) ).
fof(f7420,plain,
~ sQ206_spl,
inference(contradiction_clause,[status(thm)],[f7419]) ).
fof(f7421,plain,
( sQ205_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7400,f3386]) ).
fof(f7422,plain,
sQ205_spl,
inference(contradiction_clause,[status(thm)],[f7421]) ).
fof(f7497,plain,
( with_infima_relstr(sK218_skl)
| ~ join_complete_relstr(sK218_skl)
| ~ antisymmetric_relstr(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f904,f3307]) ).
fof(f7498,plain,
( with_infima_relstr(sK215_skl)
| ~ join_complete_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| empty_carrier(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f904,f3285]) ).
fof(f7500,plain,
( with_infima_relstr(sK206_skl)
| ~ join_complete_relstr(sK206_skl)
| ~ antisymmetric_relstr(sK206_skl)
| empty_carrier(sK206_skl)
| ~ rel_str(sK206_skl) ),
inference(resolution,[status(thm)],[f904,f3235]) ).
fof(f7502,plain,
( with_infima_relstr(sK201_skl)
| ~ join_complete_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f904,f3193]) ).
fof(f7504,plain,
( with_infima_relstr(sK198_skl)
| ~ join_complete_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| empty_carrier(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f904,f3155]) ).
fof(f7505,plain,
( with_infima_relstr(sK197_skl)
| ~ join_complete_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f904,f3139]) ).
fof(f7506,plain,
( with_infima_relstr(sK186_skl)
| ~ join_complete_relstr(sK186_skl)
| ~ antisymmetric_relstr(sK186_skl)
| empty_carrier(sK186_skl)
| ~ rel_str(sK186_skl) ),
inference(resolution,[status(thm)],[f904,f3088]) ).
fof(f7507,plain,
( with_infima_relstr(sK181_skl)
| ~ join_complete_relstr(sK181_skl)
| ~ antisymmetric_relstr(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f904,f3056]) ).
fof(f7525,definition,
( sQ219_spl
<=> antisymmetric_relstr(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f7527,plain,
( sQ219_spl
| ~ antisymmetric_relstr(sK232_skl) ),
inference(component_clause,[status(thm)],[f7525]) ).
fof(f7532,definition,
( sQ221_spl
<=> antisymmetric_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f7534,plain,
( sQ221_spl
| ~ antisymmetric_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7532]) ).
fof(f7535,definition,
( sQ222_spl
<=> with_infima_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f7537,plain,
( sQ222_spl
| ~ with_infima_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7535]) ).
fof(f7539,definition,
( sQ223_spl
<=> antisymmetric_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f7541,plain,
( sQ223_spl
| ~ antisymmetric_relstr(sK218_skl) ),
inference(component_clause,[status(thm)],[f7539]) ).
fof(f7542,definition,
( sQ224_spl
<=> with_infima_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f7545,plain,
( sQ224_spl
| ~ sQ185_spl
| ~ sQ223_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7497,f7185,f7188,f7539,f7191,f7542]) ).
fof(f7546,definition,
( sQ225_spl
<=> antisymmetric_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f7548,plain,
( sQ225_spl
| ~ antisymmetric_relstr(sK215_skl) ),
inference(component_clause,[status(thm)],[f7546]) ).
fof(f7549,definition,
( sQ226_spl
<=> with_infima_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f7552,plain,
( sQ226_spl
| ~ sQ179_spl
| ~ sQ225_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f7498,f7155,f7158,f7546,f7161,f7549]) ).
fof(f7553,definition,
( sQ227_spl
<=> antisymmetric_relstr(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f7555,plain,
( sQ227_spl
| ~ antisymmetric_relstr(sK207_skl) ),
inference(component_clause,[status(thm)],[f7553]) ).
fof(f7560,definition,
( sQ229_spl
<=> antisymmetric_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f7562,plain,
( sQ229_spl
| ~ antisymmetric_relstr(sK206_skl) ),
inference(component_clause,[status(thm)],[f7560]) ).
fof(f7563,definition,
( sQ230_spl
<=> with_infima_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f7566,plain,
( sQ230_spl
| ~ sQ144_spl
| ~ sQ229_spl
| sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f7500,f6883,f6886,f7560,f6892,f7563]) ).
fof(f7567,definition,
( sQ231_spl
<=> antisymmetric_relstr(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f7569,plain,
( sQ231_spl
| ~ antisymmetric_relstr(sK202_skl) ),
inference(component_clause,[status(thm)],[f7567]) ).
fof(f7574,definition,
( sQ233_spl
<=> antisymmetric_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f7576,plain,
( sQ233_spl
| ~ antisymmetric_relstr(sK201_skl) ),
inference(component_clause,[status(thm)],[f7574]) ).
fof(f7577,definition,
( sQ234_spl
<=> with_infima_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f7580,plain,
( sQ234_spl
| ~ sQ128_spl
| ~ sQ233_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f7502,f6769,f6772,f7574,f6778,f7577]) ).
fof(f7581,definition,
( sQ235_spl
<=> antisymmetric_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f7583,plain,
( sQ235_spl
| ~ antisymmetric_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f7581]) ).
fof(f7584,definition,
( sQ236_spl
<=> with_infima_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f7586,plain,
( sQ236_spl
| ~ with_infima_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f7584]) ).
fof(f7588,definition,
( sQ237_spl
<=> antisymmetric_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f7590,plain,
( sQ237_spl
| ~ antisymmetric_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f7588]) ).
fof(f7591,definition,
( sQ238_spl
<=> with_infima_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f7594,plain,
( sQ238_spl
| ~ sQ107_spl
| ~ sQ237_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f7504,f6643,f6646,f7588,f6652,f7591]) ).
fof(f7595,definition,
( sQ239_spl
<=> antisymmetric_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f7597,plain,
( sQ239_spl
| ~ antisymmetric_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f7595]) ).
fof(f7598,definition,
( sQ240_spl
<=> with_infima_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f7601,plain,
( sQ240_spl
| ~ sQ102_spl
| ~ sQ239_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f7505,f6618,f6621,f7595,f6627,f7598]) ).
fof(f7602,definition,
( sQ241_spl
<=> antisymmetric_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f7604,plain,
( sQ241_spl
| ~ antisymmetric_relstr(sK186_skl) ),
inference(component_clause,[status(thm)],[f7602]) ).
fof(f7605,definition,
( sQ242_spl
<=> with_infima_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f7608,plain,
( sQ242_spl
| ~ sQ94_spl
| ~ sQ241_spl
| sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f7506,f6551,f6554,f7602,f6574,f7605]) ).
fof(f7609,definition,
( sQ243_spl
<=> antisymmetric_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f7611,plain,
( sQ243_spl
| ~ antisymmetric_relstr(sK181_skl) ),
inference(component_clause,[status(thm)],[f7609]) ).
fof(f7612,definition,
( sQ244_spl
<=> with_infima_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f7615,plain,
( sQ244_spl
| ~ sQ95_spl
| ~ sQ243_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f7507,f6284,f6287,f7609,f6578,f7612]) ).
fof(f7616,definition,
( sQ245_spl
<=> antisymmetric_relstr(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f7618,plain,
( sQ245_spl
| ~ antisymmetric_relstr(sK179_skl) ),
inference(component_clause,[status(thm)],[f7616]) ).
fof(f7623,definition,
( sQ247_spl
<=> antisymmetric_relstr(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f7625,plain,
( sQ247_spl
| ~ antisymmetric_relstr(sK473_skl) ),
inference(component_clause,[status(thm)],[f7623]) ).
fof(f7630,definition,
( sQ249_spl
<=> reflexive_relstr(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f7632,plain,
( sQ249_spl
| ~ reflexive_relstr(sK232_skl) ),
inference(component_clause,[status(thm)],[f7630]) ).
fof(f7634,definition,
( sQ250_spl
<=> reflexive_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f7636,plain,
( sQ250_spl
| ~ reflexive_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7634]) ).
fof(f7638,definition,
( sQ251_spl
<=> reflexive_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f7640,plain,
( sQ251_spl
| ~ reflexive_relstr(sK218_skl) ),
inference(component_clause,[status(thm)],[f7638]) ).
fof(f7642,definition,
( sQ252_spl
<=> reflexive_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f7644,plain,
( sQ252_spl
| ~ reflexive_relstr(sK215_skl) ),
inference(component_clause,[status(thm)],[f7642]) ).
fof(f7646,definition,
( sQ253_spl
<=> reflexive_relstr(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f7648,plain,
( sQ253_spl
| ~ reflexive_relstr(sK207_skl) ),
inference(component_clause,[status(thm)],[f7646]) ).
fof(f7650,definition,
( sQ254_spl
<=> reflexive_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f7652,plain,
( sQ254_spl
| ~ reflexive_relstr(sK206_skl) ),
inference(component_clause,[status(thm)],[f7650]) ).
fof(f7654,definition,
( sQ255_spl
<=> reflexive_relstr(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f7656,plain,
( sQ255_spl
| ~ reflexive_relstr(sK202_skl) ),
inference(component_clause,[status(thm)],[f7654]) ).
fof(f7658,definition,
( sQ256_spl
<=> reflexive_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f7660,plain,
( sQ256_spl
| ~ reflexive_relstr(sK201_skl) ),
inference(component_clause,[status(thm)],[f7658]) ).
fof(f7662,definition,
( sQ257_spl
<=> reflexive_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f7664,plain,
( sQ257_spl
| ~ reflexive_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f7662]) ).
fof(f7666,definition,
( sQ258_spl
<=> reflexive_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f7668,plain,
( sQ258_spl
| ~ reflexive_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f7666]) ).
fof(f7670,definition,
( sQ259_spl
<=> reflexive_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f7672,plain,
( sQ259_spl
| ~ reflexive_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f7670]) ).
fof(f7674,definition,
( sQ260_spl
<=> reflexive_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f7676,plain,
( sQ260_spl
| ~ reflexive_relstr(sK186_skl) ),
inference(component_clause,[status(thm)],[f7674]) ).
fof(f7678,definition,
( sQ261_spl
<=> reflexive_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition]) ).
fof(f7680,plain,
( sQ261_spl
| ~ reflexive_relstr(sK181_skl) ),
inference(component_clause,[status(thm)],[f7678]) ).
fof(f7682,definition,
( sQ262_spl
<=> reflexive_relstr(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f7684,plain,
( sQ262_spl
| ~ reflexive_relstr(sK179_skl) ),
inference(component_clause,[status(thm)],[f7682]) ).
fof(f7686,definition,
( sQ263_spl
<=> reflexive_relstr(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f7688,plain,
( sQ263_spl
| ~ reflexive_relstr(sK473_skl) ),
inference(component_clause,[status(thm)],[f7686]) ).
fof(f7723,plain,
! [X0,X1] :
( v1_int_1(X1)
| ~ v4_membered(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f898]) ).
fof(f7733,definition,
! [X0] :
( sQ269_spl
<=> ( ~ v5_membered(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f7734,plain,
! [X0] :
( ~ sQ269_spl
| ~ v5_membered(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f7733]) ).
fof(f7737,definition,
! [X0] :
( sQ270_spl
<=> ( ~ v4_membered(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f7738,plain,
! [X0] :
( ~ sQ270_spl
| ~ v4_membered(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f7737]) ).
fof(f7741,definition,
! [X1] :
( sQ271_spl
<=> ( v1_int_1(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f7744,plain,
( sQ271_spl
| sQ270_spl ),
inference(split_clause,[status(thm)],[f7723,f7737,f7741]) ).
fof(f7753,plain,
( ~ sQ270_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f7822]) ).
fof(f7822,plain,
! [X0] :
( ~ sQ270_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7738,f921]) ).
fof(f7823,plain,
~ sQ270_spl,
inference(contradiction_clause,[status(thm)],[f7753]) ).
fof(f7907,plain,
! [X0,X1] :
( in(X0,sK474_skl)
| ~ related(sK473_skl,X1,X0)
| ~ in(X1,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl))
| ~ upper_relstr_subset(sK474_skl,sK473_skl)
| ~ rel_str(sK473_skl) ),
inference(resolution,[status(thm)],[f5998,f4781]) ).
fof(f7908,definition,
( sQ277_spl
<=> upper_relstr_subset(sK474_skl,sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f7910,plain,
( sQ277_spl
| ~ upper_relstr_subset(sK474_skl,sK473_skl) ),
inference(component_clause,[status(thm)],[f7908]) ).
fof(f7911,definition,
! [X0,X1] :
( sQ278_spl
<=> ( in(X0,sK474_skl)
| ~ related(sK473_skl,X1,X0)
| ~ in(X1,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f7912,plain,
! [X0,X1] :
( ~ sQ278_spl
| in(X0,sK474_skl)
| ~ related(sK473_skl,X1,X0)
| ~ in(X1,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ),
inference(component_clause,[status(thm)],[f7911]) ).
fof(f7914,plain,
( sQ278_spl
| ~ sQ277_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f7907,f6225,f7908,f7911]) ).
fof(f7915,plain,
( sQ277_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7910,f4780]) ).
fof(f7916,plain,
sQ277_spl,
inference(contradiction_clause,[status(thm)],[f7915]) ).
fof(f7957,plain,
( with_suprema_relstr(sK218_skl)
| ~ join_complete_relstr(sK218_skl)
| ~ upper_bounded_relstr(sK218_skl)
| ~ antisymmetric_relstr(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f915,f3307]) ).
fof(f7958,plain,
( with_suprema_relstr(sK215_skl)
| ~ join_complete_relstr(sK215_skl)
| ~ upper_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| empty_carrier(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f915,f3285]) ).
fof(f7964,plain,
( with_suprema_relstr(sK198_skl)
| ~ join_complete_relstr(sK198_skl)
| ~ upper_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| empty_carrier(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f915,f3155]) ).
fof(f7965,plain,
( with_suprema_relstr(sK197_skl)
| ~ join_complete_relstr(sK197_skl)
| ~ upper_bounded_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f915,f3139]) ).
fof(f7967,plain,
( with_suprema_relstr(sK181_skl)
| ~ join_complete_relstr(sK181_skl)
| ~ upper_bounded_relstr(sK181_skl)
| ~ antisymmetric_relstr(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f915,f3056]) ).
fof(f7987,definition,
( sQ279_spl
<=> upper_bounded_relstr(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f7989,plain,
( sQ279_spl
| ~ upper_bounded_relstr(sK232_skl) ),
inference(component_clause,[status(thm)],[f7987]) ).
fof(f7994,definition,
( sQ281_spl
<=> upper_bounded_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition]) ).
fof(f7996,plain,
( sQ281_spl
| ~ upper_bounded_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7994]) ).
fof(f7997,definition,
( sQ282_spl
<=> with_suprema_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f7999,plain,
( sQ282_spl
| ~ with_suprema_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f7997]) ).
fof(f8001,definition,
( sQ283_spl
<=> upper_bounded_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f8003,plain,
( sQ283_spl
| ~ upper_bounded_relstr(sK218_skl) ),
inference(component_clause,[status(thm)],[f8001]) ).
fof(f8004,definition,
( sQ284_spl
<=> with_suprema_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f8007,plain,
( sQ284_spl
| ~ sQ185_spl
| ~ sQ283_spl
| ~ sQ223_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f7957,f7185,f7188,f7539,f8001,f7191,f8004]) ).
fof(f8008,definition,
( sQ285_spl
<=> upper_bounded_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f8010,plain,
( sQ285_spl
| ~ upper_bounded_relstr(sK215_skl) ),
inference(component_clause,[status(thm)],[f8008]) ).
fof(f8011,definition,
( sQ286_spl
<=> with_suprema_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition]) ).
fof(f8014,plain,
( sQ286_spl
| ~ sQ179_spl
| ~ sQ285_spl
| ~ sQ225_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f7958,f7155,f7158,f7546,f8008,f7161,f8011]) ).
fof(f8036,definition,
( sQ293_spl
<=> upper_bounded_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f8039,definition,
( sQ294_spl
<=> with_suprema_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition]) ).
fof(f8043,definition,
( sQ295_spl
<=> upper_bounded_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f8045,plain,
( sQ295_spl
| ~ upper_bounded_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f8043]) ).
fof(f8046,definition,
( sQ296_spl
<=> with_suprema_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f8048,plain,
( sQ296_spl
| ~ with_suprema_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f8046]) ).
fof(f8050,definition,
( sQ297_spl
<=> upper_bounded_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f8052,plain,
( sQ297_spl
| ~ upper_bounded_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f8050]) ).
fof(f8053,definition,
( sQ298_spl
<=> with_suprema_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f8056,plain,
( sQ298_spl
| ~ sQ107_spl
| ~ sQ297_spl
| ~ sQ237_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f7964,f6643,f6646,f7588,f8050,f6652,f8053]) ).
fof(f8057,definition,
( sQ299_spl
<=> upper_bounded_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f8059,plain,
( sQ299_spl
| ~ upper_bounded_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f8057]) ).
fof(f8060,definition,
( sQ300_spl
<=> with_suprema_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f8063,plain,
( sQ300_spl
| ~ sQ102_spl
| ~ sQ299_spl
| ~ sQ239_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f7965,f6618,f6621,f7595,f8057,f6627,f8060]) ).
fof(f8071,definition,
( sQ303_spl
<=> upper_bounded_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition]) ).
fof(f8073,plain,
( sQ303_spl
| ~ upper_bounded_relstr(sK181_skl) ),
inference(component_clause,[status(thm)],[f8071]) ).
fof(f8074,definition,
( sQ304_spl
<=> with_suprema_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f8077,plain,
( sQ304_spl
| ~ sQ95_spl
| ~ sQ303_spl
| ~ sQ243_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f7967,f6284,f6287,f7609,f8071,f6578,f8074]) ).
fof(f8107,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7541,f3309]) ).
fof(f8108,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f8107]) ).
fof(f8109,plain,
( sQ225_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7548,f3287]) ).
fof(f8110,plain,
sQ225_spl,
inference(contradiction_clause,[status(thm)],[f8109]) ).
fof(f8111,plain,
( sQ229_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7562,f3237]) ).
fof(f8112,plain,
sQ229_spl,
inference(contradiction_clause,[status(thm)],[f8111]) ).
fof(f8113,plain,
( sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7576,f3195]) ).
fof(f8114,plain,
sQ233_spl,
inference(contradiction_clause,[status(thm)],[f8113]) ).
fof(f8115,plain,
( sQ237_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7590,f3157]) ).
fof(f8116,plain,
sQ237_spl,
inference(contradiction_clause,[status(thm)],[f8115]) ).
fof(f8117,plain,
( sQ239_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7597,f3141]) ).
fof(f8118,plain,
sQ239_spl,
inference(contradiction_clause,[status(thm)],[f8117]) ).
fof(f8119,plain,
( sQ243_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7611,f3058]) ).
fof(f8120,plain,
sQ243_spl,
inference(contradiction_clause,[status(thm)],[f8119]) ).
fof(f8121,plain,
( sQ241_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7604,f3090]) ).
fof(f8122,plain,
sQ241_spl,
inference(contradiction_clause,[status(thm)],[f8121]) ).
fof(f8123,plain,
( sQ231_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7569,f3206]) ).
fof(f8124,plain,
sQ231_spl,
inference(contradiction_clause,[status(thm)],[f8123]) ).
fof(f8125,plain,
( sQ227_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7555,f3247]) ).
fof(f8126,plain,
sQ227_spl,
inference(contradiction_clause,[status(thm)],[f8125]) ).
fof(f8127,plain,
( sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7583,f3176]) ).
fof(f8128,plain,
sQ235_spl,
inference(contradiction_clause,[status(thm)],[f8127]) ).
fof(f8129,plain,
( sQ283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8003,f3314]) ).
fof(f8130,plain,
sQ283_spl,
inference(contradiction_clause,[status(thm)],[f8129]) ).
fof(f8131,plain,
( sQ285_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8010,f3292]) ).
fof(f8132,plain,
sQ285_spl,
inference(contradiction_clause,[status(thm)],[f8131]) ).
fof(f8133,plain,
( sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8052,f3159]) ).
fof(f8134,plain,
sQ297_spl,
inference(contradiction_clause,[status(thm)],[f8133]) ).
fof(f8135,plain,
( sQ299_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8059,f3146]) ).
fof(f8136,plain,
sQ299_spl,
inference(contradiction_clause,[status(thm)],[f8135]) ).
fof(f8137,plain,
( sQ303_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8073,f3063]) ).
fof(f8138,plain,
sQ303_spl,
inference(contradiction_clause,[status(thm)],[f8137]) ).
fof(f8139,plain,
( sQ295_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8045,f3178]) ).
fof(f8140,plain,
sQ295_spl,
inference(contradiction_clause,[status(thm)],[f8139]) ).
fof(f8141,plain,
! [X0] :
( v1_membered(empty_set)
| ~ v1_membered(X0) ),
inference(resolution,[status(thm)],[f924,f6766]) ).
fof(f8143,definition,
! [X0] :
( sQ309_spl
<=> ~ v1_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f8144,plain,
! [X0] :
( ~ sQ309_spl
| ~ v1_membered(X0) ),
inference(component_clause,[status(thm)],[f8143]) ).
fof(f8146,definition,
( sQ310_spl
<=> v1_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f8149,plain,
( sQ310_spl
| sQ309_spl ),
inference(split_clause,[status(thm)],[f8141,f8143,f8146]) ).
fof(f8152,plain,
( ~ sQ309_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3094,f8144]) ).
fof(f8178,plain,
~ sQ309_spl,
inference(contradiction_clause,[status(thm)],[f8152]) ).
fof(f8181,plain,
! [X0] :
( ~ sQ278_spl
| ~ element(X0,the_carrier(sK473_skl))
| ~ rel_str(sK473_skl)
| ~ lower_bounded_relstr(sK473_skl)
| ~ antisymmetric_relstr(sK473_skl)
| empty_carrier(sK473_skl)
| in(X0,sK474_skl)
| ~ in(bottom_of_relstr(sK473_skl),sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ),
inference(resolution,[status(thm)],[f7912,f4537]) ).
fof(f8182,definition,
! [X0] :
( sQ311_spl
<=> ( ~ element(X0,the_carrier(sK473_skl))
| in(X0,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f8183,plain,
! [X0] :
( ~ sQ311_spl
| ~ element(X0,the_carrier(sK473_skl))
| in(X0,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ),
inference(component_clause,[status(thm)],[f8182]) ).
fof(f8185,plain,
( ~ sQ278_spl
| ~ sQ65_spl
| ~ sQ169_spl
| ~ sQ247_spl
| sQ63_spl
| ~ sQ36_spl
| sQ311_spl ),
inference(split_clause,[status(thm)],[f8181,f8182,f5540,f6219,f7623,f7096,f6225,f7911]) ).
fof(f8186,plain,
( sQ247_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7625,f4775]) ).
fof(f8187,plain,
sQ247_spl,
inference(contradiction_clause,[status(thm)],[f8186]) ).
fof(f8188,plain,
! [X0] :
( ~ sQ311_spl
| in(X0,sK474_skl)
| ~ element(X0,the_carrier(sK473_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f8183]) ).
fof(f8338,plain,
! [X0,X1] :
( natural(X1)
| ~ v5_membered(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f907]) ).
fof(f8353,definition,
! [X1] :
( sQ312_spl
<=> ( natural(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f8356,plain,
( sQ312_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f8338,f7733,f8353]) ).
fof(f8367,plain,
( ~ sQ269_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f8431]) ).
fof(f8431,plain,
! [X0] :
( ~ sQ269_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7734,f922]) ).
fof(f8432,plain,
~ sQ269_spl,
inference(contradiction_clause,[status(thm)],[f8367]) ).
fof(f8441,plain,
! [X0] :
( v2_membered(empty_set)
| ~ v2_membered(X0) ),
inference(resolution,[status(thm)],[f927,f6766]) ).
fof(f8443,definition,
! [X0] :
( sQ313_spl
<=> ~ v2_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f8444,plain,
! [X0] :
( ~ sQ313_spl
| ~ v2_membered(X0) ),
inference(component_clause,[status(thm)],[f8443]) ).
fof(f8446,definition,
( sQ314_spl
<=> v2_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f8449,plain,
( sQ314_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f8441,f8443,f8446]) ).
fof(f8452,plain,
( ~ sQ313_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3095,f8444]) ).
fof(f8474,plain,
~ sQ313_spl,
inference(contradiction_clause,[status(thm)],[f8452]) ).
fof(f8475,plain,
! [X0] :
( v3_membered(empty_set)
| ~ v3_membered(X0) ),
inference(resolution,[status(thm)],[f931,f6766]) ).
fof(f8477,definition,
! [X0] :
( sQ315_spl
<=> ~ v3_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f8478,plain,
! [X0] :
( ~ sQ315_spl
| ~ v3_membered(X0) ),
inference(component_clause,[status(thm)],[f8477]) ).
fof(f8480,definition,
( sQ316_spl
<=> v3_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f8483,plain,
( sQ316_spl
| sQ315_spl ),
inference(split_clause,[status(thm)],[f8475,f8477,f8480]) ).
fof(f8486,plain,
( ~ sQ315_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3096,f8478]) ).
fof(f8504,plain,
~ sQ315_spl,
inference(contradiction_clause,[status(thm)],[f8486]) ).
fof(f8505,plain,
! [X0] :
( v4_membered(empty_set)
| ~ v4_membered(X0) ),
inference(resolution,[status(thm)],[f936,f6766]) ).
fof(f8507,definition,
! [X0] :
( sQ317_spl
<=> ~ v4_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition]) ).
fof(f8508,plain,
! [X0] :
( ~ sQ317_spl
| ~ v4_membered(X0) ),
inference(component_clause,[status(thm)],[f8507]) ).
fof(f8510,definition,
( sQ318_spl
<=> v4_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f8513,plain,
( sQ318_spl
| sQ317_spl ),
inference(split_clause,[status(thm)],[f8505,f8507,f8510]) ).
fof(f8516,plain,
( ~ sQ317_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3097,f8508]) ).
fof(f8530,plain,
~ sQ317_spl,
inference(contradiction_clause,[status(thm)],[f8516]) ).
fof(f8754,plain,
! [X0,X1] :
( ordinal(X1)
| ~ ordinal(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f940]) ).
fof(f8755,plain,
! [X0,X1] :
( epsilon_connected(X1)
| ~ ordinal(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f939]) ).
fof(f8756,plain,
! [X0,X1] :
( epsilon_transitive(X1)
| ~ ordinal(X0)
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1680,f938]) ).
fof(f8767,definition,
! [X0] :
( sQ346_spl
<=> ( ~ ordinal(X0)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition]) ).
fof(f8768,plain,
! [X0] :
( ~ sQ346_spl
| ~ ordinal(X0)
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f8767]) ).
fof(f8770,definition,
! [X1] :
( sQ347_spl
<=> ( ordinal(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f8773,plain,
( sQ347_spl
| sQ346_spl ),
inference(split_clause,[status(thm)],[f8754,f8767,f8770]) ).
fof(f8774,definition,
! [X1] :
( sQ348_spl
<=> ( epsilon_connected(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ348_spl])],[split_symbol_definition]) ).
fof(f8777,plain,
( sQ348_spl
| sQ346_spl ),
inference(split_clause,[status(thm)],[f8755,f8767,f8774]) ).
fof(f8778,definition,
! [X1] :
( sQ349_spl
<=> ( epsilon_transitive(X1)
| ~ empty(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f8781,plain,
( sQ349_spl
| sQ346_spl ),
inference(split_clause,[status(thm)],[f8756,f8767,f8778]) ).
fof(f8787,plain,
( ~ sQ346_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3265,f8851]) ).
fof(f8851,plain,
! [X0] :
( ~ sQ346_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8768,f1080]) ).
fof(f8852,plain,
~ sQ346_spl,
inference(contradiction_clause,[status(thm)],[f8787]) ).
fof(f8895,plain,
one_sorted_str(sK473_skl),
inference(resolution,[status(thm)],[f2288,f4777]) ).
fof(f9098,plain,
! [X0,X1] : subset(X0,set_union2(X1,X0)),
inference(paramodulation,[status(thm)],[f1227,f4743]) ).
fof(f9139,plain,
! [X0] : empty_set = set_intersection2(empty_set,X0),
inference(paramodulation,[status(thm)],[f4357,f1230]) ).
fof(f9432,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7098,f4776]) ).
fof(f9433,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f9432]) ).
fof(f9434,plain,
( sQ257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7664,f3174]) ).
fof(f9435,plain,
sQ257_spl,
inference(contradiction_clause,[status(thm)],[f9434]) ).
fof(f9436,plain,
( sQ253_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7648,f3245]) ).
fof(f9437,plain,
sQ253_spl,
inference(contradiction_clause,[status(thm)],[f9436]) ).
fof(f9438,plain,
( sQ255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7656,f3204]) ).
fof(f9439,plain,
sQ255_spl,
inference(contradiction_clause,[status(thm)],[f9438]) ).
fof(f9440,plain,
( sQ260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7676,f3088]) ).
fof(f9441,plain,
sQ260_spl,
inference(contradiction_clause,[status(thm)],[f9440]) ).
fof(f9442,plain,
( sQ261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7680,f3056]) ).
fof(f9443,plain,
sQ261_spl,
inference(contradiction_clause,[status(thm)],[f9442]) ).
fof(f9444,plain,
( sQ259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7672,f3139]) ).
fof(f9445,plain,
sQ259_spl,
inference(contradiction_clause,[status(thm)],[f9444]) ).
fof(f9446,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7668,f3155]) ).
fof(f9447,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f9446]) ).
fof(f9448,plain,
( sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7660,f3193]) ).
fof(f9449,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f9448]) ).
fof(f9450,plain,
( sQ254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7652,f3235]) ).
fof(f9451,plain,
sQ254_spl,
inference(contradiction_clause,[status(thm)],[f9450]) ).
fof(f9452,plain,
( sQ252_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7644,f3285]) ).
fof(f9453,plain,
sQ252_spl,
inference(contradiction_clause,[status(thm)],[f9452]) ).
fof(f9454,plain,
( sQ251_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7640,f3307]) ).
fof(f9455,plain,
sQ251_spl,
inference(contradiction_clause,[status(thm)],[f9454]) ).
fof(f9456,plain,
( sQ263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7688,f4773]) ).
fof(f9457,plain,
sQ263_spl,
inference(contradiction_clause,[status(thm)],[f9456]) ).
fof(f9458,plain,
( sQ262_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7684,f3031]) ).
fof(f9459,plain,
sQ262_spl,
inference(contradiction_clause,[status(thm)],[f9458]) ).
fof(f9460,plain,
( sQ281_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7996,f3375]) ).
fof(f9461,plain,
sQ281_spl,
inference(contradiction_clause,[status(thm)],[f9460]) ).
fof(f9462,plain,
( sQ250_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7636,f3369]) ).
fof(f9463,plain,
sQ250_spl,
inference(contradiction_clause,[status(thm)],[f9462]) ).
fof(f9464,plain,
( sQ279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7989,f3394]) ).
fof(f9465,plain,
sQ279_spl,
inference(contradiction_clause,[status(thm)],[f9464]) ).
fof(f9466,plain,
( sQ249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7632,f3389]) ).
fof(f9467,plain,
sQ249_spl,
inference(contradiction_clause,[status(thm)],[f9466]) ).
fof(f9468,plain,
( sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7618,f3033]) ).
fof(f9469,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f9468]) ).
fof(f9470,plain,
( sQ221_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7534,f3371]) ).
fof(f9471,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f9470]) ).
fof(f9472,plain,
( sQ219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7527,f3391]) ).
fof(f9473,plain,
sQ219_spl,
inference(contradiction_clause,[status(thm)],[f9472]) ).
fof(f9592,plain,
( ~ sQ176_spl
| element(bottom_of_relstr(sK473_skl),sK474_skl)
| ~ rel_str(sK473_skl) ),
inference(paramodulation,[status(thm)],[f7149,f2214]) ).
fof(f9619,plain,
( ~ sQ176_spl
| sQ118_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f9592,f6225,f6710,f7148]) ).
fof(f9657,plain,
( ~ sQ118_spl
| in(bottom_of_relstr(sK473_skl),sK474_skl)
| empty(sK474_skl) ),
inference(resolution,[status(thm)],[f6711,f1677]) ).
fof(f9668,plain,
( ~ sQ118_spl
| sQ36_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f9657,f6239,f5540,f6710]) ).
fof(f9680,plain,
( ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6240,f4778]) ).
fof(f9681,plain,
~ sQ67_spl,
inference(contradiction_clause,[status(thm)],[f9680]) ).
fof(f9802,plain,
( bounded_relstr(sK201_skl)
| ~ join_complete_relstr(sK201_skl)
| ~ up_complete_relstr(sK201_skl)
| ~ upper_bounded_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1000,f3193]) ).
fof(f9845,definition,
( sQ372_spl
<=> transitive_relstr(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f9847,plain,
( sQ372_spl
| ~ transitive_relstr(sK232_skl) ),
inference(component_clause,[status(thm)],[f9845]) ).
fof(f9852,definition,
( sQ374_spl
<=> transitive_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition]) ).
fof(f9854,plain,
( sQ374_spl
| ~ transitive_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f9852]) ).
fof(f9855,definition,
( sQ375_spl
<=> bounded_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition]) ).
fof(f9859,definition,
( sQ376_spl
<=> transitive_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition]) ).
fof(f9861,plain,
( sQ376_spl
| ~ transitive_relstr(sK218_skl) ),
inference(component_clause,[status(thm)],[f9859]) ).
fof(f9862,definition,
( sQ377_spl
<=> bounded_relstr(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f9866,definition,
( sQ378_spl
<=> transitive_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f9868,plain,
( sQ378_spl
| ~ transitive_relstr(sK215_skl) ),
inference(component_clause,[status(thm)],[f9866]) ).
fof(f9869,definition,
( sQ379_spl
<=> bounded_relstr(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition]) ).
fof(f9873,definition,
( sQ380_spl
<=> transitive_relstr(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f9875,plain,
( sQ380_spl
| ~ transitive_relstr(sK207_skl) ),
inference(component_clause,[status(thm)],[f9873]) ).
fof(f9880,definition,
( sQ382_spl
<=> transitive_relstr(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ382_spl])],[split_symbol_definition]) ).
fof(f9882,plain,
( sQ382_spl
| ~ transitive_relstr(sK206_skl) ),
inference(component_clause,[status(thm)],[f9880]) ).
fof(f9887,definition,
( sQ384_spl
<=> transitive_relstr(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f9889,plain,
( sQ384_spl
| ~ transitive_relstr(sK202_skl) ),
inference(component_clause,[status(thm)],[f9887]) ).
fof(f9894,definition,
( sQ386_spl
<=> transitive_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f9896,plain,
( sQ386_spl
| ~ transitive_relstr(sK201_skl) ),
inference(component_clause,[status(thm)],[f9894]) ).
fof(f9897,definition,
( sQ387_spl
<=> bounded_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f9900,plain,
( sQ387_spl
| ~ sQ128_spl
| ~ sQ129_spl
| ~ sQ293_spl
| ~ sQ233_spl
| ~ sQ386_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f9802,f6769,f6772,f9894,f7574,f8036,f6782,f6778,f9897]) ).
fof(f9901,definition,
( sQ388_spl
<=> transitive_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f9903,plain,
( sQ388_spl
| ~ transitive_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f9901]) ).
fof(f9904,definition,
( sQ389_spl
<=> bounded_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f9908,definition,
( sQ390_spl
<=> transitive_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f9910,plain,
( sQ390_spl
| ~ transitive_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f9908]) ).
fof(f9911,definition,
( sQ391_spl
<=> bounded_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition]) ).
fof(f9915,definition,
( sQ392_spl
<=> transitive_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f9917,plain,
( sQ392_spl
| ~ transitive_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f9915]) ).
fof(f9918,definition,
( sQ393_spl
<=> bounded_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ393_spl])],[split_symbol_definition]) ).
fof(f9922,definition,
( sQ394_spl
<=> transitive_relstr(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition]) ).
fof(f9924,plain,
( sQ394_spl
| ~ transitive_relstr(sK186_skl) ),
inference(component_clause,[status(thm)],[f9922]) ).
fof(f9929,definition,
( sQ396_spl
<=> transitive_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition]) ).
fof(f9931,plain,
( sQ396_spl
| ~ transitive_relstr(sK181_skl) ),
inference(component_clause,[status(thm)],[f9929]) ).
fof(f9932,definition,
( sQ397_spl
<=> bounded_relstr(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition]) ).
fof(f9936,definition,
( sQ398_spl
<=> transitive_relstr(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ398_spl])],[split_symbol_definition]) ).
fof(f9938,plain,
( sQ398_spl
| ~ transitive_relstr(sK179_skl) ),
inference(component_clause,[status(thm)],[f9936]) ).
fof(f9943,definition,
( sQ400_spl
<=> transitive_relstr(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition]) ).
fof(f9945,plain,
( sQ400_spl
| ~ transitive_relstr(sK473_skl) ),
inference(component_clause,[status(thm)],[f9943]) ).
fof(f9982,plain,
( sQ400_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9945,f4774]) ).
fof(f9983,plain,
sQ400_spl,
inference(contradiction_clause,[status(thm)],[f9982]) ).
fof(f9984,plain,
( sQ398_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9938,f3032]) ).
fof(f9985,plain,
sQ398_spl,
inference(contradiction_clause,[status(thm)],[f9984]) ).
fof(f9986,plain,
( sQ396_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9931,f3057]) ).
fof(f9987,plain,
sQ396_spl,
inference(contradiction_clause,[status(thm)],[f9986]) ).
fof(f9988,plain,
( sQ394_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9924,f3089]) ).
fof(f9989,plain,
sQ394_spl,
inference(contradiction_clause,[status(thm)],[f9988]) ).
fof(f9990,plain,
( sQ392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9917,f3140]) ).
fof(f9991,plain,
sQ392_spl,
inference(contradiction_clause,[status(thm)],[f9990]) ).
fof(f9992,plain,
( sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9910,f3156]) ).
fof(f9993,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f9992]) ).
fof(f9994,plain,
( sQ388_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9903,f3175]) ).
fof(f9995,plain,
sQ388_spl,
inference(contradiction_clause,[status(thm)],[f9994]) ).
fof(f9996,plain,
( sQ386_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9896,f3194]) ).
fof(f9997,plain,
sQ386_spl,
inference(contradiction_clause,[status(thm)],[f9996]) ).
fof(f9998,plain,
( sQ384_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9889,f3205]) ).
fof(f9999,plain,
sQ384_spl,
inference(contradiction_clause,[status(thm)],[f9998]) ).
fof(f10000,plain,
( sQ382_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9882,f3236]) ).
fof(f10001,plain,
sQ382_spl,
inference(contradiction_clause,[status(thm)],[f10000]) ).
fof(f10002,plain,
( sQ380_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9875,f3246]) ).
fof(f10003,plain,
sQ380_spl,
inference(contradiction_clause,[status(thm)],[f10002]) ).
fof(f10004,plain,
( sQ378_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9868,f3286]) ).
fof(f10005,plain,
sQ378_spl,
inference(contradiction_clause,[status(thm)],[f10004]) ).
fof(f10006,plain,
( sQ376_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9861,f3308]) ).
fof(f10007,plain,
sQ376_spl,
inference(contradiction_clause,[status(thm)],[f10006]) ).
fof(f10008,plain,
( sQ374_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9854,f3370]) ).
fof(f10009,plain,
sQ374_spl,
inference(contradiction_clause,[status(thm)],[f10008]) ).
fof(f10010,plain,
( sQ372_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9847,f3390]) ).
fof(f10011,plain,
sQ372_spl,
inference(contradiction_clause,[status(thm)],[f10010]) ).
fof(f10219,plain,
! [X0] :
( v5_membered(empty_set)
| ~ v5_membered(X0) ),
inference(paramodulation,[status(thm)],[f4357,f2629]) ).
fof(f10223,definition,
( sQ406_spl
<=> v5_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f10227,definition,
! [X0] :
( sQ407_spl
<=> ~ v5_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f10228,plain,
! [X0] :
( ~ sQ407_spl
| ~ v5_membered(X0) ),
inference(component_clause,[status(thm)],[f10227]) ).
fof(f10230,plain,
( sQ406_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f10219,f10227,f10223]) ).
fof(f10237,plain,
( ~ sQ407_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3098,f10228]) ).
fof(f10331,plain,
~ sQ407_spl,
inference(contradiction_clause,[status(thm)],[f10237]) ).
fof(f10682,plain,
! [X0] :
( empty_set = empty_set
| ~ subset(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f9139,f4341]) ).
fof(f10687,definition,
! [X0] :
( sQ417_spl
<=> ~ subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f10688,plain,
! [X0] :
( ~ sQ417_spl
| ~ subset(empty_set,X0) ),
inference(component_clause,[status(thm)],[f10687]) ).
fof(f10690,definition,
( sQ418_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f10693,plain,
( sQ418_spl
| sQ417_spl ),
inference(split_clause,[status(thm)],[f10682,f10687,f10690]) ).
fof(f10694,plain,
( ~ sQ417_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10688,f4370]) ).
fof(f10695,plain,
~ sQ417_spl,
inference(contradiction_clause,[status(thm)],[f10694]) ).
fof(f10709,definition,
! [X0] :
( sQ420_spl
<=> ~ disjoint(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f10710,plain,
! [X0] :
( ~ sQ420_spl
| ~ disjoint(empty_set,X0) ),
inference(component_clause,[status(thm)],[f10709]) ).
fof(f10713,plain,
! [X0] : disjoint(empty_set,X0),
inference(resolution,[status(thm)],[f4747,f4581]) ).
fof(f10714,plain,
! [X0] : disjoint(X0,empty_set),
inference(resolution,[status(thm)],[f4747,f4485]) ).
fof(f10716,plain,
! [X0] :
( empty_set != empty_set
| disjoint(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f4581,f4747]) ).
fof(f10718,plain,
( ~ sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10713,f10710]) ).
fof(f10719,plain,
~ sQ420_spl,
inference(contradiction_clause,[status(thm)],[f10718]) ).
fof(f10720,definition,
! [X0] :
( sQ421_spl
<=> disjoint(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f10723,plain,
( ~ sQ418_spl
| sQ421_spl ),
inference(split_clause,[status(thm)],[f10716,f10720,f10690]) ).
fof(f10736,plain,
( with_suprema_relstr(sK201_skl)
| ~ up_complete_relstr(sK201_skl)
| ~ connected_relstr(sK201_skl)
| ~ lower_bounded_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1046,f3193]) ).
fof(f10824,definition,
( sQ429_spl
<=> connected_relstr(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f10827,plain,
( sQ294_spl
| ~ sQ129_spl
| ~ sQ429_spl
| ~ sQ162_spl
| ~ sQ233_spl
| ~ sQ386_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f10736,f6769,f6772,f9894,f7574,f7068,f10824,f6782,f8039]) ).
fof(f10836,definition,
( sQ432_spl
<=> connected_relstr(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f10838,plain,
( sQ432_spl
| ~ connected_relstr(sK197_skl) ),
inference(component_clause,[status(thm)],[f10836]) ).
fof(f10848,definition,
( sQ435_spl
<=> connected_relstr(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f10850,plain,
( sQ435_spl
| ~ connected_relstr(sK179_skl) ),
inference(component_clause,[status(thm)],[f10848]) ).
fof(f10901,plain,
( sQ432_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10838,f3148]) ).
fof(f10902,plain,
sQ432_spl,
inference(contradiction_clause,[status(thm)],[f10901]) ).
fof(f10903,plain,
( sQ435_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10850,f3034]) ).
fof(f10904,plain,
sQ435_spl,
inference(contradiction_clause,[status(thm)],[f10903]) ).
fof(f11140,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,empty_set) ),
inference(resolution,[status(thm)],[f4648,f6766]) ).
fof(f11144,definition,
! [X0] :
( sQ443_spl
<=> ~ in(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition]) ).
fof(f11147,definition,
! [X1] :
( sQ444_spl
<=> ~ empty(X1) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f11148,plain,
! [X0] :
( ~ sQ444_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f11147]) ).
fof(f11150,plain,
( sQ444_spl
| sQ443_spl ),
inference(split_clause,[status(thm)],[f11140,f11144,f11147]) ).
fof(f11151,definition,
! [X0,X1] :
( sQ445_spl
<=> ( ~ empty(X1)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f11160,plain,
( ~ sQ444_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2375,f11148]) ).
fof(f11245,plain,
~ sQ444_spl,
inference(contradiction_clause,[status(thm)],[f11160]) ).
fof(f11534,plain,
( bounded_relstr(sK197_skl)
| ~ up_complete_relstr(sK197_skl)
| ~ connected_relstr(sK197_skl)
| ~ lower_bounded_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1051,f3139]) ).
fof(f11600,plain,
( sQ393_spl
| ~ sQ103_spl
| ~ sQ432_spl
| ~ sQ165_spl
| ~ sQ239_spl
| ~ sQ392_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f11534,f6618,f6621,f9915,f7595,f7080,f10836,f6631,f9918]) ).
fof(f11921,definition,
( sQ454_spl
<=> trivial_carrier(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).
fof(f11923,plain,
( sQ454_spl
| ~ trivial_carrier(sK201_skl) ),
inference(component_clause,[status(thm)],[f11921]) ).
fof(f11953,plain,
( sQ454_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11923,f3199]) ).
fof(f11954,plain,
sQ454_spl,
inference(contradiction_clause,[status(thm)],[f11953]) ).
fof(f11988,plain,
! [X0,X1,X2] :
( related(X1,X2,X0)
| ~ in(X0,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(sK473_skl,X2,X0)
| ~ element(X2,the_carrier(sK473_skl))
| ~ subrelstr(X1,sK473_skl)
| ~ full_subrelstr(X1,sK473_skl)
| ~ rel_str(sK473_skl)
| ~ in(X0,sK474_skl) ),
inference(resolution,[status(thm)],[f6816,f7044]) ).
fof(f11993,definition,
! [X0,X1,X2] :
( sQ462_spl
<=> ( related(X1,X2,X0)
| ~ in(X0,the_carrier(X1))
| ~ in(X2,the_carrier(X1))
| ~ related(sK473_skl,X2,X0)
| ~ element(X2,the_carrier(sK473_skl))
| ~ subrelstr(X1,sK473_skl)
| ~ full_subrelstr(X1,sK473_skl)
| ~ in(X0,sK474_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition]) ).
fof(f11996,plain,
( ~ sQ65_spl
| sQ462_spl ),
inference(split_clause,[status(thm)],[f11988,f11993,f6225]) ).
fof(f12474,plain,
( v2_waybel_3(sK201_skl)
| ~ trivial_carrier(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1084,f3193]) ).
fof(f12496,definition,
( sQ484_spl
<=> v2_waybel_3(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition]) ).
fof(f12512,definition,
( sQ488_spl
<=> v2_waybel_3(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ488_spl])],[split_symbol_definition]) ).
fof(f12515,plain,
( sQ488_spl
| ~ sQ454_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f12474,f6769,f6772,f11921,f12512]) ).
fof(f12520,definition,
( sQ490_spl
<=> v2_waybel_3(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition]) ).
fof(f12524,definition,
( sQ491_spl
<=> v2_waybel_3(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition]) ).
fof(f12698,plain,
( ~ v1_yellow_3(sK232_skl)
| empty_carrier(sK232_skl)
| ~ rel_str(sK232_skl) ),
inference(resolution,[status(thm)],[f1090,f3389]) ).
fof(f12699,plain,
( ~ v1_yellow_3(sK230_skl)
| empty_carrier(sK230_skl)
| ~ rel_str(sK230_skl) ),
inference(resolution,[status(thm)],[f1090,f3369]) ).
fof(f12700,plain,
( ~ v1_yellow_3(sK218_skl)
| empty_carrier(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f1090,f3307]) ).
fof(f12702,plain,
( ~ v1_yellow_3(sK207_skl)
| empty_carrier(sK207_skl)
| ~ rel_str(sK207_skl) ),
inference(resolution,[status(thm)],[f1090,f3245]) ).
fof(f12703,plain,
( ~ v1_yellow_3(sK206_skl)
| empty_carrier(sK206_skl)
| ~ rel_str(sK206_skl) ),
inference(resolution,[status(thm)],[f1090,f3235]) ).
fof(f12704,plain,
( ~ v1_yellow_3(sK202_skl)
| empty_carrier(sK202_skl)
| ~ rel_str(sK202_skl) ),
inference(resolution,[status(thm)],[f1090,f3204]) ).
fof(f12705,plain,
( ~ v1_yellow_3(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1090,f3193]) ).
fof(f12706,plain,
( ~ v1_yellow_3(sK199_skl)
| empty_carrier(sK199_skl)
| ~ rel_str(sK199_skl) ),
inference(resolution,[status(thm)],[f1090,f3174]) ).
fof(f12709,plain,
( ~ v1_yellow_3(sK186_skl)
| empty_carrier(sK186_skl)
| ~ rel_str(sK186_skl) ),
inference(resolution,[status(thm)],[f1090,f3088]) ).
fof(f12710,plain,
( ~ v1_yellow_3(sK181_skl)
| empty_carrier(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f1090,f3056]) ).
fof(f12711,plain,
( ~ v1_yellow_3(sK179_skl)
| empty_carrier(sK179_skl)
| ~ rel_str(sK179_skl) ),
inference(resolution,[status(thm)],[f1090,f3031]) ).
fof(f12712,plain,
( ~ v1_yellow_3(sK473_skl)
| empty_carrier(sK473_skl)
| ~ rel_str(sK473_skl) ),
inference(resolution,[status(thm)],[f1090,f4773]) ).
fof(f12714,definition,
( sQ496_spl
<=> v1_yellow_3(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ496_spl])],[split_symbol_definition]) ).
fof(f12717,plain,
( ~ sQ496_spl
| sQ206_spl
| ~ sQ205_spl ),
inference(split_clause,[status(thm)],[f12698,f7398,f7401,f12714]) ).
fof(f12718,definition,
( sQ497_spl
<=> v1_yellow_3(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition]) ).
fof(f12721,plain,
( ~ sQ497_spl
| sQ200_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f12699,f7370,f7373,f12718]) ).
fof(f12722,definition,
( sQ498_spl
<=> v1_yellow_3(sK218_skl) ),
introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition]) ).
fof(f12725,plain,
( ~ sQ498_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f12700,f7185,f7188,f12722]) ).
fof(f12726,definition,
( sQ499_spl
<=> v1_yellow_3(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition]) ).
fof(f12730,definition,
( sQ500_spl
<=> v1_yellow_3(sK207_skl) ),
introduced(definition,[new_symbols(definition,[sQ500_spl])],[split_symbol_definition]) ).
fof(f12733,plain,
( ~ sQ500_spl
| sQ147_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f12702,f6908,f6911,f12730]) ).
fof(f12734,definition,
( sQ501_spl
<=> v1_yellow_3(sK206_skl) ),
introduced(definition,[new_symbols(definition,[sQ501_spl])],[split_symbol_definition]) ).
fof(f12737,plain,
( ~ sQ501_spl
| sQ142_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f12703,f6883,f6886,f12734]) ).
fof(f12738,definition,
( sQ502_spl
<=> v1_yellow_3(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ502_spl])],[split_symbol_definition]) ).
fof(f12741,plain,
( ~ sQ502_spl
| sQ131_spl
| ~ sQ130_spl ),
inference(split_clause,[status(thm)],[f12704,f6794,f6797,f12738]) ).
fof(f12742,definition,
( sQ503_spl
<=> v1_yellow_3(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ503_spl])],[split_symbol_definition]) ).
fof(f12745,plain,
( ~ sQ503_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f12705,f6769,f6772,f12742]) ).
fof(f12746,definition,
( sQ504_spl
<=> v1_yellow_3(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ504_spl])],[split_symbol_definition]) ).
fof(f12749,plain,
( ~ sQ504_spl
| sQ110_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f12706,f6668,f6671,f12746]) ).
fof(f12750,definition,
( sQ505_spl
<=> v1_yellow_3(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition]) ).
fof(f12754,definition,
( sQ506_spl
<=> v1_yellow_3(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f12758,definition,
( sQ507_spl
<=> v1_yellow_3(sK186_skl) ),
introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition]) ).
fof(f12761,plain,
( ~ sQ507_spl
| sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f12709,f6551,f6554,f12758]) ).
fof(f12762,definition,
( sQ508_spl
<=> v1_yellow_3(sK181_skl) ),
introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition]) ).
fof(f12765,plain,
( ~ sQ508_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f12710,f6284,f6287,f12762]) ).
fof(f12766,definition,
( sQ509_spl
<=> v1_yellow_3(sK179_skl) ),
introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition]) ).
fof(f12769,plain,
( ~ sQ509_spl
| sQ81_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f12711,f6297,f6300,f12766]) ).
fof(f12770,definition,
( sQ510_spl
<=> v1_yellow_3(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ510_spl])],[split_symbol_definition]) ).
fof(f12773,plain,
( ~ sQ510_spl
| sQ63_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f12712,f6225,f6219,f12770]) ).
fof(f13313,plain,
( ~ sQ140_spl
| subset(sK474_skl,the_carrier(sK473_skl)) ),
inference(resolution,[status(thm)],[f5740,f6862]) ).
fof(f13354,definition,
( sQ545_spl
<=> v3_waybel_3(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition]) ).
fof(f13356,plain,
( sQ545_spl
| ~ v3_waybel_3(sK215_skl) ),
inference(component_clause,[status(thm)],[f13354]) ).
fof(f13370,definition,
( sQ549_spl
<=> v3_waybel_3(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition]) ).
fof(f13378,definition,
( sQ551_spl
<=> v3_waybel_3(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ551_spl])],[split_symbol_definition]) ).
fof(f13380,plain,
( sQ551_spl
| ~ v3_waybel_3(sK198_skl) ),
inference(component_clause,[status(thm)],[f13378]) ).
fof(f13382,definition,
( sQ552_spl
<=> v3_waybel_3(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition]) ).
fof(f13402,plain,
( sQ551_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13380,f3168]) ).
fof(f13403,plain,
sQ551_spl,
inference(contradiction_clause,[status(thm)],[f13402]) ).
fof(f13404,plain,
( sQ545_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13356,f3297]) ).
fof(f13405,plain,
sQ545_spl,
inference(contradiction_clause,[status(thm)],[f13404]) ).
fof(f13411,plain,
( v2_waybel_3(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| empty_carrier(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1107,f3285]) ).
fof(f13417,plain,
( v2_waybel_3(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| empty_carrier(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1107,f3155]) ).
fof(f13428,plain,
( sQ484_spl
| ~ sQ545_spl
| sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f13411,f7155,f7158,f13354,f12496]) ).
fof(f13434,plain,
( sQ490_spl
| ~ sQ551_spl
| sQ105_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f13417,f6643,f6646,f13378,f12520]) ).
fof(f13449,plain,
( upper_bounded_relstr(sK201_skl)
| ~ with_infima_relstr(sK201_skl)
| ~ with_suprema_relstr(sK201_skl)
| ~ v3_waybel_3(sK201_skl)
| ~ lower_bounded_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1114,f3193]) ).
fof(f13514,plain,
( sQ293_spl
| ~ sQ234_spl
| ~ sQ294_spl
| ~ sQ549_spl
| ~ sQ162_spl
| ~ sQ233_spl
| ~ sQ386_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f13449,f6769,f9894,f7574,f7068,f13370,f8039,f7577,f8036]) ).
fof(f13666,definition,
! [X0] :
( sQ557_spl
<=> ~ disjoint(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition]) ).
fof(f13667,plain,
! [X0] :
( ~ sQ557_spl
| ~ disjoint(X0,empty_set) ),
inference(component_clause,[status(thm)],[f13666]) ).
fof(f13670,plain,
( ~ sQ557_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13667,f10714]) ).
fof(f13671,plain,
~ sQ557_spl,
inference(contradiction_clause,[status(thm)],[f13670]) ).
fof(f13755,plain,
( bounded_relstr(sK215_skl)
| ~ with_infima_relstr(sK215_skl)
| ~ with_suprema_relstr(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| ~ lower_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| ~ transitive_relstr(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1115,f3285]) ).
fof(f13761,plain,
( bounded_relstr(sK198_skl)
| ~ with_infima_relstr(sK198_skl)
| ~ with_suprema_relstr(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| ~ lower_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| ~ transitive_relstr(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1115,f3155]) ).
fof(f13820,plain,
( sQ379_spl
| ~ sQ226_spl
| ~ sQ286_spl
| ~ sQ545_spl
| ~ sQ180_spl
| ~ sQ225_spl
| ~ sQ378_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f13755,f7155,f9866,f7546,f7164,f13354,f8011,f7549,f9869]) ).
fof(f13826,plain,
( sQ391_spl
| ~ sQ238_spl
| ~ sQ298_spl
| ~ sQ551_spl
| ~ sQ164_spl
| ~ sQ237_spl
| ~ sQ390_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f13761,f6643,f9908,f7588,f7076,f13378,f8053,f7591,f9911]) ).
fof(f13883,plain,
( up_complete_relstr(sK215_skl)
| ~ with_infima_relstr(sK215_skl)
| ~ with_suprema_relstr(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| ~ lower_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| ~ transitive_relstr(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1116,f3285]) ).
fof(f13889,plain,
( up_complete_relstr(sK198_skl)
| ~ with_infima_relstr(sK198_skl)
| ~ with_suprema_relstr(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| ~ lower_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| ~ transitive_relstr(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1116,f3155]) ).
fof(f13948,plain,
( sQ182_spl
| ~ sQ226_spl
| ~ sQ286_spl
| ~ sQ545_spl
| ~ sQ180_spl
| ~ sQ225_spl
| ~ sQ378_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f13883,f7155,f9866,f7546,f7164,f13354,f8011,f7549,f7172]) ).
fof(f13954,plain,
( sQ108_spl
| ~ sQ238_spl
| ~ sQ298_spl
| ~ sQ551_spl
| ~ sQ164_spl
| ~ sQ237_spl
| ~ sQ390_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f13889,f6643,f9908,f7588,f7076,f13378,f8053,f7591,f6656]) ).
fof(f14335,plain,
( ~ v1_yellow_3(sK215_skl)
| ~ with_infima_relstr(sK215_skl)
| ~ with_suprema_relstr(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| ~ lower_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| ~ transitive_relstr(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1118,f3285]) ).
fof(f14341,plain,
( ~ v1_yellow_3(sK198_skl)
| ~ with_infima_relstr(sK198_skl)
| ~ with_suprema_relstr(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| ~ lower_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| ~ transitive_relstr(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1118,f3155]) ).
fof(f14342,plain,
( ~ v1_yellow_3(sK197_skl)
| ~ with_infima_relstr(sK197_skl)
| ~ with_suprema_relstr(sK197_skl)
| ~ v3_waybel_3(sK197_skl)
| ~ lower_bounded_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1118,f3139]) ).
fof(f14400,plain,
( ~ sQ499_spl
| ~ sQ226_spl
| ~ sQ286_spl
| ~ sQ545_spl
| ~ sQ180_spl
| ~ sQ225_spl
| ~ sQ378_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f14335,f7155,f9866,f7546,f7164,f13354,f8011,f7549,f12726]) ).
fof(f14406,plain,
( ~ sQ505_spl
| ~ sQ238_spl
| ~ sQ298_spl
| ~ sQ551_spl
| ~ sQ164_spl
| ~ sQ237_spl
| ~ sQ390_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f14341,f6643,f9908,f7588,f7076,f13378,f8053,f7591,f12750]) ).
fof(f14407,plain,
( ~ sQ506_spl
| ~ sQ240_spl
| ~ sQ300_spl
| ~ sQ552_spl
| ~ sQ165_spl
| ~ sQ239_spl
| ~ sQ392_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f14342,f6618,f9915,f7595,f7080,f13382,f8060,f7598,f12754]) ).
fof(f14463,plain,
( v1_waybel_2(sK215_skl)
| ~ with_infima_relstr(sK215_skl)
| ~ with_suprema_relstr(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| ~ lower_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| ~ transitive_relstr(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1119,f3285]) ).
fof(f14467,plain,
( v1_waybel_2(sK201_skl)
| ~ with_infima_relstr(sK201_skl)
| ~ with_suprema_relstr(sK201_skl)
| ~ v3_waybel_3(sK201_skl)
| ~ lower_bounded_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1119,f3193]) ).
fof(f14469,plain,
( v1_waybel_2(sK198_skl)
| ~ with_infima_relstr(sK198_skl)
| ~ with_suprema_relstr(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| ~ lower_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| ~ transitive_relstr(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1119,f3155]) ).
fof(f14470,plain,
( v1_waybel_2(sK197_skl)
| ~ with_infima_relstr(sK197_skl)
| ~ with_suprema_relstr(sK197_skl)
| ~ v3_waybel_3(sK197_skl)
| ~ lower_bounded_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1119,f3139]) ).
fof(f14538,definition,
( sQ561_spl
<=> v1_waybel_2(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ561_spl])],[split_symbol_definition]) ).
fof(f14541,plain,
( sQ561_spl
| ~ sQ226_spl
| ~ sQ286_spl
| ~ sQ545_spl
| ~ sQ180_spl
| ~ sQ225_spl
| ~ sQ378_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f14463,f7155,f9866,f7546,f7164,f13354,f8011,f7549,f14538]) ).
fof(f14554,definition,
( sQ565_spl
<=> v1_waybel_2(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ565_spl])],[split_symbol_definition]) ).
fof(f14557,plain,
( sQ565_spl
| ~ sQ234_spl
| ~ sQ294_spl
| ~ sQ549_spl
| ~ sQ162_spl
| ~ sQ233_spl
| ~ sQ386_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f14467,f6769,f9894,f7574,f7068,f13370,f8039,f7577,f14554]) ).
fof(f14562,definition,
( sQ567_spl
<=> v1_waybel_2(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition]) ).
fof(f14565,plain,
( sQ567_spl
| ~ sQ238_spl
| ~ sQ298_spl
| ~ sQ551_spl
| ~ sQ164_spl
| ~ sQ237_spl
| ~ sQ390_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f14469,f6643,f9908,f7588,f7076,f13378,f8053,f7591,f14562]) ).
fof(f14566,definition,
( sQ568_spl
<=> v1_waybel_2(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition]) ).
fof(f14569,plain,
( sQ568_spl
| ~ sQ240_spl
| ~ sQ300_spl
| ~ sQ552_spl
| ~ sQ165_spl
| ~ sQ239_spl
| ~ sQ392_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f14470,f6618,f9915,f7595,f7080,f13382,f8060,f7598,f14566]) ).
fof(f14640,plain,
( v2_waybel_2(sK215_skl)
| ~ with_infima_relstr(sK215_skl)
| ~ with_suprema_relstr(sK215_skl)
| ~ v3_waybel_3(sK215_skl)
| ~ lower_bounded_relstr(sK215_skl)
| ~ antisymmetric_relstr(sK215_skl)
| ~ transitive_relstr(sK215_skl)
| ~ rel_str(sK215_skl) ),
inference(resolution,[status(thm)],[f1120,f3285]) ).
fof(f14644,plain,
( v2_waybel_2(sK201_skl)
| ~ with_infima_relstr(sK201_skl)
| ~ with_suprema_relstr(sK201_skl)
| ~ v3_waybel_3(sK201_skl)
| ~ lower_bounded_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1120,f3193]) ).
fof(f14646,plain,
( v2_waybel_2(sK198_skl)
| ~ with_infima_relstr(sK198_skl)
| ~ with_suprema_relstr(sK198_skl)
| ~ v3_waybel_3(sK198_skl)
| ~ lower_bounded_relstr(sK198_skl)
| ~ antisymmetric_relstr(sK198_skl)
| ~ transitive_relstr(sK198_skl)
| ~ rel_str(sK198_skl) ),
inference(resolution,[status(thm)],[f1120,f3155]) ).
fof(f14647,plain,
( v2_waybel_2(sK197_skl)
| ~ with_infima_relstr(sK197_skl)
| ~ with_suprema_relstr(sK197_skl)
| ~ v3_waybel_3(sK197_skl)
| ~ lower_bounded_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1120,f3139]) ).
fof(f14715,definition,
( sQ576_spl
<=> v2_waybel_2(sK215_skl) ),
introduced(definition,[new_symbols(definition,[sQ576_spl])],[split_symbol_definition]) ).
fof(f14718,plain,
( sQ576_spl
| ~ sQ226_spl
| ~ sQ286_spl
| ~ sQ545_spl
| ~ sQ180_spl
| ~ sQ225_spl
| ~ sQ378_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f14640,f7155,f9866,f7546,f7164,f13354,f8011,f7549,f14715]) ).
fof(f14731,definition,
( sQ580_spl
<=> v2_waybel_2(sK201_skl) ),
introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition]) ).
fof(f14734,plain,
( sQ580_spl
| ~ sQ234_spl
| ~ sQ294_spl
| ~ sQ549_spl
| ~ sQ162_spl
| ~ sQ233_spl
| ~ sQ386_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f14644,f6769,f9894,f7574,f7068,f13370,f8039,f7577,f14731]) ).
fof(f14739,definition,
( sQ582_spl
<=> v2_waybel_2(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f14742,plain,
( sQ582_spl
| ~ sQ238_spl
| ~ sQ298_spl
| ~ sQ551_spl
| ~ sQ164_spl
| ~ sQ237_spl
| ~ sQ390_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f14646,f6643,f9908,f7588,f7076,f13378,f8053,f7591,f14739]) ).
fof(f14743,definition,
( sQ583_spl
<=> v2_waybel_2(sK197_skl) ),
introduced(definition,[new_symbols(definition,[sQ583_spl])],[split_symbol_definition]) ).
fof(f14746,plain,
( sQ583_spl
| ~ sQ240_spl
| ~ sQ300_spl
| ~ sQ552_spl
| ~ sQ165_spl
| ~ sQ239_spl
| ~ sQ392_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f14647,f6618,f9915,f7595,f7080,f13382,f8060,f7598,f14743]) ).
fof(f15169,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f4495,f4648]) ).
fof(f15346,definition,
( sQ600_spl
<=> empty(powerset(sK260_skl)) ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f15347,plain,
( ~ sQ600_spl
| empty(powerset(sK260_skl)) ),
inference(component_clause,[status(thm)],[f15346]) ).
fof(f15378,plain,
( ~ sQ600_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15347,f2403]) ).
fof(f15379,plain,
~ sQ600_spl,
inference(contradiction_clause,[status(thm)],[f15378]) ).
fof(f15412,definition,
( sQ610_spl
<=> empty(powerset(sK422_skl)) ),
introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition]) ).
fof(f15413,plain,
( ~ sQ610_spl
| empty(powerset(sK422_skl)) ),
inference(component_clause,[status(thm)],[f15412]) ).
fof(f15444,plain,
( ~ sQ610_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15413,f2403]) ).
fof(f15445,plain,
~ sQ610_spl,
inference(contradiction_clause,[status(thm)],[f15444]) ).
fof(f15571,plain,
( connected_relstr(sK201_skl)
| ~ trivial_carrier(sK201_skl)
| empty_carrier(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1142,f3193]) ).
fof(f15588,plain,
( sQ429_spl
| ~ sQ454_spl
| sQ126_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f15571,f6769,f6772,f11921,f10824]) ).
fof(f16036,plain,
! [X0,X1] :
( ~ empty(X0)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f1778,f4728]) ).
fof(f16039,plain,
! [X0,X1] :
( element(sK93_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f1778,f4220]) ).
fof(f16042,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ in(X1,X0)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f16036,f15169]) ).
fof(f16044,plain,
( sQ444_spl
| sQ445_spl ),
inference(split_clause,[status(thm)],[f16042,f11151,f11147]) ).
fof(f16101,plain,
( v3_waybel_3(sK201_skl)
| ~ v2_waybel_3(sK201_skl)
| ~ up_complete_relstr(sK201_skl)
| ~ lower_bounded_relstr(sK201_skl)
| ~ with_suprema_relstr(sK201_skl)
| ~ antisymmetric_relstr(sK201_skl)
| ~ transitive_relstr(sK201_skl)
| ~ rel_str(sK201_skl) ),
inference(resolution,[status(thm)],[f1157,f3193]) ).
fof(f16104,plain,
( v3_waybel_3(sK197_skl)
| ~ v2_waybel_3(sK197_skl)
| ~ up_complete_relstr(sK197_skl)
| ~ lower_bounded_relstr(sK197_skl)
| ~ with_suprema_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1157,f3139]) ).
fof(f16169,plain,
( sQ549_spl
| ~ sQ488_spl
| ~ sQ129_spl
| ~ sQ162_spl
| ~ sQ294_spl
| ~ sQ233_spl
| ~ sQ386_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f16101,f6769,f9894,f7574,f8039,f7068,f6782,f12512,f13370]) ).
fof(f16172,plain,
( sQ552_spl
| ~ sQ491_spl
| ~ sQ103_spl
| ~ sQ165_spl
| ~ sQ300_spl
| ~ sQ239_spl
| ~ sQ392_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f16104,f6618,f9915,f7595,f8060,f7080,f6631,f12524,f13382]) ).
fof(f16234,plain,
( bounded_relstr(sK230_skl)
| ~ upper_bounded_relstr(sK230_skl)
| ~ rel_str(sK230_skl) ),
inference(resolution,[status(thm)],[f1159,f3374]) ).
fof(f16235,plain,
( bounded_relstr(sK218_skl)
| ~ upper_bounded_relstr(sK218_skl)
| ~ rel_str(sK218_skl) ),
inference(resolution,[status(thm)],[f1159,f3313]) ).
fof(f16237,plain,
( bounded_relstr(sK199_skl)
| ~ upper_bounded_relstr(sK199_skl)
| ~ rel_str(sK199_skl) ),
inference(resolution,[status(thm)],[f1159,f3177]) ).
fof(f16240,plain,
( bounded_relstr(sK181_skl)
| ~ upper_bounded_relstr(sK181_skl)
| ~ rel_str(sK181_skl) ),
inference(resolution,[status(thm)],[f1159,f3062]) ).
fof(f16249,plain,
( sQ375_spl
| ~ sQ281_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f16234,f7370,f7994,f9855]) ).
fof(f16250,plain,
( sQ377_spl
| ~ sQ283_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f16235,f7185,f8001,f9862]) ).
fof(f16252,plain,
( sQ389_spl
| ~ sQ295_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f16237,f6668,f8043,f9904]) ).
fof(f16255,plain,
( sQ397_spl
| ~ sQ303_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f16240,f6284,f8071,f9932]) ).
fof(f16400,plain,
( v2_waybel_3(sK197_skl)
| ~ connected_relstr(sK197_skl)
| ~ complete_relstr(sK197_skl)
| ~ antisymmetric_relstr(sK197_skl)
| ~ transitive_relstr(sK197_skl)
| empty_carrier(sK197_skl)
| ~ rel_str(sK197_skl) ),
inference(resolution,[status(thm)],[f1177,f3139]) ).
fof(f16457,plain,
( sQ491_spl
| ~ sQ432_spl
| ~ sQ101_spl
| ~ sQ239_spl
| ~ sQ392_spl
| sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f16400,f6618,f6621,f9915,f7595,f6624,f10836,f12524]) ).
fof(f16502,plain,
! [X0] :
( ~ sQ311_spl
| in(sK93_skl(X0,the_carrier(sK473_skl)),sK474_skl)
| subset(the_carrier(sK473_skl),X0) ),
inference(resolution,[status(thm)],[f16039,f8188]) ).
fof(f16685,plain,
! [X0,X1] : set_difference(set_union2(X0,X1),X0) = set_difference(X1,X0),
inference(paramodulation,[status(thm)],[f1227,f4505]) ).
fof(f16749,definition,
! [X0] :
( sQ624_spl
<=> ~ subset(X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f16750,plain,
! [X0] :
( ~ sQ624_spl
| ~ subset(X0,X0) ),
inference(component_clause,[status(thm)],[f16749]) ).
fof(f16769,plain,
( ~ sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16750,f5679]) ).
fof(f16770,plain,
~ sQ624_spl,
inference(contradiction_clause,[status(thm)],[f16769]) ).
fof(f16808,plain,
( ~ sQ311_spl
| subset(the_carrier(sK473_skl),sK474_skl)
| subset(the_carrier(sK473_skl),sK474_skl) ),
inference(resolution,[status(thm)],[f16502,f1779]) ).
fof(f16815,definition,
( sQ625_spl
<=> subset(the_carrier(sK473_skl),sK474_skl) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f16818,plain,
( ~ sQ311_spl
| sQ625_spl ),
inference(split_clause,[status(thm)],[f16808,f16815,f8182]) ).
fof(f17213,definition,
! [X0] :
( sQ650_spl
<=> in(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition]) ).
fof(f17214,plain,
! [X0] :
( ~ sQ650_spl
| in(X0,empty_set) ),
inference(component_clause,[status(thm)],[f17213]) ).
fof(f17220,plain,
( ~ sQ650_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17214,f5739]) ).
fof(f17221,plain,
~ sQ650_spl,
inference(contradiction_clause,[status(thm)],[f17220]) ).
fof(f17244,definition,
( sQ651_spl
<=> one_sorted_str(sK473_skl) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f17246,plain,
( sQ651_spl
| ~ one_sorted_str(sK473_skl) ),
inference(component_clause,[status(thm)],[f17244]) ).
fof(f17248,plain,
( sQ651_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17246,f8895]) ).
fof(f17249,plain,
sQ651_spl,
inference(contradiction_clause,[status(thm)],[f17248]) ).
fof(f17331,plain,
( boolean_relstr(sK230_skl)
| ~ complemented_relstr(sK230_skl)
| ~ distributive_relstr(sK230_skl)
| ~ bounded_relstr(sK230_skl)
| ~ with_infima_relstr(sK230_skl)
| ~ with_suprema_relstr(sK230_skl)
| ~ antisymmetric_relstr(sK230_skl)
| ~ transitive_relstr(sK230_skl)
| ~ rel_str(sK230_skl) ),
inference(resolution,[status(thm)],[f5675,f3369]) ).
fof(f17338,plain,
( boolean_relstr(sK199_skl)
| ~ complemented_relstr(sK199_skl)
| ~ distributive_relstr(sK199_skl)
| ~ bounded_relstr(sK199_skl)
| ~ with_infima_relstr(sK199_skl)
| ~ with_suprema_relstr(sK199_skl)
| ~ antisymmetric_relstr(sK199_skl)
| ~ transitive_relstr(sK199_skl)
| ~ rel_str(sK199_skl) ),
inference(resolution,[status(thm)],[f5675,f3174]) ).
fof(f17381,definition,
( sQ652_spl
<=> distributive_relstr(sK232_skl) ),
introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition]) ).
fof(f17383,plain,
( sQ652_spl
| ~ distributive_relstr(sK232_skl) ),
inference(component_clause,[status(thm)],[f17381]) ).
fof(f17391,definition,
( sQ655_spl
<=> distributive_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ655_spl])],[split_symbol_definition]) ).
fof(f17393,plain,
( sQ655_spl
| ~ distributive_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f17391]) ).
fof(f17394,definition,
( sQ656_spl
<=> complemented_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition]) ).
fof(f17396,plain,
( sQ656_spl
| ~ complemented_relstr(sK230_skl) ),
inference(component_clause,[status(thm)],[f17394]) ).
fof(f17397,definition,
( sQ657_spl
<=> boolean_relstr(sK230_skl) ),
introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition]) ).
fof(f17400,plain,
( sQ657_spl
| ~ sQ656_spl
| ~ sQ655_spl
| ~ sQ375_spl
| ~ sQ222_spl
| ~ sQ282_spl
| ~ sQ221_spl
| ~ sQ374_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f17331,f7370,f9852,f7532,f7997,f7535,f9855,f17391,f17394,f17397]) ).
fof(f17461,definition,
( sQ676_spl
<=> distributive_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition]) ).
fof(f17463,plain,
( sQ676_spl
| ~ distributive_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f17461]) ).
fof(f17464,definition,
( sQ677_spl
<=> complemented_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition]) ).
fof(f17466,plain,
( sQ677_spl
| ~ complemented_relstr(sK199_skl) ),
inference(component_clause,[status(thm)],[f17464]) ).
fof(f17467,definition,
( sQ678_spl
<=> boolean_relstr(sK199_skl) ),
introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition]) ).
fof(f17470,plain,
( sQ678_spl
| ~ sQ677_spl
| ~ sQ676_spl
| ~ sQ389_spl
| ~ sQ236_spl
| ~ sQ296_spl
| ~ sQ235_spl
| ~ sQ388_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f17338,f6668,f9901,f7581,f8046,f7584,f9904,f17461,f17464,f17467]) ).
fof(f17471,definition,
( sQ679_spl
<=> distributive_relstr(sK198_skl) ),
introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition]) ).
fof(f17473,plain,
( sQ679_spl
| ~ distributive_relstr(sK198_skl) ),
inference(component_clause,[status(thm)],[f17471]) ).
fof(f17564,plain,
( sQ679_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17473,f3166]) ).
fof(f17565,plain,
sQ679_spl,
inference(contradiction_clause,[status(thm)],[f17564]) ).
fof(f17566,plain,
( sQ677_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17466,f3183]) ).
fof(f17567,plain,
sQ677_spl,
inference(contradiction_clause,[status(thm)],[f17566]) ).
fof(f17568,plain,
( sQ676_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17463,f3181]) ).
fof(f17569,plain,
sQ676_spl,
inference(contradiction_clause,[status(thm)],[f17568]) ).
fof(f17570,plain,
( sQ656_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17396,f3379]) ).
fof(f17571,plain,
sQ656_spl,
inference(contradiction_clause,[status(thm)],[f17570]) ).
fof(f17572,plain,
( sQ655_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17393,f3377]) ).
fof(f17573,plain,
sQ655_spl,
inference(contradiction_clause,[status(thm)],[f17572]) ).
fof(f17574,plain,
( sQ652_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17383,f3395]) ).
fof(f17575,plain,
sQ652_spl,
inference(contradiction_clause,[status(thm)],[f17574]) ).
fof(f17576,plain,
( sQ296_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8048,f3185]) ).
fof(f17577,plain,
sQ296_spl,
inference(contradiction_clause,[status(thm)],[f17576]) ).
fof(f17578,plain,
( sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7999,f3372]) ).
fof(f17579,plain,
sQ282_spl,
inference(contradiction_clause,[status(thm)],[f17578]) ).
fof(f17580,plain,
( sQ163_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7074,f3177]) ).
fof(f17581,plain,
sQ163_spl,
inference(contradiction_clause,[status(thm)],[f17580]) ).
fof(f17582,plain,
( sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7586,f3186]) ).
fof(f17583,plain,
sQ236_spl,
inference(contradiction_clause,[status(thm)],[f17582]) ).
fof(f17584,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7381,f3374]) ).
fof(f17585,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f17584]) ).
fof(f17586,plain,
( sQ222_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7537,f3373]) ).
fof(f17587,plain,
sQ222_spl,
inference(contradiction_clause,[status(thm)],[f17586]) ).
fof(f17743,plain,
! [X0,X1] : set_difference(set_union2(X0,X1),X0) = set_difference(set_difference(X1,X0),X0),
inference(paramodulation,[status(thm)],[f4479,f16685]) ).
fof(f17779,plain,
! [X0,X1] : set_difference(X0,X1) = set_difference(set_difference(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f16685,f17743]) ).
fof(f17903,plain,
! [X0,X1] : disjoint(set_difference(X0,X1),X1),
inference(resolution,[status(thm)],[f17779,f4747]) ).
fof(f18144,plain,
! [X0,X1] : disjoint(X0,set_difference(X1,X0)),
inference(resolution,[status(thm)],[f17903,f4017]) ).
fof(f18204,definition,
! [X0,X1] :
( sQ713_spl
<=> ~ disjoint(set_difference(X0,X1),X1) ),
introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition]) ).
fof(f18205,plain,
! [X0,X1] :
( ~ sQ713_spl
| ~ disjoint(set_difference(X0,X1),X1) ),
inference(component_clause,[status(thm)],[f18204]) ).
fof(f18208,definition,
! [X0,X1] :
( sQ714_spl
<=> ~ disjoint(X0,set_difference(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f18209,plain,
! [X0,X1] :
( ~ sQ714_spl
| ~ disjoint(X0,set_difference(X1,X0)) ),
inference(component_clause,[status(thm)],[f18208]) ).
fof(f18212,definition,
! [X0,X1] :
( sQ715_spl
<=> ~ v5_membered(set_difference(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f18213,plain,
! [X0,X1] :
( ~ sQ715_spl
| ~ v5_membered(set_difference(X0,X1)) ),
inference(component_clause,[status(thm)],[f18212]) ).
fof(f18226,definition,
! [X0,X1] :
( sQ716_spl
<=> ~ v4_membered(set_difference(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ716_spl])],[split_symbol_definition]) ).
fof(f18227,plain,
! [X0,X1] :
( ~ sQ716_spl
| ~ v4_membered(set_difference(X0,X1)) ),
inference(component_clause,[status(thm)],[f18226]) ).
fof(f18237,definition,
! [X0,X1] :
( sQ717_spl
<=> ~ v3_membered(set_difference(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition]) ).
fof(f18238,plain,
! [X0,X1] :
( ~ sQ717_spl
| ~ v3_membered(set_difference(X0,X1)) ),
inference(component_clause,[status(thm)],[f18237]) ).
fof(f18246,definition,
! [X0,X1] :
( sQ718_spl
<=> ~ v2_membered(set_difference(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition]) ).
fof(f18247,plain,
! [X0,X1] :
( ~ sQ718_spl
| ~ v2_membered(set_difference(X0,X1)) ),
inference(component_clause,[status(thm)],[f18246]) ).
fof(f18253,definition,
! [X0,X1] :
( sQ719_spl
<=> ~ v1_membered(set_difference(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition]) ).
fof(f18254,plain,
! [X0,X1] :
( ~ sQ719_spl
| ~ v1_membered(set_difference(X0,X1)) ),
inference(component_clause,[status(thm)],[f18253]) ).
fof(f18257,plain,
! [X0] :
( ~ sQ715_spl
| ~ v5_membered(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2717,f18213]) ).
fof(f18261,plain,
! [X0] :
( ~ sQ716_spl
| ~ v4_membered(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2710,f18227]) ).
fof(f18268,plain,
! [X0] :
( ~ sQ717_spl
| ~ v3_membered(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2648,f18238]) ).
fof(f18278,plain,
! [X0] :
( ~ sQ718_spl
| ~ v2_membered(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2643,f18247]) ).
fof(f18291,plain,
! [X0] :
( ~ sQ719_spl
| ~ v1_membered(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2639,f18254]) ).
fof(f18302,plain,
( ~ sQ714_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18209,f18144]) ).
fof(f18303,plain,
~ sQ714_spl,
inference(contradiction_clause,[status(thm)],[f18302]) ).
fof(f18304,plain,
( ~ sQ713_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18205,f17903]) ).
fof(f18305,plain,
~ sQ713_spl,
inference(contradiction_clause,[status(thm)],[f18304]) ).
fof(f18306,plain,
( ~ sQ715_spl
| sQ407_spl ),
inference(split_clause,[status(thm)],[f18257,f10227,f18212]) ).
fof(f18308,plain,
( ~ sQ716_spl
| sQ317_spl ),
inference(split_clause,[status(thm)],[f18261,f8507,f18226]) ).
fof(f18311,plain,
( ~ sQ717_spl
| sQ315_spl ),
inference(split_clause,[status(thm)],[f18268,f8477,f18237]) ).
fof(f18315,plain,
( ~ sQ718_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f18278,f8443,f18246]) ).
fof(f18320,plain,
( ~ sQ719_spl
| sQ309_spl ),
inference(split_clause,[status(thm)],[f18291,f8143,f18253]) ).
fof(f18831,definition,
! [X0,X1] :
( sQ730_spl
<=> ~ subset(X0,set_union2(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ730_spl])],[split_symbol_definition]) ).
fof(f18832,plain,
! [X0,X1] :
( ~ sQ730_spl
| ~ subset(X0,set_union2(X0,X1)) ),
inference(component_clause,[status(thm)],[f18831]) ).
fof(f18838,plain,
( ~ sQ730_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18832,f4743]) ).
fof(f18839,plain,
~ sQ730_spl,
inference(contradiction_clause,[status(thm)],[f18838]) ).
fof(f19059,definition,
! [X0,X1] :
( sQ731_spl
<=> ~ subset(X0,set_union2(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f19060,plain,
! [X0,X1] :
( ~ sQ731_spl
| ~ subset(X0,set_union2(X1,X0)) ),
inference(component_clause,[status(thm)],[f19059]) ).
fof(f19064,plain,
( ~ sQ731_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19060,f9098]) ).
fof(f19065,plain,
~ sQ731_spl,
inference(contradiction_clause,[status(thm)],[f19064]) ).
fof(f19070,plain,
( ~ sQ140_spl
| ~ subset(the_carrier(sK473_skl),sK474_skl)
| the_carrier(sK473_skl) = sK474_skl ),
inference(resolution,[status(thm)],[f1253,f13313]) ).
fof(f19078,definition,
( sQ732_spl
<=> subset(sK474_skl,the_carrier(sK473_skl)) ),
introduced(definition,[new_symbols(definition,[sQ732_spl])],[split_symbol_definition]) ).
fof(f19080,plain,
( sQ732_spl
| ~ subset(sK474_skl,the_carrier(sK473_skl)) ),
inference(component_clause,[status(thm)],[f19078]) ).
fof(f19082,plain,
( ~ sQ140_spl
| ~ sQ625_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f19070,f7148,f16815,f6861]) ).
fof(f19083,plain,
( sQ732_spl
| ~ sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19080,f13313]) ).
fof(f19084,plain,
( sQ732_spl
| ~ sQ140_spl ),
inference(contradiction_clause,[status(thm)],[f19083]) ).
fof(f19127,plain,
( ~ sQ35_spl
| ~ sQ176_spl
| proper_element(sK474_skl,powerset(sK474_skl)) ),
inference(backward_demodulation,[status(thm)],[f7149,f5538]) ).
fof(f19289,plain,
( ~ sQ35_spl
| ~ sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19127,f6023]) ).
fof(f19290,plain,
( ~ sQ35_spl
| ~ sQ176_spl ),
inference(contradiction_clause,[status(thm)],[f19289]) ).
fof(f19291,plain,
$false,
inference(sat_refutation,[status(thm)],[f5543,f5544,f6249,f6262,f6264,f6296,f6318,f6320,f6322,f6324,f6334,f6341,f6411,f6532,f6563,f6565,f6567,f6569,f6577,f6581,f6591,f6593,f6595,f6630,f6634,f6636,f6638,f6640,f6655,f6661,f6663,f6665,f6781,f6785,f6787,f6789,f6791,f6812,f6814,f6864,f6895,f6899,f6901,f6903,f6905,f6926,f6928,f6970,f7063,f7071,f7079,f7083,f7087,f7091,f7101,f7102,f7104,f7151,f7167,f7171,f7177,f7179,f7181,f7197,f7201,f7205,f7207,f7209,f7211,f7264,f7289,f7365,f7392,f7394,f7420,f7422,f7545,f7552,f7566,f7580,f7594,f7601,f7608,f7615,f7744,f7823,f7914,f7916,f8007,f8014,f8056,f8063,f8077,f8108,f8110,f8112,f8114,f8116,f8118,f8120,f8122,f8124,f8126,f8128,f8130,f8132,f8134,f8136,f8138,f8140,f8149,f8178,f8185,f8187,f8356,f8432,f8449,f8474,f8483,f8504,f8513,f8530,f8773,f8777,f8781,f8852,f9433,f9435,f9437,f9439,f9441,f9443,f9445,f9447,f9449,f9451,f9453,f9455,f9457,f9459,f9461,f9463,f9465,f9467,f9469,f9471,f9473,f9619,f9668,f9681,f9900,f9983,f9985,f9987,f9989,f9991,f9993,f9995,f9997,f9999,f10001,f10003,f10005,f10007,f10009,f10011,f10230,f10331,f10693,f10695,f10719,f10723,f10827,f10902,f10904,f11150,f11245,f11600,f11954,f11996,f12515,f12717,f12721,f12725,f12733,f12737,f12741,f12745,f12749,f12761,f12765,f12769,f12773,f13403,f13405,f13428,f13434,f13514,f13671,f13820,f13826,f13948,f13954,f14400,f14406,f14407,f14541,f14557,f14565,f14569,f14718,f14734,f14742,f14746,f15379,f15445,f15588,f16044,f16169,f16172,f16249,f16250,f16252,f16255,f16457,f16770,f16818,f17221,f17249,f17400,f17470,f17565,f17567,f17569,f17571,f17573,f17575,f17577,f17579,f17581,f17583,f17585,f17587,f18303,f18305,f18306,f18308,f18311,f18315,f18320,f18839,f19065,f19082,f19084,f19290]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU383+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:18:54 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.24/0.55 % Drodi V4.1.1
% 111.41/14.67 % Refutation found
% 111.41/14.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 111.41/14.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.60/15.16 % Elapsed time: 14.768748 seconds
% 4.60/15.16 % CPU time: 112.666004 seconds
% 4.60/15.16 % Total memory used: 513.487 MB
% 4.60/15.16 % Net memory used: 480.355 MB
%------------------------------------------------------------------------------