%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU174+2 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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:08 AM UTC 2025
% Result : Theorem 1.93s 2.10s
% Output : Proof 1.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU174+2 : TPTP v9.0.0. Released v3.3.0.
% 0.04/0.13 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 06:12:38 EDT 2025
% 0.12/0.33 % CPUTime :
% 1.93/2.10 % SZS status Theorem
% 1.93/2.10 % SZS output start Proof
% 1.93/2.10 tff(in_type, type, (
% 1.93/2.10 in: ( $i * $i ) > $o)).
% 1.93/2.10 tff(tptp_fun_B_25_type, type, (
% 1.93/2.10 tptp_fun_B_25: $i)).
% 1.93/2.10 tff(subset_complement_type, type, (
% 1.93/2.10 subset_complement: ( $i * $i ) > $i)).
% 1.93/2.10 tff(tptp_fun_D_16_type, type, (
% 1.93/2.10 tptp_fun_D_16: ( $i * $i * $i ) > $i)).
% 1.93/2.10 tff(tptp_fun_A_26_type, type, (
% 1.93/2.10 tptp_fun_A_26: $i)).
% 1.93/2.10 tff(tptp_fun_B_20_type, type, (
% 1.93/2.10 tptp_fun_B_20: $i > $i)).
% 1.93/2.10 tff(powerset_type, type, (
% 1.93/2.10 powerset: $i > $i)).
% 1.93/2.10 tff(empty_set_type, type, (
% 1.93/2.10 empty_set: $i)).
% 1.93/2.10 tff(element_type, type, (
% 1.93/2.10 element: ( $i * $i ) > $o)).
% 1.93/2.10 tff(complements_of_subsets_type, type, (
% 1.93/2.10 complements_of_subsets: ( $i * $i ) > $i)).
% 1.93/2.10 tff(empty_type, type, (
% 1.93/2.10 empty: $i > $o)).
% 1.93/2.10 tff(disjoint_type, type, (
% 1.93/2.10 disjoint: ( $i * $i ) > $o)).
% 1.93/2.10 tff(tptp_fun_C_24_type, type, (
% 1.93/2.10 tptp_fun_C_24: ( $i * $i ) > $i)).
% 1.93/2.10 tff(set_difference_type, type, (
% 1.93/2.10 set_difference: ( $i * $i ) > $i)).
% 1.93/2.10 tff(1,plain,
% 1.93/2.10 (^[A: $i] : refl((~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A))))) <=> (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(2,plain,
% 1.93/2.10 (![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A))))) <=> ![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[1])).
% 1.93/2.10 tff(3,plain,
% 1.93/2.10 (^[A: $i] : rewrite((element(tptp_fun_B_20(A), powerset(A)) & empty(tptp_fun_B_20(A))) <=> (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(4,plain,
% 1.93/2.10 (![A: $i] : (element(tptp_fun_B_20(A), powerset(A)) & empty(tptp_fun_B_20(A))) <=> ![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[3])).
% 1.93/2.10 tff(5,plain,
% 1.93/2.10 (![A: $i] : ?[B: $i] : (element(B, powerset(A)) & empty(B)) <=> ![A: $i] : ?[B: $i] : (element(B, powerset(A)) & empty(B))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(6,axiom,(![A: $i] : ?[B: $i] : (element(B, powerset(A)) & empty(B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','rc2_subset_1')).
% 1.93/2.10 tff(7,plain,
% 1.93/2.10 (![A: $i] : ?[B: $i] : (element(B, powerset(A)) & empty(B))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[6, 5])).
% 1.93/2.10 tff(8,plain,(
% 1.93/2.10 ![A: $i] : (element(tptp_fun_B_20(A), powerset(A)) & empty(tptp_fun_B_20(A)))),
% 1.93/2.10 inference(skolemize,[status(sab)],[7])).
% 1.93/2.10 tff(9,plain,
% 1.93/2.10 (![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[8, 4])).
% 1.93/2.10 tff(10,plain,
% 1.93/2.10 (![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[9, 2])).
% 1.93/2.10 tff(11,plain,
% 1.93/2.10 ((~![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))) | (~((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~empty(tptp_fun_B_20(powerset(A!26))))))),
% 1.93/2.10 inference(quant_inst,[status(thm)],[])).
% 1.93/2.10 tff(12,plain,
% 1.93/2.10 (~((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~empty(tptp_fun_B_20(powerset(A!26)))))),
% 1.93/2.10 inference(unit_resolution,[status(thm)],[11, 10])).
% 1.93/2.10 tff(13,plain,
% 1.93/2.10 (((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~empty(tptp_fun_B_20(powerset(A!26))))) | element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))),
% 1.93/2.10 inference(tautology,[status(thm)],[])).
% 1.93/2.10 tff(14,plain,
% 1.93/2.10 (element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))),
% 1.93/2.10 inference(unit_resolution,[status(thm)],[13, 12])).
% 1.93/2.10 tff(15,plain,
% 1.93/2.10 (^[A: $i, B: $i] : refl(((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))) <=> ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(16,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[15])).
% 1.93/2.10 tff(17,plain,
% 1.93/2.10 (^[A: $i, B: $i] : rewrite(((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))) <=> ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(18,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[17])).
% 1.93/2.10 tff(19,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(transitivity,[status(thm)],[18, 16])).
% 1.93/2.10 tff(20,plain,
% 1.93/2.10 (^[A: $i, B: $i] : rewrite(((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))) & ((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))) <=> ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(21,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))) & ((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B)))))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[20])).
% 1.93/2.10 tff(22,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(23,plain,
% 1.93/2.10 (^[A: $i, B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite(((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B)))) <=> ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))), ((element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B))))) <=> (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))), rewrite((element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) <=> ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))))), ((element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B))))) <=> ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))))))), (![C: $i] : (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B))))) <=> ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))), ((element(B, powerset(powerset(A))) => ![C: $i] : (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B)))))) <=> (element(B, powerset(powerset(A))) => ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))))))), rewrite((element(B, powerset(powerset(A))) => ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))))) <=> ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))), ((element(B, powerset(powerset(A))) => ![C: $i] : (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B)))))) <=> ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(24,plain,
% 1.93/2.10 (![A: $i, B: $i] : (element(B, powerset(powerset(A))) => ![C: $i] : (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B)))))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[23])).
% 1.93/2.10 tff(25,axiom,(![A: $i, B: $i] : (element(B, powerset(powerset(A))) => ![C: $i] : (element(C, powerset(powerset(A))) => ((C = complements_of_subsets(A, B)) <=> ![D: $i] : (element(D, powerset(A)) => (in(D, C) <=> in(subset_complement(A, D), B))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','d8_setfam_1')).
% 1.93/2.10 tff(26,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[25, 24])).
% 1.93/2.10 tff(27,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | ((C = complements_of_subsets(A, B)) <=> ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[26, 22])).
% 1.93/2.10 tff(28,plain,(
% 1.93/2.10 ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B)))) & ((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))),
% 1.93/2.10 inference(skolemize,[status(sab)],[27])).
% 1.93/2.10 tff(29,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[28, 21])).
% 1.93/2.10 tff(30,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[29, 19])).
% 1.93/2.10 tff(31,plain,
% 1.93/2.10 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(32,plain,
% 1.93/2.10 (((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) | (~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))))))))) <=> ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(33,plain,
% 1.93/2.10 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) | (~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))))),
% 1.93/2.10 inference(monotonicity,[status(thm)],[32])).
% 1.93/2.10 tff(34,plain,
% 1.93/2.10 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) | (~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))))))),
% 1.93/2.10 inference(transitivity,[status(thm)],[33, 31])).
% 1.93/2.10 tff(35,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) | (~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))))))))))),
% 1.93/2.10 inference(quant_inst,[status(thm)],[])).
% 1.93/2.10 tff(36,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[35, 34])).
% 1.93/2.10 tff(37,plain,
% 1.93/2.10 (![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))),
% 1.93/2.10 inference(unit_resolution,[status(thm)],[36, 30, 14])).
% 1.93/2.10 tff(38,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A)))))) <=> (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(39,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : (element(B, powerset(powerset(A))) => (~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))))) <=> (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(40,axiom,(~![A: $i, B: $i] : (element(B, powerset(powerset(A))) => (~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t46_setfam_1')).
% 1.93/2.10 tff(41,plain,
% 1.93/2.10 (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[40, 39])).
% 1.93/2.10 tff(42,plain,
% 1.93/2.10 (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[41, 38])).
% 1.93/2.10 tff(43,plain,
% 1.93/2.10 (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[42, 38])).
% 1.93/2.10 tff(44,plain,
% 1.93/2.10 (~![A: $i, B: $i] : ((~((~(B = empty_set)) & (complements_of_subsets(A, B) = empty_set))) | (~element(B, powerset(powerset(A)))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[43, 38])).
% 1.93/2.10 tff(45,plain,(
% 1.93/2.10 ~((~((~(B!25 = empty_set)) & (complements_of_subsets(A!26, B!25) = empty_set))) | (~element(B!25, powerset(powerset(A!26)))))),
% 1.93/2.10 inference(skolemize,[status(sab)],[44])).
% 1.93/2.10 tff(46,plain,
% 1.93/2.10 ((~(B!25 = empty_set)) & (complements_of_subsets(A!26, B!25) = empty_set)),
% 1.93/2.10 inference(or_elim,[status(thm)],[45])).
% 1.93/2.10 tff(47,plain,
% 1.93/2.10 (complements_of_subsets(A!26, B!25) = empty_set),
% 1.93/2.10 inference(and_elim,[status(thm)],[46])).
% 1.93/2.10 tff(48,plain,
% 1.93/2.10 (empty_set = complements_of_subsets(A!26, B!25)),
% 1.93/2.10 inference(symmetry,[status(thm)],[47])).
% 1.93/2.10 tff(49,plain,
% 1.93/2.10 (element(empty_set, powerset(powerset(A!26))) <=> element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26)))),
% 1.93/2.10 inference(monotonicity,[status(thm)],[48])).
% 1.93/2.10 tff(50,plain,
% 1.93/2.10 (element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26))) <=> element(empty_set, powerset(powerset(A!26)))),
% 1.93/2.10 inference(symmetry,[status(thm)],[49])).
% 1.93/2.10 tff(51,plain,
% 1.93/2.10 (element(B!25, powerset(powerset(A!26)))),
% 1.93/2.10 inference(or_elim,[status(thm)],[45])).
% 1.93/2.10 tff(52,plain,
% 1.93/2.10 (^[A: $i, B: $i] : refl(((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A)))) <=> ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A)))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(53,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A)))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[52])).
% 1.93/2.10 tff(54,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A)))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(55,plain,
% 1.93/2.10 (^[A: $i, B: $i] : rewrite((element(B, powerset(powerset(A))) => element(complements_of_subsets(A, B), powerset(powerset(A)))) <=> ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A)))))),
% 1.93/2.10 inference(bind,[status(th)],[])).
% 1.93/2.10 tff(56,plain,
% 1.93/2.10 (![A: $i, B: $i] : (element(B, powerset(powerset(A))) => element(complements_of_subsets(A, B), powerset(powerset(A)))) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(quant_intro,[status(thm)],[55])).
% 1.93/2.10 tff(57,axiom,(![A: $i, B: $i] : (element(B, powerset(powerset(A))) => element(complements_of_subsets(A, B), powerset(powerset(A))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dt_k7_setfam_1')).
% 1.93/2.10 tff(58,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[57, 56])).
% 1.93/2.10 tff(59,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[58, 54])).
% 1.93/2.10 tff(60,plain,(
% 1.93/2.10 ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(skolemize,[status(sab)],[59])).
% 1.93/2.10 tff(61,plain,
% 1.93/2.10 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[60, 53])).
% 1.93/2.10 tff(62,plain,
% 1.93/2.10 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))) | ((~element(B!25, powerset(powerset(A!26)))) | element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))) | (~element(B!25, powerset(powerset(A!26)))) | element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(63,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))) | ((~element(B!25, powerset(powerset(A!26)))) | element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26))))),
% 1.93/2.10 inference(quant_inst,[status(thm)],[])).
% 1.93/2.10 tff(64,plain,
% 1.93/2.10 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | element(complements_of_subsets(A, B), powerset(powerset(A))))) | (~element(B!25, powerset(powerset(A!26)))) | element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26)))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[63, 62])).
% 1.93/2.10 tff(65,plain,
% 1.93/2.10 (element(complements_of_subsets(A!26, B!25), powerset(powerset(A!26)))),
% 1.93/2.10 inference(unit_resolution,[status(thm)],[64, 61, 51])).
% 1.93/2.10 tff(66,plain,
% 1.93/2.10 (element(empty_set, powerset(powerset(A!26)))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[65, 50])).
% 1.93/2.10 tff(67,plain,
% 1.93/2.10 (((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))) | ((~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))) <=> ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))) | (~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))),
% 1.93/2.10 inference(rewrite,[status(thm)],[])).
% 1.93/2.10 tff(68,plain,
% 1.93/2.10 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))) | ((~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))),
% 1.93/2.10 inference(quant_inst,[status(thm)],[])).
% 1.93/2.10 tff(69,plain,
% 1.93/2.10 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (C = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))))) | (~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))))),
% 1.93/2.10 inference(modus_ponens,[status(thm)],[68, 67])).
% 1.93/2.10 tff(70,plain,
% 1.93/2.10 (~((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))))),
% 1.93/2.10 inference(unit_resolution,[status(thm)],[69, 66, 37])).
% 1.93/2.10 tff(71,plain,
% 1.93/2.10 (((~((~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), tptp_fun_B_20(powerset(A!26))))))) | (~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))))) | ((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(72,plain,
% 1.93/2.11 ((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[71, 70])).
% 1.93/2.11 tff(73,plain,
% 1.93/2.11 ((empty_set = B!25) <=> (B!25 = empty_set)),
% 1.93/2.11 inference(commutativity,[status(thm)],[])).
% 1.93/2.11 tff(74,plain,
% 1.93/2.11 (^[A: $i, B: $i] : refl(((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B)) <=> ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B)))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(75,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B)) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[74])).
% 1.93/2.11 tff(76,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B)) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(77,plain,
% 1.93/2.11 (^[A: $i, B: $i] : rewrite((element(B, powerset(powerset(A))) => (complements_of_subsets(A, complements_of_subsets(A, B)) = B)) <=> ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B)))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(78,plain,
% 1.93/2.11 (![A: $i, B: $i] : (element(B, powerset(powerset(A))) => (complements_of_subsets(A, complements_of_subsets(A, B)) = B)) <=> ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[77])).
% 1.93/2.11 tff(79,axiom,(![A: $i, B: $i] : (element(B, powerset(powerset(A))) => (complements_of_subsets(A, complements_of_subsets(A, B)) = B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','involutiveness_k7_setfam_1')).
% 1.93/2.11 tff(80,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[79, 78])).
% 1.93/2.11 tff(81,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[80, 76])).
% 1.93/2.11 tff(82,plain,(
% 1.93/2.11 ![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(skolemize,[status(sab)],[81])).
% 1.93/2.11 tff(83,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[82, 75])).
% 1.93/2.11 tff(84,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))) | ((~element(B!25, powerset(powerset(A!26)))) | (complements_of_subsets(A!26, complements_of_subsets(A!26, B!25)) = B!25))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))) | (~element(B!25, powerset(powerset(A!26)))) | (complements_of_subsets(A!26, complements_of_subsets(A!26, B!25)) = B!25))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(85,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))) | ((~element(B!25, powerset(powerset(A!26)))) | (complements_of_subsets(A!26, complements_of_subsets(A!26, B!25)) = B!25))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(86,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | (complements_of_subsets(A, complements_of_subsets(A, B)) = B))) | (~element(B!25, powerset(powerset(A!26)))) | (complements_of_subsets(A!26, complements_of_subsets(A!26, B!25)) = B!25)),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[85, 84])).
% 1.93/2.11 tff(87,plain,
% 1.93/2.11 (complements_of_subsets(A!26, complements_of_subsets(A!26, B!25)) = B!25),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[86, 83, 51])).
% 1.93/2.11 tff(88,plain,
% 1.93/2.11 ((~![A: $i] : (~((~element(tptp_fun_B_20(A), powerset(A))) | (~empty(tptp_fun_B_20(A)))))) | (~((~element(tptp_fun_B_20(empty_set), powerset(empty_set))) | (~empty(tptp_fun_B_20(empty_set)))))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(89,plain,
% 1.93/2.11 (~((~element(tptp_fun_B_20(empty_set), powerset(empty_set))) | (~empty(tptp_fun_B_20(empty_set))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[88, 10])).
% 1.93/2.11 tff(90,plain,
% 1.93/2.11 (((~element(tptp_fun_B_20(empty_set), powerset(empty_set))) | (~empty(tptp_fun_B_20(empty_set)))) | empty(tptp_fun_B_20(empty_set))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(91,plain,
% 1.93/2.11 (empty(tptp_fun_B_20(empty_set))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[90, 89])).
% 1.93/2.11 tff(92,plain,
% 1.93/2.11 (^[A: $i, B: $i] : refl(((A = B) | (~empty(A)) | (~empty(B))) <=> ((A = B) | (~empty(A)) | (~empty(B))))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(93,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B))) <=> ![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[92])).
% 1.93/2.11 tff(94,plain,
% 1.93/2.11 (^[A: $i, B: $i] : trans(monotonicity(rewrite((empty(A) & (~(A = B)) & empty(B)) <=> (~((A = B) | (~empty(A)) | (~empty(B))))), ((~(empty(A) & (~(A = B)) & empty(B))) <=> (~(~((A = B) | (~empty(A)) | (~empty(B))))))), rewrite((~(~((A = B) | (~empty(A)) | (~empty(B))))) <=> ((A = B) | (~empty(A)) | (~empty(B)))), ((~(empty(A) & (~(A = B)) & empty(B))) <=> ((A = B) | (~empty(A)) | (~empty(B)))))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(95,plain,
% 1.93/2.11 (![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B))) <=> ![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[94])).
% 1.93/2.11 tff(96,plain,
% 1.93/2.11 (![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B))) <=> ![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(97,plain,
% 1.93/2.11 (^[A: $i, B: $i] : rewrite((~((empty(A) & (~(A = B))) & empty(B))) <=> (~(empty(A) & (~(A = B)) & empty(B))))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(98,plain,
% 1.93/2.11 (![A: $i, B: $i] : (~((empty(A) & (~(A = B))) & empty(B))) <=> ![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B)))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[97])).
% 1.93/2.11 tff(99,axiom,(![A: $i, B: $i] : (~((empty(A) & (~(A = B))) & empty(B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t8_boole')).
% 1.93/2.11 tff(100,plain,
% 1.93/2.11 (![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[99, 98])).
% 1.93/2.11 tff(101,plain,
% 1.93/2.11 (![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[100, 96])).
% 1.93/2.11 tff(102,plain,(
% 1.93/2.11 ![A: $i, B: $i] : (~(empty(A) & (~(A = B)) & empty(B)))),
% 1.93/2.11 inference(skolemize,[status(sab)],[101])).
% 1.93/2.11 tff(103,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[102, 95])).
% 1.93/2.11 tff(104,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[103, 93])).
% 1.93/2.11 tff(105,plain,
% 1.93/2.11 (empty(empty_set) <=> empty(empty_set)),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(106,axiom,(empty(empty_set)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fc1_xboole_0')).
% 1.93/2.11 tff(107,plain,
% 1.93/2.11 (empty(empty_set)),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[106, 105])).
% 1.93/2.11 tff(108,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set)))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(109,plain,
% 1.93/2.11 (((empty_set = tptp_fun_B_20(empty_set)) | (~empty(empty_set)) | (~empty(tptp_fun_B_20(empty_set)))) <=> ((~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(110,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((empty_set = tptp_fun_B_20(empty_set)) | (~empty(empty_set)) | (~empty(tptp_fun_B_20(empty_set))))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set))))),
% 1.93/2.11 inference(monotonicity,[status(thm)],[109])).
% 1.93/2.11 tff(111,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((empty_set = tptp_fun_B_20(empty_set)) | (~empty(empty_set)) | (~empty(tptp_fun_B_20(empty_set))))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(transitivity,[status(thm)],[110, 108])).
% 1.93/2.11 tff(112,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((empty_set = tptp_fun_B_20(empty_set)) | (~empty(empty_set)) | (~empty(tptp_fun_B_20(empty_set))))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(113,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(empty_set)) | (empty_set = tptp_fun_B_20(empty_set))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[112, 111])).
% 1.93/2.11 tff(114,plain,
% 1.93/2.11 (empty_set = tptp_fun_B_20(empty_set)),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[113, 107, 104, 91])).
% 1.93/2.11 tff(115,plain,
% 1.93/2.11 (tptp_fun_B_20(empty_set) = empty_set),
% 1.93/2.11 inference(symmetry,[status(thm)],[114])).
% 1.93/2.11 tff(116,plain,
% 1.93/2.11 (((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~empty(tptp_fun_B_20(powerset(A!26))))) | empty(tptp_fun_B_20(powerset(A!26)))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(117,plain,
% 1.93/2.11 (empty(tptp_fun_B_20(powerset(A!26)))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[116, 12])).
% 1.93/2.11 tff(118,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(119,plain,
% 1.93/2.11 (((tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (~empty(tptp_fun_B_20(empty_set)))) <=> ((~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(120,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (~empty(tptp_fun_B_20(empty_set))))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set))))),
% 1.93/2.11 inference(monotonicity,[status(thm)],[119])).
% 1.93/2.11 tff(121,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (~empty(tptp_fun_B_20(empty_set))))) <=> ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)))),
% 1.93/2.11 inference(transitivity,[status(thm)],[120, 118])).
% 1.93/2.11 tff(122,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | ((tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (~empty(tptp_fun_B_20(empty_set))))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(123,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((A = B) | (~empty(A)) | (~empty(B)))) | (~empty(tptp_fun_B_20(empty_set))) | (~empty(tptp_fun_B_20(powerset(A!26)))) | (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[122, 121])).
% 1.93/2.11 tff(124,plain,
% 1.93/2.11 (tptp_fun_B_20(powerset(A!26)) = tptp_fun_B_20(empty_set)),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[123, 104, 91, 117])).
% 1.93/2.11 tff(125,plain,
% 1.93/2.11 (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25)),
% 1.93/2.11 inference(transitivity,[status(thm)],[124, 115, 48])).
% 1.93/2.11 tff(126,plain,
% 1.93/2.11 (complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))) = complements_of_subsets(A!26, complements_of_subsets(A!26, B!25))),
% 1.93/2.11 inference(monotonicity,[status(thm)],[125])).
% 1.93/2.11 tff(127,plain,
% 1.93/2.11 (complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))) = B!25),
% 1.93/2.11 inference(transitivity,[status(thm)],[126, 87])).
% 1.93/2.11 tff(128,plain,
% 1.93/2.11 ((empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) <=> (empty_set = B!25)),
% 1.93/2.11 inference(monotonicity,[status(thm)],[127])).
% 1.93/2.11 tff(129,plain,
% 1.93/2.11 ((empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))) <=> (B!25 = empty_set)),
% 1.93/2.11 inference(transitivity,[status(thm)],[128, 73])).
% 1.93/2.11 tff(130,plain,
% 1.93/2.11 ((B!25 = empty_set) <=> (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))),
% 1.93/2.11 inference(symmetry,[status(thm)],[129])).
% 1.93/2.11 tff(131,plain,
% 1.93/2.11 ((~(B!25 = empty_set)) <=> (~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))),
% 1.93/2.11 inference(monotonicity,[status(thm)],[130])).
% 1.93/2.11 tff(132,plain,
% 1.93/2.11 (~(B!25 = empty_set)),
% 1.93/2.11 inference(and_elim,[status(thm)],[46])).
% 1.93/2.11 tff(133,plain,
% 1.93/2.11 (~(empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[132, 131])).
% 1.93/2.11 tff(134,plain,
% 1.93/2.11 ((~((~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26)))))) | (~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))) | (empty_set = complements_of_subsets(A!26, tptp_fun_B_20(powerset(A!26))))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(135,plain,
% 1.93/2.11 (~((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[134, 133, 72])).
% 1.93/2.11 tff(136,plain,
% 1.93/2.11 (((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))) | element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(137,plain,
% 1.93/2.11 (element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[136, 135])).
% 1.93/2.11 tff(138,plain,
% 1.93/2.11 (^[A: $i, B: $i] : refl(((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A))) <=> ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A))))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(139,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A))) <=> ![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[138])).
% 1.93/2.11 tff(140,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A))) <=> ![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(141,plain,
% 1.93/2.11 (^[A: $i, B: $i] : rewrite((element(B, powerset(A)) => element(subset_complement(A, B), powerset(A))) <=> ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A))))),
% 1.93/2.11 inference(bind,[status(th)],[])).
% 1.93/2.11 tff(142,plain,
% 1.93/2.11 (![A: $i, B: $i] : (element(B, powerset(A)) => element(subset_complement(A, B), powerset(A))) <=> ![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(quant_intro,[status(thm)],[141])).
% 1.93/2.11 tff(143,axiom,(![A: $i, B: $i] : (element(B, powerset(A)) => element(subset_complement(A, B), powerset(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dt_k3_subset_1')).
% 1.93/2.11 tff(144,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[143, 142])).
% 1.93/2.11 tff(145,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[144, 140])).
% 1.93/2.11 tff(146,plain,(
% 1.93/2.11 ![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(skolemize,[status(sab)],[145])).
% 1.93/2.11 tff(147,plain,
% 1.93/2.11 (![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[146, 139])).
% 1.93/2.11 tff(148,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))) | ((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26)))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26)))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(149,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))) | ((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26)))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(150,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(A))) | element(subset_complement(A, B), powerset(A)))) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[149, 148])).
% 1.93/2.11 tff(151,plain,
% 1.93/2.11 (element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[150, 147, 137])).
% 1.93/2.11 tff(152,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25))))))))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(153,plain,
% 1.93/2.11 (((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((C = complements_of_subsets(A!26, B!25)) | (~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))))))))) <=> ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25))))))))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(154,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((C = complements_of_subsets(A!26, B!25)) | (~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25))))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))))),
% 1.93/2.11 inference(monotonicity,[status(thm)],[153])).
% 1.93/2.11 tff(155,plain,
% 1.93/2.11 (((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((C = complements_of_subsets(A!26, B!25)) | (~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25))))))))))) <=> ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25))))))))),
% 1.93/2.11 inference(transitivity,[status(thm)],[154, 152])).
% 1.93/2.11 tff(156,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | ((~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((C = complements_of_subsets(A!26, B!25)) | (~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25))))))))))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(157,plain,
% 1.93/2.11 ((~![A: $i, B: $i] : ((~element(B, powerset(powerset(A)))) | ![C: $i] : ((~element(C, powerset(powerset(A)))) | (~((~((~(C = complements_of_subsets(A, B))) | ![D: $i] : ((~element(D, powerset(A))) | (in(D, C) <=> in(subset_complement(A, D), B))))) | (~((C = complements_of_subsets(A, B)) | (~((~element(tptp_fun_D_16(C, B, A), powerset(A))) | (in(tptp_fun_D_16(C, B, A), C) <=> in(subset_complement(A, tptp_fun_D_16(C, B, A)), B))))))))))) | (~element(B!25, powerset(powerset(A!26)))) | ![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[156, 155])).
% 1.93/2.11 tff(158,plain,
% 1.93/2.11 (![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[157, 30, 51])).
% 1.93/2.11 tff(159,plain,
% 1.93/2.11 (((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | ((~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25)))))))) <=> ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | (~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25)))))))),
% 1.93/2.11 inference(rewrite,[status(thm)],[])).
% 1.93/2.11 tff(160,plain,
% 1.93/2.11 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | ((~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25)))))))),
% 1.93/2.11 inference(quant_inst,[status(thm)],[])).
% 1.93/2.11 tff(161,plain,
% 1.93/2.11 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | (~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25))))))),
% 1.93/2.11 inference(modus_ponens,[status(thm)],[160, 159])).
% 1.93/2.11 tff(162,plain,
% 1.93/2.11 ((~element(empty_set, powerset(powerset(A!26)))) | (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25))))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[161, 158])).
% 1.93/2.11 tff(163,plain,
% 1.93/2.11 (~((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25)))))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[162, 66])).
% 1.93/2.11 tff(164,plain,
% 1.93/2.11 (((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(empty_set, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, B!25, A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, B!25, A!26)), B!25)))) | (empty_set = complements_of_subsets(A!26, B!25))))) | ((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(165,plain,
% 1.93/2.11 ((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[164, 163])).
% 1.93/2.11 tff(166,plain,
% 1.93/2.11 ((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | (~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))),
% 1.93/2.11 inference(tautology,[status(thm)],[])).
% 1.93/2.11 tff(167,plain,
% 1.93/2.11 ((~((~(empty_set = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25))))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[166, 48])).
% 1.93/2.11 tff(168,plain,
% 1.93/2.11 (![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))),
% 1.93/2.11 inference(unit_resolution,[status(thm)],[167, 165])).
% 1.93/2.11 tff(169,plain,
% 1.93/2.11 (((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))) | ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))) <=> ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))) | (~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(170,plain,
% 1.95/2.12 ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))) | ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(171,plain,
% 1.95/2.12 ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, empty_set) <=> in(subset_complement(A!26, D), B!25)))) | (~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[170, 169])).
% 1.95/2.12 tff(172,plain,
% 1.95/2.12 ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[171, 168])).
% 1.95/2.12 tff(173,plain,
% 1.95/2.12 (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[172, 151])).
% 1.95/2.12 tff(174,plain,
% 1.95/2.12 (((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25)))))))) <=> ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | (~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25)))))))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(175,plain,
% 1.95/2.12 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | ((~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25)))))))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(176,plain,
% 1.95/2.12 ((~![C: $i] : ((~element(C, powerset(powerset(A!26)))) | (~((~((~(C = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, C) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(C, B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(C, B!25, A!26), C) <=> in(subset_complement(A!26, tptp_fun_D_16(C, B!25, A!26)), B!25)))) | (C = complements_of_subsets(A!26, B!25)))))))) | (~element(tptp_fun_B_20(powerset(A!26)), powerset(powerset(A!26)))) | (~((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))))))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[175, 174])).
% 1.95/2.12 tff(177,plain,
% 1.95/2.12 (~((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25)))))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[176, 158, 14])).
% 1.95/2.12 tff(178,plain,
% 1.95/2.12 (((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~((~((~element(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), powerset(A!26))) | (in(tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, tptp_fun_D_16(tptp_fun_B_20(powerset(A!26)), B!25, A!26)), B!25)))) | (tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))))) | ((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))),
% 1.95/2.12 inference(tautology,[status(thm)],[])).
% 1.95/2.12 tff(179,plain,
% 1.95/2.12 ((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[178, 177])).
% 1.95/2.12 tff(180,plain,
% 1.95/2.12 ((~((~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25))))) | (~(tptp_fun_B_20(powerset(A!26)) = complements_of_subsets(A!26, B!25))) | ![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))),
% 1.95/2.12 inference(tautology,[status(thm)],[])).
% 1.95/2.12 tff(181,plain,
% 1.95/2.12 (![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[180, 125, 179])).
% 1.95/2.12 tff(182,plain,
% 1.95/2.12 (((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))) | ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))) <=> ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))) | (~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(183,plain,
% 1.95/2.12 ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))) | ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(184,plain,
% 1.95/2.12 ((~![D: $i] : ((~element(D, powerset(A!26))) | (in(D, tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, D), B!25)))) | (~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[183, 182])).
% 1.95/2.12 tff(185,plain,
% 1.95/2.12 ((~element(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), powerset(A!26))) | (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[184, 181])).
% 1.95/2.12 tff(186,plain,
% 1.95/2.12 (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[185, 151])).
% 1.95/2.12 tff(187,plain,
% 1.95/2.12 (((~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))) | (~(in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))))),
% 1.95/2.12 inference(tautology,[status(thm)],[])).
% 1.95/2.12 tff(188,plain,
% 1.95/2.12 (~(in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[187, 135])).
% 1.95/2.12 tff(189,plain,
% 1.95/2.12 (^[A: $i] : refl((~empty(powerset(A))) <=> (~empty(powerset(A))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(190,plain,
% 1.95/2.12 (![A: $i] : (~empty(powerset(A))) <=> ![A: $i] : (~empty(powerset(A)))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[189])).
% 1.95/2.12 tff(191,plain,
% 1.95/2.12 (![A: $i] : (~empty(powerset(A))) <=> ![A: $i] : (~empty(powerset(A)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(192,axiom,(![A: $i] : (~empty(powerset(A)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fc1_subset_1')).
% 1.95/2.12 tff(193,plain,
% 1.95/2.12 (![A: $i] : (~empty(powerset(A)))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[192, 191])).
% 1.95/2.12 tff(194,plain,(
% 1.95/2.12 ![A: $i] : (~empty(powerset(A)))),
% 1.95/2.12 inference(skolemize,[status(sab)],[193])).
% 1.95/2.12 tff(195,plain,
% 1.95/2.12 (![A: $i] : (~empty(powerset(A)))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[194, 190])).
% 1.95/2.12 tff(196,plain,
% 1.95/2.12 ((~![A: $i] : (~empty(powerset(A)))) | (~empty(powerset(A!26)))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(197,plain,
% 1.95/2.12 (~empty(powerset(A!26))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[196, 195])).
% 1.95/2.12 tff(198,plain,
% 1.95/2.12 (^[A: $i, B: $i] : refl((in(A, B) | empty(B) | (~element(A, B))) <=> (in(A, B) | empty(B) | (~element(A, B))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(199,plain,
% 1.95/2.12 (![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B))) <=> ![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[198])).
% 1.95/2.12 tff(200,plain,
% 1.95/2.12 (![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B))) <=> ![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(201,plain,
% 1.95/2.12 (^[A: $i, B: $i] : rewrite((element(A, B) => (empty(B) | in(A, B))) <=> (in(A, B) | empty(B) | (~element(A, B))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(202,plain,
% 1.95/2.12 (![A: $i, B: $i] : (element(A, B) => (empty(B) | in(A, B))) <=> ![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[201])).
% 1.95/2.12 tff(203,axiom,(![A: $i, B: $i] : (element(A, B) => (empty(B) | in(A, B)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t2_subset')).
% 1.95/2.12 tff(204,plain,
% 1.95/2.12 (![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[203, 202])).
% 1.95/2.12 tff(205,plain,
% 1.95/2.12 (![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[204, 200])).
% 1.95/2.12 tff(206,plain,(
% 1.95/2.12 ![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(skolemize,[status(sab)],[205])).
% 1.95/2.12 tff(207,plain,
% 1.95/2.12 (![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[206, 199])).
% 1.95/2.12 tff(208,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | (empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))) <=> ((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(209,plain,
% 1.95/2.12 ((in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))) <=> (empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(210,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))) <=> ((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | (empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))),
% 1.95/2.12 inference(monotonicity,[status(thm)],[209])).
% 1.95/2.12 tff(211,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))) <=> ((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))),
% 1.95/2.12 inference(transitivity,[status(thm)],[210, 208])).
% 1.95/2.12 tff(212,plain,
% 1.95/2.12 ((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(213,plain,
% 1.95/2.12 ((~![A: $i, B: $i] : (in(A, B) | empty(B) | (~element(A, B)))) | empty(powerset(A!26)) | (~element(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[212, 211])).
% 1.95/2.12 tff(214,plain,
% 1.95/2.12 (in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[213, 207, 197, 137])).
% 1.95/2.12 tff(215,plain,
% 1.95/2.12 (^[A: $i, B: $i] : refl((~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))) <=> (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(216,plain,
% 1.95/2.12 (![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))) <=> ![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[215])).
% 1.95/2.12 tff(217,plain,
% 1.95/2.12 (^[A: $i, B: $i] : rewrite((~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))) <=> (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(218,plain,
% 1.95/2.12 (![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))) <=> ![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[217])).
% 1.95/2.12 tff(219,plain,
% 1.95/2.12 (![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))) <=> ![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(transitivity,[status(thm)],[218, 216])).
% 1.95/2.12 tff(220,plain,
% 1.95/2.12 (^[A: $i, B: $i] : trans(monotonicity(trans(monotonicity(rewrite((in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B)) <=> (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))), ((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) <=> (disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))))), rewrite((disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))) <=> (disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))), ((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) <=> (disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))))), trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite((in(C, A) & in(C, B)) <=> (~((~in(C, B)) | (~in(C, A))))), ((~(in(C, A) & in(C, B))) <=> (~(~((~in(C, B)) | (~in(C, A))))))), rewrite((~(~((~in(C, B)) | (~in(C, A))))) <=> ((~in(C, B)) | (~in(C, A)))), ((~(in(C, A) & in(C, B))) <=> ((~in(C, B)) | (~in(C, A)))))), (![C: $i] : (~(in(C, A) & in(C, B))) <=> ![C: $i] : ((~in(C, B)) | (~in(C, A))))), ((![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B))) <=> (![C: $i] : ((~in(C, B)) | (~in(C, A))) | (~disjoint(A, B))))), rewrite((![C: $i] : ((~in(C, B)) | (~in(C, A))) | (~disjoint(A, B))) <=> ((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))), ((![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B))) <=> ((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))), (((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) & (![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B)))) <=> ((disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))) & ((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))))), rewrite(((disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B))))) & ((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A))))) <=> (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))), (((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) & (![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B)))) <=> (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(221,plain,
% 1.95/2.12 (![A: $i, B: $i] : ((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) & (![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B)))) <=> ![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[220])).
% 1.95/2.12 tff(222,plain,
% 1.95/2.12 (![A: $i, B: $i] : ((~((~disjoint(A, B)) & ![C: $i] : (~(in(C, A) & in(C, B))))) & (~(?[C: $i] : (in(C, A) & in(C, B)) & disjoint(A, B)))) <=> ![A: $i, B: $i] : ((~((~disjoint(A, B)) & ![C: $i] : (~(in(C, A) & in(C, B))))) & (~(?[C: $i] : (in(C, A) & in(C, B)) & disjoint(A, B))))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(223,axiom,(![A: $i, B: $i] : ((~((~disjoint(A, B)) & ![C: $i] : (~(in(C, A) & in(C, B))))) & (~(?[C: $i] : (in(C, A) & in(C, B)) & disjoint(A, B))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t3_xboole_0')).
% 1.95/2.12 tff(224,plain,
% 1.95/2.12 (![A: $i, B: $i] : ((~((~disjoint(A, B)) & ![C: $i] : (~(in(C, A) & in(C, B))))) & (~(?[C: $i] : (in(C, A) & in(C, B)) & disjoint(A, B))))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[223, 222])).
% 1.95/2.12 tff(225,plain,(
% 1.95/2.12 ![A: $i, B: $i] : ((disjoint(A, B) | (in(tptp_fun_C_24(B, A), A) & in(tptp_fun_C_24(B, A), B))) & (![C: $i] : (~(in(C, A) & in(C, B))) | (~disjoint(A, B))))),
% 1.95/2.12 inference(skolemize,[status(sab)],[224])).
% 1.95/2.12 tff(226,plain,
% 1.95/2.12 (![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[225, 221])).
% 1.95/2.12 tff(227,plain,
% 1.95/2.12 (![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[226, 219])).
% 1.95/2.12 tff(228,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26)))))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))))))))))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(229,plain,
% 1.95/2.12 ((~((~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)))))) | (~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))))) <=> (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26)))))))))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(230,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)))))) | (~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))))))))))),
% 1.95/2.12 inference(monotonicity,[status(thm)],[229])).
% 1.95/2.12 tff(231,plain,
% 1.95/2.12 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)))))) | (~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))))))))))),
% 1.95/2.12 inference(transitivity,[status(thm)],[230, 228])).
% 1.95/2.12 tff(232,plain,
% 1.95/2.12 ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)))))) | (~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))))))),
% 1.95/2.12 inference(quant_inst,[status(thm)],[])).
% 1.95/2.12 tff(233,plain,
% 1.95/2.12 ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26)))))))))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[232, 231])).
% 1.95/2.12 tff(234,plain,
% 1.95/2.12 (~((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26))))))))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[233, 227])).
% 1.95/2.12 tff(235,plain,
% 1.95/2.12 (((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~(disjoint(powerset(A!26), empty_set) | (~((~in(tptp_fun_C_24(empty_set, powerset(A!26)), empty_set)) | (~in(tptp_fun_C_24(empty_set, powerset(A!26)), powerset(A!26)))))))) | ((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))),
% 1.95/2.12 inference(tautology,[status(thm)],[])).
% 1.95/2.12 tff(236,plain,
% 1.95/2.12 ((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))),
% 1.95/2.12 inference(unit_resolution,[status(thm)],[235, 234])).
% 1.95/2.12 tff(237,plain,
% 1.95/2.12 (^[A: $i, B: $i] : refl((disjoint(A, B) <=> (set_difference(A, B) = A)) <=> (disjoint(A, B) <=> (set_difference(A, B) = A)))),
% 1.95/2.12 inference(bind,[status(th)],[])).
% 1.95/2.12 tff(238,plain,
% 1.95/2.12 (![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A)) <=> ![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))),
% 1.95/2.12 inference(quant_intro,[status(thm)],[237])).
% 1.95/2.12 tff(239,plain,
% 1.95/2.12 (![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A)) <=> ![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))),
% 1.95/2.12 inference(rewrite,[status(thm)],[])).
% 1.95/2.12 tff(240,axiom,(![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t83_xboole_1')).
% 1.95/2.12 tff(241,plain,
% 1.95/2.12 (![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[240, 239])).
% 1.95/2.12 tff(242,plain,(
% 1.95/2.12 ![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))),
% 1.95/2.12 inference(skolemize,[status(sab)],[241])).
% 1.95/2.12 tff(243,plain,
% 1.95/2.12 (![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))),
% 1.95/2.12 inference(modus_ponens,[status(thm)],[242, 238])).
% 1.95/2.13 tff(244,plain,
% 1.95/2.13 ((~![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))) | (disjoint(powerset(A!26), empty_set) <=> (set_difference(powerset(A!26), empty_set) = powerset(A!26)))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(245,plain,
% 1.95/2.13 (disjoint(powerset(A!26), empty_set) <=> (set_difference(powerset(A!26), empty_set) = powerset(A!26))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[244, 243])).
% 1.95/2.13 tff(246,plain,
% 1.95/2.13 (^[A: $i] : refl((set_difference(A, empty_set) = A) <=> (set_difference(A, empty_set) = A))),
% 1.95/2.13 inference(bind,[status(th)],[])).
% 1.95/2.13 tff(247,plain,
% 1.95/2.13 (![A: $i] : (set_difference(A, empty_set) = A) <=> ![A: $i] : (set_difference(A, empty_set) = A)),
% 1.95/2.13 inference(quant_intro,[status(thm)],[246])).
% 1.95/2.13 tff(248,plain,
% 1.95/2.13 (![A: $i] : (set_difference(A, empty_set) = A) <=> ![A: $i] : (set_difference(A, empty_set) = A)),
% 1.95/2.13 inference(rewrite,[status(thm)],[])).
% 1.95/2.13 tff(249,axiom,(![A: $i] : (set_difference(A, empty_set) = A)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t3_boole')).
% 1.95/2.13 tff(250,plain,
% 1.95/2.13 (![A: $i] : (set_difference(A, empty_set) = A)),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[249, 248])).
% 1.95/2.13 tff(251,plain,(
% 1.95/2.13 ![A: $i] : (set_difference(A, empty_set) = A)),
% 1.95/2.13 inference(skolemize,[status(sab)],[250])).
% 1.95/2.13 tff(252,plain,
% 1.95/2.13 (![A: $i] : (set_difference(A, empty_set) = A)),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[251, 247])).
% 1.95/2.13 tff(253,plain,
% 1.95/2.13 ((~![A: $i] : (set_difference(A, empty_set) = A)) | (set_difference(powerset(A!26), empty_set) = powerset(A!26))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(254,plain,
% 1.95/2.13 (set_difference(powerset(A!26), empty_set) = powerset(A!26)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[253, 252])).
% 1.95/2.13 tff(255,plain,
% 1.95/2.13 ((~(disjoint(powerset(A!26), empty_set) <=> (set_difference(powerset(A!26), empty_set) = powerset(A!26)))) | disjoint(powerset(A!26), empty_set) | (~(set_difference(powerset(A!26), empty_set) = powerset(A!26)))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(256,plain,
% 1.95/2.13 (disjoint(powerset(A!26), empty_set)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[255, 254, 245])).
% 1.95/2.13 tff(257,plain,
% 1.95/2.13 ((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | (~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(258,plain,
% 1.95/2.13 ((~((~disjoint(powerset(A!26), empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26)))))) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[257, 256])).
% 1.95/2.13 tff(259,plain,
% 1.95/2.13 (![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[258, 236])).
% 1.95/2.13 tff(260,plain,
% 1.95/2.13 (((~![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))) | ((~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set)) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))) <=> ((~![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set)) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))),
% 1.95/2.13 inference(rewrite,[status(thm)],[])).
% 1.95/2.13 tff(261,plain,
% 1.95/2.13 ((~![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))) | ((~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set)) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26))))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(262,plain,
% 1.95/2.13 ((~![C: $i] : ((~in(C, empty_set)) | (~in(C, powerset(A!26))))) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set)) | (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), powerset(A!26)))),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[261, 260])).
% 1.95/2.13 tff(263,plain,
% 1.95/2.13 (~in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[262, 259, 214])).
% 1.95/2.13 tff(264,plain,
% 1.95/2.13 ((in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) <=> in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))) | in(tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26), empty_set) | in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(265,plain,
% 1.95/2.13 (in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[264, 263, 188])).
% 1.95/2.13 tff(266,plain,
% 1.95/2.13 ((~(in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26))) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))) | (~in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), tptp_fun_B_20(powerset(A!26)))) | in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(267,plain,
% 1.95/2.13 (in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[266, 265, 186])).
% 1.95/2.13 tff(268,plain,
% 1.95/2.13 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))))))),
% 1.95/2.13 inference(rewrite,[status(thm)],[])).
% 1.95/2.13 tff(269,plain,
% 1.95/2.13 ((~((~(disjoint(empty_set, empty_set) | (~((~in(tptp_fun_C_24(empty_set, empty_set), empty_set)) | (~in(tptp_fun_C_24(empty_set, empty_set), empty_set)))))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, empty_set))))))) <=> (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))))))),
% 1.95/2.13 inference(rewrite,[status(thm)],[])).
% 1.95/2.13 tff(270,plain,
% 1.95/2.13 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | (~((~in(tptp_fun_C_24(empty_set, empty_set), empty_set)) | (~in(tptp_fun_C_24(empty_set, empty_set), empty_set)))))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, empty_set)))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))))))),
% 1.95/2.13 inference(monotonicity,[status(thm)],[269])).
% 1.95/2.13 tff(271,plain,
% 1.95/2.13 (((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | (~((~in(tptp_fun_C_24(empty_set, empty_set), empty_set)) | (~in(tptp_fun_C_24(empty_set, empty_set), empty_set)))))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, empty_set)))))))) <=> ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))))))),
% 1.95/2.13 inference(transitivity,[status(thm)],[270, 268])).
% 1.95/2.13 tff(272,plain,
% 1.95/2.13 ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | (~((~in(tptp_fun_C_24(empty_set, empty_set), empty_set)) | (~in(tptp_fun_C_24(empty_set, empty_set), empty_set)))))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : ((~in(C, empty_set)) | (~in(C, empty_set)))))))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(273,plain,
% 1.95/2.13 ((~![A: $i, B: $i] : (~((~(disjoint(A, B) | (~((~in(tptp_fun_C_24(B, A), A)) | (~in(tptp_fun_C_24(B, A), B)))))) | (~((~disjoint(A, B)) | ![C: $i] : ((~in(C, B)) | (~in(C, A)))))))) | (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))))))),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[272, 271])).
% 1.95/2.13 tff(274,plain,
% 1.95/2.13 (~((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[273, 227])).
% 1.95/2.13 tff(275,plain,
% 1.95/2.13 (((~(disjoint(empty_set, empty_set) | in(tptp_fun_C_24(empty_set, empty_set), empty_set))) | (~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))))) | ((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(276,plain,
% 1.95/2.13 ((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[275, 274])).
% 1.95/2.13 tff(277,plain,
% 1.95/2.13 ((~![A: $i, B: $i] : (disjoint(A, B) <=> (set_difference(A, B) = A))) | (disjoint(empty_set, empty_set) <=> (set_difference(empty_set, empty_set) = empty_set))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(278,plain,
% 1.95/2.13 (disjoint(empty_set, empty_set) <=> (set_difference(empty_set, empty_set) = empty_set)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[277, 243])).
% 1.95/2.13 tff(279,plain,
% 1.95/2.13 (^[A: $i] : refl((set_difference(empty_set, A) = empty_set) <=> (set_difference(empty_set, A) = empty_set))),
% 1.95/2.13 inference(bind,[status(th)],[])).
% 1.95/2.13 tff(280,plain,
% 1.95/2.13 (![A: $i] : (set_difference(empty_set, A) = empty_set) <=> ![A: $i] : (set_difference(empty_set, A) = empty_set)),
% 1.95/2.13 inference(quant_intro,[status(thm)],[279])).
% 1.95/2.13 tff(281,plain,
% 1.95/2.13 (![A: $i] : (set_difference(empty_set, A) = empty_set) <=> ![A: $i] : (set_difference(empty_set, A) = empty_set)),
% 1.95/2.13 inference(rewrite,[status(thm)],[])).
% 1.95/2.13 tff(282,axiom,(![A: $i] : (set_difference(empty_set, A) = empty_set)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','t4_boole')).
% 1.95/2.13 tff(283,plain,
% 1.95/2.13 (![A: $i] : (set_difference(empty_set, A) = empty_set)),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[282, 281])).
% 1.95/2.13 tff(284,plain,(
% 1.95/2.13 ![A: $i] : (set_difference(empty_set, A) = empty_set)),
% 1.95/2.13 inference(skolemize,[status(sab)],[283])).
% 1.95/2.13 tff(285,plain,
% 1.95/2.13 (![A: $i] : (set_difference(empty_set, A) = empty_set)),
% 1.95/2.13 inference(modus_ponens,[status(thm)],[284, 280])).
% 1.95/2.13 tff(286,plain,
% 1.95/2.13 ((~![A: $i] : (set_difference(empty_set, A) = empty_set)) | (set_difference(empty_set, empty_set) = empty_set)),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(287,plain,
% 1.95/2.13 (set_difference(empty_set, empty_set) = empty_set),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[286, 285])).
% 1.95/2.13 tff(288,plain,
% 1.95/2.13 ((~(disjoint(empty_set, empty_set) <=> (set_difference(empty_set, empty_set) = empty_set))) | disjoint(empty_set, empty_set) | (~(set_difference(empty_set, empty_set) = empty_set))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(289,plain,
% 1.95/2.13 (disjoint(empty_set, empty_set)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[288, 287, 278])).
% 1.95/2.13 tff(290,plain,
% 1.95/2.13 ((~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))) | (~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(291,plain,
% 1.95/2.13 ((~((~disjoint(empty_set, empty_set)) | ![C: $i] : (~in(C, empty_set)))) | ![C: $i] : (~in(C, empty_set))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[290, 289])).
% 1.95/2.13 tff(292,plain,
% 1.95/2.13 (![C: $i] : (~in(C, empty_set))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[291, 276])).
% 1.95/2.13 tff(293,plain,
% 1.95/2.13 ((~![C: $i] : (~in(C, empty_set))) | (~in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set))),
% 1.95/2.13 inference(quant_inst,[status(thm)],[])).
% 1.95/2.13 tff(294,plain,
% 1.95/2.13 (~in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set)),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[293, 292])).
% 1.95/2.13 tff(295,plain,
% 1.95/2.13 ((~(in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))) | in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) | (~in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.13 inference(tautology,[status(thm)],[])).
% 1.95/2.13 tff(296,plain,
% 1.95/2.13 ((~(in(subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26)), empty_set) <=> in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))) | (~in(subset_complement(A!26, subset_complement(A!26, tptp_fun_D_16(empty_set, tptp_fun_B_20(powerset(A!26)), A!26))), B!25))),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[295, 294])).
% 1.95/2.13 tff(297,plain,
% 1.95/2.13 ($false),
% 1.95/2.13 inference(unit_resolution,[status(thm)],[296, 267, 173])).
% 1.95/2.13 % SZS output end Proof
% 1.98/2.15 % E exiting
%------------------------------------------------------------------------------