%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV053+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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:24 AM UTC 2025
% Result : Theorem 63.12s 63.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWV053+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n011.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:25:56 EDT 2025
% 0.12/0.34 % CPUTime :
% 63.12/63.30 % SZS status Theorem
% 63.12/63.30 % SZS output start Proof
% 63.12/63.30 tff(leq_type, type, (
% 63.12/63.30 leq: ( $i * $i ) > $o)).
% 63.12/63.30 tff(minus_type, type, (
% 63.12/63.30 minus: ( $i * $i ) > $i)).
% 63.12/63.30 tff(n1_type, type, (
% 63.12/63.30 n1: $i)).
% 63.12/63.30 tff(pv12_type, type, (
% 63.12/63.30 pv12: $i)).
% 63.12/63.30 tff(tptp_fun_E_14_type, type, (
% 63.12/63.30 tptp_fun_E_14: $i)).
% 63.12/63.30 tff(n0_type, type, (
% 63.12/63.30 n0: $i)).
% 63.12/63.30 tff(divide_type, type, (
% 63.12/63.30 divide: ( $i * $i ) > $i)).
% 63.12/63.30 tff(sum_type, type, (
% 63.12/63.30 sum: ( $i * $i * $i ) > $i)).
% 63.12/63.30 tff(sqrt_type, type, (
% 63.12/63.30 sqrt: $i > $i)).
% 63.12/63.30 tff(times_type, type, (
% 63.12/63.30 times: ( $i * $i ) > $i)).
% 63.12/63.30 tff(a_select2_type, type, (
% 63.12/63.30 a_select2: ( $i * $i ) > $i)).
% 63.12/63.30 tff(pv10_type, type, (
% 63.12/63.30 pv10: $i)).
% 63.12/63.30 tff(x_type, type, (
% 63.12/63.30 x: $i)).
% 63.12/63.30 tff(a_select3_type, type, (
% 63.12/63.30 a_select3: ( $i * $i * $i ) > $i)).
% 63.12/63.30 tff(tptp_fun_F_13_type, type, (
% 63.12/63.30 tptp_fun_F_13: $i)).
% 63.12/63.30 tff(center_type, type, (
% 63.12/63.30 center: $i)).
% 63.12/63.30 tff(n5_type, type, (
% 63.12/63.30 n5: $i)).
% 63.12/63.30 tff(q_type, type, (
% 63.12/63.30 q: $i)).
% 63.12/63.30 tff(tptp_fun_G_16_type, type, (
% 63.12/63.30 tptp_fun_G_16: $i)).
% 63.12/63.30 tff(tptp_fun_H_15_type, type, (
% 63.12/63.30 tptp_fun_H_15: $i)).
% 63.12/63.30 tff(n135300_type, type, (
% 63.12/63.30 n135300: $i)).
% 63.12/63.30 tff(pv71_type, type, (
% 63.12/63.30 pv71: $i)).
% 63.12/63.30 tff(tptp_minus_1_type, type, (
% 63.12/63.30 tptp_minus_1: $i)).
% 63.12/63.30 tff(pred_type, type, (
% 63.12/63.30 pred: $i > $i)).
% 63.12/63.30 tff(succ_type, type, (
% 63.12/63.30 succ: $i > $i)).
% 63.12/63.30 tff(1,assumption,(~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))), introduced(assumption)).
% 63.12/63.30 tff(2,plain,
% 63.12/63.30 (((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))) | leq(G!16, minus(pv10, n1))),
% 63.12/63.30 inference(tautology,[status(thm)],[])).
% 63.12/63.30 tff(3,plain,
% 63.12/63.30 (leq(G!16, minus(pv10, n1))),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[2, 1])).
% 63.12/63.30 tff(4,plain,
% 63.12/63.30 (((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))) | leq(n0, G!16)),
% 63.12/63.30 inference(tautology,[status(thm)],[])).
% 63.12/63.30 tff(5,plain,
% 63.12/63.30 (leq(n0, G!16)),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[4, 1])).
% 63.12/63.30 tff(6,plain,
% 63.12/63.30 (((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))) | (~(sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1))),
% 63.12/63.30 inference(tautology,[status(thm)],[])).
% 63.12/63.30 tff(7,plain,
% 63.12/63.30 (~(sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1)),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[6, 1])).
% 63.12/63.30 tff(8,plain,
% 63.12/63.30 (^[C: $i, D: $i] : refl(((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1)))) <=> ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1)))))),
% 63.12/63.30 inference(bind,[status(th)],[])).
% 63.12/63.30 tff(9,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1)))) <=> ![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))),
% 63.12/63.30 inference(quant_intro,[status(thm)],[8])).
% 63.12/63.30 tff(10,plain,
% 63.12/63.30 (^[C: $i, D: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, C) & leq(C, minus(pv10, n1))) <=> (~((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))))), ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) <=> (~(~((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))))))), rewrite((~(~((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))))) <=> ((~leq(n0, C)) | (~leq(C, minus(pv10, n1))))), ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) <=> ((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))))), (((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)) <=> (((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)))), rewrite((((~leq(n0, C)) | (~leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)) <=> ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))), (((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)) <=> ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))))),
% 63.12/63.30 inference(bind,[status(th)],[])).
% 63.12/63.30 tff(11,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)) <=> ![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))),
% 63.12/63.30 inference(quant_intro,[status(thm)],[10])).
% 63.12/63.30 tff(12,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)) <=> ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(13,plain,
% 63.12/63.30 ((~((((((leq(n0, pv10) & leq(n0, pv12)) & leq(pv10, minus(n135300, n1))) & leq(pv12, minus(n5, n1))) & ![A: $i, B: $i] : ((leq(n0, A) & leq(A, minus(pv12, n1))) => (a_select3(q, pv10, A) = divide(sqrt(times(minus(a_select3(center, A, n0), a_select2(x, pv10)), minus(a_select3(center, A, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, B, n0), a_select2(x, pv10)), minus(a_select3(center, B, n0), a_select2(x, pv10))))))))) & ![C: $i, D: $i] : ((leq(n0, C) & leq(C, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))) => (((((((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10)) & leq(n0, pv12)) & leq(pv10, minus(n135300, n1))) & leq(pv12, minus(n5, n1))) & ![E: $i, F: $i] : ((leq(n0, E) & leq(E, minus(pv12, n1))) => (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10))))))))) & ![G: $i, H: $i] : ((leq(n0, G) & leq(G, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))))) <=> (~((~(leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv12, n1)))) | (a_select3(q, pv10, A) = divide(sqrt(times(minus(a_select3(center, A, n0), a_select2(x, pv10)), minus(a_select3(center, A, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, B, n0), a_select2(x, pv10)), minus(a_select3(center, B, n0), a_select2(x, pv10)))))))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)))) | ((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(14,axiom,(~((((((leq(n0, pv10) & leq(n0, pv12)) & leq(pv10, minus(n135300, n1))) & leq(pv12, minus(n5, n1))) & ![A: $i, B: $i] : ((leq(n0, A) & leq(A, minus(pv12, n1))) => (a_select3(q, pv10, A) = divide(sqrt(times(minus(a_select3(center, A, n0), a_select2(x, pv10)), minus(a_select3(center, A, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, B, n0), a_select2(x, pv10)), minus(a_select3(center, B, n0), a_select2(x, pv10))))))))) & ![C: $i, D: $i] : ((leq(n0, C) & leq(C, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))) => (((((((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10)) & leq(n0, pv12)) & leq(pv10, minus(n135300, n1))) & leq(pv12, minus(n5, n1))) & ![E: $i, F: $i] : ((leq(n0, E) & leq(E, minus(pv12, n1))) => (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10))))))))) & ![G: $i, H: $i] : ((leq(n0, G) & leq(G, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','cl5_nebula_norm_0031')).
% 63.12/63.30 tff(15,plain,
% 63.12/63.30 (~((~(leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv12, n1)))) | (a_select3(q, pv10, A) = divide(sqrt(times(minus(a_select3(center, A, n0), a_select2(x, pv10)), minus(a_select3(center, A, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, B, n0), a_select2(x, pv10)), minus(a_select3(center, B, n0), a_select2(x, pv10)))))))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1)))) | ((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[14, 13])).
% 63.12/63.30 tff(16,plain,
% 63.12/63.30 (leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv12, n1)))) | (a_select3(q, pv10, A) = divide(sqrt(times(minus(a_select3(center, A, n0), a_select2(x, pv10)), minus(a_select3(center, A, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, B, n0), a_select2(x, pv10)), minus(a_select3(center, B, n0), a_select2(x, pv10)))))))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))),
% 63.12/63.30 inference(or_elim,[status(thm)],[15])).
% 63.12/63.30 tff(17,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))),
% 63.12/63.30 inference(and_elim,[status(thm)],[16])).
% 63.12/63.30 tff(18,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[17, 12])).
% 63.12/63.30 tff(19,plain,(
% 63.12/63.30 ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1))),
% 63.12/63.30 inference(skolemize,[status(sab)],[18])).
% 63.12/63.30 tff(20,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[19, 11])).
% 63.12/63.30 tff(21,plain,
% 63.12/63.30 (![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[20, 9])).
% 63.12/63.30 tff(22,plain,
% 63.12/63.30 (((~![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))) | ((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))) <=> ((~![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(23,plain,
% 63.12/63.30 ((~![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))) | ((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))),
% 63.12/63.30 inference(quant_inst,[status(thm)],[])).
% 63.12/63.30 tff(24,plain,
% 63.12/63.30 ((~![C: $i, D: $i] : ((sum(n0, minus(n5, n1), a_select3(q, C, D)) = n1) | (~leq(n0, C)) | (~leq(C, minus(pv10, n1))))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[23, 22])).
% 63.12/63.30 tff(25,plain,
% 63.12/63.30 ($false),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[24, 21, 7, 5, 3])).
% 63.12/63.30 tff(26,plain,((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))), inference(lemma,lemma(discharge,[]))).
% 63.12/63.30 tff(27,plain,
% 63.12/63.30 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(28,plain,
% 63.12/63.30 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(29,axiom,(![X: $i] : (pred(succ(X)) = X)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','pred_succ')).
% 63.12/63.30 tff(30,plain,
% 63.12/63.30 (![X: $i] : (pred(succ(X)) = X)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[29, 28])).
% 63.12/63.30 tff(31,plain,(
% 63.12/63.30 ![X: $i] : (pred(succ(X)) = X)),
% 63.12/63.30 inference(skolemize,[status(sab)],[30])).
% 63.12/63.30 tff(32,plain,
% 63.12/63.30 (![X: $i] : (pred(succ(X)) = X)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[31, 27])).
% 63.12/63.30 tff(33,plain,
% 63.12/63.30 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(tptp_minus_1)) = tptp_minus_1)),
% 63.12/63.30 inference(quant_inst,[status(thm)],[])).
% 63.12/63.30 tff(34,plain,
% 63.12/63.30 (pred(succ(tptp_minus_1)) = tptp_minus_1),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[33, 32])).
% 63.12/63.30 tff(35,plain,
% 63.12/63.30 ((succ(tptp_minus_1) = n0) <=> (succ(tptp_minus_1) = n0)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(36,axiom,(succ(tptp_minus_1) = n0), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_tptp_minus_1')).
% 63.12/63.30 tff(37,plain,
% 63.12/63.30 (succ(tptp_minus_1) = n0),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[36, 35])).
% 63.12/63.30 tff(38,plain,
% 63.12/63.30 (n0 = succ(tptp_minus_1)),
% 63.12/63.30 inference(symmetry,[status(thm)],[37])).
% 63.12/63.30 tff(39,plain,
% 63.12/63.30 (pred(n0) = pred(succ(tptp_minus_1))),
% 63.12/63.30 inference(monotonicity,[status(thm)],[38])).
% 63.12/63.30 tff(40,plain,
% 63.12/63.30 (^[X: $i] : refl((minus(X, n1) = pred(X)) <=> (minus(X, n1) = pred(X)))),
% 63.12/63.30 inference(bind,[status(th)],[])).
% 63.12/63.30 tff(41,plain,
% 63.12/63.30 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 63.12/63.30 inference(quant_intro,[status(thm)],[40])).
% 63.12/63.30 tff(42,plain,
% 63.12/63.30 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(43,axiom,(![X: $i] : (minus(X, n1) = pred(X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','pred_minus_1')).
% 63.12/63.30 tff(44,plain,
% 63.12/63.30 (![X: $i] : (minus(X, n1) = pred(X))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[43, 42])).
% 63.12/63.30 tff(45,plain,(
% 63.12/63.30 ![X: $i] : (minus(X, n1) = pred(X))),
% 63.12/63.30 inference(skolemize,[status(sab)],[44])).
% 63.12/63.30 tff(46,plain,
% 63.12/63.30 (![X: $i] : (minus(X, n1) = pred(X))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[45, 41])).
% 63.12/63.30 tff(47,plain,
% 63.12/63.30 ((~![X: $i] : (minus(X, n1) = pred(X))) | (minus(n0, n1) = pred(n0))),
% 63.12/63.30 inference(quant_inst,[status(thm)],[])).
% 63.12/63.30 tff(48,plain,
% 63.12/63.30 (minus(n0, n1) = pred(n0)),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[47, 46])).
% 63.12/63.30 tff(49,plain,
% 63.12/63.30 (minus(n0, n1) = tptp_minus_1),
% 63.12/63.30 inference(transitivity,[status(thm)],[48, 39, 34])).
% 63.12/63.30 tff(50,plain,
% 63.12/63.30 (sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))) = sum(n0, tptp_minus_1, sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))),
% 63.12/63.30 inference(monotonicity,[status(thm)],[49])).
% 63.12/63.30 tff(51,plain,
% 63.12/63.30 (sum(n0, tptp_minus_1, sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))) = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))),
% 63.12/63.30 inference(symmetry,[status(thm)],[50])).
% 63.12/63.30 tff(52,plain,
% 63.12/63.30 (^[Body: $i] : refl((sum(n0, tptp_minus_1, Body) = n0) <=> (sum(n0, tptp_minus_1, Body) = n0))),
% 63.12/63.30 inference(bind,[status(th)],[])).
% 63.12/63.30 tff(53,plain,
% 63.12/63.30 (![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0) <=> ![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)),
% 63.12/63.30 inference(quant_intro,[status(thm)],[52])).
% 63.12/63.30 tff(54,plain,
% 63.12/63.30 (![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0) <=> ![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(55,axiom,(![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','sum_plus_base')).
% 63.12/63.30 tff(56,plain,
% 63.12/63.30 (![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[55, 54])).
% 63.12/63.30 tff(57,plain,(
% 63.12/63.30 ![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)),
% 63.12/63.30 inference(skolemize,[status(sab)],[56])).
% 63.12/63.30 tff(58,plain,
% 63.12/63.30 (![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[57, 53])).
% 63.12/63.30 tff(59,plain,
% 63.12/63.30 ((~![Body: $i] : (sum(n0, tptp_minus_1, Body) = n0)) | (sum(n0, tptp_minus_1, sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))) = n0)),
% 63.12/63.30 inference(quant_inst,[status(thm)],[])).
% 63.12/63.30 tff(60,plain,
% 63.12/63.30 (sum(n0, tptp_minus_1, sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))) = n0),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[59, 58])).
% 63.12/63.30 tff(61,plain,
% 63.12/63.30 (n0 = sum(n0, tptp_minus_1, sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))),
% 63.12/63.30 inference(symmetry,[status(thm)],[60])).
% 63.12/63.30 tff(62,plain,
% 63.12/63.30 (n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))),
% 63.12/63.30 inference(transitivity,[status(thm)],[61, 51])).
% 63.12/63.30 tff(63,assumption,(~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))), introduced(assumption)).
% 63.12/63.30 tff(64,plain,
% 63.12/63.30 ($false),
% 63.12/63.30 inference(unit_resolution,[status(thm)],[63, 62])).
% 63.12/63.30 tff(65,plain,(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))), inference(lemma,lemma(discharge,[]))).
% 63.12/63.30 tff(66,plain,
% 63.12/63.30 (leq(pv12, minus(n5, n1)) <=> leq(pv12, minus(n5, n1))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(67,plain,
% 63.12/63.30 (leq(pv12, minus(n5, n1))),
% 63.12/63.30 inference(and_elim,[status(thm)],[16])).
% 63.12/63.30 tff(68,plain,
% 63.12/63.30 (leq(pv12, minus(n5, n1))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[67, 66])).
% 63.12/63.30 tff(69,plain,
% 63.12/63.30 (leq(pv10, minus(n135300, n1)) <=> leq(pv10, minus(n135300, n1))),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(70,plain,
% 63.12/63.30 (leq(pv10, minus(n135300, n1))),
% 63.12/63.30 inference(and_elim,[status(thm)],[16])).
% 63.12/63.30 tff(71,plain,
% 63.12/63.30 (leq(pv10, minus(n135300, n1))),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[70, 69])).
% 63.12/63.30 tff(72,plain,
% 63.12/63.30 (leq(n0, pv12) <=> leq(n0, pv12)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(73,plain,
% 63.12/63.30 (leq(n0, pv12)),
% 63.12/63.30 inference(and_elim,[status(thm)],[16])).
% 63.12/63.30 tff(74,plain,
% 63.12/63.30 (leq(n0, pv12)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[73, 72])).
% 63.12/63.30 tff(75,plain,
% 63.12/63.30 (leq(n0, pv10) <=> leq(n0, pv10)),
% 63.12/63.30 inference(rewrite,[status(thm)],[])).
% 63.12/63.30 tff(76,plain,
% 63.12/63.30 (leq(n0, pv10)),
% 63.12/63.30 inference(and_elim,[status(thm)],[16])).
% 63.12/63.30 tff(77,plain,
% 63.12/63.30 (leq(n0, pv10)),
% 63.12/63.30 inference(modus_ponens,[status(thm)],[76, 75])).
% 63.12/63.30 tff(78,plain,
% 63.12/63.30 (((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))) | (~leq(n0, E!14)) | (~leq(E!14, minus(pv12, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))))) <=> ((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))) | (~leq(n0, E!14)) | (~leq(E!14, minus(pv12, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(79,plain,
% 63.12/63.31 ((~((~(leq(n0, G!16) & leq(G!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1))) <=> (~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1)))))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(80,plain,
% 63.12/63.31 ((~((~(leq(n0, E!14) & leq(E!14, minus(pv12, n1)))) | (a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))))) <=> (~((a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))) | (~leq(n0, E!14)) | (~leq(E!14, minus(pv12, n1)))))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(81,plain,
% 63.12/63.31 (((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((~(leq(n0, E!14) & leq(E!14, minus(pv12, n1)))) | (a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, G!16) & leq(G!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1)))) <=> ((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))) | (~leq(n0, E!14)) | (~leq(E!14, minus(pv12, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))))),
% 63.12/63.31 inference(monotonicity,[status(thm)],[80, 79])).
% 63.12/63.31 tff(82,plain,
% 63.12/63.31 (((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((~(leq(n0, E!14) & leq(E!14, minus(pv12, n1)))) | (a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, G!16) & leq(G!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1)))) <=> ((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))) | (~leq(n0, E!14)) | (~leq(E!14, minus(pv12, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1) | (~leq(n0, G!16)) | (~leq(G!16, minus(pv10, n1))))))),
% 63.12/63.31 inference(transitivity,[status(thm)],[81, 78])).
% 63.12/63.31 tff(83,plain,
% 63.12/63.31 (((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((~(leq(n0, E!14) & leq(E!14, minus(pv12, n1)))) | (a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, G!16) & leq(G!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1)))) <=> ((~(n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10))))))) | (~leq(n0, pv10)) | (~leq(n0, pv12)) | (~leq(pv10, minus(n135300, n1))) | (~leq(pv12, minus(n5, n1))) | (~((~(leq(n0, E!14) & leq(E!14, minus(pv12, n1)))) | (a_select3(q, pv10, E!14) = divide(sqrt(times(minus(a_select3(center, E!14, n0), a_select2(x, pv10)), minus(a_select3(center, E!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F!13, n0), a_select2(x, pv10)), minus(a_select3(center, F!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, G!16) & leq(G!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G!16, H!15)) = n1))))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(84,plain,
% 63.12/63.31 (((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))) <=> ((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(85,plain,
% 63.12/63.31 ((~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))) <=> (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))))),
% 63.12/63.31 inference(monotonicity,[status(thm)],[84])).
% 63.12/63.31 tff(86,plain,
% 63.12/63.31 ((~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))) <=> (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1))))),
% 63.12/63.31 inference(rewrite,[status(thm)],[])).
% 63.12/63.31 tff(87,plain,
% 63.12/63.31 (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))),
% 63.12/63.31 inference(or_elim,[status(thm)],[15])).
% 63.12/63.31 tff(88,plain,
% 63.12/63.31 (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))),
% 63.12/63.32 inference(modus_ponens,[status(thm)],[87, 85])).
% 63.12/63.32 tff(89,plain,
% 63.12/63.32 (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))),
% 63.12/63.32 inference(modus_ponens,[status(thm)],[88, 86])).
% 63.12/63.32 tff(90,plain,
% 63.12/63.32 (~((n0 = sum(n0, minus(n0, n1), sqrt(times(minus(a_select3(center, pv71, n0), a_select2(x, pv10)), minus(a_select3(center, pv71, n0), a_select2(x, pv10)))))) & leq(n0, pv10) & leq(n0, pv12) & leq(pv10, minus(n135300, n1)) & leq(pv12, minus(n5, n1)) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv12, n1)))) | (a_select3(q, pv10, E) = divide(sqrt(times(minus(a_select3(center, E, n0), a_select2(x, pv10)), minus(a_select3(center, E, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, F, n0), a_select2(x, pv10)), minus(a_select3(center, F, n0), a_select2(x, pv10)))))))) & ![G: $i, H: $i] : ((~(leq(n0, G) & leq(G, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, G, H)) = n1)))),
% 63.12/63.32 inference(modus_ponens,[status(thm)],[89, 85])).
% 63.12/63.32 unexpected number of arguments: (let ((a!1 (sqrt (times (minus (a_select3 center pv71 n0) (a_select2 x pv10))
% 63.12/63.32 (minus (a_select3 center pv71 n0) (a_select2 x pv10)))))
% 63.12/63.32 (a!3 (refl (~ (not (leq n0 pv10)) (not (leq n0 pv10)))))
% 63.12/63.32 (a!4 (refl (~ (not (leq n0 pv12)) (not (leq n0 pv12)))))
% 63.12/63.32 (a!5 (~ (not (leq pv10 (minus n135300 n1)))
% 63.12/63.32 (not (leq pv10 (minus n135300 n1)))))
% 63.12/63.32 (a!6 (~ (not (leq pv12 (minus n5 n1))) (not (leq pv12 (minus n5 n1)))))
% 63.12/63.32 (a!7 (forall ((E $i) (F $i))
% 63.12/63.32 (let ((a!1 (not (and (leq n0 E) (leq E (minus pv12 n1)))))
% 63.12/63.32 (a!2 (sqrt (times (minus (a_select3 center E n0)
% 63.12/63.32 (a_select2 x pv10))
% 63.12/63.32 (minus (a_select3 center E n0)
% 63.12/63.32 (a_select2 x pv10)))))
% 63.12/63.32 (a!3 (sqrt (times (minus (a_select3 center F n0)
% 63.12/63.32 (a_select2 x pv10))
% 63.12/63.32 (minus (a_select3 center F n0)
% 63.12/63.32 (a_select2 x pv10))))))
% 63.12/63.32 (let ((a!4 (= (a_select3 q pv10 E)
% 63.12/63.32 (divide a!2 (sum n0 (minus n5 n1) a!3)))))
% 63.12/63.32 (or a!1 a!4)))))
% 63.12/63.32 (a!8 (not (and (leq n0 E!14) (leq E!14 (minus pv12 n1)))))
% 63.12/63.32 (a!9 (sqrt (times (minus (a_select3 center E!14 n0) (a_select2 x pv10))
% 63.12/63.32 (minus (a_select3 center E!14 n0) (a_select2 x pv10)))))
% 63.12/63.32 (a!10 (sqrt (times (minus (a_select3 center F!13 n0) (a_select2 x pv10))
% 63.12/63.32 (minus (a_select3 center F!13 n0) (a_select2 x pv10)))))
% 63.12/63.32 (a!13 (forall ((G $i) (H $i))
% 63.12/63.32 (let ((a!1 (not (and (leq n0 G) (leq G (minus pv10 n1))))))
% 63.12/63.32 (or a!1 (= (sum n0 (minus n5 n1) (a_select3 q G H)) n1)))))
% 63.12/63.32 (a!14 (not (and (leq n0 G!16) (leq G!16 (minus pv10 n1))))))
% 63.12/63.32 (let ((a!2 (not (= n0 (sum n0 (minus n0 n1) a!1))))
% 63.12/63.32 (a!11 (= (a_select3 q pv10 E!14) (divide a!9 (sum n0 (minus n5 n1) a!10))))
% 63.12/63.32 (a!15 (or a!14 (= (sum n0 (minus n5 n1) (a_select3 q G!16 H!15)) n1)))
% 63.12/63.32 (a!16 (and (= n0 (sum n0 (minus n0 n1) a!1))
% 63.12/63.32 (leq n0 pv10)
% 63.12/63.32 (leq n0 pv12)
% 63.12/63.32 (leq pv10 (minus n135300 n1))
% 63.12/63.32 (leq pv12 (minus n5 n1))
% 63.12/63.32 a!7
% 63.12/63.32 a!13)))
% 63.12/63.32 (let ((a!12 (sk (~ (not a!7) (not (or a!8 a!11)))))
% 63.12/63.32 (a!17 (or a!2
% 63.12/63.32 (not (leq n0 pv10))
% 63.12/63.32 (not (leq n0 pv12))
% 63.12/63.32 (not (leq pv10 (minus n135300 n1)))
% 63.12/63.32 (not (leq pv12 (minus n5 n1)))
% 63.12/63.32 (not (or a!8 a!11))
% 63.12/63.32 (not a!15))))
% 63.12/63.32 (nnf-neg (refl (~ a!2 a!2))
% 63.12/63.32 a!3
% 63.12/63.32 a!4
% 63.12/63.32 (refl a!5)
% 63.12/63.32 (refl a!6)
% 63.12/63.32 a!12
% 63.12/63.32 (sk (~ (not a!13) (not a!15)))
% 63.12/63.32 (~ (not a!16) a!17)))))
% 63.12/63.32 Proof display could not be completed: unexpected number of arguments
% 63.42/63.61 % E exiting
%------------------------------------------------------------------------------