%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV104+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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:31 AM UTC 2025
% Result : Theorem 8.52s 8.70s
% Output : Proof 8.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV104+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n016.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:27:47 EDT 2025
% 0.12/0.34 % CPUTime :
% 8.52/8.70 % SZS status Theorem
% 8.52/8.70 % SZS output start Proof
% 8.52/8.70 tff(gt_type, type, (
% 8.52/8.70 gt: ( $i * $i ) > $o)).
% 8.52/8.70 tff(n4_type, type, (
% 8.52/8.70 n4: $i)).
% 8.52/8.70 tff(n5_type, type, (
% 8.52/8.70 n5: $i)).
% 8.52/8.70 tff(succ_type, type, (
% 8.52/8.70 succ: $i > $i)).
% 8.52/8.70 tff(n2_type, type, (
% 8.52/8.70 n2: $i)).
% 8.52/8.70 tff(n0_type, type, (
% 8.52/8.70 n0: $i)).
% 8.52/8.70 tff(n3_type, type, (
% 8.52/8.70 n3: $i)).
% 8.52/8.70 tff(a_select2_type, type, (
% 8.52/8.70 a_select2: ( $i * $i ) > $i)).
% 8.52/8.70 tff(tptp_update2_type, type, (
% 8.52/8.70 tptp_update2: ( $i * $i * $i ) > $i)).
% 8.52/8.70 tff(use_type, type, (
% 8.52/8.70 use: $i)).
% 8.52/8.70 tff(xinit_defuse_type, type, (
% 8.52/8.70 xinit_defuse: $i)).
% 8.52/8.70 tff(a_select3_type, type, (
% 8.52/8.70 a_select3: ( $i * $i * $i ) > $i)).
% 8.52/8.70 tff(u_defuse_type, type, (
% 8.52/8.70 u_defuse: $i)).
% 8.52/8.70 tff(n1_type, type, (
% 8.52/8.70 n1: $i)).
% 8.52/8.70 tff(1,plain,
% 8.52/8.70 ((succ(succ(n0)) = n2) <=> (succ(succ(n0)) = n2)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(2,axiom,(succ(succ(n0)) = n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_2')).
% 8.52/8.70 tff(3,plain,
% 8.52/8.70 (succ(succ(n0)) = n2),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[2, 1])).
% 8.52/8.70 tff(4,plain,
% 8.52/8.70 (n2 = succ(succ(n0))),
% 8.52/8.70 inference(symmetry,[status(thm)],[3])).
% 8.52/8.70 tff(5,plain,
% 8.52/8.70 (succ(n2) = succ(succ(succ(n0)))),
% 8.52/8.70 inference(monotonicity,[status(thm)],[4])).
% 8.52/8.70 tff(6,plain,
% 8.52/8.70 (succ(succ(succ(n0))) = succ(n2)),
% 8.52/8.70 inference(symmetry,[status(thm)],[5])).
% 8.52/8.70 tff(7,plain,
% 8.52/8.70 ((succ(succ(succ(n0))) = n3) <=> (succ(succ(succ(n0))) = n3)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(8,axiom,(succ(succ(succ(n0))) = n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_3')).
% 8.52/8.70 tff(9,plain,
% 8.52/8.70 (succ(succ(succ(n0))) = n3),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[8, 7])).
% 8.52/8.70 tff(10,plain,
% 8.52/8.70 (n3 = succ(succ(succ(n0)))),
% 8.52/8.70 inference(symmetry,[status(thm)],[9])).
% 8.52/8.70 tff(11,plain,
% 8.52/8.70 (![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)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(12,plain,
% 8.52/8.70 (![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)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(13,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')).
% 8.52/8.70 tff(14,plain,
% 8.52/8.70 (![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[13, 12])).
% 8.52/8.70 tff(15,plain,(
% 8.52/8.70 ![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 8.52/8.70 inference(skolemize,[status(sab)],[14])).
% 8.52/8.70 tff(16,plain,
% 8.52/8.70 (![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[15, 11])).
% 8.52/8.70 tff(17,plain,
% 8.52/8.70 ((~![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)) | (a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4) = use)),
% 8.52/8.70 inference(quant_inst,[status(thm)],[])).
% 8.52/8.70 tff(18,plain,
% 8.52/8.70 (a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4) = use),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[17, 16])).
% 8.52/8.70 tff(19,plain,
% 8.52/8.70 (succ(n3) = succ(succ(succ(succ(n0))))),
% 8.52/8.70 inference(monotonicity,[status(thm)],[10])).
% 8.52/8.70 tff(20,plain,
% 8.52/8.70 (succ(succ(succ(succ(n0)))) = succ(n3)),
% 8.52/8.70 inference(symmetry,[status(thm)],[19])).
% 8.52/8.70 tff(21,plain,
% 8.52/8.70 ((succ(succ(succ(succ(n0)))) = n4) <=> (succ(succ(succ(succ(n0)))) = n4)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(22,axiom,(succ(succ(succ(succ(n0)))) = n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p','successor_4')).
% 8.52/8.70 tff(23,plain,
% 8.52/8.70 (succ(succ(succ(succ(n0)))) = n4),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[22, 21])).
% 8.52/8.70 tff(24,plain,
% 8.52/8.70 (n4 = succ(succ(succ(succ(n0))))),
% 8.52/8.70 inference(symmetry,[status(thm)],[23])).
% 8.52/8.70 tff(25,assumption,(n5 = n4), introduced(assumption)).
% 8.52/8.70 tff(26,plain,
% 8.52/8.70 (n5 = succ(n3)),
% 8.52/8.70 inference(transitivity,[status(thm)],[25, 24, 20])).
% 8.52/8.70 tff(27,plain,
% 8.52/8.70 (gt(n5, n4) <=> gt(succ(n3), n4)),
% 8.52/8.70 inference(monotonicity,[status(thm)],[26])).
% 8.52/8.70 tff(28,plain,
% 8.52/8.70 (gt(succ(n3), n4) <=> gt(n5, n4)),
% 8.52/8.70 inference(symmetry,[status(thm)],[27])).
% 8.52/8.70 tff(29,plain,
% 8.52/8.70 ((~gt(succ(n3), n4)) <=> (~gt(n5, n4))),
% 8.52/8.70 inference(monotonicity,[status(thm)],[28])).
% 8.52/8.70 tff(30,plain,
% 8.52/8.70 (n4 = succ(n3)),
% 8.52/8.70 inference(transitivity,[status(thm)],[24, 20])).
% 8.52/8.70 tff(31,plain,
% 8.52/8.70 (gt(n4, n4) <=> gt(succ(n3), n4)),
% 8.52/8.70 inference(monotonicity,[status(thm)],[30])).
% 8.52/8.70 tff(32,plain,
% 8.52/8.70 ((~gt(n4, n4)) <=> (~gt(succ(n3), n4))),
% 8.52/8.70 inference(monotonicity,[status(thm)],[31])).
% 8.52/8.70 tff(33,plain,
% 8.52/8.70 (^[X: $i] : refl((~gt(X, X)) <=> (~gt(X, X)))),
% 8.52/8.70 inference(bind,[status(th)],[])).
% 8.52/8.70 tff(34,plain,
% 8.52/8.70 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 8.52/8.70 inference(quant_intro,[status(thm)],[33])).
% 8.52/8.70 tff(35,plain,
% 8.52/8.70 (![X: $i] : (~gt(X, X)) <=> ![X: $i] : (~gt(X, X))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(36,axiom,(![X: $i] : (~gt(X, X))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax','irreflexivity_gt')).
% 8.52/8.70 tff(37,plain,
% 8.52/8.70 (![X: $i] : (~gt(X, X))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[36, 35])).
% 8.52/8.70 tff(38,plain,(
% 8.52/8.70 ![X: $i] : (~gt(X, X))),
% 8.52/8.70 inference(skolemize,[status(sab)],[37])).
% 8.52/8.70 tff(39,plain,
% 8.52/8.70 (![X: $i] : (~gt(X, X))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[38, 34])).
% 8.52/8.70 tff(40,plain,
% 8.52/8.70 ((~![X: $i] : (~gt(X, X))) | (~gt(n4, n4))),
% 8.52/8.70 inference(quant_inst,[status(thm)],[])).
% 8.52/8.70 tff(41,plain,
% 8.52/8.70 (~gt(n4, n4)),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[40, 39])).
% 8.52/8.70 tff(42,plain,
% 8.52/8.70 (~gt(succ(n3), n4)),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[41, 32])).
% 8.52/8.70 tff(43,plain,
% 8.52/8.70 (~gt(n5, n4)),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[42, 29])).
% 8.52/8.70 tff(44,plain,
% 8.52/8.70 (gt(n5, n4) <=> gt(n5, n4)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(45,axiom,(gt(n5, n4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','gt_5_4')).
% 8.52/8.70 tff(46,plain,
% 8.52/8.70 (gt(n5, n4)),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[45, 44])).
% 8.52/8.70 tff(47,plain,
% 8.52/8.70 ($false),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[46, 43])).
% 8.52/8.70 tff(48,plain,(~(n5 = n4)), inference(lemma,lemma(discharge,[]))).
% 8.52/8.70 tff(49,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(50,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(51,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(elim_unused_vars,[status(thm)],[])).
% 8.52/8.70 tff(52,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(destructive_equality_resolution,[status(thm)],[])).
% 8.52/8.70 tff(53,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(transitivity,[status(thm)],[52, 51])).
% 8.52/8.70 tff(54,plain,
% 8.52/8.70 (^[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)))),
% 8.52/8.70 inference(bind,[status(th)],[])).
% 8.52/8.70 tff(55,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(quant_intro,[status(thm)],[54])).
% 8.52/8.70 tff(56,plain,
% 8.52/8.70 (![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))),
% 8.52/8.70 inference(transitivity,[status(thm)],[55, 53])).
% 8.52/8.70 tff(57,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')).
% 8.52/8.70 tff(58,plain,
% 8.52/8.70 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[57, 56])).
% 8.52/8.70 tff(59,plain,
% 8.52/8.70 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[58, 50])).
% 8.52/8.70 tff(60,plain,(
% 8.52/8.70 ![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 8.52/8.70 inference(skolemize,[status(sab)],[59])).
% 8.52/8.70 tff(61,plain,
% 8.52/8.70 (![I: $i, U: $i, X: $i, VAL2: $i] : ((a_select2(tptp_update2(X, I, VAL2), U) = a_select2(X, U)) | (I = U))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[60, 49])).
% 8.52/8.70 tff(62,plain,
% 8.52/8.70 (((~![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(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(63,plain,
% 8.52/8.70 (((a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)) | (n5 = n4)) <=> ((n5 = n4) | (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(64,plain,
% 8.52/8.70 (((~![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_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4))))),
% 8.52/8.70 inference(monotonicity,[status(thm)],[63])).
% 8.52/8.70 tff(65,plain,
% 8.52/8.70 (((~![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_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)))),
% 8.52/8.70 inference(transitivity,[status(thm)],[64, 62])).
% 8.52/8.70 tff(66,plain,
% 8.52/8.70 ((~![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_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)) | (n5 = n4))),
% 8.52/8.70 inference(quant_inst,[status(thm)],[])).
% 8.52/8.70 tff(67,plain,
% 8.52/8.70 ((~![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(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4))),
% 8.52/8.70 inference(modus_ponens,[status(thm)],[66, 65])).
% 8.52/8.70 tff(68,plain,
% 8.52/8.70 (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n4)),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[67, 61, 48])).
% 8.52/8.70 tff(69,plain,
% 8.52/8.70 (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use),
% 8.52/8.70 inference(transitivity,[status(thm)],[68, 18])).
% 8.52/8.70 tff(70,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)), introduced(assumption)).
% 8.52/8.70 tff(71,plain,
% 8.52/8.70 ($false),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[70, 69])).
% 8.52/8.70 tff(72,plain,(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use), inference(lemma,lemma(discharge,[]))).
% 8.52/8.70 tff(73,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)), introduced(assumption)).
% 8.52/8.70 tff(74,plain,
% 8.52/8.70 ((~![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, n3, use), n4, use), n5, use), n5) = use)),
% 8.52/8.70 inference(quant_inst,[status(thm)],[])).
% 8.52/8.70 tff(75,plain,
% 8.52/8.70 ($false),
% 8.52/8.70 inference(unit_resolution,[status(thm)],[74, 16, 73])).
% 8.52/8.70 tff(76,plain,(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use), inference(lemma,lemma(discharge,[]))).
% 8.52/8.70 tff(77,plain,
% 8.52/8.70 ((a_select3(u_defuse, n2, n0) = use) <=> (a_select3(u_defuse, n2, n0) = use)),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(78,plain,
% 8.52/8.70 ((~(((((((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_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use)) & (a_select3(u_defuse, n2, n0) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))))),
% 8.52/8.70 inference(rewrite,[status(thm)],[])).
% 8.52/8.70 tff(79,axiom,(~(((((((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_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use)) & (a_select3(u_defuse, n2, n0) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','quaternion_ds1_inuse_0016')).
% 8.52/8.71 tff(80,plain,
% 8.52/8.71 (~((~((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_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[79, 78])).
% 8.52/8.71 tff(81,plain,
% 8.52/8.71 ((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)),
% 8.52/8.71 inference(or_elim,[status(thm)],[80])).
% 8.52/8.71 tff(82,plain,
% 8.52/8.71 (a_select3(u_defuse, n2, n0) = use),
% 8.52/8.71 inference(and_elim,[status(thm)],[81])).
% 8.52/8.71 tff(83,plain,
% 8.52/8.71 (a_select3(u_defuse, n2, n0) = use),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[82, 77])).
% 8.52/8.71 tff(84,plain,
% 8.52/8.71 ((a_select3(u_defuse, n1, n0) = use) <=> (a_select3(u_defuse, n1, n0) = use)),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(85,plain,
% 8.52/8.71 (a_select3(u_defuse, n1, n0) = use),
% 8.52/8.71 inference(and_elim,[status(thm)],[81])).
% 8.52/8.71 tff(86,plain,
% 8.52/8.71 (a_select3(u_defuse, n1, n0) = use),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[85, 84])).
% 8.52/8.71 tff(87,plain,
% 8.52/8.71 ((a_select3(u_defuse, n0, n0) = use) <=> (a_select3(u_defuse, n0, n0) = use)),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(88,plain,
% 8.52/8.71 (a_select3(u_defuse, n0, n0) = use),
% 8.52/8.71 inference(and_elim,[status(thm)],[81])).
% 8.52/8.71 tff(89,plain,
% 8.52/8.71 (a_select3(u_defuse, n0, n0) = use),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[88, 87])).
% 8.52/8.71 tff(90,plain,
% 8.52/8.71 ((~(~((~(a_select3(u_defuse, n0, n0) = use)) | (~(a_select3(u_defuse, n1, n0) = use)) | (~(a_select3(u_defuse, n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(91,plain,
% 8.52/8.71 (((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(92,plain,
% 8.52/8.71 ((~((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[91])).
% 8.52/8.71 tff(93,plain,
% 8.52/8.71 ((~((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))),
% 8.52/8.71 inference(transitivity,[status(thm)],[92, 90])).
% 8.52/8.71 tff(94,plain,
% 8.52/8.71 ((~((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), 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(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(95,plain,
% 8.52/8.71 (~((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))),
% 8.52/8.71 inference(or_elim,[status(thm)],[80])).
% 8.52/8.71 tff(96,plain,
% 8.52/8.71 (~((a_select3(u_defuse, n0, n0) = use) & (a_select3(u_defuse, n1, n0) = use) & (a_select3(u_defuse, n2, n0) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use) & (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[95, 94])).
% 8.52/8.71 tff(97,plain,
% 8.52/8.71 ((~(a_select3(u_defuse, n0, n0) = use)) | (~(a_select3(u_defuse, n1, n0) = use)) | (~(a_select3(u_defuse, n2, n0) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[96, 93])).
% 8.52/8.71 tff(98,plain,
% 8.52/8.71 ((~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n5) = use))),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[97, 89, 86, 83])).
% 8.52/8.71 tff(99,plain,
% 8.52/8.71 ((~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)) | (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n4) = use))),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[98, 76])).
% 8.52/8.71 tff(100,plain,
% 8.52/8.71 (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[99, 72])).
% 8.52/8.71 tff(101,assumption,(n4 = n3), introduced(assumption)).
% 8.52/8.71 tff(102,plain,
% 8.52/8.71 (n3 = n4),
% 8.52/8.71 inference(symmetry,[status(thm)],[101])).
% 8.52/8.71 tff(103,plain,
% 8.52/8.71 (gt(n4, n3) <=> gt(succ(n3), n4)),
% 8.52/8.71 inference(monotonicity,[status(thm)],[30, 102])).
% 8.52/8.71 tff(104,plain,
% 8.52/8.71 (gt(succ(n3), n4) <=> gt(n4, n3)),
% 8.52/8.71 inference(symmetry,[status(thm)],[103])).
% 8.52/8.71 tff(105,plain,
% 8.52/8.71 ((~gt(succ(n3), n4)) <=> (~gt(n4, n3))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[104])).
% 8.52/8.71 tff(106,plain,
% 8.52/8.71 (~gt(n4, n3)),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[42, 105])).
% 8.52/8.71 tff(107,plain,
% 8.52/8.71 (gt(n4, n3) <=> gt(n4, n3)),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(108,axiom,(gt(n4, n3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','gt_4_3')).
% 8.52/8.71 tff(109,plain,
% 8.52/8.71 (gt(n4, n3)),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[108, 107])).
% 8.52/8.71 tff(110,plain,
% 8.52/8.71 ($false),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[109, 106])).
% 8.52/8.71 tff(111,plain,(~(n4 = n3)), inference(lemma,lemma(discharge,[]))).
% 8.52/8.71 tff(112,plain,
% 8.52/8.71 ((~![X: $i, U: $i, VAL: $i] : (a_select2(tptp_update2(X, U, VAL), U) = VAL)) | (a_select2(tptp_update2(xinit_defuse, n3, use), n3) = use)),
% 8.52/8.71 inference(quant_inst,[status(thm)],[])).
% 8.52/8.71 tff(113,plain,
% 8.52/8.71 (a_select2(tptp_update2(xinit_defuse, n3, use), n3) = use),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[112, 16])).
% 8.52/8.71 tff(114,assumption,(~(n4 = n3)), introduced(assumption)).
% 8.52/8.71 tff(115,plain,
% 8.52/8.71 (((~![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(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(116,plain,
% 8.52/8.71 (((a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)) | (n4 = n3)) <=> ((n4 = n3) | (a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(117,plain,
% 8.52/8.71 (((~![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_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3))))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[116])).
% 8.52/8.71 tff(118,plain,
% 8.52/8.71 (((~![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_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)))),
% 8.52/8.71 inference(transitivity,[status(thm)],[117, 115])).
% 8.52/8.71 tff(119,plain,
% 8.52/8.71 ((~![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_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)) | (n4 = n3))),
% 8.52/8.71 inference(quant_inst,[status(thm)],[])).
% 8.52/8.71 tff(120,plain,
% 8.52/8.71 ((~![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(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3))),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[119, 118])).
% 8.52/8.71 tff(121,plain,
% 8.52/8.71 (a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3) = a_select2(tptp_update2(xinit_defuse, n3, use), n3)),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[120, 61, 114])).
% 8.52/8.71 tff(122,assumption,(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)), introduced(assumption)).
% 8.52/8.71 tff(123,plain,
% 8.52/8.71 (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use),
% 8.52/8.71 inference(transitivity,[status(thm)],[122, 121, 113])).
% 8.52/8.71 tff(124,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)), introduced(assumption)).
% 8.52/8.71 tff(125,plain,
% 8.52/8.71 ($false),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[124, 123])).
% 8.52/8.71 tff(126,plain,((~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))) | (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use) | (n4 = n3)), inference(lemma,lemma(discharge,[]))).
% 8.52/8.71 tff(127,plain,
% 8.52/8.71 ((~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))) | (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = use)),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[126, 111])).
% 8.52/8.71 tff(128,plain,
% 8.52/8.71 (~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[127, 100])).
% 8.52/8.71 tff(129,assumption,(~(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))), introduced(assumption)).
% 8.52/8.71 tff(130,assumption,(~(n5 = n3)), introduced(assumption)).
% 8.52/8.71 tff(131,plain,
% 8.52/8.71 (((~![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(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(132,plain,
% 8.52/8.71 (((a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)) | (n5 = n3)) <=> ((n5 = n3) | (a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(133,plain,
% 8.52/8.71 (((~![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_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[132])).
% 8.52/8.71 tff(134,plain,
% 8.52/8.71 (((~![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_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, 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(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)))),
% 8.52/8.71 inference(transitivity,[status(thm)],[133, 131])).
% 8.52/8.71 tff(135,plain,
% 8.52/8.71 ((~![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_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)) | (n5 = n3))),
% 8.52/8.71 inference(quant_inst,[status(thm)],[])).
% 8.52/8.71 tff(136,plain,
% 8.52/8.71 ((~![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(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3))),
% 8.52/8.71 inference(modus_ponens,[status(thm)],[135, 134])).
% 8.52/8.71 tff(137,plain,
% 8.52/8.71 ($false),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[136, 61, 130, 129])).
% 8.52/8.71 tff(138,plain,((a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n5, use), n3) = a_select2(tptp_update2(tptp_update2(xinit_defuse, n3, use), n4, use), n3)) | (n5 = n3)), inference(lemma,lemma(discharge,[]))).
% 8.52/8.71 tff(139,plain,
% 8.52/8.71 (n5 = n3),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[138, 128])).
% 8.52/8.71 tff(140,plain,
% 8.52/8.71 (n5 = succ(n2)),
% 8.52/8.71 inference(transitivity,[status(thm)],[139, 10, 6])).
% 8.52/8.71 tff(141,plain,
% 8.52/8.71 (gt(n5, n4) <=> gt(succ(n2), n4)),
% 8.52/8.71 inference(monotonicity,[status(thm)],[140])).
% 8.52/8.71 tff(142,plain,
% 8.52/8.71 (gt(succ(n2), n4) <=> gt(n5, n4)),
% 8.52/8.71 inference(symmetry,[status(thm)],[141])).
% 8.52/8.71 tff(143,plain,
% 8.52/8.71 ((~gt(succ(n2), n4)) <=> (~gt(n5, n4))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[142])).
% 8.52/8.71 tff(144,plain,
% 8.52/8.71 (n3 = succ(n2)),
% 8.52/8.71 inference(transitivity,[status(thm)],[10, 6])).
% 8.52/8.71 tff(145,plain,
% 8.52/8.71 (gt(n3, n4) <=> gt(succ(n2), n4)),
% 8.52/8.71 inference(monotonicity,[status(thm)],[144])).
% 8.52/8.71 tff(146,plain,
% 8.52/8.71 ((~gt(n3, n4)) <=> (~gt(succ(n2), n4))),
% 8.52/8.71 inference(monotonicity,[status(thm)],[145])).
% 8.52/8.71 tff(147,plain,
% 8.52/8.71 ((~![X: $i] : (~gt(X, X))) | (~gt(n3, n3))),
% 8.52/8.71 inference(quant_inst,[status(thm)],[])).
% 8.52/8.71 tff(148,plain,
% 8.52/8.71 (~gt(n3, n3)),
% 8.52/8.71 inference(unit_resolution,[status(thm)],[147, 39])).
% 8.52/8.71 tff(149,plain,
% 8.52/8.71 (![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)))),
% 8.52/8.71 inference(rewrite,[status(thm)],[])).
% 8.52/8.71 tff(150,plain,
% 8.52/8.71 (^[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)))))),
% 8.55/8.73 inference(bind,[status(th)],[])).
% 8.55/8.73 tff(151,plain,
% 8.55/8.73 (![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)))),
% 8.55/8.73 inference(quant_intro,[status(thm)],[150])).
% 8.55/8.73 tff(152,plain,
% 8.55/8.73 (![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))),
% 8.55/8.73 inference(rewrite,[status(thm)],[])).
% 8.55/8.73 tff(153,plain,
% 8.55/8.73 (^[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)))),
% 8.55/8.73 inference(bind,[status(th)],[])).
% 8.55/8.73 tff(154,plain,
% 8.55/8.73 (![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))),
% 8.55/8.73 inference(quant_intro,[status(thm)],[153])).
% 8.55/8.73 tff(155,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')).
% 8.55/8.73 tff(156,plain,
% 8.55/8.73 (![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[155, 154])).
% 8.55/8.73 tff(157,plain,
% 8.55/8.73 (![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[156, 152])).
% 8.55/8.73 tff(158,plain,(
% 8.55/8.73 ![X: $i, Y: $i, Z: $i] : ((~(gt(X, Y) & gt(Y, Z))) | gt(X, Z))),
% 8.55/8.73 inference(skolemize,[status(sab)],[157])).
% 8.55/8.73 tff(159,plain,
% 8.55/8.73 (![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[158, 151])).
% 8.55/8.73 tff(160,plain,
% 8.55/8.73 (![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[159, 149])).
% 8.55/8.73 tff(161,plain,
% 8.55/8.73 (((~![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)))),
% 8.55/8.73 inference(rewrite,[status(thm)],[])).
% 8.55/8.73 tff(162,plain,
% 8.55/8.73 ((gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3))) <=> ((~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4)))),
% 8.55/8.73 inference(rewrite,[status(thm)],[])).
% 8.55/8.73 tff(163,plain,
% 8.55/8.73 (((~![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))))),
% 8.55/8.73 inference(monotonicity,[status(thm)],[162])).
% 8.55/8.73 tff(164,plain,
% 8.55/8.73 (((~![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)))),
% 8.55/8.73 inference(transitivity,[status(thm)],[163, 161])).
% 8.55/8.73 tff(165,plain,
% 8.55/8.73 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (gt(n3, n3) | (~gt(n3, n4)) | (~gt(n4, n3)))),
% 8.55/8.73 inference(quant_inst,[status(thm)],[])).
% 8.55/8.73 tff(166,plain,
% 8.55/8.73 ((~![X: $i, Y: $i, Z: $i] : (gt(X, Z) | (~gt(X, Y)) | (~gt(Y, Z)))) | (~gt(n4, n3)) | gt(n3, n3) | (~gt(n3, n4))),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[165, 164])).
% 8.55/8.73 tff(167,plain,
% 8.55/8.73 (~gt(n3, n4)),
% 8.55/8.73 inference(unit_resolution,[status(thm)],[166, 160, 109, 148])).
% 8.55/8.73 tff(168,plain,
% 8.55/8.73 (~gt(succ(n2), n4)),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[167, 146])).
% 8.55/8.73 tff(169,plain,
% 8.55/8.73 (~gt(n5, n4)),
% 8.55/8.73 inference(modus_ponens,[status(thm)],[168, 143])).
% 8.55/8.73 tff(170,plain,
% 8.55/8.73 ($false),
% 8.55/8.73 inference(unit_resolution,[status(thm)],[46, 169])).
% 8.55/8.73 % SZS output end Proof
% 8.60/8.76 % E exiting
%------------------------------------------------------------------------------