%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LAT359+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:14:30 AM UTC 2025
% Result : Theorem 3.02s 3.19s
% Output : Proof 3.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : LAT359+1 : TPTP v9.0.0. Released v3.4.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Thu Jun 19 20:38:38 EDT 2025
% 0.12/0.35 % CPUTime :
% 3.02/3.19 % SZS status Theorem
% 3.02/3.19 % SZS output start Proof
% 3.02/3.19 tff(r2_hidden_type, type, (
% 3.02/3.19 r2_hidden: ( $i * $i ) > $o)).
% 3.02/3.19 tff(u1_altcat_1_type, type, (
% 3.02/3.19 u1_altcat_1: $i > $i)).
% 3.02/3.19 tff(tptp_fun_A_0_type, type, (
% 3.02/3.19 tptp_fun_A_0: $i)).
% 3.02/3.19 tff(k4_tarski_type, type, (
% 3.02/3.19 k4_tarski: ( $i * $i ) > $i)).
% 3.02/3.19 tff(k1_xboole_0_type, type, (
% 3.02/3.19 k1_xboole_0: $i)).
% 3.02/3.19 tff(k2_tarski_type, type, (
% 3.02/3.19 k2_tarski: ( $i * $i ) > $i)).
% 3.02/3.19 tff(k1_tarski_type, type, (
% 3.02/3.19 k1_tarski: $i > $i)).
% 3.02/3.19 tff(tptp_fun_B_3_type, type, (
% 3.02/3.19 tptp_fun_B_3: $i)).
% 3.02/3.19 tff(tptp_fun_C_2_type, type, (
% 3.02/3.19 tptp_fun_C_2: $i)).
% 3.02/3.19 tff(k1_funct_1_type, type, (
% 3.02/3.19 k1_funct_1: ( $i * $i ) > $i)).
% 3.02/3.19 tff(k1_relat_1_type, type, (
% 3.02/3.19 k1_relat_1: $i > $i)).
% 3.02/3.19 tff(v1_funct_1_type, type, (
% 3.02/3.19 v1_funct_1: $i > $o)).
% 3.02/3.19 tff(v1_relat_1_type, type, (
% 3.02/3.19 v1_relat_1: $i > $o)).
% 3.02/3.19 tff(m1_pboole_type, type, (
% 3.02/3.19 m1_pboole: ( $i * $i ) > $o)).
% 3.02/3.19 tff(k2_zfmisc_1_type, type, (
% 3.02/3.19 k2_zfmisc_1: ( $i * $i ) > $i)).
% 3.02/3.19 tff(u1_struct_0_type, type, (
% 3.02/3.19 u1_struct_0: $i > $i)).
% 3.02/3.19 tff(l1_altcat_1_type, type, (
% 3.02/3.19 l1_altcat_1: $i > $o)).
% 3.02/3.19 tff(l2_altcat_1_type, type, (
% 3.02/3.19 l2_altcat_1: $i > $o)).
% 3.02/3.19 tff(k1_altcat_1_type, type, (
% 3.02/3.19 k1_altcat_1: ( $i * $i * $i ) > $i)).
% 3.02/3.19 tff(tptp_fun_D_1_type, type, (
% 3.02/3.19 tptp_fun_D_1: $i)).
% 3.02/3.19 tff(m1_subset_1_type, type, (
% 3.02/3.19 m1_subset_1: ( $i * $i ) > $o)).
% 3.02/3.19 tff(k1_binop_1_type, type, (
% 3.02/3.19 k1_binop_1: ( $i * $i * $i ) > $i)).
% 3.02/3.19 tff(v3_struct_0_type, type, (
% 3.02/3.19 v3_struct_0: $i > $o)).
% 3.02/3.19 tff(v1_xboole_0_type, type, (
% 3.02/3.19 v1_xboole_0: $i > $o)).
% 3.02/3.19 tff(v1_membered_type, type, (
% 3.02/3.19 v1_membered: $i > $o)).
% 3.02/3.19 tff(v2_membered_type, type, (
% 3.02/3.19 v2_membered: $i > $o)).
% 3.02/3.19 tff(v3_membered_type, type, (
% 3.02/3.19 v3_membered: $i > $o)).
% 3.02/3.19 tff(v4_membered_type, type, (
% 3.02/3.19 v4_membered: $i > $o)).
% 3.02/3.19 tff(v5_membered_type, type, (
% 3.02/3.19 v5_membered: $i > $o)).
% 3.02/3.19 tff(1,assumption,((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))), introduced(assumption)).
% 3.02/3.19 tff(2,plain,
% 3.02/3.19 (^[A: $i] : refl((l1_altcat_1(A) | (~l2_altcat_1(A))) <=> (l1_altcat_1(A) | (~l2_altcat_1(A))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(3,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A))) <=> ![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[2])).
% 3.02/3.19 tff(4,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A))) <=> ![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(5,plain,
% 3.02/3.19 (^[A: $i] : rewrite((l2_altcat_1(A) => l1_altcat_1(A)) <=> (l1_altcat_1(A) | (~l2_altcat_1(A))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(6,plain,
% 3.02/3.19 (![A: $i] : (l2_altcat_1(A) => l1_altcat_1(A)) <=> ![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[5])).
% 3.02/3.19 tff(7,axiom,(![A: $i] : (l2_altcat_1(A) => l1_altcat_1(A))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_l2_altcat_1')).
% 3.02/3.19 tff(8,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[7, 6])).
% 3.02/3.19 tff(9,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[8, 4])).
% 3.02/3.19 tff(10,plain,(
% 3.02/3.19 ![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(skolemize,[status(sab)],[9])).
% 3.02/3.19 tff(11,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[10, 3])).
% 3.02/3.19 tff(12,plain,
% 3.02/3.19 ((((~v3_struct_0(A!0)) & l2_altcat_1(A!0)) & (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))) <=> ((~v3_struct_0(A!0)) & l2_altcat_1(A!0) & r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(13,plain,
% 3.02/3.19 ((r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2))))) <=> (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(14,plain,
% 3.02/3.19 ((((~v3_struct_0(A!0)) & l2_altcat_1(A!0)) & (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))) <=> (((~v3_struct_0(A!0)) & l2_altcat_1(A!0)) & (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2))))))),
% 3.02/3.19 inference(monotonicity,[status(thm)],[13])).
% 3.02/3.19 tff(15,plain,
% 3.02/3.19 ((((~v3_struct_0(A!0)) & l2_altcat_1(A!0)) & (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))) <=> ((~v3_struct_0(A!0)) & l2_altcat_1(A!0) & r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))))),
% 3.02/3.19 inference(transitivity,[status(thm)],[14, 12])).
% 3.02/3.19 tff(16,plain,
% 3.02/3.19 ((~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C)))))))) <=> (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C))))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(17,plain,
% 3.02/3.19 ((~![A: $i] : (((~v3_struct_0(A)) & l2_altcat_1(A)) => ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ![E: $i] : (m1_subset_1(E, u1_struct_0(A)) => ![F: $i] : (m1_subset_1(F, u1_struct_0(A)) => (~((((E = B) & (F = C)) & r2_hidden(D, k1_altcat_1(A, E, F))) & m1_subset_1(D, k1_altcat_1(A, E, F)))))))))) <=> (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C))))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(18,axiom,(~![A: $i] : (((~v3_struct_0(A)) & l2_altcat_1(A)) => ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ![E: $i] : (m1_subset_1(E, u1_struct_0(A)) => ![F: $i] : (m1_subset_1(F, u1_struct_0(A)) => (~((((E = B) & (F = C)) & r2_hidden(D, k1_altcat_1(A, E, F))) & m1_subset_1(D, k1_altcat_1(A, E, F)))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t12_waybel34')).
% 3.02/3.19 tff(19,plain,
% 3.02/3.19 (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[18, 17])).
% 3.02/3.19 tff(20,plain,
% 3.02/3.19 (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[19, 16])).
% 3.02/3.19 tff(21,plain,
% 3.02/3.19 (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[20, 16])).
% 3.02/3.19 tff(22,plain,
% 3.02/3.19 (~![A: $i] : ((~((~v3_struct_0(A)) & l2_altcat_1(A))) | ![B: $i, C: $i, D: $i] : (~(r2_hidden(D, k1_binop_1(u1_altcat_1(A), B, C)) & ((~m1_subset_1(B, u1_struct_0(A))) | (~m1_subset_1(D, k1_altcat_1(A, B, C))) | (~m1_subset_1(C, u1_struct_0(A))) | (~r2_hidden(D, k1_altcat_1(A, B, C)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[21, 16])).
% 3.02/3.19 tff(23,plain,
% 3.02/3.19 ((~v3_struct_0(A!0)) & l2_altcat_1(A!0) & r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) & ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[22, 15])).
% 3.02/3.19 tff(24,plain,
% 3.02/3.19 (l2_altcat_1(A!0)),
% 3.02/3.19 inference(and_elim,[status(thm)],[23])).
% 3.02/3.19 tff(25,plain,
% 3.02/3.19 (((~![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))) | (l1_altcat_1(A!0) | (~l2_altcat_1(A!0)))) <=> ((~![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))) | l1_altcat_1(A!0) | (~l2_altcat_1(A!0)))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(26,plain,
% 3.02/3.19 ((~![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))) | (l1_altcat_1(A!0) | (~l2_altcat_1(A!0)))),
% 3.02/3.19 inference(quant_inst,[status(thm)],[])).
% 3.02/3.19 tff(27,plain,
% 3.02/3.19 ((~![A: $i] : (l1_altcat_1(A) | (~l2_altcat_1(A)))) | l1_altcat_1(A!0) | (~l2_altcat_1(A!0))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[26, 25])).
% 3.02/3.19 tff(28,plain,
% 3.02/3.19 (l1_altcat_1(A!0)),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[27, 24, 11])).
% 3.02/3.19 tff(29,plain,
% 3.02/3.19 (^[A: $i] : refl(((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))) <=> ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(30,plain,
% 3.02/3.19 (![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))) <=> ![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[29])).
% 3.02/3.19 tff(31,plain,
% 3.02/3.19 (![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))) <=> ![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(32,plain,
% 3.02/3.19 (^[A: $i] : rewrite((l1_altcat_1(A) => m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))) <=> ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(33,plain,
% 3.02/3.19 (![A: $i] : (l1_altcat_1(A) => m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A)))) <=> ![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[32])).
% 3.02/3.19 tff(34,axiom,(![A: $i] : (l1_altcat_1(A) => m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_u1_altcat_1')).
% 3.02/3.19 tff(35,plain,
% 3.02/3.19 (![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[34, 33])).
% 3.02/3.19 tff(36,plain,
% 3.02/3.19 (![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[35, 31])).
% 3.02/3.19 tff(37,plain,(
% 3.02/3.19 ![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(skolemize,[status(sab)],[36])).
% 3.02/3.19 tff(38,plain,
% 3.02/3.19 (![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[37, 30])).
% 3.02/3.19 tff(39,plain,
% 3.02/3.19 (((~![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))) | ((~l1_altcat_1(A!0)) | m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))) <=> ((~![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))) | (~l1_altcat_1(A!0)) | m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(40,plain,
% 3.02/3.19 ((~![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))) | ((~l1_altcat_1(A!0)) | m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))),
% 3.02/3.19 inference(quant_inst,[status(thm)],[])).
% 3.02/3.19 tff(41,plain,
% 3.02/3.19 ((~![A: $i] : ((~l1_altcat_1(A)) | m1_pboole(u1_altcat_1(A), k2_zfmisc_1(u1_struct_0(A), u1_struct_0(A))))) | (~l1_altcat_1(A!0)) | m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[40, 39])).
% 3.02/3.19 tff(42,plain,
% 3.02/3.19 ((~l1_altcat_1(A!0)) | m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[41, 38])).
% 3.02/3.19 tff(43,plain,
% 3.02/3.19 (m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[42, 28])).
% 3.02/3.19 tff(44,plain,
% 3.02/3.19 (^[A: $i, B: $i] : refl(((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B))))) <=> ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(45,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B))))) <=> ![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[44])).
% 3.02/3.19 tff(46,plain,
% 3.02/3.19 (^[A: $i, B: $i] : rewrite(((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B))) <=> ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(47,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B))) <=> ![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[46])).
% 3.02/3.19 tff(48,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B))) <=> ![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B)))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(49,plain,
% 3.02/3.19 (^[A: $i, B: $i] : rewrite((m1_pboole(B, A) => (v1_relat_1(B) & v1_funct_1(B))) <=> ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(50,plain,
% 3.02/3.19 (![A: $i, B: $i] : (m1_pboole(B, A) => (v1_relat_1(B) & v1_funct_1(B))) <=> ![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B)))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[49])).
% 3.02/3.19 tff(51,axiom,(![A: $i, B: $i] : (m1_pboole(B, A) => (v1_relat_1(B) & v1_funct_1(B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dt_m1_pboole')).
% 3.02/3.19 tff(52,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[51, 50])).
% 3.02/3.19 tff(53,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B)))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[52, 48])).
% 3.02/3.19 tff(54,plain,(
% 3.02/3.19 ![A: $i, B: $i] : ((~m1_pboole(B, A)) | (v1_relat_1(B) & v1_funct_1(B)))),
% 3.02/3.19 inference(skolemize,[status(sab)],[53])).
% 3.02/3.19 tff(55,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[54, 47])).
% 3.02/3.19 tff(56,plain,
% 3.02/3.19 (![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[55, 45])).
% 3.02/3.19 tff(57,plain,
% 3.02/3.19 (((~![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))) | ((~m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))))) <=> ((~![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))) | (~m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(58,plain,
% 3.02/3.19 ((~![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))) | ((~m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))))),
% 3.02/3.19 inference(quant_inst,[status(thm)],[])).
% 3.02/3.19 tff(59,plain,
% 3.02/3.19 ((~![A: $i, B: $i] : ((~m1_pboole(B, A)) | (~((~v1_relat_1(B)) | (~v1_funct_1(B)))))) | (~m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0)))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[58, 57])).
% 3.02/3.19 tff(60,plain,
% 3.02/3.19 (~((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[59, 56, 43])).
% 3.02/3.19 tff(61,plain,
% 3.02/3.19 (((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0)))) | v1_funct_1(u1_altcat_1(A!0))),
% 3.02/3.19 inference(tautology,[status(thm)],[])).
% 3.02/3.19 tff(62,plain,
% 3.02/3.19 (v1_funct_1(u1_altcat_1(A!0))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[61, 60])).
% 3.02/3.19 tff(63,plain,
% 3.02/3.19 (((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0)))) | v1_relat_1(u1_altcat_1(A!0))),
% 3.02/3.19 inference(tautology,[status(thm)],[])).
% 3.02/3.19 tff(64,plain,
% 3.02/3.19 (v1_relat_1(u1_altcat_1(A!0))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[63, 60])).
% 3.02/3.19 tff(65,plain,
% 3.02/3.19 (^[A: $i] : refl(((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(66,plain,
% 3.02/3.19 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[65])).
% 3.02/3.19 tff(67,plain,
% 3.02/3.19 (^[A: $i] : rewrite(((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(68,plain,
% 3.02/3.19 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[67])).
% 3.02/3.19 tff(69,plain,
% 3.02/3.19 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(transitivity,[status(thm)],[68, 66])).
% 3.02/3.19 tff(70,plain,
% 3.02/3.19 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite((v1_relat_1(A) & v1_funct_1(A)) <=> (~((~v1_relat_1(A)) | (~v1_funct_1(A))))), ((~(v1_relat_1(A) & v1_funct_1(A))) <=> (~(~((~v1_relat_1(A)) | (~v1_funct_1(A))))))), rewrite((~(~((~v1_relat_1(A)) | (~v1_funct_1(A))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)))), ((~(v1_relat_1(A) & v1_funct_1(A))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A))))), quant_intro(proof_bind(^[B: $i, C: $i] : rewrite((((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))) <=> (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))), (![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))) <=> ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))), (((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> (((~v1_relat_1(A)) | (~v1_funct_1(A))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))))), rewrite((((~v1_relat_1(A)) | (~v1_funct_1(A))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))), (((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(71,plain,
% 3.02/3.19 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[70])).
% 3.02/3.19 tff(72,plain,
% 3.02/3.19 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(73,plain,
% 3.02/3.19 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i, C: $i] : rewrite(((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))) <=> (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))), (![B: $i, C: $i] : ((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))) <=> ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))), (((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : ((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))))), rewrite(((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))), (((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : ((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(bind,[status(th)],[])).
% 3.02/3.19 tff(74,plain,
% 3.02/3.19 (![A: $i] : ((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : ((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0))))) <=> ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))),
% 3.02/3.19 inference(quant_intro,[status(thm)],[73])).
% 3.02/3.19 tff(75,axiom,(![A: $i] : ((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : ((r2_hidden(B, k1_relat_1(A)) => ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & ((~r2_hidden(B, k1_relat_1(A))) => ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d4_funct_1')).
% 3.02/3.19 tff(76,plain,
% 3.02/3.19 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[75, 74])).
% 3.02/3.19 tff(77,plain,
% 3.02/3.19 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[76, 72])).
% 3.02/3.19 tff(78,plain,(
% 3.02/3.19 ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A))) & (r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))),
% 3.02/3.19 inference(skolemize,[status(sab)],[77])).
% 3.02/3.19 tff(79,plain,
% 3.02/3.19 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[78, 71])).
% 3.02/3.19 tff(80,plain,
% 3.02/3.19 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[79, 69])).
% 3.02/3.19 tff(81,plain,
% 3.02/3.19 (((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))) | ((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0)))))))) <=> ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(82,plain,
% 3.02/3.19 ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))) | ((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0)))))))),
% 3.02/3.19 inference(quant_inst,[status(thm)],[])).
% 3.02/3.19 tff(83,plain,
% 3.02/3.19 ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(A))) | ((C = k1_funct_1(A, B)) <=> r2_hidden(k4_tarski(B, C), A)))) | (~(r2_hidden(B, k1_relat_1(A)) | ((C = k1_funct_1(A, B)) <=> (C = k1_xboole_0)))))))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))),
% 3.02/3.19 inference(modus_ponens,[status(thm)],[82, 81])).
% 3.02/3.19 tff(84,plain,
% 3.02/3.19 (![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))),
% 3.02/3.19 inference(unit_resolution,[status(thm)],[83, 80, 64, 62])).
% 3.02/3.19 tff(85,plain,
% 3.02/3.19 (((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))))) <=> ((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(86,plain,
% 3.02/3.19 ((~((~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))) | (~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> (k1_xboole_0 = k1_xboole_0)))))) <=> (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))))),
% 3.02/3.19 inference(rewrite,[status(thm)],[])).
% 3.02/3.19 tff(87,plain,
% 3.02/3.19 (((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))) | (~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> (k1_xboole_0 = k1_xboole_0))))))) <=> ((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))))))),
% 3.02/3.20 inference(monotonicity,[status(thm)],[86])).
% 3.02/3.20 tff(88,plain,
% 3.02/3.20 (((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))) | (~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> (k1_xboole_0 = k1_xboole_0))))))) <=> ((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))))))),
% 3.02/3.20 inference(transitivity,[status(thm)],[87, 85])).
% 3.02/3.20 tff(89,plain,
% 3.02/3.20 ((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))) | (~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> (k1_xboole_0 = k1_xboole_0))))))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(90,plain,
% 3.02/3.20 ((~![B: $i, C: $i] : (~((~((~r2_hidden(B, k1_relat_1(u1_altcat_1(A!0)))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> r2_hidden(k4_tarski(B, C), u1_altcat_1(A!0))))) | (~(r2_hidden(B, k1_relat_1(u1_altcat_1(A!0))) | ((C = k1_funct_1(u1_altcat_1(A!0), B)) <=> (C = k1_xboole_0))))))) | (~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[89, 88])).
% 3.02/3.20 tff(91,plain,
% 3.02/3.20 ($false),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[90, 84, 1])).
% 3.02/3.20 tff(92,plain,(~((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0))))))), inference(lemma,lemma(discharge,[]))).
% 3.02/3.20 tff(93,assumption,(k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))), introduced(assumption)).
% 3.02/3.20 tff(94,plain,
% 3.02/3.20 (k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3))) = k1_xboole_0),
% 3.02/3.20 inference(symmetry,[status(thm)],[93])).
% 3.02/3.20 tff(95,plain,
% 3.02/3.20 (^[A: $i, B: $i] : refl((k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A))) <=> (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(96,plain,
% 3.02/3.20 (![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A))) <=> ![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[95])).
% 3.02/3.20 tff(97,plain,
% 3.02/3.20 (![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A))) <=> ![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(98,axiom,(![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d5_tarski')).
% 3.02/3.20 tff(99,plain,
% 3.02/3.20 (![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[98, 97])).
% 3.02/3.20 tff(100,plain,(
% 3.02/3.20 ![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))),
% 3.02/3.20 inference(skolemize,[status(sab)],[99])).
% 3.02/3.20 tff(101,plain,
% 3.02/3.20 (![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[100, 96])).
% 3.02/3.20 tff(102,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : (k4_tarski(A, B) = k2_tarski(k2_tarski(A, B), k1_tarski(A)))) | (k4_tarski(B!3, C!2) = k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(103,plain,
% 3.02/3.20 (k4_tarski(B!3, C!2) = k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[102, 101])).
% 3.02/3.20 tff(104,plain,
% 3.02/3.20 (k1_funct_1(u1_altcat_1(A!0), k4_tarski(B!3, C!2)) = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))),
% 3.02/3.20 inference(monotonicity,[status(thm)],[103])).
% 3.02/3.20 tff(105,plain,
% 3.02/3.20 (^[A: $i] : rewrite((![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(106,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> ![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[105])).
% 3.02/3.20 tff(107,plain,
% 3.02/3.20 (^[A: $i] : refl((![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(108,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> ![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[107])).
% 3.02/3.20 tff(109,plain,
% 3.02/3.20 (^[A: $i] : rewrite((![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(110,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> ![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[109])).
% 3.02/3.20 tff(111,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A))) <=> ![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(transitivity,[status(thm)],[110, 108])).
% 3.02/3.20 tff(112,plain,
% 3.02/3.20 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite((v1_relat_1(A) & v1_funct_1(A)) <=> (~((~v1_relat_1(A)) | (~v1_funct_1(A))))), ((~(v1_relat_1(A) & v1_funct_1(A))) <=> (~(~((~v1_relat_1(A)) | (~v1_funct_1(A))))))), rewrite((~(~((~v1_relat_1(A)) | (~v1_funct_1(A))))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A)))), ((~(v1_relat_1(A) & v1_funct_1(A))) <=> ((~v1_relat_1(A)) | (~v1_funct_1(A))))), (((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> (((~v1_relat_1(A)) | (~v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))))), rewrite((((~v1_relat_1(A)) | (~v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))), (((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(113,plain,
% 3.02/3.20 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> ![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[112])).
% 3.02/3.20 tff(114,plain,
% 3.02/3.20 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(115,plain,
% 3.02/3.20 (^[A: $i] : rewrite(((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(116,plain,
% 3.02/3.20 (![A: $i] : ((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C)))) <=> ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[115])).
% 3.02/3.20 tff(117,axiom,(![A: $i] : ((v1_relat_1(A) & v1_funct_1(A)) => ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d1_binop_1')).
% 3.02/3.20 tff(118,plain,
% 3.02/3.20 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[117, 116])).
% 3.02/3.20 tff(119,plain,
% 3.02/3.20 (![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[118, 114])).
% 3.02/3.20 tff(120,plain,(
% 3.02/3.20 ![A: $i] : ((~(v1_relat_1(A) & v1_funct_1(A))) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(skolemize,[status(sab)],[119])).
% 3.02/3.20 tff(121,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[120, 113])).
% 3.02/3.20 tff(122,plain,
% 3.02/3.20 (![A: $i] : (![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))) | (~v1_relat_1(A)) | (~v1_funct_1(A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[121, 111])).
% 3.02/3.20 tff(123,plain,
% 3.02/3.20 (![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[122, 106])).
% 3.02/3.20 tff(124,plain,
% 3.02/3.20 (((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))) | ((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C))))) <=> ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(125,plain,
% 3.02/3.20 ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))) | ((~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C))))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(126,plain,
% 3.02/3.20 ((~![A: $i] : ((~v1_relat_1(A)) | (~v1_funct_1(A)) | ![B: $i, C: $i] : (k1_binop_1(A, B, C) = k1_funct_1(A, k4_tarski(B, C))))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))) | ![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[125, 124])).
% 3.02/3.20 tff(127,plain,
% 3.02/3.20 (![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C)))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[126, 123, 64, 62])).
% 3.02/3.20 tff(128,plain,
% 3.02/3.20 ((~![B: $i, C: $i] : (k1_binop_1(u1_altcat_1(A!0), B, C) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B, C)))) | (k1_binop_1(u1_altcat_1(A!0), B!3, C!2) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B!3, C!2)))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(129,plain,
% 3.02/3.20 (k1_binop_1(u1_altcat_1(A!0), B!3, C!2) = k1_funct_1(u1_altcat_1(A!0), k4_tarski(B!3, C!2))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[128, 127])).
% 3.02/3.20 tff(130,plain,
% 3.02/3.20 (k1_binop_1(u1_altcat_1(A!0), B!3, C!2) = k1_xboole_0),
% 3.02/3.20 inference(transitivity,[status(thm)],[129, 104, 94])).
% 3.02/3.20 tff(131,plain,
% 3.02/3.20 (v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) <=> v1_xboole_0(k1_xboole_0)),
% 3.02/3.20 inference(monotonicity,[status(thm)],[130])).
% 3.02/3.20 tff(132,plain,
% 3.02/3.20 (v1_xboole_0(k1_xboole_0) <=> v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.20 inference(symmetry,[status(thm)],[131])).
% 3.02/3.20 tff(133,plain,
% 3.02/3.20 (v1_xboole_0(k1_xboole_0) <=> v1_xboole_0(k1_xboole_0)),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(134,axiom,(((((v1_xboole_0(k1_xboole_0) & v1_membered(k1_xboole_0)) & v2_membered(k1_xboole_0)) & v3_membered(k1_xboole_0)) & v4_membered(k1_xboole_0)) & v5_membered(k1_xboole_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','fc6_membered')).
% 3.02/3.20 tff(135,plain,
% 3.02/3.20 ((((v1_xboole_0(k1_xboole_0) & v1_membered(k1_xboole_0)) & v2_membered(k1_xboole_0)) & v3_membered(k1_xboole_0)) & v4_membered(k1_xboole_0)),
% 3.02/3.20 inference(and_elim,[status(thm)],[134])).
% 3.02/3.20 tff(136,plain,
% 3.02/3.20 (((v1_xboole_0(k1_xboole_0) & v1_membered(k1_xboole_0)) & v2_membered(k1_xboole_0)) & v3_membered(k1_xboole_0)),
% 3.02/3.20 inference(and_elim,[status(thm)],[135])).
% 3.02/3.20 tff(137,plain,
% 3.02/3.20 ((v1_xboole_0(k1_xboole_0) & v1_membered(k1_xboole_0)) & v2_membered(k1_xboole_0)),
% 3.02/3.20 inference(and_elim,[status(thm)],[136])).
% 3.02/3.20 tff(138,plain,
% 3.02/3.20 (v1_xboole_0(k1_xboole_0) & v1_membered(k1_xboole_0)),
% 3.02/3.20 inference(and_elim,[status(thm)],[137])).
% 3.02/3.20 tff(139,plain,
% 3.02/3.20 (v1_xboole_0(k1_xboole_0)),
% 3.02/3.20 inference(and_elim,[status(thm)],[138])).
% 3.02/3.20 tff(140,plain,
% 3.02/3.20 (v1_xboole_0(k1_xboole_0)),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[139, 133])).
% 3.02/3.20 tff(141,plain,
% 3.02/3.20 (v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[140, 132])).
% 3.02/3.20 tff(142,plain,
% 3.02/3.20 (^[A: $i, B: $i] : refl(((~v1_xboole_0(B)) | (~r2_hidden(A, B))) <=> ((~v1_xboole_0(B)) | (~r2_hidden(A, B))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(143,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B))) <=> ![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[142])).
% 3.02/3.20 tff(144,plain,
% 3.02/3.20 (^[A: $i, B: $i] : trans(monotonicity(rewrite((r2_hidden(A, B) & v1_xboole_0(B)) <=> (~((~v1_xboole_0(B)) | (~r2_hidden(A, B))))), ((~(r2_hidden(A, B) & v1_xboole_0(B))) <=> (~(~((~v1_xboole_0(B)) | (~r2_hidden(A, B))))))), rewrite((~(~((~v1_xboole_0(B)) | (~r2_hidden(A, B))))) <=> ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))), ((~(r2_hidden(A, B) & v1_xboole_0(B))) <=> ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(145,plain,
% 3.02/3.20 (![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B))) <=> ![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[144])).
% 3.02/3.20 tff(146,plain,
% 3.02/3.20 (![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B))) <=> ![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B)))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(147,axiom,(![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t7_boole')).
% 3.02/3.20 tff(148,plain,
% 3.02/3.20 (![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[147, 146])).
% 3.02/3.20 tff(149,plain,(
% 3.02/3.20 ![A: $i, B: $i] : (~(r2_hidden(A, B) & v1_xboole_0(B)))),
% 3.02/3.20 inference(skolemize,[status(sab)],[148])).
% 3.02/3.20 tff(150,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[149, 145])).
% 3.02/3.20 tff(151,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[150, 143])).
% 3.02/3.20 tff(152,plain,
% 3.02/3.20 (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.20 inference(and_elim,[status(thm)],[23])).
% 3.02/3.20 tff(153,plain,
% 3.02/3.20 (((~![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))) | ((~v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))))) <=> ((~![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))) | (~v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(154,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))) | ((~v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(155,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~v1_xboole_0(B)) | (~r2_hidden(A, B)))) | (~v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[154, 153])).
% 3.02/3.20 tff(156,plain,
% 3.02/3.20 (~v1_xboole_0(k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[155, 152, 151])).
% 3.02/3.20 tff(157,plain,
% 3.02/3.20 ($false),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[156, 141])).
% 3.02/3.20 tff(158,plain,(~(k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3))))), inference(lemma,lemma(discharge,[]))).
% 3.02/3.20 tff(159,plain,
% 3.02/3.20 (^[A: $i, B: $i] : refl(((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B))) <=> ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(160,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B))) <=> ![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[159])).
% 3.02/3.20 tff(161,plain,
% 3.02/3.20 (^[A: $i, B: $i] : trans(monotonicity(trans(monotonicity(rewrite((v1_relat_1(B) & v1_funct_1(B)) <=> (~((~v1_relat_1(B)) | (~v1_funct_1(B))))), ((~(v1_relat_1(B) & v1_funct_1(B))) <=> (~(~((~v1_relat_1(B)) | (~v1_funct_1(B))))))), rewrite((~(~((~v1_relat_1(B)) | (~v1_funct_1(B))))) <=> ((~v1_relat_1(B)) | (~v1_funct_1(B)))), ((~(v1_relat_1(B) & v1_funct_1(B))) <=> ((~v1_relat_1(B)) | (~v1_funct_1(B))))), (((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> (((~v1_relat_1(B)) | (~v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))))), rewrite((((~v1_relat_1(B)) | (~v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))), (((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(162,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[161])).
% 3.02/3.20 tff(163,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(164,plain,
% 3.02/3.20 (^[A: $i, B: $i] : rewrite(((v1_relat_1(B) & v1_funct_1(B)) => (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(165,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((v1_relat_1(B) & v1_funct_1(B)) => (m1_pboole(B, A) <=> (k1_relat_1(B) = A))) <=> ![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[164])).
% 3.02/3.20 tff(166,axiom,(![A: $i, B: $i] : ((v1_relat_1(B) & v1_funct_1(B)) => (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d3_pboole')).
% 3.02/3.20 tff(167,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[166, 165])).
% 3.02/3.20 tff(168,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[167, 163])).
% 3.02/3.20 tff(169,plain,(
% 3.02/3.20 ![A: $i, B: $i] : ((~(v1_relat_1(B) & v1_funct_1(B))) | (m1_pboole(B, A) <=> (k1_relat_1(B) = A)))),
% 3.02/3.20 inference(skolemize,[status(sab)],[168])).
% 3.02/3.20 tff(170,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[169, 162])).
% 3.02/3.20 tff(171,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[170, 160])).
% 3.02/3.20 tff(172,plain,
% 3.02/3.20 (((~![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))) | ((m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))) <=> ((~![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))) | (m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(173,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))) | ((m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0))))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(174,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((m1_pboole(B, A) <=> (k1_relat_1(B) = A)) | (~v1_relat_1(B)) | (~v1_funct_1(B)))) | (m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0)))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[173, 172])).
% 3.02/3.20 tff(175,plain,
% 3.02/3.20 ((m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~v1_relat_1(u1_altcat_1(A!0))) | (~v1_funct_1(u1_altcat_1(A!0)))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[174, 171])).
% 3.02/3.20 tff(176,plain,
% 3.02/3.20 (m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[175, 64, 62])).
% 3.02/3.20 tff(177,plain,
% 3.02/3.20 ((~(m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))) | (~m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.20 inference(tautology,[status(thm)],[])).
% 3.02/3.20 tff(178,plain,
% 3.02/3.20 ((~(m1_pboole(u1_altcat_1(A!0), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))) | (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[177, 43])).
% 3.02/3.20 tff(179,plain,
% 3.02/3.20 (k1_relat_1(u1_altcat_1(A!0)) = k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[178, 176])).
% 3.02/3.20 tff(180,plain,
% 3.02/3.20 (k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)) = k4_tarski(B!3, C!2)),
% 3.02/3.20 inference(symmetry,[status(thm)],[103])).
% 3.02/3.20 tff(181,plain,
% 3.02/3.20 (r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) <=> r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.20 inference(monotonicity,[status(thm)],[180, 179])).
% 3.02/3.20 tff(182,plain,
% 3.02/3.20 (r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))) <=> r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))),
% 3.02/3.20 inference(symmetry,[status(thm)],[181])).
% 3.02/3.20 tff(183,plain,
% 3.02/3.20 ((~r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) <=> (~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))))),
% 3.02/3.20 inference(monotonicity,[status(thm)],[182])).
% 3.02/3.20 tff(184,assumption,(~((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0))))), introduced(assumption)).
% 3.02/3.20 tff(185,plain,
% 3.02/3.20 (((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))) | r2_hidden(C!2, u1_struct_0(A!0))),
% 3.02/3.20 inference(tautology,[status(thm)],[])).
% 3.02/3.20 tff(186,plain,
% 3.02/3.20 (r2_hidden(C!2, u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[185, 184])).
% 3.02/3.20 tff(187,plain,
% 3.02/3.20 (^[A: $i, B: $i] : refl(((~r2_hidden(A, B)) | m1_subset_1(A, B)) <=> ((~r2_hidden(A, B)) | m1_subset_1(A, B)))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(188,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B)) <=> ![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[187])).
% 3.02/3.20 tff(189,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B)) <=> ![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(190,plain,
% 3.02/3.20 (^[A: $i, B: $i] : rewrite((r2_hidden(A, B) => m1_subset_1(A, B)) <=> ((~r2_hidden(A, B)) | m1_subset_1(A, B)))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(191,plain,
% 3.02/3.20 (![A: $i, B: $i] : (r2_hidden(A, B) => m1_subset_1(A, B)) <=> ![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[190])).
% 3.02/3.20 tff(192,axiom,(![A: $i, B: $i] : (r2_hidden(A, B) => m1_subset_1(A, B))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t1_subset')).
% 3.02/3.20 tff(193,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[192, 191])).
% 3.02/3.20 tff(194,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[193, 189])).
% 3.02/3.20 tff(195,plain,(
% 3.02/3.20 ![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(skolemize,[status(sab)],[194])).
% 3.02/3.20 tff(196,plain,
% 3.02/3.20 (![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[195, 188])).
% 3.02/3.20 tff(197,plain,
% 3.02/3.20 (((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(C!2, u1_struct_0(A!0))) | m1_subset_1(C!2, u1_struct_0(A!0)))) <=> ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(C!2, u1_struct_0(A!0))) | m1_subset_1(C!2, u1_struct_0(A!0)))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(198,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(C!2, u1_struct_0(A!0))) | m1_subset_1(C!2, u1_struct_0(A!0)))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(199,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(C!2, u1_struct_0(A!0))) | m1_subset_1(C!2, u1_struct_0(A!0))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[198, 197])).
% 3.02/3.20 tff(200,plain,
% 3.02/3.20 (m1_subset_1(C!2, u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[199, 196, 186])).
% 3.02/3.20 tff(201,plain,
% 3.02/3.20 (((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))) | r2_hidden(B!3, u1_struct_0(A!0))),
% 3.02/3.20 inference(tautology,[status(thm)],[])).
% 3.02/3.20 tff(202,plain,
% 3.02/3.20 (r2_hidden(B!3, u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[201, 184])).
% 3.02/3.20 tff(203,plain,
% 3.02/3.20 (((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(B!3, u1_struct_0(A!0))) | m1_subset_1(B!3, u1_struct_0(A!0)))) <=> ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(B!3, u1_struct_0(A!0))) | m1_subset_1(B!3, u1_struct_0(A!0)))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(204,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(B!3, u1_struct_0(A!0))) | m1_subset_1(B!3, u1_struct_0(A!0)))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(205,plain,
% 3.02/3.20 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(B!3, u1_struct_0(A!0))) | m1_subset_1(B!3, u1_struct_0(A!0))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[204, 203])).
% 3.02/3.20 tff(206,plain,
% 3.02/3.20 ((~r2_hidden(B!3, u1_struct_0(A!0))) | m1_subset_1(B!3, u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[205, 196])).
% 3.02/3.20 tff(207,plain,
% 3.02/3.20 (m1_subset_1(B!3, u1_struct_0(A!0))),
% 3.02/3.20 inference(unit_resolution,[status(thm)],[206, 202])).
% 3.02/3.20 tff(208,plain,
% 3.02/3.20 (^[A: $i] : refl(((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(209,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[208])).
% 3.02/3.20 tff(210,plain,
% 3.02/3.20 (^[A: $i] : rewrite(((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(211,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[210])).
% 3.02/3.20 tff(212,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(transitivity,[status(thm)],[211, 209])).
% 3.02/3.20 tff(213,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(214,plain,
% 3.02/3.20 (^[A: $i] : trans(monotonicity(quant_intro(proof_bind(^[B: $i] : trans(monotonicity(quant_intro(proof_bind(^[C: $i] : rewrite((m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))) <=> ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))), (![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))) <=> ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))), ((m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))) <=> (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))), rewrite((m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))) <=> ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))), ((m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))) <=> ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))))), (![B: $i] : (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))) <=> ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))), ((l1_altcat_1(A) => ![B: $i] : (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> (l1_altcat_1(A) => ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))))), rewrite((l1_altcat_1(A) => ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))), ((l1_altcat_1(A) => ![B: $i] : (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))))),
% 3.02/3.20 inference(bind,[status(th)],[])).
% 3.02/3.20 tff(215,plain,
% 3.02/3.20 (![A: $i] : (l1_altcat_1(A) => ![B: $i] : (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C))))) <=> ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(quant_intro,[status(thm)],[214])).
% 3.02/3.20 tff(216,axiom,(![A: $i] : (l1_altcat_1(A) => ![B: $i] : (m1_subset_1(B, u1_struct_0(A)) => ![C: $i] : (m1_subset_1(C, u1_struct_0(A)) => (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','d2_altcat_1')).
% 3.02/3.20 tff(217,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[216, 215])).
% 3.02/3.20 tff(218,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[217, 213])).
% 3.02/3.20 tff(219,plain,(
% 3.02/3.20 ![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(skolemize,[status(sab)],[218])).
% 3.02/3.20 tff(220,plain,
% 3.02/3.20 (![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[219, 212])).
% 3.02/3.20 tff(221,plain,
% 3.02/3.20 (((~![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))) | ((~l1_altcat_1(A!0)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C)))))) <=> ((~![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))) | (~l1_altcat_1(A!0)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C)))))),
% 3.02/3.20 inference(rewrite,[status(thm)],[])).
% 3.02/3.20 tff(222,plain,
% 3.02/3.20 ((~![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))) | ((~l1_altcat_1(A!0)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C)))))),
% 3.02/3.20 inference(quant_inst,[status(thm)],[])).
% 3.02/3.20 tff(223,plain,
% 3.02/3.20 ((~![A: $i] : ((~l1_altcat_1(A)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A))) | (k1_altcat_1(A, B, C) = k1_binop_1(u1_altcat_1(A), B, C)))))) | (~l1_altcat_1(A!0)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))),
% 3.02/3.20 inference(modus_ponens,[status(thm)],[222, 221])).
% 3.02/3.20 tff(224,plain,
% 3.02/3.20 ((~l1_altcat_1(A!0)) | ![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[223, 220])).
% 3.02/3.21 tff(225,plain,
% 3.02/3.21 (![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[224, 28])).
% 3.02/3.21 tff(226,plain,
% 3.02/3.21 (((~![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))) | ((~m1_subset_1(B!3, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C))))) <=> ((~![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))) | (~m1_subset_1(B!3, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C))))),
% 3.02/3.21 inference(rewrite,[status(thm)],[])).
% 3.02/3.21 tff(227,plain,
% 3.02/3.21 ((~![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))) | ((~m1_subset_1(B!3, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C))))),
% 3.02/3.21 inference(quant_inst,[status(thm)],[])).
% 3.02/3.21 tff(228,plain,
% 3.02/3.21 ((~![B: $i] : ((~m1_subset_1(B, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B, C) = k1_binop_1(u1_altcat_1(A!0), B, C))))) | (~m1_subset_1(B!3, u1_struct_0(A!0))) | ![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[227, 226])).
% 3.02/3.21 tff(229,plain,
% 3.02/3.21 (![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[228, 207, 225])).
% 3.02/3.21 tff(230,plain,
% 3.02/3.21 (((~![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))) | ((~m1_subset_1(C!2, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C!2) = k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))) <=> ((~![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C!2) = k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))),
% 3.02/3.21 inference(rewrite,[status(thm)],[])).
% 3.02/3.21 tff(231,plain,
% 3.02/3.21 ((~![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))) | ((~m1_subset_1(C!2, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C!2) = k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))),
% 3.02/3.21 inference(quant_inst,[status(thm)],[])).
% 3.02/3.21 tff(232,plain,
% 3.02/3.21 ((~![C: $i] : ((~m1_subset_1(C, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C) = k1_binop_1(u1_altcat_1(A!0), B!3, C)))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (k1_altcat_1(A!0, B!3, C!2) = k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[231, 230])).
% 3.02/3.21 tff(233,plain,
% 3.02/3.21 (k1_altcat_1(A!0, B!3, C!2) = k1_binop_1(u1_altcat_1(A!0), B!3, C!2)),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[232, 200, 229])).
% 3.02/3.21 tff(234,plain,
% 3.02/3.21 (m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2)) <=> m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.21 inference(monotonicity,[status(thm)],[233])).
% 3.02/3.21 tff(235,plain,
% 3.02/3.21 (m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) <=> m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))),
% 3.02/3.21 inference(symmetry,[status(thm)],[234])).
% 3.02/3.21 tff(236,plain,
% 3.02/3.21 (((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))) <=> ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))),
% 3.02/3.21 inference(rewrite,[status(thm)],[])).
% 3.02/3.21 tff(237,plain,
% 3.02/3.21 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | ((~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)))),
% 3.02/3.21 inference(quant_inst,[status(thm)],[])).
% 3.02/3.21 tff(238,plain,
% 3.02/3.21 ((~![A: $i, B: $i] : ((~r2_hidden(A, B)) | m1_subset_1(A, B))) | (~r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))) | m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[237, 236])).
% 3.02/3.21 tff(239,plain,
% 3.02/3.21 (m1_subset_1(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[238, 152, 196])).
% 3.02/3.21 tff(240,plain,
% 3.02/3.21 (m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[239, 235])).
% 3.02/3.21 tff(241,plain,
% 3.02/3.21 (r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)) <=> r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2))),
% 3.02/3.21 inference(monotonicity,[status(thm)],[233])).
% 3.02/3.21 tff(242,plain,
% 3.02/3.21 (r2_hidden(D!1, k1_binop_1(u1_altcat_1(A!0), B!3, C!2)) <=> r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2))),
% 3.02/3.21 inference(symmetry,[status(thm)],[241])).
% 3.02/3.21 tff(243,plain,
% 3.02/3.21 (r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[152, 242])).
% 3.02/3.21 tff(244,plain,
% 3.02/3.21 ((~m1_subset_1(B!3, u1_struct_0(A!0))) | (~m1_subset_1(D!1, k1_altcat_1(A!0, B!3, C!2))) | (~m1_subset_1(C!2, u1_struct_0(A!0))) | (~r2_hidden(D!1, k1_altcat_1(A!0, B!3, C!2)))),
% 3.02/3.21 inference(and_elim,[status(thm)],[23])).
% 3.02/3.21 tff(245,plain,
% 3.02/3.21 ($false),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[244, 243, 240, 207, 200])).
% 3.02/3.21 tff(246,plain,((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))), inference(lemma,lemma(discharge,[]))).
% 3.02/3.21 tff(247,plain,
% 3.02/3.21 (^[A: $i, B: $i, C: $i, D: $i] : refl((~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)))) <=> (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)))))),
% 3.02/3.21 inference(bind,[status(th)],[])).
% 3.02/3.21 tff(248,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)))) <=> ![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))),
% 3.02/3.21 inference(quant_intro,[status(thm)],[247])).
% 3.02/3.21 tff(249,plain,
% 3.02/3.21 (^[A: $i, B: $i, C: $i, D: $i] : trans(trans(monotonicity(rewrite((r2_hidden(A, C) & r2_hidden(B, D)) <=> (~((~r2_hidden(A, C)) | (~r2_hidden(B, D))))), ((r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D))) <=> (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (~((~r2_hidden(A, C)) | (~r2_hidden(B, D))))))), rewrite((r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (~((~r2_hidden(A, C)) | (~r2_hidden(B, D))))) <=> (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))), ((r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D))) <=> (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)))))), rewrite((~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)))) <=> (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))), ((r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D))) <=> (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))))),
% 3.02/3.21 inference(bind,[status(th)],[])).
% 3.02/3.21 tff(250,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D))) <=> ![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))),
% 3.02/3.21 inference(quant_intro,[status(thm)],[249])).
% 3.02/3.21 tff(251,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D))) <=> ![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D)))),
% 3.02/3.21 inference(rewrite,[status(thm)],[])).
% 3.02/3.21 tff(252,axiom,(![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','t106_zfmisc_1')).
% 3.02/3.21 tff(253,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D)))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[252, 251])).
% 3.02/3.21 tff(254,plain,(
% 3.02/3.21 ![A: $i, B: $i, C: $i, D: $i] : (r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D)) <=> (r2_hidden(A, C) & r2_hidden(B, D)))),
% 3.02/3.21 inference(skolemize,[status(sab)],[253])).
% 3.02/3.21 tff(255,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[254, 250])).
% 3.02/3.21 tff(256,plain,
% 3.02/3.21 (![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[255, 248])).
% 3.02/3.21 tff(257,plain,
% 3.02/3.21 ((~![A: $i, B: $i, C: $i, D: $i] : (~(((~r2_hidden(A, C)) | (~r2_hidden(B, D))) <=> r2_hidden(k4_tarski(A, B), k2_zfmisc_1(C, D))))) | (~(((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))) <=> r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))))),
% 3.02/3.21 inference(quant_inst,[status(thm)],[])).
% 3.02/3.21 tff(258,plain,
% 3.02/3.21 (~(((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))) <=> r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[257, 256])).
% 3.02/3.21 tff(259,plain,
% 3.02/3.21 ((((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0)))) <=> r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))) | (~((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0))))) | (~r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))),
% 3.02/3.21 inference(tautology,[status(thm)],[])).
% 3.02/3.21 tff(260,plain,
% 3.02/3.21 ((~((~r2_hidden(B!3, u1_struct_0(A!0))) | (~r2_hidden(C!2, u1_struct_0(A!0))))) | (~r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[259, 258])).
% 3.02/3.21 tff(261,plain,
% 3.02/3.21 (~r2_hidden(k4_tarski(B!3, C!2), k2_zfmisc_1(u1_struct_0(A!0), u1_struct_0(A!0)))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[260, 246])).
% 3.02/3.21 tff(262,plain,
% 3.02/3.21 (~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))),
% 3.02/3.21 inference(modus_ponens,[status(thm)],[261, 183])).
% 3.02/3.21 tff(263,plain,
% 3.02/3.21 ((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3))))),
% 3.02/3.21 inference(tautology,[status(thm)],[])).
% 3.02/3.21 tff(264,plain,
% 3.02/3.21 (~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[263, 262, 158])).
% 3.02/3.21 tff(265,plain,
% 3.02/3.21 (((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))) | (r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))),
% 3.02/3.21 inference(tautology,[status(thm)],[])).
% 3.02/3.21 tff(266,plain,
% 3.02/3.21 ((~(r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0))) | (k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))))) | (~((~r2_hidden(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_relat_1(u1_altcat_1(A!0)))) | ((k1_xboole_0 = k1_funct_1(u1_altcat_1(A!0), k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)))) <=> r2_hidden(k4_tarski(k2_tarski(k2_tarski(B!3, C!2), k1_tarski(B!3)), k1_xboole_0), u1_altcat_1(A!0)))))),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[265, 264])).
% 3.02/3.21 tff(267,plain,
% 3.02/3.21 ($false),
% 3.02/3.21 inference(unit_resolution,[status(thm)],[266, 92])).
% 3.02/3.21 % SZS output end Proof
% 3.02/3.22 % E exiting
%------------------------------------------------------------------------------