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