%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV205+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.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:42 AM UTC 2025
% Result : Theorem 9.68s 9.90s
% Output : Proof 9.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWV205+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.12/0.31 % Computer : n001.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Fri Jun 20 09:35:50 EDT 2025
% 0.12/0.31 % CPUTime :
% 9.68/9.90 % SZS status Theorem
% 9.68/9.90 % SZS output start Proof
% 9.68/9.90 tff(use_type, type, (
% 9.68/9.90 use: $i)).
% 9.68/9.90 tff(a_select2_type, type, (
% 9.68/9.90 a_select2: ( $i * $i ) > $i)).
% 9.68/9.90 tff(tptp_fun_E_13_type, type, (
% 9.68/9.90 tptp_fun_E_13: $i)).
% 9.68/9.90 tff(sigma_defuse_type, type, (
% 9.68/9.90 sigma_defuse: $i)).
% 9.68/9.90 tff(n5_type, type, (
% 9.68/9.90 n5: $i)).
% 9.68/9.90 tff(a_select3_type, type, (
% 9.68/9.90 a_select3: ( $i * $i * $i ) > $i)).
% 9.68/9.90 tff(z_defuse_type, type, (
% 9.68/9.90 z_defuse: $i)).
% 9.68/9.90 tff(leq_type, type, (
% 9.68/9.90 leq: ( $i * $i ) > $o)).
% 9.68/9.90 tff(n998_type, type, (
% 9.68/9.90 n998: $i)).
% 9.68/9.90 tff(n2_type, type, (
% 9.68/9.90 n2: $i)).
% 9.68/9.90 tff(n0_type, type, (
% 9.68/9.90 n0: $i)).
% 9.68/9.90 tff(u_defuse_type, type, (
% 9.68/9.90 u_defuse: $i)).
% 9.68/9.90 tff(xinit_noise_defuse_type, type, (
% 9.68/9.90 xinit_noise_defuse: $i)).
% 9.68/9.90 tff(n4_type, type, (
% 9.68/9.90 n4: $i)).
% 9.68/9.90 tff(n3_type, type, (
% 9.68/9.90 n3: $i)).
% 9.68/9.90 tff(n1_type, type, (
% 9.68/9.90 n1: $i)).
% 9.68/9.90 tff(xinit_mean_defuse_type, type, (
% 9.68/9.90 xinit_mean_defuse: $i)).
% 9.68/9.90 tff(xinit_defuse_type, type, (
% 9.68/9.90 xinit_defuse: $i)).
% 9.68/9.90 tff(rho_defuse_type, type, (
% 9.68/9.90 rho_defuse: $i)).
% 9.68/9.90 tff(succ_type, type, (
% 9.68/9.90 succ: $i > $i)).
% 9.68/9.90 tff(pred_type, type, (
% 9.68/9.90 pred: $i > $i)).
% 9.68/9.90 tff(gt_type, type, (
% 9.68/9.90 gt: ( $i * $i ) > $o)).
% 9.68/9.90 tff(plus_type, type, (
% 9.68/9.90 plus: ( $i * $i ) > $i)).
% 9.68/9.90 tff(tptp_minus_1_type, type, (
% 9.68/9.90 tptp_minus_1: $i)).
% 9.68/9.90 tff(1,plain,
% 9.68/9.90 ((a_select2(sigma_defuse, n5) = use) <=> (a_select2(sigma_defuse, n5) = use)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(2,plain,
% 9.68/9.90 ((~((((((((((((((((((((((((((((((a_select2(rho_defuse, n0) = use) & (a_select2(rho_defuse, n1) = use)) & (a_select2(rho_defuse, n2) = use)) & (a_select2(sigma_defuse, n0) = use)) & (a_select2(sigma_defuse, n1) = use)) & (a_select2(sigma_defuse, n2) = use)) & (a_select2(sigma_defuse, n3) = use)) & (a_select2(sigma_defuse, n4) = use)) & (a_select2(sigma_defuse, n5) = use)) & (a_select3(u_defuse, n0, n0) = use)) & (a_select3(u_defuse, n1, n0) = use)) & (a_select3(u_defuse, n2, n0) = use)) & (a_select2(xinit_defuse, n3) = use)) & (a_select2(xinit_defuse, n4) = use)) & (a_select2(xinit_defuse, n5) = use)) & (a_select2(xinit_mean_defuse, n0) = use)) & (a_select2(xinit_mean_defuse, n1) = use)) & (a_select2(xinit_mean_defuse, n2) = use)) & (a_select2(xinit_mean_defuse, n3) = use)) & (a_select2(xinit_mean_defuse, n4) = use)) & (a_select2(xinit_mean_defuse, n5) = use)) & (a_select2(xinit_noise_defuse, n0) = use)) & (a_select2(xinit_noise_defuse, n1) = use)) & (a_select2(xinit_noise_defuse, n2) = use)) & (a_select2(xinit_noise_defuse, n3) = use)) & (a_select2(xinit_noise_defuse, n4) = use)) & (a_select2(xinit_noise_defuse, n5) = use)) & ![A: $i, B: $i] : ((((leq(n0, A) & leq(n0, B)) & leq(A, n2)) & leq(B, n998)) => (a_select3(u_defuse, A, B) = use))) & ![C: $i, D: $i] : ((((leq(n0, C) & leq(n0, D)) & leq(C, n2)) & leq(D, n998)) => (a_select3(z_defuse, C, D) = use))) => ![E: $i] : ((leq(n0, E) & leq(E, n5)) => (a_select2(sigma_defuse, E) = use)))) <=> (~((~((a_select2(rho_defuse, n0) = use) & (a_select2(rho_defuse, n1) = use) & (a_select2(rho_defuse, n2) = use) & (a_select2(sigma_defuse, n0) = use) & (a_select2(sigma_defuse, n1) = use) & (a_select2(sigma_defuse, n2) = use) & (a_select2(sigma_defuse, n3) = use) & (a_select2(sigma_defuse, n4) = use) & (a_select2(sigma_defuse, n5) = use) & (a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(xinit_defuse, n3) = use) & (a_select2(xinit_defuse, n4) = use) & (a_select2(xinit_defuse, n5) = use) & (a_select2(xinit_mean_defuse, n0) = use) & (a_select2(xinit_mean_defuse, n1) = use) & (a_select2(xinit_mean_defuse, n2) = use) & (a_select2(xinit_mean_defuse, n3) = use) & (a_select2(xinit_mean_defuse, n4) = use) & (a_select2(xinit_mean_defuse, n5) = use) & (a_select2(xinit_noise_defuse, n0) = use) & (a_select2(xinit_noise_defuse, n1) = use) & (a_select2(xinit_noise_defuse, n2) = use) & (a_select2(xinit_noise_defuse, n3) = use) & (a_select2(xinit_noise_defuse, n4) = use) & (a_select2(xinit_noise_defuse, n5) = use) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, n2) & leq(B, n998))) | (a_select3(u_defuse, A, B) = use)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, n2) & leq(D, n998))) | (a_select3(z_defuse, C, D) = use)))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(3,axiom,(~((((((((((((((((((((((((((((((a_select2(rho_defuse, n0) = use) & (a_select2(rho_defuse, n1) = use)) & (a_select2(rho_defuse, n2) = use)) & (a_select2(sigma_defuse, n0) = use)) & (a_select2(sigma_defuse, n1) = use)) & (a_select2(sigma_defuse, n2) = use)) & (a_select2(sigma_defuse, n3) = use)) & (a_select2(sigma_defuse, n4) = use)) & (a_select2(sigma_defuse, n5) = use)) & (a_select3(u_defuse, n0, n0) = use)) & (a_select3(u_defuse, n1, n0) = use)) & (a_select3(u_defuse, n2, n0) = use)) & (a_select2(xinit_defuse, n3) = use)) & (a_select2(xinit_defuse, n4) = use)) & (a_select2(xinit_defuse, n5) = use)) & (a_select2(xinit_mean_defuse, n0) = use)) & (a_select2(xinit_mean_defuse, n1) = use)) & (a_select2(xinit_mean_defuse, n2) = use)) & (a_select2(xinit_mean_defuse, n3) = use)) & (a_select2(xinit_mean_defuse, n4) = use)) & (a_select2(xinit_mean_defuse, n5) = use)) & (a_select2(xinit_noise_defuse, n0) = use)) & (a_select2(xinit_noise_defuse, n1) = use)) & (a_select2(xinit_noise_defuse, n2) = use)) & (a_select2(xinit_noise_defuse, n3) = use)) & (a_select2(xinit_noise_defuse, n4) = use)) & (a_select2(xinit_noise_defuse, n5) = use)) & ![A: $i, B: $i] : ((((leq(n0, A) & leq(n0, B)) & leq(A, n2)) & leq(B, n998)) => (a_select3(u_defuse, A, B) = use))) & ![C: $i, D: $i] : ((((leq(n0, C) & leq(n0, D)) & leq(C, n2)) & leq(D, n998)) => (a_select3(z_defuse, C, D) = use))) => ![E: $i] : ((leq(n0, E) & leq(E, n5)) => (a_select2(sigma_defuse, E) = use)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','quaternion_ds1_inuse_0016')).
% 9.68/9.90 tff(4,plain,
% 9.68/9.90 (~((~((a_select2(rho_defuse, n0) = use) & (a_select2(rho_defuse, n1) = use) & (a_select2(rho_defuse, n2) = use) & (a_select2(sigma_defuse, n0) = use) & (a_select2(sigma_defuse, n1) = use) & (a_select2(sigma_defuse, n2) = use) & (a_select2(sigma_defuse, n3) = use) & (a_select2(sigma_defuse, n4) = use) & (a_select2(sigma_defuse, n5) = use) & (a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(xinit_defuse, n3) = use) & (a_select2(xinit_defuse, n4) = use) & (a_select2(xinit_defuse, n5) = use) & (a_select2(xinit_mean_defuse, n0) = use) & (a_select2(xinit_mean_defuse, n1) = use) & (a_select2(xinit_mean_defuse, n2) = use) & (a_select2(xinit_mean_defuse, n3) = use) & (a_select2(xinit_mean_defuse, n4) = use) & (a_select2(xinit_mean_defuse, n5) = use) & (a_select2(xinit_noise_defuse, n0) = use) & (a_select2(xinit_noise_defuse, n1) = use) & (a_select2(xinit_noise_defuse, n2) = use) & (a_select2(xinit_noise_defuse, n3) = use) & (a_select2(xinit_noise_defuse, n4) = use) & (a_select2(xinit_noise_defuse, n5) = use) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, n2) & leq(B, n998))) | (a_select3(u_defuse, A, B) = use)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, n2) & leq(D, n998))) | (a_select3(z_defuse, C, D) = use)))) | ![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use)))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[3, 2])).
% 9.68/9.90 tff(5,plain,
% 9.68/9.90 ((a_select2(rho_defuse, n0) = use) & (a_select2(rho_defuse, n1) = use) & (a_select2(rho_defuse, n2) = use) & (a_select2(sigma_defuse, n0) = use) & (a_select2(sigma_defuse, n1) = use) & (a_select2(sigma_defuse, n2) = use) & (a_select2(sigma_defuse, n3) = use) & (a_select2(sigma_defuse, n4) = use) & (a_select2(sigma_defuse, n5) = use) & (a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(xinit_defuse, n3) = use) & (a_select2(xinit_defuse, n4) = use) & (a_select2(xinit_defuse, n5) = use) & (a_select2(xinit_mean_defuse, n0) = use) & (a_select2(xinit_mean_defuse, n1) = use) & (a_select2(xinit_mean_defuse, n2) = use) & (a_select2(xinit_mean_defuse, n3) = use) & (a_select2(xinit_mean_defuse, n4) = use) & (a_select2(xinit_mean_defuse, n5) = use) & (a_select2(xinit_noise_defuse, n0) = use) & (a_select2(xinit_noise_defuse, n1) = use) & (a_select2(xinit_noise_defuse, n2) = use) & (a_select2(xinit_noise_defuse, n3) = use) & (a_select2(xinit_noise_defuse, n4) = use) & (a_select2(xinit_noise_defuse, n5) = use) & ![A: $i, B: $i] : ((~(leq(n0, A) & leq(n0, B) & leq(A, n2) & leq(B, n998))) | (a_select3(u_defuse, A, B) = use)) & ![C: $i, D: $i] : ((~(leq(n0, C) & leq(n0, D) & leq(C, n2) & leq(D, n998))) | (a_select3(z_defuse, C, D) = use))),
% 9.68/9.90 inference(or_elim,[status(thm)],[4])).
% 9.68/9.90 tff(6,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n5) = use),
% 9.68/9.90 inference(and_elim,[status(thm)],[5])).
% 9.68/9.90 tff(7,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n5) = use),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[6, 1])).
% 9.68/9.90 tff(8,plain,
% 9.68/9.90 ((succ(succ(succ(succ(succ(n0))))) = n5) <=> (succ(succ(succ(succ(succ(n0))))) = n5)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(9,axiom,(succ(succ(succ(succ(succ(n0))))) = n5), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_5')).
% 9.68/9.90 tff(10,plain,
% 9.68/9.90 (succ(succ(succ(succ(succ(n0))))) = n5),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[9, 8])).
% 9.68/9.90 tff(11,plain,
% 9.68/9.90 ((succ(succ(succ(succ(n0)))) = n4) <=> (succ(succ(succ(succ(n0)))) = n4)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(12,axiom,(succ(succ(succ(succ(n0)))) = n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_4')).
% 9.68/9.90 tff(13,plain,
% 9.68/9.90 (succ(succ(succ(succ(n0)))) = n4),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[12, 11])).
% 9.68/9.90 tff(14,plain,
% 9.68/9.90 (n4 = succ(succ(succ(succ(n0))))),
% 9.68/9.90 inference(symmetry,[status(thm)],[13])).
% 9.68/9.90 tff(15,plain,
% 9.68/9.90 ((a_select2(sigma_defuse, n4) = use) <=> (a_select2(sigma_defuse, n4) = use)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(16,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n4) = use),
% 9.68/9.90 inference(and_elim,[status(thm)],[5])).
% 9.68/9.90 tff(17,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n4) = use),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[16, 15])).
% 9.68/9.90 tff(18,assumption,(n4 = E!13), introduced(assumption)).
% 9.68/9.90 tff(19,plain,
% 9.68/9.90 (E!13 = n4),
% 9.68/9.90 inference(symmetry,[status(thm)],[18])).
% 9.68/9.90 tff(20,plain,
% 9.68/9.90 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n4)),
% 9.68/9.90 inference(monotonicity,[status(thm)],[19])).
% 9.68/9.90 tff(21,plain,
% 9.68/9.90 (a_select2(sigma_defuse, E!13) = use),
% 9.68/9.90 inference(transitivity,[status(thm)],[20, 17])).
% 9.68/9.90 tff(22,plain,
% 9.68/9.90 ((~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))) <=> (~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use)))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(23,plain,
% 9.68/9.90 (~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))),
% 9.68/9.90 inference(or_elim,[status(thm)],[4])).
% 9.68/9.90 tff(24,plain,
% 9.68/9.90 (~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[23, 22])).
% 9.68/9.90 tff(25,plain,
% 9.68/9.90 (~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[24, 22])).
% 9.68/9.90 tff(26,plain,
% 9.68/9.90 (~![E: $i] : ((~(leq(n0, E) & leq(E, n5))) | (a_select2(sigma_defuse, E) = use))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[25, 22])).
% 9.68/9.90 tff(27,plain,(
% 9.68/9.90 ~((~(leq(n0, E!13) & leq(E!13, n5))) | (a_select2(sigma_defuse, E!13) = use))),
% 9.68/9.90 inference(skolemize,[status(sab)],[26])).
% 9.68/9.90 tff(28,plain,
% 9.68/9.90 (~(a_select2(sigma_defuse, E!13) = use)),
% 9.68/9.90 inference(or_elim,[status(thm)],[27])).
% 9.68/9.90 tff(29,plain,
% 9.68/9.90 ($false),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[28, 21])).
% 9.68/9.90 tff(30,plain,(~(n4 = E!13)), inference(lemma,lemma(discharge,[]))).
% 9.68/9.90 tff(31,plain,
% 9.68/9.90 (![X: $i] : (succ(pred(X)) = X) <=> ![X: $i] : (succ(pred(X)) = X)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(32,plain,
% 9.68/9.90 (![X: $i] : (succ(pred(X)) = X) <=> ![X: $i] : (succ(pred(X)) = X)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(33,axiom,(![X: $i] : (succ(pred(X)) = X)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_pred')).
% 9.68/9.90 tff(34,plain,
% 9.68/9.90 (![X: $i] : (succ(pred(X)) = X)),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[33, 32])).
% 9.68/9.90 tff(35,plain,(
% 9.68/9.90 ![X: $i] : (succ(pred(X)) = X)),
% 9.68/9.90 inference(skolemize,[status(sab)],[34])).
% 9.68/9.90 tff(36,plain,
% 9.68/9.90 (![X: $i] : (succ(pred(X)) = X)),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[35, 31])).
% 9.68/9.90 tff(37,plain,
% 9.68/9.90 ((~![X: $i] : (succ(pred(X)) = X)) | (succ(pred(E!13)) = E!13)),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(38,plain,
% 9.68/9.90 (succ(pred(E!13)) = E!13),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[37, 36])).
% 9.68/9.90 tff(39,plain,
% 9.68/9.90 ((succ(succ(succ(n0))) = n3) <=> (succ(succ(succ(n0))) = n3)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(40,axiom,(succ(succ(succ(n0))) = n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_3')).
% 9.68/9.90 tff(41,plain,
% 9.68/9.90 (succ(succ(succ(n0))) = n3),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[40, 39])).
% 9.68/9.90 tff(42,plain,
% 9.68/9.90 (n3 = succ(succ(succ(n0)))),
% 9.68/9.90 inference(symmetry,[status(thm)],[41])).
% 9.68/9.90 tff(43,plain,
% 9.68/9.90 (succ(n3) = succ(succ(succ(succ(n0))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[42])).
% 9.68/9.90 tff(44,plain,
% 9.68/9.90 (succ(n3) = n4),
% 9.68/9.90 inference(transitivity,[status(thm)],[43, 13])).
% 9.68/9.90 tff(45,plain,
% 9.68/9.90 (leq(succ(n3), succ(pred(E!13))) <=> leq(n4, E!13)),
% 9.68/9.90 inference(monotonicity,[status(thm)],[44, 38])).
% 9.68/9.90 tff(46,plain,
% 9.68/9.90 ((a_select2(sigma_defuse, n3) = use) <=> (a_select2(sigma_defuse, n3) = use)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(47,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n3) = use),
% 9.68/9.90 inference(and_elim,[status(thm)],[5])).
% 9.68/9.90 tff(48,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n3) = use),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[47, 46])).
% 9.68/9.90 tff(49,assumption,(n3 = E!13), introduced(assumption)).
% 9.68/9.90 tff(50,plain,
% 9.68/9.90 (E!13 = n3),
% 9.68/9.90 inference(symmetry,[status(thm)],[49])).
% 9.68/9.90 tff(51,plain,
% 9.68/9.90 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n3)),
% 9.68/9.90 inference(monotonicity,[status(thm)],[50])).
% 9.68/9.90 tff(52,plain,
% 9.68/9.90 (a_select2(sigma_defuse, E!13) = use),
% 9.68/9.90 inference(transitivity,[status(thm)],[51, 48])).
% 9.68/9.90 tff(53,plain,
% 9.68/9.90 ($false),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[28, 52])).
% 9.68/9.90 tff(54,plain,(~(n3 = E!13)), inference(lemma,lemma(discharge,[]))).
% 9.68/9.90 tff(55,plain,
% 9.68/9.90 (leq(succ(n3), succ(succ(E!13))) <=> leq(n4, succ(succ(E!13)))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[44])).
% 9.68/9.90 tff(56,plain,
% 9.68/9.90 (leq(n4, succ(succ(E!13))) <=> leq(succ(n3), succ(succ(E!13)))),
% 9.68/9.90 inference(symmetry,[status(thm)],[55])).
% 9.68/9.90 tff(57,plain,
% 9.68/9.90 (succ(n4) = succ(succ(succ(succ(succ(n0)))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[14])).
% 9.68/9.90 tff(58,plain,
% 9.68/9.90 (succ(n4) = n5),
% 9.68/9.90 inference(transitivity,[status(thm)],[57, 10])).
% 9.68/9.90 tff(59,plain,
% 9.68/9.90 (leq(succ(n4), succ(succ(succ(E!13)))) <=> leq(n5, succ(succ(succ(E!13))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[58])).
% 9.68/9.90 tff(60,plain,
% 9.68/9.90 (leq(n5, succ(succ(succ(E!13)))) <=> leq(succ(n4), succ(succ(succ(E!13))))),
% 9.68/9.90 inference(symmetry,[status(thm)],[59])).
% 9.68/9.90 tff(61,plain,
% 9.68/9.90 (^[X: $i] : refl((plus(X, n4) = succ(succ(succ(succ(X))))) <=> (plus(X, n4) = succ(succ(succ(succ(X))))))),
% 9.68/9.90 inference(bind,[status(th)],[])).
% 9.68/9.90 tff(62,plain,
% 9.68/9.90 (![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X))))) <=> ![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))),
% 9.68/9.90 inference(quant_intro,[status(thm)],[61])).
% 9.68/9.90 tff(63,plain,
% 9.68/9.90 (![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X))))) <=> ![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(64,axiom,(![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_4_r')).
% 9.68/9.90 tff(65,plain,
% 9.68/9.90 (![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[64, 63])).
% 9.68/9.90 tff(66,plain,(
% 9.68/9.90 ![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))),
% 9.68/9.90 inference(skolemize,[status(sab)],[65])).
% 9.68/9.90 tff(67,plain,
% 9.68/9.90 (![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[66, 62])).
% 9.68/9.90 tff(68,plain,
% 9.68/9.90 ((~![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))) | (plus(n2, n4) = succ(succ(succ(succ(n2)))))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(69,plain,
% 9.68/9.90 (plus(n2, n4) = succ(succ(succ(succ(n2))))),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[68, 67])).
% 9.68/9.90 tff(70,plain,
% 9.68/9.90 (^[X: $i] : refl((plus(n2, X) = succ(succ(X))) <=> (plus(n2, X) = succ(succ(X))))),
% 9.68/9.90 inference(bind,[status(th)],[])).
% 9.68/9.90 tff(71,plain,
% 9.68/9.90 (![X: $i] : (plus(n2, X) = succ(succ(X))) <=> ![X: $i] : (plus(n2, X) = succ(succ(X)))),
% 9.68/9.90 inference(quant_intro,[status(thm)],[70])).
% 9.68/9.90 tff(72,plain,
% 9.68/9.90 (![X: $i] : (plus(n2, X) = succ(succ(X))) <=> ![X: $i] : (plus(n2, X) = succ(succ(X)))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(73,axiom,(![X: $i] : (plus(n2, X) = succ(succ(X)))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_2_l')).
% 9.68/9.90 tff(74,plain,
% 9.68/9.90 (![X: $i] : (plus(n2, X) = succ(succ(X)))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[73, 72])).
% 9.68/9.90 tff(75,plain,(
% 9.68/9.90 ![X: $i] : (plus(n2, X) = succ(succ(X)))),
% 9.68/9.90 inference(skolemize,[status(sab)],[74])).
% 9.68/9.90 tff(76,plain,
% 9.68/9.90 (![X: $i] : (plus(n2, X) = succ(succ(X)))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[75, 71])).
% 9.68/9.90 tff(77,plain,
% 9.68/9.90 ((~![X: $i] : (plus(n2, X) = succ(succ(X)))) | (plus(n2, n4) = succ(succ(n4)))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(78,plain,
% 9.68/9.90 (plus(n2, n4) = succ(succ(n4))),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[77, 76])).
% 9.68/9.90 tff(79,plain,
% 9.68/9.90 (succ(succ(n4)) = plus(n2, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[78])).
% 9.68/9.90 tff(80,plain,
% 9.68/9.90 (^[X: $i] : refl((plus(n1, X) = succ(X)) <=> (plus(n1, X) = succ(X)))),
% 9.68/9.90 inference(bind,[status(th)],[])).
% 9.68/9.90 tff(81,plain,
% 9.68/9.90 (![X: $i] : (plus(n1, X) = succ(X)) <=> ![X: $i] : (plus(n1, X) = succ(X))),
% 9.68/9.90 inference(quant_intro,[status(thm)],[80])).
% 9.68/9.90 tff(82,plain,
% 9.68/9.90 (![X: $i] : (plus(n1, X) = succ(X)) <=> ![X: $i] : (plus(n1, X) = succ(X))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(83,axiom,(![X: $i] : (plus(n1, X) = succ(X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_1_l')).
% 9.68/9.90 tff(84,plain,
% 9.68/9.90 (![X: $i] : (plus(n1, X) = succ(X))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[83, 82])).
% 9.68/9.90 tff(85,plain,(
% 9.68/9.90 ![X: $i] : (plus(n1, X) = succ(X))),
% 9.68/9.90 inference(skolemize,[status(sab)],[84])).
% 9.68/9.90 tff(86,plain,
% 9.68/9.90 (![X: $i] : (plus(n1, X) = succ(X))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[85, 81])).
% 9.68/9.90 tff(87,plain,
% 9.68/9.90 ((~![X: $i] : (plus(n1, X) = succ(X))) | (plus(n1, n4) = succ(n4))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(88,plain,
% 9.68/9.90 (plus(n1, n4) = succ(n4)),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[87, 86])).
% 9.68/9.90 tff(89,plain,
% 9.68/9.90 ((~![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))) | (plus(n1, n4) = succ(succ(succ(succ(n1)))))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(90,plain,
% 9.68/9.90 (plus(n1, n4) = succ(succ(succ(succ(n1))))),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[89, 67])).
% 9.68/9.90 tff(91,plain,
% 9.68/9.90 (succ(succ(succ(succ(n1)))) = plus(n1, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[90])).
% 9.68/9.90 tff(92,plain,
% 9.68/9.90 (succ(succ(succ(succ(n1)))) = succ(n4)),
% 9.68/9.90 inference(transitivity,[status(thm)],[91, 88])).
% 9.68/9.90 tff(93,plain,
% 9.68/9.90 (succ(succ(succ(succ(succ(n1))))) = succ(succ(n4))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[92])).
% 9.68/9.90 tff(94,plain,
% 9.68/9.90 (succ(n4) = plus(n1, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[88])).
% 9.68/9.90 tff(95,plain,
% 9.68/9.90 (succ(succ(succ(succ(succ(n0))))) = succ(n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[57])).
% 9.68/9.90 tff(96,plain,
% 9.68/9.90 (n5 = succ(succ(succ(succ(succ(n0)))))),
% 9.68/9.90 inference(symmetry,[status(thm)],[10])).
% 9.68/9.90 tff(97,plain,
% 9.68/9.90 (n5 = succ(succ(succ(succ(n1))))),
% 9.68/9.90 inference(transitivity,[status(thm)],[96, 95, 94, 90])).
% 9.68/9.90 tff(98,plain,
% 9.68/9.90 (succ(n5) = succ(succ(succ(succ(succ(n1)))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[97])).
% 9.68/9.90 tff(99,plain,
% 9.68/9.90 (succ(n5) = succ(succ(succ(succ(n2))))),
% 9.68/9.90 inference(transitivity,[status(thm)],[98, 93, 79, 69])).
% 9.68/9.90 tff(100,plain,
% 9.68/9.90 (leq(succ(n5), succ(succ(succ(succ(E!13))))) <=> leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13)))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[99])).
% 9.68/9.90 tff(101,plain,
% 9.68/9.90 (leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13))))) <=> leq(succ(n5), succ(succ(succ(succ(E!13)))))),
% 9.68/9.90 inference(symmetry,[status(thm)],[100])).
% 9.68/9.90 tff(102,plain,
% 9.68/9.90 (succ(succ(succ(succ(n2)))) = plus(n2, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[69])).
% 9.68/9.90 tff(103,plain,
% 9.68/9.90 (succ(succ(succ(succ(n2)))) = succ(succ(n4))),
% 9.68/9.90 inference(transitivity,[status(thm)],[102, 78])).
% 9.68/9.90 tff(104,plain,
% 9.68/9.90 (succ(succ(succ(succ(succ(n2))))) = succ(succ(succ(n4)))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[103])).
% 9.68/9.90 tff(105,plain,
% 9.68/9.90 (succ(succ(succ(n4))) = succ(succ(succ(succ(succ(n2)))))),
% 9.68/9.90 inference(symmetry,[status(thm)],[104])).
% 9.68/9.90 tff(106,plain,
% 9.68/9.90 (^[X: $i] : refl((plus(n3, X) = succ(succ(succ(X)))) <=> (plus(n3, X) = succ(succ(succ(X)))))),
% 9.68/9.90 inference(bind,[status(th)],[])).
% 9.68/9.90 tff(107,plain,
% 9.68/9.90 (![X: $i] : (plus(n3, X) = succ(succ(succ(X)))) <=> ![X: $i] : (plus(n3, X) = succ(succ(succ(X))))),
% 9.68/9.90 inference(quant_intro,[status(thm)],[106])).
% 9.68/9.90 tff(108,plain,
% 9.68/9.90 (![X: $i] : (plus(n3, X) = succ(succ(succ(X)))) <=> ![X: $i] : (plus(n3, X) = succ(succ(succ(X))))),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(109,axiom,(![X: $i] : (plus(n3, X) = succ(succ(succ(X))))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_plus_3_l')).
% 9.68/9.90 tff(110,plain,
% 9.68/9.90 (![X: $i] : (plus(n3, X) = succ(succ(succ(X))))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[109, 108])).
% 9.68/9.90 tff(111,plain,(
% 9.68/9.90 ![X: $i] : (plus(n3, X) = succ(succ(succ(X))))),
% 9.68/9.90 inference(skolemize,[status(sab)],[110])).
% 9.68/9.90 tff(112,plain,
% 9.68/9.90 (![X: $i] : (plus(n3, X) = succ(succ(succ(X))))),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[111, 107])).
% 9.68/9.90 tff(113,plain,
% 9.68/9.90 ((~![X: $i] : (plus(n3, X) = succ(succ(succ(X))))) | (plus(n3, n4) = succ(succ(succ(n4))))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(114,plain,
% 9.68/9.90 (plus(n3, n4) = succ(succ(succ(n4)))),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[113, 112])).
% 9.68/9.90 tff(115,plain,
% 9.68/9.90 ((~![X: $i] : (plus(X, n4) = succ(succ(succ(succ(X)))))) | (plus(n3, n4) = succ(succ(succ(succ(n3)))))),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(116,plain,
% 9.68/9.90 (plus(n3, n4) = succ(succ(succ(succ(n3))))),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[115, 67])).
% 9.68/9.90 tff(117,plain,
% 9.68/9.90 (succ(succ(succ(succ(n3)))) = plus(n3, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[116])).
% 9.68/9.90 tff(118,plain,
% 9.68/9.90 (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(n2)))))),
% 9.68/9.90 inference(transitivity,[status(thm)],[117, 114, 105])).
% 9.68/9.90 tff(119,plain,
% 9.68/9.90 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) <=> leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13))))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[118])).
% 9.68/9.90 tff(120,plain,
% 9.68/9.90 (succ(succ(succ(n4))) = plus(n3, n4)),
% 9.68/9.90 inference(symmetry,[status(thm)],[114])).
% 9.68/9.90 tff(121,plain,
% 9.68/9.90 (succ(succ(succ(succ(succ(n2))))) = succ(succ(succ(succ(n3))))),
% 9.68/9.90 inference(transitivity,[status(thm)],[104, 120, 116])).
% 9.68/9.90 tff(122,plain,
% 9.68/9.90 (gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13))))))) <=> gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[121])).
% 9.68/9.90 tff(123,plain,
% 9.68/9.90 ((~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13)))))))) <=> (~gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[122])).
% 9.68/9.90 tff(124,plain,
% 9.68/9.90 ((a_select2(sigma_defuse, n0) = use) <=> (a_select2(sigma_defuse, n0) = use)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(125,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n0) = use),
% 9.68/9.90 inference(and_elim,[status(thm)],[5])).
% 9.68/9.90 tff(126,plain,
% 9.68/9.90 (a_select2(sigma_defuse, n0) = use),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[125, 124])).
% 9.68/9.90 tff(127,plain,
% 9.68/9.90 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(128,plain,
% 9.68/9.90 (![X: $i] : (pred(succ(X)) = X) <=> ![X: $i] : (pred(succ(X)) = X)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(129,axiom,(![X: $i] : (pred(succ(X)) = X)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','pred_succ')).
% 9.68/9.90 tff(130,plain,
% 9.68/9.90 (![X: $i] : (pred(succ(X)) = X)),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[129, 128])).
% 9.68/9.90 tff(131,plain,(
% 9.68/9.90 ![X: $i] : (pred(succ(X)) = X)),
% 9.68/9.90 inference(skolemize,[status(sab)],[130])).
% 9.68/9.90 tff(132,plain,
% 9.68/9.90 (![X: $i] : (pred(succ(X)) = X)),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[131, 127])).
% 9.68/9.90 tff(133,plain,
% 9.68/9.90 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n0)) = n0)),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(134,plain,
% 9.68/9.90 (pred(succ(n0)) = n0),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[133, 132])).
% 9.68/9.90 tff(135,plain,
% 9.68/9.90 ((succ(n0) = n1) <=> (succ(n0) = n1)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(136,axiom,(succ(n0) = n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_1')).
% 9.68/9.90 tff(137,plain,
% 9.68/9.90 (succ(n0) = n1),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[136, 135])).
% 9.68/9.90 tff(138,plain,
% 9.68/9.90 (n1 = succ(n0)),
% 9.68/9.90 inference(symmetry,[status(thm)],[137])).
% 9.68/9.90 tff(139,plain,
% 9.68/9.90 (pred(n1) = pred(succ(n0))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[138])).
% 9.68/9.90 tff(140,plain,
% 9.68/9.90 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n1)) = n1)),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(141,plain,
% 9.68/9.90 (pred(succ(n1)) = n1),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[140, 132])).
% 9.68/9.90 tff(142,plain,
% 9.68/9.90 (succ(n1) = succ(succ(n0))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[138])).
% 9.68/9.90 tff(143,plain,
% 9.68/9.90 (succ(succ(n0)) = succ(n1)),
% 9.68/9.90 inference(symmetry,[status(thm)],[142])).
% 9.68/9.90 tff(144,plain,
% 9.68/9.90 ((succ(succ(n0)) = n2) <=> (succ(succ(n0)) = n2)),
% 9.68/9.90 inference(rewrite,[status(thm)],[])).
% 9.68/9.90 tff(145,axiom,(succ(succ(n0)) = n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_2')).
% 9.68/9.90 tff(146,plain,
% 9.68/9.90 (succ(succ(n0)) = n2),
% 9.68/9.90 inference(modus_ponens,[status(thm)],[145, 144])).
% 9.68/9.90 tff(147,plain,
% 9.68/9.90 (n2 = succ(succ(n0))),
% 9.68/9.90 inference(symmetry,[status(thm)],[146])).
% 9.68/9.90 tff(148,plain,
% 9.68/9.90 (n2 = succ(n1)),
% 9.68/9.90 inference(transitivity,[status(thm)],[147, 143])).
% 9.68/9.90 tff(149,plain,
% 9.68/9.90 (pred(n2) = pred(succ(n1))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[148])).
% 9.68/9.90 tff(150,plain,
% 9.68/9.90 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n2)) = n2)),
% 9.68/9.90 inference(quant_inst,[status(thm)],[])).
% 9.68/9.90 tff(151,plain,
% 9.68/9.90 (pred(succ(n2)) = n2),
% 9.68/9.90 inference(unit_resolution,[status(thm)],[150, 132])).
% 9.68/9.90 tff(152,plain,
% 9.68/9.90 (succ(n2) = succ(succ(succ(n0)))),
% 9.68/9.90 inference(monotonicity,[status(thm)],[147])).
% 9.68/9.90 tff(153,plain,
% 9.68/9.90 (succ(succ(succ(n0))) = succ(n2)),
% 9.68/9.91 inference(symmetry,[status(thm)],[152])).
% 9.68/9.91 tff(154,plain,
% 9.68/9.91 (n3 = succ(n2)),
% 9.68/9.91 inference(transitivity,[status(thm)],[42, 153])).
% 9.68/9.91 tff(155,plain,
% 9.68/9.91 (pred(n3) = pred(succ(n2))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[154])).
% 9.68/9.91 tff(156,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n3)) = n3)),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(157,plain,
% 9.68/9.91 (pred(succ(n3)) = n3),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[156, 132])).
% 9.68/9.91 tff(158,plain,
% 9.68/9.91 (succ(succ(succ(succ(n0)))) = succ(n3)),
% 9.68/9.91 inference(symmetry,[status(thm)],[43])).
% 9.68/9.91 tff(159,plain,
% 9.68/9.91 (n4 = succ(n3)),
% 9.68/9.91 inference(transitivity,[status(thm)],[14, 158])).
% 9.68/9.91 tff(160,plain,
% 9.68/9.91 (pred(n4) = pred(succ(n3))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[159])).
% 9.68/9.91 tff(161,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n4)) = n4)),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(162,plain,
% 9.68/9.91 (pred(succ(n4)) = n4),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[161, 132])).
% 9.68/9.91 tff(163,plain,
% 9.68/9.91 (n5 = succ(n4)),
% 9.68/9.91 inference(transitivity,[status(thm)],[96, 95])).
% 9.68/9.91 tff(164,plain,
% 9.68/9.91 (pred(n5) = pred(succ(n4))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[163])).
% 9.68/9.91 tff(165,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(n5)) = n5)),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(166,plain,
% 9.68/9.91 (pred(succ(n5)) = n5),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[165, 132])).
% 9.68/9.91 tff(167,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(n1))))) = succ(n5)),
% 9.68/9.91 inference(symmetry,[status(thm)],[98])).
% 9.68/9.91 tff(168,plain,
% 9.68/9.91 (succ(succ(n4)) = succ(succ(succ(succ(succ(n1)))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[93])).
% 9.68/9.91 tff(169,plain,
% 9.68/9.91 (succ(succ(succ(succ(n2)))) = succ(n5)),
% 9.68/9.91 inference(transitivity,[status(thm)],[102, 78, 168, 167])).
% 9.68/9.91 tff(170,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(n2))))) = pred(succ(n5))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[169])).
% 9.68/9.91 tff(171,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(succ(succ(n2)))))) = succ(succ(succ(succ(n2)))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(172,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(n2)))))) = succ(succ(succ(succ(n2))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[171, 132])).
% 9.68/9.91 tff(173,assumption,(succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))), introduced(assumption)).
% 9.68/9.91 tff(174,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(n2))))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.68/9.91 inference(transitivity,[status(thm)],[104, 120, 116, 173])).
% 9.68/9.91 tff(175,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(n2)))))) = pred(succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[174])).
% 9.68/9.91 tff(176,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(succ(succ(E!13)))))))) = pred(succ(succ(succ(succ(succ(n2))))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[175])).
% 9.68/9.91 tff(177,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(succ(succ(succ(succ(E!13)))))))) = succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(178,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(succ(succ(E!13)))))))) = succ(succ(succ(succ(succ(succ(E!13))))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[177, 132])).
% 9.68/9.91 tff(179,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(succ(E!13)))))) = pred(succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[178])).
% 9.68/9.91 tff(180,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n2))))),
% 9.68/9.91 inference(transitivity,[status(thm)],[179, 176, 172])).
% 9.68/9.91 tff(181,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(succ(E!13))))))) = pred(succ(succ(succ(succ(n2)))))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[180])).
% 9.68/9.91 tff(182,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(succ(succ(succ(E!13))))))) = succ(succ(succ(succ(succ(E!13))))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(183,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(succ(E!13))))))) = succ(succ(succ(succ(succ(E!13)))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[182, 132])).
% 9.68/9.91 tff(184,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(E!13))))) = pred(succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[183])).
% 9.68/9.91 tff(185,plain,
% 9.68/9.91 (succ(succ(succ(succ(succ(E!13))))) = n5),
% 9.68/9.91 inference(transitivity,[status(thm)],[184, 181, 170, 166])).
% 9.68/9.91 tff(186,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(E!13)))))) = pred(n5)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[185])).
% 9.68/9.91 tff(187,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(E!13)))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(188,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(E!13))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[187, 132])).
% 9.68/9.91 tff(189,plain,
% 9.68/9.91 (succ(succ(succ(succ(E!13)))) = pred(succ(succ(succ(succ(succ(E!13))))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[188])).
% 9.68/9.91 tff(190,plain,
% 9.68/9.91 (succ(succ(succ(succ(E!13)))) = n4),
% 9.68/9.91 inference(transitivity,[status(thm)],[189, 186, 164, 162])).
% 9.68/9.91 tff(191,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(E!13))))) = pred(n4)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[190])).
% 9.68/9.91 tff(192,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(succ(E!13))))) = succ(succ(succ(E!13))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(193,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(E!13))))) = succ(succ(succ(E!13)))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[192, 132])).
% 9.68/9.91 tff(194,plain,
% 9.68/9.91 (succ(succ(succ(E!13))) = pred(succ(succ(succ(succ(E!13)))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[193])).
% 9.68/9.91 tff(195,plain,
% 9.68/9.91 (succ(succ(succ(E!13))) = n3),
% 9.68/9.91 inference(transitivity,[status(thm)],[194, 191, 160, 157])).
% 9.68/9.91 tff(196,plain,
% 9.68/9.91 (pred(succ(succ(succ(E!13)))) = pred(n3)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[195])).
% 9.68/9.91 tff(197,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(succ(E!13)))) = succ(succ(E!13)))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(198,plain,
% 9.68/9.91 (pred(succ(succ(succ(E!13)))) = succ(succ(E!13))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[197, 132])).
% 9.68/9.91 tff(199,plain,
% 9.68/9.91 (succ(succ(E!13)) = pred(succ(succ(succ(E!13))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[198])).
% 9.68/9.91 tff(200,plain,
% 9.68/9.91 (succ(succ(E!13)) = n2),
% 9.68/9.91 inference(transitivity,[status(thm)],[199, 196, 155, 151])).
% 9.68/9.91 tff(201,plain,
% 9.68/9.91 (pred(succ(succ(E!13))) = pred(n2)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[200])).
% 9.68/9.91 tff(202,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(succ(E!13))) = succ(E!13))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(203,plain,
% 9.68/9.91 (pred(succ(succ(E!13))) = succ(E!13)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[202, 132])).
% 9.68/9.91 tff(204,plain,
% 9.68/9.91 (succ(E!13) = pred(succ(succ(E!13)))),
% 9.68/9.91 inference(symmetry,[status(thm)],[203])).
% 9.68/9.91 tff(205,plain,
% 9.68/9.91 (succ(E!13) = n1),
% 9.68/9.91 inference(transitivity,[status(thm)],[204, 201, 149, 141])).
% 9.68/9.91 tff(206,plain,
% 9.68/9.91 (pred(succ(E!13)) = pred(n1)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[205])).
% 9.68/9.91 tff(207,plain,
% 9.68/9.91 ((~![X: $i] : (pred(succ(X)) = X)) | (pred(succ(E!13)) = E!13)),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(208,plain,
% 9.68/9.91 (pred(succ(E!13)) = E!13),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[207, 132])).
% 9.68/9.91 tff(209,plain,
% 9.68/9.91 (E!13 = pred(succ(E!13))),
% 9.68/9.91 inference(symmetry,[status(thm)],[208])).
% 9.68/9.91 tff(210,plain,
% 9.68/9.91 (E!13 = n0),
% 9.68/9.91 inference(transitivity,[status(thm)],[209, 206, 139, 134])).
% 9.68/9.91 tff(211,plain,
% 9.68/9.91 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n0)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[210])).
% 9.68/9.91 tff(212,plain,
% 9.68/9.91 (a_select2(sigma_defuse, E!13) = use),
% 9.68/9.91 inference(transitivity,[status(thm)],[211, 126])).
% 9.68/9.91 tff(213,plain,
% 9.68/9.91 ($false),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[28, 212])).
% 9.68/9.91 tff(214,plain,(~(succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13))))))))), inference(lemma,lemma(discharge,[]))).
% 9.68/9.91 tff(215,plain,
% 9.68/9.91 (gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) <=> gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[121])).
% 9.68/9.91 tff(216,plain,
% 9.68/9.91 ((~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))) <=> (~gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[215])).
% 9.68/9.91 tff(217,plain,
% 9.68/9.91 (^[X: $i, Y: $i] : refl((leq(X, Y) <=> gt(succ(Y), X)) <=> (leq(X, Y) <=> gt(succ(Y), X)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(218,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X)) <=> ![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[217])).
% 9.68/9.91 tff(219,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X)) <=> ![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(220,axiom,(![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','leq_succ_gt_equiv')).
% 9.68/9.91 tff(221,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[220, 219])).
% 9.68/9.91 tff(222,plain,(
% 9.68/9.91 ![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))),
% 9.68/9.91 inference(skolemize,[status(sab)],[221])).
% 9.68/9.91 tff(223,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[222, 218])).
% 9.68/9.91 tff(224,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))) | (leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(225,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[224, 223])).
% 9.68/9.91 tff(226,plain,
% 9.68/9.91 (^[X: $i, Y: $i] : refl((leq(X, pred(Y)) <=> gt(Y, X)) <=> (leq(X, pred(Y)) <=> gt(Y, X)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(227,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X)) <=> ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[226])).
% 9.68/9.91 tff(228,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X)) <=> ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(229,axiom,(![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','leq_gt_pred')).
% 9.68/9.91 tff(230,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[229, 228])).
% 9.68/9.91 tff(231,plain,(
% 9.68/9.91 ![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 9.68/9.91 inference(skolemize,[status(sab)],[230])).
% 9.68/9.91 tff(232,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[231, 227])).
% 9.68/9.91 tff(233,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))) <=> gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(234,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))) <=> gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[233, 232])).
% 9.68/9.91 tff(235,plain,
% 9.68/9.91 (pred(succ(succ(succ(succ(n2))))) = n5),
% 9.68/9.91 inference(transitivity,[status(thm)],[170, 166])).
% 9.68/9.91 tff(236,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))) <=> leq(succ(succ(succ(succ(succ(succ(E!13)))))), n5)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[235])).
% 9.68/9.91 tff(237,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), n5) <=> leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2))))))),
% 9.68/9.91 inference(symmetry,[status(thm)],[236])).
% 9.68/9.91 tff(238,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4)) <=> leq(succ(succ(succ(succ(succ(succ(E!13)))))), n5)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[58])).
% 9.68/9.91 tff(239,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4)) <=> leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2))))))),
% 9.68/9.91 inference(transitivity,[status(thm)],[238, 237])).
% 9.68/9.91 tff(240,plain,
% 9.68/9.91 ((~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4))) <=> (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[239])).
% 9.68/9.91 tff(241,plain,
% 9.68/9.91 (^[X: $i, Y: $i] : refl((leq(succ(X), succ(Y)) <=> leq(X, Y)) <=> (leq(succ(X), succ(Y)) <=> leq(X, Y)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(242,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y)) <=> ![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[241])).
% 9.68/9.91 tff(243,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y)) <=> ![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(244,axiom,(![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','leq_succ_succ')).
% 9.68/9.91 tff(245,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[244, 243])).
% 9.68/9.91 tff(246,plain,(
% 9.68/9.91 ![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))),
% 9.68/9.91 inference(skolemize,[status(sab)],[245])).
% 9.68/9.91 tff(247,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[246, 242])).
% 9.68/9.91 tff(248,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4)) <=> leq(succ(succ(succ(succ(succ(E!13))))), n4))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(249,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4)) <=> leq(succ(succ(succ(succ(succ(E!13))))), n4)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[248, 247])).
% 9.68/9.91 tff(250,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(succ(succ(succ(succ(E!13)))), pred(n4)) <=> gt(n4, succ(succ(succ(succ(E!13))))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(251,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), pred(n4)) <=> gt(n4, succ(succ(succ(succ(E!13)))))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[250, 232])).
% 9.68/9.91 tff(252,plain,
% 9.68/9.91 (pred(n4) = n3),
% 9.68/9.91 inference(transitivity,[status(thm)],[160, 157])).
% 9.68/9.91 tff(253,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), pred(n4)) <=> leq(succ(succ(succ(succ(E!13)))), n3)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[252])).
% 9.68/9.91 tff(254,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), n3) <=> leq(succ(succ(succ(succ(E!13)))), pred(n4))),
% 9.68/9.91 inference(symmetry,[status(thm)],[253])).
% 9.68/9.91 tff(255,plain,
% 9.68/9.91 (succ(n2) = n3),
% 9.68/9.91 inference(transitivity,[status(thm)],[152, 41])).
% 9.68/9.91 tff(256,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), succ(n2)) <=> leq(succ(succ(succ(succ(E!13)))), n3)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[255])).
% 9.68/9.91 tff(257,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), succ(n2)) <=> leq(succ(succ(succ(succ(E!13)))), pred(n4))),
% 9.68/9.91 inference(transitivity,[status(thm)],[256, 254])).
% 9.68/9.91 tff(258,plain,
% 9.68/9.91 ((~leq(succ(succ(succ(succ(E!13)))), succ(n2))) <=> (~leq(succ(succ(succ(succ(E!13)))), pred(n4)))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[257])).
% 9.68/9.91 tff(259,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(succ(succ(succ(E!13)))), succ(n2)) <=> leq(succ(succ(succ(E!13))), n2))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(260,plain,
% 9.68/9.91 (leq(succ(succ(succ(succ(E!13)))), succ(n2)) <=> leq(succ(succ(succ(E!13))), n2)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[259, 247])).
% 9.68/9.91 tff(261,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(succ(succ(E!13)), pred(n2)) <=> gt(n2, succ(succ(E!13))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(262,plain,
% 9.68/9.91 (leq(succ(succ(E!13)), pred(n2)) <=> gt(n2, succ(succ(E!13)))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[261, 232])).
% 9.68/9.91 tff(263,plain,
% 9.68/9.91 (pred(n2) = n1),
% 9.68/9.91 inference(transitivity,[status(thm)],[149, 141])).
% 9.68/9.91 tff(264,plain,
% 9.68/9.91 (leq(succ(succ(E!13)), pred(n2)) <=> leq(succ(succ(E!13)), n1)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[263])).
% 9.68/9.91 tff(265,plain,
% 9.68/9.91 (leq(succ(succ(E!13)), n1) <=> leq(succ(succ(E!13)), pred(n2))),
% 9.68/9.91 inference(symmetry,[status(thm)],[264])).
% 9.68/9.91 tff(266,plain,
% 9.68/9.91 ((~leq(succ(succ(E!13)), n1)) <=> (~leq(succ(succ(E!13)), pred(n2)))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[265])).
% 9.68/9.91 tff(267,plain,
% 9.68/9.91 (leq(succ(succ(E!13)), succ(n0)) <=> leq(succ(succ(E!13)), n1)),
% 9.68/9.91 inference(monotonicity,[status(thm)],[137])).
% 9.68/9.91 tff(268,plain,
% 9.68/9.91 ((~leq(succ(succ(E!13)), succ(n0))) <=> (~leq(succ(succ(E!13)), n1))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[267])).
% 9.68/9.91 tff(269,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(succ(E!13)), succ(n0)) <=> leq(succ(E!13), n0))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(270,plain,
% 9.68/9.91 (leq(succ(succ(E!13)), succ(n0)) <=> leq(succ(E!13), n0)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[269, 247])).
% 9.68/9.91 tff(271,plain,
% 9.68/9.91 (leq(n1, succ(E!13)) <=> leq(succ(n0), succ(E!13))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[138])).
% 9.68/9.91 tff(272,plain,
% 9.68/9.91 (leq(succ(n0), succ(E!13)) <=> leq(n1, succ(E!13))),
% 9.68/9.91 inference(symmetry,[status(thm)],[271])).
% 9.68/9.91 tff(273,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n0), succ(E!13)) <=> leq(n0, E!13))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(274,plain,
% 9.68/9.91 (leq(succ(n0), succ(E!13)) <=> leq(n0, E!13)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[273, 247])).
% 9.68/9.91 tff(275,plain,
% 9.68/9.91 (leq(n0, E!13) & leq(E!13, n5)),
% 9.68/9.91 inference(or_elim,[status(thm)],[27])).
% 9.68/9.91 tff(276,plain,
% 9.68/9.91 (leq(n0, E!13)),
% 9.68/9.91 inference(and_elim,[status(thm)],[275])).
% 9.68/9.91 tff(277,plain,
% 9.68/9.91 ((~(leq(succ(n0), succ(E!13)) <=> leq(n0, E!13))) | leq(succ(n0), succ(E!13)) | (~leq(n0, E!13))),
% 9.68/9.91 inference(tautology,[status(thm)],[])).
% 9.68/9.91 tff(278,plain,
% 9.68/9.91 ((~(leq(succ(n0), succ(E!13)) <=> leq(n0, E!13))) | leq(succ(n0), succ(E!13))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[277, 276])).
% 9.68/9.91 tff(279,plain,
% 9.68/9.91 (leq(succ(n0), succ(E!13))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[278, 274])).
% 9.68/9.91 tff(280,plain,
% 9.68/9.91 (leq(n1, succ(E!13))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[279, 272])).
% 9.68/9.91 tff(281,plain,
% 9.68/9.91 ((succ(tptp_minus_1) = n0) <=> (succ(tptp_minus_1) = n0)),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(282,axiom,(succ(tptp_minus_1) = n0), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','succ_tptp_minus_1')).
% 9.68/9.91 tff(283,plain,
% 9.68/9.91 (succ(tptp_minus_1) = n0),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[282, 281])).
% 9.68/9.91 tff(284,plain,
% 9.68/9.91 (n0 = succ(tptp_minus_1)),
% 9.68/9.91 inference(symmetry,[status(thm)],[283])).
% 9.68/9.91 tff(285,plain,
% 9.68/9.91 (leq(n1, n0) <=> leq(succ(n0), succ(tptp_minus_1))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[138, 284])).
% 9.68/9.91 tff(286,plain,
% 9.68/9.91 (leq(succ(n0), succ(tptp_minus_1)) <=> leq(n1, n0)),
% 9.68/9.91 inference(symmetry,[status(thm)],[285])).
% 9.68/9.91 tff(287,plain,
% 9.68/9.91 (leq(succ(n0), n0) <=> leq(succ(n0), succ(tptp_minus_1))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[284])).
% 9.68/9.91 tff(288,plain,
% 9.68/9.91 (leq(succ(n0), n0) <=> leq(n1, n0)),
% 9.68/9.91 inference(transitivity,[status(thm)],[287, 286])).
% 9.68/9.91 tff(289,plain,
% 9.68/9.91 ((~leq(succ(n0), n0)) <=> (~leq(n1, n0))),
% 9.68/9.91 inference(monotonicity,[status(thm)],[288])).
% 9.68/9.91 tff(290,plain,
% 9.68/9.91 (^[X: $i] : refl((~gt(X, X)) <=> (~gt(X, X)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(291,plain,
% 9.68/9.91 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[290])).
% 9.68/9.91 tff(292,plain,
% 9.68/9.91 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(293,axiom,(![X: $i] : (~gt(X, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','irreflexivity_gt')).
% 9.68/9.91 tff(294,plain,
% 9.68/9.91 (![X: $i] : (~gt(X, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[293, 292])).
% 9.68/9.91 tff(295,plain,(
% 9.68/9.91 ![X: $i] : (~gt(X, X))),
% 9.68/9.91 inference(skolemize,[status(sab)],[294])).
% 9.68/9.91 tff(296,plain,
% 9.68/9.91 (![X: $i] : (~gt(X, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[295, 291])).
% 9.68/9.91 tff(297,plain,
% 9.68/9.91 ((~![X: $i] : (~gt(X, X))) | (~gt(n0, n0))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(298,plain,
% 9.68/9.91 (~gt(n0, n0)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[297, 296])).
% 9.68/9.91 tff(299,plain,
% 9.68/9.91 (^[X: $i, Y: $i] : refl(((~leq(succ(X), Y)) | gt(Y, X)) <=> ((~leq(succ(X), Y)) | gt(Y, X)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(300,plain,
% 9.68/9.91 (![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X)) <=> ![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[299])).
% 9.68/9.91 tff(301,plain,
% 9.68/9.91 (![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X)) <=> ![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(302,plain,
% 9.68/9.91 (^[X: $i, Y: $i] : rewrite((leq(succ(X), Y) => gt(Y, X)) <=> ((~leq(succ(X), Y)) | gt(Y, X)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(303,plain,
% 9.68/9.91 (![X: $i, Y: $i] : (leq(succ(X), Y) => gt(Y, X)) <=> ![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[302])).
% 9.68/9.91 tff(304,axiom,(![X: $i, Y: $i] : (leq(succ(X), Y) => gt(Y, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','leq_succ_gt')).
% 9.68/9.91 tff(305,plain,
% 9.68/9.91 (![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[304, 303])).
% 9.68/9.91 tff(306,plain,
% 9.68/9.91 (![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[305, 301])).
% 9.68/9.91 tff(307,plain,(
% 9.68/9.91 ![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(skolemize,[status(sab)],[306])).
% 9.68/9.91 tff(308,plain,
% 9.68/9.91 (![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[307, 300])).
% 9.68/9.91 tff(309,plain,
% 9.68/9.91 (((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(n0), n0)) | gt(n0, n0))) <=> ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(n0), n0)) | gt(n0, n0))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(310,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(n0), n0)) | gt(n0, n0))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(311,plain,
% 9.68/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(n0), n0)) | gt(n0, n0)),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[310, 309])).
% 9.68/9.91 tff(312,plain,
% 9.68/9.91 ((~leq(succ(n0), n0)) | gt(n0, n0)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[311, 308])).
% 9.68/9.91 tff(313,plain,
% 9.68/9.91 (~leq(succ(n0), n0)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[312, 298])).
% 9.68/9.91 tff(314,plain,
% 9.68/9.91 (~leq(n1, n0)),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[313, 289])).
% 9.68/9.91 tff(315,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(316,plain,
% 9.68/9.91 (^[X: $i, Y: $i, Z: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(X, Y) & leq(Y, Z)) <=> (~((~leq(Y, Z)) | (~leq(X, Y))))), ((~(leq(X, Y) & leq(Y, Z))) <=> (~(~((~leq(Y, Z)) | (~leq(X, Y))))))), rewrite((~(~((~leq(Y, Z)) | (~leq(X, Y))))) <=> ((~leq(Y, Z)) | (~leq(X, Y)))), ((~(leq(X, Y) & leq(Y, Z))) <=> ((~leq(Y, Z)) | (~leq(X, Y))))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)))), rewrite((((~leq(Y, Z)) | (~leq(X, Y))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))), (((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(317,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[316])).
% 9.68/9.91 tff(318,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(319,plain,
% 9.68/9.91 (^[X: $i, Y: $i, Z: $i] : rewrite(((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z)))),
% 9.68/9.91 inference(bind,[status(th)],[])).
% 9.68/9.91 tff(320,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z)) <=> ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 9.68/9.91 inference(quant_intro,[status(thm)],[319])).
% 9.68/9.91 tff(321,axiom,(![X: $i, Y: $i, Z: $i] : ((leq(X, Y) & leq(Y, Z)) => leq(X, Z))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','transitivity_leq')).
% 9.68/9.91 tff(322,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[321, 320])).
% 9.68/9.91 tff(323,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[322, 318])).
% 9.68/9.91 tff(324,plain,(
% 9.68/9.91 ![X: $i, Y: $i, Z: $i] : ((~(leq(X, Y) & leq(Y, Z))) | leq(X, Z))),
% 9.68/9.91 inference(skolemize,[status(sab)],[323])).
% 9.68/9.91 tff(325,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[324, 317])).
% 9.68/9.91 tff(326,plain,
% 9.68/9.91 (![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[325, 315])).
% 9.68/9.91 tff(327,plain,
% 9.68/9.91 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(n1, n0) | (~leq(succ(E!13), n0)) | (~leq(n1, succ(E!13))))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | leq(n1, n0) | (~leq(succ(E!13), n0)) | (~leq(n1, succ(E!13))))),
% 9.68/9.91 inference(rewrite,[status(thm)],[])).
% 9.68/9.91 tff(328,plain,
% 9.68/9.91 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(n1, n0) | (~leq(succ(E!13), n0)) | (~leq(n1, succ(E!13))))),
% 9.68/9.91 inference(quant_inst,[status(thm)],[])).
% 9.68/9.91 tff(329,plain,
% 9.68/9.91 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | leq(n1, n0) | (~leq(succ(E!13), n0)) | (~leq(n1, succ(E!13)))),
% 9.68/9.91 inference(modus_ponens,[status(thm)],[328, 327])).
% 9.68/9.91 tff(330,plain,
% 9.68/9.91 (leq(n1, n0) | (~leq(succ(E!13), n0)) | (~leq(n1, succ(E!13)))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[329, 326])).
% 9.68/9.91 tff(331,plain,
% 9.68/9.91 (~leq(succ(E!13), n0)),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[330, 314, 280])).
% 9.68/9.91 tff(332,plain,
% 9.68/9.91 ((~(leq(succ(succ(E!13)), succ(n0)) <=> leq(succ(E!13), n0))) | (~leq(succ(succ(E!13)), succ(n0))) | leq(succ(E!13), n0)),
% 9.68/9.91 inference(tautology,[status(thm)],[])).
% 9.68/9.91 tff(333,plain,
% 9.68/9.91 (~leq(succ(succ(E!13)), succ(n0))),
% 9.68/9.91 inference(unit_resolution,[status(thm)],[332, 331, 270])).
% 9.76/9.91 tff(334,plain,
% 9.76/9.91 (~leq(succ(succ(E!13)), n1)),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[333, 268])).
% 9.76/9.91 tff(335,plain,
% 9.76/9.91 (~leq(succ(succ(E!13)), pred(n2))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[334, 266])).
% 9.76/9.91 tff(336,plain,
% 9.76/9.91 ((~(leq(succ(succ(E!13)), pred(n2)) <=> gt(n2, succ(succ(E!13))))) | leq(succ(succ(E!13)), pred(n2)) | (~gt(n2, succ(succ(E!13))))),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(337,plain,
% 9.76/9.91 (~gt(n2, succ(succ(E!13)))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[336, 335, 262])).
% 9.76/9.91 tff(338,plain,
% 9.76/9.91 (((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(E!13))), n2)) | gt(n2, succ(succ(E!13))))) <=> ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(E!13))), n2)) | gt(n2, succ(succ(E!13))))),
% 9.76/9.91 inference(rewrite,[status(thm)],[])).
% 9.76/9.91 tff(339,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(E!13))), n2)) | gt(n2, succ(succ(E!13))))),
% 9.76/9.91 inference(quant_inst,[status(thm)],[])).
% 9.76/9.91 tff(340,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(E!13))), n2)) | gt(n2, succ(succ(E!13)))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[339, 338])).
% 9.76/9.91 tff(341,plain,
% 9.76/9.91 ((~leq(succ(succ(succ(E!13))), n2)) | gt(n2, succ(succ(E!13)))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[340, 308])).
% 9.76/9.91 tff(342,plain,
% 9.76/9.91 (~leq(succ(succ(succ(E!13))), n2)),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[341, 337])).
% 9.76/9.91 tff(343,plain,
% 9.76/9.91 ((~(leq(succ(succ(succ(succ(E!13)))), succ(n2)) <=> leq(succ(succ(succ(E!13))), n2))) | (~leq(succ(succ(succ(succ(E!13)))), succ(n2))) | leq(succ(succ(succ(E!13))), n2)),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(344,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(E!13)))), succ(n2))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[343, 342, 260])).
% 9.76/9.91 tff(345,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(E!13)))), pred(n4))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[344, 258])).
% 9.76/9.91 tff(346,plain,
% 9.76/9.91 ((~(leq(succ(succ(succ(succ(E!13)))), pred(n4)) <=> gt(n4, succ(succ(succ(succ(E!13))))))) | leq(succ(succ(succ(succ(E!13)))), pred(n4)) | (~gt(n4, succ(succ(succ(succ(E!13))))))),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(347,plain,
% 9.76/9.91 (~gt(n4, succ(succ(succ(succ(E!13)))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[346, 345, 251])).
% 9.76/9.91 tff(348,plain,
% 9.76/9.91 (((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(succ(succ(E!13))))), n4)) | gt(n4, succ(succ(succ(succ(E!13))))))) <=> ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(succ(succ(E!13))))), n4)) | gt(n4, succ(succ(succ(succ(E!13))))))),
% 9.76/9.91 inference(rewrite,[status(thm)],[])).
% 9.76/9.91 tff(349,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(succ(succ(E!13))))), n4)) | gt(n4, succ(succ(succ(succ(E!13))))))),
% 9.76/9.91 inference(quant_inst,[status(thm)],[])).
% 9.76/9.91 tff(350,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(succ(succ(E!13))))), n4)) | gt(n4, succ(succ(succ(succ(E!13)))))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[349, 348])).
% 9.76/9.91 tff(351,plain,
% 9.76/9.91 ((~leq(succ(succ(succ(succ(succ(E!13))))), n4)) | gt(n4, succ(succ(succ(succ(E!13)))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[350, 308])).
% 9.76/9.91 tff(352,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(succ(E!13))))), n4)),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[351, 347])).
% 9.76/9.91 tff(353,plain,
% 9.76/9.91 ((~(leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4)) <=> leq(succ(succ(succ(succ(succ(E!13))))), n4))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4))) | leq(succ(succ(succ(succ(succ(E!13))))), n4)),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(354,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(n4))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[353, 352, 249])).
% 9.76/9.91 tff(355,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2))))))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[354, 240])).
% 9.76/9.91 tff(356,plain,
% 9.76/9.91 ((~(leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))) <=> gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))) | leq(succ(succ(succ(succ(succ(succ(E!13)))))), pred(succ(succ(succ(succ(n2)))))) | (~gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(357,plain,
% 9.76/9.91 (~gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[356, 355, 234])).
% 9.76/9.91 tff(358,plain,
% 9.76/9.91 (((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))) | gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))) <=> ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))) | gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.91 inference(rewrite,[status(thm)],[])).
% 9.76/9.91 tff(359,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))) | gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.91 inference(quant_inst,[status(thm)],[])).
% 9.76/9.91 tff(360,plain,
% 9.76/9.91 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))) | gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[359, 358])).
% 9.76/9.91 tff(361,plain,
% 9.76/9.91 ((~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))) | gt(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[360, 308])).
% 9.76/9.91 tff(362,plain,
% 9.76/9.91 (~leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2)))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[361, 357])).
% 9.76/9.91 tff(363,plain,
% 9.76/9.91 ((~(leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))) | leq(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n2))))) | (~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.91 inference(tautology,[status(thm)],[])).
% 9.76/9.91 tff(364,plain,
% 9.76/9.91 (~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.91 inference(unit_resolution,[status(thm)],[363, 362, 225])).
% 9.76/9.91 tff(365,plain,
% 9.76/9.91 (~gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[364, 216])).
% 9.76/9.91 tff(366,plain,
% 9.76/9.91 (^[X: $i, Y: $i] : refl(((X = Y) | gt(Y, X) | gt(X, Y)) <=> ((X = Y) | gt(Y, X) | gt(X, Y)))),
% 9.76/9.91 inference(bind,[status(th)],[])).
% 9.76/9.91 tff(367,plain,
% 9.76/9.91 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y)) <=> ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.91 inference(quant_intro,[status(thm)],[366])).
% 9.76/9.91 tff(368,plain,
% 9.76/9.91 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y)) <=> ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.91 inference(rewrite,[status(thm)],[])).
% 9.76/9.91 tff(369,plain,
% 9.76/9.91 (^[X: $i, Y: $i] : trans(monotonicity(rewrite((gt(X, Y) | gt(Y, X)) <=> (gt(Y, X) | gt(X, Y))), (((gt(X, Y) | gt(Y, X)) | (X = Y)) <=> ((gt(Y, X) | gt(X, Y)) | (X = Y)))), rewrite(((gt(Y, X) | gt(X, Y)) | (X = Y)) <=> ((X = Y) | gt(Y, X) | gt(X, Y))), (((gt(X, Y) | gt(Y, X)) | (X = Y)) <=> ((X = Y) | gt(Y, X) | gt(X, Y))))),
% 9.76/9.91 inference(bind,[status(th)],[])).
% 9.76/9.91 tff(370,plain,
% 9.76/9.91 (![X: $i, Y: $i] : ((gt(X, Y) | gt(Y, X)) | (X = Y)) <=> ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.91 inference(quant_intro,[status(thm)],[369])).
% 9.76/9.91 tff(371,axiom,(![X: $i, Y: $i] : ((gt(X, Y) | gt(Y, X)) | (X = Y))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','totality')).
% 9.76/9.91 tff(372,plain,
% 9.76/9.91 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[371, 370])).
% 9.76/9.91 tff(373,plain,
% 9.76/9.91 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.91 inference(modus_ponens,[status(thm)],[372, 368])).
% 9.76/9.91 tff(374,plain,(
% 9.76/9.92 ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.92 inference(skolemize,[status(sab)],[373])).
% 9.76/9.92 tff(375,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[374, 367])).
% 9.76/9.92 tff(376,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(377,plain,
% 9.76/9.92 (((succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13))))))))) <=> (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(378,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | ((succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13))))))))))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[377])).
% 9.76/9.92 tff(379,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | ((succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.92 inference(transitivity,[status(thm)],[378, 376])).
% 9.76/9.92 tff(380,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | ((succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(381,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[380, 379])).
% 9.76/9.92 tff(382,plain,
% 9.76/9.92 (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(succ(E!13)))))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[381, 375])).
% 9.76/9.92 tff(383,plain,
% 9.76/9.92 (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))) | (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[382, 365])).
% 9.76/9.92 tff(384,plain,
% 9.76/9.92 (gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[383, 214])).
% 9.76/9.92 tff(385,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) <=> gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(386,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) <=> gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[385, 223])).
% 9.76/9.92 tff(387,plain,
% 9.76/9.92 ((~(leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) <=> gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))))) | leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | (~gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(388,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | (~gt(succ(succ(succ(succ(succ(succ(succ(E!13))))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[387, 386])).
% 9.76/9.92 tff(389,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[388, 384])).
% 9.76/9.92 tff(390,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) <=> leq(succ(succ(succ(succ(succ(n2))))), succ(n5))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[118, 169])).
% 9.76/9.92 tff(391,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(n2))))), succ(n5)) <=> leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2)))))),
% 9.76/9.92 inference(symmetry,[status(thm)],[390])).
% 9.76/9.92 tff(392,plain,
% 9.76/9.92 ((~leq(succ(succ(succ(succ(succ(n2))))), succ(n5))) <=> (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[391])).
% 9.76/9.92 tff(393,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(succ(succ(succ(succ(n2))))), succ(n5)) <=> leq(succ(succ(succ(succ(n2)))), n5))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(394,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(n2))))), succ(n5)) <=> leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[393, 247])).
% 9.76/9.92 tff(395,plain,
% 9.76/9.92 (leq(succ(n5), n5) <=> leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[99])).
% 9.76/9.92 tff(396,plain,
% 9.76/9.92 ((~leq(succ(n5), n5)) <=> (~leq(succ(succ(succ(succ(n2)))), n5))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[395])).
% 9.76/9.92 tff(397,plain,
% 9.76/9.92 ((~![X: $i] : (~gt(X, X))) | (~gt(n5, n5))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(398,plain,
% 9.76/9.92 (~gt(n5, n5)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[397, 296])).
% 9.76/9.92 tff(399,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(n5), n5)) | gt(n5, n5))) <=> ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(n5), n5)) | gt(n5, n5))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(400,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | ((~leq(succ(n5), n5)) | gt(n5, n5))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(401,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((~leq(succ(X), Y)) | gt(Y, X))) | (~leq(succ(n5), n5)) | gt(n5, n5)),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[400, 399])).
% 9.76/9.92 tff(402,plain,
% 9.76/9.92 ((~leq(succ(n5), n5)) | gt(n5, n5)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[401, 308])).
% 9.76/9.92 tff(403,plain,
% 9.76/9.92 (~leq(succ(n5), n5)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[402, 398])).
% 9.76/9.92 tff(404,plain,
% 9.76/9.92 (~leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[403, 396])).
% 9.76/9.92 tff(405,plain,
% 9.76/9.92 ((~(leq(succ(succ(succ(succ(succ(n2))))), succ(n5)) <=> leq(succ(succ(succ(succ(n2)))), n5))) | (~leq(succ(succ(succ(succ(succ(n2))))), succ(n5))) | leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(406,plain,
% 9.76/9.92 (~leq(succ(succ(succ(succ(succ(n2))))), succ(n5))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[405, 404, 394])).
% 9.76/9.92 tff(407,plain,
% 9.76/9.92 (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2)))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[406, 392])).
% 9.76/9.92 tff(408,plain,
% 9.76/9.92 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(409,plain,
% 9.76/9.92 ((leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))))) <=> (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(410,plain,
% 9.76/9.92 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))))))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[409])).
% 9.76/9.92 tff(411,plain,
% 9.76/9.92 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))))),
% 9.76/9.92 inference(transitivity,[status(thm)],[410, 408])).
% 9.76/9.92 tff(412,plain,
% 9.76/9.92 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(413,plain,
% 9.76/9.92 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(n2))))) | (~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[412, 411])).
% 9.76/9.92 tff(414,plain,
% 9.76/9.92 ((~leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))) | (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[413, 326, 407])).
% 9.76/9.92 tff(415,plain,
% 9.76/9.92 (~leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[414, 389])).
% 9.76/9.92 tff(416,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))) | (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(417,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[416, 223])).
% 9.76/9.92 tff(418,plain,
% 9.76/9.92 ((~(leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))) <=> gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13))))))))) | leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))) | (~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(419,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n2))))) | (~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13))))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[418, 417])).
% 9.76/9.92 tff(420,plain,
% 9.76/9.92 (~gt(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[419, 415])).
% 9.76/9.92 tff(421,plain,
% 9.76/9.92 (~gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[420, 123])).
% 9.76/9.92 tff(422,plain,
% 9.76/9.92 ((a_select2(sigma_defuse, n1) = use) <=> (a_select2(sigma_defuse, n1) = use)),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(423,plain,
% 9.76/9.92 (a_select2(sigma_defuse, n1) = use),
% 9.76/9.92 inference(and_elim,[status(thm)],[5])).
% 9.76/9.92 tff(424,plain,
% 9.76/9.92 (a_select2(sigma_defuse, n1) = use),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[423, 422])).
% 9.76/9.92 tff(425,assumption,(succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))), introduced(assumption)).
% 9.76/9.92 tff(426,plain,
% 9.76/9.92 (succ(succ(succ(succ(n3)))) = succ(succ(succ(succ(succ(succ(E!13))))))),
% 9.76/9.92 inference(symmetry,[status(thm)],[425])).
% 9.76/9.92 tff(427,plain,
% 9.76/9.92 (succ(succ(succ(succ(succ(n2))))) = succ(succ(succ(succ(succ(succ(E!13))))))),
% 9.76/9.92 inference(transitivity,[status(thm)],[104, 120, 116, 426])).
% 9.76/9.92 tff(428,plain,
% 9.76/9.92 (pred(succ(succ(succ(succ(succ(n2)))))) = pred(succ(succ(succ(succ(succ(succ(E!13)))))))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[427])).
% 9.76/9.92 tff(429,plain,
% 9.76/9.92 (pred(succ(succ(succ(succ(succ(succ(E!13))))))) = pred(succ(succ(succ(succ(succ(n2))))))),
% 9.76/9.92 inference(symmetry,[status(thm)],[428])).
% 9.76/9.92 tff(430,plain,
% 9.76/9.92 (succ(succ(succ(succ(succ(E!13))))) = succ(succ(succ(succ(n2))))),
% 9.76/9.92 inference(transitivity,[status(thm)],[184, 429, 172])).
% 9.76/9.92 tff(431,plain,
% 9.76/9.92 (pred(succ(succ(succ(succ(succ(E!13)))))) = pred(succ(succ(succ(succ(n2)))))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[430])).
% 9.76/9.92 tff(432,plain,
% 9.76/9.92 (succ(succ(succ(succ(E!13)))) = n5),
% 9.76/9.92 inference(transitivity,[status(thm)],[189, 431, 170, 166])).
% 9.76/9.92 tff(433,plain,
% 9.76/9.92 (pred(succ(succ(succ(succ(E!13))))) = pred(n5)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[432])).
% 9.76/9.92 tff(434,plain,
% 9.76/9.92 (succ(succ(succ(E!13))) = n4),
% 9.76/9.92 inference(transitivity,[status(thm)],[194, 433, 164, 162])).
% 9.76/9.92 tff(435,plain,
% 9.76/9.92 (pred(succ(succ(succ(E!13)))) = pred(n4)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[434])).
% 9.76/9.92 tff(436,plain,
% 9.76/9.92 (succ(succ(E!13)) = n3),
% 9.76/9.92 inference(transitivity,[status(thm)],[199, 435, 160, 157])).
% 9.76/9.92 tff(437,plain,
% 9.76/9.92 (pred(succ(succ(E!13))) = pred(n3)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[436])).
% 9.76/9.92 tff(438,plain,
% 9.76/9.92 (succ(E!13) = n2),
% 9.76/9.92 inference(transitivity,[status(thm)],[204, 437, 155, 151])).
% 9.76/9.92 tff(439,plain,
% 9.76/9.92 (pred(succ(E!13)) = pred(n2)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[438])).
% 9.76/9.92 tff(440,plain,
% 9.76/9.92 (E!13 = n1),
% 9.76/9.92 inference(transitivity,[status(thm)],[209, 439, 149, 141])).
% 9.76/9.92 tff(441,plain,
% 9.76/9.92 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n1)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[440])).
% 9.76/9.92 tff(442,plain,
% 9.76/9.92 (a_select2(sigma_defuse, E!13) = use),
% 9.76/9.92 inference(transitivity,[status(thm)],[441, 424])).
% 9.76/9.92 tff(443,plain,
% 9.76/9.92 ($false),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[28, 442])).
% 9.76/9.92 tff(444,plain,(~(succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3)))))), inference(lemma,lemma(discharge,[]))).
% 9.76/9.92 tff(445,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | ((succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | (succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(446,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | ((succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(447,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | gt(X, Y))) | (succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[446, 445])).
% 9.76/9.92 tff(448,plain,
% 9.76/9.92 ((succ(succ(succ(succ(succ(succ(E!13)))))) = succ(succ(succ(succ(n3))))) | gt(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(succ(E!13))))))) | gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[447, 375])).
% 9.76/9.92 tff(449,plain,
% 9.76/9.92 (gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[448, 444, 421])).
% 9.76/9.92 tff(450,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))) | (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) <=> gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(451,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) <=> gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[450, 223])).
% 9.76/9.92 tff(452,plain,
% 9.76/9.92 ((~(leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) <=> gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))) | leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) | (~gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(453,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13)))))) | (~gt(succ(succ(succ(succ(succ(succ(E!13)))))), succ(succ(succ(succ(n3))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[452, 451])).
% 9.76/9.92 tff(454,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n3)))), succ(succ(succ(succ(succ(E!13))))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[453, 449])).
% 9.76/9.92 tff(455,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13))))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[454, 119])).
% 9.76/9.92 tff(456,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13)))))) <=> leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13))))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(457,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13)))))) <=> leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[456, 247])).
% 9.76/9.92 tff(458,plain,
% 9.76/9.92 ((~(leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13)))))) <=> leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13))))))) | (~leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13))))))) | leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(459,plain,
% 9.76/9.92 ((~leq(succ(succ(succ(succ(succ(n2))))), succ(succ(succ(succ(succ(E!13))))))) | leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[458, 457])).
% 9.76/9.92 tff(460,plain,
% 9.76/9.92 (leq(succ(succ(succ(succ(n2)))), succ(succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[459, 455])).
% 9.76/9.92 tff(461,plain,
% 9.76/9.92 (leq(succ(n5), succ(succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[460, 101])).
% 9.76/9.92 tff(462,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n5), succ(succ(succ(succ(E!13))))) <=> leq(n5, succ(succ(succ(E!13)))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(463,plain,
% 9.76/9.92 (leq(succ(n5), succ(succ(succ(succ(E!13))))) <=> leq(n5, succ(succ(succ(E!13))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[462, 247])).
% 9.76/9.92 tff(464,plain,
% 9.76/9.92 ((~(leq(succ(n5), succ(succ(succ(succ(E!13))))) <=> leq(n5, succ(succ(succ(E!13)))))) | (~leq(succ(n5), succ(succ(succ(succ(E!13)))))) | leq(n5, succ(succ(succ(E!13))))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(465,plain,
% 9.76/9.92 ((~leq(succ(n5), succ(succ(succ(succ(E!13)))))) | leq(n5, succ(succ(succ(E!13))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[464, 463])).
% 9.76/9.92 tff(466,plain,
% 9.76/9.92 (leq(n5, succ(succ(succ(E!13))))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[465, 461])).
% 9.76/9.92 tff(467,plain,
% 9.76/9.92 (leq(succ(n4), succ(succ(succ(E!13))))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[466, 60])).
% 9.76/9.92 tff(468,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n4), succ(succ(succ(E!13)))) <=> leq(n4, succ(succ(E!13))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(469,plain,
% 9.76/9.92 (leq(succ(n4), succ(succ(succ(E!13)))) <=> leq(n4, succ(succ(E!13)))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[468, 247])).
% 9.76/9.92 tff(470,plain,
% 9.76/9.92 ((~(leq(succ(n4), succ(succ(succ(E!13)))) <=> leq(n4, succ(succ(E!13))))) | (~leq(succ(n4), succ(succ(succ(E!13))))) | leq(n4, succ(succ(E!13)))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(471,plain,
% 9.76/9.92 ((~leq(succ(n4), succ(succ(succ(E!13))))) | leq(n4, succ(succ(E!13)))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[470, 469])).
% 9.76/9.92 tff(472,plain,
% 9.76/9.92 (leq(n4, succ(succ(E!13)))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[471, 467])).
% 9.76/9.92 tff(473,plain,
% 9.76/9.92 (leq(succ(n3), succ(succ(E!13)))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[472, 56])).
% 9.76/9.92 tff(474,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n3), succ(succ(E!13))) <=> leq(n3, succ(E!13)))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(475,plain,
% 9.76/9.92 (leq(succ(n3), succ(succ(E!13))) <=> leq(n3, succ(E!13))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[474, 247])).
% 9.76/9.92 tff(476,plain,
% 9.76/9.92 ((~(leq(succ(n3), succ(succ(E!13))) <=> leq(n3, succ(E!13)))) | (~leq(succ(n3), succ(succ(E!13)))) | leq(n3, succ(E!13))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(477,plain,
% 9.76/9.92 ((~leq(succ(n3), succ(succ(E!13)))) | leq(n3, succ(E!13))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[476, 475])).
% 9.76/9.92 tff(478,plain,
% 9.76/9.92 (leq(n3, succ(E!13))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[477, 473])).
% 9.76/9.92 tff(479,plain,
% 9.76/9.92 ((a_select2(sigma_defuse, n2) = use) <=> (a_select2(sigma_defuse, n2) = use)),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(480,plain,
% 9.76/9.92 (a_select2(sigma_defuse, n2) = use),
% 9.76/9.92 inference(and_elim,[status(thm)],[5])).
% 9.76/9.92 tff(481,plain,
% 9.76/9.92 (a_select2(sigma_defuse, n2) = use),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[480, 479])).
% 9.76/9.92 tff(482,assumption,(n3 = succ(E!13)), introduced(assumption)).
% 9.76/9.92 tff(483,plain,
% 9.76/9.92 (succ(E!13) = n3),
% 9.76/9.92 inference(symmetry,[status(thm)],[482])).
% 9.76/9.92 tff(484,plain,
% 9.76/9.92 (pred(succ(E!13)) = pred(n3)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[483])).
% 9.76/9.92 tff(485,plain,
% 9.76/9.92 (E!13 = n2),
% 9.76/9.92 inference(transitivity,[status(thm)],[209, 484, 155, 151])).
% 9.76/9.92 tff(486,plain,
% 9.76/9.92 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n2)),
% 9.76/9.92 inference(monotonicity,[status(thm)],[485])).
% 9.76/9.92 tff(487,plain,
% 9.76/9.92 (a_select2(sigma_defuse, E!13) = use),
% 9.76/9.92 inference(transitivity,[status(thm)],[486, 481])).
% 9.76/9.92 tff(488,plain,
% 9.76/9.92 ($false),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[28, 487])).
% 9.76/9.92 tff(489,plain,(~(n3 = succ(E!13))), inference(lemma,lemma(discharge,[]))).
% 9.76/9.92 tff(490,plain,
% 9.76/9.92 (^[X: $i, Y: $i] : refl(((X = Y) | gt(Y, X) | (~leq(X, Y))) <=> ((X = Y) | gt(Y, X) | (~leq(X, Y))))),
% 9.76/9.92 inference(bind,[status(th)],[])).
% 9.76/9.92 tff(491,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y))) <=> ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))),
% 9.76/9.92 inference(quant_intro,[status(thm)],[490])).
% 9.76/9.92 tff(492,plain,
% 9.76/9.92 (^[X: $i, Y: $i] : trans(monotonicity(trans(monotonicity(rewrite((leq(X, Y) & (~(X = Y))) <=> (~((~leq(X, Y)) | (X = Y)))), ((~(leq(X, Y) & (~(X = Y)))) <=> (~(~((~leq(X, Y)) | (X = Y)))))), rewrite((~(~((~leq(X, Y)) | (X = Y)))) <=> ((~leq(X, Y)) | (X = Y))), ((~(leq(X, Y) & (~(X = Y)))) <=> ((~leq(X, Y)) | (X = Y)))), (((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X)) <=> (((~leq(X, Y)) | (X = Y)) | gt(Y, X)))), rewrite((((~leq(X, Y)) | (X = Y)) | gt(Y, X)) <=> ((X = Y) | gt(Y, X) | (~leq(X, Y)))), (((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X)) <=> ((X = Y) | gt(Y, X) | (~leq(X, Y)))))),
% 9.76/9.92 inference(bind,[status(th)],[])).
% 9.76/9.92 tff(493,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X)) <=> ![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))),
% 9.76/9.92 inference(quant_intro,[status(thm)],[492])).
% 9.76/9.92 tff(494,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X)) <=> ![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(495,plain,
% 9.76/9.92 (^[X: $i, Y: $i] : rewrite(((leq(X, Y) & (~(X = Y))) => gt(Y, X)) <=> ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X)))),
% 9.76/9.92 inference(bind,[status(th)],[])).
% 9.76/9.92 tff(496,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((leq(X, Y) & (~(X = Y))) => gt(Y, X)) <=> ![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X))),
% 9.76/9.92 inference(quant_intro,[status(thm)],[495])).
% 9.76/9.92 tff(497,axiom,(![X: $i, Y: $i] : ((leq(X, Y) & (~(X = Y))) => gt(Y, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','leq_gt2')).
% 9.76/9.92 tff(498,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[497, 496])).
% 9.76/9.92 tff(499,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[498, 494])).
% 9.76/9.92 tff(500,plain,(
% 9.76/9.92 ![X: $i, Y: $i] : ((~(leq(X, Y) & (~(X = Y)))) | gt(Y, X))),
% 9.76/9.92 inference(skolemize,[status(sab)],[499])).
% 9.76/9.92 tff(501,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[500, 493])).
% 9.76/9.92 tff(502,plain,
% 9.76/9.92 (![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[501, 491])).
% 9.76/9.92 tff(503,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(504,plain,
% 9.76/9.92 (((n3 = succ(E!13)) | gt(succ(E!13), n3) | (~leq(n3, succ(E!13)))) <=> ((n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(505,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = succ(E!13)) | gt(succ(E!13), n3) | (~leq(n3, succ(E!13))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3)))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[504])).
% 9.76/9.92 tff(506,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = succ(E!13)) | gt(succ(E!13), n3) | (~leq(n3, succ(E!13))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3))),
% 9.76/9.92 inference(transitivity,[status(thm)],[505, 503])).
% 9.76/9.92 tff(507,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = succ(E!13)) | gt(succ(E!13), n3) | (~leq(n3, succ(E!13))))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(508,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3)),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[507, 506])).
% 9.76/9.92 tff(509,plain,
% 9.76/9.92 ((n3 = succ(E!13)) | (~leq(n3, succ(E!13))) | gt(succ(E!13), n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[508, 502])).
% 9.76/9.92 tff(510,plain,
% 9.76/9.92 (gt(succ(E!13), n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[509, 489, 478])).
% 9.76/9.92 tff(511,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(X, Y) <=> gt(succ(Y), X))) | (leq(n3, E!13) <=> gt(succ(E!13), n3))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(512,plain,
% 9.76/9.92 (leq(n3, E!13) <=> gt(succ(E!13), n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[511, 223])).
% 9.76/9.92 tff(513,plain,
% 9.76/9.92 ((~(leq(n3, E!13) <=> gt(succ(E!13), n3))) | leq(n3, E!13) | (~gt(succ(E!13), n3))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(514,plain,
% 9.76/9.92 (leq(n3, E!13) | (~gt(succ(E!13), n3))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[513, 512])).
% 9.76/9.92 tff(515,plain,
% 9.76/9.92 (leq(n3, E!13)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[514, 510])).
% 9.76/9.92 tff(516,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(517,plain,
% 9.76/9.92 (((n3 = E!13) | gt(E!13, n3) | (~leq(n3, E!13))) <=> ((~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3))),
% 9.76/9.92 inference(rewrite,[status(thm)],[])).
% 9.76/9.92 tff(518,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = E!13) | gt(E!13, n3) | (~leq(n3, E!13)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3)))),
% 9.76/9.92 inference(monotonicity,[status(thm)],[517])).
% 9.76/9.92 tff(519,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = E!13) | gt(E!13, n3) | (~leq(n3, E!13)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3))),
% 9.76/9.92 inference(transitivity,[status(thm)],[518, 516])).
% 9.76/9.92 tff(520,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n3 = E!13) | gt(E!13, n3) | (~leq(n3, E!13)))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(521,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3)),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[520, 519])).
% 9.76/9.92 tff(522,plain,
% 9.76/9.92 ((~leq(n3, E!13)) | (n3 = E!13) | gt(E!13, n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[521, 502])).
% 9.76/9.92 tff(523,plain,
% 9.76/9.92 (gt(E!13, n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[522, 515, 54])).
% 9.76/9.92 tff(524,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(n3, pred(E!13)) <=> gt(E!13, n3))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(525,plain,
% 9.76/9.92 (leq(n3, pred(E!13)) <=> gt(E!13, n3)),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[524, 232])).
% 9.76/9.92 tff(526,plain,
% 9.76/9.92 ((~(leq(n3, pred(E!13)) <=> gt(E!13, n3))) | leq(n3, pred(E!13)) | (~gt(E!13, n3))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(527,plain,
% 9.76/9.92 (leq(n3, pred(E!13)) | (~gt(E!13, n3))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[526, 525])).
% 9.76/9.92 tff(528,plain,
% 9.76/9.92 (leq(n3, pred(E!13))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[527, 523])).
% 9.76/9.92 tff(529,plain,
% 9.76/9.92 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n3), succ(pred(E!13))) <=> leq(n3, pred(E!13)))),
% 9.76/9.92 inference(quant_inst,[status(thm)],[])).
% 9.76/9.92 tff(530,plain,
% 9.76/9.92 (leq(succ(n3), succ(pred(E!13))) <=> leq(n3, pred(E!13))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[529, 247])).
% 9.76/9.92 tff(531,plain,
% 9.76/9.92 ((~(leq(succ(n3), succ(pred(E!13))) <=> leq(n3, pred(E!13)))) | leq(succ(n3), succ(pred(E!13))) | (~leq(n3, pred(E!13)))),
% 9.76/9.92 inference(tautology,[status(thm)],[])).
% 9.76/9.92 tff(532,plain,
% 9.76/9.92 (leq(succ(n3), succ(pred(E!13))) | (~leq(n3, pred(E!13)))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[531, 530])).
% 9.76/9.92 tff(533,plain,
% 9.76/9.92 (leq(succ(n3), succ(pred(E!13)))),
% 9.76/9.92 inference(unit_resolution,[status(thm)],[532, 528])).
% 9.76/9.92 tff(534,plain,
% 9.76/9.92 (leq(n4, E!13)),
% 9.76/9.92 inference(modus_ponens,[status(thm)],[533, 45])).
% 9.76/9.92 tff(535,plain,
% 9.76/9.92 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.93 tff(536,plain,
% 9.76/9.93 (((n4 = E!13) | gt(E!13, n4) | (~leq(n4, E!13))) <=> ((~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.93 tff(537,plain,
% 9.76/9.93 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = E!13) | gt(E!13, n4) | (~leq(n4, E!13)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4)))),
% 9.76/9.93 inference(monotonicity,[status(thm)],[536])).
% 9.76/9.93 tff(538,plain,
% 9.76/9.93 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = E!13) | gt(E!13, n4) | (~leq(n4, E!13)))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4))),
% 9.76/9.93 inference(transitivity,[status(thm)],[537, 535])).
% 9.76/9.93 tff(539,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = E!13) | gt(E!13, n4) | (~leq(n4, E!13)))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(540,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4)),
% 9.76/9.93 inference(modus_ponens,[status(thm)],[539, 538])).
% 9.76/9.93 tff(541,plain,
% 9.76/9.93 ((~leq(n4, E!13)) | (n4 = E!13) | gt(E!13, n4)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[540, 502])).
% 9.76/9.93 tff(542,plain,
% 9.76/9.93 (gt(E!13, n4)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[541, 534, 30])).
% 9.76/9.93 tff(543,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(n4, pred(E!13)) <=> gt(E!13, n4))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(544,plain,
% 9.76/9.93 (leq(n4, pred(E!13)) <=> gt(E!13, n4)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[543, 232])).
% 9.76/9.93 tff(545,plain,
% 9.76/9.93 ((~(leq(n4, pred(E!13)) <=> gt(E!13, n4))) | leq(n4, pred(E!13)) | (~gt(E!13, n4))),
% 9.76/9.93 inference(tautology,[status(thm)],[])).
% 9.76/9.93 tff(546,plain,
% 9.76/9.93 (leq(n4, pred(E!13)) | (~gt(E!13, n4))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[545, 544])).
% 9.76/9.93 tff(547,plain,
% 9.76/9.93 (leq(n4, pred(E!13))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[546, 542])).
% 9.76/9.93 tff(548,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : (leq(X, pred(Y)) <=> gt(Y, X))) | (leq(n4, pred(pred(E!13))) <=> gt(pred(E!13), n4))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(549,plain,
% 9.76/9.93 (leq(n4, pred(pred(E!13))) <=> gt(pred(E!13), n4)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[548, 232])).
% 9.76/9.93 tff(550,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n4), succ(pred(pred(E!13)))) <=> leq(n4, pred(pred(E!13))))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(551,plain,
% 9.76/9.93 (leq(succ(n4), succ(pred(pred(E!13)))) <=> leq(n4, pred(pred(E!13)))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[550, 247])).
% 9.76/9.93 tff(552,plain,
% 9.76/9.93 ((~![X: $i] : (succ(pred(X)) = X)) | (succ(pred(pred(E!13))) = pred(E!13))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(553,plain,
% 9.76/9.93 (succ(pred(pred(E!13))) = pred(E!13)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[552, 36])).
% 9.76/9.93 tff(554,plain,
% 9.76/9.93 (leq(succ(n4), succ(pred(pred(E!13)))) <=> leq(n5, pred(E!13))),
% 9.76/9.93 inference(monotonicity,[status(thm)],[58, 553])).
% 9.76/9.93 tff(555,plain,
% 9.76/9.93 (leq(n5, pred(E!13)) <=> leq(succ(n4), succ(pred(pred(E!13))))),
% 9.76/9.93 inference(symmetry,[status(thm)],[554])).
% 9.76/9.93 tff(556,plain,
% 9.76/9.93 ((~leq(n5, pred(E!13))) <=> (~leq(succ(n4), succ(pred(pred(E!13)))))),
% 9.76/9.93 inference(monotonicity,[status(thm)],[555])).
% 9.76/9.93 tff(557,plain,
% 9.76/9.93 ((~![X: $i, Y: $i] : (leq(succ(X), succ(Y)) <=> leq(X, Y))) | (leq(succ(n5), succ(pred(E!13))) <=> leq(n5, pred(E!13)))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(558,plain,
% 9.76/9.93 (leq(succ(n5), succ(pred(E!13))) <=> leq(n5, pred(E!13))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[557, 247])).
% 9.76/9.93 tff(559,plain,
% 9.76/9.93 (leq(succ(n5), succ(pred(E!13))) <=> leq(succ(succ(succ(succ(n2)))), E!13)),
% 9.76/9.93 inference(monotonicity,[status(thm)],[99, 38])).
% 9.76/9.93 tff(560,plain,
% 9.76/9.93 (leq(succ(succ(succ(succ(n2)))), E!13) <=> leq(succ(n5), succ(pred(E!13)))),
% 9.76/9.93 inference(symmetry,[status(thm)],[559])).
% 9.76/9.93 tff(561,plain,
% 9.76/9.93 ((~leq(succ(succ(succ(succ(n2)))), E!13)) <=> (~leq(succ(n5), succ(pred(E!13))))),
% 9.76/9.93 inference(monotonicity,[status(thm)],[560])).
% 9.76/9.93 tff(562,plain,
% 9.76/9.93 (leq(E!13, n5)),
% 9.76/9.93 inference(and_elim,[status(thm)],[275])).
% 9.76/9.93 tff(563,plain,
% 9.76/9.93 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.93 tff(564,plain,
% 9.76/9.93 ((leq(succ(succ(succ(succ(n2)))), n5) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13))) <=> ((~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.93 tff(565,plain,
% 9.76/9.93 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n2)))), n5) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | ((~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5)))),
% 9.76/9.93 inference(monotonicity,[status(thm)],[564])).
% 9.76/9.93 tff(566,plain,
% 9.76/9.93 (((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n2)))), n5) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)))) <=> ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5))),
% 9.76/9.93 inference(transitivity,[status(thm)],[565, 563])).
% 9.76/9.93 tff(567,plain,
% 9.76/9.93 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (leq(succ(succ(succ(succ(n2)))), n5) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)))),
% 9.76/9.93 inference(quant_inst,[status(thm)],[])).
% 9.76/9.93 tff(568,plain,
% 9.76/9.93 ((~![X: $i, Y: $i, Z: $i] : (leq(X, Z) | (~leq(Y, Z)) | (~leq(X, Y)))) | (~leq(E!13, n5)) | (~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.93 inference(modus_ponens,[status(thm)],[567, 566])).
% 9.76/9.93 tff(569,plain,
% 9.76/9.93 ((~leq(succ(succ(succ(succ(n2)))), E!13)) | leq(succ(succ(succ(succ(n2)))), n5)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[568, 326, 562])).
% 9.76/9.93 tff(570,plain,
% 9.76/9.93 (~leq(succ(succ(succ(succ(n2)))), E!13)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[569, 404])).
% 9.76/9.93 tff(571,plain,
% 9.76/9.93 (~leq(succ(n5), succ(pred(E!13)))),
% 9.76/9.93 inference(modus_ponens,[status(thm)],[570, 561])).
% 9.76/9.93 tff(572,plain,
% 9.76/9.93 ((~(leq(succ(n5), succ(pred(E!13))) <=> leq(n5, pred(E!13)))) | leq(succ(n5), succ(pred(E!13))) | (~leq(n5, pred(E!13)))),
% 9.76/9.93 inference(tautology,[status(thm)],[])).
% 9.76/9.93 tff(573,plain,
% 9.76/9.93 (~leq(n5, pred(E!13))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[572, 571, 558])).
% 9.76/9.93 tff(574,plain,
% 9.76/9.93 (~leq(succ(n4), succ(pred(pred(E!13))))),
% 9.76/9.93 inference(modus_ponens,[status(thm)],[573, 556])).
% 9.76/9.93 tff(575,plain,
% 9.76/9.93 ((~(leq(succ(n4), succ(pred(pred(E!13)))) <=> leq(n4, pred(pred(E!13))))) | leq(succ(n4), succ(pred(pred(E!13)))) | (~leq(n4, pred(pred(E!13))))),
% 9.76/9.93 inference(tautology,[status(thm)],[])).
% 9.76/9.93 tff(576,plain,
% 9.76/9.93 (~leq(n4, pred(pred(E!13)))),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[575, 574, 551])).
% 9.76/9.93 tff(577,plain,
% 9.76/9.93 ((~(leq(n4, pred(pred(E!13))) <=> gt(pred(E!13), n4))) | leq(n4, pred(pred(E!13))) | (~gt(pred(E!13), n4))),
% 9.76/9.93 inference(tautology,[status(thm)],[])).
% 9.76/9.93 tff(578,plain,
% 9.76/9.93 (~gt(pred(E!13), n4)),
% 9.76/9.93 inference(unit_resolution,[status(thm)],[577, 576, 549])).
% 9.76/9.93 tff(579,plain,
% 9.76/9.93 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.93 tff(580,plain,
% 9.76/9.93 (((n4 = pred(E!13)) | gt(pred(E!13), n4) | (~leq(n4, pred(E!13)))) <=> ((~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4))),
% 9.76/9.93 inference(rewrite,[status(thm)],[])).
% 9.76/9.97 tff(581,plain,
% 9.76/9.97 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = pred(E!13)) | gt(pred(E!13), n4) | (~leq(n4, pred(E!13))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4)))),
% 9.76/9.97 inference(monotonicity,[status(thm)],[580])).
% 9.76/9.97 tff(582,plain,
% 9.76/9.97 (((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = pred(E!13)) | gt(pred(E!13), n4) | (~leq(n4, pred(E!13))))) <=> ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4))),
% 9.76/9.97 inference(transitivity,[status(thm)],[581, 579])).
% 9.76/9.97 tff(583,plain,
% 9.76/9.97 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | ((n4 = pred(E!13)) | gt(pred(E!13), n4) | (~leq(n4, pred(E!13))))),
% 9.76/9.97 inference(quant_inst,[status(thm)],[])).
% 9.76/9.97 tff(584,plain,
% 9.76/9.97 ((~![X: $i, Y: $i] : ((X = Y) | gt(Y, X) | (~leq(X, Y)))) | (~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4)),
% 9.76/9.97 inference(modus_ponens,[status(thm)],[583, 582])).
% 9.76/9.97 tff(585,plain,
% 9.76/9.97 ((~leq(n4, pred(E!13))) | (n4 = pred(E!13)) | gt(pred(E!13), n4)),
% 9.76/9.97 inference(unit_resolution,[status(thm)],[584, 502])).
% 9.76/9.97 tff(586,plain,
% 9.76/9.97 ((~leq(n4, pred(E!13))) | (n4 = pred(E!13))),
% 9.76/9.97 inference(unit_resolution,[status(thm)],[585, 578])).
% 9.76/9.97 tff(587,plain,
% 9.76/9.97 (n4 = pred(E!13)),
% 9.76/9.97 inference(unit_resolution,[status(thm)],[586, 547])).
% 9.76/9.97 tff(588,plain,
% 9.76/9.97 (pred(E!13) = n4),
% 9.76/9.97 inference(symmetry,[status(thm)],[587])).
% 9.76/9.97 tff(589,plain,
% 9.76/9.97 (pred(E!13) = succ(succ(succ(succ(n0))))),
% 9.76/9.97 inference(transitivity,[status(thm)],[588, 14])).
% 9.76/9.97 tff(590,plain,
% 9.76/9.97 (succ(pred(E!13)) = succ(succ(succ(succ(succ(n0)))))),
% 9.76/9.97 inference(monotonicity,[status(thm)],[589])).
% 9.76/9.97 tff(591,plain,
% 9.76/9.97 (E!13 = succ(pred(E!13))),
% 9.76/9.97 inference(symmetry,[status(thm)],[38])).
% 9.76/9.97 tff(592,plain,
% 9.76/9.97 (E!13 = n5),
% 9.76/9.97 inference(transitivity,[status(thm)],[591, 590, 10])).
% 9.76/9.97 tff(593,plain,
% 9.76/9.97 (a_select2(sigma_defuse, E!13) = a_select2(sigma_defuse, n5)),
% 9.76/9.97 inference(monotonicity,[status(thm)],[592])).
% 9.76/9.97 tff(594,plain,
% 9.76/9.97 (a_select2(sigma_defuse, E!13) = use),
% 9.76/9.97 inference(transitivity,[status(thm)],[593, 7])).
% 9.76/9.97 tff(595,plain,
% 9.76/9.97 ($false),
% 9.76/9.97 inference(unit_resolution,[status(thm)],[28, 594])).
% 9.76/9.97 % SZS output end Proof
% 9.83/9.98 % E exiting
%------------------------------------------------------------------------------