Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SEU417+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n005.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sat Jun 21 05:27:52 AM UTC 2025

% Result   : Theorem 2.45s 2.65s
% Output   : Proof 2.45s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : SEU417+1 : TPTP v9.0.0. Released v3.4.0.
% 0.00/0.12  % Command    : run_E %s %d THM
% 0.12/0.33  % Computer : n005.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 07:10:05 EDT 2025
% 0.12/0.33  % CPUTime    : 
% 2.45/2.65  % SZS status Theorem
% 2.45/2.65  % SZS output start Proof
% 2.45/2.65  tff(m1_subset_1_type, type, (
% 2.45/2.65     m1_subset_1: ( $i * $i ) > $o)).
% 2.45/2.65  tff(k1_zfmisc_1_type, type, (
% 2.45/2.65     k1_zfmisc_1: $i > $i)).
% 2.45/2.65  tff(tptp_fun_A_1_type, type, (
% 2.45/2.65     tptp_fun_A_1: $i)).
% 2.45/2.65  tff(k2_xboole_0_type, type, (
% 2.45/2.65     k2_xboole_0: ( $i * $i ) > $i)).
% 2.45/2.65  tff(tptp_fun_B_0_type, type, (
% 2.45/2.65     tptp_fun_B_0: $i)).
% 2.45/2.65  tff(r1_tarski_type, type, (
% 2.45/2.65     r1_tarski: ( $i * $i ) > $o)).
% 2.45/2.65  tff(k8_setfam_1_type, type, (
% 2.45/2.65     k8_setfam_1: ( $i * $i ) > $i)).
% 2.45/2.65  tff(k1_relset_2_type, type, (
% 2.45/2.65     k1_relset_2: ( $i * $i * $i ) > $i)).
% 2.45/2.65  tff(tptp_fun_C_2_type, type, (
% 2.45/2.65     tptp_fun_C_2: $i)).
% 2.45/2.65  tff(k5_subset_1_type, type, (
% 2.45/2.65     k5_subset_1: ( $i * $i * $i ) > $i)).
% 2.45/2.65  tff(k4_subset_1_type, type, (
% 2.45/2.65     k4_subset_1: ( $i * $i * $i ) > $i)).
% 2.45/2.65  tff(k3_xboole_0_type, type, (
% 2.45/2.65     k3_xboole_0: ( $i * $i ) > $i)).
% 2.45/2.65  tff(1,plain,
% 2.45/2.65      (^[A: $i] : refl((k2_xboole_0(A, A) = A) <=> (k2_xboole_0(A, A) = A))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(2,plain,
% 2.45/2.65      (![A: $i] : (k2_xboole_0(A, A) = A) <=> ![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(quant_intro,[status(thm)],[1])).
% 2.45/2.65  tff(3,plain,
% 2.45/2.65      (![A: $i] : (k2_xboole_0(A, A) = A) <=> ![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(4,plain,
% 2.45/2.65      (![A: $i, B: $i] : (k2_xboole_0(A, A) = A) <=> ![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(elim_unused_vars,[status(thm)],[])).
% 2.45/2.65  tff(5,axiom,(![A: $i, B: $i] : (k2_xboole_0(A, A) = A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','idempotence_k2_xboole_0')).
% 2.45/2.65  tff(6,plain,
% 2.45/2.65      (![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[5, 4])).
% 2.45/2.65  tff(7,plain,
% 2.45/2.65      (![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[6, 3])).
% 2.45/2.65  tff(8,plain,(
% 2.45/2.65      ![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(skolemize,[status(sab)],[7])).
% 2.45/2.65  tff(9,plain,
% 2.45/2.65      (![A: $i] : (k2_xboole_0(A, A) = A)),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[8, 2])).
% 2.45/2.65  tff(10,plain,
% 2.45/2.65      ((~![A: $i] : (k2_xboole_0(A, A) = A)) | (k2_xboole_0(B!0, B!0) = B!0)),
% 2.45/2.65      inference(quant_inst,[status(thm)],[])).
% 2.45/2.65  tff(11,plain,
% 2.45/2.65      (k2_xboole_0(B!0, B!0) = B!0),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[10, 9])).
% 2.45/2.65  tff(12,plain,
% 2.45/2.65      (m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(monotonicity,[status(thm)],[11])).
% 2.45/2.65  tff(13,plain,
% 2.45/2.65      (m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(symmetry,[status(thm)],[12])).
% 2.45/2.65  tff(14,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))) <=> (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C))))))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(15,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))) <=> (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C))))))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(16,axiom,(~![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t7_relset_2')).
% 2.45/2.65  tff(17,plain,
% 2.45/2.65      (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[16, 15])).
% 2.45/2.65  tff(18,plain,
% 2.45/2.65      (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[17, 14])).
% 2.45/2.65  tff(19,plain,
% 2.45/2.65      (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[18, 14])).
% 2.45/2.65  tff(20,plain,
% 2.45/2.65      (~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | r1_tarski(k5_subset_1(A, k8_setfam_1(A, B), k8_setfam_1(A, C)), k8_setfam_1(A, k1_relset_2(A, B, C)))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[19, 14])).
% 2.45/2.65  tff(21,plain,
% 2.45/2.65      (m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(and_elim,[status(thm)],[20])).
% 2.45/2.65  tff(22,plain,
% 2.45/2.65      (m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[21, 13])).
% 2.45/2.65  tff(23,plain,
% 2.45/2.65      (^[A: $i, B: $i] : refl(((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(24,plain,
% 2.45/2.65      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[23])).
% 2.45/2.65  tff(25,plain,
% 2.45/2.65      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(26,plain,
% 2.45/2.65      (^[A: $i, B: $i] : rewrite((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(27,plain,
% 2.45/2.65      (![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[26])).
% 2.45/2.65  tff(28,axiom,(![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_k8_setfam_1')).
% 2.45/2.65  tff(29,plain,
% 2.45/2.65      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[28, 27])).
% 2.45/2.65  tff(30,plain,
% 2.45/2.65      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[29, 25])).
% 2.45/2.65  tff(31,plain,(
% 2.45/2.65      ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(skolemize,[status(sab)],[30])).
% 2.45/2.65  tff(32,plain,
% 2.45/2.65      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[31, 24])).
% 2.45/2.65  tff(33,plain,
% 2.45/2.65      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1)))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(34,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(quant_inst,[status(thm)],[])).
% 2.45/2.65  tff(35,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[34, 33])).
% 2.45/2.65  tff(36,plain,
% 2.45/2.65      (m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[35, 21, 32])).
% 2.45/2.65  tff(37,plain,
% 2.45/2.65      (~((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))))),
% 2.45/2.65      inference(and_elim,[status(thm)],[20])).
% 2.45/2.65  tff(38,plain,
% 2.45/2.65      (m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(or_elim,[status(thm)],[37])).
% 2.45/2.65  tff(39,plain,
% 2.45/2.65      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1)))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(40,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1)))),
% 2.45/2.65      inference(quant_inst,[status(thm)],[])).
% 2.45/2.65  tff(41,plain,
% 2.45/2.65      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | m1_subset_1(k8_setfam_1(A, B), k1_zfmisc_1(A)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[40, 39])).
% 2.45/2.65  tff(42,plain,
% 2.45/2.65      (m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[41, 38, 32])).
% 2.45/2.65  tff(43,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : refl(((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(44,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[43])).
% 2.45/2.65  tff(45,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) <=> (~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> (~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))))), rewrite((~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> (((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))))), rewrite((((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(46,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[45])).
% 2.45/2.65  tff(47,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(48,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(49,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k5_subset_1(A, B, C) = k5_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[48])).
% 2.45/2.65  tff(50,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','commutativity_k5_subset_1')).
% 2.45/2.65  tff(51,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[50, 49])).
% 2.45/2.65  tff(52,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[51, 47])).
% 2.45/2.65  tff(53,plain,(
% 2.45/2.65      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k5_subset_1(A, B, C) = k5_subset_1(A, C, B)))),
% 2.45/2.65      inference(skolemize,[status(sab)],[52])).
% 2.45/2.65  tff(54,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[53, 46])).
% 2.45/2.65  tff(55,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[54, 44])).
% 2.45/2.65  tff(56,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))))) <=> ((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(57,plain,
% 2.45/2.65      (((k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1)))) <=> ((~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(58,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))))) <=> ((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0)))))),
% 2.45/2.65      inference(monotonicity,[status(thm)],[57])).
% 2.45/2.65  tff(59,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))))) <=> ((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))))),
% 2.45/2.65      inference(transitivity,[status(thm)],[58, 56])).
% 2.45/2.65  tff(60,plain,
% 2.45/2.65      ((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))))),
% 2.45/2.65      inference(quant_inst,[status(thm)],[])).
% 2.45/2.65  tff(61,plain,
% 2.45/2.65      ((~![A: $i, B: $i, C: $i] : ((k5_subset_1(A, B, C) = k5_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[60, 59])).
% 2.45/2.65  tff(62,plain,
% 2.45/2.65      ((~m1_subset_1(k8_setfam_1(A!1, B!0), k1_zfmisc_1(A!1))) | (~m1_subset_1(k8_setfam_1(A!1, C!2), k1_zfmisc_1(A!1))) | (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0)))),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[61, 55])).
% 2.45/2.65  tff(63,plain,
% 2.45/2.65      (k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[62, 42, 36])).
% 2.45/2.65  tff(64,plain,
% 2.45/2.65      (k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0)) = k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2))),
% 2.45/2.65      inference(symmetry,[status(thm)],[63])).
% 2.45/2.65  tff(65,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : refl(((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(66,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[65])).
% 2.45/2.65  tff(67,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) <=> (~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> (~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))))), rewrite((~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)) <=> (((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)))), rewrite((((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)) <=> ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)) <=> ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(68,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[67])).
% 2.45/2.65  tff(69,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(70,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, B) = B)) <=> ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B)))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(71,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, B) = B)) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[70])).
% 2.45/2.65  tff(72,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, B) = B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','idempotence_k4_subset_1')).
% 2.45/2.65  tff(73,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[72, 71])).
% 2.45/2.65  tff(74,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[73, 69])).
% 2.45/2.65  tff(75,plain,(
% 2.45/2.65      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, B) = B))),
% 2.45/2.65      inference(skolemize,[status(sab)],[74])).
% 2.45/2.65  tff(76,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[75, 68])).
% 2.45/2.65  tff(77,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[76, 66])).
% 2.45/2.65  tff(78,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(79,plain,
% 2.45/2.65      (((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(80,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0)))),
% 2.45/2.65      inference(monotonicity,[status(thm)],[79])).
% 2.45/2.65  tff(81,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0))),
% 2.45/2.65      inference(transitivity,[status(thm)],[80, 78])).
% 2.45/2.65  tff(82,plain,
% 2.45/2.65      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.65      inference(quant_inst,[status(thm)],[])).
% 2.45/2.65  tff(83,plain,
% 2.45/2.65      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, B) = B) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0)),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[82, 81])).
% 2.45/2.65  tff(84,plain,
% 2.45/2.65      (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = B!0),
% 2.45/2.65      inference(unit_resolution,[status(thm)],[83, 21, 77])).
% 2.45/2.65  tff(85,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : refl(((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(86,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[85])).
% 2.45/2.65  tff(87,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) <=> (~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> (~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))))), rewrite((~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> (((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))))), rewrite((((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(88,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[87])).
% 2.45/2.65  tff(89,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))),
% 2.45/2.65      inference(rewrite,[status(thm)],[])).
% 2.45/2.65  tff(90,plain,
% 2.45/2.65      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C))))),
% 2.45/2.65      inference(bind,[status(th)],[])).
% 2.45/2.65  tff(91,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k2_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))),
% 2.45/2.65      inference(quant_intro,[status(thm)],[90])).
% 2.45/2.65  tff(92,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','redefinition_k4_subset_1')).
% 2.45/2.65  tff(93,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[92, 91])).
% 2.45/2.65  tff(94,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[93, 89])).
% 2.45/2.65  tff(95,plain,(
% 2.45/2.65      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k2_xboole_0(B, C)))),
% 2.45/2.65      inference(skolemize,[status(sab)],[94])).
% 2.45/2.65  tff(96,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[95, 88])).
% 2.45/2.65  tff(97,plain,
% 2.45/2.65      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.65      inference(modus_ponens,[status(thm)],[96, 86])).
% 2.45/2.65  tff(98,plain,
% 2.45/2.65      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(99,plain,
% 2.45/2.66      (((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(100,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0))))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[99])).
% 2.45/2.66  tff(101,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)))),
% 2.45/2.66      inference(transitivity,[status(thm)],[100, 98])).
% 2.45/2.66  tff(102,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(quant_inst,[status(thm)],[])).
% 2.45/2.66  tff(103,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[102, 101])).
% 2.45/2.66  tff(104,plain,
% 2.45/2.66      (k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0) = k2_xboole_0(B!0, B!0)),
% 2.45/2.66      inference(unit_resolution,[status(thm)],[103, 21, 97])).
% 2.45/2.66  tff(105,plain,
% 2.45/2.66      (k2_xboole_0(B!0, B!0) = k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0)),
% 2.45/2.66      inference(symmetry,[status(thm)],[104])).
% 2.45/2.66  tff(106,plain,
% 2.45/2.66      (k2_xboole_0(B!0, B!0) = B!0),
% 2.45/2.66      inference(transitivity,[status(thm)],[105, 84])).
% 2.45/2.66  tff(107,plain,
% 2.45/2.66      (k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)) = k8_setfam_1(A!1, B!0)),
% 2.45/2.66      inference(monotonicity,[status(thm)],[106])).
% 2.45/2.66  tff(108,plain,
% 2.45/2.66      (k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0))) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, B!0))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[107])).
% 2.45/2.66  tff(109,plain,
% 2.45/2.66      (m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[105])).
% 2.45/2.66  tff(110,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(symmetry,[status(thm)],[109])).
% 2.45/2.66  tff(111,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : refl((m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(112,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[111])).
% 2.45/2.66  tff(113,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) <=> (~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> (~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))))), rewrite((~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> (((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))))), rewrite((((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(114,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> ![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[113])).
% 2.45/2.66  tff(115,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(116,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(117,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[116])).
% 2.45/2.66  tff(118,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_k4_subset_1')).
% 2.45/2.66  tff(119,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[118, 117])).
% 2.45/2.66  tff(120,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[119, 115])).
% 2.45/2.66  tff(121,plain,(
% 2.45/2.66      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)))),
% 2.45/2.66      inference(skolemize,[status(sab)],[120])).
% 2.45/2.66  tff(122,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[121, 114])).
% 2.45/2.66  tff(123,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[122, 112])).
% 2.45/2.66  tff(124,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(125,plain,
% 2.45/2.66      ((m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(126,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[125])).
% 2.45/2.66  tff(127,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(transitivity,[status(thm)],[126, 124])).
% 2.45/2.66  tff(128,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(quant_inst,[status(thm)],[])).
% 2.45/2.66  tff(129,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[128, 127])).
% 2.45/2.66  tff(130,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(unit_resolution,[status(thm)],[129, 21, 123])).
% 2.45/2.66  tff(131,plain,
% 2.45/2.66      (m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[130, 110])).
% 2.45/2.66  tff(132,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : refl(((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(133,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[132])).
% 2.45/2.66  tff(134,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) <=> (~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> (~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))))), rewrite((~(~((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> (((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))))), rewrite((((~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))), (((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(135,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[134])).
% 2.45/2.66  tff(136,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(137,plain,
% 2.45/2.66      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(138,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k4_subset_1(A, C, B))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[137])).
% 2.45/2.66  tff(139,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A))) => (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','commutativity_k4_subset_1')).
% 2.45/2.66  tff(140,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[139, 138])).
% 2.45/2.66  tff(141,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[140, 136])).
% 2.45/2.66  tff(142,plain,(
% 2.45/2.66      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(A)) & m1_subset_1(C, k1_zfmisc_1(A)))) | (k4_subset_1(A, B, C) = k4_subset_1(A, C, B)))),
% 2.45/2.66      inference(skolemize,[status(sab)],[141])).
% 2.45/2.66  tff(143,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[142, 135])).
% 2.45/2.66  tff(144,plain,
% 2.45/2.66      (![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[143, 133])).
% 2.45/2.66  tff(145,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(146,plain,
% 2.45/2.66      (((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(147,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0)))))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[146])).
% 2.45/2.66  tff(148,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))))),
% 2.45/2.66      inference(transitivity,[status(thm)],[147, 145])).
% 2.45/2.66  tff(149,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(quant_inst,[status(thm)],[])).
% 2.45/2.66  tff(150,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k4_subset_1(A, C, B)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[149, 148])).
% 2.45/2.66  tff(151,plain,
% 2.45/2.66      (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))),
% 2.45/2.66      inference(unit_resolution,[status(thm)],[150, 38, 144, 131])).
% 2.45/2.66  tff(152,plain,
% 2.45/2.66      (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)),
% 2.45/2.66      inference(monotonicity,[status(thm)],[106])).
% 2.45/2.66  tff(153,plain,
% 2.45/2.66      (k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2)),
% 2.45/2.66      inference(symmetry,[status(thm)],[152])).
% 2.45/2.66  tff(154,plain,
% 2.45/2.66      (k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))),
% 2.45/2.66      inference(transitivity,[status(thm)],[153, 151])).
% 2.45/2.66  tff(155,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[153])).
% 2.45/2.66  tff(156,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) <=> m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(symmetry,[status(thm)],[155])).
% 2.45/2.66  tff(157,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(158,plain,
% 2.45/2.66      ((m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(159,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(monotonicity,[status(thm)],[158])).
% 2.45/2.66  tff(160,plain,
% 2.45/2.66      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.66      inference(transitivity,[status(thm)],[159, 157])).
% 2.45/2.66  tff(161,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.66      inference(quant_inst,[status(thm)],[])).
% 2.45/2.66  tff(162,plain,
% 2.45/2.66      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k4_subset_1(A, B, C), k1_zfmisc_1(A)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[161, 160])).
% 2.45/2.66  tff(163,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(unit_resolution,[status(thm)],[162, 38, 123, 131])).
% 2.45/2.66  tff(164,plain,
% 2.45/2.66      (m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[163, 156])).
% 2.45/2.66  tff(165,plain,
% 2.45/2.66      (^[A: $i, B: $i] : refl(((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(166,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[165])).
% 2.45/2.66  tff(167,plain,
% 2.45/2.66      (^[A: $i, B: $i] : rewrite(((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(168,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[167])).
% 2.45/2.66  tff(169,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(transitivity,[status(thm)],[168, 166])).
% 2.45/2.66  tff(170,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(rewrite,[status(thm)],[])).
% 2.45/2.66  tff(171,plain,
% 2.45/2.66      (^[A: $i, B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(quant_intro(proof_bind(^[D: $i] : trans(monotonicity(rewrite(((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D)))) <=> ((~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))), ((m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))) <=> (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))))), rewrite((m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))) <=> ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))), ((m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))) <=> ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))), (![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))) <=> ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))), ((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D)))))) <=> (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))), rewrite((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))), ((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D)))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))))), (![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D)))))) <=> ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))), ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))))) <=> (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))))), rewrite((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))), ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))))),
% 2.45/2.66      inference(bind,[status(th)],[])).
% 2.45/2.66  tff(172,plain,
% 2.45/2.66      (![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(quant_intro,[status(thm)],[171])).
% 2.45/2.66  tff(173,axiom,(![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ![D: $i] : (m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A))) => ((B = k4_subset_1(k1_zfmisc_1(A), C, D)) => (k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t8_mssubfam')).
% 2.45/2.66  tff(174,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[173, 172])).
% 2.45/2.66  tff(175,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[174, 170])).
% 2.45/2.66  tff(176,plain,(
% 2.45/2.66      ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(skolemize,[status(sab)],[175])).
% 2.45/2.66  tff(177,plain,
% 2.45/2.66      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.66      inference(modus_ponens,[status(thm)],[176, 169])).
% 2.45/2.66  tff(178,plain,
% 2.45/2.66      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | (~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(179,plain,
% 2.45/2.67      (((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1))))))) <=> ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(180,plain,
% 2.45/2.67      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[179])).
% 2.45/2.67  tff(181,plain,
% 2.45/2.67      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | (~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))))))),
% 2.45/2.67      inference(transitivity,[status(thm)],[180, 178])).
% 2.45/2.67  tff(182,plain,
% 2.45/2.67      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))))))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(183,plain,
% 2.45/2.67      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![D: $i] : ((k8_setfam_1(A, B) = k5_subset_1(A, k8_setfam_1(A, C), k8_setfam_1(A, D))) | (~(B = k4_subset_1(k1_zfmisc_1(A), C, D))) | (~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A)))))))) | (~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[182, 181])).
% 2.45/2.67  tff(184,plain,
% 2.45/2.67      ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[183, 177])).
% 2.45/2.67  tff(185,plain,
% 2.45/2.67      (![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[184, 164])).
% 2.45/2.67  tff(186,plain,
% 2.45/2.67      (((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D)))))) <=> ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D)))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(187,plain,
% 2.45/2.67      ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D)))))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(188,plain,
% 2.45/2.67      ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C, D)))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[187, 186])).
% 2.45/2.67  tff(189,plain,
% 2.45/2.67      (![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[188, 38, 185])).
% 2.45/2.67  tff(190,plain,
% 2.45/2.67      (((~![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))) | ((~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0)))))) <=> ((~![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0)))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(191,plain,
% 2.45/2.67      ((~![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))) | ((~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0)))))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(192,plain,
% 2.45/2.67      ((~![D: $i] : ((~m1_subset_1(D, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, D))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, D))))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)))) | (~(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k4_subset_1(k1_zfmisc_1(A!1), C!2, k2_xboole_0(B!0, B!0))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[191, 190])).
% 2.45/2.67  tff(193,plain,
% 2.45/2.67      (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, C!2), k8_setfam_1(A!1, k2_xboole_0(B!0, B!0)))),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[192, 131, 189, 154])).
% 2.45/2.67  tff(194,plain,
% 2.45/2.67      (k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) = k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2))),
% 2.45/2.67      inference(transitivity,[status(thm)],[193, 108, 64])).
% 2.45/2.67  tff(195,plain,
% 2.45/2.67      (r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) <=> r1_tarski(k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[194])).
% 2.45/2.67  tff(196,plain,
% 2.45/2.67      (r1_tarski(k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) <=> r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))),
% 2.45/2.67      inference(symmetry,[status(thm)],[195])).
% 2.45/2.67  tff(197,plain,
% 2.45/2.67      ((~r1_tarski(k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))) <=> (~r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[196])).
% 2.45/2.67  tff(198,plain,
% 2.45/2.67      (~r1_tarski(k5_subset_1(A!1, k8_setfam_1(A!1, B!0), k8_setfam_1(A!1, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))),
% 2.45/2.67      inference(or_elim,[status(thm)],[37])).
% 2.45/2.67  tff(199,plain,
% 2.45/2.67      (~r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[198, 197])).
% 2.45/2.67  tff(200,assumption,(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)), introduced(assumption)).
% 2.45/2.67  tff(201,plain,
% 2.45/2.67      (k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)),
% 2.45/2.67      inference(transitivity,[status(thm)],[153, 200])).
% 2.45/2.67  tff(202,plain,
% 2.45/2.67      (k3_xboole_0(k2_xboole_0(B!0, B!0), C!2) = k3_xboole_0(B!0, C!2)),
% 2.45/2.67      inference(monotonicity,[status(thm)],[106])).
% 2.45/2.67  tff(203,plain,
% 2.45/2.67      (k3_xboole_0(B!0, C!2) = k3_xboole_0(k2_xboole_0(B!0, B!0), C!2)),
% 2.45/2.67      inference(symmetry,[status(thm)],[202])).
% 2.45/2.67  tff(204,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : refl(((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(205,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> ![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[204])).
% 2.45/2.67  tff(206,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) <=> (~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))), ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> (~(~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))))), rewrite((~(~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))), (((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> (((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))))), rewrite((((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(207,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[206])).
% 2.45/2.67  tff(208,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(209,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(210,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => (k1_relset_2(A, B, C) = k3_xboole_0(B, C))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[209])).
% 2.45/2.67  tff(211,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','redefinition_k1_relset_2')).
% 2.45/2.67  tff(212,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[211, 210])).
% 2.45/2.67  tff(213,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[212, 208])).
% 2.45/2.67  tff(214,plain,(
% 2.45/2.67      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | (k1_relset_2(A, B, C) = k3_xboole_0(B, C)))),
% 2.45/2.67      inference(skolemize,[status(sab)],[213])).
% 2.45/2.67  tff(215,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[214, 207])).
% 2.45/2.67  tff(216,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[215, 205])).
% 2.45/2.67  tff(217,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)))) <=> ((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(218,plain,
% 2.45/2.67      (((k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(219,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2))))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[218])).
% 2.45/2.67  tff(220,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)))),
% 2.45/2.67      inference(transitivity,[status(thm)],[219, 217])).
% 2.45/2.67  tff(221,plain,
% 2.45/2.67      ((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(222,plain,
% 2.45/2.67      ((~![A: $i, B: $i, C: $i] : ((k1_relset_2(A, B, C) = k3_xboole_0(B, C)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[221, 220])).
% 2.45/2.67  tff(223,plain,
% 2.45/2.67      (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(B!0, C!2)),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[222, 21, 38, 216])).
% 2.45/2.67  tff(224,plain,
% 2.45/2.67      (k1_relset_2(A!1, B!0, C!2) = k3_xboole_0(k2_xboole_0(B!0, B!0), C!2)),
% 2.45/2.67      inference(transitivity,[status(thm)],[223, 203])).
% 2.45/2.67  tff(225,plain,
% 2.45/2.67      (r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)) <=> r1_tarski(k3_xboole_0(k2_xboole_0(B!0, B!0), C!2), k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[224, 201])).
% 2.45/2.67  tff(226,plain,
% 2.45/2.67      (r1_tarski(k3_xboole_0(k2_xboole_0(B!0, B!0), C!2), k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)) <=> r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2))),
% 2.45/2.67      inference(symmetry,[status(thm)],[225])).
% 2.45/2.67  tff(227,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : refl(r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C)) <=> r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C)))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(228,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C)) <=> ![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[227])).
% 2.45/2.67  tff(229,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C)) <=> ![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(230,axiom,(![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t29_xboole_1')).
% 2.45/2.67  tff(231,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[230, 229])).
% 2.45/2.67  tff(232,plain,(
% 2.45/2.67      ![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))),
% 2.45/2.67      inference(skolemize,[status(sab)],[231])).
% 2.45/2.67  tff(233,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[232, 228])).
% 2.45/2.67  tff(234,plain,
% 2.45/2.67      ((~![A: $i, B: $i, C: $i] : r1_tarski(k3_xboole_0(A, B), k2_xboole_0(A, C))) | r1_tarski(k3_xboole_0(k2_xboole_0(B!0, B!0), C!2), k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(235,plain,
% 2.45/2.67      (r1_tarski(k3_xboole_0(k2_xboole_0(B!0, B!0), C!2), k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))),
% 2.45/2.67      inference(unit_resolution,[status(thm)],[234, 233])).
% 2.45/2.67  tff(236,plain,
% 2.45/2.67      (r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[235, 226])).
% 2.45/2.67  tff(237,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : refl((m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(238,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> ![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[237])).
% 2.45/2.67  tff(239,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) <=> (~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))), ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> (~(~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))))), rewrite((~(~((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))), ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) <=> ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))))), (((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> (((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))))), rewrite((((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))), (((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(240,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[239])).
% 2.45/2.67  tff(241,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(242,plain,
% 2.45/2.67      (^[A: $i, B: $i, C: $i] : rewrite(((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(bind,[status(th)],[])).
% 2.45/2.67  tff(243,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A)))) <=> ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))),
% 2.45/2.67      inference(quant_intro,[status(thm)],[242])).
% 2.45/2.67  tff(244,axiom,(![A: $i, B: $i, C: $i] : ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) => m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_k1_relset_2')).
% 2.45/2.67  tff(245,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[244, 243])).
% 2.45/2.67  tff(246,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[245, 241])).
% 2.45/2.67  tff(247,plain,(
% 2.45/2.67      ![A: $i, B: $i, C: $i] : ((~(m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) & m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))))) | m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))))),
% 2.45/2.67      inference(skolemize,[status(sab)],[246])).
% 2.45/2.67  tff(248,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[247, 240])).
% 2.45/2.67  tff(249,plain,
% 2.45/2.67      (![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[248, 238])).
% 2.45/2.67  tff(250,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(251,plain,
% 2.45/2.67      ((m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.67      inference(rewrite,[status(thm)],[])).
% 2.45/2.67  tff(252,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | ((~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.67      inference(monotonicity,[status(thm)],[251])).
% 2.45/2.67  tff(253,plain,
% 2.45/2.67      (((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))))),
% 2.45/2.67      inference(transitivity,[status(thm)],[252, 250])).
% 2.45/2.67  tff(254,plain,
% 2.45/2.67      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.67      inference(quant_inst,[status(thm)],[])).
% 2.45/2.67  tff(255,plain,
% 2.45/2.67      ((~![A: $i, B: $i, C: $i] : (m1_subset_1(k1_relset_2(A, B, C), k1_zfmisc_1(k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))))) | (~m1_subset_1(B!0, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.67      inference(modus_ponens,[status(thm)],[254, 253])).
% 2.45/2.67  tff(256,plain,
% 2.45/2.67      (m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.68      inference(unit_resolution,[status(thm)],[255, 21, 38, 249])).
% 2.45/2.68  tff(257,plain,
% 2.45/2.68      (^[A: $i, B: $i] : refl(((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))))),
% 2.45/2.68      inference(bind,[status(th)],[])).
% 2.45/2.68  tff(258,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(quant_intro,[status(thm)],[257])).
% 2.45/2.68  tff(259,plain,
% 2.45/2.68      (^[A: $i, B: $i] : rewrite(((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))))),
% 2.45/2.68      inference(bind,[status(th)],[])).
% 2.45/2.68  tff(260,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(quant_intro,[status(thm)],[259])).
% 2.45/2.68  tff(261,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(transitivity,[status(thm)],[260, 258])).
% 2.45/2.68  tff(262,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(263,plain,
% 2.45/2.68      (^[A: $i, B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : trans(monotonicity(rewrite((r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B))) <=> ((~r1_tarski(B, C)) | r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))), ((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))) <=> (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ((~r1_tarski(B, C)) | r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))))), rewrite((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => ((~r1_tarski(B, C)) | r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))) <=> (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))), ((m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))) <=> (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))))), (![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))) <=> ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))), ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B))))) <=> (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))))), rewrite((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C)))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))), ((m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B))))) <=> ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))))),
% 2.45/2.68      inference(bind,[status(th)],[])).
% 2.45/2.68  tff(264,plain,
% 2.45/2.68      (![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B))))) <=> ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(quant_intro,[status(thm)],[263])).
% 2.45/2.68  tff(265,axiom,(![A: $i, B: $i] : (m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A))) => ![C: $i] : (m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A))) => (r1_tarski(B, C) => r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t59_setfam_1')).
% 2.45/2.68  tff(266,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(modus_ponens,[status(thm)],[265, 264])).
% 2.45/2.68  tff(267,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(modus_ponens,[status(thm)],[266, 262])).
% 2.45/2.68  tff(268,plain,(
% 2.45/2.68      ![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(skolemize,[status(sab)],[267])).
% 2.45/2.68  tff(269,plain,
% 2.45/2.68      (![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))),
% 2.45/2.68      inference(modus_ponens,[status(thm)],[268, 261])).
% 2.45/2.68  tff(270,plain,
% 2.45/2.68      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | (~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(271,plain,
% 2.45/2.68      (((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))) <=> ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(272,plain,
% 2.45/2.68      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))))),
% 2.45/2.68      inference(monotonicity,[status(thm)],[271])).
% 2.45/2.68  tff(273,plain,
% 2.45/2.68      (((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))) <=> ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | (~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))),
% 2.45/2.68      inference(transitivity,[status(thm)],[272, 270])).
% 2.45/2.68  tff(274,plain,
% 2.45/2.68      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | ((~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C))))),
% 2.45/2.68      inference(quant_inst,[status(thm)],[])).
% 2.45/2.68  tff(275,plain,
% 2.45/2.68      ((~![A: $i, B: $i] : ((~m1_subset_1(B, k1_zfmisc_1(k1_zfmisc_1(A)))) | ![C: $i] : (r1_tarski(k8_setfam_1(A, C), k8_setfam_1(A, B)) | (~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A)))) | (~r1_tarski(B, C))))) | (~m1_subset_1(k1_relset_2(A!1, B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | ![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))),
% 2.45/2.68      inference(modus_ponens,[status(thm)],[274, 273])).
% 2.45/2.68  tff(276,plain,
% 2.45/2.68      (![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))),
% 2.45/2.68      inference(unit_resolution,[status(thm)],[275, 269, 256])).
% 2.45/2.68  tff(277,plain,
% 2.45/2.68      (((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2))))) <=> ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))) | (~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2))))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(278,plain,
% 2.45/2.68      ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))) | ((~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2))))),
% 2.45/2.68      inference(quant_inst,[status(thm)],[])).
% 2.45/2.68  tff(279,plain,
% 2.45/2.68      ((~![C: $i] : ((~m1_subset_1(C, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, C), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), C)))) | (~m1_subset_1(k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2))) | (~r1_tarski(k1_relset_2(A!1, B!0, C!2), k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)))),
% 2.45/2.68      inference(modus_ponens,[status(thm)],[278, 277])).
% 2.45/2.68  tff(280,plain,
% 2.45/2.68      (r1_tarski(k8_setfam_1(A!1, k4_subset_1(k1_zfmisc_1(A!1), B!0, C!2)), k8_setfam_1(A!1, k1_relset_2(A!1, B!0, C!2)))),
% 2.45/2.68      inference(unit_resolution,[status(thm)],[279, 276, 164, 236])).
% 2.45/2.68  tff(281,plain,
% 2.45/2.68      ($false),
% 2.45/2.68      inference(unit_resolution,[status(thm)],[280, 199])).
% 2.45/2.68  tff(282,plain,(~(k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))), inference(lemma,lemma(discharge,[]))).
% 2.45/2.68  tff(283,plain,
% 2.45/2.68      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(284,plain,
% 2.45/2.68      (((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1))))) <=> ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)))),
% 2.45/2.68      inference(rewrite,[status(thm)],[])).
% 2.45/2.68  tff(285,plain,
% 2.45/2.68      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))))),
% 2.45/2.69      inference(monotonicity,[status(thm)],[284])).
% 2.45/2.69  tff(286,plain,
% 2.45/2.69      (((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))) <=> ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)))),
% 2.45/2.69      inference(transitivity,[status(thm)],[285, 283])).
% 2.45/2.69  tff(287,plain,
% 2.45/2.69      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | ((k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2)) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))))),
% 2.45/2.69      inference(quant_inst,[status(thm)],[])).
% 2.45/2.69  tff(288,plain,
% 2.45/2.69      ((~![A: $i, B: $i, C: $i] : ((k4_subset_1(A, B, C) = k2_xboole_0(B, C)) | (~m1_subset_1(B, k1_zfmisc_1(A))) | (~m1_subset_1(C, k1_zfmisc_1(A))))) | (~m1_subset_1(C!2, k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))) | (k4_subset_1(k1_zfmisc_1(A!1), k2_xboole_0(B!0, B!0), C!2) = k2_xboole_0(k2_xboole_0(B!0, B!0), C!2))),
% 2.45/2.69      inference(modus_ponens,[status(thm)],[287, 286])).
% 2.45/2.69  tff(289,plain,
% 2.45/2.69      (~m1_subset_1(k2_xboole_0(B!0, B!0), k1_zfmisc_1(k1_zfmisc_1(A!1)))),
% 2.45/2.69      inference(unit_resolution,[status(thm)],[288, 38, 97, 282])).
% 2.45/2.69  tff(290,plain,
% 2.45/2.69      ($false),
% 2.45/2.69      inference(unit_resolution,[status(thm)],[289, 22])).
% 2.45/2.69  % SZS output end Proof
% 2.45/2.69  % E exiting
%------------------------------------------------------------------------------