%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV089+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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 0.77s 0.96s
% Output : Proof 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV089+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 09:28:33 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.77/0.96 % SZS status Theorem
% 0.77/0.96 % SZS output start Proof
% 0.77/0.96 tff(use_type, type, (
% 0.77/0.96 use: $i)).
% 0.77/0.96 tff(a_select2_type, type, (
% 0.77/0.96 a_select2: ( $i * $i ) > $i)).
% 0.77/0.96 tff(n4_type, type, (
% 0.77/0.96 n4: $i)).
% 0.77/0.96 tff(tptp_update2_type, type, (
% 0.77/0.96 tptp_update2: ( $i * $i * $i ) > $i)).
% 0.77/0.96 tff(n3_type, type, (
% 0.77/0.96 n3: $i)).
% 0.77/0.96 tff(n5_type, type, (
% 0.77/0.96 n5: $i)).
% 0.77/0.96 tff(xinit_defuse_type, type, (
% 0.77/0.96 xinit_defuse: $i)).
% 0.77/0.96 tff(gt_type, type, (
% 0.77/0.96 gt: ( $i * $i ) > $o)).
% 0.77/0.96 tff(succ_type, type, (
% 0.77/0.96 succ: $i > $i)).
% 0.77/0.96 tff(n2_type, type, (
% 0.77/0.96 n2: $i)).
% 0.77/0.96 tff(n0_type, type, (
% 0.77/0.96 n0: $i)).
% 0.77/0.96 tff(a_select3_type, type, (
% 0.77/0.96 a_select3: ( $i * $i * $i ) > $i)).
% 0.77/0.96 tff(n1_type, type, (
% 0.77/0.96 n1: $i)).
% 0.77/0.96 tff(tptp_update3_type, type, (
% 0.77/0.96 tptp_update3: ( $i * $i * $i * $i ) > $i)).
% 0.77/0.96 tff(u_defuse_type, type, (
% 0.77/0.96 u_defuse: $i)).
% 0.77/0.96 tff(true_type, type, (
% 0.77/0.96 true: $o)).
% 0.77/0.96 tff(1,plain,
% 0.77/0.96 ((succ(succ(n0)) = n2) <=> (succ(succ(n0)) = n2)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(2,axiom,(succ(succ(n0)) = n2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','successor_2')).
% 0.77/0.96 tff(3,plain,
% 0.77/0.96 (succ(succ(n0)) = n2),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.77/0.96 tff(4,plain,
% 0.77/0.96 (n2 = succ(succ(n0))),
% 0.77/0.96 inference(symmetry,[status(thm)],[3])).
% 0.77/0.96 tff(5,plain,
% 0.77/0.96 (succ(n2) = succ(succ(succ(n0)))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[4])).
% 0.77/0.96 tff(6,plain,
% 0.77/0.96 (succ(succ(succ(n0))) = succ(n2)),
% 0.77/0.96 inference(symmetry,[status(thm)],[5])).
% 0.77/0.96 tff(7,plain,
% 0.77/0.96 ((succ(succ(succ(n0))) = n3) <=> (succ(succ(succ(n0))) = n3)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(8,axiom,(succ(succ(succ(n0))) = n3), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','successor_3')).
% 0.77/0.96 tff(9,plain,
% 0.77/0.96 (succ(succ(succ(n0))) = n3),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.77/0.96 tff(10,plain,
% 0.77/0.96 (n3 = succ(succ(succ(n0)))),
% 0.77/0.96 inference(symmetry,[status(thm)],[9])).
% 0.77/0.96 tff(11,assumption,(n3 = n4), introduced(assumption)).
% 0.77/0.96 tff(12,plain,
% 0.77/0.96 (n4 = n3),
% 0.77/0.96 inference(symmetry,[status(thm)],[11])).
% 0.77/0.96 tff(13,plain,
% 0.77/0.96 (n4 = succ(n2)),
% 0.77/0.96 inference(transitivity,[status(thm)],[12, 10, 6])).
% 0.77/0.96 tff(14,plain,
% 0.77/0.96 (gt(n4, n3) <=> gt(succ(n2), n3)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[13])).
% 0.77/0.96 tff(15,plain,
% 0.77/0.96 (gt(succ(n2), n3) <=> gt(n4, n3)),
% 0.77/0.96 inference(symmetry,[status(thm)],[14])).
% 0.77/0.96 tff(16,plain,
% 0.77/0.96 ((~gt(succ(n2), n3)) <=> (~gt(n4, n3))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[15])).
% 0.77/0.96 tff(17,plain,
% 0.77/0.96 (n3 = succ(n2)),
% 0.77/0.96 inference(transitivity,[status(thm)],[10, 6])).
% 0.77/0.96 tff(18,plain,
% 0.77/0.96 (gt(n3, n3) <=> gt(succ(n2), n3)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[17])).
% 0.77/0.96 tff(19,plain,
% 0.77/0.96 ((~gt(n3, n3)) <=> (~gt(succ(n2), n3))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[18])).
% 0.77/0.96 tff(20,plain,
% 0.77/0.96 (^[X: $i] : refl((~gt(X, X)) <=> (~gt(X, X)))),
% 0.77/0.96 inference(bind,[status(th)],[])).
% 0.77/0.96 tff(21,plain,
% 0.77/0.96 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 0.77/0.96 inference(quant_intro,[status(thm)],[20])).
% 0.77/0.96 tff(22,plain,
% 0.77/0.96 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(23,axiom,(![X: $i] : (~gt(X, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','irreflexivity_gt')).
% 0.77/0.96 tff(24,plain,
% 0.77/0.96 (![X: $i] : (~gt(X, X))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.77/0.96 tff(25,plain,(
% 0.77/0.96 ![X: $i] : (~gt(X, X))),
% 0.77/0.96 inference(skolemize,[status(sab)],[24])).
% 0.77/0.96 tff(26,plain,
% 0.77/0.96 (![X: $i] : (~gt(X, X))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[25, 21])).
% 0.77/0.96 tff(27,plain,
% 0.77/0.96 ((~![X: $i] : (~gt(X, X))) | (~gt(n3, n3))),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(28,plain,
% 0.77/0.96 (~gt(n3, n3)),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.77/0.96 tff(29,plain,
% 0.77/0.96 (~gt(succ(n2), n3)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[28, 19])).
% 0.77/0.96 tff(30,plain,
% 0.77/0.96 (~gt(n4, n3)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[29, 16])).
% 0.77/0.96 tff(31,plain,
% 0.77/0.96 (gt(n4, n3) <=> gt(n4, n3)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(32,axiom,(gt(n4, n3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt_4_3')).
% 0.77/0.96 tff(33,plain,
% 0.77/0.96 (gt(n4, n3)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.77/0.96 tff(34,plain,
% 0.77/0.96 ($false),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[33, 30])).
% 0.77/0.96 tff(35,plain,(~(n3 = n4)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.96 tff(36,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(37,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(38,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(elim_unused_vars,[status(thm)],[])).
% 0.77/0.96 tff(39,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.77/0.96 tff(40,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(transitivity,[status(thm)],[39, 38])).
% 0.77/0.96 tff(41,plain,
% 0.77/0.96 (^[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)))),
% 0.77/0.96 inference(bind,[status(th)],[])).
% 0.77/0.96 tff(42,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(quant_intro,[status(thm)],[41])).
% 0.77/0.96 tff(43,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(transitivity,[status(thm)],[42, 40])).
% 0.77/0.96 tff(44,axiom,(![I: $i, U: $i, X: $i, VAL: $i, VAL2: $i] : (((~(I = U)) & (a_select2(X, U) = VAL)) => (a_select2(tptp_update2(X, I, VAL2), U) = VAL))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','sel2_update_2')).
% 0.77/0.96 tff(45,plain,
% 0.77/0.96 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.77/0.96 tff(46,plain,
% 0.77/0.96 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[45, 37])).
% 0.77/0.96 tff(47,plain,(
% 0.77/0.96 ![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 0.77/0.96 inference(skolemize,[status(sab)],[46])).
% 0.77/0.96 tff(48,plain,
% 0.77/0.96 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[47, 36])).
% 0.77/0.96 tff(49,plain,
% 0.77/0.96 (((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4)) | (n3 = n4))) <=> ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4)) | (n3 = n4))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(50,plain,
% 0.77/0.96 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4)) | (n3 = n4))),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(51,plain,
% 0.77/0.96 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4)) | (n3 = n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.77/0.96 tff(52,plain,
% 0.77/0.96 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4)),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[51, 48, 35])).
% 0.77/0.96 tff(53,plain,
% 0.77/0.96 ((a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4) = use)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[52])).
% 0.77/0.96 tff(54,plain,
% 0.77/0.96 ((a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4) = use) <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)),
% 0.77/0.96 inference(symmetry,[status(thm)],[53])).
% 0.77/0.96 tff(55,plain,
% 0.77/0.96 (![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)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(56,plain,
% 0.77/0.96 (![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)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(57,axiom,(![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','sel2_update_1')).
% 0.77/0.96 tff(58,plain,
% 0.77/0.96 (![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.77/0.96 tff(59,plain,(
% 0.77/0.96 ![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 0.77/0.96 inference(skolemize,[status(sab)],[58])).
% 0.77/0.96 tff(60,plain,
% 0.77/0.96 (![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[59, 55])).
% 0.77/0.96 tff(61,plain,
% 0.77/0.96 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4) = use)),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(62,plain,
% 0.77/0.96 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n4) = use),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[61, 60])).
% 0.77/0.96 tff(63,plain,
% 0.77/0.96 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[62, 54])).
% 0.77/0.96 tff(64,plain,
% 0.77/0.96 (succ(n3) = succ(succ(succ(succ(n0))))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[10])).
% 0.77/0.96 tff(65,plain,
% 0.77/0.96 (succ(succ(succ(succ(n0)))) = succ(n3)),
% 0.77/0.96 inference(symmetry,[status(thm)],[64])).
% 0.77/0.96 tff(66,plain,
% 0.77/0.96 ((succ(succ(succ(succ(n0)))) = n4) <=> (succ(succ(succ(succ(n0)))) = n4)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(67,axiom,(succ(succ(succ(succ(n0)))) = n4), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','successor_4')).
% 0.77/0.96 tff(68,plain,
% 0.77/0.96 (succ(succ(succ(succ(n0)))) = n4),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.77/0.96 tff(69,plain,
% 0.77/0.96 (n4 = succ(succ(succ(succ(n0))))),
% 0.77/0.96 inference(symmetry,[status(thm)],[68])).
% 0.77/0.96 tff(70,assumption,(n4 = n5), introduced(assumption)).
% 0.77/0.96 tff(71,plain,
% 0.77/0.96 (n5 = n4),
% 0.77/0.96 inference(symmetry,[status(thm)],[70])).
% 0.77/0.96 tff(72,plain,
% 0.77/0.96 (n5 = succ(n3)),
% 0.77/0.96 inference(transitivity,[status(thm)],[71, 69, 65])).
% 0.77/0.96 tff(73,plain,
% 0.77/0.96 (gt(n5, n4) <=> gt(succ(n3), n4)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[72])).
% 0.77/0.96 tff(74,plain,
% 0.77/0.96 (gt(succ(n3), n4) <=> gt(n5, n4)),
% 0.77/0.96 inference(symmetry,[status(thm)],[73])).
% 0.77/0.96 tff(75,plain,
% 0.77/0.96 ((~gt(succ(n3), n4)) <=> (~gt(n5, n4))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[74])).
% 0.77/0.96 tff(76,plain,
% 0.77/0.96 (n4 = succ(n3)),
% 0.77/0.96 inference(transitivity,[status(thm)],[69, 65])).
% 0.77/0.96 tff(77,plain,
% 0.77/0.96 (gt(n4, n4) <=> gt(succ(n3), n4)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[76])).
% 0.77/0.96 tff(78,plain,
% 0.77/0.96 ((~gt(n4, n4)) <=> (~gt(succ(n3), n4))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[77])).
% 0.77/0.96 tff(79,plain,
% 0.77/0.96 ((~![X: $i] : (~gt(X, X))) | (~gt(n4, n4))),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(80,plain,
% 0.77/0.96 (~gt(n4, n4)),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[79, 26])).
% 0.77/0.96 tff(81,plain,
% 0.77/0.96 (~gt(succ(n3), n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[80, 78])).
% 0.77/0.96 tff(82,plain,
% 0.77/0.96 (~gt(n5, n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[81, 75])).
% 0.77/0.96 tff(83,plain,
% 0.77/0.96 (gt(n5, n4) <=> gt(n5, n4)),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(84,axiom,(gt(n5, n4)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt_5_4')).
% 0.77/0.96 tff(85,plain,
% 0.77/0.96 (gt(n5, n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.77/0.96 tff(86,plain,
% 0.77/0.96 ($false),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[85, 82])).
% 0.77/0.96 tff(87,plain,(~(n4 = n5)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.96 tff(88,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5))), introduced(assumption)).
% 0.77/0.96 tff(89,plain,
% 0.77/0.96 (((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)) | (n4 = n5))) <=> ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)) | (n4 = n5))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(90,plain,
% 0.77/0.96 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)) | (n4 = n5))),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(91,plain,
% 0.77/0.96 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)) | (n4 = n5)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.77/0.96 tff(92,plain,
% 0.77/0.96 ($false),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[91, 48, 88, 87])).
% 0.77/0.96 tff(93,plain,(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.96 tff(94,plain,
% 0.77/0.96 ((~![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)) | (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5) = use)),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(95,plain,
% 0.77/0.96 (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5) = use),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[94, 60])).
% 0.77/0.96 tff(96,assumption,(n3 = n5), introduced(assumption)).
% 0.77/0.96 tff(97,plain,
% 0.77/0.96 (n5 = n3),
% 0.77/0.96 inference(symmetry,[status(thm)],[96])).
% 0.77/0.96 tff(98,plain,
% 0.77/0.96 (n5 = succ(n2)),
% 0.77/0.96 inference(transitivity,[status(thm)],[97, 10, 6])).
% 0.77/0.96 tff(99,plain,
% 0.77/0.96 (gt(n5, n4) <=> gt(succ(n2), n4)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[98])).
% 0.77/0.96 tff(100,plain,
% 0.77/0.96 (gt(succ(n2), n4) <=> gt(n5, n4)),
% 0.77/0.96 inference(symmetry,[status(thm)],[99])).
% 0.77/0.96 tff(101,plain,
% 0.77/0.96 ((~gt(succ(n2), n4)) <=> (~gt(n5, n4))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[100])).
% 0.77/0.96 tff(102,plain,
% 0.77/0.96 (gt(n3, n4) <=> gt(succ(n2), n4)),
% 0.77/0.96 inference(monotonicity,[status(thm)],[17])).
% 0.77/0.96 tff(103,plain,
% 0.77/0.96 ((~gt(n3, n4)) <=> (~gt(succ(n2), n4))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[102])).
% 0.77/0.96 tff(104,plain,
% 0.77/0.96 (![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)))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(105,plain,
% 0.77/0.96 (^[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)))))),
% 0.77/0.96 inference(bind,[status(th)],[])).
% 0.77/0.96 tff(106,plain,
% 0.77/0.96 (![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)))),
% 0.77/0.96 inference(quant_intro,[status(thm)],[105])).
% 0.77/0.96 tff(107,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(108,plain,
% 0.77/0.96 (^[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)))),
% 0.77/0.96 inference(bind,[status(th)],[])).
% 0.77/0.96 tff(109,plain,
% 0.77/0.96 (![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))),
% 0.77/0.96 inference(quant_intro,[status(thm)],[108])).
% 0.77/0.96 tff(110,axiom,(![X: $i, Y: $i, Z: $i] : ((gt(X, Y) & gt(Y, Z)) => gt(X, Z))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','transitivity_gt')).
% 0.77/0.96 tff(111,plain,
% 0.77/0.96 (![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[110, 109])).
% 0.77/0.96 tff(112,plain,
% 0.77/0.96 (![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[111, 107])).
% 0.77/0.96 tff(113,plain,(
% 0.77/0.96 ![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 0.77/0.96 inference(skolemize,[status(sab)],[112])).
% 0.77/0.96 tff(114,plain,
% 0.77/0.96 (![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[113, 106])).
% 0.77/0.96 tff(115,plain,
% 0.77/0.96 (![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[114, 104])).
% 0.77/0.96 tff(116,plain,
% 0.77/0.96 (((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | ((~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4)))) <=> ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4)))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(117,plain,
% 0.77/0.96 ((gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3))) <=> ((~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4)))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(118,plain,
% 0.77/0.96 (((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3)))) <=> ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | ((~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4))))),
% 0.77/0.96 inference(monotonicity,[status(thm)],[117])).
% 0.77/0.96 tff(119,plain,
% 0.77/0.96 (((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3)))) <=> ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4)))),
% 0.77/0.96 inference(transitivity,[status(thm)],[118, 116])).
% 0.77/0.96 tff(120,plain,
% 0.77/0.96 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3)))),
% 0.77/0.96 inference(quant_inst,[status(thm)],[])).
% 0.77/0.96 tff(121,plain,
% 0.77/0.96 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4))),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[120, 119])).
% 0.77/0.96 tff(122,plain,
% 0.77/0.96 (~gt(n3, n4)),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[121, 115, 33, 28])).
% 0.77/0.96 tff(123,plain,
% 0.77/0.96 (~gt(succ(n2), n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[122, 103])).
% 0.77/0.96 tff(124,plain,
% 0.77/0.96 (~gt(n5, n4)),
% 0.77/0.96 inference(modus_ponens,[status(thm)],[123, 101])).
% 0.77/0.96 tff(125,plain,
% 0.77/0.96 ($false),
% 0.77/0.96 inference(unit_resolution,[status(thm)],[85, 124])).
% 0.77/0.96 tff(126,plain,(~(n3 = n5)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.96 tff(127,plain,
% 0.77/0.96 (((~![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))) | ((n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)))) <=> ((~![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))) | (n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(128,plain,
% 0.77/0.96 (((a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)) | (n3 = n5)) <=> ((n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)))),
% 0.77/0.96 inference(rewrite,[status(thm)],[])).
% 0.77/0.96 tff(129,plain,
% 0.77/0.96 (((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)) | (n3 = n5))) <=> ((~![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))) | ((n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5))))),
% 0.77/0.97 inference(monotonicity,[status(thm)],[128])).
% 0.77/0.97 tff(130,plain,
% 0.77/0.97 (((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)) | (n3 = n5))) <=> ((~![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))) | (n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)))),
% 0.77/0.97 inference(transitivity,[status(thm)],[129, 127])).
% 0.77/0.97 tff(131,plain,
% 0.77/0.97 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)) | (n3 = n5))),
% 0.77/0.97 inference(quant_inst,[status(thm)],[])).
% 0.77/0.97 tff(132,plain,
% 0.77/0.97 ((~![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))) | (n3 = n5) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5))),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.77/0.97 tff(133,plain,
% 0.77/0.97 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n5)),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[132, 48, 126])).
% 0.77/0.97 tff(134,assumption,(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5)), introduced(assumption)).
% 0.77/0.97 tff(135,plain,
% 0.77/0.97 (((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5)) | (n3 = n5))) <=> ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5)) | (n3 = n5))),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(136,plain,
% 0.77/0.97 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5)) | (n3 = n5))),
% 0.77/0.97 inference(quant_inst,[status(thm)],[])).
% 0.77/0.97 tff(137,plain,
% 0.77/0.97 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5)) | (n3 = n5)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.77/0.97 tff(138,plain,
% 0.77/0.97 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5)),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[137, 48, 126])).
% 0.77/0.97 tff(139,plain,
% 0.77/0.97 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use),
% 0.77/0.97 inference(transitivity,[status(thm)],[138, 134, 133, 95])).
% 0.77/0.97 tff(140,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)), introduced(assumption)).
% 0.77/0.97 tff(141,plain,
% 0.77/0.97 ($false),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[140, 139])).
% 0.77/0.97 tff(142,plain,((~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n5) = a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n5))) | (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.97 tff(143,plain,
% 0.77/0.97 (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[142, 93])).
% 0.77/0.97 tff(144,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)), introduced(assumption)).
% 0.77/0.97 tff(145,plain,
% 0.77/0.97 ((~![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_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)),
% 0.77/0.97 inference(quant_inst,[status(thm)],[])).
% 0.77/0.97 tff(146,plain,
% 0.77/0.97 ($false),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[145, 60, 144])).
% 0.77/0.97 tff(147,plain,(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use), inference(lemma,lemma(discharge,[]))).
% 0.77/0.97 tff(148,plain,
% 0.77/0.97 (![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL) <=> ![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(149,plain,
% 0.77/0.97 (![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL) <=> ![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(150,axiom,(![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','sel3_update_1')).
% 0.77/0.97 tff(151,plain,
% 0.77/0.97 (![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[150, 149])).
% 0.77/0.97 tff(152,plain,(
% 0.77/0.97 ![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)),
% 0.77/0.97 inference(skolemize,[status(sab)],[151])).
% 0.77/0.97 tff(153,plain,
% 0.77/0.97 (![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[152, 148])).
% 0.77/0.97 tff(154,plain,
% 0.77/0.97 ((~![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0) = use)),
% 0.77/0.97 inference(quant_inst,[status(thm)],[])).
% 0.77/0.97 tff(155,plain,
% 0.77/0.97 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0) = use),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[154, 153])).
% 0.77/0.97 tff(156,assumption,(n0 = n1), introduced(assumption)).
% 0.77/0.97 tff(157,plain,
% 0.77/0.97 ((succ(n0) = n1) <=> (succ(n0) = n1)),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(158,axiom,(succ(n0) = n1), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','successor_1')).
% 0.77/0.97 tff(159,plain,
% 0.77/0.97 (succ(n0) = n1),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[158, 157])).
% 0.77/0.97 tff(160,plain,
% 0.77/0.97 (n1 = succ(n0)),
% 0.77/0.97 inference(symmetry,[status(thm)],[159])).
% 0.77/0.97 tff(161,plain,
% 0.77/0.97 (gt(n1, n0) <=> gt(succ(n0), n1)),
% 0.77/0.97 inference(monotonicity,[status(thm)],[160, 156])).
% 0.77/0.97 tff(162,plain,
% 0.77/0.97 (gt(succ(n0), n1) <=> gt(n1, n0)),
% 0.77/0.97 inference(symmetry,[status(thm)],[161])).
% 0.77/0.97 tff(163,plain,
% 0.77/0.97 ((~gt(succ(n0), n1)) <=> (~gt(n1, n0))),
% 0.77/0.97 inference(monotonicity,[status(thm)],[162])).
% 0.77/0.97 tff(164,plain,
% 0.77/0.97 (gt(n1, n1) <=> gt(succ(n0), n1)),
% 0.77/0.97 inference(monotonicity,[status(thm)],[160])).
% 0.77/0.97 tff(165,plain,
% 0.77/0.97 ((~gt(n1, n1)) <=> (~gt(succ(n0), n1))),
% 0.77/0.97 inference(monotonicity,[status(thm)],[164])).
% 0.77/0.97 tff(166,plain,
% 0.77/0.97 ((~![X: $i] : (~gt(X, X))) | (~gt(n1, n1))),
% 0.77/0.97 inference(quant_inst,[status(thm)],[])).
% 0.77/0.97 tff(167,plain,
% 0.77/0.97 (~gt(n1, n1)),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[166, 26])).
% 0.77/0.97 tff(168,plain,
% 0.77/0.97 (~gt(succ(n0), n1)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[167, 165])).
% 0.77/0.97 tff(169,plain,
% 0.77/0.97 (~gt(n1, n0)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[168, 163])).
% 0.77/0.97 tff(170,plain,
% 0.77/0.97 (gt(n1, n0) <=> gt(n1, n0)),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(171,axiom,(gt(n1, n0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt_1_0')).
% 0.77/0.97 tff(172,plain,
% 0.77/0.97 (gt(n1, n0)),
% 0.77/0.97 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.77/0.97 tff(173,plain,
% 0.77/0.97 ($false),
% 0.77/0.97 inference(unit_resolution,[status(thm)],[172, 169])).
% 0.77/0.97 tff(174,plain,(~(n0 = n1)), inference(lemma,lemma(discharge,[]))).
% 0.77/0.97 tff(175,plain,
% 0.77/0.97 (^[I: $i, U: $i, V: $i, X: $i, VAL2: $i] : refl(((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V))) <=> ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V))))),
% 0.77/0.97 inference(bind,[status(th)],[])).
% 0.77/0.97 tff(176,plain,
% 0.77/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V))) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.77/0.97 inference(quant_intro,[status(thm)],[175])).
% 0.77/0.97 tff(177,plain,
% 0.77/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V))) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.77/0.97 inference(rewrite,[status(thm)],[])).
% 0.77/0.97 tff(178,plain,
% 0.77/0.97 (^[I: $i, U: $i, V: $i, X: $i, VAL2: $i] : rewrite(((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U)) <=> ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V))))),
% 0.77/0.97 inference(bind,[status(th)],[])).
% 0.77/0.97 tff(179,plain,
% 0.77/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U)) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.77/0.97 inference(quant_intro,[status(thm)],[178])).
% 0.77/0.97 tff(180,plain,
% 0.77/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U)) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U))),
% 0.81/0.97 inference(elim_unused_vars,[status(thm)],[])).
% 0.81/0.97 tff(181,plain,
% 0.81/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U))),
% 0.81/0.97 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.81/0.97 tff(182,plain,
% 0.81/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)) | (I = U))),
% 0.81/0.97 inference(transitivity,[status(thm)],[181, 180])).
% 0.81/0.97 tff(183,plain,
% 0.81/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(transitivity,[status(thm)],[182, 179])).
% 0.81/0.97 tff(184,plain,
% 0.81/0.97 (^[I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : trans(monotonicity(rewrite((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) <=> ((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))), (((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> (((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)))), rewrite((((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL))), (((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL))))),
% 0.81/0.97 inference(bind,[status(th)],[])).
% 0.81/0.97 tff(185,plain,
% 0.81/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((~((~(I = U)) & (J = V) & (a_select3(X, U, V) = VAL))) | (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL))),
% 0.81/0.97 inference(quant_intro,[status(thm)],[184])).
% 0.81/0.97 tff(186,plain,
% 0.81/0.97 (![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL)) <=> ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(transitivity,[status(thm)],[185, 183])).
% 0.81/0.97 tff(187,axiom,(![I: $i, J: $i, U: $i, V: $i, X: $i, VAL: $i, VAL2: $i] : ((((~(I = U)) & (J = V)) & (a_select3(X, U, V) = VAL)) => (a_select3(tptp_update3(X, I, J, VAL2), U, V) = VAL))), file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax','sel3_update_2')).
% 0.81/0.97 tff(188,plain,
% 0.81/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[187, 186])).
% 0.81/0.97 tff(189,plain,
% 0.81/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[188, 177])).
% 0.81/0.97 tff(190,plain,(
% 0.81/0.97 ![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(skolemize,[status(sab)],[189])).
% 0.81/0.97 tff(191,plain,
% 0.81/0.97 (![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[190, 176])).
% 0.81/0.97 tff(192,plain,
% 0.81/0.97 (((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n1) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0)))) <=> ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n1) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0)))),
% 0.81/0.97 inference(rewrite,[status(thm)],[])).
% 0.81/0.97 tff(193,plain,
% 0.81/0.97 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n1) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0)))),
% 0.81/0.97 inference(quant_inst,[status(thm)],[])).
% 0.81/0.97 tff(194,plain,
% 0.81/0.97 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n1) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0))),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[193, 192])).
% 0.81/0.97 tff(195,plain,
% 0.81/0.97 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n1, n0)),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[194, 191, 174])).
% 0.81/0.97 tff(196,plain,
% 0.81/0.97 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use),
% 0.81/0.97 inference(transitivity,[status(thm)],[195, 155])).
% 0.81/0.97 tff(197,assumption,(~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)), introduced(assumption)).
% 0.81/0.97 tff(198,plain,
% 0.81/0.97 ($false),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[197, 196])).
% 0.81/0.97 tff(199,plain,(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use), inference(lemma,lemma(discharge,[]))).
% 0.81/0.97 tff(200,assumption,(n0 = n2), introduced(assumption)).
% 0.81/0.97 tff(201,plain,
% 0.81/0.97 (gt(n1, n0) <=> gt(succ(n0), n2)),
% 0.81/0.97 inference(monotonicity,[status(thm)],[160, 200])).
% 0.81/0.97 tff(202,plain,
% 0.81/0.97 (gt(succ(n0), n2) <=> gt(n1, n0)),
% 0.81/0.97 inference(symmetry,[status(thm)],[201])).
% 0.81/0.97 tff(203,plain,
% 0.81/0.97 ((~gt(succ(n0), n2)) <=> (~gt(n1, n0))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[202])).
% 0.81/0.97 tff(204,plain,
% 0.81/0.97 (gt(n1, n2) <=> gt(succ(n0), n2)),
% 0.81/0.97 inference(monotonicity,[status(thm)],[160])).
% 0.81/0.97 tff(205,plain,
% 0.81/0.97 ((~gt(n1, n2)) <=> (~gt(succ(n0), n2))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[204])).
% 0.81/0.97 tff(206,plain,
% 0.81/0.97 (gt(n2, n1) <=> gt(n2, n1)),
% 0.81/0.97 inference(rewrite,[status(thm)],[])).
% 0.81/0.97 tff(207,axiom,(gt(n2, n1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt_2_1')).
% 0.81/0.97 tff(208,plain,
% 0.81/0.97 (gt(n2, n1)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[207, 206])).
% 0.81/0.97 tff(209,plain,
% 0.81/0.97 (((~![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)))),
% 0.81/0.97 inference(rewrite,[status(thm)],[])).
% 0.81/0.97 tff(210,plain,
% 0.81/0.97 ((gt(n1, n1) | (~gt(n1, n2)) | (~gt(n2, n1))) <=> ((~gt(n2, n1)) | gt(n1, n1) | (~gt(n1, n2)))),
% 0.81/0.97 inference(rewrite,[status(thm)],[])).
% 0.81/0.97 tff(211,plain,
% 0.81/0.97 (((~![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))))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[210])).
% 0.81/0.97 tff(212,plain,
% 0.81/0.97 (((~![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)))),
% 0.81/0.97 inference(transitivity,[status(thm)],[211, 209])).
% 0.81/0.97 tff(213,plain,
% 0.81/0.97 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (gt(n1, n1) | (~gt(n1, n2)) | (~gt(n2, n1)))),
% 0.81/0.97 inference(quant_inst,[status(thm)],[])).
% 0.81/0.97 tff(214,plain,
% 0.81/0.97 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (~gt(n2, n1)) | gt(n1, n1) | (~gt(n1, n2))),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[213, 212])).
% 0.81/0.97 tff(215,plain,
% 0.81/0.97 (~gt(n1, n2)),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[214, 115, 208, 167])).
% 0.81/0.97 tff(216,plain,
% 0.81/0.97 (~gt(succ(n0), n2)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[215, 205])).
% 0.81/0.97 tff(217,plain,
% 0.81/0.97 (~gt(n1, n0)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[216, 203])).
% 0.81/0.97 tff(218,plain,
% 0.81/0.97 ($false),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[172, 217])).
% 0.81/0.97 tff(219,plain,(~(n0 = n2)), inference(lemma,lemma(discharge,[]))).
% 0.81/0.97 tff(220,plain,
% 0.81/0.97 ((n1 = n2) <=> (n2 = n1)),
% 0.81/0.97 inference(commutativity,[status(thm)],[])).
% 0.81/0.97 tff(221,plain,
% 0.81/0.97 ((~(n1 = n2)) <=> (~(n2 = n1))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[220])).
% 0.81/0.97 tff(222,assumption,(n1 = n2), introduced(assumption)).
% 0.81/0.97 tff(223,plain,
% 0.81/0.97 (succ(n1) = succ(succ(n0))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[160])).
% 0.81/0.97 tff(224,plain,
% 0.81/0.97 (succ(succ(n0)) = succ(n1)),
% 0.81/0.97 inference(symmetry,[status(thm)],[223])).
% 0.81/0.97 tff(225,plain,
% 0.81/0.97 (n2 = succ(n1)),
% 0.81/0.97 inference(transitivity,[status(thm)],[4, 224])).
% 0.81/0.97 tff(226,plain,
% 0.81/0.97 (gt(n2, n1) <=> gt(succ(n1), n2)),
% 0.81/0.97 inference(monotonicity,[status(thm)],[225, 222])).
% 0.81/0.97 tff(227,plain,
% 0.81/0.97 (gt(succ(n1), n2) <=> gt(n2, n1)),
% 0.81/0.97 inference(symmetry,[status(thm)],[226])).
% 0.81/0.97 tff(228,plain,
% 0.81/0.97 ((~gt(succ(n1), n2)) <=> (~gt(n2, n1))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[227])).
% 0.81/0.97 tff(229,plain,
% 0.81/0.97 (gt(n2, n2) <=> gt(succ(n1), n2)),
% 0.81/0.97 inference(monotonicity,[status(thm)],[225])).
% 0.81/0.97 tff(230,plain,
% 0.81/0.97 ((~gt(n2, n2)) <=> (~gt(succ(n1), n2))),
% 0.81/0.97 inference(monotonicity,[status(thm)],[229])).
% 0.81/0.97 tff(231,plain,
% 0.81/0.97 ((~![X: $i] : (~gt(X, X))) | (~gt(n2, n2))),
% 0.81/0.97 inference(quant_inst,[status(thm)],[])).
% 0.81/0.97 tff(232,plain,
% 0.81/0.97 (~gt(n2, n2)),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[231, 26])).
% 0.81/0.97 tff(233,plain,
% 0.81/0.97 (~gt(succ(n1), n2)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[232, 230])).
% 0.81/0.97 tff(234,plain,
% 0.81/0.97 (~gt(n2, n1)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[233, 228])).
% 0.81/0.97 tff(235,plain,
% 0.81/0.97 ($false),
% 0.81/0.97 inference(unit_resolution,[status(thm)],[208, 234])).
% 0.81/0.97 tff(236,plain,(~(n1 = n2)), inference(lemma,lemma(discharge,[]))).
% 0.81/0.97 tff(237,plain,
% 0.81/0.97 (~(n2 = n1)),
% 0.81/0.97 inference(modus_ponens,[status(thm)],[236, 221])).
% 0.81/0.97 tff(238,plain,
% 0.81/0.97 ((~![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)) | (a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0) = use)),
% 0.81/0.98 inference(quant_inst,[status(thm)],[])).
% 0.81/0.98 tff(239,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0) = use),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[238, 153])).
% 0.81/0.98 tff(240,assumption,(~(n0 = n2)), introduced(assumption)).
% 0.81/0.98 tff(241,plain,
% 0.81/0.98 (((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0)))) <=> ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0)))),
% 0.81/0.98 inference(rewrite,[status(thm)],[])).
% 0.81/0.98 tff(242,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0)))),
% 0.81/0.98 inference(quant_inst,[status(thm)],[])).
% 0.81/0.98 tff(243,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0))),
% 0.81/0.98 inference(modus_ponens,[status(thm)],[242, 241])).
% 0.81/0.98 tff(244,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n2, n0)),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[243, 191, 240])).
% 0.81/0.98 tff(245,plain,
% 0.81/0.98 ((n2 = n1) <=> (n1 = n2)),
% 0.81/0.98 inference(symmetry,[status(thm)],[220])).
% 0.81/0.98 tff(246,plain,
% 0.81/0.98 ((~(n2 = n1)) <=> (~(n1 = n2))),
% 0.81/0.98 inference(monotonicity,[status(thm)],[245])).
% 0.81/0.98 tff(247,assumption,(~(n2 = n1)), introduced(assumption)).
% 0.81/0.98 tff(248,plain,
% 0.81/0.98 (~(n1 = n2)),
% 0.81/0.98 inference(modus_ponens,[status(thm)],[247, 246])).
% 0.81/0.98 tff(249,plain,
% 0.81/0.98 (((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n1 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0)))) <=> ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n1 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0)))),
% 0.81/0.98 inference(rewrite,[status(thm)],[])).
% 0.81/0.98 tff(250,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n1 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0)))),
% 0.81/0.98 inference(quant_inst,[status(thm)],[])).
% 0.81/0.98 tff(251,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n1 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0))),
% 0.81/0.98 inference(modus_ponens,[status(thm)],[250, 249])).
% 0.81/0.98 tff(252,plain,
% 0.81/0.98 ((n1 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0))),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[251, 191])).
% 0.81/0.98 tff(253,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n2, n0)),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[252, 248])).
% 0.81/0.98 tff(254,plain,
% 0.81/0.98 (((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0)))) <=> ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0)))),
% 0.81/0.98 inference(rewrite,[status(thm)],[])).
% 0.81/0.98 tff(255,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0)))),
% 0.81/0.98 inference(quant_inst,[status(thm)],[])).
% 0.81/0.98 tff(256,plain,
% 0.81/0.98 ((~![I: $i, U: $i, V: $i, X: $i, VAL2: $i] : ((I = U) | (a_select3(tptp_update3(X, I, V, VAL2), U, V) = a_select3(X, U, V)))) | (n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0))),
% 0.81/0.98 inference(modus_ponens,[status(thm)],[255, 254])).
% 0.81/0.98 tff(257,plain,
% 0.81/0.98 ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0))),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[256, 191])).
% 0.81/0.98 tff(258,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n2, n0)),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[257, 240])).
% 0.81/0.98 tff(259,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use),
% 0.81/0.98 inference(transitivity,[status(thm)],[258, 253, 244, 239])).
% 0.81/0.98 tff(260,assumption,(~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)), introduced(assumption)).
% 0.81/0.98 tff(261,plain,
% 0.81/0.98 ($false),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[260, 259])).
% 0.81/0.98 tff(262,plain,((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) | (n2 = n1)), inference(lemma,lemma(discharge,[]))).
% 0.81/0.98 tff(263,plain,
% 0.81/0.98 ((n0 = n2) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[262, 237])).
% 0.81/0.98 tff(264,plain,
% 0.81/0.98 (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[263, 219])).
% 0.81/0.98 tff(265,assumption,(~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)), introduced(assumption)).
% 0.81/0.98 tff(266,plain,
% 0.81/0.98 ((~![X: $i, U: $i, V: $i, VAL: $i] : (a_select3(tptp_update3(X, U, V, VAL), U, V) = VAL)) | (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)),
% 0.81/0.98 inference(quant_inst,[status(thm)],[])).
% 0.81/0.98 tff(267,plain,
% 0.81/0.98 ($false),
% 0.81/0.98 inference(unit_resolution,[status(thm)],[266, 153, 265])).
% 0.81/0.98 tff(268,plain,(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use), inference(lemma,lemma(discharge,[]))).
% 0.81/0.98 tff(269,plain,
% 0.81/0.98 ((~(~((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))))) <=> ((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))),
% 0.81/0.98 inference(rewrite,[status(thm)],[])).
% 0.81/0.98 tff(270,plain,
% 0.81/0.98 (((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)) <=> (~((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))))),
% 0.81/0.98 inference(rewrite,[status(thm)],[])).
% 0.81/0.98 tff(271,plain,
% 0.81/0.98 ((~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))) <=> (~(~((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))))),
% 0.81/0.99 inference(monotonicity,[status(thm)],[270])).
% 0.81/0.99 tff(272,plain,
% 0.81/0.99 ((~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))) <=> ((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))),
% 0.81/0.99 inference(transitivity,[status(thm)],[271, 269])).
% 0.81/0.99 tff(273,plain,
% 0.81/0.99 ((~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))) <=> (~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))),
% 0.81/0.99 inference(rewrite,[status(thm)],[])).
% 0.81/0.99 tff(274,plain,
% 0.81/0.99 ((~(true => ((((((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))) <=> (~((~true) | ((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))))),
% 0.81/0.99 inference(rewrite,[status(thm)],[])).
% 0.81/0.99 tff(275,axiom,(~(true => ((((((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','quaternion_ds1_inuse_0001')).
% 0.81/0.99 tff(276,plain,
% 0.81/0.99 (~((~true) | ((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use)))),
% 0.81/0.99 inference(modus_ponens,[status(thm)],[275, 274])).
% 0.81/0.99 tff(277,plain,
% 0.81/0.99 (~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))),
% 0.81/0.99 inference(or_elim,[status(thm)],[276])).
% 0.81/0.99 tff(278,plain,
% 0.81/0.99 (~((a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use) & (a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))),
% 0.81/0.99 inference(modus_ponens,[status(thm)],[277, 273])).
% 0.81/0.99 tff(279,plain,
% 0.81/0.99 ((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n0, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))),
% 0.81/0.99 inference(modus_ponens,[status(thm)],[278, 272])).
% 0.81/0.99 tff(280,plain,
% 0.81/0.99 ((~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n1, n0) = use)) | (~(a_select3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(tptp_update3(u_defuse, n2, n0, use), n1, n0, use), n2, n0, use), n0, n0, use), n1, n0, use), n0, n0, use), n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))),
% 0.81/0.99 inference(unit_resolution,[status(thm)],[279, 268])).
% 0.81/0.99 tff(281,plain,
% 0.81/0.99 ((~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n5) = use))),
% 0.81/1.00 inference(unit_resolution,[status(thm)],[280, 264, 199])).
% 0.81/1.00 tff(282,plain,
% 0.81/1.00 (~(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n5, use), n4, use), n5, use), n3, use), n4, use), n3, use), n4) = use)),
% 0.81/1.00 inference(unit_resolution,[status(thm)],[281, 147, 143])).
% 0.81/1.00 tff(283,plain,
% 0.81/1.00 ($false),
% 0.81/1.00 inference(unit_resolution,[status(thm)],[282, 63])).
% 0.81/1.00 % SZS output end Proof
% 0.81/1.00 % E exiting
%------------------------------------------------------------------------------