%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU394+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:27:47 AM UTC 2025
% Result : Theorem 1.89s 2.10s
% Output : Proof 1.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU394+1 : TPTP v9.0.0. Released v3.3.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n014.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 07:01:24 EDT 2025
% 0.11/0.32 % CPUTime :
% 1.89/2.10 % SZS status Theorem
% 1.89/2.10 % SZS output start Proof
% 1.89/2.10 tff(filter_of_net_str_type, type, (
% 1.89/2.10 filter_of_net_str: ( $i * $i ) > $i)).
% 1.89/2.10 tff(net_of_bool_filter_type, type, (
% 1.89/2.10 net_of_bool_filter: ( $i * $i * $i ) > $i)).
% 1.89/2.10 tff(tptp_fun_B_36_type, type, (
% 1.89/2.10 tptp_fun_B_36: $i)).
% 1.89/2.10 tff(cast_as_carrier_subset_type, type, (
% 1.89/2.10 cast_as_carrier_subset: $i > $i)).
% 1.89/2.10 tff(tptp_fun_A_35_type, type, (
% 1.89/2.10 tptp_fun_A_35: $i)).
% 1.89/2.10 tff(set_difference_type, type, (
% 1.89/2.10 set_difference: ( $i * $i ) > $i)).
% 1.89/2.10 tff(singleton_type, type, (
% 1.89/2.10 singleton: $i > $i)).
% 1.89/2.10 tff(empty_set_type, type, (
% 1.89/2.10 empty_set: $i)).
% 1.89/2.10 tff(element_type, type, (
% 1.89/2.10 element: ( $i * $i ) > $o)).
% 1.89/2.10 tff(powerset_type, type, (
% 1.89/2.10 powerset: $i > $i)).
% 1.89/2.10 tff(the_carrier_type, type, (
% 1.89/2.10 the_carrier: $i > $i)).
% 1.89/2.10 tff(boole_POSet_type, type, (
% 1.89/2.10 boole_POSet: $i > $i)).
% 1.89/2.10 tff(upper_relstr_subset_type, type, (
% 1.89/2.10 upper_relstr_subset: ( $i * $i ) > $o)).
% 1.89/2.10 tff(filtered_subset_type, type, (
% 1.89/2.10 filtered_subset: ( $i * $i ) > $o)).
% 1.89/2.10 tff(empty_type, type, (
% 1.89/2.10 empty: $i > $o)).
% 1.89/2.10 tff(one_sorted_str_type, type, (
% 1.89/2.10 one_sorted_str: $i > $o)).
% 1.89/2.10 tff(proper_element_type, type, (
% 1.89/2.10 proper_element: ( $i * $i ) > $o)).
% 1.89/2.10 tff(empty_carrier_type, type, (
% 1.89/2.10 empty_carrier: $i > $o)).
% 1.89/2.10 tff(in_type, type, (
% 1.89/2.10 in: ( $i * $i ) > $o)).
% 1.89/2.10 tff(relation_type, type, (
% 1.89/2.10 relation: $i > $o)).
% 1.89/2.10 tff(relation_empty_yielding_type, type, (
% 1.89/2.10 relation_empty_yielding: $i > $o)).
% 1.89/2.10 tff(1,plain,
% 1.89/2.10 ((((~empty_carrier(A!35)) & one_sorted_str(A!35)) & (~((~((~empty(B!36)) & filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))) & element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))) | (B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36)))))) <=> ((~empty_carrier(A!35)) & one_sorted_str(A!35) & (~((~((~empty(B!36)) & filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))) & element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))) | (B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))))),
% 1.89/2.10 inference(rewrite,[status(thm)],[])).
% 1.89/2.10 tff(2,plain,
% 1.89/2.10 ((~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))) <=> (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))))),
% 1.89/2.10 inference(rewrite,[status(thm)],[])).
% 1.89/2.10 tff(3,plain,
% 1.89/2.10 ((~![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))) <=> (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))))),
% 1.89/2.10 inference(rewrite,[status(thm)],[])).
% 1.89/2.10 tff(4,axiom,(~![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t15_yellow19')).
% 1.89/2.10 tff(5,plain,
% 1.89/2.10 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.10 inference(modus_ponens,[status(thm)],[4, 3])).
% 1.89/2.10 tff(6,plain,
% 1.89/2.10 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.10 inference(modus_ponens,[status(thm)],[5, 2])).
% 1.89/2.10 tff(7,plain,
% 1.89/2.10 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.10 inference(modus_ponens,[status(thm)],[6, 2])).
% 1.89/2.10 tff(8,plain,
% 1.89/2.10 (~![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (B = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.10 inference(modus_ponens,[status(thm)],[7, 2])).
% 1.89/2.10 tff(9,plain,
% 1.89/2.10 ((~empty_carrier(A!35)) & one_sorted_str(A!35) & (~((~((~empty(B!36)) & filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))) & element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))) | (B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36)))))),
% 1.89/2.10 inference(modus_ponens,[status(thm)],[8, 1])).
% 1.89/2.10 tff(10,plain,
% 1.89/2.10 (one_sorted_str(A!35)),
% 1.89/2.10 inference(and_elim,[status(thm)],[9])).
% 1.89/2.10 tff(11,plain,
% 1.89/2.10 (~empty_carrier(A!35)),
% 1.89/2.10 inference(and_elim,[status(thm)],[9])).
% 1.89/2.10 tff(12,plain,
% 1.89/2.10 (^[A: $i] : refl((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))))),
% 1.89/2.10 inference(bind,[status(th)],[])).
% 1.89/2.10 tff(13,plain,
% 1.89/2.10 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.89/2.10 inference(quant_intro,[status(thm)],[12])).
% 1.89/2.10 tff(14,plain,
% 1.89/2.10 (^[A: $i] : rewrite((empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))))),
% 1.89/2.10 inference(bind,[status(th)],[])).
% 1.89/2.10 tff(15,plain,
% 1.89/2.10 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.89/2.10 inference(quant_intro,[status(thm)],[14])).
% 1.89/2.10 tff(16,plain,
% 1.89/2.10 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.89/2.10 inference(transitivity,[status(thm)],[15, 13])).
% 1.89/2.10 tff(17,plain,
% 1.89/2.10 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(A)) & one_sorted_str(A)) <=> (~(empty_carrier(A) | (~one_sorted_str(A))))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (~(~(empty_carrier(A) | (~one_sorted_str(A))))))), rewrite((~(~(empty_carrier(A) | (~one_sorted_str(A))))) <=> (empty_carrier(A) | (~one_sorted_str(A)))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (empty_carrier(A) | (~one_sorted_str(A))))), quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) <=> (~(empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))), ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) <=> (~(~(empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))))), rewrite((~(~(empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))) <=> (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))), ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) <=> (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))), (((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> ((empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), rewrite(((empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))), (((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))))), (![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))))), rewrite(((empty_carrier(A) | (~one_sorted_str(A))) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))), (((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))))),
% 1.89/2.11 inference(bind,[status(th)],[])).
% 1.89/2.11 tff(18,plain,
% 1.89/2.11 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.89/2.11 inference(quant_intro,[status(thm)],[17])).
% 1.89/2.11 tff(19,plain,
% 1.89/2.11 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.11 inference(rewrite,[status(thm)],[])).
% 1.89/2.11 tff(20,plain,
% 1.89/2.11 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))))), (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) <=> (((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))), rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))), (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))))), ((((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> (((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))), ((((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))))), (![B: $i] : (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))) <=> ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))))), rewrite((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), ((((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))))),
% 1.89/2.11 inference(bind,[status(th)],[])).
% 1.89/2.11 tff(21,plain,
% 1.89/2.11 (![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))))) <=> ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.11 inference(quant_intro,[status(thm)],[20])).
% 1.89/2.11 tff(22,axiom,(![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => ![B: $i] : (((((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A)))))) => (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t14_yellow19')).
% 1.89/2.11 tff(23,plain,
% 1.89/2.11 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.11 inference(modus_ponens,[status(thm)],[22, 21])).
% 1.89/2.11 tff(24,plain,
% 1.89/2.11 (![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.11 inference(modus_ponens,[status(thm)],[23, 19])).
% 1.89/2.11 tff(25,plain,(
% 1.89/2.11 ![A: $i] : ((~((~empty_carrier(A)) & one_sorted_str(A))) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(cast_as_carrier_subset(A))) & upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A))) & element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B)))))),
% 1.89/2.11 inference(skolemize,[status(sab)],[24])).
% 1.89/2.11 tff(26,plain,
% 1.89/2.11 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[25, 18])).
% 1.91/2.11 tff(27,plain,
% 1.91/2.11 (![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[26, 16])).
% 1.91/2.11 tff(28,plain,
% 1.91/2.11 (((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))) | (empty_carrier(A!35) | (~one_sorted_str(A!35)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))))) <=> ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))) | empty_carrier(A!35) | (~one_sorted_str(A!35)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(29,plain,
% 1.91/2.11 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))) | (empty_carrier(A!35) | (~one_sorted_str(A!35)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))))),
% 1.91/2.11 inference(quant_inst,[status(thm)],[])).
% 1.91/2.11 tff(30,plain,
% 1.91/2.11 ((~![A: $i] : (empty_carrier(A) | (~one_sorted_str(A)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A, net_of_bool_filter(A, cast_as_carrier_subset(A), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A))))))))) | empty_carrier(A!35) | (~one_sorted_str(A!35)) | ![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[29, 28])).
% 1.91/2.11 tff(31,plain,
% 1.91/2.11 (![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))),
% 1.91/2.11 inference(unit_resolution,[status(thm)],[30, 27, 11, 10])).
% 1.91/2.11 tff(32,plain,
% 1.91/2.11 (~((~((~empty(B!36)) & filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))) & element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))) | (B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))),
% 1.91/2.11 inference(and_elim,[status(thm)],[9])).
% 1.91/2.11 tff(33,plain,
% 1.91/2.11 ((~empty(B!36)) & filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35))) & proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))) & element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))),
% 1.91/2.11 inference(or_elim,[status(thm)],[32])).
% 1.91/2.11 tff(34,plain,
% 1.91/2.11 (element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))),
% 1.91/2.11 inference(and_elim,[status(thm)],[33])).
% 1.91/2.11 tff(35,plain,
% 1.91/2.11 (upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))),
% 1.91/2.11 inference(and_elim,[status(thm)],[33])).
% 1.91/2.11 tff(36,plain,
% 1.91/2.11 (filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))),
% 1.91/2.11 inference(and_elim,[status(thm)],[33])).
% 1.91/2.11 tff(37,plain,
% 1.91/2.11 (~empty(B!36)),
% 1.91/2.11 inference(and_elim,[status(thm)],[33])).
% 1.91/2.11 tff(38,plain,
% 1.91/2.11 (((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | (empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))) <=> ((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(39,plain,
% 1.91/2.11 ((empty(B!36) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35))))))) <=> (empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(40,plain,
% 1.91/2.11 (((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | (empty(B!36) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) <=> ((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | (empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36)))))),
% 1.91/2.11 inference(monotonicity,[status(thm)],[39])).
% 1.91/2.11 tff(41,plain,
% 1.91/2.11 (((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | (empty(B!36) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) <=> ((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))))),
% 1.91/2.11 inference(transitivity,[status(thm)],[40, 38])).
% 1.91/2.11 tff(42,plain,
% 1.91/2.11 ((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | (empty(B!36) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))),
% 1.91/2.11 inference(quant_inst,[status(thm)],[])).
% 1.91/2.11 tff(43,plain,
% 1.91/2.11 ((~![B: $i] : (empty(B) | (set_difference(B, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B))) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))))) | empty(B!36) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[42, 41])).
% 1.91/2.11 tff(44,plain,
% 1.91/2.11 (set_difference(B!36, singleton(empty_set)) = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))),
% 1.91/2.11 inference(unit_resolution,[status(thm)],[43, 37, 36, 35, 34, 31])).
% 1.91/2.11 tff(45,plain,
% 1.91/2.11 (^[A: $i, B: $i] : refl((~(in(B, A) <=> (set_difference(A, singleton(B)) = A))) <=> (~(in(B, A) <=> (set_difference(A, singleton(B)) = A))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(46,plain,
% 1.91/2.11 (![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A))) <=> ![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[45])).
% 1.91/2.11 tff(47,plain,
% 1.91/2.11 (![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A))) <=> ![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(48,plain,
% 1.91/2.11 (^[A: $i, B: $i] : trans(rewrite(((set_difference(A, singleton(B)) = A) <=> (~in(B, A))) <=> (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))), rewrite((~(in(B, A) <=> (set_difference(A, singleton(B)) = A))) <=> (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))), (((set_difference(A, singleton(B)) = A) <=> (~in(B, A))) <=> (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(49,plain,
% 1.91/2.11 (![A: $i, B: $i] : ((set_difference(A, singleton(B)) = A) <=> (~in(B, A))) <=> ![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[48])).
% 1.91/2.11 tff(50,axiom,(![A: $i, B: $i] : ((set_difference(A, singleton(B)) = A) <=> (~in(B, A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t65_zfmisc_1')).
% 1.91/2.11 tff(51,plain,
% 1.91/2.11 (![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[50, 49])).
% 1.91/2.11 tff(52,plain,
% 1.91/2.11 (![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[51, 47])).
% 1.91/2.11 tff(53,plain,(
% 1.91/2.11 ![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(skolemize,[status(sab)],[52])).
% 1.91/2.11 tff(54,plain,
% 1.91/2.11 (![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[53, 46])).
% 1.91/2.11 tff(55,plain,
% 1.91/2.11 ((~![A: $i, B: $i] : (~(in(B, A) <=> (set_difference(A, singleton(B)) = A)))) | (~(in(empty_set, B!36) <=> (set_difference(B!36, singleton(empty_set)) = B!36)))),
% 1.91/2.11 inference(quant_inst,[status(thm)],[])).
% 1.91/2.11 tff(56,plain,
% 1.91/2.11 (~(in(empty_set, B!36) <=> (set_difference(B!36, singleton(empty_set)) = B!36))),
% 1.91/2.11 inference(unit_resolution,[status(thm)],[55, 54])).
% 1.91/2.11 tff(57,plain,
% 1.91/2.11 (^[A: $i] : refl((empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A))) <=> (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(58,plain,
% 1.91/2.11 (![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A))) <=> ![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[57])).
% 1.91/2.11 tff(59,plain,
% 1.91/2.11 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite(((~empty_carrier(A)) & one_sorted_str(A)) <=> (~(empty_carrier(A) | (~one_sorted_str(A))))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (~(~(empty_carrier(A) | (~one_sorted_str(A))))))), rewrite((~(~(empty_carrier(A) | (~one_sorted_str(A))))) <=> (empty_carrier(A) | (~one_sorted_str(A)))), ((~((~empty_carrier(A)) & one_sorted_str(A))) <=> (empty_carrier(A) | (~one_sorted_str(A))))), (((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ((~empty(cast_as_carrier_subset(A))) | (empty_carrier(A) | (~one_sorted_str(A)))))), rewrite(((~empty(cast_as_carrier_subset(A))) | (empty_carrier(A) | (~one_sorted_str(A)))) <=> (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))), (((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(60,plain,
% 1.91/2.11 (![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[59])).
% 1.91/2.11 tff(61,plain,
% 1.91/2.11 (![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))) <=> ![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(62,plain,
% 1.91/2.11 (^[A: $i] : rewrite((((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(cast_as_carrier_subset(A)))) <=> ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A)))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(63,plain,
% 1.91/2.11 (![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(cast_as_carrier_subset(A)))) <=> ![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[62])).
% 1.91/2.11 tff(64,axiom,(![A: $i] : (((~empty_carrier(A)) & one_sorted_str(A)) => (~empty(cast_as_carrier_subset(A))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fc2_pre_topc')).
% 1.91/2.11 tff(65,plain,
% 1.91/2.11 (![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[64, 63])).
% 1.91/2.11 tff(66,plain,
% 1.91/2.11 (![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[65, 61])).
% 1.91/2.11 tff(67,plain,(
% 1.91/2.11 ![A: $i] : ((~empty(cast_as_carrier_subset(A))) | (~((~empty_carrier(A)) & one_sorted_str(A))))),
% 1.91/2.11 inference(skolemize,[status(sab)],[66])).
% 1.91/2.11 tff(68,plain,
% 1.91/2.11 (![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[67, 60])).
% 1.91/2.11 tff(69,plain,
% 1.91/2.11 (![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[68, 58])).
% 1.91/2.11 tff(70,plain,
% 1.91/2.11 (((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | (empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35))))) <=> ((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(71,plain,
% 1.91/2.11 ((empty_carrier(A!35) | (~empty(cast_as_carrier_subset(A!35))) | (~one_sorted_str(A!35))) <=> (empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35))))),
% 1.91/2.11 inference(rewrite,[status(thm)],[])).
% 1.91/2.11 tff(72,plain,
% 1.91/2.11 (((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | (empty_carrier(A!35) | (~empty(cast_as_carrier_subset(A!35))) | (~one_sorted_str(A!35)))) <=> ((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | (empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35)))))),
% 1.91/2.11 inference(monotonicity,[status(thm)],[71])).
% 1.91/2.11 tff(73,plain,
% 1.91/2.11 (((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | (empty_carrier(A!35) | (~empty(cast_as_carrier_subset(A!35))) | (~one_sorted_str(A!35)))) <=> ((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35))))),
% 1.91/2.11 inference(transitivity,[status(thm)],[72, 70])).
% 1.91/2.11 tff(74,plain,
% 1.91/2.11 ((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | (empty_carrier(A!35) | (~empty(cast_as_carrier_subset(A!35))) | (~one_sorted_str(A!35)))),
% 1.91/2.11 inference(quant_inst,[status(thm)],[])).
% 1.91/2.11 tff(75,plain,
% 1.91/2.11 ((~![A: $i] : (empty_carrier(A) | (~empty(cast_as_carrier_subset(A))) | (~one_sorted_str(A)))) | empty_carrier(A!35) | (~one_sorted_str(A!35)) | (~empty(cast_as_carrier_subset(A!35)))),
% 1.91/2.11 inference(modus_ponens,[status(thm)],[74, 73])).
% 1.91/2.11 tff(76,plain,
% 1.91/2.11 (~empty(cast_as_carrier_subset(A!35))),
% 1.91/2.11 inference(unit_resolution,[status(thm)],[75, 69, 11, 10])).
% 1.91/2.11 tff(77,plain,
% 1.91/2.11 (^[A: $i] : refl((empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) <=> (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(78,plain,
% 1.91/2.11 (![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[77])).
% 1.91/2.11 tff(79,plain,
% 1.91/2.11 (^[A: $i] : rewrite((empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) <=> (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(80,plain,
% 1.91/2.11 (![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.11 inference(quant_intro,[status(thm)],[79])).
% 1.91/2.11 tff(81,plain,
% 1.91/2.11 (![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.11 inference(transitivity,[status(thm)],[80, 78])).
% 1.91/2.11 tff(82,plain,
% 1.91/2.11 (^[A: $i] : rewrite((empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))) <=> (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))))),
% 1.91/2.11 inference(bind,[status(th)],[])).
% 1.91/2.11 tff(83,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.12 inference(quant_intro,[status(thm)],[82])).
% 1.91/2.12 tff(84,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))),
% 1.91/2.12 inference(rewrite,[status(thm)],[])).
% 1.91/2.12 tff(85,plain,
% 1.91/2.12 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)))), (((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) <=> (((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))))), rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))))), (((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A))))))), ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) <=> (((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))))), rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))), ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) <=> ((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A))))))), (((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))) <=> (((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))))), rewrite((((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))) <=> ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))), (((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))) <=> ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))))), (![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))) <=> ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))), (((~empty(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C))))) <=> ((~empty(A)) => ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))))), rewrite(((~empty(A)) => ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C))))) <=> (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))), (((~empty(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C))))) <=> (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))))),
% 1.91/2.12 inference(bind,[status(th)],[])).
% 1.91/2.12 tff(86,plain,
% 1.91/2.12 (![A: $i] : ((~empty(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C))))) <=> ![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))),
% 1.91/2.12 inference(quant_intro,[status(thm)],[85])).
% 1.91/2.12 tff(87,axiom,(![A: $i] : ((~empty(A)) => ![B: $i] : ((((((~empty(B)) & filtered_subset(B, boole_POSet(A))) & upper_relstr_subset(B, boole_POSet(A))) & proper_element(B, powerset(the_carrier(boole_POSet(A))))) & element(B, powerset(the_carrier(boole_POSet(A))))) => ![C: $i] : (~(in(C, B) & empty(C)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t2_yellow19')).
% 1.91/2.12 tff(88,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))),
% 1.91/2.12 inference(modus_ponens,[status(thm)],[87, 86])).
% 1.91/2.12 tff(89,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))),
% 1.91/2.12 inference(modus_ponens,[status(thm)],[88, 84])).
% 1.91/2.12 tff(90,plain,(
% 1.91/2.12 ![A: $i] : (empty(A) | ![B: $i] : ((~((~empty(B)) & filtered_subset(B, boole_POSet(A)) & upper_relstr_subset(B, boole_POSet(A)) & proper_element(B, powerset(the_carrier(boole_POSet(A)))) & element(B, powerset(the_carrier(boole_POSet(A)))))) | ![C: $i] : (~(in(C, B) & empty(C)))))),
% 1.91/2.12 inference(skolemize,[status(sab)],[89])).
% 1.91/2.12 tff(91,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.12 inference(modus_ponens,[status(thm)],[90, 83])).
% 1.91/2.12 tff(92,plain,
% 1.91/2.12 (![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.12 inference(modus_ponens,[status(thm)],[91, 81])).
% 1.91/2.12 tff(93,plain,
% 1.91/2.12 (((~![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))) | (empty(cast_as_carrier_subset(A!35)) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))) <=> ((~![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))) | empty(cast_as_carrier_subset(A!35)) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.12 inference(rewrite,[status(thm)],[])).
% 1.91/2.12 tff(94,plain,
% 1.91/2.12 ((~![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))) | (empty(cast_as_carrier_subset(A!35)) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))),
% 1.91/2.12 inference(quant_inst,[status(thm)],[])).
% 1.91/2.12 tff(95,plain,
% 1.91/2.12 ((~![A: $i] : (empty(A) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(A))) | (~upper_relstr_subset(B, boole_POSet(A))) | (~element(B, powerset(the_carrier(boole_POSet(A))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(A))))) | ![C: $i] : ((~in(C, B)) | (~empty(C)))))) | empty(cast_as_carrier_subset(A!35)) | ![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))),
% 1.91/2.12 inference(modus_ponens,[status(thm)],[94, 93])).
% 1.91/2.12 tff(96,plain,
% 1.91/2.12 (![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))),
% 1.91/2.12 inference(unit_resolution,[status(thm)],[95, 92, 76])).
% 1.91/2.12 tff(97,plain,
% 1.91/2.12 (proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))),
% 1.91/2.12 inference(and_elim,[status(thm)],[33])).
% 1.91/2.12 tff(98,plain,
% 1.91/2.12 (((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36))))) <=> ((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36))))),
% 1.91/2.12 inference(rewrite,[status(thm)],[])).
% 1.91/2.12 tff(99,plain,
% 1.91/2.12 ((empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B!36)) | (~empty(C)))) <=> (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36))))),
% 1.91/2.12 inference(rewrite,[status(thm)],[])).
% 1.91/2.12 tff(100,plain,
% 1.91/2.12 (((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B!36)) | (~empty(C))))) <=> ((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36)))))),
% 1.91/2.12 inference(monotonicity,[status(thm)],[99])).
% 1.91/2.12 tff(101,plain,
% 1.91/2.12 (((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B!36)) | (~empty(C))))) <=> ((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36))))),
% 1.91/2.12 inference(transitivity,[status(thm)],[100, 98])).
% 1.91/2.12 tff(102,plain,
% 1.91/2.12 ((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | (empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B!36)) | (~empty(C))))),
% 1.91/2.12 inference(quant_inst,[status(thm)],[])).
% 1.91/2.12 tff(103,plain,
% 1.91/2.12 ((~![B: $i] : (empty(B) | (~filtered_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~in(C, B)) | (~empty(C))))) | empty(B!36) | (~filtered_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~upper_relstr_subset(B!36, boole_POSet(cast_as_carrier_subset(A!35)))) | (~element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | (~proper_element(B!36, powerset(the_carrier(boole_POSet(cast_as_carrier_subset(A!35)))))) | ![C: $i] : ((~empty(C)) | (~in(C, B!36)))),
% 1.93/2.13 inference(modus_ponens,[status(thm)],[102, 101])).
% 1.93/2.13 tff(104,plain,
% 1.93/2.13 (![C: $i] : ((~empty(C)) | (~in(C, B!36)))),
% 1.93/2.13 inference(unit_resolution,[status(thm)],[103, 37, 36, 35, 97, 34, 96])).
% 1.93/2.13 tff(105,plain,
% 1.93/2.13 (empty(empty_set) <=> empty(empty_set)),
% 1.93/2.13 inference(rewrite,[status(thm)],[])).
% 1.93/2.13 tff(106,axiom,((empty(empty_set) & relation(empty_set)) & relation_empty_yielding(empty_set)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fc12_relat_1')).
% 1.93/2.13 tff(107,plain,
% 1.93/2.13 (empty(empty_set) & relation(empty_set)),
% 1.93/2.13 inference(and_elim,[status(thm)],[106])).
% 1.93/2.13 tff(108,plain,
% 1.93/2.13 (empty(empty_set)),
% 1.93/2.13 inference(and_elim,[status(thm)],[107])).
% 1.93/2.13 tff(109,plain,
% 1.93/2.13 (empty(empty_set)),
% 1.93/2.13 inference(modus_ponens,[status(thm)],[108, 105])).
% 1.93/2.13 tff(110,plain,
% 1.93/2.13 (((~![C: $i] : ((~empty(C)) | (~in(C, B!36)))) | ((~empty(empty_set)) | (~in(empty_set, B!36)))) <=> ((~![C: $i] : ((~empty(C)) | (~in(C, B!36)))) | (~empty(empty_set)) | (~in(empty_set, B!36)))),
% 1.93/2.13 inference(rewrite,[status(thm)],[])).
% 1.93/2.13 tff(111,plain,
% 1.93/2.13 ((~![C: $i] : ((~empty(C)) | (~in(C, B!36)))) | ((~empty(empty_set)) | (~in(empty_set, B!36)))),
% 1.93/2.13 inference(quant_inst,[status(thm)],[])).
% 1.93/2.13 tff(112,plain,
% 1.93/2.13 ((~![C: $i] : ((~empty(C)) | (~in(C, B!36)))) | (~empty(empty_set)) | (~in(empty_set, B!36))),
% 1.93/2.13 inference(modus_ponens,[status(thm)],[111, 110])).
% 1.93/2.13 tff(113,plain,
% 1.93/2.13 (~in(empty_set, B!36)),
% 1.93/2.13 inference(unit_resolution,[status(thm)],[112, 109, 104])).
% 1.93/2.13 tff(114,plain,
% 1.93/2.13 ((in(empty_set, B!36) <=> (set_difference(B!36, singleton(empty_set)) = B!36)) | in(empty_set, B!36) | (set_difference(B!36, singleton(empty_set)) = B!36)),
% 1.93/2.13 inference(tautology,[status(thm)],[])).
% 1.93/2.13 tff(115,plain,
% 1.93/2.13 (set_difference(B!36, singleton(empty_set)) = B!36),
% 1.93/2.13 inference(unit_resolution,[status(thm)],[114, 113, 56])).
% 1.93/2.13 tff(116,plain,
% 1.93/2.13 (B!36 = set_difference(B!36, singleton(empty_set))),
% 1.93/2.13 inference(symmetry,[status(thm)],[115])).
% 1.93/2.13 tff(117,plain,
% 1.93/2.13 (B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36))),
% 1.93/2.13 inference(transitivity,[status(thm)],[116, 44])).
% 1.93/2.13 tff(118,plain,
% 1.93/2.13 (~(B!36 = filter_of_net_str(A!35, net_of_bool_filter(A!35, cast_as_carrier_subset(A!35), B!36)))),
% 1.93/2.13 inference(or_elim,[status(thm)],[32])).
% 1.93/2.13 tff(119,plain,
% 1.93/2.13 ($false),
% 1.93/2.13 inference(unit_resolution,[status(thm)],[118, 117])).
% 1.93/2.13 % SZS output end Proof
% 1.93/2.14 % E exiting
%------------------------------------------------------------------------------