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