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