%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV055+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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 13.18s 13.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWV055+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n013.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 09:26:53 EDT 2025
% 0.11/0.33 % CPUTime :
% 13.18/13.40 % SZS status Theorem
% 13.18/13.40 % SZS output start Proof
% 13.18/13.40 tff(leq_type, type, (
% 13.18/13.40 leq: ( $i * $i ) > $o)).
% 13.18/13.40 tff(tptp_minus_1_type, type, (
% 13.18/13.40 tptp_minus_1: $i)).
% 13.18/13.40 tff(tptp_fun_C_14_type, type, (
% 13.18/13.40 tptp_fun_C_14: $i)).
% 13.18/13.40 tff(minus_type, type, (
% 13.18/13.40 minus: ( $i * $i ) > $i)).
% 13.18/13.40 tff(n1_type, type, (
% 13.18/13.40 n1: $i)).
% 13.18/13.40 tff(n0_type, type, (
% 13.18/13.40 n0: $i)).
% 13.18/13.40 tff(pred_type, type, (
% 13.18/13.40 pred: $i > $i)).
% 13.18/13.40 tff(succ_type, type, (
% 13.18/13.40 succ: $i > $i)).
% 13.18/13.40 tff(divide_type, type, (
% 13.18/13.40 divide: ( $i * $i ) > $i)).
% 13.18/13.40 tff(sum_type, type, (
% 13.18/13.40 sum: ( $i * $i * $i ) > $i)).
% 13.18/13.40 tff(sqrt_type, type, (
% 13.18/13.40 sqrt: $i > $i)).
% 13.18/13.40 tff(times_type, type, (
% 13.18/13.40 times: ( $i * $i ) > $i)).
% 13.18/13.40 tff(a_select2_type, type, (
% 13.18/13.40 a_select2: ( $i * $i ) > $i)).
% 13.18/13.40 tff(pv10_type, type, (
% 13.18/13.40 pv10: $i)).
% 13.18/13.40 tff(x_type, type, (
% 13.18/13.40 x: $i)).
% 13.18/13.40 tff(a_select3_type, type, (
% 13.18/13.40 a_select3: ( $i * $i * $i ) > $i)).
% 13.18/13.40 tff(tptp_fun_D_13_type, type, (
% 13.18/13.40 tptp_fun_D_13: $i)).
% 13.18/13.40 tff(center_type, type, (
% 13.18/13.40 center: $i)).
% 13.18/13.40 tff(n5_type, type, (
% 13.18/13.40 n5: $i)).
% 13.18/13.40 tff(q_type, type, (
% 13.18/13.40 q: $i)).
% 13.18/13.40 tff(tptp_fun_E_16_type, type, (
% 13.18/13.40 tptp_fun_E_16: $i)).
% 13.18/13.40 tff(tptp_fun_F_15_type, type, (
% 13.18/13.40 tptp_fun_F_15: $i)).
% 13.18/13.40 tff(n135300_type, type, (
% 13.18/13.40 n135300: $i)).
% 13.18/13.40 tff(gt_type, type, (
% 13.18/13.40 gt: ( $i * $i ) > $o)).
% 13.18/13.40 tff(1,plain,
% 13.18/13.40 (^[X: $i] : refl((minus(X, n1) = pred(X)) <=> (minus(X, n1) = pred(X)))),
% 13.18/13.40 inference(bind,[status(th)],[])).
% 13.18/13.40 tff(2,plain,
% 13.18/13.40 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 13.18/13.40 inference(quant_intro,[status(thm)],[1])).
% 13.18/13.40 tff(3,plain,
% 13.18/13.40 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 13.18/13.40 inference(rewrite,[status(thm)],[])).
% 13.18/13.40 tff(4,axiom,(![X: $i] : (minus(X, n1) = pred(X))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','pred_minus_1')).
% 13.18/13.40 tff(5,plain,
% 13.18/13.40 (![X: $i] : (minus(X, n1) = pred(X))),
% 13.18/13.40 inference(modus_ponens,[status(thm)],[4, 3])).
% 13.18/13.40 tff(6,plain,(
% 13.18/13.40 ![X: $i] : (minus(X, n1) = pred(X))),
% 13.18/13.40 inference(skolemize,[status(sab)],[5])).
% 13.18/13.40 tff(7,plain,
% 13.18/13.40 (![X: $i] : (minus(X, n1) = pred(X))),
% 13.18/13.40 inference(modus_ponens,[status(thm)],[6, 2])).
% 13.18/13.40 tff(8,plain,
% 13.18/13.40 ((~![X: $i] : (minus(X, n1) = pred(X))) | (minus(n0, n1) = pred(n0))),
% 13.18/13.40 inference(quant_inst,[status(thm)],[])).
% 13.18/13.40 tff(9,plain,
% 13.18/13.40 (minus(n0, n1) = pred(n0)),
% 13.18/13.40 inference(unit_resolution,[status(thm)],[8, 7])).
% 13.18/13.40 tff(10,plain,
% 13.18/13.40 (pred(n0) = minus(n0, n1)),
% 13.18/13.40 inference(symmetry,[status(thm)],[9])).
% 13.18/13.40 tff(11,plain,
% 13.18/13.40 ((succ(tptp_minus_1) = n0) <=> (succ(tptp_minus_1) = n0)),
% 13.18/13.40 inference(rewrite,[status(thm)],[])).
% 13.18/13.40 tff(12,axiom,(succ(tptp_minus_1) = n0), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','succ_tptp_minus_1')).
% 13.18/13.40 tff(13,plain,
% 13.18/13.40 (succ(tptp_minus_1) = n0),
% 13.18/13.40 inference(modus_ponens,[status(thm)],[12, 11])).
% 13.18/13.40 tff(14,plain,
% 13.18/13.40 (n0 = succ(tptp_minus_1)),
% 13.18/13.40 inference(symmetry,[status(thm)],[13])).
% 13.18/13.40 tff(15,plain,
% 13.18/13.40 (pred(n0) = pred(succ(tptp_minus_1))),
% 13.18/13.40 inference(monotonicity,[status(thm)],[14])).
% 13.18/13.40 tff(16,plain,
% 13.18/13.40 (pred(succ(tptp_minus_1)) = pred(n0)),
% 13.18/13.40 inference(symmetry,[status(thm)],[15])).
% 13.18/13.40 tff(17,plain,
% 13.18/13.40 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 13.18/13.40 inference(rewrite,[status(thm)],[])).
% 13.18/13.40 tff(18,plain,
% 13.18/13.40 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 13.18/13.40 inference(rewrite,[status(thm)],[])).
% 13.18/13.40 tff(19,axiom,(![X: $i] : (pred(succ(X)) = X)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','pred_succ')).
% 13.18/13.40 tff(20,plain,
% 13.18/13.40 (![X: $i] : (pred(succ(X)) = X)),
% 13.18/13.40 inference(modus_ponens,[status(thm)],[19, 18])).
% 13.18/13.40 tff(21,plain,(
% 13.18/13.40 ![X: $i] : (pred(succ(X)) = X)),
% 13.18/13.40 inference(skolemize,[status(sab)],[20])).
% 13.18/13.40 tff(22,plain,
% 13.18/13.40 (![X: $i] : (pred(succ(X)) = X)),
% 13.18/13.40 inference(modus_ponens,[status(thm)],[21, 17])).
% 13.18/13.40 tff(23,plain,
% 13.18/13.40 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(tptp_minus_1)) = tptp_minus_1)),
% 13.18/13.40 inference(quant_inst,[status(thm)],[])).
% 13.18/13.40 tff(24,plain,
% 13.18/13.40 (pred(succ(tptp_minus_1)) = tptp_minus_1),
% 13.18/13.40 inference(unit_resolution,[status(thm)],[23, 22])).
% 13.18/13.40 tff(25,plain,
% 13.18/13.40 (tptp_minus_1 = pred(succ(tptp_minus_1))),
% 13.18/13.40 inference(symmetry,[status(thm)],[24])).
% 13.18/13.40 tff(26,plain,
% 13.18/13.40 (tptp_minus_1 = minus(n0, n1)),
% 13.24/13.40 inference(transitivity,[status(thm)],[25, 16, 10])).
% 13.24/13.40 tff(27,plain,
% 13.24/13.40 (leq(C!14, tptp_minus_1) <=> leq(C!14, minus(n0, n1))),
% 13.24/13.40 inference(monotonicity,[status(thm)],[26])).
% 13.24/13.40 tff(28,plain,
% 13.24/13.40 (leq(C!14, minus(n0, n1)) <=> leq(C!14, tptp_minus_1)),
% 13.24/13.40 inference(symmetry,[status(thm)],[27])).
% 13.24/13.40 tff(29,assumption,(~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))), introduced(assumption)).
% 13.24/13.40 tff(30,plain,
% 13.24/13.40 (((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))) | leq(E!16, minus(pv10, n1))),
% 13.24/13.40 inference(tautology,[status(thm)],[])).
% 13.24/13.40 tff(31,plain,
% 13.24/13.40 (leq(E!16, minus(pv10, n1))),
% 13.24/13.40 inference(unit_resolution,[status(thm)],[30, 29])).
% 13.24/13.40 tff(32,plain,
% 13.24/13.40 (((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))) | leq(n0, E!16)),
% 13.24/13.40 inference(tautology,[status(thm)],[])).
% 13.24/13.40 tff(33,plain,
% 13.24/13.40 (leq(n0, E!16)),
% 13.24/13.40 inference(unit_resolution,[status(thm)],[32, 29])).
% 13.24/13.40 tff(34,plain,
% 13.24/13.40 (((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))) | (~(sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1))),
% 13.24/13.40 inference(tautology,[status(thm)],[])).
% 13.24/13.40 tff(35,plain,
% 13.24/13.40 (~(sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1)),
% 13.24/13.40 inference(unit_resolution,[status(thm)],[34, 29])).
% 13.24/13.40 tff(36,plain,
% 13.24/13.40 (^[A: $i, B: $i] : refl(((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1)))) <=> ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1)))))),
% 13.24/13.40 inference(bind,[status(th)],[])).
% 13.24/13.40 tff(37,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1)))) <=> ![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))),
% 13.24/13.40 inference(quant_intro,[status(thm)],[36])).
% 13.24/13.40 tff(38,plain,
% 13.24/13.40 (^[A: $i, B: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, A) & leq(A, minus(pv10, n1))) <=> (~((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))))), ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) <=> (~(~((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))))))), rewrite((~(~((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))))) <=> ((~leq(n0, A)) | (~leq(A, minus(pv10, n1))))), ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) <=> ((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))))), (((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)) <=> (((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)))), rewrite((((~leq(n0, A)) | (~leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)) <=> ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))), (((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)) <=> ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))))),
% 13.24/13.40 inference(bind,[status(th)],[])).
% 13.24/13.40 tff(39,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)) <=> ![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))),
% 13.24/13.40 inference(quant_intro,[status(thm)],[38])).
% 13.24/13.40 tff(40,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)) <=> ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(41,plain,
% 13.24/13.40 ((~(((leq(n0, pv10) & leq(pv10, minus(n135300, n1))) & ![A: $i, B: $i] : ((leq(n0, A) & leq(A, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))) => (((leq(n0, pv10) & leq(pv10, minus(n135300, n1))) & ![C: $i, D: $i] : ((leq(n0, C) & leq(C, minus(n0, n1))) => (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10))))))))) & ![E: $i, F: $i] : ((leq(n0, E) & leq(E, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))))) <=> (~((~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)))) | (leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(42,axiom,(~(((leq(n0, pv10) & leq(pv10, minus(n135300, n1))) & ![A: $i, B: $i] : ((leq(n0, A) & leq(A, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))) => (((leq(n0, pv10) & leq(pv10, minus(n135300, n1))) & ![C: $i, D: $i] : ((leq(n0, C) & leq(C, minus(n0, n1))) => (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10))))))))) & ![E: $i, F: $i] : ((leq(n0, E) & leq(E, minus(pv10, n1))) => (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cl5_nebula_norm_0037')).
% 13.24/13.40 tff(43,plain,
% 13.24/13.40 (~((~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1)))) | (leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[42, 41])).
% 13.24/13.40 tff(44,plain,
% 13.24/13.40 (leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))),
% 13.24/13.40 inference(or_elim,[status(thm)],[43])).
% 13.24/13.40 tff(45,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))),
% 13.24/13.40 inference(and_elim,[status(thm)],[44])).
% 13.24/13.40 tff(46,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[45, 40])).
% 13.24/13.40 tff(47,plain,(
% 13.24/13.40 ![A: $i, B: $i] : ((~(leq(n0, A) & leq(A, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1))),
% 13.24/13.40 inference(skolemize,[status(sab)],[46])).
% 13.24/13.40 tff(48,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[47, 39])).
% 13.24/13.40 tff(49,plain,
% 13.24/13.40 (![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[48, 37])).
% 13.24/13.40 tff(50,plain,
% 13.24/13.40 (((~![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))) | ((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))) <=> ((~![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(51,plain,
% 13.24/13.40 ((~![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))) | ((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))),
% 13.24/13.40 inference(quant_inst,[status(thm)],[])).
% 13.24/13.40 tff(52,plain,
% 13.24/13.40 ((~![A: $i, B: $i] : ((sum(n0, minus(n5, n1), a_select3(q, A, B)) = n1) | (~leq(n0, A)) | (~leq(A, minus(pv10, n1))))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[51, 50])).
% 13.24/13.40 tff(53,plain,
% 13.24/13.40 ($false),
% 13.24/13.40 inference(unit_resolution,[status(thm)],[52, 49, 35, 33, 31])).
% 13.24/13.40 tff(54,plain,((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))), inference(lemma,lemma(discharge,[]))).
% 13.24/13.40 tff(55,plain,
% 13.24/13.40 (leq(pv10, minus(n135300, n1)) <=> leq(pv10, minus(n135300, n1))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(56,plain,
% 13.24/13.40 (leq(pv10, minus(n135300, n1))),
% 13.24/13.40 inference(and_elim,[status(thm)],[44])).
% 13.24/13.40 tff(57,plain,
% 13.24/13.40 (leq(pv10, minus(n135300, n1))),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[56, 55])).
% 13.24/13.40 tff(58,plain,
% 13.24/13.40 (leq(n0, pv10) <=> leq(n0, pv10)),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(59,plain,
% 13.24/13.40 (leq(n0, pv10)),
% 13.24/13.40 inference(and_elim,[status(thm)],[44])).
% 13.24/13.40 tff(60,plain,
% 13.24/13.40 (leq(n0, pv10)),
% 13.24/13.40 inference(modus_ponens,[status(thm)],[59, 58])).
% 13.24/13.40 tff(61,plain,
% 13.24/13.40 (((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))) | (~leq(n0, C!14)) | (~leq(C!14, minus(n0, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))))) <=> ((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))) | (~leq(n0, C!14)) | (~leq(C!14, minus(n0, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(62,plain,
% 13.24/13.40 ((~((~(leq(n0, E!16) & leq(E!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1))) <=> (~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1)))))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(63,plain,
% 13.24/13.40 ((~((~(leq(n0, C!14) & leq(C!14, minus(n0, n1)))) | (a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))))) <=> (~((a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))) | (~leq(n0, C!14)) | (~leq(C!14, minus(n0, n1)))))),
% 13.24/13.40 inference(rewrite,[status(thm)],[])).
% 13.24/13.40 tff(64,plain,
% 13.24/13.40 (((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((~(leq(n0, C!14) & leq(C!14, minus(n0, n1)))) | (a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, E!16) & leq(E!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1)))) <=> ((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))) | (~leq(n0, C!14)) | (~leq(C!14, minus(n0, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))))),
% 13.24/13.41 inference(monotonicity,[status(thm)],[63, 62])).
% 13.24/13.41 tff(65,plain,
% 13.24/13.41 (((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((~(leq(n0, C!14) & leq(C!14, minus(n0, n1)))) | (a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, E!16) & leq(E!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1)))) <=> ((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))) | (~leq(n0, C!14)) | (~leq(C!14, minus(n0, n1))))) | (~((sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1) | (~leq(n0, E!16)) | (~leq(E!16, minus(pv10, n1))))))),
% 13.24/13.41 inference(transitivity,[status(thm)],[64, 61])).
% 13.24/13.41 tff(66,plain,
% 13.24/13.41 (((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((~(leq(n0, C!14) & leq(C!14, minus(n0, n1)))) | (a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, E!16) & leq(E!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1)))) <=> ((~leq(n0, pv10)) | (~leq(pv10, minus(n135300, n1))) | (~((~(leq(n0, C!14) & leq(C!14, minus(n0, n1)))) | (a_select3(q, pv10, C!14) = divide(sqrt(times(minus(a_select3(center, C!14, n0), a_select2(x, pv10)), minus(a_select3(center, C!14, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D!13, n0), a_select2(x, pv10)), minus(a_select3(center, D!13, n0), a_select2(x, pv10))))))))) | (~((~(leq(n0, E!16) & leq(E!16, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E!16, F!15)) = n1))))),
% 13.24/13.41 inference(rewrite,[status(thm)],[])).
% 13.24/13.41 tff(67,plain,
% 13.24/13.41 ((leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))) <=> (leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))),
% 13.24/13.41 inference(rewrite,[status(thm)],[])).
% 13.24/13.41 tff(68,plain,
% 13.24/13.41 ((~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))) <=> (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))))),
% 13.24/13.41 inference(monotonicity,[status(thm)],[67])).
% 13.24/13.41 tff(69,plain,
% 13.24/13.41 ((~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))) <=> (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1))))),
% 13.24/13.41 inference(rewrite,[status(thm)],[])).
% 13.24/13.41 tff(70,plain,
% 13.24/13.41 (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))),
% 13.24/13.41 inference(or_elim,[status(thm)],[43])).
% 13.24/13.41 tff(71,plain,
% 13.24/13.41 (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))),
% 13.24/13.41 inference(modus_ponens,[status(thm)],[70, 68])).
% 13.24/13.41 tff(72,plain,
% 13.24/13.41 (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))),
% 13.24/13.41 inference(modus_ponens,[status(thm)],[71, 69])).
% 13.24/13.41 tff(73,plain,
% 13.24/13.41 (~(leq(n0, pv10) & leq(pv10, minus(n135300, n1)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(C, minus(n0, n1)))) | (a_select3(q, pv10, C) = divide(sqrt(times(minus(a_select3(center, C, n0), a_select2(x, pv10)), minus(a_select3(center, C, n0), a_select2(x, pv10)))), sum(n0, minus(n5, n1), sqrt(times(minus(a_select3(center, D, n0), a_select2(x, pv10)), minus(a_select3(center, D, n0), a_select2(x, pv10)))))))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(E, minus(pv10, n1)))) | (sum(n0, minus(n5, n1), a_select3(q, E, F)) = n1)))),
% 13.24/13.41 inference(modus_ponens,[status(thm)],[72, 68])).
% 13.24/13.41 unexpected number of arguments: (let ((a!1 (refl (~ (not (leq n0 pv10)) (not (leq n0 pv10)))))
% 13.24/13.41 (a!2 (~ (not (leq pv10 (minus n135300 n1)))
% 13.24/13.41 (not (leq pv10 (minus n135300 n1)))))
% 13.24/13.41 (a!3 (forall ((C $i) (D $i))
% 13.24/13.41 (let ((a!1 (not (and (leq n0 C) (leq C (minus n0 n1)))))
% 13.24/13.41 (a!2 (sqrt (times (minus (a_select3 center C n0)
% 13.24/13.41 (a_select2 x pv10))
% 13.24/13.41 (minus (a_select3 center C n0)
% 13.24/13.41 (a_select2 x pv10)))))
% 13.24/13.41 (a!3 (sqrt (times (minus (a_select3 center D n0)
% 13.24/13.41 (a_select2 x pv10))
% 13.24/13.41 (minus (a_select3 center D n0)
% 13.24/13.41 (a_select2 x pv10))))))
% 13.24/13.41 (let ((a!4 (= (a_select3 q pv10 C)
% 13.24/13.41 (divide a!2 (sum n0 (minus n5 n1) a!3)))))
% 13.24/13.41 (or a!1 a!4)))))
% 13.24/13.41 (a!4 (not (and (leq n0 C!14) (leq C!14 (minus n0 n1)))))
% 13.24/13.41 (a!5 (sqrt (times (minus (a_select3 center C!14 n0) (a_select2 x pv10))
% 13.24/13.41 (minus (a_select3 center C!14 n0) (a_select2 x pv10)))))
% 13.24/13.41 (a!6 (sqrt (times (minus (a_select3 center D!13 n0) (a_select2 x pv10))
% 13.24/13.41 (minus (a_select3 center D!13 n0) (a_select2 x pv10)))))
% 13.24/13.41 (a!9 (forall ((E $i) (F $i))
% 13.24/13.41 (let ((a!1 (not (and (leq n0 E) (leq E (minus pv10 n1))))))
% 13.24/13.41 (or a!1 (= (sum n0 (minus n5 n1) (a_select3 q E F)) n1)))))
% 13.24/13.41 (a!10 (not (and (leq n0 E!16) (leq E!16 (minus pv10 n1))))))
% 13.24/13.41 (let ((a!7 (= (a_select3 q pv10 C!14) (divide a!5 (sum n0 (minus n5 n1) a!6))))
% 13.24/13.41 (a!11 (or a!10 (= (sum n0 (minus n5 n1) (a_select3 q E!16 F!15)) n1)))
% 13.24/13.41 (a!12 (not (and (leq n0 pv10) (leq pv10 (minus n135300 n1)) a!3 a!9))))
% 13.24/13.41 (let ((a!8 (sk (~ (not a!3) (not (or a!4 a!7)))))
% 13.24/13.41 (a!13 (or (not (leq n0 pv10))
% 13.24/13.41 (not (leq pv10 (minus n135300 n1)))
% 13.24/13.41 (not (or a!4 a!7))
% 13.24/13.41 (not a!11))))
% 13.24/13.41 (nnf-neg a!1 (refl a!2) a!8 (sk (~ (not a!9) (not a!11))) (~ a!12 a!13)))))
% 13.24/13.41 Proof display could not be completed: unexpected number of arguments
% 13.29/13.48 % E exiting
%------------------------------------------------------------------------------