%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU391+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:22:30 PM UTC 2026
% Result : Theorem 0.14s 15.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/15.79 % Computer : n013.cluster.edu
% 0.09/15.79 % Model : x86_64 x86_64
% 0.09/15.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.79 % Memory : 8046.5625MB
% 0.09/15.79 % OS : Linux 6.8.0-71-generic
% 0.09/15.79 % CPULimit : 300
% 0.09/15.79 % WCLimit : 300
% 0.09/15.79 % DateTime : Mon Sep 21 06:18:14 UTC 2026
% 0.14/15.80 % CPUTime :
% 0.14/15.81 % Drodi V4.1.1
% 0.14/15.87 % Refutation found
% 0.14/15.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/15.87 % SZS output start CNFRefutation for theBenchmark
% 0.14/15.87 fof(f1,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( strict_rel_str(A)=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f3,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& reflexive_relstr(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& reflexive_relstr(A)& up_complete_relstr(A)& join_complete_relstr(A) ) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f9,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( with_suprema_relstr(A)=> ~ empty_carrier(A) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f12,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& with_suprema_relstr(A)& with_infima_relstr(A) ) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f13,axiom,(
% 0.14/15.87 (! [A] :( finite(A)=> (! [B] :( element(B,powerset(A))=> finite(B) ) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f14,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( with_infima_relstr(A)=> ~ empty_carrier(A) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f16,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( ( ~ empty_carrier(A)& complete_relstr(A) )=> ( ~ empty_carrier(A)& bounded_relstr(A) ) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f17,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( bounded_relstr(A)=> ( lower_bounded_relstr(A)& upper_bounded_relstr(A) ) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f20,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> ( ( reflexive_relstr(A)& with_suprema_relstr(A)& up_complete_relstr(A) )=> ( ~ empty_carrier(A)& reflexive_relstr(A)& with_suprema_relstr(A)& upper_bounded_relstr(A) ) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f21,axiom,(
% 0.14/15.87 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> filter_of_net_str(A,B) = a_2_1_yellow19(A,B) ) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f25,axiom,(
% 0.14/15.87 (! [A] :( one_sorted_str(A)=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f26,axiom,(
% 0.14/15.87 (! [A,B] :( ( ~ empty_carrier(A)& one_sorted_str(A)& ~ empty_carrier(B)& net_str(B,A) )=> element(filter_of_net_str(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f28,axiom,(
% 0.14/15.87 (! [A] :( strict_rel_str(boole_POSet(A))& rel_str(boole_POSet(A)) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f29,axiom,(
% 0.14/15.87 (! [A] :( rel_str(A)=> one_sorted_str(A) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f31,axiom,(
% 0.14/15.87 (! [A] :( one_sorted_str(A)=> (! [B] :( net_str(B,A)=> rel_str(B) ) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f37,axiom,(
% 0.14/15.87 (? [A] : rel_str(A) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f39,axiom,(
% 0.14/15.87 (! [A] :( one_sorted_str(A)=> (? [B] : net_str(B,A) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f41,axiom,(
% 0.14/15.87 (! [A] :(? [B] : element(B,A) ))),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f45,axiom,(
% 0.14/15.87 (! [A] :( ( ~ empty_carrier(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& lower_relstr_subset(cast_as_carrier_subset(A),A)& upper_relstr_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f47,axiom,(
% 0.14/15.87 (! [A] : ~ empty(powerset(A)) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f48,axiom,(
% 0.14/15.87 (! [A] :( ~ empty_carrier(boole_POSet(A))& strict_rel_str(boole_POSet(A))& reflexive_relstr(boole_POSet(A))& transitive_relstr(boole_POSet(A))& antisymmetric_relstr(boole_POSet(A))& lower_bounded_relstr(boole_POSet(A))& upper_bounded_relstr(boole_POSet(A))& bounded_relstr(boole_POSet(A))& up_complete_relstr(boole_POSet(A))& join_complete_relstr(boole_POSet(A))& ~ v1_yellow_3(boole_POSet(A))& distributive_relstr(boole_POSet(A))& heyting_relstr(boole_POSet(A))& complemented_relstr(boole_POSet(A))& boolean_relstr(boole_POSet(A))& with_suprema_relstr(boole_POSet(A))& with_infima_relstr(boole_POSet(A))& complete_relstr(boole_POSet(A)) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f49,axiom,(
% 0.14/15.87 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(cast_as_carrier_subset(A)) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f50,axiom,(
% 0.14/15.87 (! [A] :( ( with_suprema_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& directed_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f56,axiom,(
% 0.14/15.87 (! [A] :( ( with_infima_relstr(A)& rel_str(A) )=> ( ~ empty(cast_as_carrier_subset(A))& filtered_subset(cast_as_carrier_subset(A),A) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f61,axiom,(
% 0.14/15.87 (! [A,B,C] :( ( ~ empty_carrier(B)& one_sorted_str(B)& ~ empty_carrier(C)& net_str(C,B) )=> ( in(A,a_2_1_yellow19(B,C))<=> (? [D] :( element(D,powerset(the_carrier(B)))& A = D& is_eventually_in(B,C,D) ) )) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f63,axiom,(
% 0.14/15.87 (! [A] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& rel_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& ~ empty(B)& filtered_subset(B,A)& upper_relstr_subset(B,A) ) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f64,axiom,(
% 0.14/15.87 (! [A] :( ( reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A)& rel_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& ~ empty(B)& directed_subset(B,A)& filtered_subset(B,A)& lower_relstr_subset(B,A)& upper_relstr_subset(B,A) ) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f65,axiom,(
% 0.14/15.87 (? [A] :( rel_str(A)& ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& connected_relstr(A) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f66,axiom,(
% 0.14/15.87 (? [A] :( rel_str(A)& ~ empty_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A)& complete_relstr(A)& lower_bounded_relstr(A)& upper_bounded_relstr(A)& bounded_relstr(A)& up_complete_relstr(A)& join_complete_relstr(A) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f68,axiom,(
% 0.14/15.87 (? [A] :( rel_str(A)& ~ empty_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& complete_relstr(A) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f72,axiom,(
% 0.14/15.87 (? [A] :( rel_str(A)& ~ empty_carrier(A)& ~ trivial_carrier(A)& strict_rel_str(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& upper_bounded_relstr(A)& bounded_relstr(A)& ~ v1_yellow_3(A)& distributive_relstr(A)& heyting_relstr(A)& complemented_relstr(A)& boolean_relstr(A)& with_suprema_relstr(A)& with_infima_relstr(A) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f92,conjecture,(
% 0.14/15.87 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( in(C,filter_of_net_str(A,B))<=> ( is_eventually_in(A,B,C)& element(C,powerset(the_carrier(A))) ) ) )) )) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f93,negated_conjecture,(
% 0.14/15.87 ~((! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( ( ~ empty_carrier(B)& net_str(B,A) )=> (! [C] :( in(C,filter_of_net_str(A,B))<=> ( is_eventually_in(A,B,C)& element(C,powerset(the_carrier(A))) ) ) )) )) ))),
% 0.14/15.87 inference(negated_conjecture,[status(cth)],[f92])).
% 0.14/15.87 fof(f95,axiom,(
% 0.14/15.87 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f98,axiom,(
% 0.14/15.87 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f99,axiom,(
% 0.14/15.87 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 0.14/15.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/15.87 fof(f103,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(~strict_rel_str(A)|A=rel_str_of(the_carrier(A),the_InternalRel(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/15.87 fof(f104,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|~strict_rel_str(X0)|X0=rel_str_of(the_carrier(X0),the_InternalRel(X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f103])).
% 0.14/15.87 fof(f107,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(((empty_carrier(A)|~reflexive_relstr(A))|~complete_relstr(A))|(((~empty_carrier(A)&reflexive_relstr(A))&up_complete_relstr(A))&join_complete_relstr(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/15.87 fof(f110,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|empty_carrier(X0)|~reflexive_relstr(X0)|~complete_relstr(X0)|up_complete_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/15.87 fof(f111,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|empty_carrier(X0)|~reflexive_relstr(X0)|~complete_relstr(X0)|join_complete_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/15.87 fof(f140,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(~with_suprema_relstr(A)|~empty_carrier(A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/15.87 fof(f141,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|~with_suprema_relstr(X0)|~empty_carrier(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f140])).
% 0.14/15.87 fof(f147,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|((empty_carrier(A)|~complete_relstr(A))|((~empty_carrier(A)&with_suprema_relstr(A))&with_infima_relstr(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/15.87 fof(f149,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|with_suprema_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f147])).
% 0.14/15.87 fof(f150,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|with_infima_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f147])).
% 0.14/15.87 fof(f151,plain,(
% 0.14/15.87 ![A]: (~finite(A)|(![B]: (~element(B,powerset(A))|finite(B))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.14/15.87 fof(f152,plain,(
% 0.14/15.87 ![X0,X1]: (~finite(X0)|~element(X1,powerset(X0))|finite(X1))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f151])).
% 0.14/15.87 fof(f153,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(~with_infima_relstr(A)|~empty_carrier(A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.14/15.87 fof(f154,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|~with_infima_relstr(X0)|~empty_carrier(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f153])).
% 0.14/15.87 fof(f161,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|((empty_carrier(A)|~complete_relstr(A))|(~empty_carrier(A)&bounded_relstr(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.14/15.87 fof(f163,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|empty_carrier(X0)|~complete_relstr(X0)|bounded_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f161])).
% 0.14/15.87 fof(f164,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(~bounded_relstr(A)|(lower_bounded_relstr(A)&upper_bounded_relstr(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.14/15.87 fof(f166,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|~bounded_relstr(X0)|upper_bounded_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f164])).
% 0.14/15.87 fof(f173,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|(((~reflexive_relstr(A)|~with_suprema_relstr(A))|~up_complete_relstr(A))|(((~empty_carrier(A)&reflexive_relstr(A))&with_suprema_relstr(A))&upper_bounded_relstr(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.14/15.87 fof(f177,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|~reflexive_relstr(X0)|~with_suprema_relstr(X0)|~up_complete_relstr(X0)|upper_bounded_relstr(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f173])).
% 0.14/15.87 fof(f178,plain,(
% 0.14/15.87 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(![B]: ((empty_carrier(B)|~net_str(B,A))|filter_of_net_str(A,B)=a_2_1_yellow19(A,B))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.14/15.87 fof(f179,plain,(
% 0.14/15.87 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|filter_of_net_str(X0,X1)=a_2_1_yellow19(X0,X1))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f178])).
% 0.14/15.87 fof(f183,plain,(
% 0.14/15.87 ![A]: (~one_sorted_str(A)|element(cast_as_carrier_subset(A),powerset(the_carrier(A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.14/15.87 fof(f184,plain,(
% 0.14/15.87 ![X0]: (~one_sorted_str(X0)|element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f183])).
% 0.14/15.87 fof(f185,plain,(
% 0.14/15.87 ![A,B]: ((((empty_carrier(A)|~one_sorted_str(A))|empty_carrier(B))|~net_str(B,A))|element(filter_of_net_str(A,B),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.14/15.87 fof(f186,plain,(
% 0.14/15.87 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|element(filter_of_net_str(X0,X1),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f185])).
% 0.14/15.87 fof(f187,plain,(
% 0.14/15.87 (![A]: strict_rel_str(boole_POSet(A)))&(![A]: rel_str(boole_POSet(A)))),
% 0.14/15.87 inference(miniscoping,[status(thm)],[f28])).
% 0.14/15.87 fof(f189,plain,(
% 0.14/15.87 ![X0]: (rel_str(boole_POSet(X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f187])).
% 0.14/15.87 fof(f190,plain,(
% 0.14/15.87 ![A]: (~rel_str(A)|one_sorted_str(A))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.14/15.87 fof(f191,plain,(
% 0.14/15.87 ![X0]: (~rel_str(X0)|one_sorted_str(X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/15.87 fof(f192,plain,(
% 0.14/15.87 ![A]: (~one_sorted_str(A)|(![B]: (~net_str(B,A)|rel_str(B))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.14/15.87 fof(f193,plain,(
% 0.14/15.87 ![X0,X1]: (~one_sorted_str(X0)|~net_str(X1,X0)|rel_str(X1))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/15.87 fof(f198,plain,(
% 0.14/15.87 rel_str(sK0_skl)),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f37])).
% 0.14/15.87 fof(f199,plain,(
% 0.14/15.87 rel_str(sK0_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/15.87 fof(f202,plain,(
% 0.14/15.87 ![A]: (~one_sorted_str(A)|(?[B]: net_str(B,A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.14/15.87 fof(f203,plain,(
% 0.14/15.87 ![A]: (~one_sorted_str(A)|net_str(sK2_skl(A),A))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B,sK2_skl(A))],[f202])).
% 0.14/15.87 fof(f204,plain,(
% 0.14/15.87 ![X0]: (~one_sorted_str(X0)|net_str(sK2_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f203])).
% 0.14/15.87 fof(f207,plain,(
% 0.14/15.87 ![A]: element(sK4_skl(A),A)),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f41])).
% 0.14/15.87 fof(f208,plain,(
% 0.14/15.87 ![X0]: (element(sK4_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f207])).
% 0.14/15.87 fof(f216,plain,(
% 0.14/15.87 ![A]: ((empty_carrier(A)|~rel_str(A))|((~empty(cast_as_carrier_subset(A))&lower_relstr_subset(cast_as_carrier_subset(A),A))&upper_relstr_subset(cast_as_carrier_subset(A),A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.14/15.87 fof(f218,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~rel_str(X0)|lower_relstr_subset(cast_as_carrier_subset(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f216])).
% 0.14/15.87 fof(f219,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~rel_str(X0)|upper_relstr_subset(cast_as_carrier_subset(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f216])).
% 0.14/15.87 fof(f222,plain,(
% 0.14/15.87 ![X0]: (~empty(powerset(X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/15.87 fof(f223,plain,(
% 0.14/15.87 (((((((((((((((((![A]: ~empty_carrier(boole_POSet(A)))&(![A]: strict_rel_str(boole_POSet(A))))&(![A]: reflexive_relstr(boole_POSet(A))))&(![A]: transitive_relstr(boole_POSet(A))))&(![A]: antisymmetric_relstr(boole_POSet(A))))&(![A]: lower_bounded_relstr(boole_POSet(A))))&(![A]: upper_bounded_relstr(boole_POSet(A))))&(![A]: bounded_relstr(boole_POSet(A))))&(![A]: up_complete_relstr(boole_POSet(A))))&(![A]: join_complete_relstr(boole_POSet(A))))&(![A]: ~v1_yellow_3(boole_POSet(A))))&(![A]: distributive_relstr(boole_POSet(A))))&(![A]: heyting_relstr(boole_POSet(A))))&(![A]: complemented_relstr(boole_POSet(A))))&(![A]: boolean_relstr(boole_POSet(A))))&(![A]: with_suprema_relstr(boole_POSet(A))))&(![A]: with_infima_relstr(boole_POSet(A))))&(![A]: complete_relstr(boole_POSet(A)))),
% 0.14/15.87 inference(miniscoping,[status(thm)],[f48])).
% 0.14/15.87 fof(f224,plain,(
% 0.14/15.87 ![X0]: (~empty_carrier(boole_POSet(X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f223])).
% 0.14/15.87 fof(f242,plain,(
% 0.14/15.87 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(cast_as_carrier_subset(A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.14/15.87 fof(f243,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(cast_as_carrier_subset(X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f242])).
% 0.14/15.87 fof(f244,plain,(
% 0.14/15.87 ![A]: ((~with_suprema_relstr(A)|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&directed_subset(cast_as_carrier_subset(A),A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.14/15.87 fof(f246,plain,(
% 0.14/15.87 ![X0]: (~with_suprema_relstr(X0)|~rel_str(X0)|directed_subset(cast_as_carrier_subset(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f244])).
% 0.14/15.87 fof(f276,plain,(
% 0.14/15.87 ![A]: ((~with_infima_relstr(A)|~rel_str(A))|(~empty(cast_as_carrier_subset(A))&filtered_subset(cast_as_carrier_subset(A),A)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.14/15.87 fof(f278,plain,(
% 0.14/15.87 ![X0]: (~with_infima_relstr(X0)|~rel_str(X0)|filtered_subset(cast_as_carrier_subset(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f276])).
% 0.14/15.87 fof(f316,plain,(
% 0.14/15.87 ![A,B,C]: ((((empty_carrier(B)|~one_sorted_str(B))|empty_carrier(C))|~net_str(C,B))|(in(A,a_2_1_yellow19(B,C))<=>(?[D]: ((element(D,powerset(the_carrier(B)))&A=D)&is_eventually_in(B,C,D)))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.14/15.87 fof(f317,plain,(
% 0.14/15.87 ![A,B,C]: ((((empty_carrier(B)|~one_sorted_str(B))|empty_carrier(C))|~net_str(C,B))|((~in(A,a_2_1_yellow19(B,C))|(?[D]: ((element(D,powerset(the_carrier(B)))&A=D)&is_eventually_in(B,C,D))))&(in(A,a_2_1_yellow19(B,C))|(![D]: ((~element(D,powerset(the_carrier(B)))|~A=D)|~is_eventually_in(B,C,D))))))),
% 0.14/15.87 inference(NNF_transformation,[status(thm)],[f316])).
% 0.14/15.87 fof(f318,plain,(
% 0.14/15.87 ![B,C]: ((((empty_carrier(B)|~one_sorted_str(B))|empty_carrier(C))|~net_str(C,B))|((![A]: (~in(A,a_2_1_yellow19(B,C))|(?[D]: ((element(D,powerset(the_carrier(B)))&A=D)&is_eventually_in(B,C,D)))))&(![A]: (in(A,a_2_1_yellow19(B,C))|(![D]: ((~element(D,powerset(the_carrier(B)))|~A=D)|~is_eventually_in(B,C,D)))))))),
% 0.14/15.87 inference(miniscoping,[status(thm)],[f317])).
% 0.14/15.87 fof(f319,plain,(
% 0.14/15.87 ![B,C]: ((((empty_carrier(B)|~one_sorted_str(B))|empty_carrier(C))|~net_str(C,B))|((![A]: (~in(A,a_2_1_yellow19(B,C))|((element(sK6_skl(A,C,B),powerset(the_carrier(B)))&A=sK6_skl(A,C,B))&is_eventually_in(B,C,sK6_skl(A,C,B)))))&(![A]: (in(A,a_2_1_yellow19(B,C))|(![D]: ((~element(D,powerset(the_carrier(B)))|~A=D)|~is_eventually_in(B,C,D)))))))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(D,sK6_skl(A,C,B))],[f318])).
% 0.14/15.87 fof(f320,plain,(
% 0.14/15.87 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~in(X2,a_2_1_yellow19(X0,X1))|element(sK6_skl(X2,X1,X0),powerset(the_carrier(X0))))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f319])).
% 0.14/15.87 fof(f321,plain,(
% 0.14/15.87 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~in(X2,a_2_1_yellow19(X0,X1))|X2=sK6_skl(X2,X1,X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f319])).
% 0.14/15.87 fof(f322,plain,(
% 0.14/15.87 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|~in(X2,a_2_1_yellow19(X0,X1))|is_eventually_in(X0,X1,sK6_skl(X2,X1,X0)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f319])).
% 0.14/15.87 fof(f323,plain,(
% 0.14/15.87 ![X0,X1,X2,X3]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|in(X2,a_2_1_yellow19(X0,X1))|~element(X3,powerset(the_carrier(X0)))|~X2=X3|~is_eventually_in(X0,X1,X3))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f319])).
% 0.14/15.87 fof(f327,plain,(
% 0.14/15.87 ![A]: ((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~rel_str(A))|(?[B]: (((element(B,powerset(the_carrier(A)))&~empty(B))&filtered_subset(B,A))&upper_relstr_subset(B,A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.14/15.87 fof(f328,plain,(
% 0.14/15.87 ![A]: ((((empty_carrier(A)|~reflexive_relstr(A))|~transitive_relstr(A))|~rel_str(A))|(((element(sK7_skl(A),powerset(the_carrier(A)))&~empty(sK7_skl(A)))&filtered_subset(sK7_skl(A),A))&upper_relstr_subset(sK7_skl(A),A)))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f327])).
% 0.14/15.87 fof(f329,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|element(sK7_skl(X0),powerset(the_carrier(X0))))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f328])).
% 0.14/15.87 fof(f331,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|filtered_subset(sK7_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f328])).
% 0.14/15.87 fof(f332,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~reflexive_relstr(X0)|~transitive_relstr(X0)|~rel_str(X0)|upper_relstr_subset(sK7_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f328])).
% 0.14/15.87 fof(f333,plain,(
% 0.14/15.87 ![A]: ((((((~reflexive_relstr(A)|~transitive_relstr(A))|~antisymmetric_relstr(A))|~with_suprema_relstr(A))|~with_infima_relstr(A))|~rel_str(A))|(?[B]: (((((element(B,powerset(the_carrier(A)))&~empty(B))&directed_subset(B,A))&filtered_subset(B,A))&lower_relstr_subset(B,A))&upper_relstr_subset(B,A))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.14/15.87 fof(f334,plain,(
% 0.14/15.87 ![A]: ((((((~reflexive_relstr(A)|~transitive_relstr(A))|~antisymmetric_relstr(A))|~with_suprema_relstr(A))|~with_infima_relstr(A))|~rel_str(A))|(((((element(sK8_skl(A),powerset(the_carrier(A)))&~empty(sK8_skl(A)))&directed_subset(sK8_skl(A),A))&filtered_subset(sK8_skl(A),A))&lower_relstr_subset(sK8_skl(A),A))&upper_relstr_subset(sK8_skl(A),A)))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f333])).
% 0.14/15.87 fof(f335,plain,(
% 0.14/15.87 ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|element(sK8_skl(X0),powerset(the_carrier(X0))))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f334])).
% 0.14/15.87 fof(f337,plain,(
% 0.14/15.87 ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|directed_subset(sK8_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f334])).
% 0.14/15.87 fof(f338,plain,(
% 0.14/15.87 ![X0]: (~reflexive_relstr(X0)|~transitive_relstr(X0)|~antisymmetric_relstr(X0)|~with_suprema_relstr(X0)|~with_infima_relstr(X0)|~rel_str(X0)|filtered_subset(sK8_skl(X0),X0))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f334])).
% 0.14/15.87 fof(f341,plain,(
% 0.14/15.87 (((((rel_str(sK9_skl)&~empty_carrier(sK9_skl))&reflexive_relstr(sK9_skl))&transitive_relstr(sK9_skl))&antisymmetric_relstr(sK9_skl))&connected_relstr(sK9_skl))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f65])).
% 0.14/15.87 fof(f342,plain,(
% 0.14/15.87 rel_str(sK9_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f341])).
% 0.14/15.87 fof(f343,plain,(
% 0.14/15.87 ~empty_carrier(sK9_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f341])).
% 0.14/15.87 fof(f344,plain,(
% 0.14/15.87 reflexive_relstr(sK9_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f341])).
% 0.14/15.87 fof(f345,plain,(
% 0.14/15.87 transitive_relstr(sK9_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f341])).
% 0.14/15.87 fof(f348,plain,(
% 0.14/15.87 (((((((((((((rel_str(sK10_skl)&~empty_carrier(sK10_skl))&strict_rel_str(sK10_skl))&reflexive_relstr(sK10_skl))&transitive_relstr(sK10_skl))&antisymmetric_relstr(sK10_skl))&with_suprema_relstr(sK10_skl))&with_infima_relstr(sK10_skl))&complete_relstr(sK10_skl))&lower_bounded_relstr(sK10_skl))&upper_bounded_relstr(sK10_skl))&bounded_relstr(sK10_skl))&up_complete_relstr(sK10_skl))&join_complete_relstr(sK10_skl))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f66])).
% 0.14/15.87 fof(f349,plain,(
% 0.14/15.87 rel_str(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f350,plain,(
% 0.14/15.87 ~empty_carrier(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f351,plain,(
% 0.14/15.87 strict_rel_str(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f352,plain,(
% 0.14/15.87 reflexive_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f353,plain,(
% 0.14/15.87 transitive_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f354,plain,(
% 0.14/15.87 antisymmetric_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f355,plain,(
% 0.14/15.87 with_suprema_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f356,plain,(
% 0.14/15.87 with_infima_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f357,plain,(
% 0.14/15.87 complete_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f358,plain,(
% 0.14/15.87 lower_bounded_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f360,plain,(
% 0.14/15.87 bounded_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f361,plain,(
% 0.14/15.87 up_complete_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f362,plain,(
% 0.14/15.87 join_complete_relstr(sK10_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.14/15.87 fof(f366,plain,(
% 0.14/15.87 ((((((rel_str(sK12_skl)&~empty_carrier(sK12_skl))&strict_rel_str(sK12_skl))&reflexive_relstr(sK12_skl))&transitive_relstr(sK12_skl))&antisymmetric_relstr(sK12_skl))&complete_relstr(sK12_skl))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f68])).
% 0.14/15.87 fof(f367,plain,(
% 0.14/15.87 rel_str(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f368,plain,(
% 0.14/15.87 ~empty_carrier(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f369,plain,(
% 0.14/15.87 strict_rel_str(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f370,plain,(
% 0.14/15.87 reflexive_relstr(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f371,plain,(
% 0.14/15.87 transitive_relstr(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f373,plain,(
% 0.14/15.87 complete_relstr(sK12_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f366])).
% 0.14/15.87 fof(f386,plain,(
% 0.14/15.87 ((((((((((((((((rel_str(sK16_skl)&~empty_carrier(sK16_skl))&~trivial_carrier(sK16_skl))&strict_rel_str(sK16_skl))&reflexive_relstr(sK16_skl))&transitive_relstr(sK16_skl))&antisymmetric_relstr(sK16_skl))&lower_bounded_relstr(sK16_skl))&upper_bounded_relstr(sK16_skl))&bounded_relstr(sK16_skl))&~v1_yellow_3(sK16_skl))&distributive_relstr(sK16_skl))&heyting_relstr(sK16_skl))&complemented_relstr(sK16_skl))&boolean_relstr(sK16_skl))&with_suprema_relstr(sK16_skl))&with_infima_relstr(sK16_skl))),
% 0.14/15.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f72])).
% 0.14/15.87 fof(f387,plain,(
% 0.14/15.87 rel_str(sK16_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f386])).
% 0.14/15.87 fof(f388,plain,(
% 0.14/15.87 ~empty_carrier(sK16_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f386])).
% 0.14/15.87 fof(f508,plain,(
% 0.14/15.87 (?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: ((~empty_carrier(B)&net_str(B,A))&(?[C]: (in(C,filter_of_net_str(A,B))<~>(is_eventually_in(A,B,C)&element(C,powerset(the_carrier(A))))))))))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.14/15.87 fof(f509,plain,(
% 0.14/15.87 ?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: ((~empty_carrier(B)&net_str(B,A))&(?[C]: ((in(C,filter_of_net_str(A,B))|(is_eventually_in(A,B,C)&element(C,powerset(the_carrier(A)))))&(~in(C,filter_of_net_str(A,B))|(~is_eventually_in(A,B,C)|~element(C,powerset(the_carrier(A))))))))))),
% 0.14/15.87 inference(NNF_transformation,[status(thm)],[f508])).
% 0.14/15.87 fof(f510,plain,(
% 0.14/15.87 ((~empty_carrier(sK34_skl)&one_sorted_str(sK34_skl))&((~empty_carrier(sK35_skl)&net_str(sK35_skl,sK34_skl))&((in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|(is_eventually_in(sK34_skl,sK35_skl,sK36_skl)&element(sK36_skl,powerset(the_carrier(sK34_skl)))))&(~in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|(~is_eventually_in(sK34_skl,sK35_skl,sK36_skl)|~element(sK36_skl,powerset(the_carrier(sK34_skl))))))))),
% 0.14/15.87 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])).
% 0.14/15.87 fof(f511,plain,(
% 0.14/15.87 ~empty_carrier(sK34_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f512,plain,(
% 0.14/15.87 one_sorted_str(sK34_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f513,plain,(
% 0.14/15.87 ~empty_carrier(sK35_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f514,plain,(
% 0.14/15.87 net_str(sK35_skl,sK34_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f515,plain,(
% 0.14/15.87 in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|is_eventually_in(sK34_skl,sK35_skl,sK36_skl)),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f516,plain,(
% 0.14/15.87 in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|element(sK36_skl,powerset(the_carrier(sK34_skl)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f517,plain,(
% 0.14/15.87 ~in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|~is_eventually_in(sK34_skl,sK35_skl,sK36_skl)|~element(sK36_skl,powerset(the_carrier(sK34_skl)))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f510])).
% 0.14/15.87 fof(f520,plain,(
% 0.14/15.87 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 0.14/15.87 fof(f521,plain,(
% 0.14/15.87 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f520])).
% 0.14/15.87 fof(f531,plain,(
% 0.14/15.87 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f98])).
% 0.14/15.87 fof(f532,plain,(
% 0.14/15.87 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 0.14/15.87 inference(miniscoping,[status(thm)],[f531])).
% 0.14/15.87 fof(f533,plain,(
% 0.14/15.87 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f532])).
% 0.14/15.87 fof(f534,plain,(
% 0.14/15.87 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 0.14/15.87 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 0.14/15.87 fof(f535,plain,(
% 0.14/15.87 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 0.14/15.87 inference(miniscoping,[status(thm)],[f534])).
% 0.14/15.87 fof(f536,plain,(
% 0.14/15.87 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 0.14/15.87 inference(cnf_transformation,[status(thm)],[f535])).
% 0.14/15.87 fof(f545,definition,(
% 0.14/15.87 sQ0_spl <=> (in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f546,plain,(
% 0.14/15.87 in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|~sQ0_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f545])).
% 0.14/15.87 fof(f548,definition,(
% 0.14/15.87 sQ1_spl <=> (is_eventually_in(sK34_skl,sK35_skl,sK36_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f549,plain,(
% 0.14/15.87 is_eventually_in(sK34_skl,sK35_skl,sK36_skl)|~sQ1_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f548])).
% 0.14/15.87 fof(f550,plain,(
% 0.14/15.87 ~is_eventually_in(sK34_skl,sK35_skl,sK36_skl)|sQ1_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f548])).
% 0.14/15.87 fof(f551,plain,(
% 0.14/15.87 sQ0_spl|sQ1_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f515,f545,f548])).
% 0.14/15.87 fof(f552,definition,(
% 0.14/15.87 sQ2_spl <=> (element(sK36_skl,powerset(the_carrier(sK34_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f553,plain,(
% 0.14/15.87 element(sK36_skl,powerset(the_carrier(sK34_skl)))|~sQ2_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f552])).
% 0.14/15.87 fof(f555,plain,(
% 0.14/15.87 sQ0_spl|sQ2_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f516,f545,f552])).
% 0.14/15.87 fof(f556,plain,(
% 0.14/15.87 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f517,f545,f548,f552])).
% 0.14/15.87 fof(f561,plain,(
% 0.14/15.87 ![X0,X1,X2]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|in(X2,a_2_1_yellow19(X0,X1))|~element(X2,powerset(the_carrier(X0)))|~is_eventually_in(X0,X1,X2))),
% 0.14/15.87 inference(destructive_equality_resolution,[status(thm)],[f323])).
% 0.14/15.87 fof(f562,plain,(
% 0.14/15.87 one_sorted_str(sK0_skl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f199,f191])).
% 0.14/15.87 fof(f563,plain,(
% 0.14/15.87 ~one_sorted_str(sK34_skl)|rel_str(sK35_skl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f514,f193])).
% 0.14/15.87 fof(f564,plain,(
% 0.14/15.87 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK35_skl)|element(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))),
% 0.14/15.87 inference(resolution,[status(thm)],[f514,f186])).
% 0.14/15.87 fof(f565,plain,(
% 0.14/15.87 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK35_skl)|filter_of_net_str(sK34_skl,sK35_skl)=a_2_1_yellow19(sK34_skl,sK35_skl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f514,f179])).
% 0.14/15.87 fof(f566,definition,(
% 0.14/15.87 sQ3_spl <=> (one_sorted_str(sK34_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f568,plain,(
% 0.14/15.87 ~one_sorted_str(sK34_skl)|sQ3_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f566])).
% 0.14/15.87 fof(f569,definition,(
% 0.14/15.87 sQ4_spl <=> (rel_str(sK35_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f570,plain,(
% 0.14/15.87 rel_str(sK35_skl)|~sQ4_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f569])).
% 0.14/15.87 fof(f572,plain,(
% 0.14/15.87 ~sQ3_spl|sQ4_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f563,f566,f569])).
% 0.14/15.87 fof(f573,definition,(
% 0.14/15.87 sQ5_spl <=> (empty_carrier(sK34_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f574,plain,(
% 0.14/15.87 empty_carrier(sK34_skl)|~sQ5_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f573])).
% 0.14/15.87 fof(f576,definition,(
% 0.14/15.87 sQ6_spl <=> (empty_carrier(sK35_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f577,plain,(
% 0.14/15.87 empty_carrier(sK35_skl)|~sQ6_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f576])).
% 0.14/15.87 fof(f579,definition,(
% 0.14/15.87 sQ7_spl <=> (element(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f580,plain,(
% 0.14/15.87 element(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|~sQ7_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f579])).
% 0.14/15.87 fof(f582,plain,(
% 0.14/15.87 sQ5_spl|~sQ3_spl|sQ6_spl|sQ7_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f564,f573,f566,f576,f579])).
% 0.14/15.87 fof(f583,definition,(
% 0.14/15.87 sQ8_spl <=> (filter_of_net_str(sK34_skl,sK35_skl)=a_2_1_yellow19(sK34_skl,sK35_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f584,plain,(
% 0.14/15.87 filter_of_net_str(sK34_skl,sK35_skl)=a_2_1_yellow19(sK34_skl,sK35_skl)|~sQ8_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f583])).
% 0.14/15.87 fof(f586,plain,(
% 0.14/15.87 sQ5_spl|~sQ3_spl|sQ6_spl|sQ8_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f565,f573,f566,f576,f583])).
% 0.14/15.87 fof(f587,plain,(
% 0.14/15.87 $false|sQ3_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f568,f512])).
% 0.14/15.87 fof(f588,plain,(
% 0.14/15.87 sQ3_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f587])).
% 0.14/15.87 fof(f589,plain,(
% 0.14/15.87 $false|~sQ6_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f577,f513])).
% 0.14/15.87 fof(f590,plain,(
% 0.14/15.87 ~sQ6_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f589])).
% 0.14/15.87 fof(f591,plain,(
% 0.14/15.87 $false|~sQ5_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f574,f511])).
% 0.14/15.87 fof(f592,plain,(
% 0.14/15.87 ~sQ5_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f591])).
% 0.14/15.87 fof(f596,plain,(
% 0.14/15.87 one_sorted_str(sK9_skl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f342,f191])).
% 0.14/15.87 fof(f599,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))|~one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl)))|empty_carrier(X0)|~net_str(X0,boole_POSet(cast_as_carrier_subset(sK34_skl)))|in(filter_of_net_str(sK34_skl,sK35_skl),a_2_1_yellow19(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0))|~is_eventually_in(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0,filter_of_net_str(sK34_skl,sK35_skl))|~sQ7_spl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f580,f561])).
% 0.14/15.87 fof(f600,plain,(
% 0.14/15.87 empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|in(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|~sQ7_spl),
% 0.14/15.87 inference(resolution,[status(thm)],[f580,f521])).
% 0.14/15.87 fof(f601,definition,(
% 0.14/15.87 sQ9_spl <=> (empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f602,plain,(
% 0.14/15.87 empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))|~sQ9_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f601])).
% 0.14/15.87 fof(f604,definition,(
% 0.14/15.87 sQ10_spl <=> (one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f606,plain,(
% 0.14/15.87 ~one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl)))|sQ10_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f604])).
% 0.14/15.87 fof(f607,definition,(
% 0.14/15.87 ![X0]: (sQ11_spl <=> (empty_carrier(X0)|~net_str(X0,boole_POSet(cast_as_carrier_subset(sK34_skl)))|in(filter_of_net_str(sK34_skl,sK35_skl),a_2_1_yellow19(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0))|~is_eventually_in(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0,filter_of_net_str(sK34_skl,sK35_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f610,plain,(
% 0.14/15.87 sQ9_spl|~sQ10_spl|sQ11_spl|~sQ7_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f599,f601,f604,f607,f579])).
% 0.14/15.87 fof(f611,definition,(
% 0.14/15.87 sQ12_spl <=> (empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f612,plain,(
% 0.14/15.87 empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|~sQ12_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f611])).
% 0.14/15.87 fof(f614,definition,(
% 0.14/15.87 sQ13_spl <=> (in(filter_of_net_str(sK34_skl,sK35_skl),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f617,plain,(
% 0.14/15.87 sQ12_spl|sQ13_spl|~sQ7_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f600,f611,f614,f579])).
% 0.14/15.87 fof(f618,plain,(
% 0.14/15.87 $false|~sQ12_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f612,f222])).
% 0.14/15.87 fof(f619,plain,(
% 0.14/15.87 ~sQ12_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f618])).
% 0.14/15.87 fof(f622,plain,(
% 0.14/15.87 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|~empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))|~sQ7_spl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f536,f580])).
% 0.14/15.87 fof(f623,definition,(
% 0.14/15.87 ![X0]: (sQ14_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f624,plain,(
% 0.14/15.87 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|~sQ14_spl)),
% 0.14/15.87 inference(component_clause,[status(thm)],[f623])).
% 0.14/15.87 fof(f626,definition,(
% 0.14/15.87 sQ15_spl <=> (empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f629,plain,(
% 0.14/15.87 sQ14_spl|~sQ15_spl|~sQ7_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f622,f623,f626,f579])).
% 0.14/15.87 fof(f630,plain,(
% 0.14/15.87 $false|~sQ14_spl|~sQ0_spl),
% 0.14/15.87 inference(backward_subsumption_resolution,[status(thm)],[f546,f624])).
% 0.14/15.87 fof(f631,plain,(
% 0.14/15.87 ~sQ14_spl|~sQ0_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f630])).
% 0.14/15.87 fof(f635,plain,(
% 0.14/15.87 ~finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))|finite(filter_of_net_str(sK34_skl,sK35_skl))|~sQ7_spl),
% 0.14/15.87 inference(resolution,[status(thm)],[f152,f580])).
% 0.14/15.87 fof(f636,definition,(
% 0.14/15.87 sQ16_spl <=> (finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f639,definition,(
% 0.14/15.87 sQ17_spl <=> (finite(filter_of_net_str(sK34_skl,sK35_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f642,plain,(
% 0.14/15.87 ~sQ16_spl|sQ17_spl|~sQ7_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f635,f636,f639,f579])).
% 0.14/15.87 fof(f653,definition,(
% 0.14/15.87 sQ19_spl <=> (rel_str(sK9_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f655,plain,(
% 0.14/15.87 ~rel_str(sK9_skl)|sQ19_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f653])).
% 0.14/15.87 fof(f656,definition,(
% 0.14/15.87 sQ20_spl <=> (empty_carrier(sK9_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f657,plain,(
% 0.14/15.87 empty_carrier(sK9_skl)|~sQ20_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f656])).
% 0.14/15.87 fof(f659,definition,(
% 0.14/15.87 sQ21_spl <=> (reflexive_relstr(sK9_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f661,plain,(
% 0.14/15.87 ~reflexive_relstr(sK9_skl)|sQ21_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f659])).
% 0.14/15.87 fof(f669,plain,(
% 0.14/15.87 $false|sQ21_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f661,f344])).
% 0.14/15.87 fof(f670,plain,(
% 0.14/15.87 sQ21_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f669])).
% 0.14/15.87 fof(f671,plain,(
% 0.14/15.87 $false|~sQ20_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f657,f343])).
% 0.14/15.87 fof(f672,plain,(
% 0.14/15.87 ~sQ20_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f671])).
% 0.14/15.87 fof(f673,plain,(
% 0.14/15.87 $false|sQ19_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f655,f342])).
% 0.14/15.87 fof(f674,plain,(
% 0.14/15.87 sQ19_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f673])).
% 0.14/15.87 fof(f675,plain,(
% 0.14/15.87 one_sorted_str(sK10_skl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f349,f191])).
% 0.14/15.87 fof(f701,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(X0)|~net_str(X0,sK34_skl)|in(sK36_skl,a_2_1_yellow19(sK34_skl,X0))|~is_eventually_in(sK34_skl,X0,sK36_skl)|~sQ2_spl)),
% 0.14/15.87 inference(resolution,[status(thm)],[f553,f561])).
% 0.14/15.87 fof(f706,definition,(
% 0.14/15.87 ![X0]: (sQ28_spl <=> (empty_carrier(X0)|~net_str(X0,sK34_skl)|in(sK36_skl,a_2_1_yellow19(sK34_skl,X0))|~is_eventually_in(sK34_skl,X0,sK36_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f707,plain,(
% 0.14/15.87 ![X0]: (empty_carrier(X0)|~net_str(X0,sK34_skl)|in(sK36_skl,a_2_1_yellow19(sK34_skl,X0))|~is_eventually_in(sK34_skl,X0,sK36_skl)|~sQ28_spl)),
% 0.14/15.87 inference(component_clause,[status(thm)],[f706])).
% 0.14/15.87 fof(f709,plain,(
% 0.14/15.87 sQ5_spl|~sQ3_spl|sQ28_spl|~sQ2_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f701,f573,f566,f706,f552])).
% 0.14/15.87 fof(f720,definition,(
% 0.14/15.87 sQ32_spl <=> (empty(the_carrier(sK34_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f724,definition,(
% 0.14/15.87 sQ33_spl <=> (empty(powerset(the_carrier(sK34_skl))))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f725,plain,(
% 0.14/15.87 empty(powerset(the_carrier(sK34_skl)))|~sQ33_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f724])).
% 0.14/15.87 fof(f731,plain,(
% 0.14/15.87 $false|~sQ33_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f725,f222])).
% 0.14/15.87 fof(f732,plain,(
% 0.14/15.87 ~sQ33_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f731])).
% 0.14/15.87 fof(f733,plain,(
% 0.14/15.87 empty_carrier(sK35_skl)|~net_str(sK35_skl,sK34_skl)|in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl))|~sQ28_spl|~sQ1_spl),
% 0.14/15.87 inference(resolution,[status(thm)],[f707,f549])).
% 0.14/15.87 fof(f734,definition,(
% 0.14/15.87 sQ35_spl <=> (net_str(sK35_skl,sK34_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f736,plain,(
% 0.14/15.87 ~net_str(sK35_skl,sK34_skl)|sQ35_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f734])).
% 0.14/15.87 fof(f737,definition,(
% 0.14/15.87 sQ36_spl <=> (in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f738,plain,(
% 0.14/15.87 in(sK36_skl,a_2_1_yellow19(sK34_skl,sK35_skl))|~sQ36_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f737])).
% 0.14/15.87 fof(f740,plain,(
% 0.14/15.87 sQ6_spl|~sQ35_spl|sQ36_spl|~sQ28_spl|~sQ1_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f733,f576,f734,f737,f706,f548])).
% 0.14/15.87 fof(f741,plain,(
% 0.14/15.87 $false|sQ35_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f736,f514])).
% 0.14/15.87 fof(f742,plain,(
% 0.14/15.87 sQ35_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f741])).
% 0.14/15.87 fof(f743,plain,(
% 0.14/15.87 in(sK36_skl,filter_of_net_str(sK34_skl,sK35_skl))|~sQ8_spl|~sQ36_spl),
% 0.14/15.87 inference(forward_demodulation,[status(thm)],[f584,f738])).
% 0.14/15.87 fof(f746,plain,(
% 0.14/15.87 $false|~sQ9_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f602,f224])).
% 0.14/15.87 fof(f747,plain,(
% 0.14/15.87 ~sQ9_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f746])).
% 0.14/15.87 fof(f751,plain,(
% 0.14/15.87 ~rel_str(sK10_skl)|sK10_skl=rel_str_of(the_carrier(sK10_skl),the_InternalRel(sK10_skl))),
% 0.14/15.87 inference(resolution,[status(thm)],[f351,f104])).
% 0.14/15.87 fof(f752,definition,(
% 0.14/15.87 sQ37_spl <=> (rel_str(sK10_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f754,plain,(
% 0.14/15.87 ~rel_str(sK10_skl)|sQ37_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f752])).
% 0.14/15.87 fof(f755,definition,(
% 0.14/15.87 sQ38_spl <=> (sK10_skl=rel_str_of(the_carrier(sK10_skl),the_InternalRel(sK10_skl)))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f758,plain,(
% 0.14/15.87 ~sQ37_spl|sQ38_spl),
% 0.14/15.87 inference(split_clause,[status(thm)],[f751,f752,f755])).
% 0.14/15.87 fof(f759,plain,(
% 0.14/15.87 $false|sQ37_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f754,f349])).
% 0.14/15.87 fof(f760,plain,(
% 0.14/15.87 sQ37_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f759])).
% 0.14/15.87 fof(f762,definition,(
% 0.14/15.87 sQ39_spl <=> (with_suprema_relstr(sK10_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f764,plain,(
% 0.14/15.87 ~with_suprema_relstr(sK10_skl)|sQ39_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f762])).
% 0.14/15.87 fof(f765,definition,(
% 0.14/15.87 sQ40_spl <=> (up_complete_relstr(sK10_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f767,plain,(
% 0.14/15.87 ~up_complete_relstr(sK10_skl)|sQ40_spl),
% 0.14/15.87 inference(component_clause,[status(thm)],[f765])).
% 0.14/15.87 fof(f768,definition,(
% 0.14/15.87 sQ41_spl <=> (upper_bounded_relstr(sK10_skl))),
% 0.14/15.87 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/15.87 fof(f772,plain,(
% 0.14/15.87 $false|sQ40_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f767,f361])).
% 0.14/15.87 fof(f773,plain,(
% 0.14/15.87 sQ40_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f772])).
% 0.14/15.87 fof(f774,plain,(
% 0.14/15.87 $false|sQ39_spl),
% 0.14/15.87 inference(forward_subsumption_resolution,[status(thm)],[f764,f355])).
% 0.14/15.87 fof(f775,plain,(
% 0.14/15.87 sQ39_spl),
% 0.14/15.87 inference(contradiction_clause,[status(thm)],[f774])).
% 0.14/15.87 fof(f776,plain,(
% 0.14/15.87 element(cast_as_carrier_subset(sK10_skl),powerset(the_carrier(sK10_skl)))),
% 0.14/15.87 inference(resolution,[status(thm)],[f184,f675])).
% 0.14/15.87 fof(f777,plain,(
% 0.14/15.87 element(cast_as_carrier_subset(sK9_skl),powerset(the_carrier(sK9_skl)))),
% 0.14/15.87 inference(resolution,[status(thm)],[f184,f596])).
% 0.14/15.87 fof(f779,plain,(
% 0.14/15.87 element(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl)))),
% 0.14/15.87 inference(resolution,[status(thm)],[f184,f562])).
% 0.14/15.88 fof(f781,plain,(
% 0.14/15.88 element(cast_as_carrier_subset(sK34_skl),powerset(the_carrier(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f184,f512])).
% 0.14/15.88 fof(f784,plain,(
% 0.14/15.88 ![X0]: (one_sorted_str(boole_POSet(X0)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f189,f191])).
% 0.14/15.88 fof(f785,plain,(
% 0.14/15.88 $false|sQ10_spl),
% 0.14/15.88 inference(backward_subsumption_resolution,[status(thm)],[f606,f784])).
% 0.14/15.88 fof(f786,plain,(
% 0.14/15.88 sQ10_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f785])).
% 0.14/15.88 fof(f799,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(X0)|~net_str(X0,sK34_skl)|in(cast_as_carrier_subset(sK34_skl),a_2_1_yellow19(sK34_skl,X0))|~is_eventually_in(sK34_skl,X0,cast_as_carrier_subset(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f781,f561])).
% 0.14/15.88 fof(f801,plain,(
% 0.14/15.88 ![X0]: (~in(X0,cast_as_carrier_subset(sK34_skl))|~empty(the_carrier(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f781,f536])).
% 0.14/15.88 fof(f802,plain,(
% 0.14/15.88 ![X0]: (~in(X0,cast_as_carrier_subset(sK34_skl))|element(X0,the_carrier(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f781,f533])).
% 0.14/15.88 fof(f803,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK34_skl)))|in(cast_as_carrier_subset(sK34_skl),powerset(the_carrier(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f781,f521])).
% 0.14/15.88 fof(f804,definition,(
% 0.14/15.88 ![X0]: (sQ42_spl <=> (empty_carrier(X0)|~net_str(X0,sK34_skl)|in(cast_as_carrier_subset(sK34_skl),a_2_1_yellow19(sK34_skl,X0))|~is_eventually_in(sK34_skl,X0,cast_as_carrier_subset(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f807,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ42_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f799,f573,f566,f804])).
% 0.14/15.88 fof(f812,definition,(
% 0.14/15.88 ![X0]: (sQ44_spl <=> (~in(X0,cast_as_carrier_subset(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f813,plain,(
% 0.14/15.88 ![X0]: (~in(X0,cast_as_carrier_subset(sK34_skl))|~sQ44_spl)),
% 0.14/15.88 inference(component_clause,[status(thm)],[f812])).
% 0.14/15.88 fof(f815,plain,(
% 0.14/15.88 sQ44_spl|~sQ32_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f801,f812,f720])).
% 0.14/15.88 fof(f816,definition,(
% 0.14/15.88 sQ45_spl <=> (in(cast_as_carrier_subset(sK34_skl),powerset(the_carrier(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f819,plain,(
% 0.14/15.88 sQ33_spl|sQ45_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f803,f724,f816])).
% 0.14/15.88 fof(f821,definition,(
% 0.14/15.88 sQ46_spl <=> (empty_carrier(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f822,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|~sQ46_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f821])).
% 0.14/15.88 fof(f824,definition,(
% 0.14/15.88 sQ47_spl <=> (reflexive_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f826,plain,(
% 0.14/15.88 ~reflexive_relstr(sK10_skl)|sQ47_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f824])).
% 0.14/15.88 fof(f827,definition,(
% 0.14/15.88 sQ48_spl <=> (join_complete_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f829,plain,(
% 0.14/15.88 ~join_complete_relstr(sK10_skl)|sQ48_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f827])).
% 0.14/15.88 fof(f830,definition,(
% 0.14/15.88 sQ49_spl <=> (with_infima_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f834,plain,(
% 0.14/15.88 $false|sQ48_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f829,f362])).
% 0.14/15.88 fof(f835,plain,(
% 0.14/15.88 sQ48_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f834])).
% 0.14/15.88 fof(f836,plain,(
% 0.14/15.88 $false|sQ47_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f826,f352])).
% 0.14/15.88 fof(f837,plain,(
% 0.14/15.88 sQ47_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f836])).
% 0.14/15.88 fof(f838,plain,(
% 0.14/15.88 $false|~sQ46_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f822,f350])).
% 0.14/15.88 fof(f839,plain,(
% 0.14/15.88 ~sQ46_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f838])).
% 0.14/15.88 fof(f845,plain,(
% 0.14/15.88 net_str(sK2_skl(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f204,f675])).
% 0.14/15.88 fof(f846,plain,(
% 0.14/15.88 net_str(sK2_skl(sK9_skl),sK9_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f204,f596])).
% 0.14/15.88 fof(f848,plain,(
% 0.14/15.88 net_str(sK2_skl(sK0_skl),sK0_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f204,f562])).
% 0.14/15.88 fof(f850,plain,(
% 0.14/15.88 net_str(sK2_skl(sK34_skl),sK34_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f204,f512])).
% 0.14/15.88 fof(f858,plain,(
% 0.14/15.88 ![X0]: (empty(X0)|in(sK4_skl(X0),X0))),
% 0.14/15.88 inference(resolution,[status(thm)],[f208,f521])).
% 0.14/15.88 fof(f863,plain,(
% 0.14/15.88 ~one_sorted_str(sK34_skl)|rel_str(sK2_skl(sK34_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f850,f193])).
% 0.14/15.88 fof(f864,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|element(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))),
% 0.14/15.88 inference(resolution,[status(thm)],[f850,f186])).
% 0.14/15.88 fof(f865,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|filter_of_net_str(sK34_skl,sK2_skl(sK34_skl))=a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f850,f179])).
% 0.14/15.88 fof(f866,definition,(
% 0.14/15.88 sQ50_spl <=> (rel_str(sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f867,plain,(
% 0.14/15.88 rel_str(sK2_skl(sK34_skl))|~sQ50_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f866])).
% 0.14/15.88 fof(f869,plain,(
% 0.14/15.88 ~sQ3_spl|sQ50_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f863,f566,f866])).
% 0.14/15.88 fof(f870,definition,(
% 0.14/15.88 sQ51_spl <=> (empty_carrier(sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f871,plain,(
% 0.14/15.88 empty_carrier(sK2_skl(sK34_skl))|~sQ51_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f870])).
% 0.14/15.88 fof(f873,definition,(
% 0.14/15.88 sQ52_spl <=> (element(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f874,plain,(
% 0.14/15.88 element(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|~sQ52_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f873])).
% 0.14/15.88 fof(f876,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|sQ52_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f864,f573,f566,f870,f873])).
% 0.14/15.88 fof(f877,definition,(
% 0.14/15.88 sQ53_spl <=> (filter_of_net_str(sK34_skl,sK2_skl(sK34_skl))=a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f878,plain,(
% 0.14/15.88 filter_of_net_str(sK34_skl,sK2_skl(sK34_skl))=a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))|~sQ53_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f877])).
% 0.14/15.88 fof(f880,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|sQ53_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f865,f573,f566,f870,f877])).
% 0.14/15.88 fof(f882,plain,(
% 0.14/15.88 ~rel_str(sK2_skl(sK34_skl))|~with_infima_relstr(sK2_skl(sK34_skl))|~sQ51_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f871,f154])).
% 0.14/15.88 fof(f883,plain,(
% 0.14/15.88 ~rel_str(sK2_skl(sK34_skl))|~with_suprema_relstr(sK2_skl(sK34_skl))|~sQ51_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f871,f141])).
% 0.14/15.88 fof(f884,definition,(
% 0.14/15.88 sQ54_spl <=> (with_infima_relstr(sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f887,plain,(
% 0.14/15.88 ~sQ50_spl|~sQ54_spl|~sQ51_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f882,f866,f884,f870])).
% 0.14/15.88 fof(f888,definition,(
% 0.14/15.88 sQ55_spl <=> (with_suprema_relstr(sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f891,plain,(
% 0.14/15.88 ~sQ50_spl|~sQ55_spl|~sQ51_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f883,f866,f888,f870])).
% 0.14/15.88 fof(f907,plain,(
% 0.14/15.88 sQ0_spl|~sQ8_spl|~sQ36_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f743,f545,f583,f737])).
% 0.14/15.88 fof(f913,plain,(
% 0.14/15.88 ~rel_str(sK10_skl)|empty_carrier(sK10_skl)|bounded_relstr(sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f357,f163])).
% 0.14/15.88 fof(f914,plain,(
% 0.14/15.88 ~rel_str(sK10_skl)|empty_carrier(sK10_skl)|with_infima_relstr(sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f357,f150])).
% 0.14/15.88 fof(f918,definition,(
% 0.14/15.88 sQ57_spl <=> (bounded_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f921,plain,(
% 0.14/15.88 ~sQ37_spl|sQ46_spl|sQ57_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f913,f752,f821,f918])).
% 0.14/15.88 fof(f922,plain,(
% 0.14/15.88 ~sQ37_spl|sQ46_spl|sQ49_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f914,f752,f821,f830])).
% 0.14/15.88 fof(f928,plain,(
% 0.14/15.88 empty_carrier(sK2_skl(sK34_skl))|lower_relstr_subset(cast_as_carrier_subset(sK2_skl(sK34_skl)),sK2_skl(sK34_skl))|~sQ50_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f218,f867])).
% 0.14/15.88 fof(f930,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|lower_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f218,f349])).
% 0.14/15.88 fof(f931,plain,(
% 0.14/15.88 empty_carrier(sK9_skl)|lower_relstr_subset(cast_as_carrier_subset(sK9_skl),sK9_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f218,f342])).
% 0.14/15.88 fof(f932,plain,(
% 0.14/15.88 empty_carrier(sK35_skl)|lower_relstr_subset(cast_as_carrier_subset(sK35_skl),sK35_skl)|~sQ4_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f218,f570])).
% 0.14/15.88 fof(f934,definition,(
% 0.14/15.88 sQ58_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK2_skl(sK34_skl)),sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f937,plain,(
% 0.14/15.88 sQ51_spl|sQ58_spl|~sQ50_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f928,f870,f934,f866])).
% 0.14/15.88 fof(f939,definition,(
% 0.14/15.88 sQ59_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f942,plain,(
% 0.14/15.88 sQ46_spl|sQ59_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f930,f821,f939])).
% 0.14/15.88 fof(f943,definition,(
% 0.14/15.88 sQ60_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK9_skl),sK9_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f946,plain,(
% 0.14/15.88 sQ20_spl|sQ60_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f931,f656,f943])).
% 0.14/15.88 fof(f947,definition,(
% 0.14/15.88 sQ61_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK35_skl),sK35_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f950,plain,(
% 0.14/15.88 sQ6_spl|sQ61_spl|~sQ4_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f932,f576,f947,f569])).
% 0.14/15.88 fof(f958,plain,(
% 0.14/15.88 empty_carrier(sK2_skl(sK34_skl))|upper_relstr_subset(cast_as_carrier_subset(sK2_skl(sK34_skl)),sK2_skl(sK34_skl))|~sQ50_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f219,f867])).
% 0.14/15.88 fof(f960,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|upper_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f219,f349])).
% 0.14/15.88 fof(f961,plain,(
% 0.14/15.88 empty_carrier(sK9_skl)|upper_relstr_subset(cast_as_carrier_subset(sK9_skl),sK9_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f219,f342])).
% 0.14/15.88 fof(f962,plain,(
% 0.14/15.88 empty_carrier(sK35_skl)|upper_relstr_subset(cast_as_carrier_subset(sK35_skl),sK35_skl)|~sQ4_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f219,f570])).
% 0.14/15.88 fof(f964,definition,(
% 0.14/15.88 sQ64_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK2_skl(sK34_skl)),sK2_skl(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f967,plain,(
% 0.14/15.88 sQ51_spl|sQ64_spl|~sQ50_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f958,f870,f964,f866])).
% 0.14/15.88 fof(f969,definition,(
% 0.14/15.88 sQ65_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f972,plain,(
% 0.14/15.88 sQ46_spl|sQ65_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f960,f821,f969])).
% 0.14/15.88 fof(f973,definition,(
% 0.14/15.88 sQ66_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK9_skl),sK9_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f976,plain,(
% 0.14/15.88 sQ20_spl|sQ66_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f961,f656,f973])).
% 0.14/15.88 fof(f977,definition,(
% 0.14/15.88 sQ67_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK35_skl),sK35_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f980,plain,(
% 0.14/15.88 sQ6_spl|sQ67_spl|~sQ4_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f962,f576,f977,f569])).
% 0.14/15.88 fof(f997,definition,(
% 0.14/15.88 sQ69_spl <=> (lower_bounded_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f999,plain,(
% 0.14/15.88 ~lower_bounded_relstr(sK10_skl)|sQ69_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f997])).
% 0.14/15.88 fof(f1001,definition,(
% 0.14/15.88 sQ70_spl <=> (antisymmetric_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1003,plain,(
% 0.14/15.88 ~antisymmetric_relstr(sK10_skl)|sQ70_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1001])).
% 0.14/15.88 fof(f1005,plain,(
% 0.14/15.88 $false|sQ69_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f999,f358])).
% 0.14/15.88 fof(f1006,plain,(
% 0.14/15.88 sQ69_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1005])).
% 0.14/15.88 fof(f1007,plain,(
% 0.14/15.88 ~rel_str(sK10_skl)|upper_bounded_relstr(sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f360,f166])).
% 0.14/15.88 fof(f1009,plain,(
% 0.14/15.88 ~sQ37_spl|sQ41_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1007,f752,f768])).
% 0.14/15.88 fof(f1023,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK10_skl)|~one_sorted_str(sK10_skl)|empty_carrier(X0)|~net_str(X0,sK10_skl)|in(cast_as_carrier_subset(sK10_skl),a_2_1_yellow19(sK10_skl,X0))|~is_eventually_in(sK10_skl,X0,cast_as_carrier_subset(sK10_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f776,f561])).
% 0.14/15.88 fof(f1027,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK10_skl)))|in(cast_as_carrier_subset(sK10_skl),powerset(the_carrier(sK10_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f776,f521])).
% 0.14/15.88 fof(f1028,definition,(
% 0.14/15.88 sQ71_spl <=> (one_sorted_str(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1030,plain,(
% 0.14/15.88 ~one_sorted_str(sK10_skl)|sQ71_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1028])).
% 0.14/15.88 fof(f1031,definition,(
% 0.14/15.88 ![X0]: (sQ72_spl <=> (empty_carrier(X0)|~net_str(X0,sK10_skl)|in(cast_as_carrier_subset(sK10_skl),a_2_1_yellow19(sK10_skl,X0))|~is_eventually_in(sK10_skl,X0,cast_as_carrier_subset(sK10_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1034,plain,(
% 0.14/15.88 sQ46_spl|~sQ71_spl|sQ72_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1023,f821,f1028,f1031])).
% 0.14/15.88 fof(f1049,definition,(
% 0.14/15.88 sQ77_spl <=> (empty(powerset(the_carrier(sK10_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1050,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK10_skl)))|~sQ77_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1049])).
% 0.14/15.88 fof(f1052,definition,(
% 0.14/15.88 sQ78_spl <=> (in(cast_as_carrier_subset(sK10_skl),powerset(the_carrier(sK10_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1055,plain,(
% 0.14/15.88 sQ77_spl|sQ78_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1027,f1049,f1052])).
% 0.14/15.88 fof(f1056,plain,(
% 0.14/15.88 $false|sQ71_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1030,f675])).
% 0.14/15.88 fof(f1057,plain,(
% 0.14/15.88 sQ71_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1056])).
% 0.14/15.88 fof(f1058,plain,(
% 0.14/15.88 $false|~sQ77_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1050,f222])).
% 0.14/15.88 fof(f1059,plain,(
% 0.14/15.88 ~sQ77_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1058])).
% 0.14/15.88 fof(f1060,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK9_skl)|~one_sorted_str(sK9_skl)|empty_carrier(X0)|~net_str(X0,sK9_skl)|in(cast_as_carrier_subset(sK9_skl),a_2_1_yellow19(sK9_skl,X0))|~is_eventually_in(sK9_skl,X0,cast_as_carrier_subset(sK9_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f777,f561])).
% 0.14/15.88 fof(f1064,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK9_skl)))|in(cast_as_carrier_subset(sK9_skl),powerset(the_carrier(sK9_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f777,f521])).
% 0.14/15.88 fof(f1065,definition,(
% 0.14/15.88 sQ79_spl <=> (one_sorted_str(sK9_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1067,plain,(
% 0.14/15.88 ~one_sorted_str(sK9_skl)|sQ79_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1065])).
% 0.14/15.88 fof(f1068,definition,(
% 0.14/15.88 ![X0]: (sQ80_spl <=> (empty_carrier(X0)|~net_str(X0,sK9_skl)|in(cast_as_carrier_subset(sK9_skl),a_2_1_yellow19(sK9_skl,X0))|~is_eventually_in(sK9_skl,X0,cast_as_carrier_subset(sK9_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1071,plain,(
% 0.14/15.88 sQ20_spl|~sQ79_spl|sQ80_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1060,f656,f1065,f1068])).
% 0.14/15.88 fof(f1086,definition,(
% 0.14/15.88 sQ85_spl <=> (empty(powerset(the_carrier(sK9_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1087,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK9_skl)))|~sQ85_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1086])).
% 0.14/15.88 fof(f1089,definition,(
% 0.14/15.88 sQ86_spl <=> (in(cast_as_carrier_subset(sK9_skl),powerset(the_carrier(sK9_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1092,plain,(
% 0.14/15.88 sQ85_spl|sQ86_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1064,f1086,f1089])).
% 0.14/15.88 fof(f1093,plain,(
% 0.14/15.88 $false|sQ79_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1067,f596])).
% 0.14/15.88 fof(f1094,plain,(
% 0.14/15.88 sQ79_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.14/15.88 fof(f1095,plain,(
% 0.14/15.88 $false|~sQ85_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1087,f222])).
% 0.14/15.88 fof(f1096,plain,(
% 0.14/15.88 ~sQ85_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1095])).
% 0.14/15.88 fof(f1101,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK0_skl)))|in(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f779,f521])).
% 0.14/15.88 fof(f1102,definition,(
% 0.14/15.88 sQ87_spl <=> (one_sorted_str(sK0_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1104,plain,(
% 0.14/15.88 ~one_sorted_str(sK0_skl)|sQ87_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1102])).
% 0.14/15.88 fof(f1123,definition,(
% 0.14/15.88 sQ93_spl <=> (empty(powerset(the_carrier(sK0_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1124,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK0_skl)))|~sQ93_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1123])).
% 0.14/15.88 fof(f1126,definition,(
% 0.14/15.88 sQ94_spl <=> (in(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1129,plain,(
% 0.14/15.88 sQ93_spl|sQ94_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1101,f1123,f1126])).
% 0.14/15.88 fof(f1130,plain,(
% 0.14/15.88 $false|~sQ93_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1124,f222])).
% 0.14/15.88 fof(f1131,plain,(
% 0.14/15.88 ~sQ93_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1130])).
% 0.14/15.88 fof(f1132,plain,(
% 0.14/15.88 $false|sQ87_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1104,f562])).
% 0.14/15.88 fof(f1133,plain,(
% 0.14/15.88 sQ87_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1132])).
% 0.14/15.88 fof(f1147,plain,(
% 0.14/15.88 empty(cast_as_carrier_subset(sK34_skl))|~sQ44_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f813,f858])).
% 0.14/15.88 fof(f1160,plain,(
% 0.14/15.88 ~one_sorted_str(sK10_skl)|rel_str(sK2_skl(sK10_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f845,f193])).
% 0.14/15.88 fof(f1163,definition,(
% 0.14/15.88 sQ95_spl <=> (rel_str(sK2_skl(sK10_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1166,plain,(
% 0.14/15.88 ~sQ71_spl|sQ95_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1160,f1028,f1163])).
% 0.14/15.88 fof(f1178,plain,(
% 0.14/15.88 ~one_sorted_str(sK9_skl)|rel_str(sK2_skl(sK9_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f846,f193])).
% 0.14/15.88 fof(f1181,definition,(
% 0.14/15.88 sQ99_spl <=> (rel_str(sK2_skl(sK9_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1184,plain,(
% 0.14/15.88 ~sQ79_spl|sQ99_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1178,f1065,f1181])).
% 0.14/15.88 fof(f1196,plain,(
% 0.14/15.88 ~one_sorted_str(sK0_skl)|rel_str(sK2_skl(sK0_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f848,f193])).
% 0.14/15.88 fof(f1199,definition,(
% 0.14/15.88 sQ103_spl <=> (rel_str(sK2_skl(sK0_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1202,plain,(
% 0.14/15.88 ~sQ87_spl|sQ103_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1196,f1102,f1199])).
% 0.14/15.88 fof(f1214,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|upper_relstr_subset(cast_as_carrier_subset(sK12_skl),sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f367,f219])).
% 0.14/15.88 fof(f1215,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|lower_relstr_subset(cast_as_carrier_subset(sK12_skl),sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f367,f218])).
% 0.14/15.88 fof(f1217,plain,(
% 0.14/15.88 one_sorted_str(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f367,f191])).
% 0.14/15.88 fof(f1218,definition,(
% 0.14/15.88 sQ107_spl <=> (empty_carrier(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1219,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|~sQ107_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1218])).
% 0.14/15.88 fof(f1221,definition,(
% 0.14/15.88 sQ108_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK12_skl),sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1224,plain,(
% 0.14/15.88 sQ107_spl|sQ108_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1214,f1218,f1221])).
% 0.14/15.88 fof(f1225,definition,(
% 0.14/15.88 sQ109_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK12_skl),sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1228,plain,(
% 0.14/15.88 sQ107_spl|sQ109_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1215,f1218,f1225])).
% 0.14/15.88 fof(f1229,plain,(
% 0.14/15.88 $false|~sQ107_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1219,f368])).
% 0.14/15.88 fof(f1230,plain,(
% 0.14/15.88 ~sQ107_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1229])).
% 0.14/15.88 fof(f1231,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|sK12_skl=rel_str_of(the_carrier(sK12_skl),the_InternalRel(sK12_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f369,f104])).
% 0.14/15.88 fof(f1232,definition,(
% 0.14/15.88 sQ110_spl <=> (rel_str(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1234,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|sQ110_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1232])).
% 0.14/15.88 fof(f1235,definition,(
% 0.14/15.88 sQ111_spl <=> (sK12_skl=rel_str_of(the_carrier(sK12_skl),the_InternalRel(sK12_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1238,plain,(
% 0.14/15.88 ~sQ110_spl|sQ111_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1231,f1232,f1235])).
% 0.14/15.88 fof(f1239,plain,(
% 0.14/15.88 $false|sQ110_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1234,f367])).
% 0.14/15.88 fof(f1240,plain,(
% 0.14/15.88 sQ110_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1239])).
% 0.14/15.88 fof(f1247,plain,(
% 0.14/15.88 ~rel_str(sK10_skl)|directed_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f246,f355])).
% 0.14/15.88 fof(f1249,definition,(
% 0.14/15.88 sQ112_spl <=> (directed_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1252,plain,(
% 0.14/15.88 ~sQ37_spl|sQ112_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1247,f752,f1249])).
% 0.14/15.88 fof(f1261,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|~sQ44_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f1147,f243])).
% 0.14/15.88 fof(f1272,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|~sQ44_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1261,f573,f566,f812])).
% 0.14/15.88 fof(f1274,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))|~one_sorted_str(boole_POSet(cast_as_carrier_subset(sK34_skl)))|empty_carrier(X0)|~net_str(X0,boole_POSet(cast_as_carrier_subset(sK34_skl)))|in(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),a_2_1_yellow19(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0))|~is_eventually_in(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|~sQ52_spl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f874,f561])).
% 0.14/15.88 fof(f1275,plain,(
% 0.14/15.88 ~finite(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))|finite(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|~sQ52_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f874,f152])).
% 0.14/15.88 fof(f1276,plain,(
% 0.14/15.88 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|~empty(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))|~sQ52_spl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f874,f536])).
% 0.14/15.88 fof(f1278,plain,(
% 0.14/15.88 empty(powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|in(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl)))))|~sQ52_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f874,f521])).
% 0.14/15.88 fof(f1279,definition,(
% 0.14/15.88 ![X0]: (sQ115_spl <=> (empty_carrier(X0)|~net_str(X0,boole_POSet(cast_as_carrier_subset(sK34_skl)))|in(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),a_2_1_yellow19(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0))|~is_eventually_in(boole_POSet(cast_as_carrier_subset(sK34_skl)),X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1282,plain,(
% 0.14/15.88 sQ9_spl|~sQ10_spl|sQ115_spl|~sQ52_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1274,f601,f604,f1279,f873])).
% 0.14/15.88 fof(f1283,definition,(
% 0.14/15.88 sQ116_spl <=> (finite(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1286,plain,(
% 0.14/15.88 ~sQ16_spl|sQ116_spl|~sQ52_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1275,f636,f1283,f873])).
% 0.14/15.88 fof(f1287,definition,(
% 0.14/15.88 ![X0]: (sQ117_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1290,plain,(
% 0.14/15.88 sQ117_spl|~sQ15_spl|~sQ52_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1276,f1287,f626,f873])).
% 0.14/15.88 fof(f1291,definition,(
% 0.14/15.88 sQ118_spl <=> (in(filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)),powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK34_skl))))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1294,plain,(
% 0.14/15.88 sQ12_spl|sQ118_spl|~sQ52_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1278,f611,f1291,f873])).
% 0.14/15.88 fof(f1295,plain,(
% 0.14/15.88 net_str(sK2_skl(sK12_skl),sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f1217,f204])).
% 0.14/15.88 fof(f1296,plain,(
% 0.14/15.88 element(cast_as_carrier_subset(sK12_skl),powerset(the_carrier(sK12_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1217,f184])).
% 0.14/15.88 fof(f1306,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|~with_suprema_relstr(sK12_skl)|~up_complete_relstr(sK12_skl)|upper_bounded_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f370,f177])).
% 0.14/15.88 fof(f1307,definition,(
% 0.14/15.88 sQ119_spl <=> (with_suprema_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1310,definition,(
% 0.14/15.88 sQ120_spl <=> (up_complete_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1313,definition,(
% 0.14/15.88 sQ121_spl <=> (upper_bounded_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1316,plain,(
% 0.14/15.88 ~sQ110_spl|~sQ119_spl|~sQ120_spl|sQ121_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1306,f1232,f1307,f1310,f1313])).
% 0.14/15.88 fof(f1318,definition,(
% 0.14/15.88 sQ122_spl <=> (reflexive_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1320,plain,(
% 0.14/15.88 ~reflexive_relstr(sK12_skl)|sQ122_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1318])).
% 0.14/15.88 fof(f1321,definition,(
% 0.14/15.88 sQ123_spl <=> (join_complete_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1324,definition,(
% 0.14/15.88 sQ124_spl <=> (with_infima_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1328,plain,(
% 0.14/15.88 $false|sQ122_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1320,f370])).
% 0.14/15.88 fof(f1329,plain,(
% 0.14/15.88 sQ122_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1328])).
% 0.14/15.88 fof(f1331,plain,(
% 0.14/15.88 ~rel_str(sK10_skl)|filtered_subset(cast_as_carrier_subset(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f278,f356])).
% 0.14/15.88 fof(f1333,definition,(
% 0.14/15.88 sQ125_spl <=> (filtered_subset(cast_as_carrier_subset(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1336,plain,(
% 0.14/15.88 ~sQ37_spl|sQ125_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1331,f752,f1333])).
% 0.14/15.88 fof(f1342,plain,(
% 0.14/15.88 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|element(sK6_skl(sK4_skl(a_2_1_yellow19(X0,X1)),X1,X0),powerset(the_carrier(X0)))|empty(a_2_1_yellow19(X0,X1)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f320,f858])).
% 0.14/15.88 fof(f1343,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|~net_str(sK2_skl(sK34_skl),sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|element(sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl),powerset(the_carrier(sK34_skl)))|~sQ53_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f878,f320])).
% 0.14/15.88 fof(f1344,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK35_skl)|~net_str(sK35_skl,sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|element(sK6_skl(X0,sK35_skl,sK34_skl),powerset(the_carrier(sK34_skl)))|~sQ8_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f584,f320])).
% 0.14/15.88 fof(f1345,definition,(
% 0.14/15.88 sQ126_spl <=> (net_str(sK2_skl(sK34_skl),sK34_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1347,plain,(
% 0.14/15.88 ~net_str(sK2_skl(sK34_skl),sK34_skl)|sQ126_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1345])).
% 0.14/15.88 fof(f1348,definition,(
% 0.14/15.88 ![X0]: (sQ127_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|element(sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl),powerset(the_carrier(sK34_skl)))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1351,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|~sQ126_spl|sQ127_spl|~sQ53_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1343,f573,f566,f870,f1345,f1348,f877])).
% 0.14/15.88 fof(f1352,definition,(
% 0.14/15.88 ![X0]: (sQ128_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|element(sK6_skl(X0,sK35_skl,sK34_skl),powerset(the_carrier(sK34_skl)))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1353,plain,(
% 0.14/15.88 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|element(sK6_skl(X0,sK35_skl,sK34_skl),powerset(the_carrier(sK34_skl)))|~sQ128_spl)),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1352])).
% 0.14/15.88 fof(f1355,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ6_spl|~sQ35_spl|sQ128_spl|~sQ8_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1344,f573,f566,f576,f734,f1352,f583])).
% 0.14/15.88 fof(f1356,plain,(
% 0.14/15.88 $false|sQ126_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1347,f850])).
% 0.14/15.88 fof(f1357,plain,(
% 0.14/15.88 sQ126_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1356])).
% 0.14/15.88 fof(f1358,plain,(
% 0.14/15.88 element(sK4_skl(cast_as_carrier_subset(sK34_skl)),the_carrier(sK34_skl))|empty(cast_as_carrier_subset(sK34_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f802,f858])).
% 0.14/15.88 fof(f1359,definition,(
% 0.14/15.88 sQ129_spl <=> (element(sK4_skl(cast_as_carrier_subset(sK34_skl)),the_carrier(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1362,definition,(
% 0.14/15.88 sQ130_spl <=> (empty(cast_as_carrier_subset(sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1363,plain,(
% 0.14/15.88 empty(cast_as_carrier_subset(sK34_skl))|~sQ130_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1362])).
% 0.14/15.88 fof(f1365,plain,(
% 0.14/15.88 sQ129_spl|sQ130_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1358,f1359,f1362])).
% 0.14/15.88 fof(f1368,plain,(
% 0.14/15.88 ~one_sorted_str(sK12_skl)|rel_str(sK2_skl(sK12_skl))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1295,f193])).
% 0.14/15.88 fof(f1371,definition,(
% 0.14/15.88 sQ131_spl <=> (one_sorted_str(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1373,plain,(
% 0.14/15.88 ~one_sorted_str(sK12_skl)|sQ131_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1371])).
% 0.14/15.88 fof(f1374,definition,(
% 0.14/15.88 sQ132_spl <=> (rel_str(sK2_skl(sK12_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1377,plain,(
% 0.14/15.88 ~sQ131_spl|sQ132_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1368,f1371,f1374])).
% 0.14/15.88 fof(f1389,plain,(
% 0.14/15.88 $false|sQ131_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1373,f1217])).
% 0.14/15.88 fof(f1390,plain,(
% 0.14/15.88 sQ131_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1389])).
% 0.14/15.88 fof(f1391,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK12_skl)|~one_sorted_str(sK12_skl)|empty_carrier(X0)|~net_str(X0,sK12_skl)|in(cast_as_carrier_subset(sK12_skl),a_2_1_yellow19(sK12_skl,X0))|~is_eventually_in(sK12_skl,X0,cast_as_carrier_subset(sK12_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1296,f561])).
% 0.14/15.88 fof(f1395,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK12_skl)))|in(cast_as_carrier_subset(sK12_skl),powerset(the_carrier(sK12_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1296,f521])).
% 0.14/15.88 fof(f1396,definition,(
% 0.14/15.88 ![X0]: (sQ136_spl <=> (empty_carrier(X0)|~net_str(X0,sK12_skl)|in(cast_as_carrier_subset(sK12_skl),a_2_1_yellow19(sK12_skl,X0))|~is_eventually_in(sK12_skl,X0,cast_as_carrier_subset(sK12_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1399,plain,(
% 0.14/15.88 sQ107_spl|~sQ131_spl|sQ136_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1391,f1218,f1371,f1396])).
% 0.14/15.88 fof(f1414,definition,(
% 0.14/15.88 sQ141_spl <=> (empty(powerset(the_carrier(sK12_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1415,plain,(
% 0.14/15.88 empty(powerset(the_carrier(sK12_skl)))|~sQ141_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1414])).
% 0.14/15.88 fof(f1417,definition,(
% 0.14/15.88 sQ142_spl <=> (in(cast_as_carrier_subset(sK12_skl),powerset(the_carrier(sK12_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1420,plain,(
% 0.14/15.88 sQ141_spl|sQ142_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1395,f1414,f1417])).
% 0.14/15.88 fof(f1421,plain,(
% 0.14/15.88 $false|~sQ141_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1415,f222])).
% 0.14/15.88 fof(f1422,plain,(
% 0.14/15.88 ~sQ141_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1421])).
% 0.14/15.88 fof(f1428,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|element(sK6_skl(sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))),sK2_skl(sK34_skl),sK34_skl),powerset(the_carrier(sK34_skl)))|empty(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1342,f850])).
% 0.14/15.88 fof(f1459,definition,(
% 0.14/15.88 sQ151_spl <=> (element(sK6_skl(sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))),sK2_skl(sK34_skl),sK34_skl),powerset(the_carrier(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1462,definition,(
% 0.14/15.88 sQ152_spl <=> (empty(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1465,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|sQ151_spl|sQ152_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1428,f573,f566,f870,f1459,f1462])).
% 0.14/15.88 fof(f1488,plain,(
% 0.14/15.88 element(sK6_skl(sK36_skl,sK35_skl,sK34_skl),powerset(the_carrier(sK34_skl)))|~sQ128_spl|~sQ0_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f1353,f546])).
% 0.14/15.88 fof(f1494,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|empty_carrier(sK12_skl)|bounded_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f373,f163])).
% 0.14/15.88 fof(f1495,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|empty_carrier(sK12_skl)|with_infima_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f373,f150])).
% 0.14/15.88 fof(f1496,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|empty_carrier(sK12_skl)|with_suprema_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f373,f149])).
% 0.14/15.88 fof(f1497,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|empty_carrier(sK12_skl)|~reflexive_relstr(sK12_skl)|join_complete_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f373,f111])).
% 0.14/15.88 fof(f1498,plain,(
% 0.14/15.88 ~rel_str(sK12_skl)|empty_carrier(sK12_skl)|~reflexive_relstr(sK12_skl)|up_complete_relstr(sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f373,f110])).
% 0.14/15.88 fof(f1499,definition,(
% 0.14/15.88 sQ156_spl <=> (bounded_relstr(sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1502,plain,(
% 0.14/15.88 ~sQ110_spl|sQ107_spl|sQ156_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1494,f1232,f1218,f1499])).
% 0.14/15.88 fof(f1503,plain,(
% 0.14/15.88 ~sQ110_spl|sQ107_spl|sQ124_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1495,f1232,f1218,f1324])).
% 0.14/15.88 fof(f1504,plain,(
% 0.14/15.88 ~sQ110_spl|sQ107_spl|sQ119_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1496,f1232,f1218,f1307])).
% 0.14/15.88 fof(f1505,plain,(
% 0.14/15.88 ~sQ110_spl|sQ107_spl|~sQ122_spl|sQ123_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1497,f1232,f1218,f1318,f1321])).
% 0.14/15.88 fof(f1506,plain,(
% 0.14/15.88 ~sQ110_spl|sQ107_spl|~sQ122_spl|sQ120_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1498,f1232,f1218,f1318,f1310])).
% 0.14/15.88 fof(f1510,plain,(
% 0.14/15.88 ![X0,X1]: (empty_carrier(X0)|~one_sorted_str(X0)|empty_carrier(X1)|~net_str(X1,X0)|sK4_skl(a_2_1_yellow19(X0,X1))=sK6_skl(sK4_skl(a_2_1_yellow19(X0,X1)),X1,X0)|empty(a_2_1_yellow19(X0,X1)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f321,f858])).
% 0.14/15.88 fof(f1511,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|~net_str(sK2_skl(sK34_skl),sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|X0=sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl)|~sQ53_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f878,f321])).
% 0.14/15.88 fof(f1512,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK35_skl)|~net_str(sK35_skl,sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|X0=sK6_skl(X0,sK35_skl,sK34_skl)|~sQ8_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f584,f321])).
% 0.14/15.88 fof(f1513,definition,(
% 0.14/15.88 ![X0]: (sQ157_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|X0=sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1516,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|~sQ126_spl|sQ157_spl|~sQ53_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1511,f573,f566,f870,f1345,f1513,f877])).
% 0.14/15.88 fof(f1517,definition,(
% 0.14/15.88 ![X0]: (sQ158_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|X0=sK6_skl(X0,sK35_skl,sK34_skl)))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1518,plain,(
% 0.14/15.88 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|X0=sK6_skl(X0,sK35_skl,sK34_skl)|~sQ158_spl)),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1517])).
% 0.14/15.88 fof(f1520,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ6_spl|~sQ35_spl|sQ158_spl|~sQ8_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1512,f573,f566,f576,f734,f1517,f583])).
% 0.14/15.88 fof(f1522,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|~net_str(sK2_skl(sK34_skl),sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|is_eventually_in(sK34_skl,sK2_skl(sK34_skl),sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl))|~sQ53_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f878,f322])).
% 0.14/15.88 fof(f1523,plain,(
% 0.14/15.88 ![X0]: (empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK35_skl)|~net_str(sK35_skl,sK34_skl)|~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|is_eventually_in(sK34_skl,sK35_skl,sK6_skl(X0,sK35_skl,sK34_skl))|~sQ8_spl)),
% 0.14/15.88 inference(paramodulation,[status(thm)],[f584,f322])).
% 0.14/15.88 fof(f1524,definition,(
% 0.14/15.88 ![X0]: (sQ159_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK2_skl(sK34_skl)))|is_eventually_in(sK34_skl,sK2_skl(sK34_skl),sK6_skl(X0,sK2_skl(sK34_skl),sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1527,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|~sQ126_spl|sQ159_spl|~sQ53_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1522,f573,f566,f870,f1345,f1524,f877])).
% 0.14/15.88 fof(f1528,definition,(
% 0.14/15.88 ![X0]: (sQ160_spl <=> (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|is_eventually_in(sK34_skl,sK35_skl,sK6_skl(X0,sK35_skl,sK34_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1529,plain,(
% 0.14/15.88 ![X0]: (~in(X0,filter_of_net_str(sK34_skl,sK35_skl))|is_eventually_in(sK34_skl,sK35_skl,sK6_skl(X0,sK35_skl,sK34_skl))|~sQ160_spl)),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1528])).
% 0.14/15.88 fof(f1531,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ6_spl|~sQ35_spl|sQ160_spl|~sQ8_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1523,f573,f566,f576,f734,f1528,f583])).
% 0.14/15.88 fof(f1534,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|~reflexive_relstr(sK12_skl)|~rel_str(sK12_skl)|element(sK7_skl(sK12_skl),powerset(the_carrier(sK12_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f329,f371])).
% 0.14/15.88 fof(f1536,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|element(sK7_skl(sK10_skl),powerset(the_carrier(sK10_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f329,f353])).
% 0.14/15.88 fof(f1537,plain,(
% 0.14/15.88 empty_carrier(sK9_skl)|~reflexive_relstr(sK9_skl)|~rel_str(sK9_skl)|element(sK7_skl(sK9_skl),powerset(the_carrier(sK9_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f329,f345])).
% 0.14/15.88 fof(f1538,definition,(
% 0.14/15.88 sQ161_spl <=> (element(sK7_skl(sK12_skl),powerset(the_carrier(sK12_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1541,plain,(
% 0.14/15.88 sQ107_spl|~sQ122_spl|~sQ110_spl|sQ161_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1534,f1218,f1318,f1232,f1538])).
% 0.14/15.88 fof(f1543,definition,(
% 0.14/15.88 sQ162_spl <=> (element(sK7_skl(sK10_skl),powerset(the_carrier(sK10_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1546,plain,(
% 0.14/15.88 sQ46_spl|~sQ47_spl|~sQ37_spl|sQ162_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1536,f821,f824,f752,f1543])).
% 0.14/15.88 fof(f1547,definition,(
% 0.14/15.88 sQ163_spl <=> (element(sK7_skl(sK9_skl),powerset(the_carrier(sK9_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1550,plain,(
% 0.14/15.88 sQ20_spl|~sQ21_spl|~sQ19_spl|sQ163_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1537,f656,f659,f653,f1547])).
% 0.14/15.88 fof(f1553,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|~sQ130_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f1363,f243])).
% 0.14/15.88 fof(f1563,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|~sQ130_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1553,f573,f566,f1362])).
% 0.14/15.88 fof(f1565,plain,(
% 0.14/15.88 sK36_skl=sK6_skl(sK36_skl,sK35_skl,sK34_skl)|~sQ158_spl|~sQ0_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f1518,f546])).
% 0.14/15.88 fof(f1567,plain,(
% 0.14/15.88 element(sK36_skl,powerset(the_carrier(sK34_skl)))|~sQ158_spl|~sQ128_spl|~sQ0_spl),
% 0.14/15.88 inference(backward_demodulation,[status(thm)],[f1565,f1488])).
% 0.14/15.88 fof(f1572,plain,(
% 0.14/15.88 sQ2_spl|~sQ158_spl|~sQ128_spl|~sQ0_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1567,f552,f1517,f1352,f545])).
% 0.14/15.88 fof(f1591,plain,(
% 0.14/15.88 empty_carrier(sK34_skl)|~one_sorted_str(sK34_skl)|empty_carrier(sK2_skl(sK34_skl))|sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl)))=sK6_skl(sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))),sK2_skl(sK34_skl),sK34_skl)|empty(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f1510,f850])).
% 0.14/15.88 fof(f1610,definition,(
% 0.14/15.88 sQ170_spl <=> (sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl)))=sK6_skl(sK4_skl(a_2_1_yellow19(sK34_skl,sK2_skl(sK34_skl))),sK2_skl(sK34_skl),sK34_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1613,plain,(
% 0.14/15.88 sQ5_spl|~sQ3_spl|sQ51_spl|sQ170_spl|sQ152_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1591,f573,f566,f870,f1610,f1462])).
% 0.14/15.88 fof(f1635,plain,(
% 0.14/15.88 empty_carrier(sK16_skl)|upper_relstr_subset(cast_as_carrier_subset(sK16_skl),sK16_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f387,f219])).
% 0.14/15.88 fof(f1636,plain,(
% 0.14/15.88 empty_carrier(sK16_skl)|lower_relstr_subset(cast_as_carrier_subset(sK16_skl),sK16_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f387,f218])).
% 0.14/15.88 fof(f1639,definition,(
% 0.14/15.88 sQ172_spl <=> (empty_carrier(sK16_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1640,plain,(
% 0.14/15.88 empty_carrier(sK16_skl)|~sQ172_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1639])).
% 0.14/15.88 fof(f1642,definition,(
% 0.14/15.88 sQ173_spl <=> (upper_relstr_subset(cast_as_carrier_subset(sK16_skl),sK16_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1645,plain,(
% 0.14/15.88 sQ172_spl|sQ173_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1635,f1639,f1642])).
% 0.14/15.88 fof(f1646,definition,(
% 0.14/15.88 sQ174_spl <=> (lower_relstr_subset(cast_as_carrier_subset(sK16_skl),sK16_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1649,plain,(
% 0.14/15.88 sQ172_spl|sQ174_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1636,f1639,f1646])).
% 0.14/15.88 fof(f1650,plain,(
% 0.14/15.88 $false|~sQ172_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1640,f388])).
% 0.14/15.88 fof(f1651,plain,(
% 0.14/15.88 ~sQ172_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1650])).
% 0.14/15.88 fof(f1652,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|~reflexive_relstr(sK12_skl)|~rel_str(sK12_skl)|filtered_subset(sK7_skl(sK12_skl),sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f331,f371])).
% 0.14/15.88 fof(f1654,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|filtered_subset(sK7_skl(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f331,f353])).
% 0.14/15.88 fof(f1655,plain,(
% 0.14/15.88 empty_carrier(sK9_skl)|~reflexive_relstr(sK9_skl)|~rel_str(sK9_skl)|filtered_subset(sK7_skl(sK9_skl),sK9_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f331,f345])).
% 0.14/15.88 fof(f1656,definition,(
% 0.14/15.88 sQ175_spl <=> (filtered_subset(sK7_skl(sK12_skl),sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1659,plain,(
% 0.14/15.88 sQ107_spl|~sQ122_spl|~sQ110_spl|sQ175_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1652,f1218,f1318,f1232,f1656])).
% 0.14/15.88 fof(f1661,definition,(
% 0.14/15.88 sQ176_spl <=> (filtered_subset(sK7_skl(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1664,plain,(
% 0.14/15.88 sQ46_spl|~sQ47_spl|~sQ37_spl|sQ176_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1654,f821,f824,f752,f1661])).
% 0.14/15.88 fof(f1665,definition,(
% 0.14/15.88 sQ177_spl <=> (filtered_subset(sK7_skl(sK9_skl),sK9_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1668,plain,(
% 0.14/15.88 sQ20_spl|~sQ21_spl|~sQ19_spl|sQ177_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1655,f656,f659,f653,f1665])).
% 0.14/15.88 fof(f1669,plain,(
% 0.14/15.88 empty_carrier(sK12_skl)|~reflexive_relstr(sK12_skl)|~rel_str(sK12_skl)|upper_relstr_subset(sK7_skl(sK12_skl),sK12_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f332,f371])).
% 0.14/15.88 fof(f1671,plain,(
% 0.14/15.88 empty_carrier(sK10_skl)|~reflexive_relstr(sK10_skl)|~rel_str(sK10_skl)|upper_relstr_subset(sK7_skl(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f332,f353])).
% 0.14/15.88 fof(f1672,plain,(
% 0.14/15.88 empty_carrier(sK9_skl)|~reflexive_relstr(sK9_skl)|~rel_str(sK9_skl)|upper_relstr_subset(sK7_skl(sK9_skl),sK9_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f332,f345])).
% 0.14/15.88 fof(f1673,definition,(
% 0.14/15.88 sQ178_spl <=> (upper_relstr_subset(sK7_skl(sK12_skl),sK12_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1676,plain,(
% 0.14/15.88 sQ107_spl|~sQ122_spl|~sQ110_spl|sQ178_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1669,f1218,f1318,f1232,f1673])).
% 0.14/15.88 fof(f1678,definition,(
% 0.14/15.88 sQ179_spl <=> (upper_relstr_subset(sK7_skl(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1681,plain,(
% 0.14/15.88 sQ46_spl|~sQ47_spl|~sQ37_spl|sQ179_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1671,f821,f824,f752,f1678])).
% 0.14/15.88 fof(f1682,definition,(
% 0.14/15.88 sQ180_spl <=> (upper_relstr_subset(sK7_skl(sK9_skl),sK9_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1685,plain,(
% 0.14/15.88 sQ20_spl|~sQ21_spl|~sQ19_spl|sQ180_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1672,f656,f659,f653,f1682])).
% 0.14/15.88 fof(f1687,plain,(
% 0.14/15.88 ~reflexive_relstr(sK10_skl)|~transitive_relstr(sK10_skl)|~antisymmetric_relstr(sK10_skl)|~with_suprema_relstr(sK10_skl)|~rel_str(sK10_skl)|element(sK8_skl(sK10_skl),powerset(the_carrier(sK10_skl)))),
% 0.14/15.88 inference(resolution,[status(thm)],[f335,f356])).
% 0.14/15.88 fof(f1689,definition,(
% 0.14/15.88 sQ181_spl <=> (transitive_relstr(sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1691,plain,(
% 0.14/15.88 ~transitive_relstr(sK10_skl)|sQ181_spl),
% 0.14/15.88 inference(component_clause,[status(thm)],[f1689])).
% 0.14/15.88 fof(f1692,definition,(
% 0.14/15.88 sQ182_spl <=> (element(sK8_skl(sK10_skl),powerset(the_carrier(sK10_skl))))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1695,plain,(
% 0.14/15.88 ~sQ47_spl|~sQ181_spl|~sQ70_spl|~sQ39_spl|~sQ37_spl|sQ182_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1687,f824,f1689,f1001,f762,f752,f1692])).
% 0.14/15.88 fof(f1696,plain,(
% 0.14/15.88 $false|sQ70_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1003,f354])).
% 0.14/15.88 fof(f1697,plain,(
% 0.14/15.88 sQ70_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1696])).
% 0.14/15.88 fof(f1698,plain,(
% 0.14/15.88 $false|sQ181_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1691,f353])).
% 0.14/15.88 fof(f1699,plain,(
% 0.14/15.88 sQ181_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1698])).
% 0.14/15.88 fof(f1701,plain,(
% 0.14/15.88 ~reflexive_relstr(sK10_skl)|~transitive_relstr(sK10_skl)|~antisymmetric_relstr(sK10_skl)|~with_suprema_relstr(sK10_skl)|~rel_str(sK10_skl)|directed_subset(sK8_skl(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f337,f356])).
% 0.14/15.88 fof(f1703,definition,(
% 0.14/15.88 sQ183_spl <=> (directed_subset(sK8_skl(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1706,plain,(
% 0.14/15.88 ~sQ47_spl|~sQ181_spl|~sQ70_spl|~sQ39_spl|~sQ37_spl|sQ183_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1701,f824,f1689,f1001,f762,f752,f1703])).
% 0.14/15.88 fof(f1708,plain,(
% 0.14/15.88 ~reflexive_relstr(sK10_skl)|~transitive_relstr(sK10_skl)|~antisymmetric_relstr(sK10_skl)|~with_suprema_relstr(sK10_skl)|~rel_str(sK10_skl)|filtered_subset(sK8_skl(sK10_skl),sK10_skl)),
% 0.14/15.88 inference(resolution,[status(thm)],[f338,f356])).
% 0.14/15.88 fof(f1710,definition,(
% 0.14/15.88 sQ184_spl <=> (filtered_subset(sK8_skl(sK10_skl),sK10_skl))),
% 0.14/15.88 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 0.14/15.88 fof(f1713,plain,(
% 0.14/15.88 ~sQ47_spl|~sQ181_spl|~sQ70_spl|~sQ39_spl|~sQ37_spl|sQ184_spl),
% 0.14/15.88 inference(split_clause,[status(thm)],[f1708,f824,f1689,f1001,f762,f752,f1710])).
% 0.14/15.88 fof(f1714,plain,(
% 0.14/15.88 is_eventually_in(sK34_skl,sK35_skl,sK6_skl(sK36_skl,sK35_skl,sK34_skl))|~sQ160_spl|~sQ0_spl),
% 0.14/15.88 inference(resolution,[status(thm)],[f1529,f546])).
% 0.14/15.88 fof(f1716,plain,(
% 0.14/15.88 is_eventually_in(sK34_skl,sK35_skl,sK36_skl)|~sQ158_spl|~sQ160_spl|~sQ0_spl),
% 0.14/15.88 inference(forward_demodulation,[status(thm)],[f1565,f1714])).
% 0.14/15.88 fof(f1717,plain,(
% 0.14/15.88 $false|sQ1_spl|~sQ158_spl|~sQ160_spl|~sQ0_spl),
% 0.14/15.88 inference(forward_subsumption_resolution,[status(thm)],[f1716,f550])).
% 0.14/15.88 fof(f1718,plain,(
% 0.14/15.88 sQ1_spl|~sQ158_spl|~sQ160_spl|~sQ0_spl),
% 0.14/15.88 inference(contradiction_clause,[status(thm)],[f1717])).
% 0.14/15.88 fof(f1719,plain,(
% 0.14/15.88 $false),
% 0.14/15.88 inference(sat_refutation,[status(thm)],[f551,f555,f556,f572,f582,f586,f588,f590,f592,f610,f617,f619,f629,f631,f642,f670,f672,f674,f709,f732,f740,f742,f747,f758,f760,f773,f775,f786,f807,f815,f819,f835,f837,f839,f869,f876,f880,f887,f891,f907,f921,f922,f937,f942,f946,f950,f967,f972,f976,f980,f1006,f1009,f1034,f1055,f1057,f1059,f1071,f1092,f1094,f1096,f1129,f1131,f1133,f1166,f1184,f1202,f1224,f1228,f1230,f1238,f1240,f1252,f1272,f1282,f1286,f1290,f1294,f1316,f1329,f1336,f1351,f1355,f1357,f1365,f1377,f1390,f1399,f1420,f1422,f1465,f1502,f1503,f1504,f1505,f1506,f1516,f1520,f1527,f1531,f1541,f1546,f1550,f1563,f1572,f1613,f1645,f1649,f1651,f1659,f1664,f1668,f1676,f1681,f1685,f1695,f1697,f1699,f1706,f1713,f1718])).
% 0.14/15.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/15.88 % Elapsed time: 0.080893 seconds
% 0.14/15.88 % CPU time: 0.379912 seconds
% 0.14/15.88 % Total memory used: 99.094 MB
% 0.14/15.88 % Net memory used: 98.803 MB
%------------------------------------------------------------------------------