%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN415+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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:39:01 AM UTC 2025
% Result : Theorem 0.12s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN415+1 : TPTP v9.0.0. Released v2.0.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n015.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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 12:33:55 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.37 % SZS status Theorem
% 0.12/0.37 % SZS output start Proof
% 0.12/0.37 tff(f_type, type, (
% 0.12/0.37 f: $i > $o)).
% 0.12/0.37 tff(tptp_fun_V_4_type, type, (
% 0.12/0.37 tptp_fun_V_4: $i > $i)).
% 0.12/0.37 tff(tptp_fun_U_3_type, type, (
% 0.12/0.37 tptp_fun_U_3: $i)).
% 0.12/0.37 tff(tptp_fun_X_0_type, type, (
% 0.12/0.37 tptp_fun_X_0: $i)).
% 0.12/0.37 tff(tptp_fun_Z_1_type, type, (
% 0.12/0.37 tptp_fun_Z_1: $i)).
% 0.12/0.37 tff(tptp_fun_Y_2_type, type, (
% 0.12/0.37 tptp_fun_Y_2: $i)).
% 0.12/0.37 tff(1,assumption,(~((~f(tptp_fun_V_4(U!3))) | (U!3 = tptp_fun_V_4(U!3)))), introduced(assumption)).
% 0.12/0.37 tff(2,plain,
% 0.12/0.37 (((~f(tptp_fun_V_4(U!3))) | (U!3 = tptp_fun_V_4(U!3))) | (~(U!3 = tptp_fun_V_4(U!3)))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(3,plain,
% 0.12/0.37 (~(U!3 = tptp_fun_V_4(U!3))),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.12/0.37 tff(4,plain,
% 0.12/0.37 (((~f(tptp_fun_V_4(U!3))) | (U!3 = tptp_fun_V_4(U!3))) | f(tptp_fun_V_4(U!3))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(5,plain,
% 0.12/0.37 (f(tptp_fun_V_4(U!3))),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.12/0.37 tff(6,assumption,(~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))), introduced(assumption)).
% 0.12/0.37 tff(7,plain,
% 0.12/0.37 (((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y))))) | f(X!0)),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(8,plain,
% 0.12/0.37 (f(X!0)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.12/0.37 tff(9,assumption,(![X: $i] : (~f(X))), introduced(assumption)).
% 0.12/0.37 tff(10,assumption,(f(X!0)), introduced(assumption)).
% 0.12/0.37 tff(11,plain,
% 0.12/0.37 ((~![X: $i] : (~f(X))) | (~f(X!0))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(12,plain,
% 0.12/0.37 ($false),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[11, 10, 9])).
% 0.12/0.37 tff(13,plain,((~![X: $i] : (~f(X))) | (~f(X!0))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.37 tff(14,plain,
% 0.12/0.37 (~![X: $i] : (~f(X))),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[13, 8])).
% 0.12/0.37 tff(15,assumption,(~((Y!2 = Z!1) | (~f(Y!2)) | (~f(Z!1)))), introduced(assumption)).
% 0.12/0.37 tff(16,plain,
% 0.12/0.37 (((Y!2 = Z!1) | (~f(Y!2)) | (~f(Z!1))) | f(Z!1)),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(17,plain,
% 0.12/0.37 (f(Z!1)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.12/0.37 tff(18,plain,
% 0.12/0.37 (((Y!2 = Z!1) | (~f(Y!2)) | (~f(Z!1))) | f(Y!2)),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(19,plain,
% 0.12/0.37 (f(Y!2)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[18, 15])).
% 0.12/0.37 tff(20,plain,
% 0.12/0.37 (((Y!2 = Z!1) | (~f(Y!2)) | (~f(Z!1))) | (~(Y!2 = Z!1))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(21,plain,
% 0.12/0.37 (~(Y!2 = Z!1)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[20, 15])).
% 0.12/0.37 tff(22,assumption,(f(Z!1)), introduced(assumption)).
% 0.12/0.37 tff(23,assumption,(![V: $i] : ((~f(V)) | (U!3 = V))), introduced(assumption)).
% 0.12/0.37 tff(24,plain,
% 0.12/0.37 (((~![V: $i] : ((~f(V)) | (U!3 = V))) | ((~f(Z!1)) | (U!3 = Z!1))) <=> ((~![V: $i] : ((~f(V)) | (U!3 = V))) | (~f(Z!1)) | (U!3 = Z!1))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(25,plain,
% 0.12/0.37 ((~![V: $i] : ((~f(V)) | (U!3 = V))) | ((~f(Z!1)) | (U!3 = Z!1))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(26,plain,
% 0.12/0.37 ((~![V: $i] : ((~f(V)) | (U!3 = V))) | (~f(Z!1)) | (U!3 = Z!1)),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.12/0.37 tff(27,plain,
% 0.12/0.37 (U!3 = Z!1),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[26, 23, 22])).
% 0.12/0.37 tff(28,assumption,(f(Y!2)), introduced(assumption)).
% 0.12/0.37 tff(29,plain,
% 0.12/0.37 (((~![V: $i] : ((~f(V)) | (U!3 = V))) | ((~f(Y!2)) | (U!3 = Y!2))) <=> ((~![V: $i] : ((~f(V)) | (U!3 = V))) | (~f(Y!2)) | (U!3 = Y!2))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(30,plain,
% 0.12/0.37 ((~![V: $i] : ((~f(V)) | (U!3 = V))) | ((~f(Y!2)) | (U!3 = Y!2))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(31,plain,
% 0.12/0.37 ((~![V: $i] : ((~f(V)) | (U!3 = V))) | (~f(Y!2)) | (U!3 = Y!2)),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.12/0.37 tff(32,plain,
% 0.12/0.37 (U!3 = Y!2),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[31, 23, 28])).
% 0.12/0.37 tff(33,plain,
% 0.12/0.37 (Y!2 = U!3),
% 0.12/0.37 inference(symmetry,[status(thm)],[32])).
% 0.12/0.37 tff(34,plain,
% 0.12/0.37 (Y!2 = Z!1),
% 0.12/0.37 inference(transitivity,[status(thm)],[33, 27])).
% 0.12/0.37 tff(35,assumption,(~(Y!2 = Z!1)), introduced(assumption)).
% 0.12/0.37 tff(36,plain,
% 0.12/0.37 ($false),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[35, 34])).
% 0.12/0.37 tff(37,plain,((~![V: $i] : ((~f(V)) | (U!3 = V))) | (Y!2 = Z!1) | (~f(Z!1)) | (~f(Y!2))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.38 tff(38,plain,
% 0.12/0.38 (~![V: $i] : ((~f(V)) | (U!3 = V))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[37, 21, 17, 19])).
% 0.12/0.38 tff(39,plain,
% 0.12/0.38 (((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V)))) | ![V: $i] : ((~f(V)) | (U!3 = V))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(40,plain,
% 0.12/0.38 ((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V)))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.12/0.38 tff(41,plain,
% 0.12/0.38 (((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V)))))) <=> ((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(42,plain,
% 0.12/0.38 (((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V)))))) <=> ((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(43,plain,
% 0.12/0.38 ((f(U!3) & ![V: $i] : ((~f(V)) | (U!3 = V))) <=> (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V)))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(44,plain,
% 0.12/0.38 ((f(X!0) & ![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))) <=> (~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(45,plain,
% 0.12/0.38 (^[Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((f(Y) & f(Z)) <=> (~((~f(Z)) | (~f(Y))))), ((~(f(Y) & f(Z))) <=> (~(~((~f(Z)) | (~f(Y))))))), rewrite((~(~((~f(Z)) | (~f(Y))))) <=> ((~f(Z)) | (~f(Y)))), ((~(f(Y) & f(Z))) <=> ((~f(Z)) | (~f(Y))))), (((~(f(Y) & f(Z))) | (Y = Z)) <=> (((~f(Z)) | (~f(Y))) | (Y = Z)))), rewrite((((~f(Z)) | (~f(Y))) | (Y = Z)) <=> ((Y = Z) | (~f(Z)) | (~f(Y)))), (((~(f(Y) & f(Z))) | (Y = Z)) <=> ((Y = Z) | (~f(Z)) | (~f(Y)))))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(46,plain,
% 0.12/0.38 (![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z)) <=> ![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[45])).
% 0.12/0.38 tff(47,plain,
% 0.12/0.38 ((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> (f(X!0) & ![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y))))),
% 0.12/0.38 inference(monotonicity,[status(thm)],[46])).
% 0.12/0.38 tff(48,plain,
% 0.12/0.38 ((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> (~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y))))))),
% 0.12/0.38 inference(transitivity,[status(thm)],[47, 44])).
% 0.12/0.38 tff(49,plain,
% 0.12/0.38 (((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) | (f(U!3) & ![V: $i] : ((~f(V)) | (U!3 = V)))) <=> ((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V))))))),
% 0.12/0.38 inference(monotonicity,[status(thm)],[48, 43])).
% 0.12/0.38 tff(50,plain,
% 0.12/0.38 (((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) | (f(U!3) & ![V: $i] : ((~f(V)) | (U!3 = V)))) <=> ((~((~f(X!0)) | (~![Y: $i, Z: $i] : ((Y = Z) | (~f(Z)) | (~f(Y)))))) | (~((~f(U!3)) | (~![V: $i] : ((~f(V)) | (U!3 = V))))))),
% 0.12/0.38 inference(transitivity,[status(thm)],[49, 42])).
% 0.12/0.38 tff(51,plain,
% 0.12/0.38 ((((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) | (f(U!3) & ![V: $i] : ((~f(V)) | (U!3 = V)))) & ((![X: $i] : (~f(X)) | (~((~(f(Y!2) & f(Z!1))) | (Y!2 = Z!1)))) | ![U: $i] : ((~f(U)) | (~((~f(tptp_fun_V_4(U))) | (U = tptp_fun_V_4(U))))))) <=> (((f(X!0) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) | (f(U!3) & ![V: $i] : ((~f(V)) | (U!3 = V)))) & (![X: $i] : (~f(X)) | (~((~(f(Y!2) & f(Z!1))) | (Y!2 = Z!1))) | ![U: $i] : ((~f(U)) | (~((~f(tptp_fun_V_4(U))) | (U = tptp_fun_V_4(U)))))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(52,plain,
% 0.12/0.38 ((~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))) <=> (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(53,plain,
% 0.12/0.38 (((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))) <=> ((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(54,plain,
% 0.12/0.39 ((~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))) <=> (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[53])).
% 0.12/0.39 tff(55,plain,
% 0.12/0.39 ((~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))) <=> (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))))),
% 0.12/0.39 inference(transitivity,[status(thm)],[54, 52])).
% 0.12/0.39 tff(56,plain,
% 0.12/0.39 (((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((f(Y) & f(Z)) => (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : (f(V) => (U = V)))) <=> ((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(57,plain,
% 0.12/0.39 ((~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((f(Y) & f(Z)) => (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : (f(V) => (U = V))))) <=> (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))))),
% 0.12/0.39 inference(monotonicity,[status(thm)],[56])).
% 0.12/0.39 tff(58,plain,
% 0.12/0.39 ((~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((f(Y) & f(Z)) => (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : (f(V) => (U = V))))) <=> (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V)))))),
% 0.12/0.39 inference(transitivity,[status(thm)],[57, 52])).
% 0.12/0.39 tff(59,axiom,(~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((f(Y) & f(Z)) => (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : (f(V) => (U = V))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','kalish317')).
% 0.12/0.39 tff(60,plain,
% 0.12/0.39 (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[59, 58])).
% 0.12/0.39 tff(61,plain,
% 0.12/0.39 (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[60, 55])).
% 0.12/0.39 tff(62,plain,
% 0.12/0.39 (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[61, 52])).
% 0.12/0.39 tff(63,plain,
% 0.12/0.39 (~((?[X: $i] : f(X) & ![Y: $i, Z: $i] : ((~(f(Y) & f(Z))) | (Y = Z))) <=> ?[U: $i] : (f(U) & ![V: $i] : ((~f(V)) | (U = V))))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[62, 55])).
% 0.12/0.39 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (f X)))
% 0.12/0.39 (a!2 (proof-bind (lambda ((Y $i) (Z $i))
% 0.12/0.39 (let ((a!1 (or (not (and (f Y) (f Z))) (= Y Z))))
% 0.12/0.39 (refl (~ a!1 a!1))))))
% 0.12/0.39 (a!3 (forall ((Y $i) (Z $i)) (or (not (and (f Y) (f Z))) (= Y Z))))
% 0.12/0.39 (a!5 (lambda ((X $i)) (refl (~ (not (f X)) (not (f X))))))
% 0.12/0.39 (a!6 (forall ((X $i)) (not (f X))))
% 0.12/0.39 (a!7 (or (not (and (f Y!2) (f Z!1))) (= Y!2 Z!1)))
% 0.12/0.39 (a!9 (exists ((U $i))
% 0.12/0.39 (let ((a!1 (forall ((V $i)) (or (not (f V)) (= U V)))))
% 0.12/0.39 (and (f U) a!1))))
% 0.12/0.39 (a!10 (forall ((V $i)) (or (not (f V)) (= U!3 V))))
% 0.12/0.39 (a!15 (lambda ((U $i))
% 0.12/0.39 (let ((a!1 (refl (~ (not (f U)) (not (f U)))))
% 0.12/0.39 (a!2 (forall ((V $i)) (or (not (f V)) (= U V))))
% 0.12/0.39 (a!3 (or (not (f (V!4 U))) (= U (V!4 U)))))
% 0.12/0.39 (let ((a!4 (~ (not (and (f U) a!2)) (or (not (f U)) (not a!3)))))
% 0.12/0.39 (nnf-neg a!1 (sk (~ (not a!2) (not a!3))) a!4)))))
% 0.12/0.39 (a!16 (forall ((U $i))
% 0.12/0.39 (let ((a!1 (or (not (f (V!4 U))) (= U (V!4 U)))))
% 0.12/0.39 (or (not (f U)) (not a!1))))))
% 0.12/0.39 (let ((a!4 (monotonicity (sk (~ a!1 (f X!0)))
% 0.12/0.39 (nnf-pos a!2 (~ a!3 a!3))
% 0.12/0.39 (~ (and a!1 a!3) (and (f X!0) a!3))))
% 0.12/0.39 (a!8 (nnf-neg (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 0.12/0.39 (sk (~ (not a!3) (not a!7)))
% 0.12/0.39 (~ (not (and a!1 a!3)) (or a!6 (not a!7)))))
% 0.12/0.39 (a!11 (sk (~ a!9 (and (f U!3) a!10))))
% 0.12/0.39 (a!12 (nnf-pos (proof-bind (lambda ((V $i))
% 0.12/0.39 (let ((a!1 (~ (or (not (f V)) (= U!3 V))
% 0.12/0.39 (or (not (f V)) (= U!3 V)))))
% 0.12/0.39 (refl a!1))))
% 0.12/0.39 (~ a!10 a!10)))
% 0.12/0.39 (a!17 (and (or (and (f X!0) a!3) (and (f U!3) a!10))
% 0.12/0.39 (or (or a!6 (not a!7)) a!16))))
% 0.12/0.39 (let ((a!13 (monotonicity (refl (~ (f U!3) (f U!3)))
% 0.12/0.39 a!12
% 0.12/0.39 (~ (and (f U!3) a!10) (and (f U!3) a!10))))
% 0.12/0.39 (a!18 (~ (not (= (and a!1 a!3) a!9)) a!17)))
% 0.12/0.39 (let ((a!14 (trans a!11 a!13 (~ a!9 (and (f U!3) a!10)))))
% 0.12/0.39 (nnf-neg a!4 a!8 a!14 (nnf-neg (proof-bind a!15) (~ (not a!9) a!16)) a!18)))))
% 0.12/0.39 Proof display could not be completed: unexpected number of arguments
% 0.12/0.39 % E exiting
%------------------------------------------------------------------------------