%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU391+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:23 PM UTC 2026
% Result : Theorem 0.49s 20.68s
% Output : CNFRefutation 0.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 190
% Syntax : Number of formulae : 819 ( 196 unt; 144 def)
% Number of atoms : 2169 ( 44 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 2074 ( 724 ~; 848 |; 309 &)
% ( 149 <=>; 43 =>; 0 <=; 1 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 178 ( 176 usr; 145 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 17 con; 0-3 aty)
% Number of variables : 290 ( 264 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,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(f4,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(f5,axiom,
! [A] :
( rel_str(A)
=> ( ( up_complete_relstr(A)
& lower_bounded_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(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(f8,axiom,
! [A] :
( empty(A)
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( rel_str(A)
=> ( ( complete_relstr(A)
& ~ empty_carrier(A) )
=> ( with_infima_relstr(A)
& with_suprema_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( rel_str(A)
=> ( ( trivial_carrier(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( complete_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( rel_str(A)
=> ( ( complete_relstr(A)
& ~ empty_carrier(A) )
=> ( bounded_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( rel_str(A)
=> ( bounded_relstr(A)
=> ( upper_bounded_relstr(A)
& lower_bounded_relstr(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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(f19,axiom,
! [A] :
( rel_str(A)
=> ( ( upper_bounded_relstr(A)
& lower_bounded_relstr(A) )
=> bounded_relstr(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( rel_str(A)
=> ( ( up_complete_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A) )
=> ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> filter_of_net_str(A,B) = a_2_1_yellow19(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B] :
( ( net_str(B,A)
& ~ empty_carrier(B)
& one_sorted_str(A)
& ~ empty_carrier(A) )
=> element(filter_of_net_str(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
? [A] : rel_str(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
? [A] : one_sorted_str(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A] :
( one_sorted_str(A)
=> ? [B] : net_str(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& boolean_relstr(boole_POSet(A))
& complemented_relstr(boole_POSet(A))
& heyting_relstr(boole_POSet(A))
& distributive_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A,B,C] :
( ( net_str(C,B)
& ~ empty_carrier(C)
& one_sorted_str(B)
& ~ empty_carrier(B) )
=> ( in(A,a_2_1_yellow19(B,C))
<=> ? [D] :
( is_eventually_in(B,C,D)
& A = D
& element(D,powerset(the_carrier(B))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,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(f66,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(f67,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,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(f69,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,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(f73,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(f74,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(f79,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(f82,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
? [A] :
( directed_relstr(A)
& transitive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( in(C,filter_of_net_str(A,B))
<=> ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( in(C,filter_of_net_str(A,B))
<=> ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f92]) ).
fof(f94,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f104,plain,
! [X0] :
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f106,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,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)],[f3]) ).
fof(f110,plain,
! [X0] :
( up_complete_relstr(X0)
| ~ complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f111,plain,
! [X0] :
( join_complete_relstr(X0)
| ~ complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f112,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)],[f4]) ).
fof(f115,plain,
! [X0] :
( lower_bounded_relstr(X0)
| ~ join_complete_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f116,plain,
! [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)
| ~ lower_bounded_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)],[f5]) ).
fof(f123,plain,
! [X0] :
( complete_relstr(X0)
| ~ up_complete_relstr(X0)
| ~ lower_bounded_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)],[f116]) ).
fof(f138,plain,
! [A] :
( finite(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f139,plain,
! [X0] :
( finite(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f147,plain,
! [A] :
( ( with_infima_relstr(A)
& with_suprema_relstr(A)
& ~ empty_carrier(A) )
| ~ complete_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f149,plain,
! [X0] :
( with_suprema_relstr(X0)
| ~ complete_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
! [X0] :
( with_infima_relstr(X0)
| ~ complete_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
! [A] :
( ! [B] :
( finite(B)
| ~ element(B,powerset(A)) )
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f152,plain,
! [X0,X1] :
( finite(X1)
| ~ element(X1,powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
! [A] :
( ( complete_relstr(A)
& antisymmetric_relstr(A)
& transitive_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)],[f15]) ).
fof(f158,plain,
! [X0] :
( transitive_relstr(X0)
| ~ trivial_carrier(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f159,plain,
! [X0] :
( antisymmetric_relstr(X0)
| ~ trivial_carrier(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f160,plain,
! [X0] :
( complete_relstr(X0)
| ~ trivial_carrier(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f161,plain,
! [A] :
( ( bounded_relstr(A)
& ~ empty_carrier(A) )
| ~ complete_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f163,plain,
! [X0] :
( bounded_relstr(X0)
| ~ complete_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f164,plain,
! [A] :
( ( upper_bounded_relstr(A)
& lower_bounded_relstr(A) )
| ~ bounded_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f165,plain,
! [X0] :
( lower_bounded_relstr(X0)
| ~ bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f166,plain,
! [X0] :
( upper_bounded_relstr(X0)
| ~ bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f167,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)],[f18]) ).
fof(f170,plain,
! [X0] :
( connected_relstr(X0)
| ~ trivial_carrier(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f171,plain,
! [A] :
( bounded_relstr(A)
| ~ upper_bounded_relstr(A)
| ~ lower_bounded_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f172,plain,
! [X0] :
( bounded_relstr(X0)
| ~ upper_bounded_relstr(X0)
| ~ lower_bounded_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [A] :
( ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ up_complete_relstr(A)
| ~ with_suprema_relstr(A)
| ~ reflexive_relstr(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f177,plain,
! [X0] :
( upper_bounded_relstr(X0)
| ~ up_complete_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f178,plain,
! [A] :
( ! [B] :
( filter_of_net_str(A,B) = a_2_1_yellow19(A,B)
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f179,plain,
! [X0,X1] :
( filter_of_net_str(X0,X1) = a_2_1_yellow19(X0,X1)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f185,plain,
! [A,B] :
( element(filter_of_net_str(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f186,plain,
! [X0,X1] :
( element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f187,plain,
( ! [A] : rel_str(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f189,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f190,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f191,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f192,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f193,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f198,plain,
rel_str(sK0_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f37]) ).
fof(f199,plain,
rel_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f200,plain,
one_sorted_str(sK1_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f38]) ).
fof(f201,plain,
one_sorted_str(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [A] :
( ? [B] : net_str(B,A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f203,plain,
! [A] :
( net_str(sK2_skl(A),A)
| ~ one_sorted_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B,sK2_skl(A))],[f202]) ).
fof(f204,plain,
! [X0] :
( net_str(sK2_skl(X0),X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f207,plain,
! [A] : element(sK4_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f41]) ).
fof(f208,plain,
! [X0] : element(sK4_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f211,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f220,plain,
! [A] :
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f221,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f222,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f223,plain,
( ! [A] : complete_relstr(boole_POSet(A))
& ! [A] : with_infima_relstr(boole_POSet(A))
& ! [A] : with_suprema_relstr(boole_POSet(A))
& ! [A] : boolean_relstr(boole_POSet(A))
& ! [A] : complemented_relstr(boole_POSet(A))
& ! [A] : heyting_relstr(boole_POSet(A))
& ! [A] : distributive_relstr(boole_POSet(A))
& ! [A] : ~ v1_yellow_3(boole_POSet(A))
& ! [A] : join_complete_relstr(boole_POSet(A))
& ! [A] : up_complete_relstr(boole_POSet(A))
& ! [A] : bounded_relstr(boole_POSet(A))
& ! [A] : upper_bounded_relstr(boole_POSet(A))
& ! [A] : lower_bounded_relstr(boole_POSet(A))
& ! [A] : antisymmetric_relstr(boole_POSet(A))
& ! [A] : transitive_relstr(boole_POSet(A))
& ! [A] : reflexive_relstr(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A))
& ! [A] : ~ empty_carrier(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f224,plain,
! [X0] : ~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f316,plain,
! [A,B,C] :
( ( in(A,a_2_1_yellow19(B,C))
<=> ? [D] :
( is_eventually_in(B,C,D)
& A = D
& element(D,powerset(the_carrier(B))) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f317,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ is_eventually_in(B,C,D)
| A != D
| ~ element(D,powerset(the_carrier(B))) )
| in(A,a_2_1_yellow19(B,C)) )
& ( ? [D] :
( is_eventually_in(B,C,D)
& A = D
& element(D,powerset(the_carrier(B))) )
| ~ in(A,a_2_1_yellow19(B,C)) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(NNF_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ is_eventually_in(B,C,D)
| A != D
| ~ element(D,powerset(the_carrier(B))) )
| in(A,a_2_1_yellow19(B,C)) )
& ! [A] :
( ? [D] :
( is_eventually_in(B,C,D)
& A = D
& element(D,powerset(the_carrier(B))) )
| ~ in(A,a_2_1_yellow19(B,C)) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(miniscoping,[status(thm)],[f317]) ).
fof(f319,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ is_eventually_in(B,C,D)
| A != D
| ~ element(D,powerset(the_carrier(B))) )
| in(A,a_2_1_yellow19(B,C)) )
& ! [A] :
( ( is_eventually_in(B,C,sK6_skl(A,C,B))
& A = sK6_skl(A,C,B)
& element(sK6_skl(A,C,B),powerset(the_carrier(B))) )
| ~ in(A,a_2_1_yellow19(B,C)) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(D,sK6_skl(A,C,B))],[f318]) ).
fof(f320,plain,
! [X0,X1,X2] :
( element(sK6_skl(X2,X1,X0),powerset(the_carrier(X0)))
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f321,plain,
! [X0,X1,X2] :
( X2 = sK6_skl(X2,X1,X0)
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f322,plain,
! [X0,X1,X2] :
( is_eventually_in(X0,X1,sK6_skl(X2,X1,X0))
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f323,plain,
! [X0,X1,X2,X3] :
( ~ is_eventually_in(X0,X1,X3)
| X2 != X3
| ~ element(X3,powerset(the_carrier(X0)))
| in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f341,plain,
( connected_relstr(sK9_skl)
& antisymmetric_relstr(sK9_skl)
& transitive_relstr(sK9_skl)
& reflexive_relstr(sK9_skl)
& ~ empty_carrier(sK9_skl)
& rel_str(sK9_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f65]) ).
fof(f342,plain,
rel_str(sK9_skl),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f343,plain,
~ empty_carrier(sK9_skl),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f348,plain,
( join_complete_relstr(sK10_skl)
& up_complete_relstr(sK10_skl)
& bounded_relstr(sK10_skl)
& upper_bounded_relstr(sK10_skl)
& lower_bounded_relstr(sK10_skl)
& complete_relstr(sK10_skl)
& with_infima_relstr(sK10_skl)
& with_suprema_relstr(sK10_skl)
& antisymmetric_relstr(sK10_skl)
& transitive_relstr(sK10_skl)
& reflexive_relstr(sK10_skl)
& strict_rel_str(sK10_skl)
& ~ empty_carrier(sK10_skl)
& rel_str(sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f66]) ).
fof(f349,plain,
rel_str(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f350,plain,
~ empty_carrier(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f351,plain,
strict_rel_str(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f352,plain,
reflexive_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f353,plain,
transitive_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f354,plain,
antisymmetric_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f355,plain,
with_suprema_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f357,plain,
complete_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f360,plain,
bounded_relstr(sK10_skl),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f363,plain,
( finite(sK11_skl)
& ~ empty(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f67]) ).
fof(f365,plain,
finite(sK11_skl),
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f366,plain,
( complete_relstr(sK12_skl)
& antisymmetric_relstr(sK12_skl)
& transitive_relstr(sK12_skl)
& reflexive_relstr(sK12_skl)
& strict_rel_str(sK12_skl)
& ~ empty_carrier(sK12_skl)
& rel_str(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f68]) ).
fof(f367,plain,
rel_str(sK12_skl),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f368,plain,
~ empty_carrier(sK12_skl),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f369,plain,
strict_rel_str(sK12_skl),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f370,plain,
reflexive_relstr(sK12_skl),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f373,plain,
complete_relstr(sK12_skl),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f374,plain,
( relation(sK13_skl)
& empty(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f69]) ).
fof(f375,plain,
empty(sK13_skl),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f386,plain,
( with_infima_relstr(sK16_skl)
& with_suprema_relstr(sK16_skl)
& boolean_relstr(sK16_skl)
& complemented_relstr(sK16_skl)
& heyting_relstr(sK16_skl)
& distributive_relstr(sK16_skl)
& ~ v1_yellow_3(sK16_skl)
& bounded_relstr(sK16_skl)
& upper_bounded_relstr(sK16_skl)
& lower_bounded_relstr(sK16_skl)
& antisymmetric_relstr(sK16_skl)
& transitive_relstr(sK16_skl)
& reflexive_relstr(sK16_skl)
& strict_rel_str(sK16_skl)
& ~ trivial_carrier(sK16_skl)
& ~ empty_carrier(sK16_skl)
& rel_str(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f72]) ).
fof(f387,plain,
rel_str(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f388,plain,
~ empty_carrier(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f390,plain,
strict_rel_str(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f391,plain,
reflexive_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f392,plain,
transitive_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f393,plain,
antisymmetric_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f394,plain,
lower_bounded_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f395,plain,
upper_bounded_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f396,plain,
bounded_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f404,plain,
( trivial_carrier(sK17_skl)
& complete_relstr(sK17_skl)
& with_infima_relstr(sK17_skl)
& with_suprema_relstr(sK17_skl)
& antisymmetric_relstr(sK17_skl)
& transitive_relstr(sK17_skl)
& reflexive_relstr(sK17_skl)
& strict_rel_str(sK17_skl)
& ~ empty_carrier(sK17_skl)
& rel_str(sK17_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f73]) ).
fof(f405,plain,
rel_str(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f406,plain,
~ empty_carrier(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f407,plain,
strict_rel_str(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
reflexive_relstr(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f413,plain,
complete_relstr(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f414,plain,
trivial_carrier(sK17_skl),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f415,plain,
( complete_relstr(sK18_skl)
& with_infima_relstr(sK18_skl)
& with_suprema_relstr(sK18_skl)
& antisymmetric_relstr(sK18_skl)
& transitive_relstr(sK18_skl)
& reflexive_relstr(sK18_skl)
& strict_rel_str(sK18_skl)
& ~ empty_carrier(sK18_skl)
& rel_str(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f74]) ).
fof(f416,plain,
rel_str(sK18_skl),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f417,plain,
~ empty_carrier(sK18_skl),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f418,plain,
strict_rel_str(sK18_skl),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f419,plain,
reflexive_relstr(sK18_skl),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f424,plain,
complete_relstr(sK18_skl),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f442,plain,
( bounded_relstr(sK23_skl)
& upper_bounded_relstr(sK23_skl)
& lower_bounded_relstr(sK23_skl)
& complete_relstr(sK23_skl)
& with_infima_relstr(sK23_skl)
& with_suprema_relstr(sK23_skl)
& antisymmetric_relstr(sK23_skl)
& transitive_relstr(sK23_skl)
& reflexive_relstr(sK23_skl)
& ~ empty_carrier(sK23_skl)
& rel_str(sK23_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f79]) ).
fof(f443,plain,
rel_str(sK23_skl),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
~ empty_carrier(sK23_skl),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f445,plain,
reflexive_relstr(sK23_skl),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f450,plain,
complete_relstr(sK23_skl),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f453,plain,
bounded_relstr(sK23_skl),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f462,plain,
( ~ empty_carrier(sK26_skl)
& one_sorted_str(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f82]) ).
fof(f463,plain,
one_sorted_str(sK26_skl),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f464,plain,
~ empty_carrier(sK26_skl),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f475,plain,
( directed_relstr(sK29_skl)
& transitive_relstr(sK29_skl)
& strict_rel_str(sK29_skl)
& ~ empty_carrier(sK29_skl)
& rel_str(sK29_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f85]) ).
fof(f476,plain,
rel_str(sK29_skl),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f477,plain,
~ empty_carrier(sK29_skl),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f478,plain,
strict_rel_str(sK29_skl),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f508,plain,
? [A] :
( ? [B] :
( ? [C] :
( in(C,filter_of_net_str(A,B))
<~> ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) ) )
& net_str(B,A)
& ~ empty_carrier(B) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f509,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ element(C,powerset(the_carrier(A)))
| ~ is_eventually_in(A,B,C)
| ~ in(C,filter_of_net_str(A,B)) )
& ( ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) )
| in(C,filter_of_net_str(A,B)) ) )
& net_str(B,A)
& ~ empty_carrier(B) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f508]) ).
fof(f510,plain,
( ( ~ element(sK36_skl,powerset(the_carrier(sK34_skl)))
| ~ is_eventually_in(sK34_skl,sK35_skl,sK36_skl)
| ~ in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) )
& ( ( element(sK36_skl,powerset(the_carrier(sK34_skl)))
& is_eventually_in(sK34_skl,sK35_skl,sK36_skl) )
| in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) )
& net_str(sK35_skl,sK34_skl)
& ~ empty_carrier(sK35_skl)
& one_sorted_str(sK34_skl)
& ~ empty_carrier(sK34_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl,sK36_skl]),skolemize(A,sK34_skl),skolemize(B,sK35_skl),skolemize(C,sK36_skl)],[f509]) ).
fof(f511,plain,
~ empty_carrier(sK34_skl),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f512,plain,
one_sorted_str(sK34_skl),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f513,plain,
~ empty_carrier(sK35_skl),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f514,plain,
net_str(sK35_skl,sK34_skl),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f515,plain,
( is_eventually_in(sK34_skl,sK35_skl,sK36_skl)
| in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f516,plain,
( element(sK36_skl,powerset(the_carrier(sK34_skl)))
| in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f517,plain,
( ~ element(sK36_skl,powerset(the_carrier(sK34_skl)))
| ~ is_eventually_in(sK34_skl,sK35_skl,sK36_skl)
| ~ in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(cnf_transformation,[status(thm)],[f510]) ).
fof(f518,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f519,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f520,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f521,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f520]) ).
fof(f527,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f97]) ).
fof(f528,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f527]) ).
fof(f529,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f528]) ).
fof(f531,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f532,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f531]) ).
fof(f533,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f532]) ).
fof(f534,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f535,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f534]) ).
fof(f536,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f535]) ).
fof(f537,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f538,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f537]) ).
fof(f545,definition,
( sQ0_spl
<=> in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( ~ sQ0_spl
| in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,definition,
( sQ1_spl
<=> is_eventually_in(sK34_skl,sK35_skl,sK36_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f549,plain,
( ~ sQ1_spl
| is_eventually_in(sK34_skl,sK35_skl,sK36_skl) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f551,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f515,f545,f548]) ).
fof(f552,definition,
( sQ2_spl
<=> element(sK36_skl,powerset(the_carrier(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f516,f545,f552]) ).
fof(f556,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f517,f545,f548,f552]) ).
fof(f557,plain,
! [X0,X1,X2] :
( ~ is_eventually_in(X0,X1,X2)
| ~ element(X2,powerset(the_carrier(X0)))
| in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f323]) ).
fof(f559,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK34_skl) ),
inference(resolution,[status(thm)],[f193,f512]) ).
fof(f560,plain,
rel_str(sK35_skl),
inference(resolution,[status(thm)],[f559,f514]) ).
fof(f561,plain,
one_sorted_str(sK35_skl),
inference(resolution,[status(thm)],[f560,f191]) ).
fof(f562,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK35_skl) ),
inference(resolution,[status(thm)],[f561,f193]) ).
fof(f563,plain,
( filter_of_net_str(sK34_skl,sK35_skl) = a_2_1_yellow19(sK34_skl,sK35_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(resolution,[status(thm)],[f179,f514]) ).
fof(f564,definition,
( sQ3_spl
<=> empty_carrier(sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( ~ sQ3_spl
| empty_carrier(sK34_skl) ),
inference(component_clause,[status(thm)],[f564]) ).
fof(f567,definition,
( sQ4_spl
<=> one_sorted_str(sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f569,plain,
( sQ4_spl
| ~ one_sorted_str(sK34_skl) ),
inference(component_clause,[status(thm)],[f567]) ).
fof(f570,definition,
( sQ5_spl
<=> empty_carrier(sK35_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f571,plain,
( ~ sQ5_spl
| empty_carrier(sK35_skl) ),
inference(component_clause,[status(thm)],[f570]) ).
fof(f573,definition,
( sQ6_spl
<=> filter_of_net_str(sK34_skl,sK35_skl) = a_2_1_yellow19(sK34_skl,sK35_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( ~ sQ6_spl
| filter_of_net_str(sK34_skl,sK35_skl) = a_2_1_yellow19(sK34_skl,sK35_skl) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f576,plain,
( sQ6_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f563,f564,f567,f570,f573]) ).
fof(f577,plain,
one_sorted_str(sK0_skl),
inference(resolution,[status(thm)],[f199,f191]) ).
fof(f578,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK1_skl) ),
inference(resolution,[status(thm)],[f201,f193]) ).
fof(f580,plain,
one_sorted_str(sK9_skl),
inference(resolution,[status(thm)],[f342,f191]) ).
fof(f581,plain,
one_sorted_str(sK10_skl),
inference(resolution,[status(thm)],[f349,f191]) ).
fof(f582,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK0_skl) ),
inference(resolution,[status(thm)],[f577,f193]) ).
fof(f583,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f580,f193]) ).
fof(f584,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f581,f193]) ).
fof(f585,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| in(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) ),
inference(resolution,[status(thm)],[f521,f186]) ).
fof(f587,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| in(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f222]) ).
fof(f588,plain,
! [X0,X1] :
( ~ element(X1,powerset(empty_set))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f536,f211]) ).
fof(f589,plain,
! [X0,X1] :
( ~ in(X1,powerset(empty_set))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f588,f519]) ).
fof(f590,plain,
! [X0] :
( ~ sQ0_spl
| element(sK36_skl,X0)
| ~ element(filter_of_net_str(sK34_skl,sK35_skl),powerset(X0)) ),
inference(resolution,[status(thm)],[f533,f546]) ).
fof(f591,plain,
( empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl)
| in(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))) ),
inference(resolution,[status(thm)],[f587,f514]) ).
fof(f592,definition,
( sQ7_spl
<=> in(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f591,f592,f564,f567,f570]) ).
fof(f596,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f571,f513]) ).
fof(f597,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f596]) ).
fof(f598,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f569,f512]) ).
fof(f599,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f598]) ).
fof(f600,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f511]) ).
fof(f601,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f600]) ).
fof(f602,plain,
( sK10_skl = rel_str_of(the_carrier(sK10_skl),the_InternalRel(sK10_skl))
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f351,f104]) ).
fof(f603,definition,
( sQ8_spl
<=> rel_str(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f605,plain,
( sQ8_spl
| ~ rel_str(sK10_skl) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f606,definition,
( sQ9_spl
<=> sK10_skl = rel_str_of(the_carrier(sK10_skl),the_InternalRel(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f602,f603,f606]) ).
fof(f610,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f605,f349]) ).
fof(f611,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f610]) ).
fof(f612,plain,
( join_complete_relstr(sK10_skl)
| ~ reflexive_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f357,f111]) ).
fof(f613,plain,
( up_complete_relstr(sK10_skl)
| ~ reflexive_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f357,f110]) ).
fof(f614,definition,
( sQ10_spl
<=> empty_carrier(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( ~ sQ10_spl
| empty_carrier(sK10_skl) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f617,definition,
( sQ11_spl
<=> reflexive_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f619,plain,
( sQ11_spl
| ~ reflexive_relstr(sK10_skl) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f620,definition,
( sQ12_spl
<=> join_complete_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ12_spl
| ~ sQ11_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f612,f603,f614,f617,f620]) ).
fof(f624,definition,
( sQ13_spl
<=> up_complete_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( sQ13_spl
| ~ sQ11_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f613,f603,f614,f617,f624]) ).
fof(f628,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f352]) ).
fof(f629,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f628]) ).
fof(f630,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f615,f350]) ).
fof(f631,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f632,plain,
one_sorted_str(sK12_skl),
inference(resolution,[status(thm)],[f367,f191]) ).
fof(f634,definition,
( sQ14_spl
<=> lower_bounded_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f639,definition,
( sQ15_spl
<=> transitive_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( sQ15_spl
| ~ transitive_relstr(sK10_skl) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f642,definition,
( sQ16_spl
<=> antisymmetric_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ16_spl
| ~ antisymmetric_relstr(sK10_skl) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ17_spl
<=> with_infima_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( complete_relstr(sK10_skl)
| ~ up_complete_relstr(sK10_skl)
| ~ lower_bounded_relstr(sK10_skl)
| ~ antisymmetric_relstr(sK10_skl)
| ~ transitive_relstr(sK10_skl)
| ~ reflexive_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f123,f355]) ).
fof(f650,definition,
( sQ18_spl
<=> complete_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f653,plain,
( sQ18_spl
| ~ sQ13_spl
| ~ sQ14_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ11_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f649,f603,f614,f617,f639,f642,f634,f624,f650]) ).
fof(f654,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f354]) ).
fof(f655,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f656,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f641,f353]) ).
fof(f657,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f656]) ).
fof(f658,plain,
( ~ sQ0_spl
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl)
| element(sK36_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
inference(resolution,[status(thm)],[f590,f186]) ).
fof(f660,definition,
( sQ19_spl
<=> element(sK36_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f661,plain,
( ~ sQ19_spl
| element(sK36_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
inference(component_clause,[status(thm)],[f660]) ).
fof(f663,definition,
( sQ20_spl
<=> net_str(sK35_skl,sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( sQ20_spl
| ~ net_str(sK35_skl,sK34_skl) ),
inference(component_clause,[status(thm)],[f663]) ).
fof(f666,plain,
( ~ sQ0_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f658,f660,f564,f567,f570,f663,f545]) ).
fof(f667,plain,
( ~ sQ19_spl
| in(sK36_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))
| empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
inference(resolution,[status(thm)],[f661,f521]) ).
fof(f668,definition,
( sQ21_spl
<=> empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( ~ sQ21_spl
| empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f671,definition,
( sQ22_spl
<=> in(sK36_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f674,plain,
( ~ sQ19_spl
| sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f667,f668,f671,f660]) ).
fof(f675,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f665,f514]) ).
fof(f676,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f677,plain,
( ~ sQ21_spl
| ~ one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl)))
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
inference(resolution,[status(thm)],[f669,f221]) ).
fof(f680,definition,
( sQ23_spl
<=> empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( ~ sQ23_spl
| empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,definition,
( sQ24_spl
<=> one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( sQ24_spl
| ~ one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f686,plain,
( ~ sQ21_spl
| ~ sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f677,f680,f683,f668]) ).
fof(f689,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK12_skl) ),
inference(resolution,[status(thm)],[f632,f193]) ).
fof(f698,definition,
( sQ25_spl
<=> upper_bounded_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sK12_skl = rel_str_of(the_carrier(sK12_skl),the_InternalRel(sK12_skl))
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f369,f104]) ).
fof(f703,definition,
( sQ26_spl
<=> rel_str(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f705,plain,
( sQ26_spl
| ~ rel_str(sK12_skl) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,definition,
( sQ27_spl
<=> sK12_skl = rel_str_of(the_carrier(sK12_skl),the_InternalRel(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f702,f703,f706]) ).
fof(f710,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f367]) ).
fof(f711,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f710]) ).
fof(f712,plain,
( join_complete_relstr(sK12_skl)
| ~ reflexive_relstr(sK12_skl)
| empty_carrier(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f373,f111]) ).
fof(f713,plain,
( up_complete_relstr(sK12_skl)
| ~ reflexive_relstr(sK12_skl)
| empty_carrier(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f373,f110]) ).
fof(f714,definition,
( sQ28_spl
<=> empty_carrier(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f715,plain,
( ~ sQ28_spl
| empty_carrier(sK12_skl) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,definition,
( sQ29_spl
<=> reflexive_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( sQ29_spl
| ~ reflexive_relstr(sK12_skl) ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,definition,
( sQ30_spl
<=> join_complete_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( ~ sQ30_spl
| join_complete_relstr(sK12_skl) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,plain,
( sQ30_spl
| ~ sQ29_spl
| sQ28_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f712,f703,f714,f717,f720]) ).
fof(f724,definition,
( sQ31_spl
<=> up_complete_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f725,plain,
( ~ sQ31_spl
| up_complete_relstr(sK12_skl) ),
inference(component_clause,[status(thm)],[f724]) ).
fof(f727,plain,
( sQ31_spl
| ~ sQ29_spl
| sQ28_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f713,f703,f714,f717,f724]) ).
fof(f728,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f370]) ).
fof(f729,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f728]) ).
fof(f730,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f715,f368]) ).
fof(f731,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f732,plain,
! [X0,X1] :
( ~ element(X1,powerset(sK13_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f375,f536]) ).
fof(f734,plain,
one_sorted_str(sK16_skl),
inference(resolution,[status(thm)],[f387,f191]) ).
fof(f735,plain,
( sK16_skl = rel_str_of(the_carrier(sK16_skl),the_InternalRel(sK16_skl))
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f390,f104]) ).
fof(f736,definition,
( sQ32_spl
<=> rel_str(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f738,plain,
( sQ32_spl
| ~ rel_str(sK16_skl) ),
inference(component_clause,[status(thm)],[f736]) ).
fof(f739,definition,
( sQ33_spl
<=> sK16_skl = rel_str_of(the_carrier(sK16_skl),the_InternalRel(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f742,plain,
( sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f735,f736,f739]) ).
fof(f743,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f387]) ).
fof(f744,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f743]) ).
fof(f746,definition,
( sQ34_spl
<=> bounded_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f753,definition,
( sQ35_spl
<=> with_suprema_relstr(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f757,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f734,f193]) ).
fof(f758,plain,
! [X0,X1] :
( ~ in(X1,powerset(sK13_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f732,f519]) ).
fof(f759,plain,
finite(sK13_skl),
inference(resolution,[status(thm)],[f139,f375]) ).
fof(f762,definition,
( sQ36_spl
<=> empty_carrier(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f763,plain,
( ~ sQ36_spl
| empty_carrier(sK16_skl) ),
inference(component_clause,[status(thm)],[f762]) ).
fof(f765,definition,
( sQ37_spl
<=> reflexive_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f767,plain,
( sQ37_spl
| ~ reflexive_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f768,definition,
( sQ38_spl
<=> antisymmetric_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f770,plain,
( sQ38_spl
| ~ antisymmetric_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f778,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f770,f393]) ).
fof(f779,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f778]) ).
fof(f780,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f391]) ).
fof(f781,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f780]) ).
fof(f782,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f388]) ).
fof(f783,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f788,definition,
( sQ41_spl
<=> transitive_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ41_spl
| ~ transitive_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f791,definition,
( sQ42_spl
<=> lower_bounded_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f793,plain,
( sQ42_spl
| ~ lower_bounded_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f791]) ).
fof(f797,definition,
( sQ44_spl
<=> bounded_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f801,definition,
( sQ45_spl
<=> upper_bounded_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f793,f394]) ).
fof(f814,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f813]) ).
fof(f815,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f790,f392]) ).
fof(f816,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f823,plain,
one_sorted_str(sK17_skl),
inference(resolution,[status(thm)],[f405,f191]) ).
fof(f824,plain,
( sK17_skl = rel_str_of(the_carrier(sK17_skl),the_InternalRel(sK17_skl))
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f407,f104]) ).
fof(f825,definition,
( sQ48_spl
<=> rel_str(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f827,plain,
( sQ48_spl
| ~ rel_str(sK17_skl) ),
inference(component_clause,[status(thm)],[f825]) ).
fof(f828,definition,
( sQ49_spl
<=> sK17_skl = rel_str_of(the_carrier(sK17_skl),the_InternalRel(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f831,plain,
( sQ49_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f824,f825,f828]) ).
fof(f832,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f827,f405]) ).
fof(f833,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f832]) ).
fof(f834,plain,
( join_complete_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f413,f111]) ).
fof(f835,plain,
( up_complete_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f413,f110]) ).
fof(f836,definition,
( sQ50_spl
<=> empty_carrier(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f837,plain,
( ~ sQ50_spl
| empty_carrier(sK17_skl) ),
inference(component_clause,[status(thm)],[f836]) ).
fof(f839,definition,
( sQ51_spl
<=> reflexive_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( sQ51_spl
| ~ reflexive_relstr(sK17_skl) ),
inference(component_clause,[status(thm)],[f839]) ).
fof(f842,definition,
( sQ52_spl
<=> join_complete_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f843,plain,
( ~ sQ52_spl
| join_complete_relstr(sK17_skl) ),
inference(component_clause,[status(thm)],[f842]) ).
fof(f845,plain,
( sQ52_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f834,f825,f836,f839,f842]) ).
fof(f846,definition,
( sQ53_spl
<=> up_complete_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f847,plain,
( ~ sQ53_spl
| up_complete_relstr(sK17_skl) ),
inference(component_clause,[status(thm)],[f846]) ).
fof(f849,plain,
( sQ53_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f835,f825,f836,f839,f846]) ).
fof(f850,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f841,f408]) ).
fof(f851,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f850]) ).
fof(f852,plain,
( ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f837,f406]) ).
fof(f853,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f852]) ).
fof(f854,plain,
one_sorted_str(sK18_skl),
inference(resolution,[status(thm)],[f416,f191]) ).
fof(f855,plain,
( sK18_skl = rel_str_of(the_carrier(sK18_skl),the_InternalRel(sK18_skl))
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f418,f104]) ).
fof(f856,definition,
( sQ54_spl
<=> rel_str(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f858,plain,
( sQ54_spl
| ~ rel_str(sK18_skl) ),
inference(component_clause,[status(thm)],[f856]) ).
fof(f859,definition,
( sQ55_spl
<=> sK18_skl = rel_str_of(the_carrier(sK18_skl),the_InternalRel(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f862,plain,
( sQ55_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f855,f856,f859]) ).
fof(f863,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f858,f416]) ).
fof(f864,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f863]) ).
fof(f866,plain,
( with_suprema_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f149,f413]) ).
fof(f867,plain,
( with_suprema_relstr(sK12_skl)
| empty_carrier(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f149,f373]) ).
fof(f868,plain,
( with_suprema_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f149,f357]) ).
fof(f869,definition,
( sQ56_spl
<=> with_suprema_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f872,plain,
( sQ56_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f866,f825,f836,f869]) ).
fof(f873,definition,
( sQ57_spl
<=> with_suprema_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f876,plain,
( sQ57_spl
| sQ28_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f867,f703,f714,f873]) ).
fof(f877,plain,
( sQ35_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f868,f603,f614,f753]) ).
fof(f878,plain,
( with_infima_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f150,f413]) ).
fof(f879,plain,
( with_infima_relstr(sK12_skl)
| empty_carrier(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f150,f373]) ).
fof(f880,plain,
( with_infima_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f150,f357]) ).
fof(f881,definition,
( sQ58_spl
<=> with_infima_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f884,plain,
( sQ58_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f878,f825,f836,f881]) ).
fof(f885,definition,
( sQ59_spl
<=> with_infima_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f888,plain,
( sQ59_spl
| sQ28_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f879,f703,f714,f885]) ).
fof(f889,plain,
( sQ17_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f880,f603,f614,f645]) ).
fof(f890,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f823,f193]) ).
fof(f891,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f854,f193]) ).
fof(f892,plain,
! [X0] :
( finite(X0)
| ~ element(X0,powerset(sK11_skl)) ),
inference(resolution,[status(thm)],[f152,f365]) ).
fof(f893,plain,
( with_infima_relstr(sK18_skl)
| empty_carrier(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f424,f150]) ).
fof(f894,plain,
( with_suprema_relstr(sK18_skl)
| empty_carrier(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f424,f149]) ).
fof(f895,plain,
( join_complete_relstr(sK18_skl)
| ~ reflexive_relstr(sK18_skl)
| empty_carrier(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f424,f111]) ).
fof(f896,plain,
( up_complete_relstr(sK18_skl)
| ~ reflexive_relstr(sK18_skl)
| empty_carrier(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f424,f110]) ).
fof(f897,definition,
( sQ60_spl
<=> empty_carrier(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f898,plain,
( ~ sQ60_spl
| empty_carrier(sK18_skl) ),
inference(component_clause,[status(thm)],[f897]) ).
fof(f900,definition,
( sQ61_spl
<=> with_infima_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f903,plain,
( sQ61_spl
| sQ60_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f893,f856,f897,f900]) ).
fof(f904,definition,
( sQ62_spl
<=> with_suprema_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f907,plain,
( sQ62_spl
| sQ60_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f894,f856,f897,f904]) ).
fof(f908,definition,
( sQ63_spl
<=> reflexive_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f910,plain,
( sQ63_spl
| ~ reflexive_relstr(sK18_skl) ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f911,definition,
( sQ64_spl
<=> join_complete_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( ~ sQ64_spl
| join_complete_relstr(sK18_skl) ),
inference(component_clause,[status(thm)],[f911]) ).
fof(f914,plain,
( sQ64_spl
| ~ sQ63_spl
| sQ60_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f895,f856,f897,f908,f911]) ).
fof(f915,definition,
( sQ65_spl
<=> up_complete_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f916,plain,
( ~ sQ65_spl
| up_complete_relstr(sK18_skl) ),
inference(component_clause,[status(thm)],[f915]) ).
fof(f918,plain,
( sQ65_spl
| ~ sQ63_spl
| sQ60_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f896,f856,f897,f908,f915]) ).
fof(f919,plain,
( ~ sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f898,f417]) ).
fof(f920,plain,
~ sQ60_spl,
inference(contradiction_clause,[status(thm)],[f919]) ).
fof(f921,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f910,f419]) ).
fof(f922,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f921]) ).
fof(f923,plain,
one_sorted_str(sK23_skl),
inference(resolution,[status(thm)],[f443,f191]) ).
fof(f924,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK23_skl) ),
inference(resolution,[status(thm)],[f923,f193]) ).
fof(f925,plain,
( transitive_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f158,f414]) ).
fof(f926,definition,
( sQ66_spl
<=> transitive_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f929,plain,
( sQ66_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f925,f825,f836,f839,f926]) ).
fof(f930,plain,
( with_infima_relstr(sK23_skl)
| empty_carrier(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f450,f150]) ).
fof(f931,plain,
( with_suprema_relstr(sK23_skl)
| empty_carrier(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f450,f149]) ).
fof(f932,plain,
( join_complete_relstr(sK23_skl)
| ~ reflexive_relstr(sK23_skl)
| empty_carrier(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f450,f111]) ).
fof(f933,plain,
( up_complete_relstr(sK23_skl)
| ~ reflexive_relstr(sK23_skl)
| empty_carrier(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f450,f110]) ).
fof(f934,definition,
( sQ67_spl
<=> rel_str(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f936,plain,
( sQ67_spl
| ~ rel_str(sK23_skl) ),
inference(component_clause,[status(thm)],[f934]) ).
fof(f937,definition,
( sQ68_spl
<=> empty_carrier(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( ~ sQ68_spl
| empty_carrier(sK23_skl) ),
inference(component_clause,[status(thm)],[f937]) ).
fof(f940,definition,
( sQ69_spl
<=> with_infima_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f943,plain,
( sQ69_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f930,f934,f937,f940]) ).
fof(f944,definition,
( sQ70_spl
<=> with_suprema_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f947,plain,
( sQ70_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f931,f934,f937,f944]) ).
fof(f948,definition,
( sQ71_spl
<=> reflexive_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( sQ71_spl
| ~ reflexive_relstr(sK23_skl) ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,definition,
( sQ72_spl
<=> join_complete_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f954,plain,
( sQ72_spl
| ~ sQ71_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f932,f934,f937,f948,f951]) ).
fof(f955,definition,
( sQ73_spl
<=> up_complete_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f958,plain,
( sQ73_spl
| ~ sQ71_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f933,f934,f937,f948,f955]) ).
fof(f959,plain,
( ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f938,f444]) ).
fof(f960,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f959]) ).
fof(f961,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f936,f443]) ).
fof(f962,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f961]) ).
fof(f963,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f950,f445]) ).
fof(f964,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f963]) ).
fof(f970,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK26_skl) ),
inference(resolution,[status(thm)],[f463,f193]) ).
fof(f971,plain,
one_sorted_str(sK29_skl),
inference(resolution,[status(thm)],[f476,f191]) ).
fof(f972,plain,
( antisymmetric_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f159,f414]) ).
fof(f973,definition,
( sQ75_spl
<=> antisymmetric_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( sQ75_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f972,f825,f836,f839,f973]) ).
fof(f977,plain,
( complete_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f160,f414]) ).
fof(f978,definition,
( sQ76_spl
<=> complete_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f981,plain,
( sQ76_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f977,f825,f836,f839,f978]) ).
fof(f982,plain,
( bounded_relstr(sK23_skl)
| empty_carrier(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f163,f450]) ).
fof(f986,plain,
( bounded_relstr(sK10_skl)
| empty_carrier(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f163,f357]) ).
fof(f987,definition,
( sQ77_spl
<=> bounded_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f990,plain,
( sQ77_spl
| sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f982,f934,f937,f987]) ).
fof(f991,definition,
( sQ78_spl
<=> bounded_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f995,definition,
( sQ79_spl
<=> bounded_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f999,definition,
( sQ80_spl
<=> bounded_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( sQ34_spl
| sQ10_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f986,f603,f614,f746]) ).
fof(f1004,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK29_skl) ),
inference(resolution,[status(thm)],[f971,f193]) ).
fof(f1005,plain,
( sK29_skl = rel_str_of(the_carrier(sK29_skl),the_InternalRel(sK29_skl))
| ~ rel_str(sK29_skl) ),
inference(resolution,[status(thm)],[f478,f104]) ).
fof(f1006,definition,
( sQ81_spl
<=> rel_str(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1008,plain,
( sQ81_spl
| ~ rel_str(sK29_skl) ),
inference(component_clause,[status(thm)],[f1006]) ).
fof(f1009,definition,
( sQ82_spl
<=> sK29_skl = rel_str_of(the_carrier(sK29_skl),the_InternalRel(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( sQ82_spl
| ~ sQ81_spl ),
inference(split_clause,[status(thm)],[f1005,f1006,f1009]) ).
fof(f1013,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1008,f476]) ).
fof(f1014,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f1013]) ).
fof(f1015,plain,
( lower_bounded_relstr(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f165,f453]) ).
fof(f1017,plain,
( lower_bounded_relstr(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f165,f360]) ).
fof(f1018,definition,
( sQ83_spl
<=> lower_bounded_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
( sQ83_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1015,f934,f1018]) ).
fof(f1023,plain,
( sQ14_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1017,f603,f634]) ).
fof(f1025,plain,
( ~ sQ30_spl
| lower_bounded_relstr(sK12_skl)
| ~ reflexive_relstr(sK12_skl)
| empty_carrier(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f721,f115]) ).
fof(f1030,definition,
( sQ85_spl
<=> lower_bounded_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1033,plain,
( ~ sQ30_spl
| sQ85_spl
| ~ sQ29_spl
| sQ28_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1025,f703,f714,f717,f1030,f720]) ).
fof(f1034,plain,
! [X0] :
( finite(X0)
| ~ element(X0,powerset(sK13_skl)) ),
inference(resolution,[status(thm)],[f759,f152]) ).
fof(f1036,plain,
( upper_bounded_relstr(sK23_skl)
| ~ rel_str(sK23_skl) ),
inference(resolution,[status(thm)],[f166,f453]) ).
fof(f1037,plain,
( upper_bounded_relstr(sK16_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f166,f396]) ).
fof(f1038,plain,
( upper_bounded_relstr(sK10_skl)
| ~ rel_str(sK10_skl) ),
inference(resolution,[status(thm)],[f166,f360]) ).
fof(f1039,definition,
( sQ86_spl
<=> upper_bounded_relstr(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( sQ86_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1036,f934,f1039]) ).
fof(f1043,plain,
( sQ45_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1037,f736,f801]) ).
fof(f1044,plain,
( sQ25_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1038,f603,f698]) ).
fof(f1045,plain,
( connected_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f170,f414]) ).
fof(f1046,definition,
( sQ87_spl
<=> connected_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( sQ87_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1045,f825,f836,f839,f1046]) ).
fof(f1061,plain,
( ~ sQ52_spl
| lower_bounded_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| empty_carrier(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f843,f115]) ).
fof(f1063,definition,
( sQ88_spl
<=> lower_bounded_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1066,plain,
( ~ sQ52_spl
| sQ88_spl
| ~ sQ51_spl
| sQ50_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1061,f825,f836,f839,f1063,f842]) ).
fof(f1068,plain,
( ~ sQ64_spl
| lower_bounded_relstr(sK18_skl)
| ~ reflexive_relstr(sK18_skl)
| empty_carrier(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f912,f115]) ).
fof(f1073,definition,
( sQ90_spl
<=> lower_bounded_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1076,plain,
( ~ sQ64_spl
| sQ90_spl
| ~ sQ63_spl
| sQ60_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1068,f856,f897,f908,f1073,f911]) ).
fof(f1083,definition,
( sQ91_spl
<=> upper_bounded_relstr(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1084,plain,
( ~ sQ91_spl
| upper_bounded_relstr(sK12_skl) ),
inference(component_clause,[status(thm)],[f1083]) ).
fof(f1090,definition,
( sQ92_spl
<=> upper_bounded_relstr(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1091,plain,
( ~ sQ92_spl
| upper_bounded_relstr(sK17_skl) ),
inference(component_clause,[status(thm)],[f1090]) ).
fof(f1097,definition,
( sQ93_spl
<=> upper_bounded_relstr(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
( ~ sQ93_spl
| upper_bounded_relstr(sK18_skl) ),
inference(component_clause,[status(thm)],[f1097]) ).
fof(f1103,plain,
( bounded_relstr(sK16_skl)
| ~ lower_bounded_relstr(sK16_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f172,f395]) ).
fof(f1106,plain,
( sQ44_spl
| ~ sQ42_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1103,f736,f791,f797]) ).
fof(f1109,plain,
( ~ sQ65_spl
| upper_bounded_relstr(sK18_skl)
| ~ with_suprema_relstr(sK18_skl)
| ~ reflexive_relstr(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f177,f916]) ).
fof(f1110,plain,
( ~ sQ53_spl
| upper_bounded_relstr(sK17_skl)
| ~ with_suprema_relstr(sK17_skl)
| ~ reflexive_relstr(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f177,f847]) ).
fof(f1111,plain,
( ~ sQ31_spl
| upper_bounded_relstr(sK12_skl)
| ~ with_suprema_relstr(sK12_skl)
| ~ reflexive_relstr(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f177,f725]) ).
fof(f1114,plain,
( ~ sQ65_spl
| sQ93_spl
| ~ sQ62_spl
| ~ sQ63_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1109,f856,f908,f904,f1097,f915]) ).
fof(f1115,plain,
( ~ sQ53_spl
| sQ92_spl
| ~ sQ56_spl
| ~ sQ51_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1110,f825,f839,f869,f1090,f846]) ).
fof(f1116,plain,
( ~ sQ31_spl
| sQ91_spl
| ~ sQ57_spl
| ~ sQ29_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1111,f703,f717,f873,f1083,f724]) ).
fof(f1118,plain,
( ~ sQ91_spl
| bounded_relstr(sK12_skl)
| ~ lower_bounded_relstr(sK12_skl)
| ~ rel_str(sK12_skl) ),
inference(resolution,[status(thm)],[f1084,f172]) ).
fof(f1120,plain,
( ~ sQ91_spl
| sQ80_spl
| ~ sQ85_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1118,f703,f1030,f999,f1083]) ).
fof(f1122,plain,
( ~ sQ92_spl
| bounded_relstr(sK17_skl)
| ~ lower_bounded_relstr(sK17_skl)
| ~ rel_str(sK17_skl) ),
inference(resolution,[status(thm)],[f1091,f172]) ).
fof(f1124,plain,
( ~ sQ92_spl
| sQ79_spl
| ~ sQ88_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f1122,f825,f1063,f995,f1090]) ).
fof(f1126,plain,
( ~ sQ93_spl
| bounded_relstr(sK18_skl)
| ~ lower_bounded_relstr(sK18_skl)
| ~ rel_str(sK18_skl) ),
inference(resolution,[status(thm)],[f1098,f172]) ).
fof(f1128,plain,
( ~ sQ93_spl
| sQ78_spl
| ~ sQ90_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1126,f856,f1073,f991,f1097]) ).
fof(f1147,plain,
! [X0] : one_sorted_str(boole_POSet(X0)),
inference(resolution,[status(thm)],[f189,f191]) ).
fof(f1148,plain,
( sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f685,f1147]) ).
fof(f1150,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1148]) ).
fof(f1153,definition,
( sQ94_spl
<=> rel_str(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1155,plain,
( sQ94_spl
| ~ rel_str(boole_POSet(cast_as_carrier_subset(sK34_skl))) ),
inference(component_clause,[status(thm)],[f1153]) ).
fof(f1164,plain,
( sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1155,f189]) ).
fof(f1165,plain,
sQ94_spl,
inference(contradiction_clause,[status(thm)],[f1164]) ).
fof(f1166,plain,
( ~ sQ23_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f681,f224]) ).
fof(f1167,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1166]) ).
fof(f1185,plain,
net_str(sK2_skl(sK29_skl),sK29_skl),
inference(resolution,[status(thm)],[f204,f971]) ).
fof(f1186,plain,
net_str(sK2_skl(sK26_skl),sK26_skl),
inference(resolution,[status(thm)],[f204,f463]) ).
fof(f1187,plain,
net_str(sK2_skl(sK23_skl),sK23_skl),
inference(resolution,[status(thm)],[f204,f923]) ).
fof(f1188,plain,
net_str(sK2_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f204,f854]) ).
fof(f1189,plain,
net_str(sK2_skl(sK17_skl),sK17_skl),
inference(resolution,[status(thm)],[f204,f823]) ).
fof(f1190,plain,
net_str(sK2_skl(sK16_skl),sK16_skl),
inference(resolution,[status(thm)],[f204,f734]) ).
fof(f1191,plain,
net_str(sK2_skl(sK12_skl),sK12_skl),
inference(resolution,[status(thm)],[f204,f632]) ).
fof(f1192,plain,
net_str(sK2_skl(sK10_skl),sK10_skl),
inference(resolution,[status(thm)],[f204,f581]) ).
fof(f1193,plain,
net_str(sK2_skl(sK9_skl),sK9_skl),
inference(resolution,[status(thm)],[f204,f580]) ).
fof(f1194,plain,
net_str(sK2_skl(sK0_skl),sK0_skl),
inference(resolution,[status(thm)],[f204,f577]) ).
fof(f1195,plain,
net_str(sK2_skl(sK1_skl),sK1_skl),
inference(resolution,[status(thm)],[f204,f201]) ).
fof(f1196,plain,
net_str(sK2_skl(sK35_skl),sK35_skl),
inference(resolution,[status(thm)],[f204,f561]) ).
fof(f1197,plain,
net_str(sK2_skl(sK34_skl),sK34_skl),
inference(resolution,[status(thm)],[f204,f512]) ).
fof(f1198,plain,
rel_str(sK2_skl(sK29_skl)),
inference(resolution,[status(thm)],[f1185,f1004]) ).
fof(f1204,definition,
( sQ98_spl
<=> empty_carrier(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
( ~ sQ98_spl
| empty_carrier(sK29_skl) ),
inference(component_clause,[status(thm)],[f1204]) ).
fof(f1207,definition,
( sQ99_spl
<=> one_sorted_str(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1209,plain,
( sQ99_spl
| ~ one_sorted_str(sK29_skl) ),
inference(component_clause,[status(thm)],[f1207]) ).
fof(f1221,definition,
( sQ102_spl
<=> rel_str(sK2_skl(sK29_skl)) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
( sQ102_spl
| ~ rel_str(sK2_skl(sK29_skl)) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1232,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f1198]) ).
fof(f1233,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f1232]) ).
fof(f1234,plain,
( sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1209,f971]) ).
fof(f1235,plain,
sQ99_spl,
inference(contradiction_clause,[status(thm)],[f1234]) ).
fof(f1236,plain,
( ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1205,f477]) ).
fof(f1237,plain,
~ sQ98_spl,
inference(contradiction_clause,[status(thm)],[f1236]) ).
fof(f1240,plain,
rel_str(sK2_skl(sK23_skl)),
inference(resolution,[status(thm)],[f1187,f924]) ).
fof(f1246,definition,
( sQ106_spl
<=> one_sorted_str(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( sQ106_spl
| ~ one_sorted_str(sK23_skl) ),
inference(component_clause,[status(thm)],[f1246]) ).
fof(f1260,definition,
( sQ109_spl
<=> rel_str(sK2_skl(sK23_skl)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
( sQ109_spl
| ~ rel_str(sK2_skl(sK23_skl)) ),
inference(component_clause,[status(thm)],[f1260]) ).
fof(f1271,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1262,f1240]) ).
fof(f1272,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f1271]) ).
fof(f1273,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1248,f923]) ).
fof(f1274,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1273]) ).
fof(f1277,plain,
rel_str(sK2_skl(sK34_skl)),
inference(resolution,[status(thm)],[f1197,f559]) ).
fof(f1304,plain,
! [X0] : ~ in(X0,sK4_skl(powerset(sK13_skl))),
inference(resolution,[status(thm)],[f208,f732]) ).
fof(f1306,plain,
! [X0] :
( in(sK4_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f208,f521]) ).
fof(f1308,plain,
one_sorted_str(sK2_skl(sK34_skl)),
inference(resolution,[status(thm)],[f1277,f191]) ).
fof(f1311,definition,
( sQ115_spl
<=> rel_str(sK2_skl(sK34_skl)) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1313,plain,
( sQ115_spl
| ~ rel_str(sK2_skl(sK34_skl)) ),
inference(component_clause,[status(thm)],[f1311]) ).
fof(f1322,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1313,f1277]) ).
fof(f1323,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f1322]) ).
fof(f1324,plain,
net_str(sK2_skl(sK2_skl(sK34_skl)),sK2_skl(sK34_skl)),
inference(resolution,[status(thm)],[f1308,f204]) ).
fof(f1325,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK2_skl(sK34_skl)) ),
inference(resolution,[status(thm)],[f1308,f193]) ).
fof(f1331,plain,
rel_str(sK2_skl(sK18_skl)),
inference(resolution,[status(thm)],[f1188,f891]) ).
fof(f1337,definition,
( sQ119_spl
<=> one_sorted_str(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( sQ119_spl
| ~ one_sorted_str(sK18_skl) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1351,definition,
( sQ122_spl
<=> rel_str(sK2_skl(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1353,plain,
( sQ122_spl
| ~ rel_str(sK2_skl(sK18_skl)) ),
inference(component_clause,[status(thm)],[f1351]) ).
fof(f1362,plain,
( sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1353,f1331]) ).
fof(f1363,plain,
sQ122_spl,
inference(contradiction_clause,[status(thm)],[f1362]) ).
fof(f1364,plain,
( sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1339,f854]) ).
fof(f1365,plain,
sQ119_spl,
inference(contradiction_clause,[status(thm)],[f1364]) ).
fof(f1370,plain,
! [X0] :
( ~ in(X0,sK4_skl(powerset(sK13_skl)))
| empty(powerset(sK13_skl)) ),
inference(resolution,[status(thm)],[f1306,f758]) ).
fof(f1371,plain,
! [X0] :
( ~ in(X0,sK4_skl(powerset(empty_set)))
| empty(powerset(empty_set)) ),
inference(resolution,[status(thm)],[f1306,f589]) ).
fof(f1373,plain,
! [X0,X1] :
( element(sK4_skl(X0),X1)
| ~ element(X0,powerset(X1))
| empty(X0) ),
inference(resolution,[status(thm)],[f1306,f533]) ).
fof(f1374,plain,
! [X0] :
( ~ in(X0,sK4_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f1306,f106]) ).
fof(f1376,definition,
( sQ125_spl
<=> empty(powerset(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( ~ sQ125_spl
| empty(powerset(sK13_skl)) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1379,definition,
! [X0] :
( sQ126_spl
<=> ~ in(X0,sK4_skl(powerset(sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1382,plain,
( sQ126_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1370,f1376,f1379]) ).
fof(f1383,definition,
( sQ127_spl
<=> empty(powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( ~ sQ127_spl
| empty(powerset(empty_set)) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1386,definition,
! [X0] :
( sQ128_spl
<=> ~ in(X0,sK4_skl(powerset(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1389,plain,
( sQ128_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f1371,f1383,f1386]) ).
fof(f1390,plain,
( ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1384,f222]) ).
fof(f1391,plain,
~ sQ127_spl,
inference(contradiction_clause,[status(thm)],[f1390]) ).
fof(f1392,plain,
( ~ sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1377,f222]) ).
fof(f1393,plain,
~ sQ125_spl,
inference(contradiction_clause,[status(thm)],[f1392]) ).
fof(f1394,plain,
rel_str(sK2_skl(sK17_skl)),
inference(resolution,[status(thm)],[f1189,f890]) ).
fof(f1400,definition,
( sQ130_spl
<=> one_sorted_str(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ130_spl
| ~ one_sorted_str(sK17_skl) ),
inference(component_clause,[status(thm)],[f1400]) ).
fof(f1412,plain,
rel_str(sK2_skl(sK35_skl)),
inference(resolution,[status(thm)],[f1196,f562]) ).
fof(f1418,definition,
( sQ134_spl
<=> one_sorted_str(sK35_skl) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1420,plain,
( sQ134_spl
| ~ one_sorted_str(sK35_skl) ),
inference(component_clause,[status(thm)],[f1418]) ).
fof(f1429,plain,
( sQ134_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1420,f561]) ).
fof(f1430,plain,
sQ134_spl,
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1431,plain,
one_sorted_str(sK2_skl(sK35_skl)),
inference(resolution,[status(thm)],[f1412,f191]) ).
fof(f1434,definition,
( sQ137_spl
<=> rel_str(sK2_skl(sK35_skl)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( sQ137_spl
| ~ rel_str(sK2_skl(sK35_skl)) ),
inference(component_clause,[status(thm)],[f1434]) ).
fof(f1445,plain,
( sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1436,f1412]) ).
fof(f1446,plain,
sQ137_spl,
inference(contradiction_clause,[status(thm)],[f1445]) ).
fof(f1447,plain,
net_str(sK2_skl(sK2_skl(sK35_skl)),sK2_skl(sK35_skl)),
inference(resolution,[status(thm)],[f1431,f204]) ).
fof(f1448,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK2_skl(sK35_skl)) ),
inference(resolution,[status(thm)],[f1431,f193]) ).
fof(f1452,definition,
( sQ140_spl
<=> rel_str(sK2_skl(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1454,plain,
( sQ140_spl
| ~ rel_str(sK2_skl(sK17_skl)) ),
inference(component_clause,[status(thm)],[f1452]) ).
fof(f1463,plain,
( sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1454,f1394]) ).
fof(f1464,plain,
sQ140_spl,
inference(contradiction_clause,[status(thm)],[f1463]) ).
fof(f1465,plain,
( sQ130_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1402,f823]) ).
fof(f1466,plain,
sQ130_spl,
inference(contradiction_clause,[status(thm)],[f1465]) ).
fof(f1469,plain,
rel_str(sK2_skl(sK16_skl)),
inference(resolution,[status(thm)],[f1190,f757]) ).
fof(f1475,definition,
( sQ144_spl
<=> one_sorted_str(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1477,plain,
( sQ144_spl
| ~ one_sorted_str(sK16_skl) ),
inference(component_clause,[status(thm)],[f1475]) ).
fof(f1489,definition,
( sQ147_spl
<=> rel_str(sK2_skl(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
( sQ147_spl
| ~ rel_str(sK2_skl(sK16_skl)) ),
inference(component_clause,[status(thm)],[f1489]) ).
fof(f1500,plain,
( sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1491,f1469]) ).
fof(f1501,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f1500]) ).
fof(f1502,plain,
( sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1477,f734]) ).
fof(f1503,plain,
sQ144_spl,
inference(contradiction_clause,[status(thm)],[f1502]) ).
fof(f1506,plain,
rel_str(sK2_skl(sK12_skl)),
inference(resolution,[status(thm)],[f1191,f689]) ).
fof(f1512,definition,
( sQ151_spl
<=> one_sorted_str(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1514,plain,
( sQ151_spl
| ~ one_sorted_str(sK12_skl) ),
inference(component_clause,[status(thm)],[f1512]) ).
fof(f1523,plain,
rel_str(sK2_skl(sK10_skl)),
inference(resolution,[status(thm)],[f1192,f584]) ).
fof(f1529,definition,
( sQ155_spl
<=> one_sorted_str(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1531,plain,
( sQ155_spl
| ~ one_sorted_str(sK10_skl) ),
inference(component_clause,[status(thm)],[f1529]) ).
fof(f1540,plain,
( sQ155_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1531,f581]) ).
fof(f1541,plain,
sQ155_spl,
inference(contradiction_clause,[status(thm)],[f1540]) ).
fof(f1549,plain,
sK13_skl = empty_set,
inference(resolution,[status(thm)],[f538,f375]) ).
fof(f1551,plain,
! [X0] :
( X0 = sK13_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f1549,f538]) ).
fof(f1563,plain,
rel_str(sK2_skl(sK2_skl(sK34_skl))),
inference(resolution,[status(thm)],[f1324,f1325]) ).
fof(f1569,definition,
( sQ159_spl
<=> one_sorted_str(sK2_skl(sK34_skl)) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1571,plain,
( sQ159_spl
| ~ one_sorted_str(sK2_skl(sK34_skl)) ),
inference(component_clause,[status(thm)],[f1569]) ).
fof(f1580,plain,
( sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1571,f1308]) ).
fof(f1581,plain,
sQ159_spl,
inference(contradiction_clause,[status(thm)],[f1580]) ).
fof(f1586,plain,
one_sorted_str(sK2_skl(sK2_skl(sK34_skl))),
inference(resolution,[status(thm)],[f1563,f191]) ).
fof(f1592,definition,
( sQ162_spl
<=> rel_str(sK2_skl(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f1594,plain,
( sQ162_spl
| ~ rel_str(sK2_skl(sK12_skl)) ),
inference(component_clause,[status(thm)],[f1592]) ).
fof(f1603,plain,
( sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1594,f1506]) ).
fof(f1604,plain,
sQ162_spl,
inference(contradiction_clause,[status(thm)],[f1603]) ).
fof(f1605,plain,
( sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1514,f632]) ).
fof(f1606,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f1605]) ).
fof(f1610,definition,
( sQ165_spl
<=> rel_str(sK2_skl(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1612,plain,
( sQ165_spl
| ~ rel_str(sK2_skl(sK10_skl)) ),
inference(component_clause,[status(thm)],[f1610]) ).
fof(f1621,plain,
( sQ165_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1612,f1523]) ).
fof(f1622,plain,
sQ165_spl,
inference(contradiction_clause,[status(thm)],[f1621]) ).
fof(f1629,plain,
rel_str(sK2_skl(sK9_skl)),
inference(resolution,[status(thm)],[f1193,f583]) ).
fof(f1635,definition,
( sQ169_spl
<=> empty_carrier(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1636,plain,
( ~ sQ169_spl
| empty_carrier(sK9_skl) ),
inference(component_clause,[status(thm)],[f1635]) ).
fof(f1638,definition,
( sQ170_spl
<=> one_sorted_str(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1640,plain,
( sQ170_spl
| ~ one_sorted_str(sK9_skl) ),
inference(component_clause,[status(thm)],[f1638]) ).
fof(f1653,definition,
( sQ173_spl
<=> rel_str(sK2_skl(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1655,plain,
( sQ173_spl
| ~ rel_str(sK2_skl(sK9_skl)) ),
inference(component_clause,[status(thm)],[f1653]) ).
fof(f1664,plain,
( sQ173_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1655,f1629]) ).
fof(f1665,plain,
sQ173_spl,
inference(contradiction_clause,[status(thm)],[f1664]) ).
fof(f1666,plain,
( sQ170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1640,f580]) ).
fof(f1667,plain,
sQ170_spl,
inference(contradiction_clause,[status(thm)],[f1666]) ).
fof(f1668,plain,
( ~ sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1636,f343]) ).
fof(f1669,plain,
~ sQ169_spl,
inference(contradiction_clause,[status(thm)],[f1668]) ).
fof(f1672,plain,
net_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl))),sK2_skl(sK2_skl(sK34_skl))),
inference(resolution,[status(thm)],[f1586,f204]) ).
fof(f1673,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK2_skl(sK2_skl(sK34_skl))) ),
inference(resolution,[status(thm)],[f1586,f193]) ).
fof(f1674,plain,
rel_str(sK2_skl(sK2_skl(sK35_skl))),
inference(resolution,[status(thm)],[f1447,f1448]) ).
fof(f1680,definition,
( sQ177_spl
<=> one_sorted_str(sK2_skl(sK35_skl)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f1682,plain,
( sQ177_spl
| ~ one_sorted_str(sK2_skl(sK35_skl)) ),
inference(component_clause,[status(thm)],[f1680]) ).
fof(f1695,plain,
one_sorted_str(sK2_skl(sK2_skl(sK35_skl))),
inference(resolution,[status(thm)],[f1674,f191]) ).
fof(f1696,plain,
net_str(sK2_skl(sK2_skl(sK2_skl(sK35_skl))),sK2_skl(sK2_skl(sK35_skl))),
inference(resolution,[status(thm)],[f1695,f204]) ).
fof(f1697,plain,
! [X0] :
( rel_str(X0)
| ~ net_str(X0,sK2_skl(sK2_skl(sK35_skl))) ),
inference(resolution,[status(thm)],[f1695,f193]) ).
fof(f1703,definition,
( sQ181_spl
<=> one_sorted_str(sK2_skl(sK2_skl(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f1705,plain,
( sQ181_spl
| ~ one_sorted_str(sK2_skl(sK2_skl(sK34_skl))) ),
inference(component_clause,[status(thm)],[f1703]) ).
fof(f1714,plain,
rel_str(sK2_skl(sK0_skl)),
inference(resolution,[status(thm)],[f1194,f582]) ).
fof(f1723,definition,
( sQ186_spl
<=> one_sorted_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1725,plain,
( sQ186_spl
| ~ one_sorted_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f1723]) ).
fof(f1737,definition,
( sQ189_spl
<=> rel_str(sK2_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1739,plain,
( sQ189_spl
| ~ rel_str(sK2_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1737]) ).
fof(f1748,plain,
( sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1739,f1714]) ).
fof(f1749,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f1748]) ).
fof(f1750,plain,
( sQ186_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1725,f577]) ).
fof(f1751,plain,
sQ186_spl,
inference(contradiction_clause,[status(thm)],[f1750]) ).
fof(f1754,definition,
( sQ192_spl
<=> rel_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1756,plain,
( sQ192_spl
| ~ rel_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f1754]) ).
fof(f1765,plain,
( sQ192_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1756,f199]) ).
fof(f1766,plain,
sQ192_spl,
inference(contradiction_clause,[status(thm)],[f1765]) ).
fof(f1767,plain,
( sQ181_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1705,f1586]) ).
fof(f1768,plain,
sQ181_spl,
inference(contradiction_clause,[status(thm)],[f1767]) ).
fof(f1769,plain,
( sQ177_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1682,f1431]) ).
fof(f1770,plain,
sQ177_spl,
inference(contradiction_clause,[status(thm)],[f1769]) ).
fof(f1775,definition,
( sQ195_spl
<=> rel_str(sK2_skl(sK2_skl(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1777,plain,
( sQ195_spl
| ~ rel_str(sK2_skl(sK2_skl(sK34_skl))) ),
inference(component_clause,[status(thm)],[f1775]) ).
fof(f1786,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1777,f1563]) ).
fof(f1787,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f1786]) ).
fof(f1788,plain,
empty(sK4_skl(powerset(sK13_skl))),
inference(resolution,[status(thm)],[f1304,f1306]) ).
fof(f1802,definition,
( sQ198_spl
<=> rel_str(sK2_skl(sK2_skl(sK35_skl))) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1804,plain,
( sQ198_spl
| ~ rel_str(sK2_skl(sK2_skl(sK35_skl))) ),
inference(component_clause,[status(thm)],[f1802]) ).
fof(f1813,plain,
( sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1804,f1674]) ).
fof(f1814,plain,
sQ198_spl,
inference(contradiction_clause,[status(thm)],[f1813]) ).
fof(f1815,plain,
rel_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl)))),
inference(resolution,[status(thm)],[f1673,f1672]) ).
fof(f1816,plain,
sK4_skl(powerset(sK13_skl)) = sK13_skl,
inference(resolution,[status(thm)],[f1788,f1551]) ).
fof(f1823,plain,
( in(sK13_skl,powerset(sK13_skl))
| empty(powerset(sK13_skl)) ),
inference(paramodulation,[status(thm)],[f1816,f1306]) ).
fof(f1825,definition,
( sQ201_spl
<=> in(sK13_skl,powerset(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
( sQ201_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1823,f1376,f1825]) ).
fof(f1831,plain,
( ~ in(powerset(sK13_skl),sK13_skl)
| empty(powerset(sK13_skl)) ),
inference(paramodulation,[status(thm)],[f1816,f1374]) ).
fof(f1832,definition,
( sQ202_spl
<=> in(powerset(sK13_skl),sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1835,plain,
( ~ sQ202_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1831,f1376,f1832]) ).
fof(f1842,plain,
! [X0] :
( element(sK13_skl,X0)
| ~ element(powerset(sK13_skl),powerset(X0))
| empty(powerset(sK13_skl)) ),
inference(paramodulation,[status(thm)],[f1816,f1373]) ).
fof(f1843,definition,
! [X0] :
( sQ203_spl
<=> ( element(sK13_skl,X0)
| ~ element(powerset(sK13_skl),powerset(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f1846,plain,
( sQ203_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1842,f1376,f1843]) ).
fof(f1850,plain,
rel_str(sK2_skl(sK26_skl)),
inference(resolution,[status(thm)],[f1186,f970]) ).
fof(f1856,definition,
( sQ205_spl
<=> empty_carrier(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1857,plain,
( ~ sQ205_spl
| empty_carrier(sK26_skl) ),
inference(component_clause,[status(thm)],[f1856]) ).
fof(f1859,definition,
( sQ206_spl
<=> one_sorted_str(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f1861,plain,
( sQ206_spl
| ~ one_sorted_str(sK26_skl) ),
inference(component_clause,[status(thm)],[f1859]) ).
fof(f1870,plain,
( sQ206_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1861,f463]) ).
fof(f1871,plain,
sQ206_spl,
inference(contradiction_clause,[status(thm)],[f1870]) ).
fof(f1872,plain,
( ~ sQ205_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1857,f464]) ).
fof(f1873,plain,
~ sQ205_spl,
inference(contradiction_clause,[status(thm)],[f1872]) ).
fof(f1877,definition,
( sQ209_spl
<=> rel_str(sK2_skl(sK26_skl)) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( sQ209_spl
| ~ rel_str(sK2_skl(sK26_skl)) ),
inference(component_clause,[status(thm)],[f1877]) ).
fof(f1888,plain,
( sQ209_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1879,f1850]) ).
fof(f1889,plain,
sQ209_spl,
inference(contradiction_clause,[status(thm)],[f1888]) ).
fof(f1892,plain,
rel_str(sK2_skl(sK1_skl)),
inference(resolution,[status(thm)],[f1195,f578]) ).
fof(f1901,definition,
( sQ214_spl
<=> one_sorted_str(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f1903,plain,
( sQ214_spl
| ~ one_sorted_str(sK1_skl) ),
inference(component_clause,[status(thm)],[f1901]) ).
fof(f1912,plain,
( sQ214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1903,f201]) ).
fof(f1913,plain,
sQ214_spl,
inference(contradiction_clause,[status(thm)],[f1912]) ).
fof(f1929,definition,
( sQ220_spl
<=> rel_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
( sQ220_spl
| ~ rel_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl)))) ),
inference(component_clause,[status(thm)],[f1929]) ).
fof(f1941,plain,
( sQ220_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1931,f1815]) ).
fof(f1942,plain,
sQ220_spl,
inference(contradiction_clause,[status(thm)],[f1941]) ).
fof(f1948,definition,
( sQ223_spl
<=> rel_str(sK2_skl(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f1950,plain,
( sQ223_spl
| ~ rel_str(sK2_skl(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1948]) ).
fof(f1959,plain,
( sQ223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1950,f1892]) ).
fof(f1960,plain,
sQ223_spl,
inference(contradiction_clause,[status(thm)],[f1959]) ).
fof(f1981,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| subset(filter_of_net_str(X0,X1),the_carrier(boole_POSet(cast_as_carrier_subset(X0)))) ),
inference(resolution,[status(thm)],[f529,f186]) ).
fof(f1989,plain,
rel_str(sK2_skl(sK2_skl(sK2_skl(sK35_skl)))),
inference(resolution,[status(thm)],[f1696,f1697]) ).
fof(f1995,definition,
( sQ227_spl
<=> one_sorted_str(sK2_skl(sK2_skl(sK35_skl))) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f1997,plain,
( sQ227_spl
| ~ one_sorted_str(sK2_skl(sK2_skl(sK35_skl))) ),
inference(component_clause,[status(thm)],[f1995]) ).
fof(f2006,plain,
( sQ227_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1997,f1695]) ).
fof(f2007,plain,
sQ227_spl,
inference(contradiction_clause,[status(thm)],[f2006]) ).
fof(f2019,definition,
( sQ230_spl
<=> rel_str(sK2_skl(sK2_skl(sK2_skl(sK35_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2021,plain,
( sQ230_spl
| ~ rel_str(sK2_skl(sK2_skl(sK2_skl(sK35_skl)))) ),
inference(component_clause,[status(thm)],[f2019]) ).
fof(f2030,plain,
( sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2021,f1989]) ).
fof(f2031,plain,
sQ230_spl,
inference(contradiction_clause,[status(thm)],[f2030]) ).
fof(f2065,plain,
! [X0] :
( ~ in(X0,powerset(sK11_skl))
| finite(X0) ),
inference(resolution,[status(thm)],[f892,f519]) ).
fof(f2071,plain,
! [X0] :
( ~ in(X0,powerset(sK13_skl))
| finite(X0) ),
inference(resolution,[status(thm)],[f1034,f519]) ).
fof(f2075,definition,
( sQ233_spl
<=> empty(filter_of_net_str(sK34_skl,sK35_skl)) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2076,plain,
( ~ sQ233_spl
| empty(filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(component_clause,[status(thm)],[f2075]) ).
fof(f2082,plain,
! [X0] :
( ~ sQ6_spl
| X0 = sK6_skl(X0,sK35_skl,sK34_skl)
| ~ in(X0,filter_of_net_str(sK34_skl,sK35_skl))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(paramodulation,[status(thm)],[f574,f321]) ).
fof(f2083,definition,
( sQ234_spl
<=> net_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl))),sK2_skl(sK2_skl(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
( sQ234_spl
| ~ net_str(sK2_skl(sK2_skl(sK2_skl(sK34_skl))),sK2_skl(sK2_skl(sK34_skl))) ),
inference(component_clause,[status(thm)],[f2083]) ).
fof(f2090,definition,
( sQ236_spl
<=> net_str(sK2_skl(sK26_skl),sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f2092,plain,
( sQ236_spl
| ~ net_str(sK2_skl(sK26_skl),sK26_skl) ),
inference(component_clause,[status(thm)],[f2090]) ).
fof(f2097,definition,
! [X0] :
( sQ238_spl
<=> ( X0 = sK6_skl(X0,sK35_skl,sK34_skl)
| ~ in(X0,filter_of_net_str(sK34_skl,sK35_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f2098,plain,
! [X0] :
( ~ sQ238_spl
| X0 = sK6_skl(X0,sK35_skl,sK34_skl)
| ~ in(X0,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(component_clause,[status(thm)],[f2097]) ).
fof(f2100,plain,
( ~ sQ6_spl
| sQ238_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2082,f564,f567,f570,f663,f2097,f573]) ).
fof(f2101,plain,
( sQ236_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f1186]) ).
fof(f2102,plain,
sQ236_spl,
inference(contradiction_clause,[status(thm)],[f2101]) ).
fof(f2103,plain,
( sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2085,f1672]) ).
fof(f2104,plain,
sQ234_spl,
inference(contradiction_clause,[status(thm)],[f2103]) ).
fof(f2105,plain,
! [X0,X1,X2] :
( ~ element(sK6_skl(X2,X1,X0),powerset(the_carrier(X0)))
| in(sK6_skl(X2,X1,X0),a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(resolution,[status(thm)],[f322,f557]) ).
fof(f2106,plain,
! [X0,X1,X2] :
( ~ element(sK6_skl(X2,X1,X0),powerset(the_carrier(X0)))
| in(sK6_skl(X2,X1,X0),a_2_1_yellow19(X0,X1))
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2105]) ).
fof(f2107,plain,
! [X0,X1,X2] :
( in(sK6_skl(X2,X1,X0),a_2_1_yellow19(X0,X1))
| ~ in(X2,a_2_1_yellow19(X0,X1))
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2106,f320]) ).
fof(f2115,plain,
( ~ sQ238_spl
| empty(filter_of_net_str(sK34_skl,sK35_skl))
| sK4_skl(filter_of_net_str(sK34_skl,sK35_skl)) = sK6_skl(sK4_skl(filter_of_net_str(sK34_skl,sK35_skl)),sK35_skl,sK34_skl) ),
inference(resolution,[status(thm)],[f2098,f1306]) ).
fof(f2116,plain,
( ~ sQ0_spl
| ~ sQ238_spl
| sK36_skl = sK6_skl(sK36_skl,sK35_skl,sK34_skl) ),
inference(resolution,[status(thm)],[f2098,f546]) ).
fof(f2117,definition,
( sQ239_spl
<=> sK4_skl(filter_of_net_str(sK34_skl,sK35_skl)) = sK6_skl(sK4_skl(filter_of_net_str(sK34_skl,sK35_skl)),sK35_skl,sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( ~ sQ238_spl
| sQ233_spl
| sQ239_spl ),
inference(split_clause,[status(thm)],[f2115,f2117,f2075,f2097]) ).
fof(f2122,plain,
( ~ sQ233_spl
| filter_of_net_str(sK34_skl,sK35_skl) = sK13_skl ),
inference(resolution,[status(thm)],[f2076,f1551]) ).
fof(f2127,plain,
( ~ sQ0_spl
| ~ sQ238_spl
| is_eventually_in(sK34_skl,sK35_skl,sK36_skl)
| ~ in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(paramodulation,[status(thm)],[f2116,f322]) ).
fof(f2129,plain,
( ~ sQ0_spl
| ~ sQ238_spl
| element(sK36_skl,powerset(the_carrier(sK34_skl)))
| ~ in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(paramodulation,[status(thm)],[f2116,f320]) ).
fof(f2130,definition,
( sQ240_spl
<=> in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl)) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f2131,plain,
( ~ sQ240_spl
| in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl)) ),
inference(component_clause,[status(thm)],[f2130]) ).
fof(f2132,plain,
( sQ240_spl
| ~ in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl)) ),
inference(component_clause,[status(thm)],[f2130]) ).
fof(f2133,plain,
( ~ sQ0_spl
| ~ sQ238_spl
| sQ1_spl
| ~ sQ240_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2127,f564,f567,f570,f663,f2130,f548,f2097,f545]) ).
fof(f2138,plain,
( ~ sQ0_spl
| ~ sQ238_spl
| sQ2_spl
| ~ sQ240_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2129,f564,f567,f570,f663,f2130,f552,f2097,f545]) ).
fof(f2139,plain,
( sQ240_spl
| ~ sQ6_spl
| ~ in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(forward_demodulation,[status(thm)],[f574,f2132]) ).
fof(f2152,plain,
( ~ sQ233_spl
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl)
| subset(sK13_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
inference(paramodulation,[status(thm)],[f2122,f1981]) ).
fof(f2153,plain,
( ~ sQ233_spl
| element(sK13_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(paramodulation,[status(thm)],[f2122,f186]) ).
fof(f2154,definition,
( sQ242_spl
<=> subset(sK13_skl,the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f2157,plain,
( ~ sQ233_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f2152,f2154,f564,f567,f570,f663,f2075]) ).
fof(f2158,definition,
( sQ243_spl
<=> element(sK13_skl,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f2161,plain,
( ~ sQ233_spl
| sQ243_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2153,f564,f567,f570,f663,f2158,f2075]) ).
fof(f2162,plain,
( ~ sQ1_spl
| ~ element(sK36_skl,powerset(the_carrier(sK34_skl)))
| in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(resolution,[status(thm)],[f549,f557]) ).
fof(f2163,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| sQ240_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2162,f564,f567,f570,f663,f2130,f552,f548]) ).
fof(f2165,plain,
( empty(powerset(sK11_skl))
| finite(sK4_skl(powerset(sK11_skl))) ),
inference(resolution,[status(thm)],[f2065,f1306]) ).
fof(f2167,definition,
( sQ244_spl
<=> finite(sK4_skl(powerset(sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2170,definition,
( sQ245_spl
<=> empty(powerset(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f2171,plain,
( ~ sQ245_spl
| empty(powerset(sK11_skl)) ),
inference(component_clause,[status(thm)],[f2170]) ).
fof(f2173,plain,
( sQ245_spl
| sQ244_spl ),
inference(split_clause,[status(thm)],[f2165,f2167,f2170]) ).
fof(f2174,plain,
( ~ sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2171,f222]) ).
fof(f2175,plain,
~ sQ245_spl,
inference(contradiction_clause,[status(thm)],[f2174]) ).
fof(f2177,plain,
( empty(powerset(sK13_skl))
| finite(sK4_skl(powerset(sK13_skl))) ),
inference(resolution,[status(thm)],[f2071,f1306]) ).
fof(f2179,definition,
( sQ246_spl
<=> finite(sK4_skl(powerset(sK13_skl))) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f2182,plain,
( sQ125_spl
| sQ246_spl ),
inference(split_clause,[status(thm)],[f2177,f2179,f1376]) ).
fof(f2190,definition,
( sQ247_spl
<=> empty(powerset(the_carrier(sK34_skl))) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f2191,plain,
( ~ sQ247_spl
| empty(powerset(the_carrier(sK34_skl))) ),
inference(component_clause,[status(thm)],[f2190]) ).
fof(f2194,plain,
( ~ sQ247_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2191,f222]) ).
fof(f2195,plain,
~ sQ247_spl,
inference(contradiction_clause,[status(thm)],[f2194]) ).
fof(f2209,plain,
( ~ sQ240_spl
| ~ sQ6_spl
| in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)) ),
inference(backward_demodulation,[status(thm)],[f574,f2131]) ).
fof(f2210,plain,
! [X0] :
( ~ sQ6_spl
| in(sK6_skl(X0,sK35_skl,sK34_skl),a_2_1_yellow19(sK34_skl,sK35_skl))
| ~ in(X0,filter_of_net_str(sK34_skl,sK35_skl))
| ~ net_str(sK35_skl,sK34_skl)
| empty_carrier(sK35_skl)
| ~ one_sorted_str(sK34_skl)
| empty_carrier(sK34_skl) ),
inference(paramodulation,[status(thm)],[f574,f2107]) ).
fof(f2212,plain,
( ~ sQ240_spl
| ~ sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2209,f545,f573,f2130]) ).
fof(f2213,definition,
! [X0] :
( sQ250_spl
<=> ( in(sK6_skl(X0,sK35_skl,sK34_skl),a_2_1_yellow19(sK34_skl,sK35_skl))
| ~ in(X0,filter_of_net_str(sK34_skl,sK35_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f2216,plain,
( ~ sQ6_spl
| sQ250_spl
| ~ sQ20_spl
| sQ5_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2210,f564,f567,f570,f663,f2213,f573]) ).
fof(f2219,plain,
( sQ240_spl
| ~ sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2139,f545,f573,f2130]) ).
fof(f2220,plain,
$false,
inference(sat_refutation,[status(thm)],[f551,f555,f556,f576,f595,f597,f599,f601,f609,f611,f623,f627,f629,f631,f653,f655,f657,f666,f674,f676,f686,f709,f711,f723,f727,f729,f731,f742,f744,f779,f781,f783,f814,f816,f831,f833,f845,f849,f851,f853,f862,f864,f872,f876,f877,f884,f888,f889,f903,f907,f914,f918,f920,f922,f929,f943,f947,f954,f958,f960,f962,f964,f976,f981,f990,f1003,f1012,f1014,f1021,f1023,f1033,f1042,f1043,f1044,f1049,f1066,f1076,f1106,f1114,f1115,f1116,f1120,f1124,f1128,f1150,f1165,f1167,f1233,f1235,f1237,f1272,f1274,f1323,f1363,f1365,f1382,f1389,f1391,f1393,f1430,f1446,f1464,f1466,f1501,f1503,f1541,f1581,f1604,f1606,f1622,f1665,f1667,f1669,f1749,f1751,f1766,f1768,f1770,f1787,f1814,f1828,f1835,f1846,f1871,f1873,f1889,f1913,f1942,f1960,f2007,f2031,f2100,f2102,f2104,f2120,f2133,f2138,f2157,f2161,f2163,f2173,f2175,f2182,f2195,f2212,f2216,f2219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/20.59 % CPULimit : 300
% 0.08/20.59 % WCLimit : 300
% 0.08/20.59 % DateTime : Mon Sep 21 06:19:03 UTC 2026
% 0.08/20.59 % CPUTime :
% 0.49/20.61 % Drodi V4.1.1
% 0.49/20.68 % Refutation found
% 0.49/20.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.49/20.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.49/20.74 % Elapsed time: 0.130218 seconds
% 0.49/20.74 % CPU time: 0.561566 seconds
% 0.49/20.74 % Total memory used: 99.283 MB
% 0.49/20.74 % Net memory used: 98.927 MB
%------------------------------------------------------------------------------