%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV117+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:32 AM UTC 2025
% Result : Theorem 84.51s 84.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SWV117+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.09/0.14 % Command : run_E %s %d THM
% 0.14/0.35 % Computer : n003.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri Jun 20 09:28:24 EDT 2025
% 0.14/0.36 % CPUTime :
% 84.51/84.71 % SZS status Theorem
% 84.51/84.71 % SZS output start Proof
% 84.51/84.71 tff(leq_type, type, (
% 84.51/84.71 leq: ( $i * $i ) > $o)).
% 84.51/84.71 tff(minus_type, type, (
% 84.51/84.71 minus: ( $i * $i ) > $i)).
% 84.51/84.71 tff(n1_type, type, (
% 84.51/84.71 n1: $i)).
% 84.51/84.71 tff(n6_type, type, (
% 84.51/84.71 n6: $i)).
% 84.51/84.71 tff(tptp_fun_J_13_type, type, (
% 84.51/84.71 tptp_fun_J_13: $i)).
% 84.51/84.71 tff(tptp_fun_I_14_type, type, (
% 84.51/84.71 tptp_fun_I_14: $i)).
% 84.51/84.71 tff(n0_type, type, (
% 84.51/84.71 n0: $i)).
% 84.51/84.71 tff(a_select3_type, type, (
% 84.51/84.71 a_select3: ( $i * $i * $i ) > $i)).
% 84.51/84.71 tff(q_ds1_filter_type, type, (
% 84.51/84.71 q_ds1_filter: $i)).
% 84.51/84.71 tff(tptp_fun_N_17_type, type, (
% 84.51/84.71 tptp_fun_N_17: $i)).
% 84.51/84.71 tff(tptp_fun_M_18_type, type, (
% 84.51/84.71 tptp_fun_M_18: $i)).
% 84.51/84.71 tff(pminus_ds1_filter_type, type, (
% 84.51/84.71 pminus_ds1_filter: $i)).
% 84.51/84.71 tff(id_ds1_filter_type, type, (
% 84.51/84.71 id_ds1_filter: $i)).
% 84.51/84.71 tff(plus_type, type, (
% 84.51/84.71 plus: ( $i * $i ) > $i)).
% 84.51/84.71 tff(r_ds1_filter_type, type, (
% 84.51/84.71 r_ds1_filter: $i)).
% 84.51/84.71 tff(n3_type, type, (
% 84.51/84.71 n3: $i)).
% 84.51/84.71 tff(n999_type, type, (
% 84.51/84.71 n999: $i)).
% 84.51/84.71 tff(pv5_type, type, (
% 84.51/84.71 pv5: $i)).
% 84.51/84.71 tff(tptp_fun_L_15_type, type, (
% 84.51/84.71 tptp_fun_L_15: $i)).
% 84.51/84.71 tff(tptp_fun_K_16_type, type, (
% 84.51/84.71 tptp_fun_K_16: $i)).
% 84.51/84.71 tff(tptp_fun_O_19_type, type, (
% 84.51/84.71 tptp_fun_O_19: $i)).
% 84.51/84.71 tff(tptp_fun_P_20_type, type, (
% 84.51/84.71 tptp_fun_P_20: $i)).
% 84.51/84.71 tff(succ_type, type, (
% 84.51/84.71 succ: $i > $i)).
% 84.51/84.71 tff(n5_type, type, (
% 84.51/84.71 n5: $i)).
% 84.51/84.71 tff(pred_type, type, (
% 84.51/84.71 pred: $i > $i)).
% 84.51/84.71 tff(1,assumption,(~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))), introduced(assumption)).
% 84.51/84.71 tff(2,plain,
% 84.51/84.71 (((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))) | leq(N!17, minus(n6, n1))),
% 84.51/84.71 inference(tautology,[status(thm)],[])).
% 84.51/84.71 tff(3,plain,
% 84.51/84.71 (leq(N!17, minus(n6, n1))),
% 84.51/84.71 inference(unit_resolution,[status(thm)],[2, 1])).
% 84.51/84.71 tff(4,plain,
% 84.51/84.71 (((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))) | leq(M!18, minus(n6, n1))),
% 84.51/84.71 inference(tautology,[status(thm)],[])).
% 84.51/84.71 tff(5,plain,
% 84.51/84.71 (leq(M!18, minus(n6, n1))),
% 84.51/84.71 inference(unit_resolution,[status(thm)],[4, 1])).
% 84.51/84.71 tff(6,plain,
% 84.51/84.71 (((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))) | leq(n0, N!17)),
% 84.51/84.71 inference(tautology,[status(thm)],[])).
% 84.51/84.71 tff(7,plain,
% 84.51/84.71 (leq(n0, N!17)),
% 84.51/84.71 inference(unit_resolution,[status(thm)],[6, 1])).
% 84.51/84.71 tff(8,plain,
% 84.51/84.71 (((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))) | leq(n0, M!18)),
% 84.51/84.71 inference(tautology,[status(thm)],[])).
% 84.51/84.71 tff(9,plain,
% 84.51/84.71 (leq(n0, M!18)),
% 84.51/84.71 inference(unit_resolution,[status(thm)],[8, 1])).
% 84.51/84.71 tff(10,plain,
% 84.51/84.71 (((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))) | (~(a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))),
% 84.51/84.71 inference(tautology,[status(thm)],[])).
% 84.51/84.71 tff(11,plain,
% 84.51/84.71 (~(a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18))),
% 84.51/84.71 inference(unit_resolution,[status(thm)],[10, 1])).
% 84.51/84.71 tff(12,plain,
% 84.51/84.71 (^[E: $i, F: $i] : refl(((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))) <=> ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))))),
% 84.51/84.71 inference(bind,[status(th)],[])).
% 84.51/84.71 tff(13,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))) <=> ![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))),
% 84.51/84.71 inference(quant_intro,[status(thm)],[12])).
% 84.51/84.71 tff(14,plain,
% 84.51/84.71 (^[E: $i, F: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1))) <=> (~((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))))), ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) <=> (~(~((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))))))), rewrite((~(~((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))))) <=> ((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))), ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) <=> ((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))))), (((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) <=> (((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))))), rewrite((((~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) <=> ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))), (((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) <=> ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))))),
% 84.51/84.71 inference(bind,[status(th)],[])).
% 84.51/84.71 tff(15,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) <=> ![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))),
% 84.51/84.71 inference(quant_intro,[status(thm)],[14])).
% 84.51/84.71 tff(16,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) <=> ![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))),
% 84.51/84.71 inference(rewrite,[status(thm)],[])).
% 84.51/84.71 tff(17,plain,
% 84.51/84.71 ((~((((((leq(n0, pv5) & leq(pv5, minus(n999, n1))) & ![A: $i, B: $i] : ((((leq(n0, A) & leq(n0, B)) & leq(A, minus(n6, n1))) & leq(B, minus(n6, n1))) => (a_select3(q_ds1_filter, A, B) = a_select3(q_ds1_filter, B, A)))) & ![C: $i, D: $i] : ((((leq(n0, C) & leq(n0, D)) & leq(C, minus(n3, n1))) & leq(D, minus(n3, n1))) => (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))) & ![E: $i, F: $i] : ((((leq(n0, E) & leq(n0, F)) & leq(E, minus(n6, n1))) & leq(F, minus(n6, n1))) => (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))) & ![G: $i] : ((leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1))) => ![H: $i] : ((leq(n0, H) & leq(H, minus(n6, n1))) => (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))) => (((((leq(n0, pv5) & leq(pv5, minus(n999, n1))) & ![I: $i, J: $i] : ((((leq(n0, I) & leq(n0, J)) & leq(I, minus(n6, n1))) & leq(J, minus(n6, n1))) => (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I)))) & ![K: $i, L: $i] : ((((leq(n0, K) & leq(n0, L)) & leq(K, minus(n3, n1))) & leq(L, minus(n3, n1))) => (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K)))) & ![M: $i, N: $i] : ((((leq(n0, M) & leq(n0, N)) & leq(M, minus(n6, n1))) & leq(N, minus(n6, n1))) => (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M)))) & ![O: $i] : ((leq(n0, O) & leq(O, minus(n6, n1))) => ![P: $i] : ((leq(n0, P) & leq(P, minus(n6, n1))) => (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))))) <=> (~((~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, minus(n6, n1)) & leq(B, minus(n6, n1)))) | (a_select3(q_ds1_filter, A, B) = a_select3(q_ds1_filter, B, A))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) & ![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))))) | (leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))))),
% 84.51/84.71 inference(rewrite,[status(thm)],[])).
% 84.51/84.71 tff(18,axiom,(~((((((leq(n0, pv5) & leq(pv5, minus(n999, n1))) & ![A: $i, B: $i] : ((((leq(n0, A) & leq(n0, B)) & leq(A, minus(n6, n1))) & leq(B, minus(n6, n1))) => (a_select3(q_ds1_filter, A, B) = a_select3(q_ds1_filter, B, A)))) & ![C: $i, D: $i] : ((((leq(n0, C) & leq(n0, D)) & leq(C, minus(n3, n1))) & leq(D, minus(n3, n1))) => (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))) & ![E: $i, F: $i] : ((((leq(n0, E) & leq(n0, F)) & leq(E, minus(n6, n1))) & leq(F, minus(n6, n1))) => (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))) & ![G: $i] : ((leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1))) => ![H: $i] : ((leq(n0, H) & leq(H, minus(n6, n1))) => (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))) => (((((leq(n0, pv5) & leq(pv5, minus(n999, n1))) & ![I: $i, J: $i] : ((((leq(n0, I) & leq(n0, J)) & leq(I, minus(n6, n1))) & leq(J, minus(n6, n1))) => (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I)))) & ![K: $i, L: $i] : ((((leq(n0, K) & leq(n0, L)) & leq(K, minus(n3, n1))) & leq(L, minus(n3, n1))) => (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K)))) & ![M: $i, N: $i] : ((((leq(n0, M) & leq(n0, N)) & leq(M, minus(n6, n1))) & leq(N, minus(n6, n1))) => (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M)))) & ![O: $i] : ((leq(n0, O) & leq(O, minus(n6, n1))) => ![P: $i] : ((leq(n0, P) & leq(P, minus(n6, n1))) => (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','quaternion_ds1_symm_0010')).
% 84.51/84.71 tff(19,plain,
% 84.51/84.71 (~((~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, minus(n6, n1)) & leq(B, minus(n6, n1)))) | (a_select3(q_ds1_filter, A, B) = a_select3(q_ds1_filter, B, A))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) & ![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))))) | (leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))))),
% 84.51/84.71 inference(modus_ponens,[status(thm)],[18, 17])).
% 84.51/84.71 tff(20,plain,
% 84.51/84.71 (leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, minus(n6, n1)) & leq(B, minus(n6, n1)))) | (a_select3(q_ds1_filter, A, B) = a_select3(q_ds1_filter, B, A))) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) & ![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E))) & ![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))),
% 84.51/84.71 inference(or_elim,[status(thm)],[19])).
% 84.51/84.71 tff(21,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))),
% 84.51/84.71 inference(and_elim,[status(thm)],[20])).
% 84.51/84.71 tff(22,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))),
% 84.51/84.71 inference(modus_ponens,[status(thm)],[21, 16])).
% 84.51/84.71 tff(23,plain,(
% 84.51/84.71 ![E: $i, F: $i] : ((~(leq(n0, E) & leq(n0, F) & leq(E, minus(n6, n1)) & leq(F, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)))),
% 84.51/84.71 inference(skolemize,[status(sab)],[22])).
% 84.51/84.71 tff(24,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))),
% 84.51/84.71 inference(modus_ponens,[status(thm)],[23, 15])).
% 84.51/84.71 tff(25,plain,
% 84.51/84.71 (![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))),
% 84.51/84.71 inference(modus_ponens,[status(thm)],[24, 13])).
% 84.51/84.71 tff(26,plain,
% 84.51/84.71 (((~![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))) | ((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))) <=> ((~![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))),
% 84.51/84.71 inference(rewrite,[status(thm)],[])).
% 84.51/84.71 tff(27,plain,
% 84.51/84.71 ((~![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))) | ((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(28,plain,
% 84.58/84.72 ((~![E: $i, F: $i] : ((a_select3(pminus_ds1_filter, E, F) = a_select3(pminus_ds1_filter, F, E)) | (~leq(n0, E)) | (~leq(n0, F)) | (~leq(E, minus(n6, n1))) | (~leq(F, minus(n6, n1))))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[27, 26])).
% 84.58/84.72 tff(29,plain,
% 84.58/84.72 ($false),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[28, 25, 11, 9, 7, 5, 3])).
% 84.58/84.72 tff(30,plain,((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))), inference(lemma,lemma(discharge,[]))).
% 84.58/84.72 tff(31,assumption,(~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))), introduced(assumption)).
% 84.58/84.72 tff(32,plain,
% 84.58/84.72 (((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))) | leq(L!15, minus(n3, n1))),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(33,plain,
% 84.58/84.72 (leq(L!15, minus(n3, n1))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[32, 31])).
% 84.58/84.72 tff(34,plain,
% 84.58/84.72 (((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))) | leq(K!16, minus(n3, n1))),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(35,plain,
% 84.58/84.72 (leq(K!16, minus(n3, n1))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[34, 31])).
% 84.58/84.72 tff(36,plain,
% 84.58/84.72 (((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))) | leq(n0, L!15)),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(37,plain,
% 84.58/84.72 (leq(n0, L!15)),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[36, 31])).
% 84.58/84.72 tff(38,plain,
% 84.58/84.72 (((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))) | leq(n0, K!16)),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(39,plain,
% 84.58/84.72 (leq(n0, K!16)),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[38, 31])).
% 84.58/84.72 tff(40,plain,
% 84.58/84.72 (((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))) | (~(a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(41,plain,
% 84.58/84.72 (~(a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[40, 31])).
% 84.58/84.72 tff(42,plain,
% 84.58/84.72 (^[C: $i, D: $i] : refl(((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))) <=> ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(43,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))) <=> ![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[42])).
% 84.58/84.72 tff(44,plain,
% 84.58/84.72 (^[C: $i, D: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1))) <=> (~((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))))), ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) <=> (~(~((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))))))), rewrite((~(~((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))))) <=> ((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))), ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) <=> ((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))))), (((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) <=> (((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))))), rewrite((((~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) <=> ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))), (((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) <=> ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(45,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) <=> ![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[44])).
% 84.58/84.72 tff(46,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C))) <=> ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(47,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))),
% 84.58/84.72 inference(and_elim,[status(thm)],[20])).
% 84.58/84.72 tff(48,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[47, 46])).
% 84.58/84.72 tff(49,plain,(
% 84.58/84.72 ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, minus(n3, n1)) & leq(D, minus(n3, n1)))) | (a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)))),
% 84.58/84.72 inference(skolemize,[status(sab)],[48])).
% 84.58/84.72 tff(50,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[49, 45])).
% 84.58/84.72 tff(51,plain,
% 84.58/84.72 (![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[50, 43])).
% 84.58/84.72 tff(52,plain,
% 84.58/84.72 (((~![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))) | ((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))) <=> ((~![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(53,plain,
% 84.58/84.72 ((~![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))) | ((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(54,plain,
% 84.58/84.72 ((~![C: $i, D: $i] : ((a_select3(r_ds1_filter, C, D) = a_select3(r_ds1_filter, D, C)) | (~leq(n0, C)) | (~leq(n0, D)) | (~leq(C, minus(n3, n1))) | (~leq(D, minus(n3, n1))))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[53, 52])).
% 84.58/84.72 tff(55,plain,
% 84.58/84.72 ($false),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[54, 51, 41, 39, 37, 35, 33])).
% 84.58/84.72 tff(56,plain,((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))), inference(lemma,lemma(discharge,[]))).
% 84.58/84.72 tff(57,plain,
% 84.58/84.72 ((succ(succ(succ(succ(succ(succ(n0)))))) = n6) <=> (succ(succ(succ(succ(succ(succ(n0)))))) = n6)),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(58,axiom,(succ(succ(succ(succ(succ(succ(n0)))))) = n6), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_6')).
% 84.58/84.72 tff(59,plain,
% 84.58/84.72 (succ(succ(succ(succ(succ(succ(n0)))))) = n6),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[58, 57])).
% 84.58/84.72 tff(60,plain,
% 84.58/84.72 ((succ(succ(succ(succ(succ(n0))))) = n5) <=> (succ(succ(succ(succ(succ(n0))))) = n5)),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(61,axiom,(succ(succ(succ(succ(succ(n0))))) = n5), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_5')).
% 84.58/84.72 tff(62,plain,
% 84.58/84.72 (succ(succ(succ(succ(succ(n0))))) = n5),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[61, 60])).
% 84.58/84.72 tff(63,plain,
% 84.58/84.72 (succ(succ(succ(succ(succ(succ(n0)))))) = succ(n5)),
% 84.58/84.72 inference(monotonicity,[status(thm)],[62])).
% 84.58/84.72 tff(64,plain,
% 84.58/84.72 (succ(n5) = succ(succ(succ(succ(succ(succ(n0))))))),
% 84.58/84.72 inference(symmetry,[status(thm)],[63])).
% 84.58/84.72 tff(65,plain,
% 84.58/84.72 (^[X: $i] : refl((plus(n1, X) = succ(X)) <=> (plus(n1, X) = succ(X)))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(66,plain,
% 84.58/84.72 (![X: $i] : (plus(n1, X) = succ(X)) <=> ![X: $i] : (plus(n1, X) = succ(X))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[65])).
% 84.58/84.72 tff(67,plain,
% 84.58/84.72 (![X: $i] : (plus(n1, X) = succ(X)) <=> ![X: $i] : (plus(n1, X) = succ(X))),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(68,axiom,(![X: $i] : (plus(n1, X) = succ(X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_1_l')).
% 84.58/84.72 tff(69,plain,
% 84.58/84.72 (![X: $i] : (plus(n1, X) = succ(X))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[68, 67])).
% 84.58/84.72 tff(70,plain,(
% 84.58/84.72 ![X: $i] : (plus(n1, X) = succ(X))),
% 84.58/84.72 inference(skolemize,[status(sab)],[69])).
% 84.58/84.72 tff(71,plain,
% 84.58/84.72 (![X: $i] : (plus(n1, X) = succ(X))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[70, 66])).
% 84.58/84.72 tff(72,plain,
% 84.58/84.72 ((~![X: $i] : (plus(n1, X) = succ(X))) | (plus(n1, n5) = succ(n5))),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(73,plain,
% 84.58/84.72 (plus(n1, n5) = succ(n5)),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[72, 71])).
% 84.58/84.72 tff(74,plain,
% 84.58/84.72 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(75,plain,
% 84.58/84.72 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(76,axiom,(![X: $i] : (pred(succ(X)) = X)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','pred_succ')).
% 84.58/84.72 tff(77,plain,
% 84.58/84.72 (![X: $i] : (pred(succ(X)) = X)),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[76, 75])).
% 84.58/84.72 tff(78,plain,(
% 84.58/84.72 ![X: $i] : (pred(succ(X)) = X)),
% 84.58/84.72 inference(skolemize,[status(sab)],[77])).
% 84.58/84.72 tff(79,plain,
% 84.58/84.72 (![X: $i] : (pred(succ(X)) = X)),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[78, 74])).
% 84.58/84.72 tff(80,plain,
% 84.58/84.72 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n5)) = n5)),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(81,plain,
% 84.58/84.72 (pred(succ(n5)) = n5),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[80, 79])).
% 84.58/84.72 tff(82,plain,
% 84.58/84.72 (^[X: $i] : refl((plus(X, n5) = succ(succ(succ(succ(succ(X)))))) <=> (plus(X, n5) = succ(succ(succ(succ(succ(X)))))))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(83,plain,
% 84.58/84.72 (![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X)))))) <=> ![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[82])).
% 84.58/84.72 tff(84,plain,
% 84.58/84.72 (![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X)))))) <=> ![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(85,axiom,(![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_5_r')).
% 84.58/84.72 tff(86,plain,
% 84.58/84.72 (![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[85, 84])).
% 84.58/84.72 tff(87,plain,(
% 84.58/84.72 ![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))),
% 84.58/84.72 inference(skolemize,[status(sab)],[86])).
% 84.58/84.72 tff(88,plain,
% 84.58/84.72 (![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[87, 83])).
% 84.58/84.72 tff(89,plain,
% 84.58/84.72 ((~![X: $i] : (plus(X, n5) = succ(succ(succ(succ(succ(X))))))) | (plus(n1, n5) = succ(succ(succ(succ(succ(n1))))))),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(90,plain,
% 84.58/84.72 (plus(n1, n5) = succ(succ(succ(succ(succ(n1)))))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[89, 88])).
% 84.58/84.72 tff(91,plain,
% 84.58/84.72 (succ(succ(succ(succ(succ(n1))))) = plus(n1, n5)),
% 84.58/84.72 inference(symmetry,[status(thm)],[90])).
% 84.58/84.72 tff(92,plain,
% 84.58/84.72 (succ(succ(succ(succ(succ(n1))))) = succ(n5)),
% 84.58/84.72 inference(transitivity,[status(thm)],[91, 73])).
% 84.58/84.72 tff(93,plain,
% 84.58/84.72 (pred(succ(succ(succ(succ(succ(n1)))))) = pred(succ(n5))),
% 84.58/84.72 inference(monotonicity,[status(thm)],[92])).
% 84.58/84.72 tff(94,plain,
% 84.58/84.72 (^[X: $i] : refl((minus(X, n1) = pred(X)) <=> (minus(X, n1) = pred(X)))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(95,plain,
% 84.58/84.72 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[94])).
% 84.58/84.72 tff(96,plain,
% 84.58/84.72 (![X: $i] : (minus(X, n1) = pred(X)) <=> ![X: $i] : (minus(X, n1) = pred(X))),
% 84.58/84.72 inference(rewrite,[status(thm)],[])).
% 84.58/84.72 tff(97,axiom,(![X: $i] : (minus(X, n1) = pred(X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','pred_minus_1')).
% 84.58/84.72 tff(98,plain,
% 84.58/84.72 (![X: $i] : (minus(X, n1) = pred(X))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[97, 96])).
% 84.58/84.72 tff(99,plain,(
% 84.58/84.72 ![X: $i] : (minus(X, n1) = pred(X))),
% 84.58/84.72 inference(skolemize,[status(sab)],[98])).
% 84.58/84.72 tff(100,plain,
% 84.58/84.72 (![X: $i] : (minus(X, n1) = pred(X))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[99, 95])).
% 84.58/84.72 tff(101,plain,
% 84.58/84.72 ((~![X: $i] : (minus(X, n1) = pred(X))) | (minus(succ(succ(succ(succ(succ(n1))))), n1) = pred(succ(succ(succ(succ(succ(n1)))))))),
% 84.58/84.72 inference(quant_inst,[status(thm)],[])).
% 84.58/84.72 tff(102,plain,
% 84.58/84.72 (minus(succ(succ(succ(succ(succ(n1))))), n1) = pred(succ(succ(succ(succ(succ(n1))))))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[101, 100])).
% 84.58/84.72 tff(103,plain,
% 84.58/84.72 (succ(n5) = plus(n1, n5)),
% 84.58/84.72 inference(symmetry,[status(thm)],[73])).
% 84.58/84.72 tff(104,plain,
% 84.58/84.72 (n6 = succ(succ(succ(succ(succ(succ(n0))))))),
% 84.58/84.72 inference(symmetry,[status(thm)],[59])).
% 84.58/84.72 tff(105,plain,
% 84.58/84.72 (n6 = succ(succ(succ(succ(succ(n1)))))),
% 84.58/84.72 inference(transitivity,[status(thm)],[104, 63, 103, 90])).
% 84.58/84.72 tff(106,plain,
% 84.58/84.72 (minus(n6, n1) = minus(succ(succ(succ(succ(succ(n1))))), n1)),
% 84.58/84.72 inference(monotonicity,[status(thm)],[105])).
% 84.58/84.72 tff(107,plain,
% 84.58/84.72 (minus(n6, n1) = n5),
% 84.58/84.72 inference(transitivity,[status(thm)],[106, 102, 93, 81])).
% 84.58/84.72 tff(108,plain,
% 84.58/84.72 (plus(n1, minus(n6, n1)) = plus(n1, n5)),
% 84.58/84.72 inference(monotonicity,[status(thm)],[107])).
% 84.58/84.72 tff(109,plain,
% 84.58/84.72 (plus(n1, minus(n6, n1)) = n6),
% 84.58/84.72 inference(transitivity,[status(thm)],[108, 73, 64, 59])).
% 84.58/84.72 tff(110,plain,
% 84.58/84.72 (minus(plus(n1, minus(n6, n1)), n1) = minus(n6, n1)),
% 84.58/84.72 inference(monotonicity,[status(thm)],[109])).
% 84.58/84.72 tff(111,plain,
% 84.58/84.72 (leq(O!19, minus(plus(n1, minus(n6, n1)), n1)) <=> leq(O!19, minus(n6, n1))),
% 84.58/84.72 inference(monotonicity,[status(thm)],[110])).
% 84.58/84.72 tff(112,plain,
% 84.58/84.72 (leq(O!19, minus(n6, n1)) <=> leq(O!19, minus(plus(n1, minus(n6, n1)), n1))),
% 84.58/84.72 inference(symmetry,[status(thm)],[111])).
% 84.58/84.72 tff(113,assumption,(~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1))))), introduced(assumption)).
% 84.58/84.72 tff(114,plain,
% 84.58/84.72 (((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))) | leq(O!19, minus(n6, n1))),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(115,plain,
% 84.58/84.72 (leq(O!19, minus(n6, n1))),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[114, 113])).
% 84.58/84.72 tff(116,plain,
% 84.58/84.72 (leq(O!19, minus(plus(n1, minus(n6, n1)), n1))),
% 84.58/84.72 inference(modus_ponens,[status(thm)],[115, 112])).
% 84.58/84.72 tff(117,plain,
% 84.58/84.72 (((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))) | leq(n0, O!19)),
% 84.58/84.72 inference(tautology,[status(thm)],[])).
% 84.58/84.72 tff(118,plain,
% 84.58/84.72 (leq(n0, O!19)),
% 84.58/84.72 inference(unit_resolution,[status(thm)],[117, 113])).
% 84.58/84.72 tff(119,plain,
% 84.58/84.72 (^[G: $i] : refl(((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(120,plain,
% 84.58/84.72 (![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[119])).
% 84.58/84.72 tff(121,plain,
% 84.58/84.72 (^[G: $i] : rewrite(((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))))),
% 84.58/84.72 inference(bind,[status(th)],[])).
% 84.58/84.72 tff(122,plain,
% 84.58/84.72 (![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.72 inference(quant_intro,[status(thm)],[121])).
% 84.58/84.72 tff(123,plain,
% 84.58/84.72 (![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.72 inference(transitivity,[status(thm)],[122, 120])).
% 84.58/84.72 tff(124,plain,
% 84.58/84.72 (^[G: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1))) <=> (~((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))))), ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) <=> (~(~((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))))))), rewrite((~(~((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))))), ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))))), quant_intro(proof_bind(^[H: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(n0, H) & leq(H, minus(n6, n1))) <=> (~((~leq(n0, H)) | (~leq(H, minus(n6, n1)))))), ((~(leq(n0, H) & leq(H, minus(n6, n1)))) <=> (~(~((~leq(n0, H)) | (~leq(H, minus(n6, n1)))))))), rewrite((~(~((~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) <=> ((~leq(n0, H)) | (~leq(H, minus(n6, n1))))), ((~(leq(n0, H) & leq(H, minus(n6, n1)))) <=> ((~leq(n0, H)) | (~leq(H, minus(n6, n1)))))), (((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))) <=> (((~leq(n0, H)) | (~leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))), rewrite((((~leq(n0, H)) | (~leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))) <=> ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))), (((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))) <=> ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))))), (![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))) <=> ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))), (((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))) <=> (((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))))), rewrite((((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))), (((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))) <=> ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))))),
% 84.58/84.73 inference(bind,[status(th)],[])).
% 84.58/84.73 tff(125,plain,
% 84.58/84.73 (![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))) <=> ![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.73 inference(quant_intro,[status(thm)],[124])).
% 84.58/84.73 tff(126,plain,
% 84.58/84.73 (![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)))) <=> ![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(127,plain,
% 84.58/84.73 (![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))),
% 84.58/84.73 inference(and_elim,[status(thm)],[20])).
% 84.58/84.73 tff(128,plain,
% 84.58/84.73 (![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[127, 126])).
% 84.58/84.73 tff(129,plain,(
% 84.58/84.73 ![G: $i] : ((~(leq(n0, G) & leq(G, minus(plus(n1, minus(n6, n1)), n1)))) | ![H: $i] : ((~(leq(n0, H) & leq(H, minus(n6, n1)))) | (a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G))))),
% 84.58/84.73 inference(skolemize,[status(sab)],[128])).
% 84.58/84.73 tff(130,plain,
% 84.58/84.73 (![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[129, 125])).
% 84.58/84.73 tff(131,plain,
% 84.58/84.73 (![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[130, 123])).
% 84.58/84.73 tff(132,plain,
% 84.58/84.73 (((~![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) | ((~leq(n0, O!19)) | (~leq(O!19, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) <=> ((~![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) | (~leq(n0, O!19)) | (~leq(O!19, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(133,plain,
% 84.58/84.73 ((~![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) | ((~leq(n0, O!19)) | (~leq(O!19, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))),
% 84.58/84.73 inference(quant_inst,[status(thm)],[])).
% 84.58/84.73 tff(134,plain,
% 84.58/84.73 ((~![G: $i] : ((~leq(n0, G)) | (~leq(G, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, G, H) = a_select3(id_ds1_filter, H, G)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1)))))) | (~leq(n0, O!19)) | (~leq(O!19, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[133, 132])).
% 84.58/84.73 tff(135,plain,
% 84.58/84.73 ((~leq(O!19, minus(plus(n1, minus(n6, n1)), n1))) | ![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[134, 131, 118])).
% 84.58/84.73 tff(136,plain,
% 84.58/84.73 (![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[135, 116])).
% 84.58/84.73 tff(137,plain,
% 84.58/84.73 (((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))) | leq(P!20, minus(n6, n1))),
% 84.58/84.73 inference(tautology,[status(thm)],[])).
% 84.58/84.73 tff(138,plain,
% 84.58/84.73 (leq(P!20, minus(n6, n1))),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[137, 113])).
% 84.58/84.73 tff(139,plain,
% 84.58/84.73 (((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))) | leq(n0, P!20)),
% 84.58/84.73 inference(tautology,[status(thm)],[])).
% 84.58/84.73 tff(140,plain,
% 84.58/84.73 (leq(n0, P!20)),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[139, 113])).
% 84.58/84.73 tff(141,plain,
% 84.58/84.73 (((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))) | (~(a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)))),
% 84.58/84.73 inference(tautology,[status(thm)],[])).
% 84.58/84.73 tff(142,plain,
% 84.58/84.73 (~(a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19))),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[141, 113])).
% 84.58/84.73 tff(143,plain,
% 84.58/84.73 (((~![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) | ((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))))) <=> ((~![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(144,plain,
% 84.58/84.73 ((~![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) | ((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))))),
% 84.58/84.73 inference(quant_inst,[status(thm)],[])).
% 84.58/84.73 tff(145,plain,
% 84.58/84.73 ((~![H: $i] : ((a_select3(id_ds1_filter, O!19, H) = a_select3(id_ds1_filter, H, O!19)) | (~leq(n0, H)) | (~leq(H, minus(n6, n1))))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1)))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[144, 143])).
% 84.58/84.73 tff(146,plain,
% 84.58/84.73 ($false),
% 84.58/84.73 inference(unit_resolution,[status(thm)],[145, 142, 140, 138, 136])).
% 84.58/84.73 tff(147,plain,((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))), inference(lemma,lemma(discharge,[]))).
% 84.58/84.73 tff(148,plain,
% 84.58/84.73 (leq(pv5, minus(n999, n1)) <=> leq(pv5, minus(n999, n1))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(149,plain,
% 84.58/84.73 (leq(pv5, minus(n999, n1))),
% 84.58/84.73 inference(and_elim,[status(thm)],[20])).
% 84.58/84.73 tff(150,plain,
% 84.58/84.73 (leq(pv5, minus(n999, n1))),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[149, 148])).
% 84.58/84.73 tff(151,plain,
% 84.58/84.73 (leq(n0, pv5) <=> leq(n0, pv5)),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(152,plain,
% 84.58/84.73 (leq(n0, pv5)),
% 84.58/84.73 inference(and_elim,[status(thm)],[20])).
% 84.58/84.73 tff(153,plain,
% 84.58/84.73 (leq(n0, pv5)),
% 84.58/84.73 inference(modus_ponens,[status(thm)],[152, 151])).
% 84.58/84.73 tff(154,plain,
% 84.58/84.73 (((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)) | (~leq(n0, I!14)) | (~leq(n0, J!13)) | (~leq(I!14, minus(n6, n1))) | (~leq(J!13, minus(n6, n1))))) | (~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))) | (~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))) | (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))))) <=> ((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1))))) | (~((a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)) | (~leq(n0, I!14)) | (~leq(n0, J!13)) | (~leq(I!14, minus(n6, n1))) | (~leq(J!13, minus(n6, n1))))) | (~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))) | (~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(155,plain,
% 84.58/84.73 ((leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1)))))) <=> (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(156,plain,
% 84.58/84.73 ((~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)))) <=> (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(157,plain,
% 84.58/84.73 ((leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19))))) <=> (leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))))))),
% 84.58/84.73 inference(monotonicity,[status(thm)],[156])).
% 84.58/84.73 tff(158,plain,
% 84.58/84.73 ((leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19))))) <=> (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1)))))),
% 84.58/84.73 inference(transitivity,[status(thm)],[157, 155])).
% 84.58/84.73 tff(159,plain,
% 84.58/84.73 ((~((~(leq(n0, M!18) & leq(n0, N!17) & leq(M!18, minus(n6, n1)) & leq(N!17, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))) <=> (~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(160,plain,
% 84.58/84.73 ((~((~(leq(n0, K!16) & leq(n0, L!15) & leq(K!16, minus(n3, n1)) & leq(L!15, minus(n3, n1)))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))) <=> (~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(161,plain,
% 84.58/84.73 ((~((~(leq(n0, I!14) & leq(n0, J!13) & leq(I!14, minus(n6, n1)) & leq(J!13, minus(n6, n1)))) | (a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)))) <=> (~((a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)) | (~leq(n0, I!14)) | (~leq(n0, J!13)) | (~leq(I!14, minus(n6, n1))) | (~leq(J!13, minus(n6, n1)))))),
% 84.58/84.73 inference(rewrite,[status(thm)],[])).
% 84.58/84.73 tff(162,plain,
% 84.58/84.73 (((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((~(leq(n0, I!14) & leq(n0, J!13) & leq(I!14, minus(n6, n1)) & leq(J!13, minus(n6, n1)))) | (a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)))) | (~((~(leq(n0, K!16) & leq(n0, L!15) & leq(K!16, minus(n3, n1)) & leq(L!15, minus(n3, n1)))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))) | (~((~(leq(n0, M!18) & leq(n0, N!17) & leq(M!18, minus(n6, n1)) & leq(N!17, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))) | (leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)))))) <=> ((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)) | (~leq(n0, I!14)) | (~leq(n0, J!13)) | (~leq(I!14, minus(n6, n1))) | (~leq(J!13, minus(n6, n1))))) | (~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))) | (~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))) | (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1))))))),
% 84.58/84.74 inference(monotonicity,[status(thm)],[161, 160, 159, 158])).
% 84.58/84.74 tff(163,plain,
% 84.58/84.74 (((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((~(leq(n0, I!14) & leq(n0, J!13) & leq(I!14, minus(n6, n1)) & leq(J!13, minus(n6, n1)))) | (a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)))) | (~((~(leq(n0, K!16) & leq(n0, L!15) & leq(K!16, minus(n3, n1)) & leq(L!15, minus(n3, n1)))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))) | (~((~(leq(n0, M!18) & leq(n0, N!17) & leq(M!18, minus(n6, n1)) & leq(N!17, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))) | (leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)))))) <=> ((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)) | (~leq(n0, P!20)) | (~leq(P!20, minus(n6, n1))) | (~leq(n0, O!19)) | (~leq(O!19, minus(n6, n1))))) | (~((a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)) | (~leq(n0, I!14)) | (~leq(n0, J!13)) | (~leq(I!14, minus(n6, n1))) | (~leq(J!13, minus(n6, n1))))) | (~((a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)) | (~leq(n0, K!16)) | (~leq(n0, L!15)) | (~leq(K!16, minus(n3, n1))) | (~leq(L!15, minus(n3, n1))))) | (~((a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)) | (~leq(n0, M!18)) | (~leq(n0, N!17)) | (~leq(M!18, minus(n6, n1))) | (~leq(N!17, minus(n6, n1))))))),
% 84.58/84.74 inference(transitivity,[status(thm)],[162, 154])).
% 84.58/84.74 tff(164,plain,
% 84.58/84.74 (((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((~(leq(n0, I!14) & leq(n0, J!13) & leq(I!14, minus(n6, n1)) & leq(J!13, minus(n6, n1)))) | (a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)))) | (~((~(leq(n0, K!16) & leq(n0, L!15) & leq(K!16, minus(n3, n1)) & leq(L!15, minus(n3, n1)))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))) | (~((~(leq(n0, M!18) & leq(n0, N!17) & leq(M!18, minus(n6, n1)) & leq(N!17, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))) | ((leq(n0, O!19) & leq(O!19, minus(n6, n1))) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19)))))) <=> ((~leq(n0, pv5)) | (~leq(pv5, minus(n999, n1))) | (~((~(leq(n0, I!14) & leq(n0, J!13) & leq(I!14, minus(n6, n1)) & leq(J!13, minus(n6, n1)))) | (a_select3(q_ds1_filter, I!14, J!13) = a_select3(q_ds1_filter, J!13, I!14)))) | (~((~(leq(n0, K!16) & leq(n0, L!15) & leq(K!16, minus(n3, n1)) & leq(L!15, minus(n3, n1)))) | (a_select3(r_ds1_filter, K!16, L!15) = a_select3(r_ds1_filter, L!15, K!16)))) | (~((~(leq(n0, M!18) & leq(n0, N!17) & leq(M!18, minus(n6, n1)) & leq(N!17, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M!18, N!17) = a_select3(pminus_ds1_filter, N!17, M!18)))) | (leq(n0, O!19) & leq(O!19, minus(n6, n1)) & (~((~(leq(n0, P!20) & leq(P!20, minus(n6, n1)))) | (a_select3(id_ds1_filter, O!19, P!20) = a_select3(id_ds1_filter, P!20, O!19))))))),
% 84.58/84.74 inference(rewrite,[status(thm)],[])).
% 84.58/84.74 tff(165,plain,
% 84.58/84.74 ((leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))) <=> (leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))),
% 84.58/84.74 inference(rewrite,[status(thm)],[])).
% 84.58/84.74 tff(166,plain,
% 84.58/84.74 ((~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))) <=> (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))))),
% 84.58/84.74 inference(monotonicity,[status(thm)],[165])).
% 84.58/84.74 tff(167,plain,
% 84.58/84.74 ((~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))) <=> (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O))))))),
% 84.58/84.75 inference(rewrite,[status(thm)],[])).
% 84.58/84.75 tff(168,plain,
% 84.58/84.75 (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))),
% 84.58/84.75 inference(or_elim,[status(thm)],[19])).
% 84.58/84.75 tff(169,plain,
% 84.58/84.75 (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))),
% 84.58/84.75 inference(modus_ponens,[status(thm)],[168, 166])).
% 84.58/84.75 tff(170,plain,
% 84.58/84.75 (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))),
% 84.58/84.75 inference(modus_ponens,[status(thm)],[169, 167])).
% 84.58/84.75 tff(171,plain,
% 84.58/84.75 (~(leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ![I: $i, J: $i] : ((~(leq(n0, I) & leq(n0, J) & leq(I, minus(n6, n1)) & leq(J, minus(n6, n1)))) | (a_select3(q_ds1_filter, I, J) = a_select3(q_ds1_filter, J, I))) & ![K: $i, L: $i] : ((~(leq(n0, K) & leq(n0, L) & leq(K, minus(n3, n1)) & leq(L, minus(n3, n1)))) | (a_select3(r_ds1_filter, K, L) = a_select3(r_ds1_filter, L, K))) & ![M: $i, N: $i] : ((~(leq(n0, M) & leq(n0, N) & leq(M, minus(n6, n1)) & leq(N, minus(n6, n1)))) | (a_select3(pminus_ds1_filter, M, N) = a_select3(pminus_ds1_filter, N, M))) & ![O: $i] : ((~(leq(n0, O) & leq(O, minus(n6, n1)))) | ![P: $i] : ((~(leq(n0, P) & leq(P, minus(n6, n1)))) | (a_select3(id_ds1_filter, O, P) = a_select3(id_ds1_filter, P, O)))))),
% 84.58/84.75 inference(modus_ponens,[status(thm)],[170, 166])).
% 84.58/84.75 unexpected number of arguments: (let ((a!1 (refl (~ (not (leq n0 pv5)) (not (leq n0 pv5)))))
% 84.58/84.75 (a!2 (~ (not (leq pv5 (minus n999 n1))) (not (leq pv5 (minus n999 n1)))))
% 84.58/84.75 (a!3 (forall ((I $i) (J $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 I)
% 84.58/84.75 (leq n0 J)
% 84.58/84.75 (leq I (minus n6 n1))
% 84.58/84.75 (leq J (minus n6 n1))))))
% 84.58/84.75 (or a!1
% 84.58/84.75 (= (a_select3 q_ds1_filter I J) (a_select3 q_ds1_filter J I))))))
% 84.58/84.75 (a!4 (not (and (leq n0 I!14)
% 84.58/84.75 (leq n0 J!13)
% 84.58/84.75 (leq I!14 (minus n6 n1))
% 84.58/84.75 (leq J!13 (minus n6 n1)))))
% 84.58/84.75 (a!6 (forall ((K $i) (L $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 K)
% 84.58/84.75 (leq n0 L)
% 84.58/84.75 (leq K (minus n3 n1))
% 84.58/84.75 (leq L (minus n3 n1))))))
% 84.58/84.75 (or a!1
% 84.58/84.75 (= (a_select3 r_ds1_filter K L) (a_select3 r_ds1_filter L K))))))
% 84.58/84.75 (a!7 (not (and (leq n0 K!16)
% 84.58/84.75 (leq n0 L!15)
% 84.58/84.75 (leq K!16 (minus n3 n1))
% 84.58/84.75 (leq L!15 (minus n3 n1)))))
% 84.58/84.75 (a!9 (forall ((M $i) (N $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 M)
% 84.58/84.75 (leq n0 N)
% 84.58/84.75 (leq M (minus n6 n1))
% 84.58/84.75 (leq N (minus n6 n1))))))
% 84.58/84.75 (or a!1
% 84.58/84.75 (= (a_select3 pminus_ds1_filter M N)
% 84.58/84.75 (a_select3 pminus_ds1_filter N M))))))
% 84.58/84.75 (a!10 (not (and (leq n0 M!18)
% 84.58/84.75 (leq n0 N!17)
% 84.58/84.75 (leq M!18 (minus n6 n1))
% 84.58/84.75 (leq N!17 (minus n6 n1)))))
% 84.58/84.75 (a!12 (forall ((O $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 O) (leq O (minus n6 n1)))))
% 84.58/84.75 (a!2 (forall ((P $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 P)
% 84.58/84.75 (leq P (minus n6 n1))))))
% 84.58/84.75 (or a!1
% 84.58/84.75 (= (a_select3 id_ds1_filter O P)
% 84.58/84.75 (a_select3 id_ds1_filter P O)))))))
% 84.58/84.75 (or a!1 a!2))))
% 84.58/84.75 (a!13 (not (and (leq n0 O!19) (leq O!19 (minus n6 n1)))))
% 84.58/84.75 (a!14 (forall ((P $i))
% 84.58/84.75 (let ((a!1 (not (and (leq n0 P) (leq P (minus n6 n1))))))
% 84.58/84.75 (or a!1
% 84.58/84.75 (= (a_select3 id_ds1_filter O!19 P)
% 84.58/84.75 (a_select3 id_ds1_filter P O!19))))))
% 84.58/84.75 (a!16 (~ (and (leq n0 O!19) (leq O!19 (minus n6 n1)))
% 84.58/84.75 (and (leq n0 O!19) (leq O!19 (minus n6 n1)))))
% 84.58/84.75 (a!17 (not (and (leq n0 P!20) (leq P!20 (minus n6 n1))))))
% 84.58/84.75 (let ((a!5 (not (or a!4
% 84.58/84.75 (= (a_select3 q_ds1_filter I!14 J!13)
% 84.58/84.75 (a_select3 q_ds1_filter J!13 I!14)))))
% 84.58/84.75 (a!8 (not (or a!7
% 84.58/84.75 (= (a_select3 r_ds1_filter K!16 L!15)
% 84.58/84.75 (a_select3 r_ds1_filter L!15 K!16)))))
% 84.58/84.75 (a!11 (not (or a!10
% 84.58/84.75 (= (a_select3 pminus_ds1_filter M!18 N!17)
% 84.58/84.75 (a_select3 pminus_ds1_filter N!17 M!18)))))
% 84.58/84.75 (a!15 (sk (~ (not a!12) (not (or a!13 a!14)))))
% 84.58/84.75 (a!18 (not (or a!17
% 84.58/84.75 (= (a_select3 id_ds1_filter O!19 P!20)
% 84.58/84.75 (a_select3 id_ds1_filter P!20 O!19)))))
% 84.58/84.75 (a!21 (not (and (leq n0 pv5) (leq pv5 (minus n999 n1)) a!3 a!6 a!9 a!12))))
% 84.58/84.75 (let ((a!19 (and (and (leq n0 O!19) (leq O!19 (minus n6 n1))) a!18)))
% 84.58/84.75 (let ((a!20 (nnf-neg (refl a!16)
% 84.58/84.75 (sk (~ (not a!14) a!18))
% 84.58/84.75 (~ (not (or a!13 a!14)) a!19)))
% 84.58/84.75 (a!22 (or (not (leq n0 pv5))
% 84.58/84.75 (not (leq pv5 (minus n999 n1)))
% 84.58/84.75 a!5
% 84.58/84.75 a!8
% 84.58/84.75 a!11
% 84.58/84.75 a!19)))
% 84.58/84.75 (nnf-neg a!1
% 84.58/84.75 (refl a!2)
% 84.58/84.75 (sk (~ (not a!3) a!5))
% 84.58/84.75 (sk (~ (not a!6) a!8))
% 84.58/84.75 (sk (~ (not a!9) a!11))
% 84.58/84.75 (trans a!15 a!20 (~ (not a!12) a!19))
% 84.58/84.75 (~ a!21 a!22))))))
% 84.58/84.75 Proof display could not be completed: unexpected number of arguments
% 84.92/85.09 % E exiting
%------------------------------------------------------------------------------