%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV537-1.004 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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:34:22 AM UTC 2025
% Result : Unsatisfiable 0.12s 0.39s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV537-1.004 : TPTP v9.0.0. Released v4.0.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 10:12:56 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.39 % SZS status Unsatisfiable
% 0.12/0.39 % SZS output start Proof
% 0.12/0.39 tff(e_492_type, type, (
% 0.12/0.39 e_492: $i)).
% 0.12/0.39 tff(e_491_type, type, (
% 0.12/0.39 e_491: $i)).
% 0.12/0.39 tff(select_type, type, (
% 0.12/0.39 select: ( $i * $i ) > $i)).
% 0.12/0.39 tff(i_490_type, type, (
% 0.12/0.39 i_490: $i)).
% 0.12/0.39 tff(a_489_type, type, (
% 0.12/0.39 a_489: $i)).
% 0.12/0.39 tff(a_479_type, type, (
% 0.12/0.39 a_479: $i)).
% 0.12/0.39 tff(store_type, type, (
% 0.12/0.39 store: ( $i * $i * $i ) > $i)).
% 0.12/0.39 tff(e_478_type, type, (
% 0.12/0.39 e_478: $i)).
% 0.12/0.39 tff(i0_type, type, (
% 0.12/0.39 i0: $i)).
% 0.12/0.39 tff(a_477_type, type, (
% 0.12/0.39 a_477: $i)).
% 0.12/0.39 tff(e_488_type, type, (
% 0.12/0.39 e_488: $i)).
% 0.12/0.39 tff(i2_type, type, (
% 0.12/0.39 i2: $i)).
% 0.12/0.39 tff(a_487_type, type, (
% 0.12/0.39 a_487: $i)).
% 0.12/0.39 tff(a_475_type, type, (
% 0.12/0.39 a_475: $i)).
% 0.12/0.39 tff(i3_type, type, (
% 0.12/0.39 i3: $i)).
% 0.12/0.39 tff(a_471_type, type, (
% 0.12/0.39 a_471: $i)).
% 0.12/0.39 tff(e_472_type, type, (
% 0.12/0.39 e_472: $i)).
% 0.12/0.39 tff(e_474_type, type, (
% 0.12/0.39 e_474: $i)).
% 0.12/0.39 tff(a_473_type, type, (
% 0.12/0.39 a_473: $i)).
% 0.12/0.39 tff(a_467_type, type, (
% 0.12/0.39 a_467: $i)).
% 0.12/0.39 tff(e_468_type, type, (
% 0.12/0.39 e_468: $i)).
% 0.12/0.39 tff(e_470_type, type, (
% 0.12/0.39 e_470: $i)).
% 0.12/0.39 tff(a_469_type, type, (
% 0.12/0.39 a_469: $i)).
% 0.12/0.39 tff(e_465_type, type, (
% 0.12/0.39 e_465: $i)).
% 0.12/0.39 tff(i1_type, type, (
% 0.12/0.39 i1: $i)).
% 0.12/0.39 tff(a_466_type, type, (
% 0.12/0.39 a_466: $i)).
% 0.12/0.39 tff(a_481_type, type, (
% 0.12/0.39 a_481: $i)).
% 0.12/0.39 tff(a_480_type, type, (
% 0.12/0.39 a_480: $i)).
% 0.12/0.39 tff(e_482_type, type, (
% 0.12/0.39 e_482: $i)).
% 0.12/0.39 tff(a_485_type, type, (
% 0.12/0.39 a_485: $i)).
% 0.12/0.39 tff(e_484_type, type, (
% 0.12/0.39 e_484: $i)).
% 0.12/0.39 tff(a_483_type, type, (
% 0.12/0.39 a_483: $i)).
% 0.12/0.39 tff(e_486_type, type, (
% 0.12/0.39 e_486: $i)).
% 0.12/0.39 tff(sk_type, type, (
% 0.12/0.39 sk: ( $i * $i ) > $i)).
% 0.12/0.39 tff(e_476_type, type, (
% 0.12/0.39 e_476: $i)).
% 0.12/0.39 tff(1,plain,
% 0.12/0.39 ((e_492 = select(a_489, i_490)) <=> (e_492 = select(a_489, i_490))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(2,axiom,(e_492 = select(a_489, i_490)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp26')).
% 0.12/0.39 tff(3,plain,
% 0.12/0.39 (e_492 = select(a_489, i_490)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.12/0.39 tff(4,plain,
% 0.12/0.39 (select(a_489, i_490) = e_492),
% 0.12/0.39 inference(symmetry,[status(thm)],[3])).
% 0.12/0.39 tff(5,plain,
% 0.12/0.39 ((a_479 = store(a_477, i0, e_478)) <=> (a_479 = store(a_477, i0, e_478))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(6,axiom,(a_479 = store(a_477, i0, e_478)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp7')).
% 0.12/0.39 tff(7,plain,
% 0.12/0.39 (a_479 = store(a_477, i0, e_478)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.12/0.39 tff(8,plain,
% 0.12/0.39 (store(a_477, i0, e_478) = a_479),
% 0.12/0.39 inference(symmetry,[status(thm)],[7])).
% 0.12/0.39 tff(9,plain,
% 0.12/0.39 ((e_478 = select(a_475, i2)) <=> (e_478 = select(a_475, i2))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(10,axiom,(e_478 = select(a_475, i2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp20')).
% 0.12/0.39 tff(11,plain,
% 0.12/0.39 (e_478 = select(a_475, i2)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.12/0.39 tff(12,plain,
% 0.12/0.39 (select(a_475, i2) = e_478),
% 0.12/0.39 inference(symmetry,[status(thm)],[11])).
% 0.12/0.39 tff(13,plain,
% 0.12/0.39 ((e_474 = select(a_471, i3)) <=> (e_474 = select(a_471, i3))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(14,axiom,(e_474 = select(a_471, i3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp18')).
% 0.12/0.39 tff(15,plain,
% 0.12/0.39 (e_474 = select(a_471, i3)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[14, 13])).
% 0.12/0.39 tff(16,plain,
% 0.12/0.39 (select(a_471, i3) = e_474),
% 0.12/0.39 inference(symmetry,[status(thm)],[15])).
% 0.12/0.39 tff(17,plain,
% 0.12/0.39 ((a_473 = store(a_471, i3, e_472)) <=> (a_473 = store(a_471, i3, e_472))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(18,axiom,(a_473 = store(a_471, i3, e_472)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp4')).
% 0.12/0.39 tff(19,plain,
% 0.12/0.39 (a_473 = store(a_471, i3, e_472)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.12/0.39 tff(20,plain,
% 0.12/0.39 (store(a_471, i3, e_472) = a_473),
% 0.12/0.39 inference(symmetry,[status(thm)],[19])).
% 0.12/0.39 tff(21,plain,
% 0.12/0.39 (store(store(a_471, i3, e_472), i2, select(a_471, i3)) = store(a_473, i2, e_474)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[20, 16])).
% 0.12/0.39 tff(22,plain,
% 0.12/0.39 (store(a_473, i2, e_474) = store(store(a_471, i3, e_472), i2, select(a_471, i3))),
% 0.12/0.39 inference(symmetry,[status(thm)],[21])).
% 0.12/0.39 tff(23,plain,
% 0.12/0.39 ((a_475 = store(a_473, i2, e_474)) <=> (a_475 = store(a_473, i2, e_474))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(24,axiom,(a_475 = store(a_473, i2, e_474)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp5')).
% 0.12/0.39 tff(25,plain,
% 0.12/0.39 (a_475 = store(a_473, i2, e_474)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.12/0.39 tff(26,plain,
% 0.12/0.39 (a_475 = store(store(a_471, i3, e_472), i2, select(a_471, i3))),
% 0.12/0.39 inference(transitivity,[status(thm)],[25, 22])).
% 0.12/0.39 tff(27,plain,
% 0.12/0.39 (select(a_475, i2) = select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i2)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[26])).
% 0.12/0.39 tff(28,plain,
% 0.12/0.39 (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i2) = select(a_475, i2)),
% 0.12/0.39 inference(symmetry,[status(thm)],[27])).
% 0.12/0.39 tff(29,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E) <=> ![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(30,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E) <=> ![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(31,axiom,(![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a1')).
% 0.12/0.39 tff(32,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.12/0.39 tff(33,plain,(
% 0.12/0.39 ![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.39 inference(skolemize,[status(sab)],[32])).
% 0.12/0.39 tff(34,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[33, 29])).
% 0.12/0.39 tff(35,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i2) = select(a_471, i3))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(36,plain,
% 0.12/0.39 (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i2) = select(a_471, i3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[35, 34])).
% 0.12/0.39 tff(37,plain,
% 0.12/0.39 (select(a_471, i3) = select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i2)),
% 0.12/0.39 inference(symmetry,[status(thm)],[36])).
% 0.12/0.39 tff(38,plain,
% 0.12/0.39 ((e_470 = select(a_467, i0)) <=> (e_470 = select(a_467, i0))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(39,axiom,(e_470 = select(a_467, i0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp16')).
% 0.12/0.39 tff(40,plain,
% 0.12/0.39 (e_470 = select(a_467, i0)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.12/0.39 tff(41,plain,
% 0.12/0.39 (select(a_467, i0) = e_470),
% 0.12/0.39 inference(symmetry,[status(thm)],[40])).
% 0.12/0.39 tff(42,plain,
% 0.12/0.39 ((a_469 = store(a_467, i0, e_468)) <=> (a_469 = store(a_467, i0, e_468))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(43,axiom,(a_469 = store(a_467, i0, e_468)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp2')).
% 0.12/0.39 tff(44,plain,
% 0.12/0.39 (a_469 = store(a_467, i0, e_468)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.12/0.39 tff(45,plain,
% 0.12/0.39 (store(a_467, i0, e_468) = a_469),
% 0.12/0.39 inference(symmetry,[status(thm)],[44])).
% 0.12/0.39 tff(46,plain,
% 0.12/0.39 (store(store(a_467, i0, e_468), i3, select(a_467, i0)) = store(a_469, i3, e_470)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[45, 41])).
% 0.12/0.39 tff(47,plain,
% 0.12/0.39 (store(a_469, i3, e_470) = store(store(a_467, i0, e_468), i3, select(a_467, i0))),
% 0.12/0.39 inference(symmetry,[status(thm)],[46])).
% 0.12/0.39 tff(48,plain,
% 0.12/0.39 ((a_471 = store(a_469, i3, e_470)) <=> (a_471 = store(a_469, i3, e_470))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(49,axiom,(a_471 = store(a_469, i3, e_470)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp3')).
% 0.12/0.39 tff(50,plain,
% 0.12/0.39 (a_471 = store(a_469, i3, e_470)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.12/0.39 tff(51,plain,
% 0.12/0.39 (a_471 = store(store(a_467, i0, e_468), i3, select(a_467, i0))),
% 0.12/0.39 inference(transitivity,[status(thm)],[50, 47])).
% 0.12/0.39 tff(52,plain,
% 0.12/0.39 (select(a_471, i3) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i3)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[51])).
% 0.12/0.39 tff(53,plain,
% 0.12/0.39 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i3) = select(a_471, i3)),
% 0.12/0.39 inference(symmetry,[status(thm)],[52])).
% 0.12/0.39 tff(54,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i3) = select(a_467, i0))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(55,plain,
% 0.12/0.39 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i3) = select(a_467, i0)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[54, 34])).
% 0.12/0.39 tff(56,plain,
% 0.12/0.39 (select(a_467, i0) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i3)),
% 0.12/0.39 inference(symmetry,[status(thm)],[55])).
% 0.12/0.39 tff(57,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i3) = select(a_467, i0))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(58,plain,
% 0.12/0.39 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i3) = select(a_467, i0)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[57, 34])).
% 0.12/0.39 tff(59,plain,
% 0.12/0.39 ((a_467 = store(a_466, i1, e_465)) <=> (a_467 = store(a_466, i1, e_465))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(60,axiom,(a_467 = store(a_466, i1, e_465)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp1')).
% 0.12/0.39 tff(61,plain,
% 0.12/0.39 (a_467 = store(a_466, i1, e_465)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.12/0.39 tff(62,plain,
% 0.12/0.39 (store(a_466, i1, e_465) = a_467),
% 0.12/0.39 inference(symmetry,[status(thm)],[61])).
% 0.12/0.39 tff(63,plain,
% 0.12/0.39 (store(store(a_466, i1, e_465), i3, select(a_467, i0)) = store(a_467, i3, e_470)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[62, 41])).
% 0.12/0.39 tff(64,plain,
% 0.12/0.39 (store(a_467, i3, e_470) = store(store(a_466, i1, e_465), i3, select(a_467, i0))),
% 0.12/0.39 inference(symmetry,[status(thm)],[63])).
% 0.12/0.39 tff(65,plain,
% 0.12/0.39 (select(store(a_467, i3, e_470), i3) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i3)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[64])).
% 0.12/0.39 tff(66,plain,
% 0.12/0.39 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i3) = select(store(a_467, i3, e_470), i3)),
% 0.12/0.39 inference(symmetry,[status(thm)],[65])).
% 0.12/0.39 tff(67,plain,
% 0.12/0.39 (select(a_467, i0) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i3)),
% 0.12/0.39 inference(symmetry,[status(thm)],[58])).
% 0.12/0.39 tff(68,assumption,(~(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))), introduced(assumption)).
% 0.12/0.39 tff(69,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J))) <=> ![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(70,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J))) <=> ![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(71,axiom,(![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','a2')).
% 0.12/0.39 tff(72,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.12/0.39 tff(73,plain,(
% 0.12/0.39 ![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))),
% 0.12/0.39 inference(skolemize,[status(sab)],[72])).
% 0.12/0.39 tff(74,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[73, 69])).
% 0.12/0.39 tff(75,plain,
% 0.12/0.39 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i3) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i3) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(76,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i3) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(77,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i3) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.12/0.40 tff(78,plain,
% 0.12/0.40 ((i0 = i3) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[77, 74])).
% 0.12/0.40 tff(79,plain,
% 0.12/0.40 (i0 = i3),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[78, 68])).
% 0.12/0.40 tff(80,plain,
% 0.12/0.40 (i3 = i0),
% 0.12/0.40 inference(symmetry,[status(thm)],[79])).
% 0.12/0.40 tff(81,plain,
% 0.12/0.40 (select(a_467, i3) = select(a_467, i0)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[80])).
% 0.12/0.40 tff(82,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0) = select(a_467, i3))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(83,plain,
% 0.12/0.40 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0) = select(a_467, i3)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[82, 34])).
% 0.12/0.40 tff(84,plain,
% 0.12/0.40 ((e_468 = select(a_467, i3)) <=> (e_468 = select(a_467, i3))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(85,axiom,(e_468 = select(a_467, i3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp15')).
% 0.12/0.40 tff(86,plain,
% 0.12/0.40 (e_468 = select(a_467, i3)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.12/0.40 tff(87,plain,
% 0.12/0.40 (select(a_467, i3) = e_468),
% 0.12/0.40 inference(symmetry,[status(thm)],[86])).
% 0.12/0.40 tff(88,plain,
% 0.12/0.40 ((a_480 = store(a_467, i3, e_470)) <=> (a_480 = store(a_467, i3, e_470))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(89,axiom,(a_480 = store(a_467, i3, e_470)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp8')).
% 0.12/0.40 tff(90,plain,
% 0.12/0.40 (a_480 = store(a_467, i3, e_470)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.12/0.40 tff(91,plain,
% 0.12/0.40 (store(a_467, i3, e_470) = a_480),
% 0.12/0.40 inference(symmetry,[status(thm)],[90])).
% 0.12/0.40 tff(92,plain,
% 0.12/0.40 (store(store(a_467, i3, e_470), i0, select(a_467, i3)) = store(a_480, i0, e_468)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[91, 87])).
% 0.12/0.40 tff(93,plain,
% 0.12/0.40 (store(a_480, i0, e_468) = store(store(a_467, i3, e_470), i0, select(a_467, i3))),
% 0.12/0.40 inference(symmetry,[status(thm)],[92])).
% 0.12/0.40 tff(94,plain,
% 0.12/0.40 ((a_481 = store(a_480, i0, e_468)) <=> (a_481 = store(a_480, i0, e_468))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(95,axiom,(a_481 = store(a_480, i0, e_468)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp9')).
% 0.12/0.40 tff(96,plain,
% 0.12/0.40 (a_481 = store(a_480, i0, e_468)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.12/0.40 tff(97,plain,
% 0.12/0.40 (a_481 = store(store(a_467, i3, e_470), i0, select(a_467, i3))),
% 0.12/0.40 inference(transitivity,[status(thm)],[96, 93])).
% 0.12/0.40 tff(98,plain,
% 0.12/0.40 (select(a_481, i3) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[97, 80])).
% 0.12/0.40 tff(99,plain,
% 0.12/0.40 (store(a_480, i0, e_468) = a_481),
% 0.12/0.40 inference(symmetry,[status(thm)],[96])).
% 0.12/0.40 tff(100,plain,
% 0.12/0.40 (store(store(a_467, i3, e_470), i0, select(a_467, i3)) = a_481),
% 0.12/0.40 inference(transitivity,[status(thm)],[92, 99])).
% 0.12/0.40 tff(101,plain,
% 0.12/0.40 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(a_481, i3)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[100])).
% 0.12/0.40 tff(102,plain,
% 0.12/0.40 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)),
% 0.12/0.40 inference(transitivity,[status(thm)],[101, 98, 83, 81, 67, 66])).
% 0.12/0.40 tff(103,plain,
% 0.12/0.40 ($false),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[68, 102])).
% 0.12/0.40 tff(104,plain,(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.40 tff(105,plain,
% 0.12/0.40 (select(a_481, i3) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[97])).
% 0.12/0.40 tff(106,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i2) = select(a_481, i3))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(107,plain,
% 0.20/0.40 (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i2) = select(a_481, i3)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[106, 34])).
% 0.20/0.40 tff(108,plain,
% 0.20/0.40 ((e_484 = select(a_481, i3)) <=> (e_484 = select(a_481, i3))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(109,axiom,(e_484 = select(a_481, i3)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp22')).
% 0.20/0.40 tff(110,plain,
% 0.20/0.40 (e_484 = select(a_481, i3)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[109, 108])).
% 0.20/0.40 tff(111,plain,
% 0.20/0.40 (select(a_481, i3) = e_484),
% 0.20/0.40 inference(symmetry,[status(thm)],[110])).
% 0.20/0.40 tff(112,plain,
% 0.20/0.40 ((a_483 = store(a_481, i3, e_482)) <=> (a_483 = store(a_481, i3, e_482))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(113,axiom,(a_483 = store(a_481, i3, e_482)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp10')).
% 0.20/0.40 tff(114,plain,
% 0.20/0.40 (a_483 = store(a_481, i3, e_482)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.20/0.40 tff(115,plain,
% 0.20/0.40 (store(a_481, i3, e_482) = a_483),
% 0.20/0.40 inference(symmetry,[status(thm)],[114])).
% 0.20/0.40 tff(116,plain,
% 0.20/0.40 (store(store(a_481, i3, e_482), i2, select(a_481, i3)) = store(a_483, i2, e_484)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[115, 111])).
% 0.20/0.40 tff(117,plain,
% 0.20/0.40 (store(a_483, i2, e_484) = store(store(a_481, i3, e_482), i2, select(a_481, i3))),
% 0.20/0.40 inference(symmetry,[status(thm)],[116])).
% 0.20/0.40 tff(118,plain,
% 0.20/0.40 ((a_485 = store(a_483, i2, e_484)) <=> (a_485 = store(a_483, i2, e_484))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(119,axiom,(a_485 = store(a_483, i2, e_484)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp11')).
% 0.20/0.40 tff(120,plain,
% 0.20/0.40 (a_485 = store(a_483, i2, e_484)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.20/0.40 tff(121,plain,
% 0.20/0.40 (a_485 = store(store(a_481, i3, e_482), i2, select(a_481, i3))),
% 0.20/0.40 inference(transitivity,[status(thm)],[120, 117])).
% 0.20/0.40 tff(122,plain,
% 0.20/0.40 (select(a_485, i2) = select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i2)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[121])).
% 0.20/0.40 tff(123,assumption,(~(i0 = i2)), introduced(assumption)).
% 0.20/0.40 tff(124,plain,
% 0.20/0.40 ((i0 = i2) <=> (i2 = i0)),
% 0.20/0.40 inference(commutativity,[status(thm)],[])).
% 0.20/0.40 tff(125,plain,
% 0.20/0.40 ((i2 = i0) <=> (i0 = i2)),
% 0.20/0.40 inference(symmetry,[status(thm)],[124])).
% 0.20/0.40 tff(126,assumption,(i0 = sk(a_479, a_489)), introduced(assumption)).
% 0.20/0.40 tff(127,plain,
% 0.20/0.40 (sk(a_479, a_489) = i0),
% 0.20/0.40 inference(symmetry,[status(thm)],[126])).
% 0.20/0.40 tff(128,plain,
% 0.20/0.40 ((i2 = sk(a_479, a_489)) <=> (i2 = i0)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[127])).
% 0.20/0.40 tff(129,plain,
% 0.20/0.40 ((i2 = sk(a_479, a_489)) <=> (i0 = i2)),
% 0.20/0.40 inference(transitivity,[status(thm)],[128, 125])).
% 0.20/0.40 tff(130,plain,
% 0.20/0.40 ((e_492 = e_491) <=> (e_491 = e_492)),
% 0.20/0.40 inference(commutativity,[status(thm)],[])).
% 0.20/0.40 tff(131,plain,
% 0.20/0.40 ((e_491 = select(a_479, i_490)) <=> (e_491 = select(a_479, i_490))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(132,axiom,(e_491 = select(a_479, i_490)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp25')).
% 0.20/0.40 tff(133,plain,
% 0.20/0.40 (e_491 = select(a_479, i_490)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.20/0.40 tff(134,plain,
% 0.20/0.40 (select(a_479, i_490) = e_491),
% 0.20/0.40 inference(symmetry,[status(thm)],[133])).
% 0.20/0.40 tff(135,plain,
% 0.20/0.40 ((i_490 = sk(a_479, a_489)) <=> (i_490 = sk(a_479, a_489))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(136,axiom,(i_490 = sk(a_479, a_489)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp27')).
% 0.20/0.40 tff(137,plain,
% 0.20/0.40 (i_490 = sk(a_479, a_489)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.20/0.40 tff(138,plain,
% 0.20/0.40 (i_490 = i0),
% 0.20/0.40 inference(transitivity,[status(thm)],[137, 127])).
% 0.20/0.40 tff(139,plain,
% 0.20/0.40 ((a_477 = store(a_475, i2, e_476)) <=> (a_477 = store(a_475, i2, e_476))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(140,axiom,(a_477 = store(a_475, i2, e_476)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp6')).
% 0.20/0.40 tff(141,plain,
% 0.20/0.40 (a_477 = store(a_475, i2, e_476)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.20/0.40 tff(142,plain,
% 0.20/0.40 (store(a_475, i2, e_476) = a_477),
% 0.20/0.40 inference(symmetry,[status(thm)],[141])).
% 0.20/0.40 tff(143,plain,
% 0.20/0.40 (store(store(a_475, i2, e_476), i0, select(a_475, i2)) = store(a_477, i0, e_478)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[142, 12])).
% 0.20/0.40 tff(144,plain,
% 0.20/0.40 (store(a_477, i0, e_478) = store(store(a_475, i2, e_476), i0, select(a_475, i2))),
% 0.20/0.40 inference(symmetry,[status(thm)],[143])).
% 0.20/0.40 tff(145,plain,
% 0.20/0.40 (a_479 = store(store(a_475, i2, e_476), i0, select(a_475, i2))),
% 0.20/0.40 inference(transitivity,[status(thm)],[7, 144])).
% 0.20/0.40 tff(146,plain,
% 0.20/0.40 (select(a_479, i_490) = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[145, 138])).
% 0.20/0.40 tff(147,plain,
% 0.20/0.40 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0) = select(a_479, i_490)),
% 0.20/0.40 inference(symmetry,[status(thm)],[146])).
% 0.20/0.40 tff(148,plain,
% 0.20/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0) = select(a_475, i2))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(149,plain,
% 0.20/0.40 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0) = select(a_475, i2)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[148, 34])).
% 0.20/0.40 tff(150,plain,
% 0.20/0.40 (select(a_475, i2) = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0)),
% 0.20/0.40 inference(symmetry,[status(thm)],[149])).
% 0.20/0.40 tff(151,plain,
% 0.20/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_483, i2, e_484), i0, select(a_485, i2)), i0) = select(a_485, i2))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(152,plain,
% 0.20/0.40 (select(store(store(a_483, i2, e_484), i0, select(a_485, i2)), i0) = select(a_485, i2)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[151, 34])).
% 0.20/0.40 tff(153,plain,
% 0.20/0.40 ((e_486 = select(a_485, i2)) <=> (e_486 = select(a_485, i2))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(154,axiom,(e_486 = select(a_485, i2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp23')).
% 0.20/0.40 tff(155,plain,
% 0.20/0.40 (e_486 = select(a_485, i2)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[154, 153])).
% 0.20/0.40 tff(156,plain,
% 0.20/0.40 (select(a_485, i2) = e_486),
% 0.20/0.40 inference(symmetry,[status(thm)],[155])).
% 0.20/0.40 tff(157,plain,
% 0.20/0.40 (store(a_483, i2, e_484) = a_485),
% 0.20/0.40 inference(symmetry,[status(thm)],[120])).
% 0.20/0.40 tff(158,plain,
% 0.20/0.40 (store(store(a_483, i2, e_484), i0, select(a_485, i2)) = store(a_485, i0, e_486)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[157, 156])).
% 0.20/0.40 tff(159,plain,
% 0.20/0.40 (store(a_485, i0, e_486) = store(store(a_483, i2, e_484), i0, select(a_485, i2))),
% 0.20/0.40 inference(symmetry,[status(thm)],[158])).
% 0.20/0.40 tff(160,plain,
% 0.20/0.40 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i0, select(a_485, i2)), i0)),
% 0.20/0.40 inference(monotonicity,[status(thm)],[159, 127])).
% 0.20/0.40 tff(161,plain,
% 0.20/0.40 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = e_491),
% 0.20/0.40 inference(transitivity,[status(thm)],[160, 152, 122, 107, 105, 104, 65, 58, 56, 53, 37, 28, 150, 147, 134])).
% 0.20/0.40 tff(162,plain,
% 0.20/0.40 (sk(a_479, a_489) = i_490),
% 0.20/0.40 inference(symmetry,[status(thm)],[137])).
% 0.20/0.40 tff(163,plain,
% 0.20/0.40 ((a_489 = store(a_487, i2, e_488)) <=> (a_489 = store(a_487, i2, e_488))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(164,axiom,(a_489 = store(a_487, i2, e_488)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp13')).
% 0.20/0.40 tff(165,plain,
% 0.20/0.40 (a_489 = store(a_487, i2, e_488)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[164, 163])).
% 0.20/0.40 tff(166,plain,
% 0.20/0.40 (store(a_487, i2, e_488) = a_489),
% 0.20/0.40 inference(symmetry,[status(thm)],[165])).
% 0.20/0.40 tff(167,plain,
% 0.20/0.40 ((e_488 = select(a_485, i0)) <=> (e_488 = select(a_485, i0))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(168,axiom,(e_488 = select(a_485, i0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp24')).
% 0.20/0.40 tff(169,plain,
% 0.20/0.40 (e_488 = select(a_485, i0)),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[168, 167])).
% 0.20/0.40 tff(170,plain,
% 0.20/0.40 (select(a_485, i0) = e_488),
% 0.20/0.40 inference(symmetry,[status(thm)],[169])).
% 0.20/0.40 tff(171,plain,
% 0.20/0.40 ((a_487 = store(a_485, i0, e_486)) <=> (a_487 = store(a_485, i0, e_486))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(172,axiom,(a_487 = store(a_485, i0, e_486)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp12')).
% 0.20/0.41 tff(173,plain,
% 0.20/0.41 (a_487 = store(a_485, i0, e_486)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[172, 171])).
% 0.20/0.41 tff(174,plain,
% 0.20/0.41 (store(a_485, i0, e_486) = a_487),
% 0.20/0.41 inference(symmetry,[status(thm)],[173])).
% 0.20/0.41 tff(175,plain,
% 0.20/0.41 (store(store(a_485, i0, e_486), i2, select(a_485, i0)) = store(a_487, i2, e_488)),
% 0.20/0.41 inference(monotonicity,[status(thm)],[174, 170])).
% 0.20/0.41 tff(176,plain,
% 0.20/0.41 (store(store(a_485, i0, e_486), i2, select(a_485, i0)) = a_489),
% 0.20/0.41 inference(transitivity,[status(thm)],[175, 166])).
% 0.20/0.41 tff(177,plain,
% 0.20/0.41 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(a_489, i_490)),
% 0.20/0.41 inference(monotonicity,[status(thm)],[176, 162])).
% 0.20/0.41 tff(178,plain,
% 0.20/0.41 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = e_492),
% 0.20/0.41 inference(transitivity,[status(thm)],[177, 4])).
% 0.20/0.41 tff(179,plain,
% 0.20/0.41 ((select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))) <=> (e_492 = e_491)),
% 0.20/0.41 inference(monotonicity,[status(thm)],[178, 161])).
% 0.20/0.41 tff(180,plain,
% 0.20/0.41 ((select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))) <=> (e_491 = e_492)),
% 0.20/0.41 inference(transitivity,[status(thm)],[179, 130])).
% 0.20/0.41 tff(181,plain,
% 0.20/0.41 ((e_491 = e_492) <=> (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))),
% 0.20/0.41 inference(symmetry,[status(thm)],[180])).
% 0.20/0.41 tff(182,plain,
% 0.20/0.41 ((~(e_491 = e_492)) <=> (~(select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[181])).
% 0.20/0.41 tff(183,plain,
% 0.20/0.41 ((~(e_491 = e_492)) <=> (~(e_491 = e_492))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(184,axiom,(~(e_491 = e_492)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','goal')).
% 0.20/0.41 tff(185,plain,
% 0.20/0.41 (~(e_491 = e_492)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[184, 183])).
% 0.20/0.41 tff(186,plain,
% 0.20/0.41 (~(select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[185, 182])).
% 0.20/0.41 tff(187,plain,
% 0.20/0.41 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(188,plain,
% 0.20/0.41 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))))),
% 0.20/0.41 inference(quant_inst,[status(thm)],[])).
% 0.20/0.41 tff(189,plain,
% 0.20/0.41 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[188, 187])).
% 0.20/0.41 tff(190,plain,
% 0.20/0.41 ((i2 = sk(a_479, a_489)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[189, 74])).
% 0.20/0.41 tff(191,plain,
% 0.20/0.41 (i2 = sk(a_479, a_489)),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[190, 186])).
% 0.20/0.41 tff(192,plain,
% 0.20/0.41 (i0 = i2),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[191, 129])).
% 0.20/0.41 tff(193,plain,
% 0.20/0.41 ($false),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[123, 192])).
% 0.20/0.41 tff(194,plain,((~(i0 = sk(a_479, a_489))) | (i0 = i2)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.41 tff(195,plain,
% 0.20/0.41 (~(i0 = sk(a_479, a_489))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[194, 123])).
% 0.20/0.41 tff(196,assumption,(~(i3 = i0)), introduced(assumption)).
% 0.20/0.41 tff(197,plain,
% 0.20/0.41 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0)))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(198,plain,
% 0.20/0.41 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0)))),
% 0.20/0.41 inference(quant_inst,[status(thm)],[])).
% 0.20/0.41 tff(199,plain,
% 0.20/0.41 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[198, 197])).
% 0.20/0.41 tff(200,plain,
% 0.20/0.41 ((i3 = i0) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[199, 74])).
% 0.20/0.41 tff(201,plain,
% 0.20/0.41 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0)),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[200, 196])).
% 0.20/0.41 tff(202,plain,
% 0.20/0.41 (store(a_487, i2, e_488) = store(store(a_485, i0, e_486), i2, select(a_485, i0))),
% 0.20/0.41 inference(symmetry,[status(thm)],[175])).
% 0.20/0.41 tff(203,plain,
% 0.20/0.41 (a_489 = store(store(a_485, i0, e_486), i2, select(a_485, i0))),
% 0.20/0.41 inference(transitivity,[status(thm)],[165, 202])).
% 0.20/0.41 tff(204,plain,
% 0.20/0.41 (select(a_489, i_490) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[203, 137])).
% 0.20/0.41 tff(205,plain,
% 0.20/0.41 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(a_489, i_490)),
% 0.20/0.41 inference(symmetry,[status(thm)],[204])).
% 0.20/0.41 tff(206,assumption,(~(i2 = sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.41 tff(207,plain,
% 0.20/0.41 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[190, 206])).
% 0.20/0.41 tff(208,plain,
% 0.20/0.41 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.41 inference(symmetry,[status(thm)],[207])).
% 0.20/0.41 tff(209,plain,
% 0.20/0.41 (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i2) = select(a_485, i2)),
% 0.20/0.41 inference(symmetry,[status(thm)],[122])).
% 0.20/0.41 tff(210,plain,
% 0.20/0.41 (select(a_481, i3) = select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i2)),
% 0.20/0.41 inference(symmetry,[status(thm)],[107])).
% 0.20/0.41 tff(211,plain,
% 0.20/0.41 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(a_481, i3)),
% 0.20/0.41 inference(symmetry,[status(thm)],[105])).
% 0.20/0.41 tff(212,plain,
% 0.20/0.41 (select(store(a_467, i3, e_470), i3) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3)),
% 0.20/0.41 inference(symmetry,[status(thm)],[104])).
% 0.20/0.41 tff(213,plain,
% 0.20/0.41 (select(a_467, i0) = e_486),
% 0.20/0.41 inference(transitivity,[status(thm)],[67, 66, 212, 211, 210, 209, 156])).
% 0.20/0.41 tff(214,plain,
% 0.20/0.41 (store(store(a_483, i2, e_484), i0, select(a_467, i0)) = store(a_485, i0, e_486)),
% 0.20/0.41 inference(monotonicity,[status(thm)],[157, 213])).
% 0.20/0.41 tff(215,plain,
% 0.20/0.41 (store(a_485, i0, e_486) = store(store(a_483, i2, e_484), i0, select(a_467, i0))),
% 0.20/0.41 inference(symmetry,[status(thm)],[214])).
% 0.20/0.41 tff(216,plain,
% 0.20/0.41 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[215])).
% 0.20/0.42 tff(217,plain,
% 0.20/0.42 (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))),
% 0.20/0.42 inference(symmetry,[status(thm)],[216])).
% 0.20/0.42 tff(218,plain,
% 0.20/0.42 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(219,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))),
% 0.20/0.42 inference(quant_inst,[status(thm)],[])).
% 0.20/0.42 tff(220,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489)))),
% 0.20/0.42 inference(modus_ponens,[status(thm)],[219, 218])).
% 0.20/0.42 tff(221,plain,
% 0.20/0.42 (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.42 inference(unit_resolution,[status(thm)],[220, 74, 195])).
% 0.20/0.42 tff(222,plain,
% 0.20/0.42 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(symmetry,[status(thm)],[221])).
% 0.20/0.42 tff(223,plain,
% 0.20/0.42 (select(a_467, i0) = e_484),
% 0.20/0.42 inference(transitivity,[status(thm)],[67, 66, 212, 211, 111])).
% 0.20/0.42 tff(224,plain,
% 0.20/0.42 (store(store(a_481, i3, e_482), i2, select(a_467, i0)) = store(a_483, i2, e_484)),
% 0.20/0.42 inference(monotonicity,[status(thm)],[115, 223])).
% 0.20/0.42 tff(225,plain,
% 0.20/0.42 (store(a_483, i2, e_484) = store(store(a_481, i3, e_482), i2, select(a_467, i0))),
% 0.20/0.42 inference(symmetry,[status(thm)],[224])).
% 0.20/0.42 tff(226,plain,
% 0.20/0.42 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[225])).
% 0.20/0.42 tff(227,plain,
% 0.20/0.42 (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.42 inference(symmetry,[status(thm)],[226])).
% 0.20/0.42 tff(228,plain,
% 0.20/0.42 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(229,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))))),
% 0.20/0.42 inference(quant_inst,[status(thm)],[])).
% 0.20/0.42 tff(230,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489)))),
% 0.20/0.42 inference(modus_ponens,[status(thm)],[229, 228])).
% 0.20/0.42 tff(231,plain,
% 0.20/0.42 (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.42 inference(unit_resolution,[status(thm)],[230, 74, 206])).
% 0.20/0.42 tff(232,plain,
% 0.20/0.42 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(symmetry,[status(thm)],[231])).
% 0.20/0.42 tff(233,plain,
% 0.20/0.42 ((~(i0 = i2)) <=> (~(i2 = i0))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[124])).
% 0.20/0.42 tff(234,plain,
% 0.20/0.42 (~(i2 = i0)),
% 0.20/0.42 inference(modus_ponens,[status(thm)],[123, 233])).
% 0.20/0.42 tff(235,plain,
% 0.20/0.42 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = i0) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = i0) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0)))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(236,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = i0) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0)))),
% 0.20/0.42 inference(quant_inst,[status(thm)],[])).
% 0.20/0.42 tff(237,plain,
% 0.20/0.42 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = i0) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0))),
% 0.20/0.42 inference(modus_ponens,[status(thm)],[236, 235])).
% 0.20/0.42 tff(238,plain,
% 0.20/0.42 ((i2 = i0) | (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0))),
% 0.20/0.42 inference(unit_resolution,[status(thm)],[237, 74])).
% 0.20/0.42 tff(239,plain,
% 0.20/0.42 (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0)),
% 0.20/0.42 inference(unit_resolution,[status(thm)],[238, 234])).
% 0.20/0.42 tff(240,assumption,(select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0)), introduced(assumption)).
% 0.20/0.42 tff(241,assumption,(~(i0 = sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.42 tff(242,plain,
% 0.20/0.42 (select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.42 inference(unit_resolution,[status(thm)],[220, 74, 241])).
% 0.20/0.42 tff(243,plain,
% 0.20/0.42 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i0, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(symmetry,[status(thm)],[242])).
% 0.20/0.42 tff(244,plain,
% 0.20/0.42 ((e_482 = select(a_481, i2)) <=> (e_482 = select(a_481, i2))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(245,axiom,(e_482 = select(a_481, i2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp21')).
% 0.20/0.42 tff(246,plain,
% 0.20/0.42 (e_482 = select(a_481, i2)),
% 0.20/0.42 inference(modus_ponens,[status(thm)],[245, 244])).
% 0.20/0.42 tff(247,plain,
% 0.20/0.42 (select(a_481, i2) = e_482),
% 0.20/0.42 inference(symmetry,[status(thm)],[246])).
% 0.20/0.42 tff(248,assumption,(i3 = i2), introduced(assumption)).
% 0.20/0.42 tff(249,plain,
% 0.20/0.42 (i2 = i3),
% 0.20/0.42 inference(symmetry,[status(thm)],[248])).
% 0.20/0.42 tff(250,plain,
% 0.20/0.42 (select(a_481, i2) = select(a_481, i3)),
% 0.20/0.42 inference(monotonicity,[status(thm)],[249])).
% 0.20/0.42 tff(251,plain,
% 0.20/0.42 (select(a_481, i3) = select(a_481, i2)),
% 0.20/0.42 inference(symmetry,[status(thm)],[250])).
% 0.20/0.42 tff(252,plain,
% 0.20/0.42 (select(a_467, i0) = e_482),
% 0.20/0.42 inference(transitivity,[status(thm)],[67, 66, 212, 211, 251, 247])).
% 0.20/0.42 tff(253,plain,
% 0.20/0.42 (store(store(a_480, i0, e_468), i2, select(a_467, i0)) = store(a_481, i3, e_482)),
% 0.20/0.42 inference(monotonicity,[status(thm)],[99, 249, 252])).
% 0.20/0.42 tff(254,plain,
% 0.20/0.42 (store(a_481, i3, e_482) = store(store(a_480, i0, e_468), i2, select(a_467, i0))),
% 0.20/0.42 inference(symmetry,[status(thm)],[253])).
% 0.20/0.42 tff(255,plain,
% 0.20/0.42 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[254])).
% 0.20/0.42 tff(256,plain,
% 0.20/0.42 (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[255])).
% 0.20/0.43 tff(257,plain,
% 0.20/0.43 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(258,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.43 inference(quant_inst,[status(thm)],[])).
% 0.20/0.43 tff(259,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[258, 257])).
% 0.20/0.43 tff(260,plain,
% 0.20/0.43 (select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.43 inference(unit_resolution,[status(thm)],[259, 74, 206])).
% 0.20/0.43 tff(261,plain,
% 0.20/0.43 (select(store(a_480, i0, e_468), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[260])).
% 0.20/0.43 tff(262,plain,
% 0.20/0.43 (select(store(a_480, i0, e_468), sk(a_479, a_489)) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.43 inference(monotonicity,[status(thm)],[93])).
% 0.20/0.43 tff(263,plain,
% 0.20/0.43 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[262])).
% 0.20/0.43 tff(264,plain,
% 0.20/0.43 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(265,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.43 inference(quant_inst,[status(thm)],[])).
% 0.20/0.43 tff(266,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[265, 264])).
% 0.20/0.43 tff(267,plain,
% 0.20/0.43 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.43 inference(unit_resolution,[status(thm)],[266, 74, 241])).
% 0.20/0.43 tff(268,plain,
% 0.20/0.43 (select(store(a_467, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[267])).
% 0.20/0.43 tff(269,plain,
% 0.20/0.43 (store(store(a_466, i1, e_465), i2, select(a_467, i0)) = store(a_467, i3, e_470)),
% 0.20/0.43 inference(monotonicity,[status(thm)],[62, 249, 41])).
% 0.20/0.43 tff(270,plain,
% 0.20/0.43 (store(a_467, i3, e_470) = store(store(a_466, i1, e_465), i2, select(a_467, i0))),
% 0.20/0.43 inference(symmetry,[status(thm)],[269])).
% 0.20/0.43 tff(271,plain,
% 0.20/0.43 (select(store(a_467, i3, e_470), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.43 inference(monotonicity,[status(thm)],[270])).
% 0.20/0.43 tff(272,plain,
% 0.20/0.43 (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[271])).
% 0.20/0.43 tff(273,plain,
% 0.20/0.43 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(274,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.43 inference(quant_inst,[status(thm)],[])).
% 0.20/0.43 tff(275,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489)))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[274, 273])).
% 0.20/0.43 tff(276,plain,
% 0.20/0.43 (select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.43 inference(unit_resolution,[status(thm)],[275, 74, 206])).
% 0.20/0.43 tff(277,plain,
% 0.20/0.43 (select(store(a_466, i1, e_465), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[276])).
% 0.20/0.43 tff(278,plain,
% 0.20/0.43 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(279,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.43 inference(quant_inst,[status(thm)],[])).
% 0.20/0.43 tff(280,plain,
% 0.20/0.43 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489)))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[279, 278])).
% 0.20/0.43 tff(281,plain,
% 0.20/0.43 (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.43 inference(unit_resolution,[status(thm)],[280, 74, 241])).
% 0.20/0.43 tff(282,plain,
% 0.20/0.43 (store(store(a_466, i1, e_465), i0, select(a_467, i3)) = store(a_467, i0, e_468)),
% 0.20/0.43 inference(monotonicity,[status(thm)],[62, 87])).
% 0.20/0.43 tff(283,plain,
% 0.20/0.43 (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))),
% 0.20/0.43 inference(monotonicity,[status(thm)],[282])).
% 0.20/0.43 tff(284,plain,
% 0.20/0.43 (select(store(a_467, i0, e_468), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.43 inference(symmetry,[status(thm)],[283])).
% 0.20/0.43 tff(285,plain,
% 0.20/0.44 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(286,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(287,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[286, 285])).
% 0.20/0.44 tff(288,plain,
% 0.20/0.44 (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[287, 74, 206])).
% 0.20/0.44 tff(289,plain,
% 0.20/0.44 (store(store(a_467, i0, e_468), i2, select(a_467, i0)) = store(a_469, i3, e_470)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[45, 249, 41])).
% 0.20/0.44 tff(290,plain,
% 0.20/0.44 (select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))),
% 0.20/0.44 inference(monotonicity,[status(thm)],[289])).
% 0.20/0.44 tff(291,plain,
% 0.20/0.44 (select(store(a_469, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i0, e_468), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.44 inference(symmetry,[status(thm)],[290])).
% 0.20/0.44 tff(292,plain,
% 0.20/0.44 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(293,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(294,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[293, 292])).
% 0.20/0.44 tff(295,plain,
% 0.20/0.44 (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[294, 74, 206])).
% 0.20/0.44 tff(296,plain,
% 0.20/0.44 ((e_472 = select(a_471, i2)) <=> (e_472 = select(a_471, i2))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(297,axiom,(e_472 = select(a_471, i2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp17')).
% 0.20/0.44 tff(298,plain,
% 0.20/0.44 (e_472 = select(a_471, i2)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[297, 296])).
% 0.20/0.44 tff(299,plain,
% 0.20/0.44 (select(a_471, i2) = e_472),
% 0.20/0.44 inference(symmetry,[status(thm)],[298])).
% 0.20/0.44 tff(300,plain,
% 0.20/0.44 (select(a_471, i2) = select(a_471, i3)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[249])).
% 0.20/0.44 tff(301,plain,
% 0.20/0.44 (select(a_471, i3) = select(a_471, i2)),
% 0.20/0.44 inference(symmetry,[status(thm)],[300])).
% 0.20/0.44 tff(302,plain,
% 0.20/0.44 (select(a_467, i0) = e_472),
% 0.20/0.44 inference(transitivity,[status(thm)],[56, 53, 301, 299])).
% 0.20/0.44 tff(303,plain,
% 0.20/0.44 (store(a_469, i3, e_470) = a_471),
% 0.20/0.44 inference(symmetry,[status(thm)],[50])).
% 0.20/0.44 tff(304,plain,
% 0.20/0.44 (store(store(a_469, i3, e_470), i2, select(a_467, i0)) = store(a_471, i3, e_472)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[303, 249, 302])).
% 0.20/0.44 tff(305,plain,
% 0.20/0.44 (select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))),
% 0.20/0.44 inference(monotonicity,[status(thm)],[304])).
% 0.20/0.44 tff(306,plain,
% 0.20/0.44 (select(store(a_471, i3, e_472), sk(a_479, a_489)) = select(store(store(a_469, i3, e_470), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.44 inference(symmetry,[status(thm)],[305])).
% 0.20/0.44 tff(307,plain,
% 0.20/0.44 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(308,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(309,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[308, 307])).
% 0.20/0.44 tff(310,plain,
% 0.20/0.44 (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[309, 74, 206])).
% 0.20/0.44 tff(311,plain,
% 0.20/0.44 (select(a_467, i0) = e_474),
% 0.20/0.44 inference(transitivity,[status(thm)],[56, 53, 16])).
% 0.20/0.44 tff(312,plain,
% 0.20/0.44 (store(store(a_471, i3, e_472), i2, select(a_467, i0)) = store(a_473, i2, e_474)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[20, 311])).
% 0.20/0.44 tff(313,plain,
% 0.20/0.44 (select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))),
% 0.20/0.44 inference(monotonicity,[status(thm)],[312])).
% 0.20/0.44 tff(314,plain,
% 0.20/0.44 (select(store(a_473, i2, e_474), sk(a_479, a_489)) = select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.44 inference(symmetry,[status(thm)],[313])).
% 0.20/0.44 tff(315,plain,
% 0.20/0.44 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(316,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(317,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[316, 315])).
% 0.20/0.44 tff(318,plain,
% 0.20/0.44 ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[317, 74])).
% 0.20/0.44 tff(319,plain,
% 0.20/0.44 (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[318, 206])).
% 0.20/0.44 tff(320,plain,
% 0.20/0.44 ((e_476 = select(a_475, i0)) <=> (e_476 = select(a_475, i0))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(321,axiom,(e_476 = select(a_475, i0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','hyp19')).
% 0.20/0.44 tff(322,plain,
% 0.20/0.44 (e_476 = select(a_475, i0)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[321, 320])).
% 0.20/0.44 tff(323,plain,
% 0.20/0.44 (select(a_475, i0) = e_476),
% 0.20/0.44 inference(symmetry,[status(thm)],[322])).
% 0.20/0.44 tff(324,plain,
% 0.20/0.44 (store(a_473, i2, e_474) = a_475),
% 0.20/0.44 inference(symmetry,[status(thm)],[25])).
% 0.20/0.44 tff(325,plain,
% 0.20/0.44 (store(store(a_473, i2, e_474), i2, select(a_475, i0)) = store(a_475, i2, e_476)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[324, 323])).
% 0.20/0.44 tff(326,plain,
% 0.20/0.44 (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.44 inference(monotonicity,[status(thm)],[325])).
% 0.20/0.44 tff(327,plain,
% 0.20/0.44 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489))),
% 0.20/0.44 inference(symmetry,[status(thm)],[326])).
% 0.20/0.44 tff(328,plain,
% 0.20/0.44 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(329,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(330,plain,
% 0.20/0.44 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[329, 328])).
% 0.20/0.44 tff(331,plain,
% 0.20/0.44 ((i0 = sk(a_479, a_489)) | (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[330, 74])).
% 0.20/0.44 tff(332,plain,
% 0.20/0.44 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[331, 241])).
% 0.20/0.44 tff(333,plain,
% 0.20/0.44 (store(store(a_475, i2, e_476), i0, select(a_475, i2)) = a_479),
% 0.20/0.44 inference(transitivity,[status(thm)],[143, 8])).
% 0.20/0.44 tff(334,plain,
% 0.20/0.44 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(a_479, i_490)),
% 0.20/0.44 inference(monotonicity,[status(thm)],[333, 162])).
% 0.20/0.44 tff(335,plain,
% 0.20/0.44 (select(a_479, i_490) = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489))),
% 0.20/0.44 inference(symmetry,[status(thm)],[334])).
% 0.20/0.44 tff(336,plain,
% 0.20/0.44 (e_491 = e_492),
% 0.20/0.44 inference(transitivity,[status(thm)],[133, 335, 332, 327, 319, 314, 310, 306, 295, 291, 288, 284, 281, 277, 272, 268, 263, 261, 256, 232, 227, 243, 217, 208, 205, 4])).
% 0.20/0.44 tff(337,plain,
% 0.20/0.44 ($false),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[185, 336])).
% 0.20/0.44 tff(338,plain,((i2 = sk(a_479, a_489)) | (~(i3 = i2)) | (i0 = sk(a_479, a_489))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.45 tff(339,plain,
% 0.20/0.45 (~(i3 = i2)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[338, 206, 195])).
% 0.20/0.45 tff(340,plain,
% 0.20/0.45 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i2) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i2) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(341,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i2) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(342,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i2) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[341, 340])).
% 0.20/0.45 tff(343,plain,
% 0.20/0.45 ((i3 = i2) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[342, 74])).
% 0.20/0.45 tff(344,plain,
% 0.20/0.45 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[343, 339])).
% 0.20/0.45 tff(345,plain,
% 0.20/0.45 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i2) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i2) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(346,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i2) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(347,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i2) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[346, 345])).
% 0.20/0.45 tff(348,plain,
% 0.20/0.45 (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[347, 74, 123])).
% 0.20/0.45 tff(349,plain,
% 0.20/0.45 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i2) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i2) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(350,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i2) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(351,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i2) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[350, 349])).
% 0.20/0.45 tff(352,plain,
% 0.20/0.45 ((i3 = i2) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[351, 74])).
% 0.20/0.45 tff(353,plain,
% 0.20/0.45 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[352, 339])).
% 0.20/0.45 tff(354,assumption,(select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.45 tff(355,plain,
% 0.20/0.45 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.45 inference(symmetry,[status(thm)],[354])).
% 0.20/0.45 tff(356,assumption,(select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.45 tff(357,plain,
% 0.20/0.45 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.45 inference(symmetry,[status(thm)],[356])).
% 0.20/0.45 tff(358,plain,
% 0.20/0.45 (store(store(a_480, i0, e_468), i3, select(a_481, i2)) = store(a_481, i3, e_482)),
% 0.20/0.45 inference(monotonicity,[status(thm)],[99, 247])).
% 0.20/0.45 tff(359,plain,
% 0.20/0.45 (store(a_481, i3, e_482) = store(store(a_480, i0, e_468), i3, select(a_481, i2))),
% 0.20/0.45 inference(symmetry,[status(thm)],[358])).
% 0.20/0.45 tff(360,plain,
% 0.20/0.45 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[359])).
% 0.20/0.45 tff(361,plain,
% 0.20/0.45 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.45 inference(symmetry,[status(thm)],[360])).
% 0.20/0.45 tff(362,assumption,(~(i3 = sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.45 tff(363,plain,
% 0.20/0.45 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(364,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(365,plain,
% 0.20/0.45 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[364, 363])).
% 0.20/0.45 tff(366,plain,
% 0.20/0.45 ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[365, 74])).
% 0.20/0.45 tff(367,plain,
% 0.20/0.45 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[366, 362])).
% 0.20/0.45 tff(368,plain,
% 0.20/0.45 (select(store(a_480, i0, e_468), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), sk(a_479, a_489))),
% 0.20/0.45 inference(symmetry,[status(thm)],[367])).
% 0.20/0.45 tff(369,plain,
% 0.20/0.45 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0) = select(store(a_480, i0, e_468), i0)),
% 0.20/0.45 inference(monotonicity,[status(thm)],[92])).
% 0.20/0.45 tff(370,plain,
% 0.20/0.45 (select(store(a_480, i0, e_468), i0) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.20/0.45 inference(symmetry,[status(thm)],[369])).
% 0.20/0.45 tff(371,plain,
% 0.20/0.45 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_481, i3, e_482), i0)),
% 0.20/0.45 inference(monotonicity,[status(thm)],[358])).
% 0.20/0.46 tff(372,plain,
% 0.20/0.46 (select(store(a_481, i3, e_482), i0) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0)),
% 0.20/0.46 inference(symmetry,[status(thm)],[371])).
% 0.20/0.46 tff(373,assumption,(select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0)), introduced(assumption)).
% 0.20/0.46 tff(374,plain,
% 0.20/0.46 (store(store(a_481, i3, e_482), i2, select(a_481, i3)) = a_485),
% 0.20/0.46 inference(transitivity,[status(thm)],[116, 157])).
% 0.20/0.46 tff(375,plain,
% 0.20/0.46 (select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(a_485, i0)),
% 0.20/0.46 inference(monotonicity,[status(thm)],[374])).
% 0.20/0.46 tff(376,plain,
% 0.20/0.46 (select(a_485, i0) = select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0)),
% 0.20/0.46 inference(symmetry,[status(thm)],[375])).
% 0.20/0.46 tff(377,plain,
% 0.20/0.46 (select(a_485, i0) = e_468),
% 0.20/0.46 inference(transitivity,[status(thm)],[376, 373, 372, 240, 370, 83, 87])).
% 0.20/0.46 tff(378,plain,
% 0.20/0.46 (store(store(a_467, i3, e_470), i0, select(a_485, i0)) = store(a_480, i0, e_468)),
% 0.20/0.46 inference(monotonicity,[status(thm)],[91, 377])).
% 0.20/0.46 tff(379,plain,
% 0.20/0.46 (store(a_480, i0, e_468) = store(store(a_467, i3, e_470), i0, select(a_485, i0))),
% 0.20/0.46 inference(symmetry,[status(thm)],[378])).
% 0.20/0.46 tff(380,plain,
% 0.20/0.46 (select(store(a_480, i0, e_468), sk(a_479, a_489)) = select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.46 inference(monotonicity,[status(thm)],[379])).
% 0.20/0.46 tff(381,plain,
% 0.20/0.46 (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.46 inference(symmetry,[status(thm)],[380])).
% 0.20/0.46 tff(382,plain,
% 0.20/0.46 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(383,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(384,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[383, 382])).
% 0.20/0.46 tff(385,plain,
% 0.20/0.46 (select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[384, 74, 241])).
% 0.20/0.46 tff(386,plain,
% 0.20/0.46 (select(store(a_467, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i3, e_470), i0, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.46 inference(symmetry,[status(thm)],[385])).
% 0.20/0.46 tff(387,plain,
% 0.20/0.46 (select(store(a_467, i3, e_470), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.46 inference(monotonicity,[status(thm)],[64])).
% 0.20/0.46 tff(388,plain,
% 0.20/0.46 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.46 inference(symmetry,[status(thm)],[387])).
% 0.20/0.46 tff(389,plain,
% 0.20/0.46 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(390,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(391,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[390, 389])).
% 0.20/0.46 tff(392,plain,
% 0.20/0.46 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[391, 74, 362])).
% 0.20/0.46 tff(393,plain,
% 0.20/0.46 (select(store(a_466, i1, e_465), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.46 inference(symmetry,[status(thm)],[392])).
% 0.20/0.46 tff(394,plain,
% 0.20/0.46 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(395,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(396,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[395, 394])).
% 0.20/0.46 tff(397,plain,
% 0.20/0.46 (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[396, 74, 241])).
% 0.20/0.46 tff(398,plain,
% 0.20/0.46 (store(store(a_466, i1, e_465), i0, select(a_485, i0)) = store(a_467, i0, e_468)),
% 0.20/0.46 inference(monotonicity,[status(thm)],[62, 377])).
% 0.20/0.46 tff(399,plain,
% 0.20/0.46 (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))),
% 0.20/0.46 inference(monotonicity,[status(thm)],[398])).
% 0.20/0.46 tff(400,plain,
% 0.20/0.46 (select(store(a_467, i0, e_468), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), sk(a_479, a_489))),
% 0.20/0.46 inference(symmetry,[status(thm)],[399])).
% 0.20/0.46 tff(401,plain,
% 0.20/0.46 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(402,plain,
% 0.20/0.46 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(403,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[402, 401])).
% 0.20/0.47 tff(404,plain,
% 0.20/0.47 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[403, 74, 362])).
% 0.20/0.47 tff(405,plain,
% 0.20/0.47 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[46])).
% 0.20/0.47 tff(406,plain,
% 0.20/0.47 (select(store(a_469, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[405])).
% 0.20/0.47 tff(407,plain,
% 0.20/0.47 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(408,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(409,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[408, 407])).
% 0.20/0.47 tff(410,plain,
% 0.20/0.47 ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[409, 74])).
% 0.20/0.47 tff(411,plain,
% 0.20/0.47 (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[410, 362])).
% 0.20/0.47 tff(412,plain,
% 0.20/0.47 (select(a_471, i2) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[51])).
% 0.20/0.47 tff(413,plain,
% 0.20/0.47 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(a_471, i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[412])).
% 0.20/0.47 tff(414,assumption,(select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)), introduced(assumption)).
% 0.20/0.47 tff(415,plain,
% 0.20/0.47 (select(store(a_467, i0, e_468), i2) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[414])).
% 0.20/0.47 tff(416,plain,
% 0.20/0.47 (store(a_467, i0, e_468) = store(store(a_466, i1, e_465), i0, select(a_485, i0))),
% 0.20/0.47 inference(symmetry,[status(thm)],[398])).
% 0.20/0.47 tff(417,plain,
% 0.20/0.47 (select(store(a_467, i0, e_468), i2) = select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[416])).
% 0.20/0.47 tff(418,plain,
% 0.20/0.47 (select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_467, i0, e_468), i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[417])).
% 0.20/0.47 tff(419,assumption,(select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2)), introduced(assumption)).
% 0.20/0.47 tff(420,plain,
% 0.20/0.47 (select(store(a_466, i1, e_465), i2) = select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[419])).
% 0.20/0.47 tff(421,assumption,(select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2)), introduced(assumption)).
% 0.20/0.47 tff(422,plain,
% 0.20/0.47 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_467, i3, e_470), i2)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[63])).
% 0.20/0.47 tff(423,plain,
% 0.20/0.47 (select(store(a_467, i3, e_470), i2) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[422])).
% 0.20/0.47 tff(424,assumption,(~(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2))), introduced(assumption)).
% 0.20/0.47 tff(425,plain,
% 0.20/0.47 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i2) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i2) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(426,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i0 = i2) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(427,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i0 = i2) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[426, 425])).
% 0.20/0.47 tff(428,plain,
% 0.20/0.47 ((i0 = i2) | (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[427, 74])).
% 0.20/0.47 tff(429,plain,
% 0.20/0.47 (i0 = i2),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[428, 424])).
% 0.20/0.47 tff(430,assumption,(i0 = i2), introduced(assumption)).
% 0.20/0.47 tff(431,assumption,(~(i0 = i3)), introduced(assumption)).
% 0.20/0.47 tff(432,plain,
% 0.20/0.47 ((i2 = i3) <=> (i3 = i2)),
% 0.20/0.47 inference(commutativity,[status(thm)],[])).
% 0.20/0.47 tff(433,plain,
% 0.20/0.47 ((i0 = i3) <=> (i2 = i3)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[430])).
% 0.20/0.47 tff(434,plain,
% 0.20/0.47 ((i0 = i3) <=> (i3 = i2)),
% 0.20/0.47 inference(transitivity,[status(thm)],[433, 432])).
% 0.20/0.47 tff(435,plain,
% 0.20/0.47 ((i3 = i2) <=> (i0 = i3)),
% 0.20/0.47 inference(symmetry,[status(thm)],[434])).
% 0.20/0.47 tff(436,plain,
% 0.20/0.47 (i0 = i3),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[248, 435])).
% 0.20/0.47 tff(437,plain,
% 0.20/0.47 ($false),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[431, 436])).
% 0.20/0.47 tff(438,plain,((~(i3 = i2)) | (i0 = i3) | (~(i0 = i2))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.47 tff(439,plain,
% 0.20/0.47 (~(i3 = i2)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[438, 431, 430])).
% 0.20/0.47 tff(440,plain,
% 0.20/0.47 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[352, 439])).
% 0.20/0.47 tff(441,plain,
% 0.20/0.47 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[78, 431])).
% 0.20/0.47 tff(442,plain,
% 0.20/0.47 ((i0 = sk(a_479, a_489)) <=> (i2 = sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[430])).
% 0.20/0.47 tff(443,plain,
% 0.20/0.47 ((i2 = sk(a_479, a_489)) <=> (i0 = sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[442])).
% 0.20/0.47 tff(444,assumption,(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3)), introduced(assumption)).
% 0.20/0.47 tff(445,plain,
% 0.20/0.47 (select(store(a_467, i3, e_470), i3) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3)),
% 0.20/0.47 inference(symmetry,[status(thm)],[444])).
% 0.20/0.47 tff(446,plain,
% 0.20/0.47 (select(a_467, i0) = e_486),
% 0.20/0.47 inference(transitivity,[status(thm)],[67, 66, 445, 211, 210, 209, 156])).
% 0.20/0.47 tff(447,plain,
% 0.20/0.47 (i2 = i0),
% 0.20/0.47 inference(symmetry,[status(thm)],[430])).
% 0.20/0.47 tff(448,plain,
% 0.20/0.47 (store(store(a_483, i2, e_484), i2, select(a_467, i0)) = store(a_485, i0, e_486)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[157, 447, 446])).
% 0.20/0.47 tff(449,plain,
% 0.20/0.47 (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[448])).
% 0.20/0.47 tff(450,plain,
% 0.20/0.47 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(451,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(452,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[451, 450])).
% 0.20/0.47 tff(453,plain,
% 0.20/0.47 (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[452, 74, 206])).
% 0.20/0.47 tff(454,plain,
% 0.20/0.47 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[453])).
% 0.20/0.47 tff(455,plain,
% 0.20/0.47 (select(a_467, i0) = e_484),
% 0.20/0.47 inference(transitivity,[status(thm)],[67, 66, 445, 211, 111])).
% 0.20/0.47 tff(456,plain,
% 0.20/0.47 (store(store(a_481, i3, e_482), i2, select(a_467, i0)) = store(a_483, i2, e_484)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[115, 455])).
% 0.20/0.47 tff(457,plain,
% 0.20/0.47 (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[456])).
% 0.20/0.47 tff(458,plain,
% 0.20/0.47 (select(a_481, i2) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[97, 447])).
% 0.20/0.47 tff(459,plain,
% 0.20/0.47 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0) = select(a_481, i2)),
% 0.20/0.47 inference(symmetry,[status(thm)],[458])).
% 0.20/0.47 tff(460,plain,
% 0.20/0.47 (select(a_467, i3) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.20/0.47 inference(symmetry,[status(thm)],[83])).
% 0.20/0.47 tff(461,plain,
% 0.20/0.47 (select(a_467, i3) = e_482),
% 0.20/0.47 inference(transitivity,[status(thm)],[460, 459, 247])).
% 0.20/0.47 tff(462,plain,
% 0.20/0.47 (store(store(a_480, i0, e_468), i3, select(a_467, i3)) = store(a_481, i3, e_482)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[99, 461])).
% 0.20/0.47 tff(463,plain,
% 0.20/0.47 (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[462])).
% 0.20/0.47 tff(464,assumption,(select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.47 tff(465,plain,
% 0.20/0.47 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(466,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(467,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[466, 465])).
% 0.20/0.47 tff(468,plain,
% 0.20/0.47 ((i2 = sk(a_479, a_489)) | (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[467, 74])).
% 0.20/0.47 tff(469,plain,
% 0.20/0.47 (select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[468, 206])).
% 0.20/0.47 tff(470,plain,
% 0.20/0.47 (store(a_485, i0, e_486) = store(store(a_483, i2, e_484), i2, select(a_467, i0))),
% 0.20/0.47 inference(symmetry,[status(thm)],[448])).
% 0.20/0.47 tff(471,plain,
% 0.20/0.47 (select(store(a_485, i0, e_486), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[470])).
% 0.20/0.47 tff(472,plain,
% 0.20/0.47 (select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[471])).
% 0.20/0.47 tff(473,assumption,(select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.47 tff(474,plain,
% 0.20/0.47 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[473])).
% 0.20/0.47 tff(475,plain,
% 0.20/0.47 (store(a_483, i2, e_484) = store(store(a_481, i3, e_482), i2, select(a_467, i0))),
% 0.20/0.47 inference(symmetry,[status(thm)],[456])).
% 0.20/0.47 tff(476,plain,
% 0.20/0.47 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[475])).
% 0.20/0.47 tff(477,plain,
% 0.20/0.47 (select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[476])).
% 0.20/0.47 tff(478,assumption,(i3 = sk(a_479, a_489)), introduced(assumption)).
% 0.20/0.47 tff(479,plain,
% 0.20/0.47 (sk(a_479, a_489) = i3),
% 0.20/0.47 inference(symmetry,[status(thm)],[478])).
% 0.20/0.47 tff(480,plain,
% 0.20/0.47 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3)),
% 0.20/0.47 inference(monotonicity,[status(thm)],[359, 479])).
% 0.20/0.47 tff(481,plain,
% 0.20/0.47 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.47 inference(symmetry,[status(thm)],[480])).
% 0.20/0.47 tff(482,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3) = select(a_481, i2))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(483,plain,
% 0.20/0.47 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3) = select(a_481, i2)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[482, 34])).
% 0.20/0.47 tff(484,plain,
% 0.20/0.47 (select(a_481, i2) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3)),
% 0.20/0.47 inference(symmetry,[status(thm)],[483])).
% 0.20/0.47 tff(485,plain,
% 0.20/0.47 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0) = select(a_467, i3))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(486,plain,
% 0.20/0.47 (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0) = select(a_467, i3)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[485, 34])).
% 0.20/0.47 tff(487,plain,
% 0.20/0.47 (store(a_467, i0, e_468) = store(store(a_466, i1, e_465), i0, select(a_467, i3))),
% 0.20/0.48 inference(symmetry,[status(thm)],[282])).
% 0.20/0.48 tff(488,plain,
% 0.20/0.48 (select(store(a_467, i0, e_468), i2) = select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[487, 447])).
% 0.20/0.48 tff(489,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i3) = select(a_471, i2))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(490,plain,
% 0.20/0.48 (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i3) = select(a_471, i2)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[489, 34])).
% 0.20/0.48 tff(491,plain,
% 0.20/0.48 (store(store(a_469, i3, e_470), i3, select(a_471, i2)) = store(a_471, i3, e_472)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[303, 299])).
% 0.20/0.48 tff(492,plain,
% 0.20/0.48 (store(a_471, i3, e_472) = store(store(a_469, i3, e_470), i3, select(a_471, i2))),
% 0.20/0.48 inference(symmetry,[status(thm)],[491])).
% 0.20/0.48 tff(493,plain,
% 0.20/0.48 (select(store(a_471, i3, e_472), sk(a_479, a_489)) = select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i3)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[492, 479])).
% 0.20/0.48 tff(494,assumption,(select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.48 tff(495,plain,
% 0.20/0.48 (store(a_473, i2, e_474) = store(store(a_471, i3, e_472), i2, select(a_467, i0))),
% 0.20/0.48 inference(symmetry,[status(thm)],[312])).
% 0.20/0.48 tff(496,plain,
% 0.20/0.48 (select(store(a_473, i2, e_474), sk(a_479, a_489)) = select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[495])).
% 0.20/0.48 tff(497,assumption,(select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.48 tff(498,plain,
% 0.20/0.48 (select(a_475, i0) = select(a_475, i2)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[430])).
% 0.20/0.48 tff(499,plain,
% 0.20/0.48 (select(a_475, i2) = select(a_475, i0)),
% 0.20/0.48 inference(symmetry,[status(thm)],[498])).
% 0.20/0.48 tff(500,plain,
% 0.20/0.48 (select(a_467, i0) = e_476),
% 0.20/0.48 inference(transitivity,[status(thm)],[56, 53, 37, 28, 499, 323])).
% 0.20/0.48 tff(501,plain,
% 0.20/0.48 (store(store(a_473, i2, e_474), i2, select(a_467, i0)) = store(a_475, i2, e_476)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[324, 500])).
% 0.20/0.48 tff(502,plain,
% 0.20/0.48 (store(a_475, i2, e_476) = store(store(a_473, i2, e_474), i2, select(a_467, i0))),
% 0.20/0.48 inference(symmetry,[status(thm)],[501])).
% 0.20/0.48 tff(503,plain,
% 0.20/0.48 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[502])).
% 0.20/0.48 tff(504,plain,
% 0.20/0.48 (select(a_479, i_490) = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[145, 137])).
% 0.20/0.48 tff(505,plain,
% 0.20/0.48 (e_491 = e_492),
% 0.20/0.48 inference(transitivity,[status(thm)],[133, 504, 464, 503, 497, 496, 494, 493, 490, 412, 414, 488, 486, 460, 459, 484, 481, 357, 477, 474, 472, 355, 205, 4])).
% 0.20/0.48 tff(506,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[185, 505])).
% 0.20/0.48 tff(507,plain,((~(i3 = sk(a_479, a_489))) | (~(select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489)))) | (~(select(store(store(a_473, i2, e_474), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))) | (~(select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489)))) | (~(select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2))) | (~(select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))) | (~(select(store(store(a_483, i2, e_484), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489)))) | (~(select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489)))) | (~(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))) | (~(i0 = i2))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.48 tff(508,plain,
% 0.20/0.48 (~(i3 = sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[507, 469, 464, 310, 414, 207, 453, 231, 444, 430])).
% 0.20/0.48 tff(509,plain,
% 0.20/0.48 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(510,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(511,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[510, 509])).
% 0.20/0.48 tff(512,plain,
% 0.20/0.48 ((i3 = sk(a_479, a_489)) | (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[511, 74])).
% 0.20/0.48 tff(513,plain,
% 0.20/0.48 (select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[512, 508])).
% 0.20/0.48 tff(514,plain,
% 0.20/0.48 (select(store(a_480, i0, e_468), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i3, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.48 inference(symmetry,[status(thm)],[513])).
% 0.20/0.48 tff(515,plain,
% 0.20/0.48 (store(store(a_467, i3, e_470), i2, select(a_467, i3)) = store(a_480, i0, e_468)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[91, 447, 87])).
% 0.20/0.48 tff(516,plain,
% 0.20/0.48 (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_480, i0, e_468), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[515])).
% 0.20/0.48 tff(517,plain,
% 0.20/0.48 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(518,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(519,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[518, 517])).
% 0.20/0.48 tff(520,plain,
% 0.20/0.48 (select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[519, 74, 206])).
% 0.20/0.48 tff(521,plain,
% 0.20/0.48 (select(store(a_467, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i3, e_470), i2, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.48 inference(symmetry,[status(thm)],[520])).
% 0.20/0.48 tff(522,plain,
% 0.20/0.48 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i3, e_470), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[63])).
% 0.20/0.48 tff(523,plain,
% 0.20/0.48 (select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[391, 74, 508])).
% 0.20/0.48 tff(524,plain,
% 0.20/0.48 (select(store(a_466, i1, e_465), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.48 inference(symmetry,[status(thm)],[523])).
% 0.20/0.48 tff(525,plain,
% 0.20/0.48 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(526,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(527,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = sk(a_479, a_489)) | (select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[526, 525])).
% 0.20/0.48 tff(528,plain,
% 0.20/0.48 (select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_466, i1, e_465), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[527, 74, 206])).
% 0.20/0.48 tff(529,plain,
% 0.20/0.48 (store(store(a_466, i1, e_465), i2, select(a_467, i3)) = store(a_467, i0, e_468)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[62, 447, 87])).
% 0.20/0.48 tff(530,plain,
% 0.20/0.48 (store(a_467, i0, e_468) = store(store(a_466, i1, e_465), i2, select(a_467, i3))),
% 0.20/0.48 inference(symmetry,[status(thm)],[529])).
% 0.20/0.48 tff(531,plain,
% 0.20/0.48 (select(store(a_467, i0, e_468), sk(a_479, a_489)) = select(store(store(a_466, i1, e_465), i2, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[530])).
% 0.20/0.48 tff(532,plain,
% 0.20/0.48 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_467, i0, e_468), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[403, 74, 508])).
% 0.20/0.48 tff(533,plain,
% 0.20/0.48 (select(store(a_469, i3, e_470), sk(a_479, a_489)) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[47])).
% 0.20/0.48 tff(534,plain,
% 0.20/0.48 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(535,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(536,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[535, 534])).
% 0.20/0.48 tff(537,plain,
% 0.20/0.48 ((i3 = sk(a_479, a_489)) | (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[536, 74])).
% 0.20/0.48 tff(538,plain,
% 0.20/0.48 (select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489)) = select(store(a_469, i3, e_470), sk(a_479, a_489))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[537, 508])).
% 0.20/0.48 tff(539,plain,
% 0.20/0.48 (select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0) = select(store(a_467, i0, e_468), i2)),
% 0.20/0.48 inference(symmetry,[status(thm)],[488])).
% 0.20/0.48 tff(540,plain,
% 0.20/0.48 (select(a_467, i3) = select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0)),
% 0.20/0.48 inference(symmetry,[status(thm)],[486])).
% 0.20/0.48 tff(541,plain,
% 0.20/0.48 (select(a_467, i3) = e_472),
% 0.20/0.48 inference(transitivity,[status(thm)],[540, 539, 415, 413, 299])).
% 0.20/0.48 tff(542,plain,
% 0.20/0.48 (store(store(a_469, i3, e_470), i3, select(a_467, i3)) = store(a_471, i3, e_472)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[303, 541])).
% 0.20/0.48 tff(543,plain,
% 0.20/0.48 (store(a_471, i3, e_472) = store(store(a_469, i3, e_470), i3, select(a_467, i3))),
% 0.20/0.48 inference(symmetry,[status(thm)],[542])).
% 0.20/0.48 tff(544,plain,
% 0.20/0.48 (select(store(a_471, i3, e_472), sk(a_479, a_489)) = select(store(store(a_469, i3, e_470), i3, select(a_467, i3)), sk(a_479, a_489))),
% 0.20/0.48 inference(monotonicity,[status(thm)],[543])).
% 0.20/0.48 tff(545,plain,
% 0.20/0.48 (e_491 = e_492),
% 0.20/0.48 inference(transitivity,[status(thm)],[133, 504, 464, 503, 469, 496, 310, 544, 538, 533, 532, 531, 528, 524, 522, 521, 516, 514, 463, 232, 457, 454, 449, 208, 177, 4])).
% 0.20/0.48 tff(546,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[185, 545])).
% 0.20/0.48 tff(547,plain,((i2 = sk(a_479, a_489)) | (~(select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489)))) | (~(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))) | (~(i0 = i2)) | (~(select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.48 tff(548,plain,
% 0.20/0.48 (i2 = sk(a_479, a_489)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[547, 332, 444, 430, 414])).
% 0.20/0.48 tff(549,plain,
% 0.20/0.48 (i0 = sk(a_479, a_489)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[548, 443])).
% 0.20/0.48 tff(550,plain,
% 0.20/0.48 ($false),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[241, 549])).
% 0.20/0.48 tff(551,plain,((i0 = sk(a_479, a_489)) | (~(i0 = i2)) | (~(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i3) = select(store(a_467, i3, e_470), i3))) | (~(select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.48 tff(552,plain,
% 0.20/0.48 (i0 = sk(a_479, a_489)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[551, 441, 430, 440])).
% 0.20/0.48 tff(553,plain,
% 0.20/0.48 (sk(a_479, a_489) = i0),
% 0.20/0.48 inference(symmetry,[status(thm)],[552])).
% 0.20/0.48 tff(554,plain,
% 0.20/0.48 (sk(a_479, a_489) = i2),
% 0.20/0.48 inference(transitivity,[status(thm)],[553, 430])).
% 0.20/0.48 tff(555,plain,
% 0.20/0.48 (store(a_475, i2, e_476) = store(store(a_473, i2, e_474), i2, select(a_475, i0))),
% 0.20/0.48 inference(symmetry,[status(thm)],[325])).
% 0.20/0.48 tff(556,plain,
% 0.20/0.48 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2)),
% 0.20/0.48 inference(monotonicity,[status(thm)],[555, 554])).
% 0.20/0.48 tff(557,plain,
% 0.20/0.48 (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2) = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.48 inference(symmetry,[status(thm)],[556])).
% 0.20/0.48 tff(558,plain,
% 0.20/0.48 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2) = select(a_475, i0))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(559,plain,
% 0.20/0.49 (select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2) = select(a_475, i0)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[558, 34])).
% 0.20/0.49 tff(560,plain,
% 0.20/0.49 (select(a_475, i0) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[559])).
% 0.20/0.49 tff(561,plain,
% 0.20/0.49 (select(a_485, i0) = select(a_485, i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[430])).
% 0.20/0.49 tff(562,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2) = select(a_485, i0))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(563,plain,
% 0.20/0.49 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2) = select(a_485, i0)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[562, 34])).
% 0.20/0.49 tff(564,plain,
% 0.20/0.49 (i_490 = i2),
% 0.20/0.49 inference(transitivity,[status(thm)],[137, 553, 430])).
% 0.20/0.49 tff(565,plain,
% 0.20/0.49 (select(a_489, i_490) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[203, 564])).
% 0.20/0.49 tff(566,plain,
% 0.20/0.49 (e_492 = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.49 inference(transitivity,[status(thm)],[3, 565, 563, 561, 122, 107, 105, 441, 65, 58, 56, 53, 37, 28, 499, 560, 557])).
% 0.20/0.49 tff(567,plain,
% 0.20/0.49 (e_491 = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489))),
% 0.20/0.49 inference(transitivity,[status(thm)],[133, 335])).
% 0.20/0.49 tff(568,plain,
% 0.20/0.49 ((e_491 = e_492) <=> (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489)))),
% 0.20/0.49 inference(monotonicity,[status(thm)],[567, 566])).
% 0.20/0.49 tff(569,plain,
% 0.20/0.49 ((select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))) <=> (e_491 = e_492)),
% 0.20/0.49 inference(symmetry,[status(thm)],[568])).
% 0.20/0.49 tff(570,plain,
% 0.20/0.49 (i_490 = i0),
% 0.20/0.49 inference(transitivity,[status(thm)],[137, 553])).
% 0.20/0.49 tff(571,plain,
% 0.20/0.49 (select(a_479, i_490) = select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[145, 570])).
% 0.20/0.49 tff(572,plain,
% 0.20/0.49 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.49 inference(transitivity,[status(thm)],[334, 571, 149, 499, 560, 557])).
% 0.20/0.49 tff(573,plain,
% 0.20/0.49 (e_491 = e_492),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[572, 569])).
% 0.20/0.49 tff(574,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[185, 573])).
% 0.20/0.49 tff(575,plain,((i0 = i3) | (~(i0 = i2))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(576,plain,
% 0.20/0.49 (i0 = i3),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[575, 429])).
% 0.20/0.49 tff(577,plain,
% 0.20/0.49 (i2 = i0),
% 0.20/0.49 inference(symmetry,[status(thm)],[429])).
% 0.20/0.49 tff(578,plain,
% 0.20/0.49 (i2 = i3),
% 0.20/0.49 inference(transitivity,[status(thm)],[577, 576])).
% 0.20/0.49 tff(579,plain,
% 0.20/0.49 (select(store(a_467, i3, e_470), i2) = select(store(a_467, i3, e_470), i3)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[578])).
% 0.20/0.49 tff(580,plain,
% 0.20/0.49 (select(store(a_467, i3, e_470), i3) = select(store(a_467, i3, e_470), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[579])).
% 0.20/0.49 tff(581,plain,
% 0.20/0.49 (i3 = i0),
% 0.20/0.49 inference(symmetry,[status(thm)],[576])).
% 0.20/0.49 tff(582,plain,
% 0.20/0.49 (select(a_467, i3) = select(a_467, i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[581])).
% 0.20/0.49 tff(583,plain,
% 0.20/0.49 (select(a_481, i2) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[97, 577])).
% 0.20/0.49 tff(584,plain,
% 0.20/0.49 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(a_481, i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[100])).
% 0.20/0.49 tff(585,plain,
% 0.20/0.49 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2)),
% 0.20/0.49 inference(transitivity,[status(thm)],[584, 583, 83, 582, 67, 66, 580])).
% 0.20/0.49 tff(586,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[424, 585])).
% 0.20/0.49 tff(587,plain,(select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2) = select(store(a_467, i3, e_470), i2)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(588,plain,
% 0.20/0.49 (select(a_481, i2) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[584])).
% 0.20/0.49 tff(589,plain,
% 0.20/0.49 (select(a_481, i2) = e_472),
% 0.20/0.49 inference(transitivity,[status(thm)],[588, 587, 423, 421, 420, 418, 415, 413, 299])).
% 0.20/0.49 tff(590,plain,
% 0.20/0.49 (store(store(a_469, i3, e_470), i3, select(a_481, i2)) = store(a_471, i3, e_472)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[303, 589])).
% 0.20/0.49 tff(591,plain,
% 0.20/0.49 (select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489))),
% 0.20/0.49 inference(monotonicity,[status(thm)],[590])).
% 0.20/0.49 tff(592,plain,
% 0.20/0.49 (select(store(a_471, i3, e_472), sk(a_479, a_489)) = select(store(store(a_469, i3, e_470), i3, select(a_481, i2)), sk(a_479, a_489))),
% 0.20/0.49 inference(symmetry,[status(thm)],[591])).
% 0.20/0.49 tff(593,assumption,(select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))), introduced(assumption)).
% 0.20/0.49 tff(594,plain,
% 0.20/0.49 (e_491 = e_492),
% 0.20/0.49 inference(transitivity,[status(thm)],[133, 335, 332, 327, 593, 314, 494, 592, 411, 406, 404, 400, 397, 393, 388, 386, 381, 368, 361, 357, 227, 243, 217, 355, 205, 4])).
% 0.20/0.49 tff(595,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[185, 594])).
% 0.20/0.49 tff(596,plain,((i3 = sk(a_479, a_489)) | (~(select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), sk(a_479, a_489)) = select(store(a_485, i0, e_486), sk(a_479, a_489)))) | (~(select(store(store(a_481, i3, e_482), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_481, i3, e_482), sk(a_479, a_489)))) | (~(select(store(store(a_471, i3, e_472), i2, select(a_467, i0)), sk(a_479, a_489)) = select(store(a_471, i3, e_472), sk(a_479, a_489)))) | (~(select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489)))) | (~(select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i2) = select(store(a_467, i0, e_468), i2))) | (~(select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2) = select(store(a_466, i1, e_465), i2))) | (~(select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2) = select(store(a_466, i1, e_465), i2))) | (~(select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0))) | (~(select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0) = select(store(a_481, i3, e_482), i0))) | (i0 = sk(a_479, a_489))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(597,plain,
% 0.20/0.49 (i3 = sk(a_479, a_489)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[596, 207, 231, 310, 319, 353, 348, 344, 240, 239, 195])).
% 0.20/0.49 tff(598,plain,
% 0.20/0.49 (sk(a_479, a_489) = i3),
% 0.20/0.49 inference(symmetry,[status(thm)],[597])).
% 0.20/0.49 tff(599,plain,
% 0.20/0.49 (select(store(a_481, i3, e_482), sk(a_479, a_489)) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[359, 598])).
% 0.20/0.49 tff(600,plain,
% 0.20/0.49 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3) = select(store(a_481, i3, e_482), sk(a_479, a_489))),
% 0.20/0.49 inference(symmetry,[status(thm)],[599])).
% 0.20/0.49 tff(601,plain,
% 0.20/0.49 (select(store(a_467, i3, e_470), i2) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[587])).
% 0.20/0.49 tff(602,plain,
% 0.20/0.49 (select(store(a_466, i1, e_465), i2) = select(store(store(a_466, i1, e_465), i3, select(a_467, i0)), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[344])).
% 0.20/0.49 tff(603,plain,
% 0.20/0.49 (select(a_485, i0) = e_468),
% 0.20/0.49 inference(transitivity,[status(thm)],[376, 239, 372, 240, 370, 83, 87])).
% 0.20/0.49 tff(604,plain,
% 0.20/0.49 (store(store(a_466, i1, e_465), i0, select(a_485, i0)) = store(a_467, i0, e_468)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[62, 603])).
% 0.20/0.49 tff(605,plain,
% 0.20/0.49 (store(a_467, i0, e_468) = store(store(a_466, i1, e_465), i0, select(a_485, i0))),
% 0.20/0.49 inference(symmetry,[status(thm)],[604])).
% 0.20/0.49 tff(606,plain,
% 0.20/0.49 (select(store(a_467, i0, e_468), i2) = select(store(store(a_466, i1, e_465), i0, select(a_485, i0)), i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[605])).
% 0.20/0.49 tff(607,plain,
% 0.20/0.49 (select(store(a_471, i3, e_472), sk(a_479, a_489)) = select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i3)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[492, 598])).
% 0.20/0.49 tff(608,plain,
% 0.20/0.49 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), sk(a_479, a_489))),
% 0.20/0.49 inference(monotonicity,[status(thm)],[555])).
% 0.20/0.49 tff(609,plain,
% 0.20/0.49 (select(store(store(a_475, i2, e_476), i0, select(a_475, i2)), sk(a_479, a_489)) = select(store(a_475, i2, e_476), sk(a_479, a_489))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[331, 195])).
% 0.20/0.49 tff(610,plain,
% 0.20/0.49 (e_491 = e_492),
% 0.20/0.49 inference(transitivity,[status(thm)],[133, 504, 609, 608, 319, 496, 310, 607, 490, 412, 353, 606, 348, 602, 422, 601, 584, 484, 600, 232, 227, 222, 217, 208, 205, 4])).
% 0.20/0.49 tff(611,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[185, 610])).
% 0.20/0.49 tff(612,plain,((i2 = sk(a_479, a_489)) | (~(select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0) = select(store(a_480, i0, e_468), i0))) | (i0 = i2)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(613,plain,
% 0.20/0.49 (i2 = sk(a_479, a_489)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[612, 201, 123])).
% 0.20/0.49 tff(614,plain,
% 0.20/0.49 (sk(a_479, a_489) = i2),
% 0.20/0.49 inference(symmetry,[status(thm)],[613])).
% 0.20/0.49 tff(615,plain,
% 0.20/0.49 (i_490 = i2),
% 0.20/0.49 inference(transitivity,[status(thm)],[137, 614])).
% 0.20/0.49 tff(616,plain,
% 0.20/0.49 (select(a_489, i_490) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[203, 615])).
% 0.20/0.49 tff(617,plain,
% 0.20/0.49 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2) = select(a_489, i_490)),
% 0.20/0.49 inference(symmetry,[status(thm)],[616])).
% 0.20/0.49 tff(618,plain,
% 0.20/0.49 (select(a_485, i0) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2)),
% 0.20/0.49 inference(symmetry,[status(thm)],[563])).
% 0.20/0.49 tff(619,plain,
% 0.20/0.49 (select(store(a_481, i3, e_482), i0) = select(store(store(a_481, i3, e_482), i2, select(a_481, i3)), i0)),
% 0.20/0.49 inference(symmetry,[status(thm)],[239])).
% 0.20/0.49 tff(620,plain,
% 0.20/0.49 (select(store(a_480, i0, e_468), i0) = select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i0)),
% 0.20/0.49 inference(symmetry,[status(thm)],[201])).
% 0.20/0.49 tff(621,plain,
% 0.20/0.49 (select(store(a_467, i0, e_468), i0) = select(store(store(a_466, i1, e_465), i0, select(a_467, i3)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[487])).
% 0.20/0.49 tff(622,plain,
% 0.20/0.49 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0) = select(store(a_467, i0, e_468), i0)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0) = select(store(a_467, i0, e_468), i0)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(623,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0) = select(store(a_467, i0, e_468), i0)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(624,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0) = select(store(a_467, i0, e_468), i0))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[623, 622])).
% 0.20/0.49 tff(625,plain,
% 0.20/0.49 (select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0) = select(store(a_467, i0, e_468), i0)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[624, 74, 196])).
% 0.20/0.49 tff(626,plain,
% 0.20/0.49 (select(store(a_469, i3, e_470), i0) = select(store(store(a_467, i0, e_468), i3, select(a_467, i0)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[47])).
% 0.20/0.49 tff(627,plain,
% 0.20/0.49 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(628,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i3 = i0) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(629,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i3 = i0) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[628, 627])).
% 0.20/0.49 tff(630,plain,
% 0.20/0.49 ((i3 = i0) | (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[629, 74])).
% 0.20/0.49 tff(631,plain,
% 0.20/0.49 (select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0) = select(store(a_469, i3, e_470), i0)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[630, 196])).
% 0.20/0.49 tff(632,plain,
% 0.20/0.49 (select(store(a_471, i3, e_472), i0) = select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[492])).
% 0.20/0.49 tff(633,plain,
% 0.20/0.49 (((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = i0) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0)))) <=> ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = i0) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(634,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | ((i2 = i0) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(635,plain,
% 0.20/0.49 ((~![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))) | (i2 = i0) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[634, 633])).
% 0.20/0.49 tff(636,plain,
% 0.20/0.49 ((i2 = i0) | (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[635, 74])).
% 0.20/0.49 tff(637,plain,
% 0.20/0.49 (select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0) = select(store(a_471, i3, e_472), i0)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[636, 234])).
% 0.20/0.49 tff(638,plain,
% 0.20/0.49 (select(a_475, i0) = select(store(store(a_471, i3, e_472), i2, select(a_471, i3)), i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[26])).
% 0.20/0.49 tff(639,plain,
% 0.20/0.49 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[555, 614])).
% 0.20/0.49 tff(640,plain,
% 0.20/0.49 (e_491 = e_492),
% 0.20/0.49 inference(transitivity,[status(thm)],[133, 504, 609, 639, 559, 638, 637, 632, 631, 626, 625, 621, 486, 460, 369, 620, 371, 619, 375, 618, 617, 4])).
% 0.20/0.49 tff(641,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[185, 640])).
% 0.20/0.49 tff(642,plain,((i3 = i0) | (i0 = i2)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(643,plain,
% 0.20/0.49 (i3 = i0),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[642, 123])).
% 0.20/0.49 tff(644,plain,
% 0.20/0.49 (e_474 = select(a_467, i0)),
% 0.20/0.49 inference(transitivity,[status(thm)],[15, 52, 55])).
% 0.20/0.49 tff(645,assumption,(i3 = i0), introduced(assumption)).
% 0.20/0.49 tff(646,plain,
% 0.20/0.49 (select(a_467, i3) = select(a_467, i0)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[645])).
% 0.20/0.49 tff(647,plain,
% 0.20/0.49 (select(a_467, i0) = select(a_467, i3)),
% 0.20/0.49 inference(symmetry,[status(thm)],[646])).
% 0.20/0.49 tff(648,plain,
% 0.20/0.49 (e_470 = e_468),
% 0.20/0.49 inference(transitivity,[status(thm)],[40, 647, 87])).
% 0.20/0.50 tff(649,plain,
% 0.20/0.50 (e_468 = e_470),
% 0.20/0.50 inference(transitivity,[status(thm)],[86, 646, 41])).
% 0.20/0.50 tff(650,plain,
% 0.20/0.50 (i0 = i3),
% 0.20/0.50 inference(symmetry,[status(thm)],[645])).
% 0.20/0.50 tff(651,plain,
% 0.20/0.50 (store(a_467, i0, e_468) = store(a_467, i3, e_470)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[650, 649])).
% 0.20/0.50 tff(652,plain,
% 0.20/0.50 (a_469 = a_480),
% 0.20/0.50 inference(transitivity,[status(thm)],[44, 651, 91])).
% 0.20/0.50 tff(653,plain,
% 0.20/0.50 (store(a_469, i3, e_470) = store(a_480, i0, e_468)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[652, 645, 648])).
% 0.20/0.50 tff(654,plain,
% 0.20/0.50 (a_471 = a_481),
% 0.20/0.50 inference(transitivity,[status(thm)],[50, 653, 99])).
% 0.20/0.50 tff(655,plain,
% 0.20/0.50 (select(a_471, i2) = select(a_481, i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[654])).
% 0.20/0.50 tff(656,plain,
% 0.20/0.50 (e_472 = e_482),
% 0.20/0.50 inference(transitivity,[status(thm)],[298, 655, 247])).
% 0.20/0.50 tff(657,plain,
% 0.20/0.50 (store(a_471, i3, e_472) = store(a_481, i3, e_482)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[654, 656])).
% 0.20/0.50 tff(658,plain,
% 0.20/0.50 (a_473 = store(a_481, i3, e_482)),
% 0.20/0.50 inference(transitivity,[status(thm)],[19, 657])).
% 0.20/0.50 tff(659,plain,
% 0.20/0.50 (store(a_473, i2, e_474) = store(store(a_481, i3, e_482), i2, select(a_467, i0))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[658, 644])).
% 0.20/0.50 tff(660,plain,
% 0.20/0.50 (store(store(a_481, i3, e_482), i2, select(a_467, i0)) = store(a_473, i2, e_474)),
% 0.20/0.50 inference(symmetry,[status(thm)],[659])).
% 0.20/0.50 tff(661,plain,
% 0.20/0.50 (store(a_483, i2, e_484) = store(a_473, i2, e_474)),
% 0.20/0.50 inference(transitivity,[status(thm)],[225, 660])).
% 0.20/0.50 tff(662,plain,
% 0.20/0.50 (select(store(a_483, i2, e_484), sk(a_479, a_489)) = select(store(a_473, i2, e_474), sk(a_479, a_489))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[661])).
% 0.20/0.50 tff(663,plain,
% 0.20/0.50 (select(store(a_473, i2, e_474), sk(a_479, a_489)) = select(store(a_483, i2, e_484), sk(a_479, a_489))),
% 0.20/0.50 inference(symmetry,[status(thm)],[662])).
% 0.20/0.50 tff(664,plain,
% 0.20/0.50 (e_491 = e_492),
% 0.20/0.50 inference(transitivity,[status(thm)],[133, 335, 332, 327, 319, 663, 243, 217, 208, 205, 4])).
% 0.20/0.50 tff(665,plain,
% 0.20/0.50 ($false),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[185, 664])).
% 0.20/0.50 tff(666,plain,((i2 = sk(a_479, a_489)) | (~(i3 = i0)) | (i0 = sk(a_479, a_489))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.50 tff(667,plain,
% 0.20/0.50 (i2 = sk(a_479, a_489)),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[666, 643, 195])).
% 0.20/0.50 tff(668,plain,
% 0.20/0.50 (sk(a_479, a_489) = i2),
% 0.20/0.50 inference(symmetry,[status(thm)],[667])).
% 0.20/0.50 tff(669,plain,
% 0.20/0.50 (i_490 = i2),
% 0.20/0.50 inference(transitivity,[status(thm)],[137, 668])).
% 0.20/0.50 tff(670,plain,
% 0.20/0.50 (select(a_489, i_490) = select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[203, 669])).
% 0.20/0.50 tff(671,plain,
% 0.20/0.50 (select(store(store(a_485, i0, e_486), i2, select(a_485, i0)), i2) = select(a_489, i_490)),
% 0.20/0.50 inference(symmetry,[status(thm)],[670])).
% 0.20/0.50 tff(672,plain,
% 0.20/0.50 (select(store(store(a_480, i0, e_468), i3, select(a_481, i2)), i3) = select(store(a_481, i3, e_482), i0)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[358, 643])).
% 0.20/0.50 tff(673,plain,
% 0.20/0.50 (select(a_467, i3) = select(a_467, i0)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[643])).
% 0.20/0.50 tff(674,plain,
% 0.20/0.50 (select(a_467, i0) = select(a_467, i3)),
% 0.20/0.50 inference(symmetry,[status(thm)],[673])).
% 0.20/0.50 tff(675,plain,
% 0.20/0.50 (e_470 = e_468),
% 0.20/0.50 inference(transitivity,[status(thm)],[40, 674, 87])).
% 0.20/0.50 tff(676,plain,
% 0.20/0.50 (e_468 = e_470),
% 0.20/0.50 inference(transitivity,[status(thm)],[86, 673, 41])).
% 0.20/0.50 tff(677,plain,
% 0.20/0.50 (i0 = i3),
% 0.20/0.50 inference(symmetry,[status(thm)],[643])).
% 0.20/0.50 tff(678,plain,
% 0.20/0.50 (store(a_467, i0, e_468) = store(a_467, i3, e_470)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[677, 676])).
% 0.20/0.50 tff(679,plain,
% 0.20/0.50 (a_469 = a_480),
% 0.20/0.50 inference(transitivity,[status(thm)],[44, 678, 91])).
% 0.20/0.50 tff(680,plain,
% 0.20/0.50 (store(a_469, i3, e_470) = store(a_480, i0, e_468)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[679, 643, 675])).
% 0.20/0.50 tff(681,plain,
% 0.20/0.50 (a_471 = a_481),
% 0.20/0.50 inference(transitivity,[status(thm)],[50, 680, 99])).
% 0.20/0.50 tff(682,plain,
% 0.20/0.50 (select(a_471, i2) = select(a_481, i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[681])).
% 0.20/0.50 tff(683,plain,
% 0.20/0.50 (select(store(a_471, i3, e_472), i0) = select(store(store(a_469, i3, e_470), i3, select(a_471, i2)), i3)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[492, 677])).
% 0.20/0.50 tff(684,plain,
% 0.20/0.50 (select(store(a_475, i2, e_476), sk(a_479, a_489)) = select(store(store(a_473, i2, e_474), i2, select(a_475, i0)), i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[555, 668])).
% 0.20/0.50 tff(685,plain,
% 0.20/0.50 (e_491 = e_492),
% 0.20/0.50 inference(transitivity,[status(thm)],[133, 504, 609, 684, 559, 638, 637, 683, 490, 682, 484, 672, 619, 375, 618, 671, 4])).
% 0.20/0.50 tff(686,plain,
% 0.20/0.50 ($false),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[185, 685])).
% 0.20/0.50 tff(687,plain,(i0 = i2), inference(lemma,lemma(discharge,[]))).
% 0.20/0.50 tff(688,plain,
% 0.20/0.50 (select(a_485, i0) = select(a_485, i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[687])).
% 0.20/0.50 tff(689,plain,
% 0.20/0.50 (e_488 = e_478),
% 0.20/0.50 inference(transitivity,[status(thm)],[169, 688, 122, 107, 105, 104, 65, 58, 56, 53, 37, 28, 12])).
% 0.20/0.50 tff(690,plain,
% 0.20/0.50 (i2 = i0),
% 0.20/0.50 inference(symmetry,[status(thm)],[687])).
% 0.20/0.50 tff(691,plain,
% 0.20/0.50 (select(a_475, i0) = select(a_475, i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[687])).
% 0.20/0.50 tff(692,plain,
% 0.20/0.50 (e_476 = select(a_467, i0)),
% 0.20/0.50 inference(transitivity,[status(thm)],[322, 691, 27, 36, 52, 55])).
% 0.20/0.50 tff(693,plain,
% 0.20/0.50 (store(a_475, i2, e_476) = store(store(a_473, i2, e_474), i2, select(a_467, i0))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[25, 692])).
% 0.20/0.50 tff(694,plain,
% 0.20/0.50 (store(store(a_473, i2, e_474), i2, select(a_467, i0)) = store(a_475, i2, e_476)),
% 0.20/0.50 inference(symmetry,[status(thm)],[693])).
% 0.20/0.50 tff(695,plain,
% 0.20/0.50 (select(a_481, i2) = select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[97, 690])).
% 0.20/0.50 tff(696,plain,
% 0.20/0.50 (select(store(store(a_467, i3, e_470), i0, select(a_467, i3)), i0) = select(a_481, i2)),
% 0.20/0.50 inference(symmetry,[status(thm)],[695])).
% 0.20/0.50 tff(697,plain,
% 0.20/0.50 ((i3 = i0) <=> (i0 = i3)),
% 0.20/0.50 inference(commutativity,[status(thm)],[])).
% 0.20/0.50 tff(698,plain,
% 0.20/0.50 ((i3 = i2) <=> (i3 = i0)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[690])).
% 0.20/0.50 tff(699,plain,
% 0.20/0.50 ((i3 = i2) <=> (i0 = i3)),
% 0.20/0.50 inference(transitivity,[status(thm)],[698, 697])).
% 0.20/0.50 tff(700,plain,
% 0.20/0.50 ((i0 = i3) <=> (i3 = i2)),
% 0.20/0.50 inference(symmetry,[status(thm)],[699])).
% 0.20/0.50 tff(701,plain,
% 0.20/0.50 (i0 = i3),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[575, 687])).
% 0.20/0.50 tff(702,plain,
% 0.20/0.50 (i3 = i2),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[701, 700])).
% 0.20/0.50 tff(703,plain,
% 0.20/0.50 (select(a_467, i3) = select(store(a_466, i1, e_465), i2)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[61, 702])).
% 0.20/0.50 tff(704,plain,
% 0.20/0.50 (select(store(a_466, i1, e_465), i2) = select(a_467, i3)),
% 0.20/0.50 inference(symmetry,[status(thm)],[703])).
% 0.20/0.50 tff(705,plain,
% 0.20/0.50 (select(store(a_466, i1, e_465), i2) = select(a_467, i0)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[62, 690])).
% 0.20/0.50 tff(706,plain,
% 0.20/0.50 (select(a_467, i0) = select(store(a_466, i1, e_465), i2)),
% 0.20/0.50 inference(symmetry,[status(thm)],[705])).
% 0.20/0.50 tff(707,plain,
% 0.20/0.50 (i2 = i3),
% 0.20/0.50 inference(symmetry,[status(thm)],[702])).
% 0.20/0.50 tff(708,plain,
% 0.20/0.50 (select(a_471, i2) = select(a_471, i3)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[707])).
% 0.20/0.50 tff(709,plain,
% 0.20/0.50 (e_472 = e_482),
% 0.20/0.50 inference(transitivity,[status(thm)],[298, 708, 52, 55, 706, 704, 460, 696, 247])).
% 0.20/0.50 tff(710,plain,
% 0.20/0.50 (e_470 = e_468),
% 0.20/0.50 inference(transitivity,[status(thm)],[40, 706, 704, 87])).
% 0.20/0.50 tff(711,plain,
% 0.20/0.50 (i3 = i0),
% 0.20/0.50 inference(transitivity,[status(thm)],[702, 690])).
% 0.20/0.50 tff(712,plain,
% 0.20/0.50 (select(a_485, i0) = e_470),
% 0.20/0.50 inference(transitivity,[status(thm)],[688, 122, 107, 105, 104, 65, 58, 41])).
% 0.20/0.50 tff(713,plain,
% 0.20/0.50 (i0 = i3),
% 0.20/0.50 inference(transitivity,[status(thm)],[687, 707])).
% 0.20/0.50 tff(714,plain,
% 0.20/0.50 (store(store(a_466, i1, e_465), i0, select(a_485, i0)) = store(a_467, i3, e_470)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[62, 713, 712])).
% 0.20/0.50 tff(715,plain,
% 0.20/0.50 (select(a_485, i2) = select(a_485, i0)),
% 0.20/0.50 inference(symmetry,[status(thm)],[688])).
% 0.20/0.50 tff(716,plain,
% 0.20/0.50 (e_468 = select(a_485, i0)),
% 0.20/0.50 inference(transitivity,[status(thm)],[86, 703, 705, 67, 66, 212, 211, 210, 209, 715])).
% 0.20/0.50 tff(717,plain,
% 0.20/0.50 (store(a_467, i0, e_468) = store(store(a_466, i1, e_465), i0, select(a_485, i0))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[61, 716])).
% 0.20/0.50 tff(718,plain,
% 0.20/0.50 (a_469 = a_480),
% 0.20/0.50 inference(transitivity,[status(thm)],[44, 717, 714, 91])).
% 0.20/0.50 tff(719,plain,
% 0.20/0.50 (store(a_469, i3, e_470) = store(a_480, i0, e_468)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[718, 711, 710])).
% 0.20/0.50 tff(720,plain,
% 0.20/0.50 (a_471 = a_481),
% 0.20/0.50 inference(transitivity,[status(thm)],[50, 719, 99])).
% 0.20/0.50 tff(721,plain,
% 0.20/0.50 (store(a_471, i3, e_472) = store(a_481, i3, e_482)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[720, 709])).
% 0.20/0.50 tff(722,plain,
% 0.20/0.50 (a_473 = store(a_481, i3, e_482)),
% 0.20/0.50 inference(transitivity,[status(thm)],[19, 721])).
% 0.20/0.50 tff(723,plain,
% 0.20/0.50 (store(a_473, i2, e_474) = store(store(a_481, i3, e_482), i2, select(a_467, i0))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[722, 644])).
% 0.20/0.50 tff(724,plain,
% 0.20/0.50 (store(a_473, i2, e_474) = store(a_483, i2, e_484)),
% 0.20/0.50 inference(transitivity,[status(thm)],[723, 224])).
% 0.20/0.50 tff(725,plain,
% 0.20/0.50 (store(store(a_473, i2, e_474), i2, select(a_467, i0)) = store(store(a_483, i2, e_484), i2, select(a_467, i0))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[724])).
% 0.20/0.50 tff(726,plain,
% 0.20/0.50 (store(store(a_483, i2, e_484), i2, select(a_467, i0)) = store(store(a_473, i2, e_474), i2, select(a_467, i0))),
% 0.20/0.50 inference(symmetry,[status(thm)],[725])).
% 0.20/0.50 tff(727,plain,
% 0.20/0.50 (store(store(a_483, i2, e_484), i2, select(a_467, i0)) = store(a_485, i0, e_486)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[157, 690, 213])).
% 0.20/0.50 tff(728,plain,
% 0.20/0.50 (store(a_485, i0, e_486) = store(store(a_483, i2, e_484), i2, select(a_467, i0))),
% 0.20/0.50 inference(symmetry,[status(thm)],[727])).
% 0.20/0.50 tff(729,plain,
% 0.20/0.50 (a_487 = a_477),
% 0.20/0.50 inference(transitivity,[status(thm)],[173, 728, 726, 694, 142])).
% 0.20/0.50 tff(730,plain,
% 0.20/0.50 (store(a_487, i2, e_488) = store(a_477, i0, e_478)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[729, 690, 689])).
% 0.20/0.50 tff(731,plain,
% 0.20/0.50 (a_489 = a_479),
% 0.20/0.50 inference(transitivity,[status(thm)],[165, 730, 8])).
% 0.20/0.50 tff(732,plain,
% 0.20/0.50 (select(a_489, i_490) = select(a_479, i_490)),
% 0.20/0.50 inference(monotonicity,[status(thm)],[731])).
% 0.20/0.50 tff(733,plain,
% 0.20/0.50 (select(a_479, i_490) = select(a_489, i_490)),
% 0.20/0.50 inference(symmetry,[status(thm)],[732])).
% 0.20/0.50 tff(734,plain,
% 0.20/0.50 (e_491 = e_492),
% 0.20/0.50 inference(transitivity,[status(thm)],[133, 733, 4])).
% 0.20/0.50 tff(735,plain,
% 0.20/0.50 ($false),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[185, 734])).
% 0.20/0.50 % SZS output end Proof
% 0.20/0.50 % E exiting
%------------------------------------------------------------------------------