%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV030+1 : TPTP v9.0.0. Bugfixed v3.3.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:31:22 AM UTC 2025
% Result : Theorem 238.29s 238.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWV030+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.03/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 09:23:10 EDT 2025
% 0.12/0.34 % CPUTime :
% 238.29/238.51 % SZS status Theorem
% 238.29/238.51 % SZS output start Proof
% 238.29/238.51 tff(leq_type, type, (
% 238.29/238.51 leq: ( $i * $i ) > $o)).
% 238.29/238.51 tff(n3_type, type, (
% 238.29/238.51 n3: $i)).
% 238.29/238.51 tff(n0_type, type, (
% 238.29/238.51 n0: $i)).
% 238.29/238.51 tff(init_type, type, (
% 238.29/238.51 init: $i)).
% 238.29/238.51 tff(a_select3_type, type, (
% 238.29/238.51 a_select3: ( $i * $i * $i ) > $i)).
% 238.29/238.51 tff(tptp_fun_D_13_type, type, (
% 238.29/238.51 tptp_fun_D_13: $i)).
% 238.29/238.51 tff(simplex7_init_type, type, (
% 238.29/238.51 simplex7_init: $i)).
% 238.29/238.51 tff(n2_type, type, (
% 238.29/238.51 n2: $i)).
% 238.29/238.51 tff(tptp_fun_E_14_type, type, (
% 238.29/238.51 tptp_fun_E_14: $i)).
% 238.29/238.51 tff(minus_type, type, (
% 238.29/238.51 minus: ( $i * $i ) > $i)).
% 238.29/238.51 tff(n1_type, type, (
% 238.29/238.51 n1: $i)).
% 238.29/238.51 tff(pv1376_type, type, (
% 238.29/238.51 pv1376: $i)).
% 238.29/238.51 tff(tptp_fun_F_15_type, type, (
% 238.29/238.51 tptp_fun_F_15: $i)).
% 238.29/238.51 tff(a_select2_type, type, (
% 238.29/238.51 a_select2: ( $i * $i ) > $i)).
% 238.29/238.51 tff(s_values7_init_type, type, (
% 238.29/238.51 s_values7_init: $i)).
% 238.29/238.51 tff(n330_type, type, (
% 238.29/238.51 n330: $i)).
% 238.29/238.51 tff(pv20_type, type, (
% 238.29/238.51 pv20: $i)).
% 238.29/238.51 tff(n410_type, type, (
% 238.29/238.51 n410: $i)).
% 238.29/238.51 tff(pv19_type, type, (
% 238.29/238.51 pv19: $i)).
% 238.29/238.51 tff(pv7_type, type, (
% 238.29/238.51 pv7: $i)).
% 238.29/238.51 tff(1,assumption,(~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))), introduced(assumption)).
% 238.29/238.51 tff(2,plain,
% 238.29/238.51 (((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))) | leq(F!15, minus(pv1376, n1))),
% 238.29/238.51 inference(tautology,[status(thm)],[])).
% 238.29/238.51 tff(3,plain,
% 238.29/238.51 (leq(F!15, minus(pv1376, n1))),
% 238.29/238.51 inference(unit_resolution,[status(thm)],[2, 1])).
% 238.29/238.51 tff(4,plain,
% 238.29/238.51 (((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))) | leq(n0, F!15)),
% 238.29/238.51 inference(tautology,[status(thm)],[])).
% 238.29/238.51 tff(5,plain,
% 238.29/238.51 (leq(n0, F!15)),
% 238.29/238.51 inference(unit_resolution,[status(thm)],[4, 1])).
% 238.29/238.51 tff(6,plain,
% 238.29/238.51 (((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))) | (~(a_select2(s_values7_init, F!15) = init))),
% 238.29/238.51 inference(tautology,[status(thm)],[])).
% 238.29/238.51 tff(7,plain,
% 238.29/238.51 (~(a_select2(s_values7_init, F!15) = init)),
% 238.29/238.51 inference(unit_resolution,[status(thm)],[6, 1])).
% 238.29/238.51 tff(8,plain,
% 238.29/238.51 (^[C: $i] : refl(((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))))),
% 238.29/238.51 inference(bind,[status(th)],[])).
% 238.29/238.51 tff(9,plain,
% 238.29/238.51 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))) <=> ![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))),
% 238.29/238.51 inference(quant_intro,[status(thm)],[8])).
% 238.29/238.51 tff(10,plain,
% 238.29/238.51 (^[C: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, C) & leq(C, minus(pv1376, n1))) <=> (~((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))))), ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) <=> (~(~((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))))))), rewrite((~(~((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))))) <=> ((~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))), ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) <=> ((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))))), (((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)) <=> (((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)))), rewrite((((~leq(n0, C)) | (~leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))), (((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)) <=> ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))))),
% 238.29/238.51 inference(bind,[status(th)],[])).
% 238.29/238.51 tff(11,plain,
% 238.29/238.51 (![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)) <=> ![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))),
% 238.29/238.51 inference(quant_intro,[status(thm)],[10])).
% 238.29/238.51 tff(12,plain,
% 238.29/238.51 (![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)) <=> ![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init))),
% 238.29/238.51 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(13,plain,
% 238.29/238.52 ((~((((((((((((init = init) & leq(n0, pv7)) & leq(n0, pv19)) & leq(n0, pv20)) & leq(n0, pv1376)) & leq(pv7, minus(n410, n1))) & leq(pv19, minus(n410, n1))) & leq(pv20, minus(n330, n1))) & leq(pv1376, 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, minus(pv1376, n1))) => (a_select2(s_values7_init, C) = init))) => (((((((((((init = init) & leq(n0, pv7)) & leq(n0, pv19)) & leq(n0, pv20)) & leq(n0, pv1376)) & leq(pv7, minus(n410, n1))) & leq(pv19, minus(n410, n1))) & leq(pv20, minus(n330, n1))) & leq(pv1376, n3)) & ![D: $i] : ((leq(n0, D) & leq(D, n2)) => ![E: $i] : ((leq(n0, E) & leq(E, n3)) => (a_select3(simplex7_init, E, D) = init)))) & ![F: $i] : ((leq(n0, F) & leq(F, minus(pv1376, n1))) => (a_select2(s_values7_init, F) = init))))) <=> (~((~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, 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, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)))) | (leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(14,axiom,(~((((((((((((init = init) & leq(n0, pv7)) & leq(n0, pv19)) & leq(n0, pv20)) & leq(n0, pv1376)) & leq(pv7, minus(n410, n1))) & leq(pv19, minus(n410, n1))) & leq(pv20, minus(n330, n1))) & leq(pv1376, 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, minus(pv1376, n1))) => (a_select2(s_values7_init, C) = init))) => (((((((((((init = init) & leq(n0, pv7)) & leq(n0, pv19)) & leq(n0, pv20)) & leq(n0, pv1376)) & leq(pv7, minus(n410, n1))) & leq(pv19, minus(n410, n1))) & leq(pv20, minus(n330, n1))) & leq(pv1376, n3)) & ![D: $i] : ((leq(n0, D) & leq(D, n2)) => ![E: $i] : ((leq(n0, E) & leq(E, n3)) => (a_select3(simplex7_init, E, D) = init)))) & ![F: $i] : ((leq(n0, F) & leq(F, minus(pv1376, n1))) => (a_select2(s_values7_init, F) = init))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gauss_init_0033')).
% 238.29/238.52 tff(15,plain,
% 238.29/238.52 (~((~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, 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, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init)))) | (leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init))))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[14, 13])).
% 238.29/238.52 tff(16,plain,
% 238.29/238.52 (leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, 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, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init))),
% 238.29/238.52 inference(or_elim,[status(thm)],[15])).
% 238.29/238.52 tff(17,plain,
% 238.29/238.52 (![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init))),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(18,plain,
% 238.29/238.52 (![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[17, 12])).
% 238.29/238.52 tff(19,plain,(
% 238.29/238.52 ![C: $i] : ((~(leq(n0, C) & leq(C, minus(pv1376, n1)))) | (a_select2(s_values7_init, C) = init))),
% 238.29/238.52 inference(skolemize,[status(sab)],[18])).
% 238.29/238.52 tff(20,plain,
% 238.29/238.52 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[19, 11])).
% 238.29/238.52 tff(21,plain,
% 238.29/238.52 (![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[20, 9])).
% 238.29/238.52 tff(22,plain,
% 238.29/238.52 (((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))) | ((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))) <=> ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))) | (a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(23,plain,
% 238.29/238.52 ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))) | ((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))),
% 238.29/238.52 inference(quant_inst,[status(thm)],[])).
% 238.29/238.52 tff(24,plain,
% 238.29/238.52 ((~![C: $i] : ((a_select2(s_values7_init, C) = init) | (~leq(n0, C)) | (~leq(C, minus(pv1376, n1))))) | (a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[23, 22])).
% 238.29/238.52 tff(25,plain,
% 238.29/238.52 ($false),
% 238.29/238.52 inference(unit_resolution,[status(thm)],[24, 21, 7, 5, 3])).
% 238.29/238.52 tff(26,plain,((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))), inference(lemma,lemma(discharge,[]))).
% 238.29/238.52 tff(27,plain,
% 238.29/238.52 (leq(pv1376, n3) <=> leq(pv1376, n3)),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(28,plain,
% 238.29/238.52 (leq(pv1376, n3)),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(29,plain,
% 238.29/238.52 (leq(pv1376, n3)),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[28, 27])).
% 238.29/238.52 tff(30,plain,
% 238.29/238.52 (leq(pv20, minus(n330, n1)) <=> leq(pv20, minus(n330, n1))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(31,plain,
% 238.29/238.52 (leq(pv20, minus(n330, n1))),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(32,plain,
% 238.29/238.52 (leq(pv20, minus(n330, n1))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[31, 30])).
% 238.29/238.52 tff(33,plain,
% 238.29/238.52 (leq(pv19, minus(n410, n1)) <=> leq(pv19, minus(n410, n1))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(34,plain,
% 238.29/238.52 (leq(pv19, minus(n410, n1))),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(35,plain,
% 238.29/238.52 (leq(pv19, minus(n410, n1))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[34, 33])).
% 238.29/238.52 tff(36,plain,
% 238.29/238.52 (leq(pv7, minus(n410, n1)) <=> leq(pv7, minus(n410, n1))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(37,plain,
% 238.29/238.52 (leq(pv7, minus(n410, n1))),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(38,plain,
% 238.29/238.52 (leq(pv7, minus(n410, n1))),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[37, 36])).
% 238.29/238.52 tff(39,plain,
% 238.29/238.52 (leq(n0, pv1376) <=> leq(n0, pv1376)),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(40,plain,
% 238.29/238.52 (leq(n0, pv1376)),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(41,plain,
% 238.29/238.52 (leq(n0, pv1376)),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[40, 39])).
% 238.29/238.52 tff(42,plain,
% 238.29/238.52 (leq(n0, pv20) <=> leq(n0, pv20)),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(43,plain,
% 238.29/238.52 (leq(n0, pv20)),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(44,plain,
% 238.29/238.52 (leq(n0, pv20)),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[43, 42])).
% 238.29/238.52 tff(45,plain,
% 238.29/238.52 (leq(n0, pv19) <=> leq(n0, pv19)),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(46,plain,
% 238.29/238.52 (leq(n0, pv19)),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(47,plain,
% 238.29/238.52 (leq(n0, pv19)),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[46, 45])).
% 238.29/238.52 tff(48,plain,
% 238.29/238.52 (leq(n0, pv7) <=> leq(n0, pv7)),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(49,plain,
% 238.29/238.52 (leq(n0, pv7)),
% 238.29/238.52 inference(and_elim,[status(thm)],[16])).
% 238.29/238.52 tff(50,plain,
% 238.29/238.52 (leq(n0, pv7)),
% 238.29/238.52 inference(modus_ponens,[status(thm)],[49, 48])).
% 238.29/238.52 tff(51,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))) | (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2))))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2)))) | (~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(52,plain,
% 238.29/238.52 ((leq(n0, D!13) & leq(D!13, n2) & (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3))))) <=> (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(53,plain,
% 238.29/238.52 ((~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init))) <=> (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(54,plain,
% 238.29/238.52 ((leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) <=> (leq(n0, D!13) & leq(D!13, n2) & (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)))))),
% 238.29/238.52 inference(monotonicity,[status(thm)],[53])).
% 238.29/238.52 tff(55,plain,
% 238.29/238.52 ((leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) <=> (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2))))),
% 238.29/238.52 inference(transitivity,[status(thm)],[54, 52])).
% 238.29/238.52 tff(56,plain,
% 238.29/238.52 ((~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))) <=> (~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1)))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(57,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init))))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))) | (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2)))))),
% 238.29/238.52 inference(monotonicity,[status(thm)],[56, 55])).
% 238.29/238.52 tff(58,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init))))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((a_select3(simplex7_init, E!14, D!13) = init) | (~leq(n0, E!14)) | (~leq(E!14, n3)) | (~leq(n0, D!13)) | (~leq(D!13, n2)))) | (~((a_select2(s_values7_init, F!15) = init) | (~leq(n0, F!15)) | (~leq(F!15, minus(pv1376, n1))))))),
% 238.29/238.52 inference(transitivity,[status(thm)],[57, 51])).
% 238.29/238.52 tff(59,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init)))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(60,plain,
% 238.29/238.52 (((leq(n0, D!13) & leq(D!13, n2)) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) <=> (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init))))),
% 238.29/238.52 inference(rewrite,[status(thm)],[])).
% 238.29/238.52 tff(61,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | ((leq(n0, D!13) & leq(D!13, n2)) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init)))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))))),
% 238.29/238.52 inference(monotonicity,[status(thm)],[60])).
% 238.29/238.52 tff(62,plain,
% 238.29/238.52 (((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | ((leq(n0, D!13) & leq(D!13, n2)) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init)))) <=> ((~leq(n0, pv7)) | (~leq(n0, pv19)) | (~leq(n0, pv20)) | (~leq(n0, pv1376)) | (~leq(pv7, minus(n410, n1))) | (~leq(pv19, minus(n410, n1))) | (~leq(pv20, minus(n330, n1))) | (~leq(pv1376, n3)) | (~((~(leq(n0, F!15) & leq(F!15, minus(pv1376, n1)))) | (a_select2(s_values7_init, F!15) = init))) | (leq(n0, D!13) & leq(D!13, n2) & (~((~(leq(n0, E!14) & leq(E!14, n3))) | (a_select3(simplex7_init, E!14, D!13) = init)))))),
% 238.29/238.52 inference(transitivity,[status(thm)],[61, 59])).
% 238.29/238.52 tff(63,plain,
% 238.29/238.52 ((leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init))) <=> (leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))),
% 238.29/238.53 inference(rewrite,[status(thm)],[])).
% 238.29/238.53 tff(64,plain,
% 238.29/238.53 ((~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))) <=> (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init))))),
% 238.29/238.53 inference(monotonicity,[status(thm)],[63])).
% 238.29/238.53 tff(65,plain,
% 238.29/238.53 ((~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))) <=> (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init))))),
% 238.29/238.53 inference(rewrite,[status(thm)],[])).
% 238.29/238.53 tff(66,plain,
% 238.29/238.53 (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))),
% 238.29/238.53 inference(or_elim,[status(thm)],[15])).
% 238.29/238.53 tff(67,plain,
% 238.29/238.53 (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))),
% 238.29/238.53 inference(modus_ponens,[status(thm)],[66, 64])).
% 238.29/238.53 tff(68,plain,
% 238.29/238.53 (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))),
% 238.29/238.53 inference(modus_ponens,[status(thm)],[67, 65])).
% 238.29/238.53 tff(69,plain,
% 238.29/238.53 (~(leq(n0, pv7) & leq(n0, pv19) & leq(n0, pv20) & leq(n0, pv1376) & leq(pv7, minus(n410, n1)) & leq(pv19, minus(n410, n1)) & leq(pv20, minus(n330, n1)) & leq(pv1376, n3) & ![D: $i] : ((~(leq(n0, D) & leq(D, n2))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n3))) | (a_select3(simplex7_init, E, D) = init))) & ![F: $i] : ((~(leq(n0, F) & leq(F, minus(pv1376, n1)))) | (a_select2(s_values7_init, F) = init)))),
% 238.29/238.53 inference(modus_ponens,[status(thm)],[68, 64])).
% 238.29/238.53 unexpected number of arguments: (let ((a!1 (refl (~ (not (leq n0 pv7)) (not (leq n0 pv7)))))
% 238.29/238.53 (a!2 (refl (~ (not (leq n0 pv19)) (not (leq n0 pv19)))))
% 238.29/238.53 (a!3 (refl (~ (not (leq n0 pv20)) (not (leq n0 pv20)))))
% 238.29/238.53 (a!4 (refl (~ (not (leq n0 pv1376)) (not (leq n0 pv1376)))))
% 238.29/238.53 (a!5 (~ (not (leq pv7 (minus n410 n1))) (not (leq pv7 (minus n410 n1)))))
% 238.29/238.53 (a!6 (~ (not (leq pv19 (minus n410 n1))) (not (leq pv19 (minus n410 n1)))))
% 238.29/238.53 (a!7 (~ (not (leq pv20 (minus n330 n1))) (not (leq pv20 (minus n330 n1)))))
% 238.29/238.53 (a!8 (refl (~ (not (leq pv1376 n3)) (not (leq pv1376 n3)))))
% 238.29/238.53 (a!9 (forall ((D $i))
% 238.29/238.53 (let ((a!1 (forall ((E $i))
% 238.29/238.53 (or (not (and (leq n0 E) (leq E n3)))
% 238.29/238.53 (= (a_select3 simplex7_init E D) init)))))
% 238.29/238.53 (or (not (and (leq n0 D) (leq D n2))) a!1))))
% 238.29/238.53 (a!10 (forall ((E $i))
% 238.29/238.53 (or (not (and (leq n0 E) (leq E n3)))
% 238.29/238.53 (= (a_select3 simplex7_init E D!13) init))))
% 238.29/238.53 (a!12 (refl (~ (and (leq n0 D!13) (leq D!13 n2))
% 238.29/238.53 (and (leq n0 D!13) (leq D!13 n2)))))
% 238.29/238.53 (a!13 (or (not (and (leq n0 E!14) (leq E!14 n3)))
% 238.29/238.53 (= (a_select3 simplex7_init E!14 D!13) init)))
% 238.29/238.53 (a!17 (forall ((F $i))
% 238.29/238.53 (let ((a!1 (not (and (leq n0 F) (leq F (minus pv1376 n1))))))
% 238.29/238.53 (or a!1 (= (a_select2 s_values7_init F) init)))))
% 238.29/238.53 (a!18 (not (and (leq n0 F!15) (leq F!15 (minus pv1376 n1))))))
% 238.29/238.53 (let ((a!11 (or (not (and (leq n0 D!13) (leq D!13 n2))) a!10))
% 238.29/238.53 (a!14 (and (and (leq n0 D!13) (leq D!13 n2)) (not a!13)))
% 238.29/238.53 (a!19 (not (or a!18 (= (a_select2 s_values7_init F!15) init))))
% 238.29/238.53 (a!20 (not (and (leq n0 pv7)
% 238.29/238.53 (leq n0 pv19)
% 238.29/238.53 (leq n0 pv20)
% 238.29/238.53 (leq n0 pv1376)
% 238.29/238.53 (leq pv7 (minus n410 n1))
% 238.29/238.53 (leq pv19 (minus n410 n1))
% 238.29/238.53 (leq pv20 (minus n330 n1))
% 238.29/238.53 (leq pv1376 n3)
% 238.29/238.53 a!9
% 238.29/238.53 a!17))))
% 238.29/238.53 (let ((a!15 (nnf-neg a!12 (sk (~ (not a!10) (not a!13))) (~ (not a!11) a!14)))
% 238.29/238.53 (a!21 (or (not (leq n0 pv7))
% 238.29/238.53 (not (leq n0 pv19))
% 238.29/238.53 (not (leq n0 pv20))
% 238.29/238.53 (not (leq n0 pv1376))
% 238.29/238.53 (not (leq pv7 (minus n410 n1)))
% 238.29/238.53 (not (leq pv19 (minus n410 n1)))
% 238.29/238.53 (not (leq pv20 (minus n330 n1)))
% 238.29/238.53 (not (leq pv1376 n3))
% 238.29/238.53 a!14
% 238.29/238.53 a!19)))
% 238.29/238.53 (let ((a!16 (trans (sk (~ (not a!9) (not a!11))) a!15 (~ (not a!9) a!14))))
% 238.29/238.53 (nnf-neg a!1
% 238.29/238.53 a!2
% 238.29/238.53 a!3
% 238.29/238.53 a!4
% 238.29/238.53 (refl a!5)
% 238.29/238.53 (refl a!6)
% 238.29/238.53 (refl a!7)
% 238.29/238.53 a!8
% 238.29/238.53 a!16
% 238.29/238.53 (sk (~ (not a!17) a!19))
% 238.29/238.53 (~ a!20 a!21))))))
% 238.29/238.53 Proof display could not be completed: unexpected number of arguments
% 239.44/239.67 % E exiting
%------------------------------------------------------------------------------