%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV039+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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:31:23 AM UTC 2025
% Result : Theorem 258.95s 259.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV039+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n009.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 09:23:33 EDT 2025
% 0.11/0.33 % CPUTime :
% 258.95/259.26 % SZS status Theorem
% 258.95/259.26 % SZS output start Proof
% 258.95/259.26 tff(gt_type, type, (
% 258.95/259.26 gt: ( $i * $i ) > $o)).
% 258.95/259.26 tff(n1_type, type, (
% 258.95/259.26 n1: $i)).
% 258.95/259.26 tff(loopcounter_type, type, (
% 258.95/259.26 loopcounter: $i)).
% 258.95/259.26 tff(init_type, type, (
% 258.95/259.26 init: $i)).
% 258.95/259.26 tff(pvar1402_init_type, type, (
% 258.95/259.26 pvar1402_init: $i)).
% 258.95/259.26 tff(pvar1401_init_type, type, (
% 258.95/259.26 pvar1401_init: $i)).
% 258.95/259.26 tff(pvar1400_init_type, type, (
% 258.95/259.26 pvar1400_init: $i)).
% 258.95/259.26 tff(leq_type, type, (
% 258.95/259.26 leq: ( $i * $i ) > $o)).
% 258.95/259.26 tff(n2_type, type, (
% 258.95/259.26 n2: $i)).
% 258.95/259.26 tff(tptp_fun_E_13_type, type, (
% 258.95/259.26 tptp_fun_E_13: $i)).
% 258.95/259.26 tff(n0_type, type, (
% 258.95/259.26 n0: $i)).
% 258.95/259.26 tff(n3_type, type, (
% 258.95/259.26 n3: $i)).
% 258.95/259.26 tff(tptp_fun_F_14_type, type, (
% 258.95/259.26 tptp_fun_F_14: $i)).
% 258.95/259.26 tff(a_select3_type, type, (
% 258.95/259.26 a_select3: ( $i * $i * $i ) > $i)).
% 258.95/259.26 tff(simplex7_init_type, type, (
% 258.95/259.26 simplex7_init: $i)).
% 258.95/259.26 tff(a_select2_type, type, (
% 258.95/259.26 a_select2: ( $i * $i ) > $i)).
% 258.95/259.26 tff(s_center7_init_type, type, (
% 258.95/259.26 s_center7_init: $i)).
% 258.95/259.26 tff(s_values7_init_type, type, (
% 258.95/259.26 s_values7_init: $i)).
% 258.95/259.26 tff(s_worst7_type, type, (
% 258.95/259.26 s_worst7: $i)).
% 258.95/259.26 tff(s_sworst7_type, type, (
% 258.95/259.26 s_sworst7: $i)).
% 258.95/259.26 tff(s_best7_type, type, (
% 258.95/259.26 s_best7: $i)).
% 258.95/259.26 tff(s_worst7_init_type, type, (
% 258.95/259.26 s_worst7_init: $i)).
% 258.95/259.26 tff(s_sworst7_init_type, type, (
% 258.95/259.26 s_sworst7_init: $i)).
% 258.95/259.26 tff(s_best7_init_type, type, (
% 258.95/259.26 s_best7_init: $i)).
% 258.95/259.26 tff(s_try7_init_type, type, (
% 258.95/259.26 s_try7_init: $i)).
% 258.95/259.26 tff(minus_type, type, (
% 258.95/259.26 minus: ( $i * $i ) > $i)).
% 258.95/259.26 tff(tptp_fun_I_17_type, type, (
% 258.95/259.26 tptp_fun_I_17: $i)).
% 258.95/259.26 tff(tptp_minus_1_type, type, (
% 258.95/259.26 tptp_minus_1: $i)).
% 258.95/259.26 tff(pred_type, type, (
% 258.95/259.26 pred: $i > $i)).
% 258.95/259.26 tff(succ_type, type, (
% 258.95/259.26 succ: $i > $i)).
% 258.95/259.26 tff(tptp_fun_G_15_type, type, (
% 258.95/259.26 tptp_fun_G_15: $i)).
% 258.95/259.26 tff(tptp_fun_H_16_type, type, (
% 258.95/259.26 tptp_fun_H_16: $i)).
% 258.95/259.26 tff(1,assumption,(~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2)))), introduced(assumption)).
% 258.95/259.26 tff(2,plain,
% 258.95/259.26 (((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))) | leq(E!13, n2)),
% 258.95/259.26 inference(tautology,[status(thm)],[])).
% 258.95/259.26 tff(3,plain,
% 258.95/259.26 (leq(E!13, n2)),
% 258.95/259.26 inference(unit_resolution,[status(thm)],[2, 1])).
% 258.95/259.26 tff(4,plain,
% 258.95/259.26 (((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))) | leq(n0, E!13)),
% 258.95/259.26 inference(tautology,[status(thm)],[])).
% 258.95/259.26 tff(5,plain,
% 258.95/259.26 (leq(n0, E!13)),
% 258.95/259.26 inference(unit_resolution,[status(thm)],[4, 1])).
% 258.95/259.26 tff(6,plain,
% 258.95/259.26 (^[A: $i] : refl(((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))))),
% 258.95/259.26 inference(bind,[status(th)],[])).
% 258.95/259.26 tff(7,plain,
% 258.95/259.26 (![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.26 inference(quant_intro,[status(thm)],[6])).
% 258.95/259.26 tff(8,plain,
% 258.95/259.26 (^[A: $i] : rewrite(((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))))),
% 258.95/259.26 inference(bind,[status(th)],[])).
% 258.95/259.26 tff(9,plain,
% 258.95/259.26 (![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.26 inference(quant_intro,[status(thm)],[8])).
% 258.95/259.26 tff(10,plain,
% 258.95/259.26 (![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.26 inference(transitivity,[status(thm)],[9, 7])).
% 258.95/259.26 tff(11,plain,
% 258.95/259.26 (^[A: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, A) & leq(A, n2)) <=> (~((~leq(n0, A)) | (~leq(A, n2))))), ((~(leq(n0, A) & leq(A, n2))) <=> (~(~((~leq(n0, A)) | (~leq(A, n2))))))), rewrite((~(~((~leq(n0, A)) | (~leq(A, n2))))) <=> ((~leq(n0, A)) | (~leq(A, n2)))), ((~(leq(n0, A) & leq(A, n2))) <=> ((~leq(n0, A)) | (~leq(A, n2))))), quant_intro(proof_bind(^[B: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, B) & leq(B, n3)) <=> (~((~leq(n0, B)) | (~leq(B, n3))))), ((~(leq(n0, B) & leq(B, n3))) <=> (~(~((~leq(n0, B)) | (~leq(B, n3))))))), rewrite((~(~((~leq(n0, B)) | (~leq(B, n3))))) <=> ((~leq(n0, B)) | (~leq(B, n3)))), ((~(leq(n0, B) & leq(B, n3))) <=> ((~leq(n0, B)) | (~leq(B, n3))))), (((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)) <=> (((~leq(n0, B)) | (~leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)))), rewrite((((~leq(n0, B)) | (~leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)) <=> ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))), (((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)) <=> ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))))), (![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)) <=> ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))), (((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) <=> (((~leq(n0, A)) | (~leq(A, n2))) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))))), rewrite((((~leq(n0, A)) | (~leq(A, n2))) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3)))) <=> ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))), (((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) <=> ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))))),
% 258.95/259.26 inference(bind,[status(th)],[])).
% 258.95/259.26 tff(12,plain,
% 258.95/259.26 (![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) <=> ![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.26 inference(quant_intro,[status(thm)],[11])).
% 258.95/259.26 tff(13,plain,
% 258.95/259.26 (![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) <=> ![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)))),
% 258.95/259.26 inference(rewrite,[status(thm)],[])).
% 258.95/259.26 tff(14,plain,
% 258.95/259.26 ((~((((((((((((((s_best7_init = init) & (s_sworst7_init = init)) & (s_worst7_init = init)) & leq(n0, s_best7)) & leq(n0, s_sworst7)) & leq(n0, s_worst7)) & leq(s_best7, n3)) & leq(s_sworst7, n3)) & leq(s_worst7, n3)) & ![A: $i] : ((leq(n0, A) & leq(A, n2)) => ![B: $i] : ((leq(n0, B) & leq(B, n3)) => (a_select3(simplex7_init, B, A) = init)))) & ![C: $i] : ((leq(n0, C) & leq(C, n3)) => (a_select2(s_values7_init, C) = init))) & ![D: $i] : ((leq(n0, D) & leq(D, n2)) => (a_select2(s_center7_init, D) = init))) & (gt(loopcounter, n1) => (((pvar1400_init = init) & (pvar1401_init = init)) & (pvar1402_init = init)))) => ((((((((((((((s_best7_init = init) & (s_sworst7_init = init)) & (s_worst7_init = init)) & leq(n0, s_best7)) & leq(n0, s_sworst7)) & leq(n0, s_worst7)) & leq(s_best7, n3)) & leq(s_sworst7, n3)) & leq(s_worst7, n3)) & ![E: $i] : ((leq(n0, E) & leq(E, n2)) => ![F: $i] : ((leq(n0, F) & leq(F, n3)) => (a_select3(simplex7_init, F, E) = init)))) & ![G: $i] : ((leq(n0, G) & leq(G, n3)) => (a_select2(s_values7_init, G) = init))) & ![H: $i] : ((leq(n0, H) & leq(H, n2)) => (a_select2(s_center7_init, H) = init))) & ![I: $i] : ((leq(n0, I) & leq(I, minus(n0, n1))) => (a_select2(s_try7_init, I) = init))) & (gt(loopcounter, n1) => (((pvar1400_init = init) & (pvar1401_init = init)) & (pvar1402_init = init)))))) <=> (~((~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) & ![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) | ((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(15,axiom,(~((((((((((((((s_best7_init = init) & (s_sworst7_init = init)) & (s_worst7_init = init)) & leq(n0, s_best7)) & leq(n0, s_sworst7)) & leq(n0, s_worst7)) & leq(s_best7, n3)) & leq(s_sworst7, n3)) & leq(s_worst7, n3)) & ![A: $i] : ((leq(n0, A) & leq(A, n2)) => ![B: $i] : ((leq(n0, B) & leq(B, n3)) => (a_select3(simplex7_init, B, A) = init)))) & ![C: $i] : ((leq(n0, C) & leq(C, n3)) => (a_select2(s_values7_init, C) = init))) & ![D: $i] : ((leq(n0, D) & leq(D, n2)) => (a_select2(s_center7_init, D) = init))) & (gt(loopcounter, n1) => (((pvar1400_init = init) & (pvar1401_init = init)) & (pvar1402_init = init)))) => ((((((((((((((s_best7_init = init) & (s_sworst7_init = init)) & (s_worst7_init = init)) & leq(n0, s_best7)) & leq(n0, s_sworst7)) & leq(n0, s_worst7)) & leq(s_best7, n3)) & leq(s_sworst7, n3)) & leq(s_worst7, n3)) & ![E: $i] : ((leq(n0, E) & leq(E, n2)) => ![F: $i] : ((leq(n0, F) & leq(F, n3)) => (a_select3(simplex7_init, F, E) = init)))) & ![G: $i] : ((leq(n0, G) & leq(G, n3)) => (a_select2(s_values7_init, G) = init))) & ![H: $i] : ((leq(n0, H) & leq(H, n2)) => (a_select2(s_center7_init, H) = init))) & ![I: $i] : ((leq(n0, I) & leq(I, minus(n0, n1))) => (a_select2(s_try7_init, I) = init))) & (gt(loopcounter, n1) => (((pvar1400_init = init) & (pvar1401_init = init)) & (pvar1402_init = init)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gauss_init_0069')).
% 258.95/259.27 tff(16,plain,
% 258.95/259.27 (~((~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) & ![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) | ((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[15, 14])).
% 258.95/259.27 tff(17,plain,
% 258.95/259.27 ((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init))) & ![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))),
% 258.95/259.27 inference(or_elim,[status(thm)],[16])).
% 258.95/259.27 tff(18,plain,
% 258.95/259.27 (![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)))),
% 258.95/259.27 inference(and_elim,[status(thm)],[17])).
% 258.95/259.27 tff(19,plain,
% 258.95/259.27 (![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[18, 13])).
% 258.95/259.27 tff(20,plain,(
% 258.95/259.27 ![A: $i] : ((~(leq(n0, A) & leq(A, n2))) | ![B: $i] : ((~(leq(n0, B) & leq(B, n3))) | (a_select3(simplex7_init, B, A) = init)))),
% 258.95/259.27 inference(skolemize,[status(sab)],[19])).
% 258.95/259.27 tff(21,plain,
% 258.95/259.27 (![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[20, 12])).
% 258.95/259.27 tff(22,plain,
% 258.95/259.27 (![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[21, 10])).
% 258.95/259.27 tff(23,plain,
% 258.95/259.27 (((~![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))) | ((~leq(n0, E!13)) | (~leq(E!13, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3))))) <=> ((~![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))) | (~leq(n0, E!13)) | (~leq(E!13, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(24,plain,
% 258.95/259.27 ((~![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))) | ((~leq(n0, E!13)) | (~leq(E!13, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3))))),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(25,plain,
% 258.95/259.27 ((~![A: $i] : ((~leq(n0, A)) | (~leq(A, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, A) = init) | (~leq(n0, B)) | (~leq(B, n3))))) | (~leq(n0, E!13)) | (~leq(E!13, n2)) | ![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[24, 23])).
% 258.95/259.27 tff(26,plain,
% 258.95/259.27 (![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[25, 22, 5, 3])).
% 258.95/259.27 tff(27,plain,
% 258.95/259.27 (((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))) | leq(F!14, n3)),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(28,plain,
% 258.95/259.27 (leq(F!14, n3)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[27, 1])).
% 258.95/259.27 tff(29,plain,
% 258.95/259.27 (((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))) | leq(n0, F!14)),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(30,plain,
% 258.95/259.27 (leq(n0, F!14)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[29, 1])).
% 258.95/259.27 tff(31,plain,
% 258.95/259.27 (((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))) | (~(a_select3(simplex7_init, F!14, E!13) = init))),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(32,plain,
% 258.95/259.27 (~(a_select3(simplex7_init, F!14, E!13) = init)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[31, 1])).
% 258.95/259.27 tff(33,plain,
% 258.95/259.27 (((~![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))) | ((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)))) <=> ((~![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))) | (a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(34,plain,
% 258.95/259.27 ((~![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))) | ((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)))),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(35,plain,
% 258.95/259.27 ((~![B: $i] : ((a_select3(simplex7_init, B, E!13) = init) | (~leq(n0, B)) | (~leq(B, n3)))) | (a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[34, 33])).
% 258.95/259.27 tff(36,plain,
% 258.95/259.27 ($false),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[35, 32, 30, 28, 26])).
% 258.95/259.27 tff(37,plain,((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))), inference(lemma,lemma(discharge,[]))).
% 258.95/259.27 tff(38,plain,
% 258.95/259.27 (^[X: $i] : refl((minus(X, n1) = pred(X)) <=> (minus(X, n1) = pred(X)))),
% 258.95/259.27 inference(bind,[status(th)],[])).
% 258.95/259.27 tff(39,plain,
% 258.95/259.27 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 258.95/259.27 inference(quant_intro,[status(thm)],[38])).
% 258.95/259.27 tff(40,plain,
% 258.95/259.27 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(41,axiom,(![X: $i] : (minus(X, n1) = pred(X))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','pred_minus_1')).
% 258.95/259.27 tff(42,plain,
% 258.95/259.27 (![X: $i] : (minus(X, n1) = pred(X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[41, 40])).
% 258.95/259.27 tff(43,plain,(
% 258.95/259.27 ![X: $i] : (minus(X, n1) = pred(X))),
% 258.95/259.27 inference(skolemize,[status(sab)],[42])).
% 258.95/259.27 tff(44,plain,
% 258.95/259.27 (![X: $i] : (minus(X, n1) = pred(X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[43, 39])).
% 258.95/259.27 tff(45,plain,
% 258.95/259.27 ((~![X: $i] : (minus(X, n1) = pred(X))) | (minus(n0, n1) = pred(n0))),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(46,plain,
% 258.95/259.27 (minus(n0, n1) = pred(n0)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[45, 44])).
% 258.95/259.27 tff(47,plain,
% 258.95/259.27 (pred(n0) = minus(n0, n1)),
% 258.95/259.27 inference(symmetry,[status(thm)],[46])).
% 258.95/259.27 tff(48,plain,
% 258.95/259.27 ((succ(tptp_minus_1) = n0) <=> (succ(tptp_minus_1) = n0)),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(49,axiom,(succ(tptp_minus_1) = n0), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','succ_tptp_minus_1')).
% 258.95/259.27 tff(50,plain,
% 258.95/259.27 (succ(tptp_minus_1) = n0),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[49, 48])).
% 258.95/259.27 tff(51,plain,
% 258.95/259.27 (n0 = succ(tptp_minus_1)),
% 258.95/259.27 inference(symmetry,[status(thm)],[50])).
% 258.95/259.27 tff(52,plain,
% 258.95/259.27 (pred(n0) = pred(succ(tptp_minus_1))),
% 258.95/259.27 inference(monotonicity,[status(thm)],[51])).
% 258.95/259.27 tff(53,plain,
% 258.95/259.27 (pred(succ(tptp_minus_1)) = pred(n0)),
% 258.95/259.27 inference(symmetry,[status(thm)],[52])).
% 258.95/259.27 tff(54,plain,
% 258.95/259.27 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(55,plain,
% 258.95/259.27 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(56,axiom,(![X: $i] : (pred(succ(X)) = X)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','pred_succ')).
% 258.95/259.27 tff(57,plain,
% 258.95/259.27 (![X: $i] : (pred(succ(X)) = X)),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[56, 55])).
% 258.95/259.27 tff(58,plain,(
% 258.95/259.27 ![X: $i] : (pred(succ(X)) = X)),
% 258.95/259.27 inference(skolemize,[status(sab)],[57])).
% 258.95/259.27 tff(59,plain,
% 258.95/259.27 (![X: $i] : (pred(succ(X)) = X)),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[58, 54])).
% 258.95/259.27 tff(60,plain,
% 258.95/259.27 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(tptp_minus_1)) = tptp_minus_1)),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(61,plain,
% 258.95/259.27 (pred(succ(tptp_minus_1)) = tptp_minus_1),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[60, 59])).
% 258.95/259.27 tff(62,plain,
% 258.95/259.27 (tptp_minus_1 = pred(succ(tptp_minus_1))),
% 258.95/259.27 inference(symmetry,[status(thm)],[61])).
% 258.95/259.27 tff(63,plain,
% 258.95/259.27 (tptp_minus_1 = minus(n0, n1)),
% 258.95/259.27 inference(transitivity,[status(thm)],[62, 53, 47])).
% 258.95/259.27 tff(64,plain,
% 258.95/259.27 (leq(I!17, tptp_minus_1) <=> leq(I!17, minus(n0, n1))),
% 258.95/259.27 inference(monotonicity,[status(thm)],[63])).
% 258.95/259.27 tff(65,plain,
% 258.95/259.27 (leq(I!17, minus(n0, n1)) <=> leq(I!17, tptp_minus_1)),
% 258.95/259.27 inference(symmetry,[status(thm)],[64])).
% 258.95/259.27 tff(66,assumption,(~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1))))), introduced(assumption)).
% 258.95/259.27 tff(67,plain,
% 258.95/259.27 (((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1)))) | leq(I!17, minus(n0, n1))),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(68,plain,
% 258.95/259.27 (leq(I!17, minus(n0, n1))),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[67, 66])).
% 258.95/259.27 tff(69,plain,
% 258.95/259.27 (leq(I!17, tptp_minus_1)),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[68, 65])).
% 258.95/259.27 tff(70,plain,
% 258.95/259.27 (pred(n0) = tptp_minus_1),
% 258.95/259.27 inference(transitivity,[status(thm)],[52, 61])).
% 258.95/259.27 tff(71,plain,
% 258.95/259.27 (leq(n0, pred(n0)) <=> leq(n0, tptp_minus_1)),
% 258.95/259.27 inference(monotonicity,[status(thm)],[70])).
% 258.95/259.27 tff(72,plain,
% 258.95/259.27 ((~leq(n0, pred(n0))) <=> (~leq(n0, tptp_minus_1))),
% 258.95/259.27 inference(monotonicity,[status(thm)],[71])).
% 258.95/259.27 tff(73,plain,
% 258.95/259.27 (^[X: $i, Y: $i] : refl((leq(X, pred(Y)) <=> gt(Y, X)) <=> (leq(X, pred(Y)) <=> gt(Y, X)))),
% 258.95/259.27 inference(bind,[status(th)],[])).
% 258.95/259.27 tff(74,plain,
% 258.95/259.27 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X)) <=> ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 258.95/259.27 inference(quant_intro,[status(thm)],[73])).
% 258.95/259.27 tff(75,plain,
% 258.95/259.27 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X)) <=> ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(76,axiom,(![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','leq_gt_pred')).
% 258.95/259.27 tff(77,plain,
% 258.95/259.27 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[76, 75])).
% 258.95/259.27 tff(78,plain,(
% 258.95/259.27 ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 258.95/259.27 inference(skolemize,[status(sab)],[77])).
% 258.95/259.27 tff(79,plain,
% 258.95/259.27 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[78, 74])).
% 258.95/259.27 tff(80,plain,
% 258.95/259.27 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(n0, pred(n0)) <=> gt(n0, n0))),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(81,plain,
% 258.95/259.27 (leq(n0, pred(n0)) <=> gt(n0, n0)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[80, 79])).
% 258.95/259.27 tff(82,plain,
% 258.95/259.27 (^[X: $i] : refl((~gt(X, X)) <=> (~gt(X, X)))),
% 258.95/259.27 inference(bind,[status(th)],[])).
% 258.95/259.27 tff(83,plain,
% 258.95/259.27 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 258.95/259.27 inference(quant_intro,[status(thm)],[82])).
% 258.95/259.27 tff(84,plain,
% 258.95/259.27 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(85,axiom,(![X: $i] : (~gt(X, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','irreflexivity_gt')).
% 258.95/259.27 tff(86,plain,
% 258.95/259.27 (![X: $i] : (~gt(X, X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[85, 84])).
% 258.95/259.27 tff(87,plain,(
% 258.95/259.27 ![X: $i] : (~gt(X, X))),
% 258.95/259.27 inference(skolemize,[status(sab)],[86])).
% 258.95/259.27 tff(88,plain,
% 258.95/259.27 (![X: $i] : (~gt(X, X))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[87, 83])).
% 258.95/259.27 tff(89,plain,
% 258.95/259.27 ((~![X: $i] : (~gt(X, X))) | (~gt(n0, n0))),
% 258.95/259.27 inference(quant_inst,[status(thm)],[])).
% 258.95/259.27 tff(90,plain,
% 258.95/259.27 (~gt(n0, n0)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[89, 88])).
% 258.95/259.27 tff(91,plain,
% 258.95/259.27 ((~(leq(n0, pred(n0)) <=> gt(n0, n0))) | (~leq(n0, pred(n0))) | gt(n0, n0)),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(92,plain,
% 258.95/259.27 (~leq(n0, pred(n0))),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[91, 90, 81])).
% 258.95/259.27 tff(93,plain,
% 258.95/259.27 (~leq(n0, tptp_minus_1)),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[92, 72])).
% 258.95/259.27 tff(94,plain,
% 258.95/259.27 (((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1)))) | leq(n0, I!17)),
% 258.95/259.27 inference(tautology,[status(thm)],[])).
% 258.95/259.27 tff(95,plain,
% 258.95/259.27 (leq(n0, I!17)),
% 258.95/259.27 inference(unit_resolution,[status(thm)],[94, 66])).
% 258.95/259.27 tff(96,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(97,plain,
% 258.95/259.27 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(X, Y) & leq(Y, Z)) <=> (~((~leq(Y, Z)) | (~leq(X, Y))))), ((~(leq(X, Y) & leq(Y, Z))) <=> (~(~((~leq(Y, Z)) | (~leq(X, Y))))))), rewrite((~(~((~leq(Y, Z)) | (~leq(X, Y))))) <=> ((~leq(Y, Z)) | (~leq(X, Y)))), ((~(leq(X, Y) & leq(Y, Z))) <=> ((~leq(Y, Z)) | (~leq(X, Y))))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)))), rewrite((((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))))),
% 258.95/259.27 inference(bind,[status(th)],[])).
% 258.95/259.27 tff(98,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 258.95/259.27 inference(quant_intro,[status(thm)],[97])).
% 258.95/259.27 tff(99,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 258.95/259.27 inference(rewrite,[status(thm)],[])).
% 258.95/259.27 tff(100,plain,
% 258.95/259.27 (^[X: $i, Y: $i, Z: $i] : rewrite(((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)))),
% 258.95/259.27 inference(bind,[status(th)],[])).
% 258.95/259.27 tff(101,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 258.95/259.27 inference(quant_intro,[status(thm)],[100])).
% 258.95/259.27 tff(102,axiom,(![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','transitivity_leq')).
% 258.95/259.27 tff(103,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[102, 101])).
% 258.95/259.27 tff(104,plain,
% 258.95/259.27 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 258.95/259.27 inference(modus_ponens,[status(thm)],[103, 99])).
% 258.95/259.27 tff(105,plain,(
% 258.95/259.28 ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 258.95/259.28 inference(skolemize,[status(sab)],[104])).
% 258.95/259.28 tff(106,plain,
% 258.95/259.28 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[105, 98])).
% 258.95/259.28 tff(107,plain,
% 258.95/259.28 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[106, 96])).
% 258.95/259.28 tff(108,plain,
% 258.95/259.28 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(109,plain,
% 258.95/259.28 ((leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)) | (~leq(n0, I!17))) <=> ((~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(110,plain,
% 258.95/259.28 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)) | (~leq(n0, I!17)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1))))),
% 258.95/259.28 inference(monotonicity,[status(thm)],[109])).
% 258.95/259.28 tff(111,plain,
% 258.95/259.28 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)) | (~leq(n0, I!17)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)))),
% 258.95/259.28 inference(transitivity,[status(thm)],[110, 108])).
% 258.95/259.28 tff(112,plain,
% 258.95/259.28 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1)) | (~leq(n0, I!17)))),
% 258.95/259.28 inference(quant_inst,[status(thm)],[])).
% 258.95/259.28 tff(113,plain,
% 258.95/259.28 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(n0, I!17)) | leq(n0, tptp_minus_1) | (~leq(I!17, tptp_minus_1))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[112, 111])).
% 258.95/259.28 tff(114,plain,
% 258.95/259.28 (~leq(I!17, tptp_minus_1)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[113, 107, 95, 93])).
% 258.95/259.28 tff(115,plain,
% 258.95/259.28 ($false),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[114, 69])).
% 258.95/259.28 tff(116,plain,((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1)))), inference(lemma,lemma(discharge,[]))).
% 258.95/259.28 tff(117,assumption,(~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))), introduced(assumption)).
% 258.95/259.28 tff(118,plain,
% 258.95/259.28 (((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))) | leq(G!15, n3)),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(119,plain,
% 258.95/259.28 (leq(G!15, n3)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[118, 117])).
% 258.95/259.28 tff(120,plain,
% 258.95/259.28 (((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))) | leq(n0, G!15)),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(121,plain,
% 258.95/259.28 (leq(n0, G!15)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[120, 117])).
% 258.95/259.28 tff(122,plain,
% 258.95/259.28 (((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))) | (~(a_select2(s_values7_init, G!15) = init))),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(123,plain,
% 258.95/259.28 (~(a_select2(s_values7_init, G!15) = init)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[122, 117])).
% 258.95/259.28 tff(124,plain,
% 258.95/259.28 (^[C: $i] : refl(((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3))) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3))))),
% 258.95/259.28 inference(bind,[status(th)],[])).
% 258.95/259.28 tff(125,plain,
% 258.95/259.28 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3))) <=> ![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))),
% 258.95/259.28 inference(quant_intro,[status(thm)],[124])).
% 258.95/259.28 tff(126,plain,
% 258.95/259.28 (^[C: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, C) & leq(C, n3)) <=> (~((~leq(n0, C)) | (~leq(C, n3))))), ((~(leq(n0, C) & leq(C, n3))) <=> (~(~((~leq(n0, C)) | (~leq(C, n3))))))), rewrite((~(~((~leq(n0, C)) | (~leq(C, n3))))) <=> ((~leq(n0, C)) | (~leq(C, n3)))), ((~(leq(n0, C) & leq(C, n3))) <=> ((~leq(n0, C)) | (~leq(C, n3))))), (((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) <=> (((~leq(n0, C)) | (~leq(C, n3))) | (a_select2(s_values7_init, C) = init)))), rewrite((((~leq(n0, C)) | (~leq(C, n3))) | (a_select2(s_values7_init, C) = init)) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))), (((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))))),
% 258.95/259.28 inference(bind,[status(th)],[])).
% 258.95/259.28 tff(127,plain,
% 258.95/259.28 (![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) <=> ![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))),
% 258.95/259.28 inference(quant_intro,[status(thm)],[126])).
% 258.95/259.28 tff(128,plain,
% 258.95/259.28 (![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init)) <=> ![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(129,plain,
% 258.95/259.28 (![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init))),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(130,plain,
% 258.95/259.28 (![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[129, 128])).
% 258.95/259.28 tff(131,plain,(
% 258.95/259.28 ![C: $i] : ((~(leq(n0, C) & leq(C, n3))) | (a_select2(s_values7_init, C) = init))),
% 258.95/259.28 inference(skolemize,[status(sab)],[130])).
% 258.95/259.28 tff(132,plain,
% 258.95/259.28 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[131, 127])).
% 258.95/259.28 tff(133,plain,
% 258.95/259.28 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[132, 125])).
% 258.95/259.28 tff(134,plain,
% 258.95/259.28 (((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))) | ((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))) <=> ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))) | (a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(135,plain,
% 258.95/259.28 ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))) | ((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))),
% 258.95/259.28 inference(quant_inst,[status(thm)],[])).
% 258.95/259.28 tff(136,plain,
% 258.95/259.28 ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, n3)))) | (a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[135, 134])).
% 258.95/259.28 tff(137,plain,
% 258.95/259.28 ($false),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[136, 133, 123, 121, 119])).
% 258.95/259.28 tff(138,plain,((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))), inference(lemma,lemma(discharge,[]))).
% 258.95/259.28 tff(139,assumption,(~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))), introduced(assumption)).
% 258.95/259.28 tff(140,plain,
% 258.95/259.28 (((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))) | leq(H!16, n2)),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(141,plain,
% 258.95/259.28 (leq(H!16, n2)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[140, 139])).
% 258.95/259.28 tff(142,plain,
% 258.95/259.28 (((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))) | leq(n0, H!16)),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(143,plain,
% 258.95/259.28 (leq(n0, H!16)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[142, 139])).
% 258.95/259.28 tff(144,plain,
% 258.95/259.28 (((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))) | (~(a_select2(s_center7_init, H!16) = init))),
% 258.95/259.28 inference(tautology,[status(thm)],[])).
% 258.95/259.28 tff(145,plain,
% 258.95/259.28 (~(a_select2(s_center7_init, H!16) = init)),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[144, 139])).
% 258.95/259.28 tff(146,plain,
% 258.95/259.28 (^[D: $i] : refl(((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2))) <=> ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2))))),
% 258.95/259.28 inference(bind,[status(th)],[])).
% 258.95/259.28 tff(147,plain,
% 258.95/259.28 (![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2))) <=> ![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))),
% 258.95/259.28 inference(quant_intro,[status(thm)],[146])).
% 258.95/259.28 tff(148,plain,
% 258.95/259.28 (^[D: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, D) & leq(D, n2)) <=> (~((~leq(n0, D)) | (~leq(D, n2))))), ((~(leq(n0, D) & leq(D, n2))) <=> (~(~((~leq(n0, D)) | (~leq(D, n2))))))), rewrite((~(~((~leq(n0, D)) | (~leq(D, n2))))) <=> ((~leq(n0, D)) | (~leq(D, n2)))), ((~(leq(n0, D) & leq(D, n2))) <=> ((~leq(n0, D)) | (~leq(D, n2))))), (((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) <=> (((~leq(n0, D)) | (~leq(D, n2))) | (a_select2(s_center7_init, D) = init)))), rewrite((((~leq(n0, D)) | (~leq(D, n2))) | (a_select2(s_center7_init, D) = init)) <=> ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))), (((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) <=> ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))))),
% 258.95/259.28 inference(bind,[status(th)],[])).
% 258.95/259.28 tff(149,plain,
% 258.95/259.28 (![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) <=> ![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))),
% 258.95/259.28 inference(quant_intro,[status(thm)],[148])).
% 258.95/259.28 tff(150,plain,
% 258.95/259.28 (![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init)) <=> ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(151,plain,
% 258.95/259.28 (![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init))),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(152,plain,
% 258.95/259.28 (![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[151, 150])).
% 258.95/259.28 tff(153,plain,(
% 258.95/259.28 ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | (a_select2(s_center7_init, D) = init))),
% 258.95/259.28 inference(skolemize,[status(sab)],[152])).
% 258.95/259.28 tff(154,plain,
% 258.95/259.28 (![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[153, 149])).
% 258.95/259.28 tff(155,plain,
% 258.95/259.28 (![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[154, 147])).
% 258.95/259.28 tff(156,plain,
% 258.95/259.28 (((~![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))) | ((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))) <=> ((~![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))) | (a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(157,plain,
% 258.95/259.28 ((~![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))) | ((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))),
% 258.95/259.28 inference(quant_inst,[status(thm)],[])).
% 258.95/259.28 tff(158,plain,
% 258.95/259.28 ((~![D: $i] : ((a_select2(s_center7_init, D) = init) | (~leq(n0, D)) | (~leq(D, n2)))) | (a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[157, 156])).
% 258.95/259.28 tff(159,plain,
% 258.95/259.28 ($false),
% 258.95/259.28 inference(unit_resolution,[status(thm)],[158, 155, 145, 143, 141])).
% 258.95/259.28 tff(160,plain,((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))), inference(lemma,lemma(discharge,[]))).
% 258.95/259.28 tff(161,plain,
% 258.95/259.28 (leq(s_worst7, n3) <=> leq(s_worst7, n3)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(162,plain,
% 258.95/259.28 (leq(s_worst7, n3)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(163,plain,
% 258.95/259.28 (leq(s_worst7, n3)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[162, 161])).
% 258.95/259.28 tff(164,plain,
% 258.95/259.28 (leq(s_sworst7, n3) <=> leq(s_sworst7, n3)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(165,plain,
% 258.95/259.28 (leq(s_sworst7, n3)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(166,plain,
% 258.95/259.28 (leq(s_sworst7, n3)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[165, 164])).
% 258.95/259.28 tff(167,plain,
% 258.95/259.28 (leq(s_best7, n3) <=> leq(s_best7, n3)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(168,plain,
% 258.95/259.28 (leq(s_best7, n3)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(169,plain,
% 258.95/259.28 (leq(s_best7, n3)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[168, 167])).
% 258.95/259.28 tff(170,plain,
% 258.95/259.28 (leq(n0, s_worst7) <=> leq(n0, s_worst7)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(171,plain,
% 258.95/259.28 (leq(n0, s_worst7)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(172,plain,
% 258.95/259.28 (leq(n0, s_worst7)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[171, 170])).
% 258.95/259.28 tff(173,plain,
% 258.95/259.28 (leq(n0, s_sworst7) <=> leq(n0, s_sworst7)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(174,plain,
% 258.95/259.28 (leq(n0, s_sworst7)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(175,plain,
% 258.95/259.28 (leq(n0, s_sworst7)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[174, 173])).
% 258.95/259.28 tff(176,plain,
% 258.95/259.28 (leq(n0, s_best7) <=> leq(n0, s_best7)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(177,plain,
% 258.95/259.28 (leq(n0, s_best7)),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(178,plain,
% 258.95/259.28 (leq(n0, s_best7)),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[177, 176])).
% 258.95/259.28 tff(179,plain,
% 258.95/259.28 ((s_worst7_init = init) <=> (s_worst7_init = init)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(180,plain,
% 258.95/259.28 (s_worst7_init = init),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(181,plain,
% 258.95/259.28 (s_worst7_init = init),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[180, 179])).
% 258.95/259.28 tff(182,plain,
% 258.95/259.28 ((s_sworst7_init = init) <=> (s_sworst7_init = init)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(183,plain,
% 258.95/259.28 (s_sworst7_init = init),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(184,plain,
% 258.95/259.28 (s_sworst7_init = init),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[183, 182])).
% 258.95/259.28 tff(185,plain,
% 258.95/259.28 ((s_best7_init = init) <=> (s_best7_init = init)),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(186,plain,
% 258.95/259.28 (s_best7_init = init),
% 258.95/259.28 inference(and_elim,[status(thm)],[17])).
% 258.95/259.28 tff(187,plain,
% 258.95/259.28 (s_best7_init = init),
% 258.95/259.28 inference(modus_ponens,[status(thm)],[186, 185])).
% 258.95/259.28 tff(188,plain,
% 258.95/259.28 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))) | (~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))) | (~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1))))) | (~((~gt(loopcounter, n1)) | (~((~(pvar1400_init = init)) | (~(pvar1401_init = init)) | (~(pvar1402_init = init)))))) | (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~gt(loopcounter, n1)) | (~((~(pvar1400_init = init)) | (~(pvar1401_init = init)) | (~(pvar1402_init = init)))))) | (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2)))) | (~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))) | (~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))) | (~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1))))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(189,plain,
% 258.95/259.28 ((leq(n0, E!13) & leq(E!13, n2) & (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3))))) <=> (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(190,plain,
% 258.95/259.28 ((~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init))) <=> (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(191,plain,
% 258.95/259.28 ((leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) <=> (leq(n0, E!13) & leq(E!13, n2) & (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)))))),
% 258.95/259.28 inference(monotonicity,[status(thm)],[190])).
% 258.95/259.28 tff(192,plain,
% 258.95/259.28 ((leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) <=> (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2))))),
% 258.95/259.28 inference(transitivity,[status(thm)],[191, 189])).
% 258.95/259.28 tff(193,plain,
% 258.95/259.28 ((~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) <=> (~((~gt(loopcounter, n1)) | (~((~(pvar1400_init = init)) | (~(pvar1401_init = init)) | (~(pvar1402_init = init))))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(194,plain,
% 258.95/259.28 ((~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) <=> (~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1)))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(195,plain,
% 258.95/259.28 ((~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) <=> (~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(196,plain,
% 258.95/259.28 ((~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) <=> (~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3))))),
% 258.95/259.28 inference(rewrite,[status(thm)],[])).
% 258.95/259.28 tff(197,plain,
% 258.95/259.28 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))) | (~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))) | (~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1))))) | (~((~gt(loopcounter, n1)) | (~((~(pvar1400_init = init)) | (~(pvar1401_init = init)) | (~(pvar1402_init = init)))))) | (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2)))))),
% 258.95/259.29 inference(monotonicity,[status(thm)],[196, 195, 194, 193, 192])).
% 258.95/259.29 tff(198,plain,
% 258.95/259.29 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~gt(loopcounter, n1)) | (~((~(pvar1400_init = init)) | (~(pvar1401_init = init)) | (~(pvar1402_init = init)))))) | (~((a_select3(simplex7_init, F!14, E!13) = init) | (~leq(n0, F!14)) | (~leq(F!14, n3)) | (~leq(n0, E!13)) | (~leq(E!13, n2)))) | (~((a_select2(s_values7_init, G!15) = init) | (~leq(n0, G!15)) | (~leq(G!15, n3)))) | (~((a_select2(s_center7_init, H!16) = init) | (~leq(n0, H!16)) | (~leq(H!16, n2)))) | (~((a_select2(s_try7_init, I!17) = init) | (~leq(n0, I!17)) | (~leq(I!17, minus(n0, n1))))))),
% 258.95/259.29 inference(transitivity,[status(thm)],[197, 188])).
% 258.95/259.29 tff(199,plain,
% 258.95/259.29 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))))),
% 259.04/259.29 inference(rewrite,[status(thm)],[])).
% 259.04/259.29 tff(200,plain,
% 259.04/259.29 (((leq(n0, E!13) & leq(E!13, n2)) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) <=> (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init))))),
% 259.04/259.29 inference(rewrite,[status(thm)],[])).
% 259.04/259.29 tff(201,plain,
% 259.04/259.29 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | ((leq(n0, E!13) & leq(E!13, n2)) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))))),
% 259.04/259.29 inference(monotonicity,[status(thm)],[200])).
% 259.04/259.29 tff(202,plain,
% 259.04/259.29 (((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | ((leq(n0, E!13) & leq(E!13, n2)) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) <=> ((~(s_best7_init = init)) | (~(s_sworst7_init = init)) | (~(s_worst7_init = init)) | (~leq(n0, s_best7)) | (~leq(n0, s_sworst7)) | (~leq(n0, s_worst7)) | (~leq(s_best7, n3)) | (~leq(s_sworst7, n3)) | (~leq(s_worst7, n3)) | (~((~(leq(n0, G!15) & leq(G!15, n3))) | (a_select2(s_values7_init, G!15) = init))) | (~((~(leq(n0, H!16) & leq(H!16, n2))) | (a_select2(s_center7_init, H!16) = init))) | (~((~(leq(n0, I!17) & leq(I!17, minus(n0, n1)))) | (a_select2(s_try7_init, I!17) = init))) | (~((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) | (leq(n0, E!13) & leq(E!13, n2) & (~((~(leq(n0, F!14) & leq(F!14, n3))) | (a_select3(simplex7_init, F!14, E!13) = init)))))),
% 259.04/259.29 inference(transitivity,[status(thm)],[201, 199])).
% 259.04/259.29 tff(203,plain,
% 259.04/259.29 (((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))) <=> ((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))),
% 259.04/259.29 inference(rewrite,[status(thm)],[])).
% 259.04/259.29 tff(204,plain,
% 259.04/259.29 ((~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) <=> (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))))),
% 259.04/259.29 inference(monotonicity,[status(thm)],[203])).
% 259.04/259.29 tff(205,plain,
% 259.04/259.29 ((~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))) <=> (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init)))))),
% 259.04/259.29 inference(rewrite,[status(thm)],[])).
% 259.04/259.29 tff(206,plain,
% 259.04/259.29 (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))),
% 259.04/259.30 inference(or_elim,[status(thm)],[16])).
% 259.04/259.30 tff(207,plain,
% 259.04/259.30 (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))),
% 259.04/259.30 inference(modus_ponens,[status(thm)],[206, 204])).
% 259.04/259.30 tff(208,plain,
% 259.04/259.30 (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))),
% 259.04/259.30 inference(modus_ponens,[status(thm)],[207, 205])).
% 259.04/259.30 tff(209,plain,
% 259.04/259.30 (~((s_best7_init = init) & (s_sworst7_init = init) & (s_worst7_init = init) & leq(n0, s_best7) & leq(n0, s_sworst7) & leq(n0, s_worst7) & leq(s_best7, n3) & leq(s_sworst7, n3) & leq(s_worst7, n3) & ![E: $i] : ((~(leq(n0, E) & leq(E, n2))) | ![F: $i] : ((~(leq(n0, F) & leq(F, n3))) | (a_select3(simplex7_init, F, E) = init))) & ![G: $i] : ((~(leq(n0, G) & leq(G, n3))) | (a_select2(s_values7_init, G) = init)) & ![H: $i] : ((~(leq(n0, H) & leq(H, n2))) | (a_select2(s_center7_init, H) = init)) & ![I: $i] : ((~(leq(n0, I) & leq(I, minus(n0, n1)))) | (a_select2(s_try7_init, I) = init)) & ((~gt(loopcounter, n1)) | ((pvar1400_init = init) & (pvar1401_init = init) & (pvar1402_init = init))))),
% 259.04/259.30 inference(modus_ponens,[status(thm)],[208, 204])).
% 259.04/259.30 unexpected number of arguments: (let ((a!1 (refl (~ (not (= s_best7_init init)) (not (= s_best7_init init)))))
% 259.04/259.30 (a!2 (refl (~ (not (= s_sworst7_init init)) (not (= s_sworst7_init init)))))
% 259.04/259.30 (a!3 (refl (~ (not (= s_worst7_init init)) (not (= s_worst7_init init)))))
% 259.04/259.30 (a!4 (refl (~ (not (leq n0 s_best7)) (not (leq n0 s_best7)))))
% 259.04/259.30 (a!5 (refl (~ (not (leq n0 s_sworst7)) (not (leq n0 s_sworst7)))))
% 259.04/259.30 (a!6 (refl (~ (not (leq n0 s_worst7)) (not (leq n0 s_worst7)))))
% 259.04/259.30 (a!7 (refl (~ (not (leq s_best7 n3)) (not (leq s_best7 n3)))))
% 259.04/259.30 (a!8 (refl (~ (not (leq s_sworst7 n3)) (not (leq s_sworst7 n3)))))
% 259.04/259.30 (a!9 (refl (~ (not (leq s_worst7 n3)) (not (leq s_worst7 n3)))))
% 259.04/259.30 (a!10 (forall ((E $i))
% 259.04/259.30 (let ((a!1 (forall ((F $i))
% 259.04/259.30 (or (not (and (leq n0 F) (leq F n3)))
% 259.04/259.30 (= (a_select3 simplex7_init F E) init)))))
% 259.04/259.30 (or (not (and (leq n0 E) (leq E n2))) a!1))))
% 259.04/259.30 (a!11 (forall ((F $i))
% 259.04/259.30 (or (not (and (leq n0 F) (leq F n3)))
% 259.04/259.30 (= (a_select3 simplex7_init F E!13) init))))
% 259.04/259.30 (a!13 (refl (~ (and (leq n0 E!13) (leq E!13 n2))
% 259.04/259.30 (and (leq n0 E!13) (leq E!13 n2)))))
% 259.04/259.30 (a!14 (or (not (and (leq n0 F!14) (leq F!14 n3)))
% 259.04/259.30 (= (a_select3 simplex7_init F!14 E!13) init)))
% 259.04/259.30 (a!18 (forall ((G $i))
% 259.04/259.30 (or (not (and (leq n0 G) (leq G n3)))
% 259.04/259.30 (= (a_select2 s_values7_init G) init))))
% 259.04/259.30 (a!19 (or (not (and (leq n0 G!15) (leq G!15 n3)))
% 259.04/259.30 (= (a_select2 s_values7_init G!15) init)))
% 259.04/259.30 (a!20 (forall ((H $i))
% 259.04/259.30 (or (not (and (leq n0 H) (leq H n2)))
% 259.04/259.30 (= (a_select2 s_center7_init H) init))))
% 259.04/259.30 (a!21 (or (not (and (leq n0 H!16) (leq H!16 n2)))
% 259.04/259.30 (= (a_select2 s_center7_init H!16) init)))
% 259.04/259.30 (a!22 (forall ((I $i))
% 259.04/259.30 (let ((a!1 (not (and (leq n0 I) (leq I (minus n0 n1))))))
% 259.04/259.30 (or a!1 (= (a_select2 s_try7_init I) init)))))
% 259.04/259.30 (a!23 (not (and (leq n0 I!17) (leq I!17 (minus n0 n1)))))
% 259.04/259.30 (a!25 (or (not (gt loopcounter n1))
% 259.04/259.30 (and (= pvar1400_init init)
% 259.04/259.30 (= pvar1401_init init)
% 259.04/259.30 (= pvar1402_init init)))))
% 259.04/259.30 (let ((a!12 (or (not (and (leq n0 E!13) (leq E!13 n2))) a!11))
% 259.04/259.30 (a!15 (and (and (leq n0 E!13) (leq E!13 n2)) (not a!14)))
% 259.04/259.30 (a!24 (not (or a!23 (= (a_select2 s_try7_init I!17) init)))))
% 259.04/259.30 (let ((a!16 (nnf-neg a!13 (sk (~ (not a!11) (not a!14))) (~ (not a!12) a!15)))
% 259.04/259.30 (a!26 (~ (not (and (= s_best7_init init)
% 259.04/259.30 (= s_sworst7_init init)
% 259.04/259.30 (= s_worst7_init init)
% 259.04/259.30 (leq n0 s_best7)
% 259.04/259.30 (leq n0 s_sworst7)
% 259.04/259.30 (leq n0 s_worst7)
% 259.04/259.30 (leq s_best7 n3)
% 259.04/259.30 (leq s_sworst7 n3)
% 259.04/259.30 (leq s_worst7 n3)
% 259.04/259.30 a!10
% 259.04/259.30 a!18
% 259.04/259.30 a!20
% 259.04/259.30 a!22
% 259.04/259.30 a!25))
% 259.04/259.30 (or (not (= s_best7_init init))
% 259.04/259.30 (not (= s_sworst7_init init))
% 259.04/259.30 (not (= s_worst7_init init))
% 259.04/259.30 (not (leq n0 s_best7))
% 259.04/259.30 (not (leq n0 s_sworst7))
% 259.04/259.30 (not (leq n0 s_worst7))
% 259.04/259.30 (not (leq s_best7 n3))
% 259.04/259.30 (not (leq s_sworst7 n3))
% 259.04/259.30 (not (leq s_worst7 n3))
% 259.04/259.30 a!15
% 259.04/259.30 (not a!19)
% 259.04/259.30 (not a!21)
% 259.04/259.30 a!24
% 259.04/259.30 (not a!25)))))
% 259.04/259.30 (let ((a!17 (trans (sk (~ (not a!10) (not a!12))) a!16 (~ (not a!10) a!15))))
% 259.04/259.30 (nnf-neg a!1
% 259.04/259.30 a!2
% 259.04/259.30 a!3
% 259.04/259.30 a!4
% 259.04/259.30 a!5
% 259.04/259.30 a!6
% 259.04/259.30 a!7
% 259.04/259.30 a!8
% 259.04/259.30 a!9
% 259.04/259.30 a!17
% 259.04/259.30 (sk (~ (not a!18) (not a!19)))
% 259.04/259.30 (sk (~ (not a!20) (not a!21)))
% 259.04/259.30 (sk (~ (not a!22) a!24))
% 259.04/259.30 (refl (~ (not a!25) (not a!25)))
% 259.04/259.30 a!26)))))
% 259.04/259.30 Proof display could not be completed: unexpected number of arguments
% 259.65/259.91 % E exiting
%------------------------------------------------------------------------------