%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN036+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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.19s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN036+1 : TPTP v9.0.0. Released v2.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n007.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:27:50 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.37 % SZS status Theorem
% 0.19/0.37 % SZS output start Proof
% 0.19/0.37 tff(big_q_type, type, (
% 0.19/0.37 big_q: $i > $o)).
% 0.19/0.37 tff(tptp_fun_Y1_5_type, type, (
% 0.19/0.37 tptp_fun_Y1_5: $i > $i)).
% 0.19/0.37 tff(tptp_fun_U_2_type, type, (
% 0.19/0.37 tptp_fun_U_2: $i)).
% 0.19/0.37 tff(tptp_fun_W_3_type, type, (
% 0.19/0.37 tptp_fun_W_3: $i)).
% 0.19/0.37 tff(big_p_type, type, (
% 0.19/0.37 big_p: $i > $o)).
% 0.19/0.37 tff(tptp_fun_Y_1_type, type, (
% 0.19/0.37 tptp_fun_Y_1: $i > $i)).
% 0.19/0.37 tff(elem_13_type, type, (
% 0.19/0.37 elem_13: $i)).
% 0.19/0.37 tff(tptp_fun_W1_7_type, type, (
% 0.19/0.37 tptp_fun_W1_7: $i)).
% 0.19/0.37 tff(tptp_fun_U1_6_type, type, (
% 0.19/0.37 tptp_fun_U1_6: $i)).
% 0.19/0.37 tff(tptp_fun_X_0_type, type, (
% 0.19/0.37 tptp_fun_X_0: $i)).
% 0.19/0.37 tff(tptp_fun_X1_4_type, type, (
% 0.19/0.37 tptp_fun_X1_4: $i)).
% 0.19/0.37 tff(1,assumption,(~big_q(W!3)), introduced(assumption)).
% 0.19/0.37 tff(2,assumption,(![W: $i] : big_q(W)), introduced(assumption)).
% 0.19/0.37 tff(3,plain,
% 0.19/0.37 ((~![W: $i] : big_q(W)) | big_q(W!3)),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(4,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[3, 1, 2])).
% 0.19/0.37 tff(5,plain,((~![W: $i] : big_q(W)) | big_q(W!3)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(6,plain,
% 0.19/0.37 (~![W: $i] : big_q(W)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[5, 1])).
% 0.19/0.37 tff(7,assumption,(~big_q(U!2)), introduced(assumption)).
% 0.19/0.37 tff(8,assumption,(![W1: $i] : big_p(W1)), introduced(assumption)).
% 0.19/0.37 tff(9,plain,
% 0.19/0.37 ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) | (~![W1: $i] : big_p(W1))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(10,plain,
% 0.19/0.37 (![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[9, 8])).
% 0.19/0.37 tff(11,assumption,(~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1)))))), introduced(assumption)).
% 0.19/0.37 tff(12,plain,
% 0.19/0.37 (((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))))) | ((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1)))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(13,plain,
% 0.19/0.37 ((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[12, 11])).
% 0.19/0.37 tff(14,assumption,(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)), introduced(assumption)).
% 0.19/0.37 tff(15,plain,
% 0.19/0.37 (((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))))) | (big_p(U1!6) | ![W1: $i] : big_p(W1))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(16,plain,
% 0.19/0.37 (big_p(U1!6) | ![W1: $i] : big_p(W1)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[15, 11])).
% 0.19/0.37 tff(17,assumption,(~![W1: $i] : big_p(W1)), introduced(assumption)).
% 0.19/0.37 tff(18,plain,
% 0.19/0.37 ((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))) | ![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(19,plain,
% 0.19/0.37 (![U1: $i] : (~big_p(U1))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[18, 17, 14])).
% 0.19/0.37 tff(20,assumption,(big_p(U1!6) | ![W1: $i] : big_p(W1)), introduced(assumption)).
% 0.19/0.37 tff(21,plain,
% 0.19/0.37 ((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | big_p(U1!6) | ![W1: $i] : big_p(W1)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(22,plain,
% 0.19/0.37 (big_p(U1!6)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[21, 17, 20])).
% 0.19/0.37 tff(23,plain,
% 0.19/0.37 ((~![U1: $i] : (~big_p(U1))) | (~big_p(U1!6))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(24,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[23, 22, 19])).
% 0.19/0.37 tff(25,plain,(![W1: $i] : big_p(W1) | (~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(26,plain,
% 0.19/0.37 (![W1: $i] : big_p(W1)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[25, 16, 14])).
% 0.19/0.37 tff(27,assumption,(~big_p(W1!7)), introduced(assumption)).
% 0.19/0.37 tff(28,plain,
% 0.19/0.37 ((~![W1: $i] : big_p(W1)) | big_p(W1!7)),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(29,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[28, 27, 8])).
% 0.19/0.37 tff(30,plain,(big_p(W1!7) | (~![W1: $i] : big_p(W1))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(31,plain,
% 0.19/0.37 (big_p(W1!7)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[30, 26])).
% 0.19/0.37 tff(32,plain,
% 0.19/0.37 ((~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1)))) | (~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(33,plain,
% 0.19/0.38 (![U1: $i] : (~big_p(U1))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[32, 31, 13])).
% 0.19/0.38 tff(34,plain,
% 0.19/0.38 ((~![U1: $i] : (~big_p(U1))) | (~big_p(W1!7))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(35,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[34, 31, 33])).
% 0.19/0.38 tff(36,plain,(((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(37,plain,
% 0.19/0.38 ((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[36, 10])).
% 0.19/0.38 tff(38,assumption,(~(big_p(elem!13) <=> big_p(tptp_fun_Y_1(elem!13)))), introduced(assumption)).
% 0.19/0.38 tff(39,plain,
% 0.19/0.38 ((~![W1: $i] : big_p(W1)) | big_p(elem!13)),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(40,plain,
% 0.19/0.38 (big_p(elem!13)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[39, 8])).
% 0.19/0.38 tff(41,plain,
% 0.19/0.38 ((~![W1: $i] : big_p(W1)) | big_p(tptp_fun_Y_1(elem!13))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(42,plain,
% 0.19/0.38 (big_p(tptp_fun_Y_1(elem!13))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[41, 8])).
% 0.19/0.38 tff(43,plain,
% 0.19/0.38 ((big_p(elem!13) <=> big_p(tptp_fun_Y_1(elem!13))) | (~big_p(elem!13)) | (~big_p(tptp_fun_Y_1(elem!13)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(44,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[43, 42, 40, 38])).
% 0.19/0.38 tff(45,plain,((big_p(elem!13) <=> big_p(tptp_fun_Y_1(elem!13))) | (~![W1: $i] : big_p(W1))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(46,plain,
% 0.19/0.38 (big_p(elem!13) <=> big_p(tptp_fun_Y_1(elem!13))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[45, 8])).
% 0.19/0.38 tff(47,plain,
% 0.19/0.38 ((~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))) | (~(big_p(elem!13) <=> big_p(tptp_fun_Y_1(elem!13))))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(48,plain,
% 0.19/0.38 (~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[47, 46])).
% 0.19/0.38 tff(49,assumption,(~![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X))))), introduced(assumption)).
% 0.19/0.38 tff(50,assumption,((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1))))), introduced(assumption)).
% 0.19/0.38 tff(51,assumption,(~![U: $i] : (~big_q(U))), introduced(assumption)).
% 0.19/0.38 tff(52,assumption,(~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))), introduced(assumption)).
% 0.19/0.38 tff(53,plain,
% 0.19/0.38 (((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)))) | (big_q(U!2) | (~big_q(W!3)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(54,plain,
% 0.19/0.38 (big_q(U!2) | (~big_q(W!3))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[53, 52])).
% 0.19/0.38 tff(55,assumption,(big_q(U!2) | ![W: $i] : big_q(W)), introduced(assumption)).
% 0.19/0.38 tff(56,plain,
% 0.19/0.38 ((~(big_q(U!2) | ![W: $i] : big_q(W))) | big_q(U!2) | ![W: $i] : big_q(W)),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(57,plain,
% 0.19/0.38 (![W: $i] : big_q(W)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[56, 7, 55])).
% 0.19/0.38 tff(58,assumption,(big_q(U!2) | (~big_q(W!3))), introduced(assumption)).
% 0.19/0.38 tff(59,plain,
% 0.19/0.38 ((~(big_q(U!2) | (~big_q(W!3)))) | big_q(U!2) | (~big_q(W!3))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(60,plain,
% 0.19/0.38 (~big_q(W!3)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[59, 7, 58])).
% 0.19/0.38 tff(61,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[3, 60, 57])).
% 0.19/0.38 tff(62,plain,(big_q(U!2) | (~(big_q(U!2) | (~big_q(W!3)))) | (~(big_q(U!2) | ![W: $i] : big_q(W)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(63,plain,
% 0.19/0.38 (~(big_q(U!2) | ![W: $i] : big_q(W))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[62, 54, 7])).
% 0.19/0.38 tff(64,plain,
% 0.19/0.38 (((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)))) | (![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(65,plain,
% 0.19/0.38 (![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[64, 52])).
% 0.19/0.38 tff(66,plain,
% 0.19/0.38 ((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))) | ![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(67,plain,
% 0.19/0.38 (![W: $i] : big_q(W)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[66, 65, 51])).
% 0.19/0.38 tff(68,plain,
% 0.19/0.38 ((big_q(U!2) | ![W: $i] : big_q(W)) | (~![W: $i] : big_q(W))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(69,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[68, 67, 63])).
% 0.19/0.38 tff(70,plain,(((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)))) | ![U: $i] : (~big_q(U)) | big_q(U!2)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(71,plain,
% 0.19/0.38 ((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[70, 51, 7])).
% 0.19/0.38 tff(72,plain,
% 0.19/0.38 ((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))) | ![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)))))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(73,plain,
% 0.19/0.38 (~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[72, 71, 49])).
% 0.19/0.38 tff(74,plain,
% 0.19/0.38 (((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~((~big_q(W!3)) | ![U: $i] : (~big_q(U))))))))) | (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(75,plain,
% 0.19/0.38 ((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~((~big_q(W!3)) | ![U: $i] : (~big_q(U))))))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.19/0.38 tff(76,plain,
% 0.19/0.38 (((~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))) | (~(big_q(U!2) | (~big_q(W!3)))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~(![U: $i] : (~big_q(U)) | (~big_q(W!3)))))))))) | (~((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))) | (~(big_p(U1!6) | (~big_p(W1!7)))))))) | (~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))))))) <=> ((~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_q(U!2) | (~big_q(W!3)))) | (~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~((~big_q(W!3)) | ![U: $i] : (~big_q(U)))))))))) | (~((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(big_p(U1!6) | (~big_p(W1!7)))) | (~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))))))) | (~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~((~big_p(W1!7)) | ![U1: $i] : (~big_p(U1)))))))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(77,plain,
% 0.19/0.38 (((~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))) | (~(big_q(U!2) | (~big_q(W!3)))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~(![U: $i] : (~big_q(U)) | (~big_q(W!3)))))))))) | (~((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))) | (~(big_p(U1!6) | (~big_p(W1!7)))))))) | (~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))))))) <=> ((~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))) | (~(big_q(U!2) | (~big_q(W!3)))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~(![U: $i] : (~big_q(U)) | (~big_q(W!3)))))))))) | (~((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))) | (~(big_p(U1!6) | (~big_p(W1!7)))))))) | (~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(78,plain,
% 0.19/0.38 ((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))) <=> ((~((~(![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W))) | (~(big_q(U!2) | (~big_q(W!3)))))))) | (~(![Y: $i] : (big_p(X!0) <=> big_p(Y)) | (~((~(big_q(U!2) | ![W: $i] : big_q(W))) | (~(![U: $i] : (~big_q(U)) | (~big_q(W!3)))))))))) | (~((~(![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | (~((~(![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1))) | (~(big_p(U1!6) | (~big_p(W1!7)))))))) | (~(![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | (~((~(big_p(U1!6) | ![W1: $i] : big_p(W1))) | (~(![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(79,plain,
% 0.19/0.38 (((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))) <=> ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(80,plain,
% 0.19/0.38 (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) <=> ((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(81,plain,
% 0.19/0.38 ((((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))) <=> (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[80, 79])).
% 0.19/0.39 tff(82,plain,
% 0.19/0.39 (((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))) <=> ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(83,plain,
% 0.19/0.39 (((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) <=> ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(84,plain,
% 0.19/0.39 ((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))) <=> (((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[83, 82])).
% 0.19/0.39 tff(85,plain,
% 0.19/0.39 (((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))) & (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7)))))))) <=> ((((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))) & (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![U: $i] : (~big_q(U)) | ![W: $i] : big_q(W)) & (big_q(U!2) | (~big_q(W!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_q(U!2) | ![W: $i] : big_q(W)) & (![U: $i] : (~big_q(U)) | (~big_q(W!3)))))) | ((![Y1: $i] : (big_q(X1!4) <=> big_q(Y1)) | ((![U1: $i] : (~big_p(U1)) | ![W1: $i] : big_p(W1)) & (big_p(U1!6) | (~big_p(W1!7))))) & (![X1: $i] : (~(big_q(X1) <=> big_q(tptp_fun_Y1_5(X1)))) | ((big_p(U1!6) | ![W1: $i] : big_p(W1)) & (![U1: $i] : (~big_p(U1)) | (~big_p(W1!7))))))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[84, 81])).
% 0.19/0.39 tff(86,plain,
% 0.19/0.39 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(87,plain,
% 0.19/0.39 ((?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(88,plain,
% 0.19/0.39 ((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(89,plain,
% 0.19/0.39 (((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1)))) <=> ((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[88, 87])).
% 0.19/0.39 tff(90,plain,
% 0.19/0.39 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1)))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[89])).
% 0.19/0.39 tff(91,plain,
% 0.19/0.39 ((~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))) <=> (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1)))))),
% 0.19/0.39 inference(transitivity,[status(thm)],[90, 86])).
% 0.19/0.39 tff(92,axiom,(~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pel34')).
% 0.19/0.39 tff(93,plain,
% 0.19/0.39 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.19/0.39 tff(94,plain,
% 0.19/0.39 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[93, 91])).
% 0.19/0.39 tff(95,plain,
% 0.19/0.40 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[94, 86])).
% 0.19/0.40 tff(96,plain,
% 0.19/0.40 (~((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[U: $i] : big_q(U) <=> ![W: $i] : big_q(W))) <=> (?[X1: $i] : ![Y1: $i] : (big_q(X1) <=> big_q(Y1)) <=> (?[U1: $i] : big_p(U1) <=> ![W1: $i] : big_p(W1))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[95, 91])).
% 0.19/0.40 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (forall ((Y $i)) (= (big_p X) (big_p Y)))))
% 0.19/0.40 (a!2 (forall ((Y $i)) (= (big_p X!0) (big_p Y))))
% 0.19/0.40 (a!3 (lambda ((Y $i))
% 0.19/0.40 (refl (~ (= (big_p X!0) (big_p Y)) (= (big_p X!0) (big_p Y))))))
% 0.19/0.40 (a!5 (lambda ((X $i))
% 0.19/0.40 (let ((a!1 (forall ((Y $i)) (= (big_p X) (big_p Y))))
% 0.19/0.40 (a!2 (not (= (big_p X) (big_p (Y!1 X))))))
% 0.19/0.40 (sk (~ (not a!1) a!2)))))
% 0.19/0.40 (a!6 (forall ((X $i)) (not (= (big_p X) (big_p (Y!1 X))))))
% 0.19/0.40 (a!7 (exists ((U $i)) (big_q U)))
% 0.19/0.40 (a!8 (lambda ((U $i)) (refl (~ (not (big_q U)) (not (big_q U))))))
% 0.19/0.40 (a!9 (forall ((U $i)) (not (big_q U))))
% 0.19/0.40 (a!10 (lambda ((W $i)) (refl (~ (big_q W) (big_q W)))))
% 0.19/0.40 (a!11 (forall ((W $i)) (big_q W)))
% 0.19/0.40 (a!20 (exists ((X1 $i)) (forall ((Y1 $i)) (= (big_q X1) (big_q Y1)))))
% 0.19/0.40 (a!21 (forall ((Y1 $i)) (= (big_q X1!4) (big_q Y1))))
% 0.19/0.40 (a!22 (lambda ((Y1 $i))
% 0.19/0.40 (refl (~ (= (big_q X1!4) (big_q Y1)) (= (big_q X1!4) (big_q Y1))))))
% 0.19/0.40 (a!24 (lambda ((X1 $i))
% 0.19/0.40 (let ((a!1 (forall ((Y1 $i)) (= (big_q X1) (big_q Y1))))
% 0.19/0.40 (a!2 (not (= (big_q X1) (big_q (Y1!5 X1))))))
% 0.19/0.40 (sk (~ (not a!1) a!2)))))
% 0.19/0.40 (a!25 (forall ((X1 $i)) (not (= (big_q X1) (big_q (Y1!5 X1))))))
% 0.19/0.40 (a!26 (exists ((U1 $i)) (big_p U1)))
% 0.19/0.40 (a!27 (lambda ((U1 $i)) (refl (~ (not (big_p U1)) (not (big_p U1))))))
% 0.19/0.40 (a!28 (forall ((U1 $i)) (not (big_p U1))))
% 0.19/0.40 (a!29 (lambda ((W1 $i)) (refl (~ (big_p W1) (big_p W1)))))
% 0.19/0.40 (a!30 (forall ((W1 $i)) (big_p W1))))
% 0.19/0.40 (let ((a!4 (trans (sk (~ a!1 a!2))
% 0.19/0.40 (nnf-pos (proof-bind a!3) (~ a!2 a!2))
% 0.19/0.40 (~ a!1 a!2)))
% 0.19/0.40 (a!12 (sk (~ (not a!11) (not (big_q W!3)))))
% 0.19/0.40 (a!13 (and (or a!9 a!11) (or (big_q U!2) (not (big_q W!3)))))
% 0.19/0.40 (a!15 (and (or (big_q U!2) a!11) (or a!9 (not (big_q W!3)))))
% 0.19/0.40 (a!23 (trans (sk (~ a!20 a!21))
% 0.19/0.40 (nnf-pos (proof-bind a!22) (~ a!21 a!21))
% 0.19/0.40 (~ a!20 a!21)))
% 0.19/0.40 (a!31 (sk (~ (not a!30) (not (big_p W1!7)))))
% 0.19/0.40 (a!32 (and (or a!28 a!30) (or (big_p U1!6) (not (big_p W1!7)))))
% 0.19/0.40 (a!34 (and (or (big_p U1!6) a!30) (or a!28 (not (big_p W1!7)))))
% 0.19/0.40 (a!39 (not (= (= a!1 (= a!7 a!11)) (= a!20 (= a!26 a!30))))))
% 0.19/0.40 (let ((a!14 (nnf-pos (sk (~ a!7 (big_q U!2)))
% 0.19/0.40 (nnf-neg (proof-bind a!8) (~ (not a!7) a!9))
% 0.19/0.40 (nnf-pos (proof-bind a!10) (~ a!11 a!11))
% 0.19/0.40 a!12
% 0.19/0.40 (~ (= a!7 a!11) a!13)))
% 0.19/0.40 (a!16 (nnf-neg (sk (~ a!7 (big_q U!2)))
% 0.19/0.40 (nnf-neg (proof-bind a!8) (~ (not a!7) a!9))
% 0.19/0.40 (nnf-pos (proof-bind a!10) (~ a!11 a!11))
% 0.19/0.40 a!12
% 0.19/0.40 (~ (not (= a!7 a!11)) a!15)))
% 0.19/0.40 (a!18 (~ (not (= a!1 (= a!7 a!11))) (and (or a!2 a!13) (or a!6 a!15))))
% 0.19/0.40 (a!33 (nnf-pos (sk (~ a!26 (big_p U1!6)))
% 0.19/0.40 (nnf-neg (proof-bind a!27) (~ (not a!26) a!28))
% 0.19/0.40 (nnf-pos (proof-bind a!29) (~ a!30 a!30))
% 0.19/0.40 a!31
% 0.19/0.40 (~ (= a!26 a!30) a!32)))
% 0.19/0.40 (a!35 (nnf-neg (sk (~ a!26 (big_p U1!6)))
% 0.19/0.40 (nnf-neg (proof-bind a!27) (~ (not a!26) a!28))
% 0.19/0.40 (nnf-pos (proof-bind a!29) (~ a!30 a!30))
% 0.19/0.40 a!31
% 0.19/0.40 (~ (not (= a!26 a!30)) a!34)))
% 0.19/0.40 (a!37 (~ (not (= a!20 (= a!26 a!30))) (and (or a!21 a!32) (or a!25 a!34))))
% 0.19/0.40 (a!40 (and (or (and (or a!6 a!13) (or a!2 a!15))
% 0.19/0.40 (and (or a!25 a!32) (or a!21 a!34)))
% 0.19/0.40 (or (and (or a!2 a!13) (or a!6 a!15))
% 0.19/0.40 (and (or a!21 a!32) (or a!25 a!34))))))
% 0.19/0.40 (let ((a!17 (nnf-pos a!4
% 0.19/0.40 (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 0.19/0.40 a!14
% 0.19/0.40 a!16
% 0.19/0.40 (~ (= a!1 (= a!7 a!11)) (and (or a!6 a!13) (or a!2 a!15)))))
% 0.19/0.40 (a!19 (nnf-neg a!4
% 0.19/0.40 (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 0.19/0.40 a!14
% 0.19/0.40 a!16
% 0.19/0.40 a!18))
% 0.19/0.40 (a!36 (nnf-pos a!23
% 0.19/0.40 (nnf-neg (proof-bind a!24) (~ (not a!20) a!25))
% 0.19/0.40 a!33
% 0.19/0.40 a!35
% 0.19/0.40 (~ (= a!20 (= a!26 a!30))
% 0.19/0.40 (and (or a!25 a!32) (or a!21 a!34)))))
% 0.19/0.40 (a!38 (nnf-neg a!23
% 0.19/0.40 (nnf-neg (proof-bind a!24) (~ (not a!20) a!25))
% 0.19/0.40 a!33
% 0.19/0.40 a!35
% 0.19/0.40 a!37)))
% 0.19/0.40 (nnf-neg a!17 a!19 a!36 a!38 (~ a!39 a!40))))))
% 0.19/0.40 Proof display could not be completed: unexpected number of arguments
% 0.19/0.41 % E exiting
%------------------------------------------------------------------------------