%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV540-1.004 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:34:27 AM UTC 2025
% Result : Unsatisfiable 0.12s 0.38s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV540-1.004 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 10:13:33 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.38 % SZS status Unsatisfiable
% 0.12/0.38 % SZS output start Proof
% 0.12/0.38 tff(a_440_type, type, (
% 0.12/0.38 a_440: $i)).
% 0.12/0.38 tff(a_430_type, type, (
% 0.12/0.38 a_430: $i)).
% 0.12/0.38 tff(store_type, type, (
% 0.12/0.38 store: ( $i * $i * $i ) > $i)).
% 0.12/0.38 tff(e_439_type, type, (
% 0.12/0.38 e_439: $i)).
% 0.12/0.38 tff(i2_type, type, (
% 0.12/0.38 i2: $i)).
% 0.12/0.38 tff(a_438_type, type, (
% 0.12/0.38 a_438: $i)).
% 0.12/0.38 tff(select_type, type, (
% 0.12/0.38 select: ( $i * $i ) > $i)).
% 0.12/0.38 tff(i0_type, type, (
% 0.12/0.38 i0: $i)).
% 0.12/0.38 tff(a_426_type, type, (
% 0.12/0.38 a_426: $i)).
% 0.12/0.38 tff(e_425_type, type, (
% 0.12/0.38 e_425: $i)).
% 0.12/0.38 tff(a_424_type, type, (
% 0.12/0.38 a_424: $i)).
% 0.12/0.38 tff(a_436_type, type, (
% 0.12/0.38 a_436: $i)).
% 0.12/0.38 tff(e_435_type, type, (
% 0.12/0.38 e_435: $i)).
% 0.12/0.38 tff(a_434_type, type, (
% 0.12/0.38 a_434: $i)).
% 0.12/0.38 tff(i3_type, type, (
% 0.12/0.38 i3: $i)).
% 0.12/0.38 tff(a_422_type, type, (
% 0.12/0.38 a_422: $i)).
% 0.12/0.38 tff(a_418_type, type, (
% 0.12/0.38 a_418: $i)).
% 0.12/0.38 tff(e_419_type, type, (
% 0.12/0.38 e_419: $i)).
% 0.12/0.38 tff(e_421_type, type, (
% 0.12/0.38 e_421: $i)).
% 0.12/0.38 tff(a_420_type, type, (
% 0.12/0.38 a_420: $i)).
% 0.12/0.38 tff(e_416_type, type, (
% 0.12/0.38 e_416: $i)).
% 0.12/0.38 tff(i1_type, type, (
% 0.12/0.38 i1: $i)).
% 0.12/0.38 tff(a1_type, type, (
% 0.12/0.38 a1: $i)).
% 0.12/0.38 tff(a_417_type, type, (
% 0.12/0.38 a_417: $i)).
% 0.12/0.38 tff(a_432_type, type, (
% 0.12/0.38 a_432: $i)).
% 0.12/0.38 tff(a_431_type, type, (
% 0.12/0.38 a_431: $i)).
% 0.12/0.38 tff(e_423_type, type, (
% 0.12/0.38 e_423: $i)).
% 0.12/0.38 tff(e_433_type, type, (
% 0.12/0.38 e_433: $i)).
% 0.12/0.38 tff(e_437_type, type, (
% 0.12/0.38 e_437: $i)).
% 0.12/0.38 tff(e_429_type, type, (
% 0.12/0.38 e_429: $i)).
% 0.12/0.38 tff(a_428_type, type, (
% 0.12/0.38 a_428: $i)).
% 0.12/0.38 tff(e_427_type, type, (
% 0.12/0.38 e_427: $i)).
% 0.12/0.38 tff(1,plain,
% 0.12/0.38 ((a_440 = store(a_438, i2, e_439)) <=> (a_440 = store(a_438, i2, e_439))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(2,axiom,(a_440 = store(a_438, i2, e_439)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp13')).
% 0.12/0.38 tff(3,plain,
% 0.12/0.38 (a_440 = store(a_438, i2, e_439)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.12/0.38 tff(4,plain,
% 0.12/0.38 (store(a_438, i2, e_439) = a_440),
% 0.12/0.38 inference(symmetry,[status(thm)],[3])).
% 0.12/0.38 tff(5,plain,
% 0.12/0.38 ((a_426 = store(a_424, i2, e_425)) <=> (a_426 = store(a_424, i2, e_425))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(6,axiom,(a_426 = store(a_424, i2, e_425)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp5')).
% 0.12/0.38 tff(7,plain,
% 0.12/0.38 (a_426 = store(a_424, i2, e_425)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.12/0.38 tff(8,plain,
% 0.12/0.38 (store(a_424, i2, e_425) = a_426),
% 0.12/0.38 inference(symmetry,[status(thm)],[7])).
% 0.12/0.38 tff(9,plain,
% 0.12/0.38 ((e_425 = select(a_422, i3)) <=> (e_425 = select(a_422, i3))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(10,axiom,(e_425 = select(a_422, i3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp18')).
% 0.12/0.38 tff(11,plain,
% 0.12/0.38 (e_425 = select(a_422, i3)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.12/0.38 tff(12,plain,
% 0.12/0.38 (select(a_422, i3) = e_425),
% 0.12/0.38 inference(symmetry,[status(thm)],[11])).
% 0.12/0.38 tff(13,plain,
% 0.12/0.38 ((e_421 = select(a_418, i0)) <=> (e_421 = select(a_418, i0))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(14,axiom,(e_421 = select(a_418, i0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp16')).
% 0.12/0.38 tff(15,plain,
% 0.12/0.38 (e_421 = select(a_418, i0)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[14, 13])).
% 0.12/0.38 tff(16,plain,
% 0.12/0.38 (select(a_418, i0) = e_421),
% 0.12/0.38 inference(symmetry,[status(thm)],[15])).
% 0.12/0.38 tff(17,plain,
% 0.12/0.38 ((a_420 = store(a_418, i0, e_419)) <=> (a_420 = store(a_418, i0, e_419))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(18,axiom,(a_420 = store(a_418, i0, e_419)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp2')).
% 0.12/0.38 tff(19,plain,
% 0.12/0.38 (a_420 = store(a_418, i0, e_419)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.12/0.38 tff(20,plain,
% 0.12/0.38 (store(a_418, i0, e_419) = a_420),
% 0.12/0.38 inference(symmetry,[status(thm)],[19])).
% 0.12/0.38 tff(21,plain,
% 0.12/0.38 (store(store(a_418, i0, e_419), i3, select(a_418, i0)) = store(a_420, i3, e_421)),
% 0.12/0.38 inference(monotonicity,[status(thm)],[20, 16])).
% 0.12/0.38 tff(22,plain,
% 0.12/0.38 (store(a_420, i3, e_421) = store(store(a_418, i0, e_419), i3, select(a_418, i0))),
% 0.12/0.38 inference(symmetry,[status(thm)],[21])).
% 0.12/0.38 tff(23,plain,
% 0.12/0.38 ((a_422 = store(a_420, i3, e_421)) <=> (a_422 = store(a_420, i3, e_421))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(24,axiom,(a_422 = store(a_420, i3, e_421)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp3')).
% 0.12/0.38 tff(25,plain,
% 0.12/0.38 (a_422 = store(a_420, i3, e_421)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.12/0.38 tff(26,plain,
% 0.12/0.38 (a_422 = store(store(a_418, i0, e_419), i3, select(a_418, i0))),
% 0.12/0.38 inference(transitivity,[status(thm)],[25, 22])).
% 0.12/0.38 tff(27,plain,
% 0.12/0.38 (select(a_422, i3) = select(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3)),
% 0.12/0.38 inference(monotonicity,[status(thm)],[26])).
% 0.12/0.38 tff(28,plain,
% 0.12/0.38 (select(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3) = select(a_422, i3)),
% 0.12/0.38 inference(symmetry,[status(thm)],[27])).
% 0.12/0.38 tff(29,plain,
% 0.12/0.38 (![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.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(30,plain,
% 0.12/0.38 (![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.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(31,axiom,(![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','a1')).
% 0.12/0.38 tff(32,plain,
% 0.12/0.38 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.12/0.38 tff(33,plain,(
% 0.12/0.38 ![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.38 inference(skolemize,[status(sab)],[32])).
% 0.12/0.38 tff(34,plain,
% 0.12/0.38 (![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[33, 29])).
% 0.12/0.38 tff(35,plain,
% 0.12/0.38 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3) = select(a_418, i0))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(36,plain,
% 0.12/0.38 (select(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3) = select(a_418, i0)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[35, 34])).
% 0.12/0.38 tff(37,plain,
% 0.12/0.38 (select(a_418, i0) = select(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3)),
% 0.12/0.38 inference(symmetry,[status(thm)],[36])).
% 0.12/0.38 tff(38,plain,
% 0.12/0.38 ((a_418 = store(a_417, i1, e_416)) <=> (a_418 = store(a_417, i1, e_416))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(39,axiom,(a_418 = store(a_417, i1, e_416)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp1')).
% 0.12/0.38 tff(40,plain,
% 0.12/0.38 (a_418 = store(a_417, i1, e_416)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.12/0.38 tff(41,plain,
% 0.12/0.38 (store(a_417, i1, e_416) = a_418),
% 0.12/0.38 inference(symmetry,[status(thm)],[40])).
% 0.12/0.38 tff(42,plain,
% 0.12/0.38 ((e_416 = select(a1, i1)) <=> (e_416 = select(a1, i1))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(43,axiom,(e_416 = select(a1, i1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp14')).
% 0.12/0.38 tff(44,plain,
% 0.12/0.38 (e_416 = select(a1, i1)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.12/0.38 tff(45,plain,
% 0.12/0.38 (store(a1, i1, e_416) = store(a1, i1, select(a1, i1))),
% 0.12/0.38 inference(monotonicity,[status(thm)],[44])).
% 0.12/0.38 tff(46,plain,
% 0.12/0.38 ((a_417 = store(a1, i1, e_416)) <=> (a_417 = store(a1, i1, e_416))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(47,axiom,(a_417 = store(a1, i1, e_416)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp0')).
% 0.12/0.38 tff(48,plain,
% 0.12/0.38 (a_417 = store(a1, i1, e_416)),
% 0.12/0.38 inference(modus_ponens,[status(thm)],[47, 46])).
% 0.12/0.38 tff(49,plain,
% 0.12/0.38 (a_417 = store(a1, i1, select(a1, i1))),
% 0.12/0.38 inference(transitivity,[status(thm)],[48, 45])).
% 0.12/0.38 tff(50,plain,
% 0.12/0.38 (store(a_417, i1, e_416) = store(store(a1, i1, select(a1, i1)), i1, select(a1, i1))),
% 0.12/0.38 inference(monotonicity,[status(thm)],[49, 44])).
% 0.12/0.38 tff(51,plain,
% 0.12/0.38 (store(store(a1, i1, select(a1, i1)), i1, select(a1, i1)) = store(a_417, i1, e_416)),
% 0.12/0.38 inference(symmetry,[status(thm)],[50])).
% 0.12/0.38 tff(52,plain,
% 0.12/0.38 (^[I: $i, E: $i, A: $i, F: $i] : refl((store(store(A, I, E), I, F) = store(A, I, F)) <=> (store(store(A, I, E), I, F) = store(A, I, F)))),
% 0.12/0.38 inference(bind,[status(th)],[])).
% 0.12/0.38 tff(53,plain,
% 0.12/0.38 (![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F)) <=> ![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))),
% 0.12/0.38 inference(quant_intro,[status(thm)],[52])).
% 0.12/0.38 tff(54,plain,
% 0.12/0.38 (![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F)) <=> ![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(55,axiom,(![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','a4')).
% 0.12/0.39 tff(56,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.12/0.39 tff(57,plain,(
% 0.12/0.39 ![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))),
% 0.12/0.39 inference(skolemize,[status(sab)],[56])).
% 0.12/0.39 tff(58,plain,
% 0.12/0.39 (![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[57, 53])).
% 0.12/0.39 tff(59,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))) | (store(store(a1, i1, select(a1, i1)), i1, select(a1, i1)) = store(a1, i1, select(a1, i1)))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(60,plain,
% 0.12/0.39 (store(store(a1, i1, select(a1, i1)), i1, select(a1, i1)) = store(a1, i1, select(a1, i1))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.12/0.39 tff(61,plain,
% 0.12/0.39 (store(a1, i1, select(a1, i1)) = store(store(a1, i1, select(a1, i1)), i1, select(a1, i1))),
% 0.12/0.39 inference(symmetry,[status(thm)],[60])).
% 0.12/0.39 tff(62,plain,
% 0.12/0.39 (store(a1, i1, e_416) = a_418),
% 0.12/0.39 inference(transitivity,[status(thm)],[45, 61, 51, 41])).
% 0.12/0.39 tff(63,plain,
% 0.12/0.39 (select(store(a1, i1, e_416), i0) = select(a_418, i0)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[62])).
% 0.12/0.39 tff(64,plain,
% 0.12/0.39 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i3) = select(a_418, i0))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(65,plain,
% 0.12/0.39 (select(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i3) = select(a_418, i0)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[64, 34])).
% 0.12/0.39 tff(66,plain,
% 0.12/0.39 (store(store(a_417, i1, e_416), i3, select(a_418, i0)) = store(a_418, i3, e_421)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[41, 16])).
% 0.12/0.39 tff(67,plain,
% 0.12/0.39 (store(a_418, i3, e_421) = store(store(a_417, i1, e_416), i3, select(a_418, i0))),
% 0.12/0.39 inference(symmetry,[status(thm)],[66])).
% 0.12/0.39 tff(68,plain,
% 0.12/0.39 (select(store(a_418, i3, e_421), i3) = select(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i3)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[67])).
% 0.12/0.39 tff(69,assumption,(~(i0 = i3)), introduced(assumption)).
% 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,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(72,axiom,(![I: $i, E: $i, A: $i, J: $i] : ((I = J) | (select(store(A, I, E), J) = select(A, J)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','a2')).
% 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(modus_ponens,[status(thm)],[72, 71])).
% 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(skolemize,[status(sab)],[73])).
% 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)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[74, 70])).
% 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_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), 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_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), i3)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(77,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_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), i3)))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(78,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_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), i3))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.12/0.39 tff(79,plain,
% 0.12/0.39 ((i0 = i3) | (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), i3))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[78, 75])).
% 0.12/0.39 tff(80,plain,
% 0.12/0.39 (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i3) = select(store(a_418, i3, e_421), i3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[79, 69])).
% 0.12/0.39 tff(81,plain,
% 0.12/0.39 ((e_419 = select(a_418, i3)) <=> (e_419 = select(a_418, i3))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(82,axiom,(e_419 = select(a_418, i3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp15')).
% 0.12/0.39 tff(83,plain,
% 0.12/0.39 (e_419 = select(a_418, i3)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[82, 81])).
% 0.12/0.39 tff(84,plain,
% 0.12/0.39 (select(a_418, i3) = e_419),
% 0.12/0.39 inference(symmetry,[status(thm)],[83])).
% 0.12/0.39 tff(85,plain,
% 0.12/0.39 ((a_431 = store(a_418, i3, e_421)) <=> (a_431 = store(a_418, i3, e_421))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(86,axiom,(a_431 = store(a_418, i3, e_421)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp8')).
% 0.12/0.39 tff(87,plain,
% 0.12/0.39 (a_431 = store(a_418, i3, e_421)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[86, 85])).
% 0.12/0.39 tff(88,plain,
% 0.12/0.39 (store(a_418, i3, e_421) = a_431),
% 0.12/0.39 inference(symmetry,[status(thm)],[87])).
% 0.12/0.39 tff(89,plain,
% 0.12/0.39 (store(store(a_418, i3, e_421), i0, select(a_418, i3)) = store(a_431, i0, e_419)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[88, 84])).
% 0.12/0.39 tff(90,plain,
% 0.12/0.39 (store(a_431, i0, e_419) = store(store(a_418, i3, e_421), i0, select(a_418, i3))),
% 0.12/0.39 inference(symmetry,[status(thm)],[89])).
% 0.12/0.39 tff(91,plain,
% 0.12/0.39 ((a_432 = store(a_431, i0, e_419)) <=> (a_432 = store(a_431, i0, e_419))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(92,axiom,(a_432 = store(a_431, i0, e_419)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp9')).
% 0.12/0.39 tff(93,plain,
% 0.12/0.39 (a_432 = store(a_431, i0, e_419)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.12/0.39 tff(94,plain,
% 0.12/0.39 (a_432 = store(store(a_418, i3, e_421), i0, select(a_418, i3))),
% 0.12/0.39 inference(transitivity,[status(thm)],[93, 90])).
% 0.12/0.39 tff(95,plain,
% 0.12/0.39 (select(a_432, i3) = select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i3)),
% 0.12/0.39 inference(monotonicity,[status(thm)],[94])).
% 0.12/0.39 tff(96,plain,
% 0.12/0.39 ((e_435 = select(a_432, i3)) <=> (e_435 = select(a_432, i3))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(97,axiom,(e_435 = select(a_432, i3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp22')).
% 0.12/0.39 tff(98,plain,
% 0.12/0.39 (e_435 = select(a_432, i3)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[97, 96])).
% 0.12/0.39 tff(99,plain,
% 0.12/0.39 (e_435 = e_425),
% 0.12/0.39 inference(transitivity,[status(thm)],[98, 95, 80, 68, 65, 37, 28, 12])).
% 0.12/0.39 tff(100,plain,
% 0.12/0.39 ((a_424 = store(a_422, i3, e_423)) <=> (a_424 = store(a_422, i3, e_423))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(101,axiom,(a_424 = store(a_422, i3, e_423)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp4')).
% 0.12/0.39 tff(102,plain,
% 0.12/0.39 (a_424 = store(a_422, i3, e_423)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[101, 100])).
% 0.12/0.39 tff(103,plain,
% 0.12/0.39 (store(a_422, i3, e_423) = a_424),
% 0.12/0.39 inference(symmetry,[status(thm)],[102])).
% 0.12/0.39 tff(104,plain,
% 0.12/0.39 ((e_423 = select(a_422, i2)) <=> (e_423 = select(a_422, i2))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(105,axiom,(e_423 = select(a_422, i2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp17')).
% 0.12/0.39 tff(106,plain,
% 0.12/0.39 (e_423 = select(a_422, i2)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.12/0.39 tff(107,plain,
% 0.12/0.39 (select(a_422, i2) = e_423),
% 0.12/0.39 inference(symmetry,[status(thm)],[106])).
% 0.12/0.40 tff(108,plain,
% 0.12/0.40 (store(a_431, i0, e_419) = a_432),
% 0.12/0.40 inference(symmetry,[status(thm)],[93])).
% 0.12/0.40 tff(109,plain,
% 0.12/0.40 (store(store(a_417, i1, e_416), i3, select(a_418, i0)) = a_431),
% 0.12/0.40 inference(transitivity,[status(thm)],[66, 88])).
% 0.12/0.40 tff(110,plain,
% 0.12/0.40 (store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3)) = store(a_431, i0, e_419)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[109, 84])).
% 0.12/0.40 tff(111,plain,
% 0.12/0.40 (^[I: $i, E: $i, A: $i, J: $i, F: $i] : refl(((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E))) <=> ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(112,plain,
% 0.12/0.40 (![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E))) <=> ![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[111])).
% 0.12/0.40 tff(113,plain,
% 0.12/0.40 (![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E))) <=> ![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(114,axiom,(![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','a5')).
% 0.12/0.40 tff(115,plain,
% 0.12/0.40 (![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[114, 113])).
% 0.12/0.40 tff(116,plain,(
% 0.12/0.40 ![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))),
% 0.12/0.40 inference(skolemize,[status(sab)],[115])).
% 0.12/0.40 tff(117,plain,
% 0.12/0.40 (![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[116, 112])).
% 0.12/0.40 tff(118,plain,
% 0.12/0.40 (((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | ((i0 = i3) | (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3))))) <=> ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | (i0 = i3) | (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3))))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(119,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | ((i0 = i3) | (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3))))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(120,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | (i0 = i3) | (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.12/0.40 tff(121,plain,
% 0.12/0.40 ((i0 = i3) | (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3)))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[120, 117])).
% 0.12/0.40 tff(122,plain,
% 0.12/0.40 (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[121, 69])).
% 0.12/0.40 tff(123,plain,
% 0.12/0.40 (store(store(a_417, i1, e_416), i0, select(a_418, i3)) = store(a_418, i0, e_419)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[41, 84])).
% 0.12/0.40 tff(124,plain,
% 0.12/0.40 (store(a_418, i0, e_419) = store(store(a_417, i1, e_416), i0, select(a_418, i3))),
% 0.12/0.40 inference(symmetry,[status(thm)],[123])).
% 0.12/0.40 tff(125,plain,
% 0.12/0.40 (a_420 = store(store(a_417, i1, e_416), i0, select(a_418, i3))),
% 0.12/0.40 inference(transitivity,[status(thm)],[19, 124])).
% 0.12/0.40 tff(126,plain,
% 0.12/0.40 (store(a_420, i3, e_421) = store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[125, 15])).
% 0.12/0.40 tff(127,plain,
% 0.12/0.40 (a_422 = a_432),
% 0.12/0.40 inference(transitivity,[status(thm)],[25, 126, 122, 110, 108])).
% 0.12/0.40 tff(128,plain,
% 0.12/0.40 (select(a_422, i2) = select(a_432, i2)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[127])).
% 0.12/0.40 tff(129,plain,
% 0.12/0.40 (select(a_432, i2) = select(a_422, i2)),
% 0.12/0.40 inference(symmetry,[status(thm)],[128])).
% 0.12/0.40 tff(130,plain,
% 0.12/0.40 ((e_433 = select(a_432, i2)) <=> (e_433 = select(a_432, i2))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(131,axiom,(e_433 = select(a_432, i2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp21')).
% 0.12/0.40 tff(132,plain,
% 0.12/0.40 (e_433 = select(a_432, i2)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.12/0.40 tff(133,plain,
% 0.12/0.40 (e_433 = e_423),
% 0.12/0.40 inference(transitivity,[status(thm)],[132, 129, 107])).
% 0.12/0.40 tff(134,plain,
% 0.12/0.40 (store(a_420, i3, e_421) = a_422),
% 0.12/0.40 inference(symmetry,[status(thm)],[25])).
% 0.12/0.40 tff(135,plain,
% 0.12/0.40 (store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0)) = store(a_420, i3, e_421)),
% 0.12/0.40 inference(symmetry,[status(thm)],[126])).
% 0.12/0.40 tff(136,plain,
% 0.12/0.40 (store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3)) = store(store(store(a_417, i1, e_416), i0, select(a_418, i3)), i3, select(a_418, i0))),
% 0.12/0.40 inference(symmetry,[status(thm)],[122])).
% 0.12/0.40 tff(137,plain,
% 0.12/0.40 (store(a_431, i0, e_419) = store(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i0, select(a_418, i3))),
% 0.12/0.40 inference(symmetry,[status(thm)],[110])).
% 0.12/0.40 tff(138,plain,
% 0.12/0.40 (a_432 = a_422),
% 0.12/0.40 inference(transitivity,[status(thm)],[93, 137, 136, 135, 134])).
% 0.12/0.40 tff(139,plain,
% 0.12/0.40 (store(a_432, i3, e_433) = store(a_422, i3, e_423)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[138, 133])).
% 0.12/0.40 tff(140,plain,
% 0.12/0.40 ((a_434 = store(a_432, i3, e_433)) <=> (a_434 = store(a_432, i3, e_433))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(141,axiom,(a_434 = store(a_432, i3, e_433)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp10')).
% 0.12/0.40 tff(142,plain,
% 0.12/0.40 (a_434 = store(a_432, i3, e_433)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[141, 140])).
% 0.12/0.40 tff(143,plain,
% 0.12/0.40 (a_434 = a_424),
% 0.12/0.40 inference(transitivity,[status(thm)],[142, 139, 103])).
% 0.12/0.40 tff(144,plain,
% 0.12/0.40 (store(a_434, i2, e_435) = store(a_424, i2, e_425)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[143, 99])).
% 0.12/0.40 tff(145,plain,
% 0.12/0.40 ((a_436 = store(a_434, i2, e_435)) <=> (a_436 = store(a_434, i2, e_435))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(146,axiom,(a_436 = store(a_434, i2, e_435)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp11')).
% 0.12/0.40 tff(147,plain,
% 0.12/0.40 (a_436 = store(a_434, i2, e_435)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.12/0.40 tff(148,plain,
% 0.12/0.40 (a_436 = a_426),
% 0.12/0.40 inference(transitivity,[status(thm)],[147, 144, 8])).
% 0.12/0.40 tff(149,plain,
% 0.12/0.40 (select(a_436, i0) = select(a_426, i0)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[148])).
% 0.12/0.40 tff(150,plain,
% 0.12/0.40 ((e_439 = select(a_436, i0)) <=> (e_439 = select(a_436, i0))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(151,axiom,(e_439 = select(a_436, i0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp24')).
% 0.12/0.40 tff(152,plain,
% 0.12/0.40 (e_439 = select(a_436, i0)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.12/0.40 tff(153,plain,
% 0.12/0.40 (e_439 = select(a_426, i0)),
% 0.12/0.40 inference(transitivity,[status(thm)],[152, 149])).
% 0.12/0.40 tff(154,plain,
% 0.12/0.40 (store(store(a_422, i3, e_423), i2, select(a_422, i3)) = store(a_424, i2, e_425)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[103, 12])).
% 0.12/0.40 tff(155,plain,
% 0.12/0.40 (store(a_424, i2, e_425) = store(store(a_422, i3, e_423), i2, select(a_422, i3))),
% 0.12/0.40 inference(symmetry,[status(thm)],[154])).
% 0.12/0.40 tff(156,plain,
% 0.12/0.40 (a_426 = store(store(a_422, i3, e_423), i2, select(a_422, i3))),
% 0.12/0.40 inference(transitivity,[status(thm)],[7, 155])).
% 0.12/0.40 tff(157,plain,
% 0.12/0.40 (select(a_426, i2) = select(store(store(a_422, i3, e_423), i2, select(a_422, i3)), i2)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[156])).
% 0.12/0.40 tff(158,plain,
% 0.12/0.40 (select(store(store(a_422, i3, e_423), i2, select(a_422, i3)), i2) = select(a_426, i2)),
% 0.12/0.40 inference(symmetry,[status(thm)],[157])).
% 0.12/0.40 tff(159,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_422, i3, e_423), i2, select(a_422, i3)), i2) = select(a_422, i3))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(160,plain,
% 0.12/0.40 (select(store(store(a_422, i3, e_423), i2, select(a_422, i3)), i2) = select(a_422, i3)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[159, 34])).
% 0.12/0.40 tff(161,plain,
% 0.12/0.40 (select(a_422, i3) = select(store(store(a_422, i3, e_423), i2, select(a_422, i3)), i2)),
% 0.12/0.40 inference(symmetry,[status(thm)],[160])).
% 0.12/0.40 tff(162,plain,
% 0.12/0.40 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_432, i3, e_433), i2, select(a_432, i3)), i2) = select(a_432, i3))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(163,plain,
% 0.12/0.40 (select(store(store(a_432, i3, e_433), i2, select(a_432, i3)), i2) = select(a_432, i3)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[162, 34])).
% 0.12/0.40 tff(164,plain,
% 0.12/0.40 (select(a_432, i3) = e_435),
% 0.12/0.40 inference(symmetry,[status(thm)],[98])).
% 0.12/0.40 tff(165,plain,
% 0.12/0.40 (store(a_432, i3, e_433) = a_434),
% 0.12/0.40 inference(symmetry,[status(thm)],[142])).
% 0.12/0.40 tff(166,plain,
% 0.12/0.40 (store(store(a_432, i3, e_433), i2, select(a_432, i3)) = store(a_434, i2, e_435)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[165, 164])).
% 0.12/0.40 tff(167,plain,
% 0.12/0.40 (store(a_434, i2, e_435) = store(store(a_432, i3, e_433), i2, select(a_432, i3))),
% 0.12/0.40 inference(symmetry,[status(thm)],[166])).
% 0.12/0.40 tff(168,plain,
% 0.12/0.40 (a_436 = store(store(a_432, i3, e_433), i2, select(a_432, i3))),
% 0.12/0.40 inference(transitivity,[status(thm)],[147, 167])).
% 0.12/0.40 tff(169,plain,
% 0.12/0.40 (select(a_436, i2) = select(store(store(a_432, i3, e_433), i2, select(a_432, i3)), i2)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[168])).
% 0.12/0.40 tff(170,plain,
% 0.12/0.40 ((e_437 = select(a_436, i2)) <=> (e_437 = select(a_436, i2))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(171,axiom,(e_437 = select(a_436, i2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp23')).
% 0.12/0.40 tff(172,plain,
% 0.12/0.40 (e_437 = select(a_436, i2)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.12/0.40 tff(173,plain,
% 0.12/0.40 (e_437 = select(a_426, i2)),
% 0.12/0.40 inference(transitivity,[status(thm)],[172, 169, 163, 95, 80, 68, 65, 37, 28, 161, 158])).
% 0.12/0.40 tff(174,plain,
% 0.12/0.40 (a_436 = store(a_424, i2, e_425)),
% 0.12/0.40 inference(transitivity,[status(thm)],[147, 144])).
% 0.12/0.40 tff(175,plain,
% 0.12/0.40 (store(a_436, i0, e_437) = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[174, 173])).
% 0.12/0.40 tff(176,plain,
% 0.12/0.40 ((a_438 = store(a_436, i0, e_437)) <=> (a_438 = store(a_436, i0, e_437))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(177,axiom,(a_438 = store(a_436, i0, e_437)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp12')).
% 0.12/0.40 tff(178,plain,
% 0.12/0.40 (a_438 = store(a_436, i0, e_437)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.12/0.40 tff(179,plain,
% 0.12/0.40 (a_438 = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.12/0.40 inference(transitivity,[status(thm)],[178, 175])).
% 0.12/0.40 tff(180,plain,
% 0.12/0.40 (store(a_438, i2, e_439) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.12/0.40 inference(monotonicity,[status(thm)],[179, 153])).
% 0.12/0.40 tff(181,plain,
% 0.12/0.40 (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(a_438, i2, e_439)),
% 0.12/0.40 inference(symmetry,[status(thm)],[180])).
% 0.12/0.40 tff(182,plain,
% 0.12/0.40 (select(a_436, i2) = e_437),
% 0.12/0.40 inference(symmetry,[status(thm)],[172])).
% 0.12/0.40 tff(183,plain,
% 0.12/0.40 (store(a_434, i2, e_435) = a_436),
% 0.12/0.40 inference(symmetry,[status(thm)],[147])).
% 0.12/0.40 tff(184,plain,
% 0.12/0.40 (store(store(a_434, i2, e_435), i0, select(a_436, i2)) = store(a_436, i0, e_437)),
% 0.12/0.40 inference(monotonicity,[status(thm)],[183, 182])).
% 0.12/0.41 tff(185,plain,
% 0.12/0.41 (store(a_436, i0, e_437) = store(store(a_434, i2, e_435), i0, select(a_436, i2))),
% 0.12/0.41 inference(symmetry,[status(thm)],[184])).
% 0.12/0.41 tff(186,plain,
% 0.12/0.41 (select(store(a_436, i0, e_437), i0) = select(store(store(a_434, i2, e_435), i0, select(a_436, i2)), i0)),
% 0.12/0.41 inference(monotonicity,[status(thm)],[185])).
% 0.12/0.41 tff(187,plain,
% 0.12/0.41 (select(store(store(a_434, i2, e_435), i0, select(a_436, i2)), i0) = select(store(a_436, i0, e_437), i0)),
% 0.12/0.41 inference(symmetry,[status(thm)],[186])).
% 0.12/0.41 tff(188,plain,
% 0.12/0.41 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_434, i2, e_435), i0, select(a_436, i2)), i0) = select(a_436, i2))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(189,plain,
% 0.12/0.41 (select(store(store(a_434, i2, e_435), i0, select(a_436, i2)), i0) = select(a_436, i2)),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[188, 34])).
% 0.12/0.41 tff(190,plain,
% 0.12/0.41 (select(a_436, i2) = select(store(store(a_434, i2, e_435), i0, select(a_436, i2)), i0)),
% 0.12/0.41 inference(symmetry,[status(thm)],[189])).
% 0.12/0.41 tff(191,plain,
% 0.12/0.41 (select(store(store(a_432, i3, e_433), i2, select(a_432, i3)), i2) = select(a_436, i2)),
% 0.12/0.41 inference(symmetry,[status(thm)],[169])).
% 0.12/0.41 tff(192,plain,
% 0.12/0.41 (select(a_432, i3) = select(store(store(a_432, i3, e_433), i2, select(a_432, i3)), i2)),
% 0.12/0.41 inference(symmetry,[status(thm)],[163])).
% 0.12/0.41 tff(193,plain,
% 0.12/0.41 (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i3) = select(a_432, i3)),
% 0.12/0.41 inference(symmetry,[status(thm)],[95])).
% 0.12/0.41 tff(194,plain,
% 0.12/0.41 (select(store(a_418, i3, e_421), i3) = select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i3)),
% 0.12/0.41 inference(symmetry,[status(thm)],[80])).
% 0.12/0.41 tff(195,plain,
% 0.12/0.41 (select(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i3) = select(store(a_418, i3, e_421), i3)),
% 0.12/0.41 inference(symmetry,[status(thm)],[68])).
% 0.12/0.41 tff(196,plain,
% 0.12/0.41 (select(a_418, i0) = select(store(store(a_417, i1, e_416), i3, select(a_418, i0)), i3)),
% 0.12/0.41 inference(symmetry,[status(thm)],[65])).
% 0.12/0.41 tff(197,plain,
% 0.12/0.41 ((store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))) <=> (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.12/0.41 inference(commutativity,[status(thm)],[])).
% 0.12/0.41 tff(198,plain,
% 0.12/0.41 (a_440 = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.12/0.41 inference(transitivity,[status(thm)],[3, 180])).
% 0.12/0.41 tff(199,plain,
% 0.12/0.41 ((e_429 = select(a_426, i2)) <=> (e_429 = select(a_426, i2))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(200,axiom,(e_429 = select(a_426, i2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp20')).
% 0.12/0.41 tff(201,plain,
% 0.12/0.41 (e_429 = select(a_426, i2)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[200, 199])).
% 0.12/0.41 tff(202,plain,
% 0.12/0.41 (select(a_426, i2) = e_429),
% 0.12/0.41 inference(symmetry,[status(thm)],[201])).
% 0.12/0.41 tff(203,plain,
% 0.12/0.41 ((a_428 = store(a_426, i2, e_427)) <=> (a_428 = store(a_426, i2, e_427))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(204,axiom,(a_428 = store(a_426, i2, e_427)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp6')).
% 0.12/0.41 tff(205,plain,
% 0.12/0.41 (a_428 = store(a_426, i2, e_427)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[204, 203])).
% 0.12/0.41 tff(206,plain,
% 0.12/0.41 (store(a_426, i2, e_427) = a_428),
% 0.12/0.41 inference(symmetry,[status(thm)],[205])).
% 0.12/0.41 tff(207,plain,
% 0.12/0.41 ((e_427 = select(a_426, i0)) <=> (e_427 = select(a_426, i0))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(208,axiom,(e_427 = select(a_426, i0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp19')).
% 0.12/0.41 tff(209,plain,
% 0.12/0.41 (e_427 = select(a_426, i0)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[208, 207])).
% 0.12/0.41 tff(210,plain,
% 0.12/0.41 (select(a_426, i0) = e_427),
% 0.12/0.41 inference(symmetry,[status(thm)],[209])).
% 0.12/0.41 tff(211,plain,
% 0.12/0.41 (store(store(a_424, i2, e_425), i2, select(a_426, i0)) = store(a_426, i2, e_427)),
% 0.12/0.41 inference(monotonicity,[status(thm)],[8, 210])).
% 0.12/0.41 tff(212,plain,
% 0.12/0.41 (store(store(a_424, i2, e_425), i2, select(a_426, i0)) = a_428),
% 0.12/0.41 inference(transitivity,[status(thm)],[211, 206])).
% 0.12/0.41 tff(213,plain,
% 0.12/0.41 (store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)) = store(a_428, i0, e_429)),
% 0.12/0.41 inference(monotonicity,[status(thm)],[212, 202])).
% 0.12/0.41 tff(214,plain,
% 0.12/0.41 (store(a_428, i0, e_429) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))),
% 0.12/0.41 inference(symmetry,[status(thm)],[213])).
% 0.12/0.41 tff(215,plain,
% 0.12/0.41 ((a_430 = store(a_428, i0, e_429)) <=> (a_430 = store(a_428, i0, e_429))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(216,axiom,(a_430 = store(a_428, i0, e_429)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','hyp7')).
% 0.12/0.41 tff(217,plain,
% 0.12/0.41 (a_430 = store(a_428, i0, e_429)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[216, 215])).
% 0.12/0.41 tff(218,plain,
% 0.12/0.41 (a_430 = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))),
% 0.12/0.41 inference(transitivity,[status(thm)],[217, 214])).
% 0.12/0.41 tff(219,plain,
% 0.12/0.41 ((a_430 = a_440) <=> (store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)))),
% 0.12/0.41 inference(monotonicity,[status(thm)],[218, 198])).
% 0.12/0.41 tff(220,plain,
% 0.12/0.41 ((a_430 = a_440) <=> (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.12/0.41 inference(transitivity,[status(thm)],[219, 197])).
% 0.12/0.41 tff(221,plain,
% 0.12/0.41 ((~(a_430 = a_440)) <=> (~(store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))))),
% 0.12/0.41 inference(monotonicity,[status(thm)],[220])).
% 0.12/0.41 tff(222,plain,
% 0.12/0.41 ((~(a_430 = a_440)) <=> (~(a_430 = a_440))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(223,axiom,(~(a_430 = a_440)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','goal')).
% 0.12/0.41 tff(224,plain,
% 0.12/0.41 (~(a_430 = a_440)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[223, 222])).
% 0.12/0.41 tff(225,plain,
% 0.12/0.41 (~(store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[224, 221])).
% 0.12/0.41 tff(226,plain,
% 0.12/0.41 (((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | ((i0 = i2) | (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))))) <=> ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | (i0 = i2) | (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(227,plain,
% 0.12/0.41 ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | ((i0 = i2) | (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(228,plain,
% 0.12/0.41 ((~![I: $i, E: $i, A: $i, J: $i, F: $i] : ((I = J) | (store(store(A, I, E), J, F) = store(store(A, J, F), I, E)))) | (i0 = i2) | (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[227, 226])).
% 0.12/0.41 tff(229,plain,
% 0.12/0.41 ((i0 = i2) | (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[228, 117])).
% 0.12/0.41 tff(230,plain,
% 0.12/0.41 (i0 = i2),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[229, 225])).
% 0.19/0.41 tff(231,plain,
% 0.19/0.41 (select(a_426, i0) = select(a_426, i2)),
% 0.19/0.41 inference(monotonicity,[status(thm)],[230])).
% 0.19/0.41 tff(232,plain,
% 0.19/0.41 (select(a_426, i0) = select(store(a_436, i0, e_437), i0)),
% 0.19/0.41 inference(transitivity,[status(thm)],[231, 157, 160, 27, 36, 196, 195, 194, 193, 192, 191, 190, 187])).
% 0.19/0.41 tff(233,plain,
% 0.19/0.41 (i2 = i0),
% 0.19/0.41 inference(symmetry,[status(thm)],[230])).
% 0.19/0.41 tff(234,plain,
% 0.19/0.41 (store(store(a_424, i2, e_425), i0, select(a_426, i2)) = store(a_436, i0, e_437)),
% 0.19/0.41 inference(symmetry,[status(thm)],[175])).
% 0.19/0.41 tff(235,plain,
% 0.19/0.41 (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0))),
% 0.19/0.41 inference(monotonicity,[status(thm)],[234, 233, 232])).
% 0.19/0.41 tff(236,plain,
% 0.19/0.41 (store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0)) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.19/0.41 inference(symmetry,[status(thm)],[235])).
% 0.19/0.41 tff(237,plain,
% 0.19/0.41 (^[I: $i, A: $i] : refl((store(A, I, select(A, I)) = A) <=> (store(A, I, select(A, I)) = A))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(238,plain,
% 0.19/0.41 (![I: $i, A: $i] : (store(A, I, select(A, I)) = A) <=> ![I: $i, A: $i] : (store(A, I, select(A, I)) = A)),
% 0.19/0.41 inference(quant_intro,[status(thm)],[237])).
% 0.19/0.41 tff(239,plain,
% 0.19/0.41 (![I: $i, A: $i] : (store(A, I, select(A, I)) = A) <=> ![I: $i, A: $i] : (store(A, I, select(A, I)) = A)),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(240,axiom,(![I: $i, A: $i] : (store(A, I, select(A, I)) = A)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','a3')).
% 0.19/0.41 tff(241,plain,
% 0.19/0.41 (![I: $i, A: $i] : (store(A, I, select(A, I)) = A)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[240, 239])).
% 0.19/0.41 tff(242,plain,(
% 0.19/0.41 ![I: $i, A: $i] : (store(A, I, select(A, I)) = A)),
% 0.19/0.41 inference(skolemize,[status(sab)],[241])).
% 0.19/0.41 tff(243,plain,
% 0.19/0.41 (![I: $i, A: $i] : (store(A, I, select(A, I)) = A)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[242, 238])).
% 0.19/0.41 tff(244,plain,
% 0.19/0.41 ((~![I: $i, A: $i] : (store(A, I, select(A, I)) = A)) | (store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0)) = store(a_436, i0, e_437))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(245,plain,
% 0.19/0.42 (store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0)) = store(a_436, i0, e_437)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[244, 243])).
% 0.19/0.42 tff(246,plain,
% 0.19/0.42 (store(a_436, i0, e_437) = store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0))),
% 0.19/0.42 inference(symmetry,[status(thm)],[245])).
% 0.19/0.42 tff(247,plain,
% 0.19/0.42 ((~![I: $i, A: $i] : (store(A, I, select(A, I)) = A)) | (store(store(a_424, i2, e_425), i0, select(store(a_424, i2, e_425), i0)) = store(a_424, i2, e_425))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(248,plain,
% 0.19/0.42 (store(store(a_424, i2, e_425), i0, select(store(a_424, i2, e_425), i0)) = store(a_424, i2, e_425)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[247, 243])).
% 0.19/0.42 tff(249,plain,
% 0.19/0.42 (select(store(a_424, i2, e_425), i0) = select(a_426, i0)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[8])).
% 0.19/0.42 tff(250,plain,
% 0.19/0.42 (select(a_426, i0) = select(store(a_424, i2, e_425), i0)),
% 0.19/0.42 inference(symmetry,[status(thm)],[249])).
% 0.19/0.42 tff(251,plain,
% 0.19/0.42 (e_427 = select(store(a_424, i2, e_425), i0)),
% 0.19/0.42 inference(transitivity,[status(thm)],[209, 250])).
% 0.19/0.42 tff(252,plain,
% 0.19/0.42 (store(a_426, i2, e_427) = store(store(a_424, i2, e_425), i0, select(store(a_424, i2, e_425), i0))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[7, 233, 251])).
% 0.19/0.42 tff(253,plain,
% 0.19/0.42 (a_428 = store(a_424, i2, e_425)),
% 0.19/0.42 inference(transitivity,[status(thm)],[205, 252, 248])).
% 0.19/0.42 tff(254,plain,
% 0.19/0.42 (store(a_428, i0, e_429) = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[253, 201])).
% 0.19/0.42 tff(255,plain,
% 0.19/0.42 (a_430 = a_440),
% 0.19/0.42 inference(transitivity,[status(thm)],[217, 254, 234, 246, 236, 181, 4])).
% 0.19/0.42 tff(256,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[224, 255])).
% 0.19/0.42 tff(257,plain,(i0 = i3), inference(lemma,lemma(discharge,[]))).
% 0.19/0.42 tff(258,plain,
% 0.19/0.42 (i3 = i0),
% 0.19/0.42 inference(symmetry,[status(thm)],[257])).
% 0.19/0.42 tff(259,plain,
% 0.19/0.42 (select(store(a1, i1, e_416), i3) = select(store(a1, i1, e_416), i0)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[258])).
% 0.19/0.42 tff(260,plain,
% 0.19/0.42 (store(a1, i1, select(a1, i1)) = store(a1, i1, e_416)),
% 0.19/0.42 inference(symmetry,[status(thm)],[45])).
% 0.19/0.42 tff(261,plain,
% 0.19/0.42 (a_418 = store(a1, i1, e_416)),
% 0.19/0.42 inference(transitivity,[status(thm)],[40, 50, 60, 260])).
% 0.19/0.42 tff(262,plain,
% 0.19/0.42 (select(a_418, i3) = select(store(a1, i1, e_416), i3)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[261])).
% 0.19/0.42 tff(263,plain,
% 0.19/0.42 ((~![I: $i, E: $i, A: $i] : (select(store(A, I, E), I) = E)) | (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i0) = select(a_418, i3))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(264,plain,
% 0.19/0.42 (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i0) = select(a_418, i3)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[263, 34])).
% 0.19/0.42 tff(265,plain,
% 0.19/0.42 (select(a_432, i3) = select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i0)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[94, 258])).
% 0.19/0.42 tff(266,plain,
% 0.19/0.42 (e_435 = e_425),
% 0.19/0.42 inference(transitivity,[status(thm)],[98, 265, 264, 262, 259, 63, 37, 28, 12])).
% 0.19/0.42 tff(267,plain,
% 0.19/0.42 (store(a_422, i3, e_423) = store(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3, select(a_422, i2))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[26, 106])).
% 0.19/0.42 tff(268,plain,
% 0.19/0.42 (store(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3, select(a_422, i2)) = store(a_422, i3, e_423)),
% 0.19/0.42 inference(symmetry,[status(thm)],[267])).
% 0.19/0.42 tff(269,plain,
% 0.19/0.42 ((~![I: $i, E: $i, A: $i, F: $i] : (store(store(A, I, E), I, F) = store(A, I, F))) | (store(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3, select(a_422, i2)) = store(store(a_418, i0, e_419), i3, select(a_422, i2)))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(270,plain,
% 0.19/0.42 (store(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3, select(a_422, i2)) = store(store(a_418, i0, e_419), i3, select(a_422, i2))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[269, 58])).
% 0.19/0.42 tff(271,plain,
% 0.19/0.42 (store(store(a_418, i0, e_419), i3, select(a_422, i2)) = store(store(store(a_418, i0, e_419), i3, select(a_418, i0)), i3, select(a_422, i2))),
% 0.19/0.42 inference(symmetry,[status(thm)],[270])).
% 0.19/0.42 tff(272,plain,
% 0.19/0.42 ((~![I: $i, A: $i] : (store(A, I, select(A, I)) = A)) | (store(store(a_417, i1, e_416), i3, select(store(a_417, i1, e_416), i3)) = store(a_417, i1, e_416))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(273,plain,
% 0.19/0.42 (store(store(a_417, i1, e_416), i3, select(store(a_417, i1, e_416), i3)) = store(a_417, i1, e_416)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[272, 243])).
% 0.19/0.42 tff(274,plain,
% 0.19/0.42 (select(store(a_417, i1, e_416), i3) = select(a_418, i3)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[41])).
% 0.19/0.42 tff(275,plain,
% 0.19/0.42 (select(a_418, i3) = select(store(a_417, i1, e_416), i3)),
% 0.19/0.42 inference(symmetry,[status(thm)],[274])).
% 0.19/0.42 tff(276,plain,
% 0.19/0.42 (store(a1, i1, e_416) = store(a_417, i1, e_416)),
% 0.19/0.42 inference(transitivity,[status(thm)],[45, 61, 51])).
% 0.19/0.42 tff(277,plain,
% 0.19/0.42 (store(store(a1, i1, e_416), i0, select(a_418, i3)) = store(store(a_417, i1, e_416), i3, select(store(a_417, i1, e_416), i3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[276, 257, 275])).
% 0.19/0.42 tff(278,plain,
% 0.19/0.42 (store(a_418, i0, e_419) = store(store(a1, i1, e_416), i0, select(a_418, i3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[261, 83])).
% 0.19/0.42 tff(279,plain,
% 0.19/0.42 (store(a_418, i0, e_419) = store(a1, i1, select(a1, i1))),
% 0.19/0.42 inference(transitivity,[status(thm)],[278, 277, 273, 50, 60])).
% 0.19/0.42 tff(280,plain,
% 0.19/0.42 (store(store(a_418, i0, e_419), i3, select(a_422, i2)) = store(store(a1, i1, select(a1, i1)), i3, select(a_422, i2))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[279])).
% 0.19/0.42 tff(281,plain,
% 0.19/0.42 (store(store(a1, i1, select(a1, i1)), i3, select(a_422, i2)) = store(store(a_418, i0, e_419), i3, select(a_422, i2))),
% 0.19/0.42 inference(symmetry,[status(thm)],[280])).
% 0.19/0.42 tff(282,plain,
% 0.19/0.42 (store(store(a1, i1, e_416), i0, select(a_418, i3)) = store(a_418, i0, e_419)),
% 0.19/0.42 inference(symmetry,[status(thm)],[278])).
% 0.19/0.42 tff(283,plain,
% 0.19/0.42 (store(store(a_417, i1, e_416), i3, select(store(a_417, i1, e_416), i3)) = store(store(a1, i1, e_416), i0, select(a_418, i3))),
% 0.19/0.42 inference(symmetry,[status(thm)],[277])).
% 0.19/0.42 tff(284,plain,
% 0.19/0.42 (store(a_417, i1, e_416) = store(store(a_417, i1, e_416), i3, select(store(a_417, i1, e_416), i3))),
% 0.19/0.42 inference(symmetry,[status(thm)],[273])).
% 0.19/0.42 tff(285,plain,
% 0.19/0.42 ((~![I: $i, A: $i] : (store(A, I, select(A, I)) = A)) | (store(store(a_417, i1, e_416), i0, select(store(a_417, i1, e_416), i0)) = store(a_417, i1, e_416))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(286,plain,
% 0.19/0.42 (store(store(a_417, i1, e_416), i0, select(store(a_417, i1, e_416), i0)) = store(a_417, i1, e_416)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[285, 243])).
% 0.19/0.42 tff(287,plain,
% 0.19/0.42 (select(store(a_417, i1, e_416), i0) = select(a_418, i0)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[41])).
% 0.19/0.42 tff(288,plain,
% 0.19/0.42 (select(a_418, i0) = select(store(a_417, i1, e_416), i0)),
% 0.19/0.42 inference(symmetry,[status(thm)],[287])).
% 0.19/0.42 tff(289,plain,
% 0.19/0.42 (store(store(a1, i1, e_416), i3, select(a_418, i0)) = store(store(a_417, i1, e_416), i0, select(store(a_417, i1, e_416), i0))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[276, 258, 288])).
% 0.19/0.42 tff(290,plain,
% 0.19/0.42 (a_420 = store(a1, i1, e_416)),
% 0.19/0.42 inference(transitivity,[status(thm)],[19, 278, 277, 273, 50, 60, 260])).
% 0.19/0.42 tff(291,plain,
% 0.19/0.42 (store(a_420, i3, e_421) = store(store(a1, i1, e_416), i3, select(a_418, i0))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[290, 15])).
% 0.19/0.42 tff(292,plain,
% 0.19/0.42 (a_422 = store(a_418, i0, e_419)),
% 0.19/0.42 inference(transitivity,[status(thm)],[25, 291, 289, 286, 284, 283, 282])).
% 0.19/0.42 tff(293,plain,
% 0.19/0.42 (select(a_422, i2) = select(store(a_418, i0, e_419), i2)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[292])).
% 0.19/0.42 tff(294,plain,
% 0.19/0.42 (select(store(a_418, i0, e_419), i2) = select(a_422, i2)),
% 0.19/0.42 inference(symmetry,[status(thm)],[293])).
% 0.19/0.42 tff(295,plain,
% 0.19/0.42 (store(a_418, i3, e_421) = store(store(a1, i1, e_416), i3, select(a_418, i0))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[261, 15])).
% 0.19/0.42 tff(296,plain,
% 0.19/0.42 ((~![I: $i, A: $i] : (store(A, I, select(A, I)) = A)) | (store(store(a_418, i3, e_421), i3, select(store(a_418, i3, e_421), i3)) = store(a_418, i3, e_421))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(297,plain,
% 0.19/0.42 (store(store(a_418, i3, e_421), i3, select(store(a_418, i3, e_421), i3)) = store(a_418, i3, e_421)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[296, 243])).
% 0.19/0.42 tff(298,plain,
% 0.19/0.42 (e_419 = select(store(a_418, i3, e_421), i3)),
% 0.19/0.42 inference(transitivity,[status(thm)],[83, 262, 259, 63, 196, 195])).
% 0.19/0.42 tff(299,plain,
% 0.19/0.42 (store(a_431, i0, e_419) = store(store(a_418, i3, e_421), i3, select(store(a_418, i3, e_421), i3))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[87, 257, 298])).
% 0.19/0.42 tff(300,plain,
% 0.19/0.42 (a_432 = store(a_418, i0, e_419)),
% 0.19/0.42 inference(transitivity,[status(thm)],[93, 299, 297, 295, 289, 286, 284, 283, 282])).
% 0.19/0.42 tff(301,plain,
% 0.19/0.42 (select(a_432, i2) = select(store(a_418, i0, e_419), i2)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[300])).
% 0.19/0.42 tff(302,plain,
% 0.19/0.42 (select(a_432, i2) = select(a_422, i2)),
% 0.19/0.42 inference(transitivity,[status(thm)],[301, 294])).
% 0.19/0.42 tff(303,plain,
% 0.19/0.42 (store(a_418, i3, e_421) = store(a1, i1, select(a1, i1))),
% 0.19/0.42 inference(transitivity,[status(thm)],[295, 289, 286, 50, 60])).
% 0.19/0.42 tff(304,plain,
% 0.19/0.42 (store(store(a_418, i3, e_421), i3, select(a_432, i2)) = store(store(a1, i1, select(a1, i1)), i3, select(a_422, i2))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[303, 302])).
% 0.19/0.42 tff(305,plain,
% 0.19/0.42 (a_432 = store(a_418, i3, e_421)),
% 0.19/0.42 inference(transitivity,[status(thm)],[93, 299, 297])).
% 0.19/0.42 tff(306,plain,
% 0.19/0.42 (store(a_432, i3, e_433) = store(store(a_418, i3, e_421), i3, select(a_432, i2))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[305, 132])).
% 0.19/0.42 tff(307,plain,
% 0.19/0.42 (a_434 = a_424),
% 0.19/0.42 inference(transitivity,[status(thm)],[142, 306, 304, 281, 271, 268, 103])).
% 0.19/0.42 tff(308,plain,
% 0.19/0.42 (store(a_434, i2, e_435) = store(a_424, i2, e_425)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[307, 266])).
% 0.19/0.42 tff(309,plain,
% 0.19/0.42 (a_436 = a_426),
% 0.19/0.42 inference(transitivity,[status(thm)],[147, 308, 8])).
% 0.19/0.42 tff(310,plain,
% 0.19/0.43 (select(a_436, i0) = select(a_426, i0)),
% 0.19/0.43 inference(monotonicity,[status(thm)],[309])).
% 0.19/0.43 tff(311,plain,
% 0.19/0.43 (e_439 = select(a_426, i0)),
% 0.19/0.43 inference(transitivity,[status(thm)],[152, 310])).
% 0.19/0.43 tff(312,plain,
% 0.19/0.43 (e_437 = select(a_426, i2)),
% 0.19/0.43 inference(transitivity,[status(thm)],[172, 169, 163, 265, 264, 262, 259, 63, 37, 28, 161, 158])).
% 0.19/0.43 tff(313,plain,
% 0.19/0.43 (a_436 = store(a_424, i2, e_425)),
% 0.19/0.43 inference(transitivity,[status(thm)],[147, 308])).
% 0.19/0.43 tff(314,plain,
% 0.19/0.43 (store(a_436, i0, e_437) = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[313, 312])).
% 0.19/0.43 tff(315,plain,
% 0.19/0.43 (a_438 = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.19/0.43 inference(transitivity,[status(thm)],[178, 314])).
% 0.19/0.43 tff(316,plain,
% 0.19/0.43 (store(a_438, i2, e_439) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[315, 311])).
% 0.19/0.43 tff(317,plain,
% 0.19/0.43 (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(a_438, i2, e_439)),
% 0.19/0.43 inference(symmetry,[status(thm)],[316])).
% 0.19/0.43 tff(318,plain,
% 0.19/0.43 (select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i0) = select(a_432, i3)),
% 0.19/0.43 inference(symmetry,[status(thm)],[265])).
% 0.19/0.43 tff(319,plain,
% 0.19/0.43 (select(a_418, i3) = select(store(store(a_418, i3, e_421), i0, select(a_418, i3)), i0)),
% 0.19/0.43 inference(symmetry,[status(thm)],[264])).
% 0.19/0.43 tff(320,plain,
% 0.19/0.43 (select(store(a1, i1, e_416), i3) = select(a_418, i3)),
% 0.19/0.43 inference(symmetry,[status(thm)],[262])).
% 0.19/0.43 tff(321,plain,
% 0.19/0.43 (select(store(a1, i1, e_416), i0) = select(store(a1, i1, e_416), i3)),
% 0.19/0.43 inference(symmetry,[status(thm)],[259])).
% 0.19/0.43 tff(322,plain,
% 0.19/0.43 (select(a_418, i0) = select(store(a1, i1, e_416), i0)),
% 0.19/0.43 inference(symmetry,[status(thm)],[63])).
% 0.19/0.43 tff(323,plain,
% 0.19/0.43 (a_440 = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.19/0.43 inference(transitivity,[status(thm)],[3, 316])).
% 0.19/0.43 tff(324,plain,
% 0.19/0.43 ((a_430 = a_440) <=> (store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[218, 323])).
% 0.19/0.43 tff(325,plain,
% 0.19/0.43 ((a_430 = a_440) <=> (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.19/0.43 inference(transitivity,[status(thm)],[324, 197])).
% 0.19/0.43 tff(326,plain,
% 0.19/0.43 ((~(a_430 = a_440)) <=> (~(store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2))))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[325])).
% 0.19/0.43 tff(327,plain,
% 0.19/0.43 (~(store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(store(a_424, i2, e_425), i2, select(a_426, i0)), i0, select(a_426, i2)))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[224, 326])).
% 0.19/0.43 tff(328,plain,
% 0.19/0.43 (i0 = i2),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[229, 327])).
% 0.19/0.43 tff(329,plain,
% 0.19/0.43 (select(a_426, i0) = select(a_426, i2)),
% 0.19/0.43 inference(monotonicity,[status(thm)],[328])).
% 0.19/0.43 tff(330,plain,
% 0.19/0.43 (select(a_426, i0) = select(store(a_436, i0, e_437), i0)),
% 0.19/0.43 inference(transitivity,[status(thm)],[329, 157, 160, 27, 36, 322, 321, 320, 319, 318, 192, 191, 190, 187])).
% 0.19/0.43 tff(331,plain,
% 0.19/0.43 (i2 = i0),
% 0.19/0.43 inference(symmetry,[status(thm)],[328])).
% 0.19/0.43 tff(332,plain,
% 0.19/0.43 (store(store(a_424, i2, e_425), i0, select(a_426, i2)) = store(a_436, i0, e_437)),
% 0.19/0.43 inference(symmetry,[status(thm)],[314])).
% 0.19/0.43 tff(333,plain,
% 0.19/0.43 (store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0)) = store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[332, 331, 330])).
% 0.19/0.43 tff(334,plain,
% 0.19/0.43 (store(store(a_436, i0, e_437), i0, select(store(a_436, i0, e_437), i0)) = store(store(store(a_424, i2, e_425), i0, select(a_426, i2)), i2, select(a_426, i0))),
% 0.19/0.43 inference(symmetry,[status(thm)],[333])).
% 0.19/0.43 tff(335,plain,
% 0.19/0.43 (store(a_426, i2, e_427) = store(store(a_424, i2, e_425), i0, select(store(a_424, i2, e_425), i0))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[7, 331, 251])).
% 0.19/0.43 tff(336,plain,
% 0.19/0.43 (a_428 = store(a_424, i2, e_425)),
% 0.19/0.43 inference(transitivity,[status(thm)],[205, 335, 248])).
% 0.19/0.43 tff(337,plain,
% 0.19/0.43 (store(a_428, i0, e_429) = store(store(a_424, i2, e_425), i0, select(a_426, i2))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[336, 201])).
% 0.19/0.43 tff(338,plain,
% 0.19/0.43 (a_430 = a_440),
% 0.19/0.43 inference(transitivity,[status(thm)],[217, 337, 332, 246, 334, 317, 4])).
% 0.19/0.43 tff(339,plain,
% 0.19/0.43 ($false),
% 0.19/0.43 inference(unit_resolution,[status(thm)],[224, 338])).
% 0.19/0.43 % SZS output end Proof
% 0.19/0.43 % E exiting
%------------------------------------------------------------------------------