%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN036+2 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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:37:59 AM UTC 2025
% Result : Theorem 0.12s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN036+2 : TPTP v9.0.0. Released v2.0.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:26:08 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.38 % SZS status Theorem
% 0.12/0.38 % SZS output start Proof
% 0.12/0.38 tff(big_q_type, type, (
% 0.12/0.38 big_q: $i > $o)).
% 0.12/0.38 tff(tptp_fun_W1_7_type, type, (
% 0.12/0.38 tptp_fun_W1_7: $i)).
% 0.12/0.38 tff(tptp_fun_Y1_5_type, type, (
% 0.12/0.38 tptp_fun_Y1_5: $i > $i)).
% 0.12/0.38 tff(big_p_type, type, (
% 0.12/0.38 big_p: $i > $o)).
% 0.12/0.38 tff(tptp_fun_U1_6_type, type, (
% 0.12/0.38 tptp_fun_U1_6: $i)).
% 0.12/0.38 tff(tptp_fun_X1_4_type, type, (
% 0.12/0.38 tptp_fun_X1_4: $i)).
% 0.12/0.38 tff(tptp_fun_W_3_type, type, (
% 0.12/0.38 tptp_fun_W_3: $i)).
% 0.12/0.38 tff(tptp_fun_U_2_type, type, (
% 0.12/0.38 tptp_fun_U_2: $i)).
% 0.12/0.38 tff(tptp_fun_X_0_type, type, (
% 0.12/0.38 tptp_fun_X_0: $i)).
% 0.12/0.38 tff(tptp_fun_Y_1_type, type, (
% 0.12/0.38 tptp_fun_Y_1: $i > $i)).
% 0.12/0.38 tff(elem_8_type, type, (
% 0.12/0.38 elem_8: $i)).
% 0.12/0.38 tff(elem_12_type, type, (
% 0.12/0.38 elem_12: $i)).
% 0.12/0.38 tff(1,assumption,(~big_q(W1!7)), introduced(assumption)).
% 0.12/0.38 tff(2,assumption,(~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U)))))))))), introduced(assumption)).
% 0.12/0.38 tff(3,plain,
% 0.12/0.38 (((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U))))))))) | (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U)))))))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(4,plain,
% 0.12/0.38 (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U))))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[3, 2])).
% 0.12/0.38 tff(5,plain,
% 0.12/0.38 (((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U))))))))) | (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(6,plain,
% 0.12/0.38 (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[5, 2])).
% 0.12/0.38 tff(7,assumption,(~![U: $i] : (~big_q(U))), introduced(assumption)).
% 0.12/0.38 tff(8,assumption,(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))))), introduced(assumption)).
% 0.12/0.38 tff(9,assumption,(~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))), introduced(assumption)).
% 0.12/0.38 tff(10,plain,
% 0.12/0.38 (((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))) | (big_q(U!2) | (~big_p(W!3)))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(11,plain,
% 0.12/0.38 (big_q(U!2) | (~big_p(W!3))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[10, 9])).
% 0.12/0.38 tff(12,plain,
% 0.12/0.38 ((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))))) | ((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(13,plain,
% 0.12/0.38 (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[12, 9])).
% 0.12/0.38 tff(14,assumption,(~big_p(U1!6)), introduced(assumption)).
% 0.12/0.38 tff(15,assumption,(![W: $i] : big_p(W)), introduced(assumption)).
% 0.12/0.38 tff(16,plain,
% 0.12/0.38 ((~![W: $i] : big_p(W)) | big_p(U1!6)),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(17,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[16, 15, 14])).
% 0.12/0.38 tff(18,plain,((~![W: $i] : big_p(W)) | big_p(U1!6)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(19,plain,
% 0.12/0.38 (~![W: $i] : big_p(W)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[18, 14])).
% 0.12/0.38 tff(20,assumption,(![W1: $i] : big_q(W1)), introduced(assumption)).
% 0.12/0.38 tff(21,plain,
% 0.12/0.38 ((~![W1: $i] : big_q(W1)) | big_q(W1!7)),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(22,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[21, 1, 20])).
% 0.12/0.38 tff(23,plain,(big_q(W1!7) | (~![W1: $i] : big_q(W1))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(24,plain,
% 0.12/0.38 (~![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[23, 1])).
% 0.12/0.38 tff(25,plain,
% 0.12/0.38 ((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | big_p(U1!6) | ![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(26,plain,
% 0.12/0.38 (~(big_p(U1!6) | ![W1: $i] : big_q(W1))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[25, 24, 14])).
% 0.12/0.38 tff(27,plain,
% 0.12/0.38 (((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))) | (big_p(U1!6) | ![W1: $i] : big_q(W1))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(28,plain,
% 0.12/0.38 ((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.12/0.38 tff(29,assumption,((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)))), introduced(assumption)).
% 0.12/0.38 tff(30,assumption,((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))), introduced(assumption)).
% 0.12/0.38 tff(31,assumption,(~![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1))))), introduced(assumption)).
% 0.12/0.38 tff(32,assumption,(~((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))))), introduced(assumption)).
% 0.12/0.38 tff(33,plain,
% 0.12/0.38 (((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)))) | (![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(34,plain,
% 0.12/0.38 (![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[33, 32])).
% 0.12/0.38 tff(35,plain,
% 0.12/0.38 (((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)))) | (big_p(U1!6) | (~big_q(W1!7)))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(36,plain,
% 0.12/0.38 (big_p(U1!6) | (~big_q(W1!7))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[35, 32])).
% 0.12/0.38 tff(37,assumption,(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)), introduced(assumption)).
% 0.12/0.38 tff(38,assumption,(~![W1: $i] : big_q(W1)), introduced(assumption)).
% 0.12/0.38 tff(39,plain,
% 0.12/0.38 ((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))) | ![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(40,plain,
% 0.12/0.38 (![U1: $i] : (~big_p(U1))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[39, 38, 37])).
% 0.12/0.38 tff(41,assumption,(big_p(tptp_fun_Y_1(U1!6))), introduced(assumption)).
% 0.12/0.38 tff(42,assumption,(![U1: $i] : (~big_p(U1))), introduced(assumption)).
% 0.12/0.38 tff(43,plain,
% 0.12/0.38 ((~![U1: $i] : (~big_p(U1))) | (~big_p(tptp_fun_Y_1(U1!6)))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(44,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[43, 42, 41])).
% 0.12/0.38 tff(45,plain,((~big_p(tptp_fun_Y_1(U1!6))) | (~![U1: $i] : (~big_p(U1)))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(46,plain,
% 0.12/0.38 (~big_p(tptp_fun_Y_1(U1!6))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[45, 40])).
% 0.12/0.38 tff(47,assumption,(big_p(U1!6) | ![W1: $i] : big_q(W1)), introduced(assumption)).
% 0.12/0.38 tff(48,plain,
% 0.12/0.38 (big_p(U1!6)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[25, 38, 47])).
% 0.12/0.38 tff(49,plain,
% 0.12/0.38 ((~![U1: $i] : (~big_p(U1))) | (~big_p(U1!6))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(50,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[49, 48, 40])).
% 0.12/0.38 tff(51,plain,(![W1: $i] : big_q(W1) | (~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(52,plain,
% 0.12/0.38 (~(big_p(U1!6) | ![W1: $i] : big_q(W1))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[51, 38, 37])).
% 0.12/0.38 tff(53,plain,
% 0.12/0.38 ((big_p(U1!6) | ![W1: $i] : big_q(W1)) | (~big_p(U1!6))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(54,plain,
% 0.12/0.38 (~big_p(U1!6)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[53, 52])).
% 0.12/0.38 tff(55,assumption,(~big_p(tptp_fun_Y_1(U1!6))), introduced(assumption)).
% 0.12/0.38 tff(56,plain,
% 0.12/0.38 ((big_p(U1!6) <=> big_p(tptp_fun_Y_1(U1!6))) | big_p(U1!6) | big_p(tptp_fun_Y_1(U1!6))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(57,plain,
% 0.12/0.38 (big_p(U1!6) <=> big_p(tptp_fun_Y_1(U1!6))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[56, 14, 55])).
% 0.12/0.38 tff(58,assumption,(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))), introduced(assumption)).
% 0.12/0.38 tff(59,plain,
% 0.12/0.38 ((~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))) | (~(big_p(U1!6) <=> big_p(tptp_fun_Y_1(U1!6))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(60,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[59, 58, 57])).
% 0.12/0.38 tff(61,plain,((~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))) | big_p(U1!6) | big_p(tptp_fun_Y_1(U1!6))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(62,plain,
% 0.12/0.38 (~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[61, 54, 46])).
% 0.12/0.38 tff(63,plain,
% 0.12/0.38 (~![W: $i] : big_p(W)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[18, 54])).
% 0.12/0.38 tff(64,assumption,(big_p(U1!6) | (~big_q(W1!7))), introduced(assumption)).
% 0.12/0.38 tff(65,assumption,(~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))))), introduced(assumption)).
% 0.12/0.38 tff(66,plain,
% 0.12/0.38 (((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))) | ((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(67,plain,
% 0.12/0.38 ((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[66, 65])).
% 0.12/0.38 tff(68,plain,
% 0.12/0.38 (big_p(U1!6) | ![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[27, 65])).
% 0.12/0.38 tff(69,plain,
% 0.12/0.38 (![W1: $i] : big_q(W1)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[51, 68, 37])).
% 0.12/0.38 tff(70,plain,
% 0.12/0.38 (big_q(W1!7)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[23, 69])).
% 0.12/0.38 tff(71,plain,
% 0.12/0.38 ((~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))) | (~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(72,plain,
% 0.12/0.38 (![U1: $i] : (~big_p(U1))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[71, 70, 67])).
% 0.12/0.38 tff(73,plain,
% 0.12/0.38 ((~(big_p(U1!6) | (~big_q(W1!7)))) | big_p(U1!6) | (~big_q(W1!7))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(74,plain,
% 0.12/0.38 (big_p(U1!6)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[73, 70, 64])).
% 0.12/0.38 tff(75,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[49, 74, 72])).
% 0.12/0.38 tff(76,plain,(((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))) | (~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(77,plain,
% 0.12/0.38 ((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[76, 64, 37])).
% 0.12/0.38 tff(78,plain,
% 0.12/0.38 (~big_q(W1!7)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[73, 54, 64])).
% 0.12/0.38 tff(79,assumption,(![U: $i] : (~big_q(U))), introduced(assumption)).
% 0.12/0.38 tff(80,assumption,(~![W: $i] : big_p(W)), introduced(assumption)).
% 0.12/0.38 tff(81,assumption,(~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))), introduced(assumption)).
% 0.12/0.38 tff(82,assumption,(big_q(tptp_fun_Y1_5(W1!7))), introduced(assumption)).
% 0.12/0.38 tff(83,plain,
% 0.12/0.38 ((~![U: $i] : (~big_q(U))) | (~big_q(tptp_fun_Y1_5(W1!7)))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(84,plain,
% 0.12/0.38 ($false),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[83, 79, 82])).
% 0.12/0.38 tff(85,plain,((~big_q(tptp_fun_Y1_5(W1!7))) | (~![U: $i] : (~big_q(U)))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(86,plain,
% 0.12/0.38 (~big_q(tptp_fun_Y1_5(W1!7))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[85, 79])).
% 0.12/0.38 tff(87,assumption,(~big_q(tptp_fun_Y1_5(W1!7))), introduced(assumption)).
% 0.12/0.38 tff(88,plain,
% 0.12/0.38 ((big_q(W1!7) <=> big_q(tptp_fun_Y1_5(W1!7))) | big_q(W1!7) | big_q(tptp_fun_Y1_5(W1!7))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(89,plain,
% 0.12/0.38 (big_q(W1!7) <=> big_q(tptp_fun_Y1_5(W1!7))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[88, 1, 87])).
% 0.12/0.39 tff(90,assumption,(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1))))), introduced(assumption)).
% 0.12/0.39 tff(91,plain,
% 0.12/0.39 ((~![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1))))) | (~(big_q(W1!7) <=> big_q(tptp_fun_Y1_5(W1!7))))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(92,plain,
% 0.12/0.39 ($false),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[91, 90, 89])).
% 0.12/0.39 tff(93,plain,((~![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1))))) | big_q(W1!7) | big_q(tptp_fun_Y1_5(W1!7))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.39 tff(94,plain,
% 0.12/0.39 (~![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[93, 86, 1])).
% 0.12/0.39 tff(95,plain,
% 0.12/0.39 ((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))))))) | ![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))))),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(96,plain,
% 0.12/0.39 (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[95, 94, 30])).
% 0.12/0.39 tff(97,plain,
% 0.12/0.39 (((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))))))) | (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))))))),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(98,plain,
% 0.12/0.39 ((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1))))))))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[97, 96])).
% 0.12/0.39 tff(99,plain,
% 0.12/0.39 (((~((~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))) | (~(big_q(U!2) | (~big_p(W!3)))))))) | (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~(![U: $i] : (~big_q(U)) | (~big_p(W!3)))))))))) | (~((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))) | (~(big_p(U1!6) | (~big_q(W1!7)))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))))))) <=> ((~((~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | (~big_p(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))))))) | (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~((~big_p(W!3)) | ![U: $i] : (~big_q(U)))))))))) | (~((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | (~big_q(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~((~big_q(W1!7)) | ![U1: $i] : (~big_p(U1)))))))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(100,plain,
% 0.12/0.39 (((~((~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))) | (~(big_q(U!2) | (~big_p(W!3)))))))) | (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~(![U: $i] : (~big_q(U)) | (~big_p(W!3)))))))))) | (~((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))) | (~(big_p(U1!6) | (~big_q(W1!7)))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))))))) <=> ((~((~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))) | (~(big_q(U!2) | (~big_p(W!3)))))))) | (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~(![U: $i] : (~big_q(U)) | (~big_p(W!3)))))))))) | (~((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))) | (~(big_p(U1!6) | (~big_q(W1!7)))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(101,plain,
% 0.12/0.39 ((((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))) <=> ((~((~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W))) | (~(big_q(U!2) | (~big_p(W!3)))))))) | (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | ![W: $i] : big_p(W))) | (~(![U: $i] : (~big_q(U)) | (~big_p(W!3)))))))))) | (~((~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1))) | (~(big_p(U1!6) | (~big_q(W1!7)))))))) | (~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | ![W1: $i] : big_q(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(102,plain,
% 0.12/0.39 (((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))) <=> ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(103,plain,
% 0.12/0.39 (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) <=> ((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(104,plain,
% 0.12/0.39 ((((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))) <=> (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[103, 102])).
% 0.12/0.39 tff(105,plain,
% 0.12/0.39 (((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))) <=> ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(106,plain,
% 0.12/0.39 (((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) <=> ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3))))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(107,plain,
% 0.12/0.39 ((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))) <=> (((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[106, 105])).
% 0.12/0.39 tff(108,plain,
% 0.12/0.39 (((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))) & (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7)))))))) <=> ((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))) & (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_p(W)) & (big_q(U!2) | (~big_p(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_p(W)) & (![U: $i] : (~big_q(U)) | (~big_p(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_q(W1)) & (big_p(U1!6) | (~big_q(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_q(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_q(W1!7))))))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[107, 104])).
% 0.12/0.40 tff(109,plain,
% 0.12/0.40 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1)))))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(110,plain,
% 0.12/0.40 ((?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(111,plain,
% 0.12/0.40 ((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(112,plain,
% 0.12/0.40 (((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1)))) <=> ((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[111, 110])).
% 0.12/0.40 tff(113,plain,
% 0.12/0.40 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1)))))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[112])).
% 0.12/0.40 tff(114,plain,
% 0.12/0.40 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1)))))),
% 0.12/0.40 inference(transitivity,[status(thm)],[113, 109])).
% 0.12/0.40 tff(115,axiom,(~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','pel34')).
% 0.12/0.40 tff(116,plain,
% 0.12/0.40 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.12/0.40 tff(117,plain,
% 0.12/0.40 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[116, 114])).
% 0.21/0.41 tff(118,plain,
% 0.21/0.41 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[117, 109])).
% 0.21/0.41 tff(119,plain,
% 0.21/0.41 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_p(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_q(W1))))),
% 0.21/0.41 inference(modus_ponens,[status(thm)],[118, 114])).
% 0.21/0.41 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (forall ((Y $i)) (= (big_p X) (big_p Y)))))
% 0.21/0.41 (a!2 (forall ((Y $i)) (= (big_p X!0) (big_p Y))))
% 0.21/0.41 (a!3 (lambda ((Y $i))
% 0.21/0.41 (refl (~ (= (big_p X!0) (big_p Y)) (= (big_p X!0) (big_p Y))))))
% 0.21/0.41 (a!5 (lambda ((X $i))
% 0.21/0.41 (let ((a!1 (forall ((Y $i)) (= (big_p X) (big_p Y))))
% 0.21/0.41 (a!2 (not (= (big_p X) (big_p (Y!1 X))))))
% 0.21/0.41 (sk (~ (not a!1) a!2)))))
% 0.21/0.41 (a!6 (forall ((X $i)) (not (= (big_p X) (big_p (Y!1 X))))))
% 0.21/0.41 (a!7 (exists ((U $i)) (big_q U)))
% 0.21/0.41 (a!8 (lambda ((U $i)) (refl (~ (not (big_q U)) (not (big_q U))))))
% 0.21/0.41 (a!9 (forall ((U $i)) (not (big_q U))))
% 0.21/0.41 (a!10 (lambda ((W $i)) (refl (~ (big_p W) (big_p W)))))
% 0.21/0.41 (a!11 (forall ((W $i)) (big_p W)))
% 0.21/0.41 (a!20 (exists ((X1 $i)) (forall ((Y1 $i)) (= (big_q X1) (big_q Y1)))))
% 0.21/0.41 (a!21 (forall ((Y1 $i)) (= (big_q X1!4) (big_q Y1))))
% 0.21/0.41 (a!22 (lambda ((Y1 $i))
% 0.21/0.41 (refl (~ (= (big_q X1!4) (big_q Y1)) (= (big_q X1!4) (big_q Y1))))))
% 0.21/0.41 (a!24 (lambda ((X1 $i))
% 0.21/0.41 (let ((a!1 (forall ((Y1 $i)) (= (big_q X1) (big_q Y1))))
% 0.21/0.41 (a!2 (not (= (big_q X1) (big_q (Y1!5 X1))))))
% 0.21/0.41 (sk (~ (not a!1) a!2)))))
% 0.21/0.41 (a!25 (forall ((X1 $i)) (not (= (big_q X1) (big_q (Y1!5 X1))))))
% 0.21/0.41 (a!26 (exists ((U1 $i)) (big_p U1)))
% 0.21/0.41 (a!27 (lambda ((U1 $i)) (refl (~ (not (big_p U1)) (not (big_p U1))))))
% 0.21/0.41 (a!28 (forall ((U1 $i)) (not (big_p U1))))
% 0.21/0.41 (a!29 (lambda ((W1 $i)) (refl (~ (big_q W1) (big_q W1)))))
% 0.21/0.41 (a!30 (forall ((W1 $i)) (big_q W1))))
% 0.21/0.41 (let ((a!4 (trans (sk (~ a!1 a!2))
% 0.21/0.41 (nnf-pos (proof-bind a!3) (~ a!2 a!2))
% 0.21/0.41 (~ a!1 a!2)))
% 0.21/0.41 (a!12 (sk (~ (not a!11) (not (big_p W!3)))))
% 0.21/0.41 (a!13 (and (or a!9 a!11) (or (big_q U!2) (not (big_p W!3)))))
% 0.21/0.41 (a!15 (and (or (big_q U!2) a!11) (or a!9 (not (big_p W!3)))))
% 0.21/0.41 (a!23 (trans (sk (~ a!20 a!21))
% 0.21/0.41 (nnf-pos (proof-bind a!22) (~ a!21 a!21))
% 0.21/0.41 (~ a!20 a!21)))
% 0.21/0.41 (a!31 (sk (~ (not a!30) (not (big_q W1!7)))))
% 0.21/0.41 (a!32 (and (or a!28 a!30) (or (big_p U1!6) (not (big_q W1!7)))))
% 0.21/0.41 (a!34 (and (or (big_p U1!6) a!30) (or a!28 (not (big_q W1!7)))))
% 0.21/0.41 (a!39 (not (= (= a!1 (= a!7 a!11)) (= a!20 (= a!26 a!30))))))
% 0.21/0.41 (let ((a!14 (nnf-pos (sk (~ a!7 (big_q U!2)))
% 0.21/0.41 (nnf-neg (proof-bind a!8) (~ (not a!7) a!9))
% 0.21/0.41 (nnf-pos (proof-bind a!10) (~ a!11 a!11))
% 0.21/0.41 a!12
% 0.21/0.41 (~ (= a!7 a!11) a!13)))
% 0.21/0.41 (a!16 (nnf-neg (sk (~ a!7 (big_q U!2)))
% 0.21/0.41 (nnf-neg (proof-bind a!8) (~ (not a!7) a!9))
% 0.21/0.41 (nnf-pos (proof-bind a!10) (~ a!11 a!11))
% 0.21/0.41 a!12
% 0.21/0.41 (~ (not (= a!7 a!11)) a!15)))
% 0.21/0.41 (a!18 (~ (not (= a!1 (= a!7 a!11))) (and (or a!2 a!13) (or a!6 a!15))))
% 0.21/0.41 (a!33 (nnf-pos (sk (~ a!26 (big_p U1!6)))
% 0.21/0.41 (nnf-neg (proof-bind a!27) (~ (not a!26) a!28))
% 0.21/0.41 (nnf-pos (proof-bind a!29) (~ a!30 a!30))
% 0.21/0.41 a!31
% 0.21/0.41 (~ (= a!26 a!30) a!32)))
% 0.21/0.41 (a!35 (nnf-neg (sk (~ a!26 (big_p U1!6)))
% 0.21/0.41 (nnf-neg (proof-bind a!27) (~ (not a!26) a!28))
% 0.21/0.41 (nnf-pos (proof-bind a!29) (~ a!30 a!30))
% 0.21/0.41 a!31
% 0.21/0.41 (~ (not (= a!26 a!30)) a!34)))
% 0.21/0.41 (a!37 (~ (not (= a!20 (= a!26 a!30))) (and (or a!21 a!32) (or a!25 a!34))))
% 0.21/0.41 (a!40 (and (or (and (or a!6 a!13) (or a!2 a!15))
% 0.21/0.41 (and (or a!25 a!32) (or a!21 a!34)))
% 0.21/0.41 (or (and (or a!2 a!13) (or a!6 a!15))
% 0.21/0.41 (and (or a!21 a!32) (or a!25 a!34))))))
% 0.21/0.41 (let ((a!17 (nnf-pos a!4
% 0.21/0.41 (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 0.21/0.41 a!14
% 0.21/0.41 a!16
% 0.21/0.41 (~ (= a!1 (= a!7 a!11)) (and (or a!6 a!13) (or a!2 a!15)))))
% 0.21/0.41 (a!19 (nnf-neg a!4
% 0.21/0.41 (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 0.21/0.41 a!14
% 0.21/0.41 a!16
% 0.21/0.41 a!18))
% 0.21/0.41 (a!36 (nnf-pos a!23
% 0.21/0.41 (nnf-neg (proof-bind a!24) (~ (not a!20) a!25))
% 0.21/0.41 a!33
% 0.21/0.41 a!35
% 0.21/0.41 (~ (= a!20 (= a!26 a!30))
% 0.21/0.41 (and (or a!25 a!32) (or a!21 a!34)))))
% 0.21/0.41 (a!38 (nnf-neg a!23
% 0.21/0.41 (nnf-neg (proof-bind a!24) (~ (not a!20) a!25))
% 0.21/0.41 a!33
% 0.21/0.41 a!35
% 0.21/0.41 a!37)))
% 0.21/0.41 (nnf-neg a!17 a!19 a!36 a!38 (~ a!39 a!40))))))
% 0.21/0.41 Proof display could not be completed: unexpected number of arguments
% 0.21/0.41 % E exiting
%------------------------------------------------------------------------------