%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SET144+3 : TPTP v9.0.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:25:20 AM UTC 2025
% Result : Theorem 192.62s 192.95s
% Output : Proof 192.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET144+3 : TPTP v9.0.0. Released v2.2.0.
% 0.10/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n003.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 04:24:54 EDT 2025
% 0.19/0.33 % CPUTime :
% 192.62/192.95 % SZS status Theorem
% 192.62/192.95 % SZS output start Proof
% 192.62/192.95 tff(member_type, type, (
% 192.62/192.95 member: ( $i * $i ) > $o)).
% 192.62/192.95 tff(intersection_type, type, (
% 192.62/192.95 intersection: ( $i * $i ) > $i)).
% 192.62/192.95 tff(tptp_fun_D_2_type, type, (
% 192.62/192.95 tptp_fun_D_2: $i)).
% 192.62/192.95 tff(tptp_fun_C_3_type, type, (
% 192.62/192.95 tptp_fun_C_3: $i)).
% 192.62/192.95 tff(tptp_fun_D_1_type, type, (
% 192.62/192.95 tptp_fun_D_1: ( $i * $i ) > $i)).
% 192.62/192.95 tff(union_type, type, (
% 192.62/192.95 union: ( $i * $i ) > $i)).
% 192.62/192.95 tff(tptp_fun_B_4_type, type, (
% 192.62/192.95 tptp_fun_B_4: $i)).
% 192.62/192.95 tff(tptp_fun_D_0_type, type, (
% 192.62/192.95 tptp_fun_D_0: ( $i * $i ) > $i)).
% 192.62/192.95 tff(subset_type, type, (
% 192.62/192.95 subset: ( $i * $i ) > $o)).
% 192.62/192.95 tff(1,assumption,(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))), introduced(assumption)).
% 192.62/192.95 tff(2,plain,
% 192.62/192.95 (^[B: $i, C: $i, D: $i] : refl((~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C)))) <=> (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C)))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(3,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C)))) <=> ![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[2])).
% 192.62/192.95 tff(4,plain,
% 192.62/192.95 (^[B: $i, C: $i, D: $i] : trans(trans(monotonicity(rewrite((member(D, B) & member(D, C)) <=> (~((~member(D, B)) | (~member(D, C))))), ((member(D, intersection(B, C)) <=> (member(D, B) & member(D, C))) <=> (member(D, intersection(B, C)) <=> (~((~member(D, B)) | (~member(D, C))))))), rewrite((member(D, intersection(B, C)) <=> (~((~member(D, B)) | (~member(D, C))))) <=> (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))), ((member(D, intersection(B, C)) <=> (member(D, B) & member(D, C))) <=> (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C)))))), rewrite((~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C)))) <=> (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))), ((member(D, intersection(B, C)) <=> (member(D, B) & member(D, C))) <=> (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(5,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C))) <=> ![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[4])).
% 192.62/192.95 tff(6,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C))) <=> ![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C)))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(7,axiom,(![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersection_defn')).
% 192.62/192.95 tff(8,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[7, 6])).
% 192.62/192.95 tff(9,plain,(
% 192.62/192.95 ![B: $i, C: $i, D: $i] : (member(D, intersection(B, C)) <=> (member(D, B) & member(D, C)))),
% 192.62/192.95 inference(skolemize,[status(sab)],[8])).
% 192.62/192.95 tff(10,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[9, 5])).
% 192.62/192.95 tff(11,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[10, 3])).
% 192.62/192.95 tff(12,plain,
% 192.62/192.95 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))))),
% 192.62/192.95 inference(quant_inst,[status(thm)],[])).
% 192.62/192.95 tff(13,plain,
% 192.62/192.95 ($false),
% 192.62/192.95 inference(unit_resolution,[status(thm)],[12, 11, 1])).
% 192.62/192.95 tff(14,plain,(~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.95 tff(15,assumption,(~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))), introduced(assumption)).
% 192.62/192.95 tff(16,plain,
% 192.62/192.95 (^[B: $i, C: $i, D: $i] : refl((member(D, union(B, C)) <=> (member(D, C) | member(D, B))) <=> (member(D, union(B, C)) <=> (member(D, C) | member(D, B))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(17,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B))) <=> ![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[16])).
% 192.62/192.95 tff(18,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B))) <=> ![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(19,plain,
% 192.62/192.95 (^[B: $i, C: $i, D: $i] : rewrite((member(D, union(B, C)) <=> (member(D, B) | member(D, C))) <=> (member(D, union(B, C)) <=> (member(D, C) | member(D, B))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(20,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, B) | member(D, C))) <=> ![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[19])).
% 192.62/192.95 tff(21,axiom,(![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, B) | member(D, C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','union_defn')).
% 192.62/192.95 tff(22,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[21, 20])).
% 192.62/192.95 tff(23,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[22, 18])).
% 192.62/192.95 tff(24,plain,(
% 192.62/192.95 ![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(skolemize,[status(sab)],[23])).
% 192.62/192.95 tff(25,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[24, 17])).
% 192.62/192.95 tff(26,plain,
% 192.62/192.95 ((~![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))) | (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))),
% 192.62/192.95 inference(quant_inst,[status(thm)],[])).
% 192.62/192.95 tff(27,plain,
% 192.62/192.95 ($false),
% 192.62/192.95 inference(unit_resolution,[status(thm)],[26, 25, 15])).
% 192.62/192.95 tff(28,plain,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.95 tff(29,plain,
% 192.62/192.95 (^[B: $i, C: $i] : refl((intersection(B, C) = intersection(C, B)) <=> (intersection(B, C) = intersection(C, B)))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(30,plain,
% 192.62/192.95 (![B: $i, C: $i] : (intersection(B, C) = intersection(C, B)) <=> ![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[29])).
% 192.62/192.95 tff(31,plain,
% 192.62/192.95 (![B: $i, C: $i] : (intersection(B, C) = intersection(C, B)) <=> ![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(32,axiom,(![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','commutativity_of_intersection')).
% 192.62/192.95 tff(33,plain,
% 192.62/192.95 (![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[32, 31])).
% 192.62/192.95 tff(34,plain,(
% 192.62/192.95 ![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))),
% 192.62/192.95 inference(skolemize,[status(sab)],[33])).
% 192.62/192.95 tff(35,plain,
% 192.62/192.95 (![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[34, 30])).
% 192.62/192.95 tff(36,plain,
% 192.62/192.95 ((~![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))) | (intersection(D!2, C!3) = intersection(C!3, D!2))),
% 192.62/192.95 inference(quant_inst,[status(thm)],[])).
% 192.62/192.95 tff(37,plain,
% 192.62/192.95 (intersection(D!2, C!3) = intersection(C!3, D!2)),
% 192.62/192.95 inference(unit_resolution,[status(thm)],[36, 35])).
% 192.62/192.95 tff(38,plain,
% 192.62/192.95 (intersection(C!3, D!2) = intersection(D!2, C!3)),
% 192.62/192.95 inference(symmetry,[status(thm)],[37])).
% 192.62/192.95 tff(39,plain,
% 192.62/192.95 (union(intersection(C!3, D!2), B!4) = union(intersection(D!2, C!3), B!4)),
% 192.62/192.95 inference(monotonicity,[status(thm)],[38])).
% 192.62/192.95 tff(40,plain,
% 192.62/192.95 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))),
% 192.62/192.95 inference(monotonicity,[status(thm)],[39])).
% 192.62/192.95 tff(41,plain,
% 192.62/192.95 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))),
% 192.62/192.95 inference(symmetry,[status(thm)],[40])).
% 192.62/192.95 tff(42,plain,
% 192.62/192.95 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))) <=> (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)))),
% 192.62/192.95 inference(monotonicity,[status(thm)],[41])).
% 192.62/192.95 tff(43,assumption,(~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))), introduced(assumption)).
% 192.62/192.95 tff(44,plain,
% 192.62/192.95 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(45,plain,
% 192.62/192.95 ((~(~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))) <=> (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(46,plain,
% 192.62/192.95 ((~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))) <=> (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(47,plain,
% 192.62/192.95 (((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))) <=> (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(48,plain,
% 192.62/192.95 (((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(49,plain,
% 192.62/192.95 ((((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))) <=> ((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))),
% 192.62/192.95 inference(monotonicity,[status(thm)],[48])).
% 192.62/192.95 tff(50,plain,
% 192.62/192.95 ((((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))) <=> (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[49, 47])).
% 192.62/192.95 tff(51,plain,
% 192.62/192.95 ((((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))) <=> (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[50, 46])).
% 192.62/192.95 tff(52,plain,
% 192.62/192.95 ((~(((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))) <=> (~(~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))))),
% 192.62/192.95 inference(monotonicity,[status(thm)],[51])).
% 192.62/192.95 tff(53,plain,
% 192.62/192.95 ((~(((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))) <=> (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))),
% 192.62/192.95 inference(transitivity,[status(thm)],[52, 45])).
% 192.62/192.95 tff(54,plain,
% 192.62/192.95 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(monotonicity,[status(thm)],[53])).
% 192.62/192.95 tff(55,plain,
% 192.62/192.95 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[54, 44])).
% 192.62/192.95 tff(56,plain,
% 192.62/192.95 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2)) | (~member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2))) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.95 inference(quant_inst,[status(thm)],[])).
% 192.62/192.95 tff(57,plain,
% 192.62/192.95 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[56, 55])).
% 192.62/192.95 tff(58,plain,
% 192.62/192.95 ($false),
% 192.62/192.95 inference(unit_resolution,[status(thm)],[57, 11, 43])).
% 192.62/192.95 tff(59,plain,(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.95 tff(60,plain,
% 192.62/192.95 (^[B: $i, C: $i, D: $i] : refl((~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(61,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[60])).
% 192.62/192.95 tff(62,plain,
% 192.62/192.95 (![B: $i, C: $i] : ![D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(pull_quant,[status(thm)],[])).
% 192.62/192.95 tff(63,plain,
% 192.62/192.95 (^[B: $i, C: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(pull_quant(((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) <=> ![D: $i] : ((~(B = C)) | (member(D, B) <=> member(D, C)))), ((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) <=> (~![D: $i] : ((~(B = C)) | (member(D, B) <=> member(D, C)))))), pull_quant((~![D: $i] : ((~(B = C)) | (member(D, B) <=> member(D, C)))) <=> ?[D: $i] : (~((~(B = C)) | (member(D, B) <=> member(D, C))))), ((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) <=> ?[D: $i] : (~((~(B = C)) | (member(D, B) <=> member(D, C)))))), (((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))) <=> (?[D: $i] : (~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))), pull_quant((?[D: $i] : (~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))) <=> ?[D: $i] : ((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))), (((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))) <=> ?[D: $i] : ((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))), ((~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> (~?[D: $i] : ((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))))), pull_quant((~?[D: $i] : ((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))), ((~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(64,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i] : ![D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[63])).
% 192.62/192.95 tff(65,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[64, 62])).
% 192.62/192.95 tff(66,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[65, 61])).
% 192.62/192.95 tff(67,plain,
% 192.62/192.95 (^[B: $i, C: $i] : rewrite((~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(68,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[67])).
% 192.62/192.95 tff(69,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))) <=> ![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(transitivity,[status(thm)],[68, 66])).
% 192.62/192.95 tff(70,plain,
% 192.62/192.95 (^[B: $i, C: $i] : trans(monotonicity(rewrite(((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) <=> ((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))), trans(monotonicity(rewrite((~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))) <=> (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))), (((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))) <=> ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))), rewrite(((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))) <=> ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))), (((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))) <=> ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))), ((((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))) <=> (((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))))), rewrite((((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))) <=> (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))), ((((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))) <=> (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))))),
% 192.62/192.95 inference(bind,[status(th)],[])).
% 192.62/192.95 tff(71,plain,
% 192.62/192.95 (![B: $i, C: $i] : (((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C))))) <=> ![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(quant_intro,[status(thm)],[70])).
% 192.62/192.95 tff(72,plain,
% 192.62/192.95 (![B: $i, C: $i] : ((B = C) <=> ![D: $i] : (member(D, B) <=> member(D, C))) <=> ![B: $i, C: $i] : ((B = C) <=> ![D: $i] : (member(D, B) <=> member(D, C)))),
% 192.62/192.95 inference(rewrite,[status(thm)],[])).
% 192.62/192.95 tff(73,axiom,(![B: $i, C: $i] : ((B = C) <=> ![D: $i] : (member(D, B) <=> member(D, C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','equal_member_defn')).
% 192.62/192.95 tff(74,plain,
% 192.62/192.95 (![B: $i, C: $i] : ((B = C) <=> ![D: $i] : (member(D, B) <=> member(D, C)))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[73, 72])).
% 192.62/192.95 tff(75,plain,(
% 192.62/192.95 ![B: $i, C: $i] : (((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C))) & ((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))),
% 192.62/192.95 inference(skolemize,[status(sab)],[74])).
% 192.62/192.95 tff(76,plain,
% 192.62/192.95 (![B: $i, C: $i] : (~((~((~(B = C)) | ![D: $i] : (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[75, 71])).
% 192.62/192.95 tff(77,plain,
% 192.62/192.95 (![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))),
% 192.62/192.95 inference(modus_ponens,[status(thm)],[76, 69])).
% 192.62/192.95 tff(78,plain,
% 192.62/192.95 ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(D!2 = intersection(D!2, D!2))) | (member(tptp_fun_D_0(B!4, union(D!2, B!4)), D!2) <=> member(tptp_fun_D_0(B!4, union(D!2, B!4)), intersection(D!2, D!2))))) | (~((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))))))),
% 192.62/192.95 inference(quant_inst,[status(thm)],[])).
% 192.62/192.95 tff(79,plain,
% 192.62/192.95 (~((~((~(D!2 = intersection(D!2, D!2))) | (member(tptp_fun_D_0(B!4, union(D!2, B!4)), D!2) <=> member(tptp_fun_D_0(B!4, union(D!2, B!4)), intersection(D!2, D!2))))) | (~((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))))))),
% 192.62/192.95 inference(unit_resolution,[status(thm)],[78, 77])).
% 192.62/192.95 tff(80,plain,
% 192.62/192.95 (((~((~(D!2 = intersection(D!2, D!2))) | (member(tptp_fun_D_0(B!4, union(D!2, B!4)), D!2) <=> member(tptp_fun_D_0(B!4, union(D!2, B!4)), intersection(D!2, D!2))))) | (~((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))))) | ((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))))),
% 192.62/192.95 inference(tautology,[status(thm)],[])).
% 192.62/192.95 tff(81,plain,
% 192.62/192.95 ((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[80, 79])).
% 192.62/192.96 tff(82,plain,
% 192.62/192.96 ((~((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2)))))) | (D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.96 inference(tautology,[status(thm)],[])).
% 192.62/192.96 tff(83,plain,
% 192.62/192.96 ((D!2 = intersection(D!2, D!2)) | (~(member(tptp_fun_D_1(intersection(D!2, D!2), D!2), D!2) <=> member(tptp_fun_D_1(intersection(D!2, D!2), D!2), intersection(D!2, D!2))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[82, 81])).
% 192.62/192.96 tff(84,plain,
% 192.62/192.96 (D!2 = intersection(D!2, D!2)),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[83, 59])).
% 192.62/192.96 tff(85,plain,
% 192.62/192.96 (intersection(D!2, D!2) = D!2),
% 192.62/192.96 inference(symmetry,[status(thm)],[84])).
% 192.62/192.96 tff(86,plain,
% 192.62/192.96 (union(intersection(D!2, D!2), B!4) = union(D!2, B!4)),
% 192.62/192.96 inference(monotonicity,[status(thm)],[85])).
% 192.62/192.96 tff(87,plain,
% 192.62/192.96 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[86])).
% 192.62/192.96 tff(88,plain,
% 192.62/192.96 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4))),
% 192.62/192.96 inference(symmetry,[status(thm)],[87])).
% 192.62/192.96 tff(89,plain,
% 192.62/192.96 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))) <=> (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[88])).
% 192.62/192.96 tff(90,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(91,plain,
% 192.62/192.96 (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[90, 11])).
% 192.62/192.96 tff(92,assumption,(~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))), introduced(assumption)).
% 192.62/192.96 tff(93,plain,
% 192.62/192.96 (^[B: $i, C: $i] : refl((union(B, C) = union(C, B)) <=> (union(B, C) = union(C, B)))),
% 192.62/192.96 inference(bind,[status(th)],[])).
% 192.62/192.96 tff(94,plain,
% 192.62/192.96 (![B: $i, C: $i] : (union(B, C) = union(C, B)) <=> ![B: $i, C: $i] : (union(B, C) = union(C, B))),
% 192.62/192.96 inference(quant_intro,[status(thm)],[93])).
% 192.62/192.96 tff(95,plain,
% 192.62/192.96 (![B: $i, C: $i] : (union(B, C) = union(C, B)) <=> ![B: $i, C: $i] : (union(B, C) = union(C, B))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(96,axiom,(![B: $i, C: $i] : (union(B, C) = union(C, B))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','commutativity_of_union')).
% 192.62/192.96 tff(97,plain,
% 192.62/192.96 (![B: $i, C: $i] : (union(B, C) = union(C, B))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[96, 95])).
% 192.62/192.96 tff(98,plain,(
% 192.62/192.96 ![B: $i, C: $i] : (union(B, C) = union(C, B))),
% 192.62/192.96 inference(skolemize,[status(sab)],[97])).
% 192.62/192.96 tff(99,plain,
% 192.62/192.96 (![B: $i, C: $i] : (union(B, C) = union(C, B))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[98, 94])).
% 192.62/192.96 tff(100,plain,
% 192.62/192.96 ((~![B: $i, C: $i] : (union(B, C) = union(C, B))) | (union(B!4, D!2) = union(D!2, B!4))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(101,plain,
% 192.62/192.96 (union(B!4, D!2) = union(D!2, B!4)),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[100, 99])).
% 192.62/192.96 tff(102,plain,
% 192.62/192.96 (union(D!2, B!4) = union(B!4, D!2)),
% 192.62/192.96 inference(symmetry,[status(thm)],[101])).
% 192.62/192.96 tff(103,assumption,(~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))), introduced(assumption)).
% 192.62/192.96 tff(104,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(105,plain,
% 192.62/192.96 ((~(~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))) <=> (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(106,plain,
% 192.62/192.96 ((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) <=> (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(107,plain,
% 192.62/192.96 (((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))) <=> (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(108,plain,
% 192.62/192.96 (((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(109,plain,
% 192.62/192.96 ((((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))) <=> ((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[108])).
% 192.62/192.96 tff(110,plain,
% 192.62/192.96 ((((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))) <=> (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(transitivity,[status(thm)],[109, 107])).
% 192.62/192.96 tff(111,plain,
% 192.62/192.96 ((((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))) <=> (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(transitivity,[status(thm)],[110, 106])).
% 192.62/192.96 tff(112,plain,
% 192.62/192.96 ((~(((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) <=> (~(~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[111])).
% 192.62/192.96 tff(113,plain,
% 192.62/192.96 ((~(((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) <=> (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))),
% 192.62/192.96 inference(transitivity,[status(thm)],[112, 105])).
% 192.62/192.96 tff(114,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[113])).
% 192.62/192.96 tff(115,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))) <=> ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(transitivity,[status(thm)],[114, 104])).
% 192.62/192.96 tff(116,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3)) | (~member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3))) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(117,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[116, 115])).
% 192.62/192.96 tff(118,plain,
% 192.62/192.96 ($false),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[117, 11, 103])).
% 192.62/192.96 tff(119,plain,(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.96 tff(120,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(121,plain,
% 192.62/192.96 ((~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((C!3 = intersection(C!3, C!3)) | (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))))))) <=> (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(122,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((C!3 = intersection(C!3, C!3)) | (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))))))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[121])).
% 192.62/192.96 tff(123,plain,
% 192.62/192.96 (((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((C!3 = intersection(C!3, C!3)) | (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))))))) <=> ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))))))),
% 192.62/192.96 inference(transitivity,[status(thm)],[122, 120])).
% 192.62/192.96 tff(124,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((C!3 = intersection(C!3, C!3)) | (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3))))))))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(125,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))))))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[124, 123])).
% 192.62/192.96 tff(126,plain,
% 192.62/192.96 (~((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[125, 77])).
% 192.62/192.96 tff(127,plain,
% 192.62/192.96 (((~((~(C!3 = intersection(C!3, C!3))) | (member(tptp_fun_D_1(C!3, B!4), C!3) <=> member(tptp_fun_D_1(C!3, B!4), intersection(C!3, C!3))))) | (~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))))) | ((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))),
% 192.62/192.96 inference(tautology,[status(thm)],[])).
% 192.62/192.96 tff(128,plain,
% 192.62/192.96 ((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[127, 126])).
% 192.62/192.96 tff(129,plain,
% 192.62/192.96 ((~((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3)))) | (~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))),
% 192.62/192.96 inference(tautology,[status(thm)],[])).
% 192.62/192.96 tff(130,plain,
% 192.62/192.96 ((~(member(tptp_fun_D_1(intersection(C!3, C!3), C!3), C!3) <=> member(tptp_fun_D_1(intersection(C!3, C!3), C!3), intersection(C!3, C!3)))) | (C!3 = intersection(C!3, C!3))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[129, 128])).
% 192.62/192.96 tff(131,plain,
% 192.62/192.96 (C!3 = intersection(C!3, C!3)),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[130, 119])).
% 192.62/192.96 tff(132,plain,
% 192.62/192.96 (intersection(C!3, C!3) = C!3),
% 192.62/192.96 inference(symmetry,[status(thm)],[131])).
% 192.62/192.96 tff(133,plain,
% 192.62/192.96 (intersection(intersection(C!3, C!3), union(D!2, B!4)) = intersection(C!3, union(B!4, D!2))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[132, 102])).
% 192.62/192.96 tff(134,plain,
% 192.62/192.96 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[133])).
% 192.62/192.96 tff(135,plain,
% 192.62/192.96 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))),
% 192.62/192.96 inference(symmetry,[status(thm)],[134])).
% 192.62/192.96 tff(136,plain,
% 192.62/192.96 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))) <=> (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4))))),
% 192.62/192.96 inference(monotonicity,[status(thm)],[135])).
% 192.62/192.96 tff(137,plain,
% 192.62/192.96 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[92, 136])).
% 192.62/192.96 tff(138,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))), introduced(assumption)).
% 192.62/192.96 tff(139,plain,
% 192.62/192.96 ($false),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[138, 137])).
% 192.62/192.96 tff(140,plain,((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.96 tff(141,plain,
% 192.62/192.96 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[140, 92])).
% 192.62/192.96 tff(142,plain,
% 192.62/192.96 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))) | ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))),
% 192.62/192.96 inference(tautology,[status(thm)],[])).
% 192.62/192.96 tff(143,plain,
% 192.62/192.96 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))) | ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[142, 141])).
% 192.62/192.96 tff(144,plain,
% 192.62/192.96 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[143, 91])).
% 192.62/192.96 tff(145,plain,
% 192.62/192.96 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[26, 25])).
% 192.62/192.96 tff(146,assumption,((~((~(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2)))) | (member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))) | (~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))))), introduced(assumption)).
% 192.62/192.96 tff(147,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2)))) | (member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))) | (~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))))))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(148,plain,
% 192.62/192.96 ($false),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[147, 77, 146])).
% 192.62/192.96 tff(149,plain,(~((~((~(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2)))) | (member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))) | (~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.96 tff(150,plain,
% 192.62/192.96 (((~((~(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2)))) | (member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(union(D!2, B!4), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))) | (~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))))) | ((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))))),
% 192.62/192.96 inference(tautology,[status(thm)],[])).
% 192.62/192.96 tff(151,plain,
% 192.62/192.96 ((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[150, 149])).
% 192.62/192.96 tff(152,plain,
% 192.62/192.96 ((~![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))) | (intersection(union(B!4, D!2), C!3) = intersection(C!3, union(B!4, D!2)))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(153,plain,
% 192.62/192.96 (intersection(union(B!4, D!2), C!3) = intersection(C!3, union(B!4, D!2))),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[152, 35])).
% 192.62/192.96 tff(154,plain,
% 192.62/192.96 (intersection(C!3, union(B!4, D!2)) = intersection(union(B!4, D!2), C!3)),
% 192.62/192.96 inference(symmetry,[status(thm)],[153])).
% 192.62/192.96 tff(155,assumption,(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))), introduced(assumption)).
% 192.62/192.96 tff(156,plain,
% 192.62/192.96 ((~![B: $i, C: $i] : (union(B, C) = union(C, B))) | (union(B!4, intersection(D!2, C!3)) = union(intersection(D!2, C!3), B!4))),
% 192.62/192.96 inference(quant_inst,[status(thm)],[])).
% 192.62/192.96 tff(157,plain,
% 192.62/192.96 (union(B!4, intersection(D!2, C!3)) = union(intersection(D!2, C!3), B!4)),
% 192.62/192.96 inference(unit_resolution,[status(thm)],[156, 99])).
% 192.62/192.96 tff(158,plain,
% 192.62/192.96 (union(B!4, intersection(D!2, C!3)) = intersection(union(B!4, D!2), C!3)),
% 192.62/192.96 inference(transitivity,[status(thm)],[157, 155, 154])).
% 192.62/192.96 tff(159,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C)))) <=> (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(160,plain,
% 192.62/192.96 ((~![B: $i, C: $i, D: $i] : (subset(B, C) => (union(B, intersection(D, C)) = intersection(union(B, D), C)))) <=> (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C))))),
% 192.62/192.96 inference(rewrite,[status(thm)],[])).
% 192.62/192.96 tff(161,axiom,(~![B: $i, C: $i, D: $i] : (subset(B, C) => (union(B, intersection(D, C)) = intersection(union(B, D), C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_th44')).
% 192.62/192.96 tff(162,plain,
% 192.62/192.96 (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C)))),
% 192.62/192.96 inference(modus_ponens,[status(thm)],[161, 160])).
% 192.62/192.96 tff(163,plain,
% 192.62/192.96 (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C)))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[162, 159])).
% 192.62/192.97 tff(164,plain,
% 192.62/192.97 (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C)))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[163, 159])).
% 192.62/192.97 tff(165,plain,
% 192.62/192.97 (~![B: $i, C: $i, D: $i] : ((~subset(B, C)) | (union(B, intersection(D, C)) = intersection(union(B, D), C)))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[164, 159])).
% 192.62/192.97 tff(166,plain,(
% 192.62/192.97 ~((~subset(B!4, C!3)) | (union(B!4, intersection(D!2, C!3)) = intersection(union(B!4, D!2), C!3)))),
% 192.62/192.97 inference(skolemize,[status(sab)],[165])).
% 192.62/192.97 tff(167,plain,
% 192.62/192.97 (~(union(B!4, intersection(D!2, C!3)) = intersection(union(B!4, D!2), C!3))),
% 192.62/192.97 inference(or_elim,[status(thm)],[166])).
% 192.62/192.97 tff(168,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[167, 158])).
% 192.62/192.97 tff(169,plain,(~(union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2)))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(170,plain,
% 192.62/192.97 ((~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))))) | (union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(171,plain,
% 192.62/192.97 ((~((union(intersection(D!2, C!3), B!4) = intersection(C!3, union(B!4, D!2))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[170, 169])).
% 192.62/192.97 tff(172,plain,
% 192.62/192.97 (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[171, 151])).
% 192.62/192.97 tff(173,plain,
% 192.62/192.97 ((member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(174,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[173, 172])).
% 192.62/192.97 tff(175,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[174, 92])).
% 192.62/192.97 tff(176,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))), introduced(assumption)).
% 192.62/192.97 tff(177,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[176, 41])).
% 192.62/192.97 tff(178,assumption,(~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))), introduced(assumption)).
% 192.62/192.97 tff(179,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[178, 177])).
% 192.62/192.97 tff(180,plain,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(181,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[180, 175])).
% 192.62/192.97 tff(182,plain,
% 192.62/192.97 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))) | (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(183,plain,
% 192.62/192.97 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))) | (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[182, 181])).
% 192.62/192.97 tff(184,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[183, 145])).
% 192.62/192.97 tff(185,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))), introduced(assumption)).
% 192.62/192.97 tff(186,assumption,(~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))), introduced(assumption)).
% 192.62/192.97 tff(187,assumption,(~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))), introduced(assumption)).
% 192.62/192.97 tff(188,assumption,((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))), introduced(assumption)).
% 192.62/192.97 tff(189,assumption,(((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))), introduced(assumption)).
% 192.62/192.97 tff(190,plain,
% 192.62/192.97 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))),
% 192.62/192.97 inference(quant_inst,[status(thm)],[])).
% 192.62/192.97 tff(191,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[190, 11, 189])).
% 192.62/192.97 tff(192,plain,(~(((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(193,plain,
% 192.62/192.97 ((((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))) | (~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(194,plain,
% 192.62/192.97 ((~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[193, 192])).
% 192.62/192.97 tff(195,plain,
% 192.62/192.97 (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[194, 188])).
% 192.62/192.97 tff(196,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))),
% 192.62/192.97 inference(monotonicity,[status(thm)],[131])).
% 192.62/192.97 tff(197,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3)),
% 192.62/192.97 inference(symmetry,[status(thm)],[196])).
% 192.62/192.97 tff(198,plain,
% 192.62/192.97 ((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))) <=> (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3))),
% 192.62/192.97 inference(monotonicity,[status(thm)],[197])).
% 192.62/192.97 tff(199,assumption,(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)), introduced(assumption)).
% 192.62/192.97 tff(200,plain,
% 192.62/192.97 ((~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(201,plain,
% 192.62/192.97 (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[200, 199, 188])).
% 192.62/192.97 tff(202,plain,
% 192.62/192.97 (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3)),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[201, 198])).
% 192.62/192.97 tff(203,plain,
% 192.62/192.97 (^[B: $i, C: $i] : refl((~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))) <=> (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))))),
% 192.62/192.97 inference(bind,[status(th)],[])).
% 192.62/192.97 tff(204,plain,
% 192.62/192.97 (![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))) <=> ![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(quant_intro,[status(thm)],[203])).
% 192.62/192.97 tff(205,plain,
% 192.62/192.97 (^[B: $i, C: $i] : rewrite((~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))) <=> (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))))),
% 192.62/192.97 inference(bind,[status(th)],[])).
% 192.62/192.97 tff(206,plain,
% 192.62/192.97 (![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))) <=> ![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(quant_intro,[status(thm)],[205])).
% 192.62/192.97 tff(207,plain,
% 192.62/192.97 (![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))) <=> ![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(transitivity,[status(thm)],[206, 204])).
% 192.62/192.97 tff(208,plain,
% 192.62/192.97 (^[B: $i, C: $i] : trans(monotonicity(rewrite(((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) <=> ((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))), rewrite((subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))) <=> (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))), ((((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))) <=> (((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))))), rewrite((((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))) <=> (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))), ((((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))) <=> (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))))),
% 192.62/192.97 inference(bind,[status(th)],[])).
% 192.62/192.97 tff(209,plain,
% 192.62/192.97 (![B: $i, C: $i] : (((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C))))) <=> ![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(quant_intro,[status(thm)],[208])).
% 192.62/192.97 tff(210,plain,
% 192.62/192.97 (![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C))) <=> ![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C)))),
% 192.62/192.97 inference(rewrite,[status(thm)],[])).
% 192.62/192.97 tff(211,plain,
% 192.62/192.97 (^[B: $i, C: $i] : rewrite((subset(B, C) <=> ![D: $i] : (member(D, B) => member(D, C))) <=> (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C))))),
% 192.62/192.97 inference(bind,[status(th)],[])).
% 192.62/192.97 tff(212,plain,
% 192.62/192.97 (![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : (member(D, B) => member(D, C))) <=> ![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C)))),
% 192.62/192.97 inference(quant_intro,[status(thm)],[211])).
% 192.62/192.97 tff(213,axiom,(![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : (member(D, B) => member(D, C)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','subset_defn')).
% 192.62/192.97 tff(214,plain,
% 192.62/192.97 (![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C)))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[213, 212])).
% 192.62/192.97 tff(215,plain,
% 192.62/192.97 (![B: $i, C: $i] : (subset(B, C) <=> ![D: $i] : ((~member(D, B)) | member(D, C)))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[214, 210])).
% 192.62/192.97 tff(216,plain,(
% 192.62/192.97 ![B: $i, C: $i] : (((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C))) & (subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))),
% 192.62/192.97 inference(skolemize,[status(sab)],[215])).
% 192.62/192.97 tff(217,plain,
% 192.62/192.97 (![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[216, 209])).
% 192.62/192.97 tff(218,plain,
% 192.62/192.97 (![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[217, 207])).
% 192.62/192.97 tff(219,plain,
% 192.62/192.97 ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))) | (~(subset(B!4, C!3) | (~((~member(tptp_fun_D_0(C!3, B!4), B!4)) | member(tptp_fun_D_0(C!3, B!4), C!3)))))))),
% 192.62/192.97 inference(quant_inst,[status(thm)],[])).
% 192.62/192.97 tff(220,plain,
% 192.62/192.97 (~((~((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))) | (~(subset(B!4, C!3) | (~((~member(tptp_fun_D_0(C!3, B!4), B!4)) | member(tptp_fun_D_0(C!3, B!4), C!3))))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[219, 218])).
% 192.62/192.97 tff(221,plain,
% 192.62/192.97 (((~((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))) | (~(subset(B!4, C!3) | (~((~member(tptp_fun_D_0(C!3, B!4), B!4)) | member(tptp_fun_D_0(C!3, B!4), C!3)))))) | ((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(222,plain,
% 192.62/192.97 ((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[221, 220])).
% 192.62/192.97 tff(223,plain,
% 192.62/192.97 (subset(B!4, C!3)),
% 192.62/192.97 inference(or_elim,[status(thm)],[166])).
% 192.62/192.97 tff(224,plain,
% 192.62/192.97 ((~((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))) | (~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(225,plain,
% 192.62/192.97 ((~((~subset(B!4, C!3)) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3)))) | ![D: $i] : ((~member(D, B!4)) | member(D, C!3))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[224, 223])).
% 192.62/192.97 tff(226,plain,
% 192.62/192.97 (![D: $i] : ((~member(D, B!4)) | member(D, C!3))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[225, 222])).
% 192.62/192.97 tff(227,plain,
% 192.62/192.97 (((~![D: $i] : ((~member(D, B!4)) | member(D, C!3))) | ((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3))) <=> ((~![D: $i] : ((~member(D, B!4)) | member(D, C!3))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3))),
% 192.62/192.97 inference(rewrite,[status(thm)],[])).
% 192.62/192.97 tff(228,plain,
% 192.62/192.97 ((~![D: $i] : ((~member(D, B!4)) | member(D, C!3))) | ((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3))),
% 192.62/192.97 inference(quant_inst,[status(thm)],[])).
% 192.62/192.97 tff(229,plain,
% 192.62/192.97 ((~![D: $i] : ((~member(D, B!4)) | member(D, C!3))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3)),
% 192.62/192.97 inference(modus_ponens,[status(thm)],[228, 227])).
% 192.62/192.97 tff(230,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), C!3)),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[229, 226, 199])).
% 192.62/192.97 tff(231,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[230, 202])).
% 192.62/192.97 tff(232,plain,((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(233,plain,
% 192.62/192.97 (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[232, 188])).
% 192.62/192.97 tff(234,plain,
% 192.62/192.97 ((member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(235,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[234, 233, 195, 187])).
% 192.62/192.97 tff(236,plain,((~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))))) | (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(237,plain,
% 192.62/192.97 (~((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[236, 187])).
% 192.62/192.97 tff(238,plain,
% 192.62/192.97 (((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(239,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[238, 237])).
% 192.62/192.97 tff(240,plain,
% 192.62/192.97 ((((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))) | ((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(241,plain,
% 192.62/192.97 (((~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(C!3, C!3)))) | member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[240, 192])).
% 192.62/192.97 tff(242,plain,
% 192.62/192.97 (member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[241, 237])).
% 192.62/192.97 tff(243,plain,
% 192.62/192.97 ((member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4)) | (~member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(244,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[243, 242, 239, 187])).
% 192.62/192.97 tff(245,plain,(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(246,assumption,((~((~(B!4 = intersection(B!4, intersection(C!3, C!3)))) | (member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), B!4) <=> member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), intersection(B!4, intersection(C!3, C!3)))))) | (~((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))))), introduced(assumption)).
% 192.62/192.97 tff(247,plain,
% 192.62/192.97 ((~![B: $i, C: $i, D: $i] : (~((~((~(B = C)) | (member(D, B) <=> member(D, C)))) | (~((B = C) | (~(member(tptp_fun_D_1(C, B), B) <=> member(tptp_fun_D_1(C, B), C)))))))) | (~((~((~(B!4 = intersection(B!4, intersection(C!3, C!3)))) | (member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), B!4) <=> member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), intersection(B!4, intersection(C!3, C!3)))))) | (~((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))))))),
% 192.62/192.97 inference(quant_inst,[status(thm)],[])).
% 192.62/192.97 tff(248,plain,
% 192.62/192.97 ($false),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[247, 77, 246])).
% 192.62/192.97 tff(249,plain,(~((~((~(B!4 = intersection(B!4, intersection(C!3, C!3)))) | (member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), B!4) <=> member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), intersection(B!4, intersection(C!3, C!3)))))) | (~((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))))))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.97 tff(250,plain,
% 192.62/192.97 (((~((~(B!4 = intersection(B!4, intersection(C!3, C!3)))) | (member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), B!4) <=> member(tptp_fun_D_1(intersection(C!3, C!3), union(D!2, intersection(C!3, D!2))), intersection(B!4, intersection(C!3, C!3)))))) | (~((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))))) | ((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))))),
% 192.62/192.97 inference(tautology,[status(thm)],[])).
% 192.62/192.97 tff(251,plain,
% 192.62/192.97 ((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))),
% 192.62/192.97 inference(unit_resolution,[status(thm)],[250, 249])).
% 192.62/192.97 tff(252,plain,
% 192.62/192.97 ((~((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3))))))) | (B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))),
% 192.62/192.98 inference(tautology,[status(thm)],[])).
% 192.62/192.98 tff(253,plain,
% 192.62/192.98 ((B!4 = intersection(B!4, intersection(C!3, C!3))) | (~(member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), B!4) <=> member(tptp_fun_D_1(intersection(B!4, intersection(C!3, C!3)), B!4), intersection(B!4, intersection(C!3, C!3)))))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[252, 251])).
% 192.62/192.98 tff(254,plain,
% 192.62/192.98 (B!4 = intersection(B!4, intersection(C!3, C!3))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[253, 245])).
% 192.62/192.98 tff(255,plain,
% 192.62/192.98 (intersection(B!4, intersection(C!3, C!3)) = B!4),
% 192.62/192.98 inference(symmetry,[status(thm)],[254])).
% 192.62/192.98 tff(256,plain,
% 192.62/192.98 ((~![B: $i, C: $i] : (intersection(B, C) = intersection(C, B))) | (intersection(intersection(C!3, C!3), B!4) = intersection(B!4, intersection(C!3, C!3)))),
% 192.62/192.98 inference(quant_inst,[status(thm)],[])).
% 192.62/192.98 tff(257,plain,
% 192.62/192.98 (intersection(intersection(C!3, C!3), B!4) = intersection(B!4, intersection(C!3, C!3))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[256, 35])).
% 192.62/192.98 tff(258,plain,
% 192.62/192.98 (intersection(intersection(C!3, C!3), B!4) = B!4),
% 192.62/192.98 inference(transitivity,[status(thm)],[257, 255])).
% 192.62/192.98 tff(259,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)),
% 192.62/192.98 inference(monotonicity,[status(thm)],[258])).
% 192.62/192.98 tff(260,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))),
% 192.62/192.98 inference(symmetry,[status(thm)],[259])).
% 192.62/192.98 tff(261,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)), introduced(assumption)).
% 192.62/192.98 tff(262,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))),
% 192.62/192.98 inference(modus_ponens,[status(thm)],[261, 260])).
% 192.62/192.98 tff(263,plain,
% 192.62/192.98 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))))),
% 192.62/192.98 inference(quant_inst,[status(thm)],[])).
% 192.62/192.98 tff(264,plain,
% 192.62/192.98 (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4)))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[263, 11])).
% 192.62/192.98 tff(265,plain,
% 192.62/192.98 (((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))),
% 192.62/192.98 inference(tautology,[status(thm)],[])).
% 192.62/192.98 tff(266,plain,
% 192.62/192.98 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[265, 186])).
% 192.62/192.98 tff(267,plain,
% 192.62/192.98 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))) | (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4)))),
% 192.62/192.98 inference(tautology,[status(thm)],[])).
% 192.62/192.98 tff(268,plain,
% 192.62/192.98 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4)))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[267, 266])).
% 192.62/192.98 tff(269,plain,
% 192.62/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), B!4))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[268, 264])).
% 192.62/192.98 tff(270,plain,
% 192.62/192.98 ($false),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[269, 262])).
% 192.62/192.98 tff(271,plain,((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))), inference(lemma,lemma(discharge,[]))).
% 192.62/192.98 tff(272,plain,
% 192.62/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[271, 186])).
% 192.62/192.98 tff(273,plain,
% 192.62/192.98 (intersection(intersection(C!3, C!3), intersection(D!2, D!2)) = intersection(C!3, D!2)),
% 192.62/192.98 inference(monotonicity,[status(thm)],[132, 85])).
% 192.62/192.98 tff(274,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.62/192.98 inference(monotonicity,[status(thm)],[273])).
% 192.62/192.98 tff(275,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.62/192.98 inference(symmetry,[status(thm)],[274])).
% 192.62/192.98 tff(276,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))), introduced(assumption)).
% 192.62/192.98 tff(277,plain,
% 192.62/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.62/192.98 inference(modus_ponens,[status(thm)],[276, 275])).
% 192.62/192.98 tff(278,plain,
% 192.62/192.98 (~(((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.62/192.98 inference(unit_resolution,[status(thm)],[12, 11])).
% 192.62/192.98 tff(279,plain,
% 192.62/192.98 (((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(280,plain,
% 192.68/192.98 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[279, 186])).
% 192.68/192.98 tff(281,plain,
% 192.68/192.98 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))) | (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(282,plain,
% 192.68/192.98 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[281, 280])).
% 192.68/192.98 tff(283,plain,
% 192.68/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[282, 278])).
% 192.68/192.98 tff(284,plain,
% 192.68/192.98 ($false),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[283, 277])).
% 192.68/192.98 tff(285,plain,((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))), inference(lemma,lemma(discharge,[]))).
% 192.68/192.98 tff(286,plain,
% 192.68/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[285, 186])).
% 192.68/192.98 tff(287,plain,
% 192.68/192.98 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(288,plain,
% 192.68/192.98 ($false),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[287, 286, 272, 185])).
% 192.68/192.98 tff(289,plain,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3)) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))), inference(lemma,lemma(discharge,[]))).
% 192.68/192.98 tff(290,plain,
% 192.68/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[289, 184])).
% 192.68/192.98 tff(291,plain,
% 192.68/192.98 ((~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(292,plain,
% 192.68/192.98 ((~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[291, 290])).
% 192.68/192.98 tff(293,plain,
% 192.68/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[292, 144])).
% 192.68/192.98 tff(294,plain,
% 192.68/192.98 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4))),
% 192.68/192.98 inference(modus_ponens,[status(thm)],[293, 89])).
% 192.68/192.98 tff(295,plain,
% 192.68/192.98 ((~![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))) | (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))),
% 192.68/192.98 inference(quant_inst,[status(thm)],[])).
% 192.68/192.98 tff(296,plain,
% 192.68/192.98 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[295, 25])).
% 192.68/192.98 tff(297,plain,
% 192.68/192.98 ((~![B: $i, C: $i, D: $i] : (~(((~member(D, B)) | (~member(D, C))) <=> member(D, intersection(B, C))))) | (~(((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))))),
% 192.68/192.98 inference(quant_inst,[status(thm)],[])).
% 192.68/192.98 tff(298,plain,
% 192.68/192.98 (~(((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[297, 11])).
% 192.68/192.98 tff(299,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))),
% 192.68/192.98 inference(monotonicity,[status(thm)],[273])).
% 192.68/192.98 tff(300,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2)) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/192.98 inference(symmetry,[status(thm)],[299])).
% 192.68/192.98 tff(301,assumption,(~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))), introduced(assumption)).
% 192.68/192.98 tff(302,plain,
% 192.68/192.98 (((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(303,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[302, 301])).
% 192.68/192.98 tff(304,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/192.98 inference(modus_ponens,[status(thm)],[303, 300])).
% 192.68/192.98 tff(305,plain,
% 192.68/192.98 ((((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(306,plain,
% 192.68/192.98 (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[305, 304, 298])).
% 192.68/192.98 tff(307,plain,
% 192.68/192.98 ((~![B: $i, C: $i, D: $i] : (member(D, union(B, C)) <=> (member(D, C) | member(D, B)))) | (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))))),
% 192.68/192.98 inference(quant_inst,[status(thm)],[])).
% 192.68/192.98 tff(308,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[307, 25])).
% 192.68/192.98 tff(309,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))),
% 192.68/192.98 inference(monotonicity,[status(thm)],[86])).
% 192.68/192.98 tff(310,plain,
% 192.68/192.98 (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)) <=> member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4))),
% 192.68/192.98 inference(symmetry,[status(thm)],[309])).
% 192.68/192.98 tff(311,plain,
% 192.68/192.98 ((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))) <=> (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)))),
% 192.68/192.98 inference(monotonicity,[status(thm)],[310])).
% 192.68/192.98 tff(312,plain,
% 192.68/192.98 (((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(313,plain,
% 192.68/192.98 (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[312, 301])).
% 192.68/192.98 tff(314,plain,
% 192.68/192.98 (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4))),
% 192.68/192.98 inference(modus_ponens,[status(thm)],[313, 311])).
% 192.68/192.98 tff(315,plain,
% 192.68/192.98 ((~(member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(intersection(D!2, D!2), B!4)) | (~(member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(316,plain,
% 192.68/192.98 (~(member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[315, 314, 308])).
% 192.68/192.98 tff(317,plain,
% 192.68/192.98 ((member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), B!4) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(318,plain,
% 192.68/192.98 (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[317, 316])).
% 192.68/192.98 tff(319,plain,
% 192.68/192.98 (((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, C!3))) | (~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2)))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(D!2, D!2))),
% 192.68/192.98 inference(tautology,[status(thm)],[])).
% 192.68/192.98 tff(320,plain,
% 192.68/192.98 ($false),
% 192.68/192.98 inference(unit_resolution,[status(thm)],[319, 318, 306])).
% 192.68/192.98 tff(321,plain,((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))), inference(lemma,lemma(discharge,[]))).
% 192.68/192.98 tff(322,plain,
% 192.68/192.98 (((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))))))) <=> ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))))))),
% 192.68/192.98 inference(rewrite,[status(thm)],[])).
% 192.68/192.98 tff(323,plain,
% 192.68/192.98 ((~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~(subset(intersection(C!3, D!2), union(D!2, B!4)) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))))))) <=> (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))))))),
% 192.68/192.98 inference(rewrite,[status(thm)],[])).
% 192.68/192.98 tff(324,plain,
% 192.68/192.98 (((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~(subset(intersection(C!3, D!2), union(D!2, B!4)) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))))))))) <=> ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))))))),
% 192.68/192.99 inference(monotonicity,[status(thm)],[323])).
% 192.68/192.99 tff(325,plain,
% 192.68/192.99 (((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~(subset(intersection(C!3, D!2), union(D!2, B!4)) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))))))))) <=> ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))))))),
% 192.68/192.99 inference(transitivity,[status(thm)],[324, 322])).
% 192.68/192.99 tff(326,plain,
% 192.68/192.99 ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~(subset(intersection(C!3, D!2), union(D!2, B!4)) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4))))))))),
% 192.68/192.99 inference(quant_inst,[status(thm)],[])).
% 192.68/192.99 tff(327,plain,
% 192.68/192.99 ((~![B: $i, C: $i] : (~((~((~subset(B, C)) | ![D: $i] : ((~member(D, B)) | member(D, C)))) | (~(subset(B, C) | (~((~member(tptp_fun_D_0(C, B), B)) | member(tptp_fun_D_0(C, B), C)))))))) | (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))))))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[326, 325])).
% 192.68/192.99 tff(328,plain,
% 192.68/192.99 (~((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[327, 218])).
% 192.68/192.99 tff(329,plain,
% 192.68/192.99 (((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))))) | ((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(330,plain,
% 192.68/192.99 ((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[329, 328])).
% 192.68/192.99 tff(331,plain,
% 192.68/192.99 ((~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4)))) | (~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(332,plain,
% 192.68/192.99 ((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[331, 330])).
% 192.68/192.99 tff(333,plain,
% 192.68/192.99 (subset(intersection(C!3, D!2), union(D!2, B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[332, 321])).
% 192.68/192.99 tff(334,plain,
% 192.68/192.99 (((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~((~((~member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), intersection(C!3, D!2))) | member(tptp_fun_D_0(union(D!2, B!4), intersection(C!3, D!2)), union(D!2, B!4)))) | subset(intersection(C!3, D!2), union(D!2, B!4))))) | ((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(335,plain,
% 192.68/192.99 ((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[334, 328])).
% 192.68/192.99 tff(336,plain,
% 192.68/192.99 ((~((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4))))) | (~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(337,plain,
% 192.68/192.99 ((~subset(intersection(C!3, D!2), union(D!2, B!4))) | ![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[336, 335])).
% 192.68/192.99 tff(338,plain,
% 192.68/192.99 (![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[337, 333])).
% 192.68/192.99 tff(339,plain,
% 192.68/192.99 (((~![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))) | ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> ((~![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))),
% 192.68/192.99 inference(rewrite,[status(thm)],[])).
% 192.68/192.99 tff(340,plain,
% 192.68/192.99 ((~![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))) | ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))),
% 192.68/192.99 inference(quant_inst,[status(thm)],[])).
% 192.68/192.99 tff(341,plain,
% 192.68/192.99 ((~![D: $i] : ((~member(D, intersection(C!3, D!2))) | member(D, union(D!2, B!4)))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[340, 339])).
% 192.68/192.99 tff(342,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[341, 338, 293])).
% 192.68/192.99 tff(343,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[287, 342, 184])).
% 192.68/192.99 tff(344,plain,
% 192.68/192.99 ((member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(345,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[344, 343])).
% 192.68/192.99 tff(346,plain,
% 192.68/192.99 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(347,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[346, 345, 296])).
% 192.68/192.99 tff(348,plain,
% 192.68/192.99 ($false),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[347, 294])).
% 192.68/192.99 tff(349,plain,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))), inference(lemma,lemma(discharge,[]))).
% 192.68/192.99 tff(350,plain,
% 192.68/192.99 ((member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4)) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2)))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(351,plain,
% 192.68/192.99 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, union(B!4, D!2))))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[350, 172])).
% 192.68/192.99 tff(352,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, C!3), B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[351, 349])).
% 192.68/192.99 tff(353,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[352, 42])).
% 192.68/192.99 tff(354,plain,
% 192.68/192.99 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(355,plain,
% 192.68/192.99 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(C!3, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))) | (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[354, 353])).
% 192.68/192.99 tff(356,plain,
% 192.68/192.99 (~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[355, 28])).
% 192.68/192.99 tff(357,plain,
% 192.68/192.99 ((member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2)))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(358,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[357, 356])).
% 192.68/192.99 tff(359,plain,
% 192.68/192.99 ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) <=> (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2))))),
% 192.68/192.99 inference(monotonicity,[status(thm)],[275])).
% 192.68/192.99 tff(360,assumption,(~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))), introduced(assumption)).
% 192.68/192.99 tff(361,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[360, 359])).
% 192.68/192.99 tff(362,assumption,(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))), introduced(assumption)).
% 192.68/192.99 tff(363,plain,
% 192.68/192.99 ($false),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[362, 361])).
% 192.68/192.99 tff(364,plain,((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))), inference(lemma,lemma(discharge,[]))).
% 192.68/192.99 tff(365,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[364, 358])).
% 192.68/192.99 tff(366,plain,
% 192.68/192.99 ((member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, D!2))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(367,plain,
% 192.68/192.99 (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4)),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[366, 356])).
% 192.68/192.99 tff(368,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[349, 135])).
% 192.68/192.99 tff(369,plain,
% 192.68/192.99 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))) | (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4))))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(370,plain,
% 192.68/192.99 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), union(D!2, B!4)))) | (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[369, 368])).
% 192.68/192.99 tff(371,plain,
% 192.68/192.99 (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[370, 91])).
% 192.68/192.99 tff(372,plain,
% 192.68/192.99 (((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(373,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4))),
% 192.68/192.99 inference(unit_resolution,[status(thm)],[372, 371])).
% 192.68/192.99 tff(374,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4))),
% 192.68/192.99 inference(modus_ponens,[status(thm)],[373, 88])).
% 192.68/192.99 tff(375,plain,
% 192.68/192.99 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4)) <=> (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(intersection(D!2, D!2), B!4))) | (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))),
% 192.68/192.99 inference(tautology,[status(thm)],[])).
% 192.68/192.99 tff(376,plain,
% 192.68/192.99 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[375, 374, 296])).
% 192.68/193.03 tff(377,plain,
% 192.68/193.03 ((~(member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))),
% 192.68/193.03 inference(tautology,[status(thm)],[])).
% 192.68/193.03 tff(378,plain,
% 192.68/193.03 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), B!4) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[377, 376])).
% 192.68/193.03 tff(379,plain,
% 192.68/193.03 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[378, 367])).
% 192.68/193.03 tff(380,plain,
% 192.68/193.03 (((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), union(D!2, B!4)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))),
% 192.68/193.03 inference(tautology,[status(thm)],[])).
% 192.68/193.03 tff(381,plain,
% 192.68/193.03 (member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[380, 371])).
% 192.68/193.03 tff(382,plain,
% 192.68/193.03 ((~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))),
% 192.68/193.03 inference(tautology,[status(thm)],[])).
% 192.68/193.03 tff(383,plain,
% 192.68/193.03 ((~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[382, 381])).
% 192.68/193.03 tff(384,plain,
% 192.68/193.03 (~((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2))))),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[383, 379])).
% 192.68/193.03 tff(385,plain,
% 192.68/193.03 ((((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) <=> member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))) | ((~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(C!3, C!3))) | (~member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(D!2, D!2)))) | member(tptp_fun_D_1(intersection(C!3, union(B!4, D!2)), union(intersection(D!2, C!3), B!4)), intersection(intersection(C!3, C!3), intersection(D!2, D!2)))),
% 192.68/193.03 inference(tautology,[status(thm)],[])).
% 192.68/193.03 tff(386,plain,
% 192.68/193.03 ($false),
% 192.68/193.03 inference(unit_resolution,[status(thm)],[385, 384, 365, 14])).
% 192.68/193.03 % SZS output end Proof
% 192.68/193.04 % E exiting
%------------------------------------------------------------------------------