%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV543-1.007 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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:52 AM UTC 2025
% Result : Unsatisfiable 0.19s 0.37s
% Output : Proof 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 103
% Syntax : Number of formulae : 284 ( 229 unt; 0 typ; 0 def)
% Number of atoms : 341 ( 339 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 65 ( 9 ~; 5 |; 0 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 66 ( 63 !; 0 ?; 66 :)
% Comments :
%------------------------------------------------------------------------------
tff(a_829_type,type,
a_829: $i ).
tff(a_808_type,type,
a_808: $i ).
tff(store_type,type,
store: ( $i * $i * $i ) > $i ).
tff(e_828_type,type,
e_828: $i ).
tff(i2_type,type,
i2: $i ).
tff(a_827_type,type,
a_827: $i ).
tff(e_807_type,type,
e_807: $i ).
tff(a_806_type,type,
a_806: $i ).
tff(select_type,type,
select: ( $i * $i ) > $i ).
tff(i5_type,type,
i5: $i ).
tff(a_804_type,type,
a_804: $i ).
tff(a_825_type,type,
a_825: $i ).
tff(e_803_type,type,
e_803: $i ).
tff(a_802_type,type,
a_802: $i ).
tff(e_824_type,type,
e_824: $i ).
tff(a_823_type,type,
a_823: $i ).
tff(a_800_type,type,
a_800: $i ).
tff(a_821_type,type,
a_821: $i ).
tff(e_798_type,type,
e_798: $i ).
tff(i1_type,type,
i1: $i ).
tff(a_799_type,type,
a_799: $i ).
tff(e_819_type,type,
e_819: $i ).
tff(a_820_type,type,
a_820: $i ).
tff(a_797_type,type,
a_797: $i ).
tff(a_818_type,type,
a_818: $i ).
tff(e_796_type,type,
e_796: $i ).
tff(a_795_type,type,
a_795: $i ).
tff(e_813_type,type,
e_813: $i ).
tff(i0_type,type,
i0: $i ).
tff(a_812_type,type,
a_812: $i ).
tff(a_793_type,type,
a_793: $i ).
tff(a_814_type,type,
a_814: $i ).
tff(e_788_type,type,
e_788: $i ).
tff(a_787_type,type,
a_787: $i ).
tff(a_810_type,type,
a_810: $i ).
tff(a_789_type,type,
a_789: $i ).
tff(e_784_type,type,
e_784: $i ).
tff(i3_type,type,
i3: $i ).
tff(a_783_type,type,
a_783: $i ).
tff(a_785_type,type,
a_785: $i ).
tff(e_786_type,type,
e_786: $i ).
tff(a_809_type,type,
a_809: $i ).
tff(e_811_type,type,
e_811: $i ).
tff(e_792_type,type,
e_792: $i ).
tff(a_791_type,type,
a_791: $i ).
tff(e_790_type,type,
e_790: $i ).
tff(e_794_type,type,
e_794: $i ).
tff(e_817_type,type,
e_817: $i ).
tff(a_816_type,type,
a_816: $i ).
tff(e_815_type,type,
e_815: $i ).
tff(e_801_type,type,
e_801: $i ).
tff(e_822_type,type,
e_822: $i ).
tff(e_805_type,type,
e_805: $i ).
tff(e_826_type,type,
e_826: $i ).
tff(1,plain,
( ( a_829 = store(a_827,i2,e_828) )
<=> ( a_829 = store(a_827,i2,e_828) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(2,axiom,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
tff(3,plain,
a_829 = store(a_827,i2,e_828),
inference(modus_ponens,[status(thm)],[2,1]) ).
tff(4,plain,
store(a_827,i2,e_828) = a_829,
inference(symmetry,[status(thm)],[3]) ).
tff(5,plain,
( ( e_807 = select(a_804,i5) )
<=> ( e_807 = select(a_804,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(6,axiom,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
tff(7,plain,
e_807 = select(a_804,i5),
inference(modus_ponens,[status(thm)],[6,5]) ).
tff(8,plain,
select(a_804,i5) = e_807,
inference(symmetry,[status(thm)],[7]) ).
tff(9,plain,
( ( a_804 = store(a_802,i2,e_803) )
<=> ( a_804 = store(a_802,i2,e_803) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(10,axiom,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
tff(11,plain,
a_804 = store(a_802,i2,e_803),
inference(modus_ponens,[status(thm)],[10,9]) ).
tff(12,plain,
store(a_802,i2,e_803) = a_804,
inference(symmetry,[status(thm)],[11]) ).
tff(13,plain,
( ( e_803 = select(a_800,i5) )
<=> ( e_803 = select(a_800,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(14,axiom,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
tff(15,plain,
e_803 = select(a_800,i5),
inference(modus_ponens,[status(thm)],[14,13]) ).
tff(16,plain,
select(a_800,i5) = e_803,
inference(symmetry,[status(thm)],[15]) ).
tff(17,plain,
( ( a_800 = store(a_799,i1,e_798) )
<=> ( a_800 = store(a_799,i1,e_798) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(18,axiom,
a_800 = store(a_799,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
tff(19,plain,
a_800 = store(a_799,i1,e_798),
inference(modus_ponens,[status(thm)],[18,17]) ).
tff(20,plain,
store(a_799,i1,e_798) = a_800,
inference(symmetry,[status(thm)],[19]) ).
tff(21,plain,
( ( e_798 = select(a_797,i1) )
<=> ( e_798 = select(a_797,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(22,axiom,
e_798 = select(a_797,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
tff(23,plain,
e_798 = select(a_797,i1),
inference(modus_ponens,[status(thm)],[22,21]) ).
tff(24,plain,
select(a_797,i1) = e_798,
inference(symmetry,[status(thm)],[23]) ).
tff(25,plain,
( ( a_797 = store(a_795,i5,e_796) )
<=> ( a_797 = store(a_795,i5,e_796) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(26,axiom,
a_797 = store(a_795,i5,e_796),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
tff(27,plain,
a_797 = store(a_795,i5,e_796),
inference(modus_ponens,[status(thm)],[26,25]) ).
tff(28,plain,
store(a_795,i5,e_796) = a_797,
inference(symmetry,[status(thm)],[27]) ).
tff(29,plain,
( ( e_796 = select(a_793,i2) )
<=> ( e_796 = select(a_793,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(30,axiom,
e_796 = select(a_793,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
tff(31,plain,
e_796 = select(a_793,i2),
inference(modus_ponens,[status(thm)],[30,29]) ).
tff(32,plain,
select(a_793,i2) = e_796,
inference(symmetry,[status(thm)],[31]) ).
tff(33,plain,
( ( a_814 = store(a_812,i0,e_813) )
<=> ( a_814 = store(a_812,i0,e_813) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(34,axiom,
a_814 = store(a_812,i0,e_813),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
tff(35,plain,
a_814 = store(a_812,i0,e_813),
inference(modus_ponens,[status(thm)],[34,33]) ).
tff(36,plain,
store(a_812,i0,e_813) = a_814,
inference(symmetry,[status(thm)],[35]) ).
tff(37,plain,
( ( e_813 = select(a_810,i5) )
<=> ( e_813 = select(a_810,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(38,axiom,
e_813 = select(a_810,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
tff(39,plain,
e_813 = select(a_810,i5),
inference(modus_ponens,[status(thm)],[38,37]) ).
tff(40,plain,
select(a_810,i5) = e_813,
inference(symmetry,[status(thm)],[39]) ).
tff(41,plain,
( ( a_789 = store(a_787,i1,e_788) )
<=> ( a_789 = store(a_787,i1,e_788) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(42,axiom,
a_789 = store(a_787,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
tff(43,plain,
a_789 = store(a_787,i1,e_788),
inference(modus_ponens,[status(thm)],[42,41]) ).
tff(44,plain,
store(a_787,i1,e_788) = a_789,
inference(symmetry,[status(thm)],[43]) ).
tff(45,plain,
( ( e_788 = select(a_785,i2) )
<=> ( e_788 = select(a_785,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(46,axiom,
e_788 = select(a_785,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
tff(47,plain,
e_788 = select(a_785,i2),
inference(modus_ponens,[status(thm)],[46,45]) ).
tff(48,plain,
select(a_785,i2) = e_788,
inference(symmetry,[status(thm)],[47]) ).
tff(49,plain,
( ( a_785 = store(a_783,i3,e_784) )
<=> ( a_785 = store(a_783,i3,e_784) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(50,axiom,
a_785 = store(a_783,i3,e_784),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
tff(51,plain,
a_785 = store(a_783,i3,e_784),
inference(modus_ponens,[status(thm)],[50,49]) ).
tff(52,plain,
store(a_783,i3,e_784) = a_785,
inference(symmetry,[status(thm)],[51]) ).
tff(53,plain,
select(store(a_783,i3,e_784),i2) = select(a_785,i2),
inference(monotonicity,[status(thm)],[52]) ).
tff(54,plain,
select(store(a_783,i3,e_784),i2) = e_788,
inference(transitivity,[status(thm)],[53,48]) ).
tff(55,plain,
( ( a_787 = store(a_785,i2,e_786) )
<=> ( a_787 = store(a_785,i2,e_786) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(56,axiom,
a_787 = store(a_785,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
tff(57,plain,
a_787 = store(a_785,i2,e_786),
inference(modus_ponens,[status(thm)],[56,55]) ).
tff(58,plain,
store(a_785,i2,e_786) = a_787,
inference(symmetry,[status(thm)],[57]) ).
tff(59,plain,
( ( e_786 = select(a_785,i1) )
<=> ( e_786 = select(a_785,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(60,axiom,
e_786 = select(a_785,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
tff(61,plain,
e_786 = select(a_785,i1),
inference(modus_ponens,[status(thm)],[60,59]) ).
tff(62,plain,
select(a_785,i1) = e_786,
inference(symmetry,[status(thm)],[61]) ).
tff(63,plain,
select(store(a_783,i3,e_784),i1) = select(a_785,i1),
inference(monotonicity,[status(thm)],[52]) ).
tff(64,plain,
select(store(a_783,i3,e_784),i1) = e_786,
inference(transitivity,[status(thm)],[63,62]) ).
tff(65,plain,
store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)) = store(a_785,i2,e_786),
inference(monotonicity,[status(thm)],[52,64]) ).
tff(66,plain,
store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)) = a_787,
inference(transitivity,[status(thm)],[65,58]) ).
tff(67,plain,
store(store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)),i1,select(store(a_783,i3,e_784),i2)) = store(a_787,i1,e_788),
inference(monotonicity,[status(thm)],[66,54]) ).
tff(68,plain,
^ [I: $i,A: $i,J: $i] :
refl(( ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
<=> ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ) )),
inference(bind,[status(th)],[]) ).
tff(69,plain,
( ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
<=> ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ) ),
inference(quant_intro,[status(thm)],[68]) ).
tff(70,plain,
( ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
<=> ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(71,axiom,
! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
tff(72,plain,
! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ),
inference(modus_ponens,[status(thm)],[71,70]) ).
tff(73,plain,
! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ),
inference(skolemize,[status(sab)],[72]) ).
tff(74,plain,
! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ),
inference(modus_ponens,[status(thm)],[73,69]) ).
tff(75,plain,
( ~ ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
| ( store(store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)),i1,select(store(a_783,i3,e_784),i2)) = store(store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),i2,select(store(a_783,i3,e_784),i1)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(76,plain,
store(store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)),i1,select(store(a_783,i3,e_784),i2)) = store(store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),i2,select(store(a_783,i3,e_784),i1)),
inference(unit_resolution,[status(thm)],[75,74]) ).
tff(77,plain,
store(store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),i2,select(store(a_783,i3,e_784),i1)) = store(store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)),i1,select(store(a_783,i3,e_784),i2)),
inference(symmetry,[status(thm)],[76]) ).
tff(78,plain,
select(a_785,i1) = select(store(a_783,i3,e_784),i1),
inference(symmetry,[status(thm)],[63]) ).
tff(79,plain,
e_786 = select(store(a_783,i3,e_784),i1),
inference(transitivity,[status(thm)],[61,78]) ).
tff(80,plain,
store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)) = store(a_785,i1,e_788),
inference(monotonicity,[status(thm)],[52,54]) ).
tff(81,plain,
store(a_785,i1,e_788) = store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),
inference(symmetry,[status(thm)],[80]) ).
tff(82,plain,
( ( a_809 = store(a_785,i1,e_788) )
<=> ( a_809 = store(a_785,i1,e_788) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(83,axiom,
a_809 = store(a_785,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
tff(84,plain,
a_809 = store(a_785,i1,e_788),
inference(modus_ponens,[status(thm)],[83,82]) ).
tff(85,plain,
a_809 = store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),
inference(transitivity,[status(thm)],[84,81]) ).
tff(86,plain,
store(a_809,i2,e_786) = store(store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),i2,select(store(a_783,i3,e_784),i1)),
inference(monotonicity,[status(thm)],[85,79]) ).
tff(87,plain,
( ( a_810 = store(a_809,i2,e_786) )
<=> ( a_810 = store(a_809,i2,e_786) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(88,axiom,
a_810 = store(a_809,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
tff(89,plain,
a_810 = store(a_809,i2,e_786),
inference(modus_ponens,[status(thm)],[88,87]) ).
tff(90,plain,
a_810 = a_789,
inference(transitivity,[status(thm)],[89,86,77,67,44]) ).
tff(91,plain,
select(a_810,i5) = select(a_789,i5),
inference(monotonicity,[status(thm)],[90]) ).
tff(92,plain,
select(a_789,i5) = select(a_810,i5),
inference(symmetry,[status(thm)],[91]) ).
tff(93,plain,
select(store(a_787,i1,e_788),i5) = select(a_789,i5),
inference(monotonicity,[status(thm)],[44]) ).
tff(94,plain,
select(store(a_787,i1,e_788),i5) = e_813,
inference(transitivity,[status(thm)],[93,92,40]) ).
tff(95,plain,
( ( a_812 = store(a_810,i5,e_811) )
<=> ( a_812 = store(a_810,i5,e_811) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(96,axiom,
a_812 = store(a_810,i5,e_811),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
tff(97,plain,
a_812 = store(a_810,i5,e_811),
inference(modus_ponens,[status(thm)],[96,95]) ).
tff(98,plain,
store(a_810,i5,e_811) = a_812,
inference(symmetry,[status(thm)],[97]) ).
tff(99,plain,
( ( e_811 = select(a_810,i0) )
<=> ( e_811 = select(a_810,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(100,axiom,
e_811 = select(a_810,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
tff(101,plain,
e_811 = select(a_810,i0),
inference(modus_ponens,[status(thm)],[100,99]) ).
tff(102,plain,
select(a_810,i0) = e_811,
inference(symmetry,[status(thm)],[101]) ).
tff(103,plain,
select(a_810,i0) = select(a_789,i0),
inference(monotonicity,[status(thm)],[90]) ).
tff(104,plain,
select(a_789,i0) = select(a_810,i0),
inference(symmetry,[status(thm)],[103]) ).
tff(105,plain,
select(store(a_787,i1,e_788),i0) = select(a_789,i0),
inference(monotonicity,[status(thm)],[44]) ).
tff(106,plain,
select(store(a_787,i1,e_788),i0) = e_811,
inference(transitivity,[status(thm)],[105,104,102]) ).
tff(107,plain,
store(a_809,i2,e_786) = a_810,
inference(symmetry,[status(thm)],[89]) ).
tff(108,plain,
store(store(store(a_783,i3,e_784),i1,select(store(a_783,i3,e_784),i2)),i2,select(store(a_783,i3,e_784),i1)) = store(a_809,i2,e_786),
inference(symmetry,[status(thm)],[86]) ).
tff(109,plain,
store(a_787,i1,e_788) = store(store(store(a_783,i3,e_784),i2,select(store(a_783,i3,e_784),i1)),i1,select(store(a_783,i3,e_784),i2)),
inference(symmetry,[status(thm)],[67]) ).
tff(110,plain,
store(a_787,i1,e_788) = a_810,
inference(transitivity,[status(thm)],[109,76,108,107]) ).
tff(111,plain,
store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)) = store(a_810,i5,e_811),
inference(monotonicity,[status(thm)],[110,106]) ).
tff(112,plain,
store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)) = a_812,
inference(transitivity,[status(thm)],[111,98]) ).
tff(113,plain,
store(store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)),i0,select(store(a_787,i1,e_788),i5)) = store(a_812,i0,e_813),
inference(monotonicity,[status(thm)],[112,94]) ).
tff(114,plain,
( ~ ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
| ( store(store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),i5,select(store(a_787,i1,e_788),i0)) = store(store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)),i0,select(store(a_787,i1,e_788),i5)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(115,plain,
store(store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),i5,select(store(a_787,i1,e_788),i0)) = store(store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)),i0,select(store(a_787,i1,e_788),i5)),
inference(unit_resolution,[status(thm)],[114,74]) ).
tff(116,plain,
select(a_789,i0) = select(store(a_787,i1,e_788),i0),
inference(symmetry,[status(thm)],[105]) ).
tff(117,plain,
( ( e_792 = select(a_789,i0) )
<=> ( e_792 = select(a_789,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(118,axiom,
e_792 = select(a_789,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
tff(119,plain,
e_792 = select(a_789,i0),
inference(modus_ponens,[status(thm)],[118,117]) ).
tff(120,plain,
e_792 = select(store(a_787,i1,e_788),i0),
inference(transitivity,[status(thm)],[119,116]) ).
tff(121,plain,
( ( e_790 = select(a_789,i5) )
<=> ( e_790 = select(a_789,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(122,axiom,
e_790 = select(a_789,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
tff(123,plain,
e_790 = select(a_789,i5),
inference(modus_ponens,[status(thm)],[122,121]) ).
tff(124,plain,
select(a_789,i5) = e_790,
inference(symmetry,[status(thm)],[123]) ).
tff(125,plain,
select(store(a_787,i1,e_788),i5) = e_790,
inference(transitivity,[status(thm)],[93,124]) ).
tff(126,plain,
store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)) = store(a_789,i0,e_790),
inference(monotonicity,[status(thm)],[44,125]) ).
tff(127,plain,
store(a_789,i0,e_790) = store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),
inference(symmetry,[status(thm)],[126]) ).
tff(128,plain,
( ( a_791 = store(a_789,i0,e_790) )
<=> ( a_791 = store(a_789,i0,e_790) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(129,axiom,
a_791 = store(a_789,i0,e_790),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
tff(130,plain,
a_791 = store(a_789,i0,e_790),
inference(modus_ponens,[status(thm)],[129,128]) ).
tff(131,plain,
a_791 = store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),
inference(transitivity,[status(thm)],[130,127]) ).
tff(132,plain,
store(a_791,i5,e_792) = store(store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),i5,select(store(a_787,i1,e_788),i0)),
inference(monotonicity,[status(thm)],[131,120]) ).
tff(133,plain,
( ( a_793 = store(a_791,i5,e_792) )
<=> ( a_793 = store(a_791,i5,e_792) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(134,axiom,
a_793 = store(a_791,i5,e_792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
tff(135,plain,
a_793 = store(a_791,i5,e_792),
inference(modus_ponens,[status(thm)],[134,133]) ).
tff(136,plain,
a_793 = a_814,
inference(transitivity,[status(thm)],[135,132,115,113,36]) ).
tff(137,plain,
select(a_793,i2) = select(a_814,i2),
inference(monotonicity,[status(thm)],[136]) ).
tff(138,plain,
select(a_814,i2) = select(a_793,i2),
inference(symmetry,[status(thm)],[137]) ).
tff(139,plain,
select(store(a_812,i0,e_813),i2) = select(a_814,i2),
inference(monotonicity,[status(thm)],[36]) ).
tff(140,plain,
select(store(a_812,i0,e_813),i2) = e_796,
inference(transitivity,[status(thm)],[139,138,32]) ).
tff(141,plain,
( ( a_795 = store(a_793,i2,e_794) )
<=> ( a_795 = store(a_793,i2,e_794) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(142,axiom,
a_795 = store(a_793,i2,e_794),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
tff(143,plain,
a_795 = store(a_793,i2,e_794),
inference(modus_ponens,[status(thm)],[142,141]) ).
tff(144,plain,
store(a_793,i2,e_794) = a_795,
inference(symmetry,[status(thm)],[143]) ).
tff(145,plain,
( ( e_794 = select(a_793,i5) )
<=> ( e_794 = select(a_793,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(146,axiom,
e_794 = select(a_793,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
tff(147,plain,
e_794 = select(a_793,i5),
inference(modus_ponens,[status(thm)],[146,145]) ).
tff(148,plain,
select(a_793,i5) = e_794,
inference(symmetry,[status(thm)],[147]) ).
tff(149,plain,
store(a_791,i5,e_792) = a_793,
inference(symmetry,[status(thm)],[135]) ).
tff(150,plain,
store(store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),i5,select(store(a_787,i1,e_788),i0)) = store(a_791,i5,e_792),
inference(symmetry,[status(thm)],[132]) ).
tff(151,plain,
store(store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)),i0,select(store(a_787,i1,e_788),i5)) = store(store(store(a_787,i1,e_788),i0,select(store(a_787,i1,e_788),i5)),i5,select(store(a_787,i1,e_788),i0)),
inference(symmetry,[status(thm)],[115]) ).
tff(152,plain,
store(a_812,i0,e_813) = store(store(store(a_787,i1,e_788),i5,select(store(a_787,i1,e_788),i0)),i0,select(store(a_787,i1,e_788),i5)),
inference(symmetry,[status(thm)],[113]) ).
tff(153,plain,
a_814 = a_793,
inference(transitivity,[status(thm)],[35,152,151,150,149]) ).
tff(154,plain,
select(a_814,i5) = select(a_793,i5),
inference(monotonicity,[status(thm)],[153]) ).
tff(155,plain,
select(store(a_812,i0,e_813),i5) = select(a_814,i5),
inference(monotonicity,[status(thm)],[36]) ).
tff(156,plain,
select(store(a_812,i0,e_813),i5) = e_794,
inference(transitivity,[status(thm)],[155,154,148]) ).
tff(157,plain,
store(a_812,i0,e_813) = a_793,
inference(transitivity,[status(thm)],[152,151,150,149]) ).
tff(158,plain,
store(store(a_812,i0,e_813),i2,select(store(a_812,i0,e_813),i5)) = store(a_793,i2,e_794),
inference(monotonicity,[status(thm)],[157,156]) ).
tff(159,plain,
store(store(a_812,i0,e_813),i2,select(store(a_812,i0,e_813),i5)) = a_795,
inference(transitivity,[status(thm)],[158,144]) ).
tff(160,plain,
store(store(store(a_812,i0,e_813),i2,select(store(a_812,i0,e_813),i5)),i5,select(store(a_812,i0,e_813),i2)) = store(a_795,i5,e_796),
inference(monotonicity,[status(thm)],[159,140]) ).
tff(161,plain,
( ~ ! [I: $i,A: $i,J: $i] : ( store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) )
| ( store(store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)),i2,select(store(a_812,i0,e_813),i5)) = store(store(store(a_812,i0,e_813),i2,select(store(a_812,i0,e_813),i5)),i5,select(store(a_812,i0,e_813),i2)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(162,plain,
store(store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)),i2,select(store(a_812,i0,e_813),i5)) = store(store(store(a_812,i0,e_813),i2,select(store(a_812,i0,e_813),i5)),i5,select(store(a_812,i0,e_813),i2)),
inference(unit_resolution,[status(thm)],[161,74]) ).
tff(163,plain,
select(a_814,i5) = select(store(a_812,i0,e_813),i5),
inference(symmetry,[status(thm)],[155]) ).
tff(164,plain,
( ( e_817 = select(a_814,i5) )
<=> ( e_817 = select(a_814,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(165,axiom,
e_817 = select(a_814,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
tff(166,plain,
e_817 = select(a_814,i5),
inference(modus_ponens,[status(thm)],[165,164]) ).
tff(167,plain,
e_817 = select(store(a_812,i0,e_813),i5),
inference(transitivity,[status(thm)],[166,163]) ).
tff(168,plain,
( ( e_815 = select(a_814,i2) )
<=> ( e_815 = select(a_814,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(169,axiom,
e_815 = select(a_814,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
tff(170,plain,
e_815 = select(a_814,i2),
inference(modus_ponens,[status(thm)],[169,168]) ).
tff(171,plain,
select(a_814,i2) = e_815,
inference(symmetry,[status(thm)],[170]) ).
tff(172,plain,
select(store(a_812,i0,e_813),i2) = e_815,
inference(transitivity,[status(thm)],[139,171]) ).
tff(173,plain,
store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)) = store(a_814,i5,e_815),
inference(monotonicity,[status(thm)],[36,172]) ).
tff(174,plain,
store(a_814,i5,e_815) = store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)),
inference(symmetry,[status(thm)],[173]) ).
tff(175,plain,
( ( a_816 = store(a_814,i5,e_815) )
<=> ( a_816 = store(a_814,i5,e_815) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(176,axiom,
a_816 = store(a_814,i5,e_815),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
tff(177,plain,
a_816 = store(a_814,i5,e_815),
inference(modus_ponens,[status(thm)],[176,175]) ).
tff(178,plain,
a_816 = store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)),
inference(transitivity,[status(thm)],[177,174]) ).
tff(179,plain,
store(a_816,i2,e_817) = store(store(store(a_812,i0,e_813),i5,select(store(a_812,i0,e_813),i2)),i2,select(store(a_812,i0,e_813),i5)),
inference(monotonicity,[status(thm)],[178,167]) ).
tff(180,plain,
( ( a_818 = store(a_816,i2,e_817) )
<=> ( a_818 = store(a_816,i2,e_817) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(181,axiom,
a_818 = store(a_816,i2,e_817),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
tff(182,plain,
a_818 = store(a_816,i2,e_817),
inference(modus_ponens,[status(thm)],[181,180]) ).
tff(183,plain,
a_818 = a_797,
inference(transitivity,[status(thm)],[182,179,162,160,28]) ).
tff(184,plain,
select(a_818,i1) = select(a_797,i1),
inference(monotonicity,[status(thm)],[183]) ).
tff(185,plain,
( ( e_819 = select(a_818,i1) )
<=> ( e_819 = select(a_818,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(186,axiom,
e_819 = select(a_818,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
tff(187,plain,
e_819 = select(a_818,i1),
inference(modus_ponens,[status(thm)],[186,185]) ).
tff(188,plain,
e_819 = e_798,
inference(transitivity,[status(thm)],[187,184,24]) ).
tff(189,plain,
( ( a_799 = store(a_797,i1,e_798) )
<=> ( a_799 = store(a_797,i1,e_798) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(190,axiom,
a_799 = store(a_797,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
tff(191,plain,
a_799 = store(a_797,i1,e_798),
inference(modus_ponens,[status(thm)],[190,189]) ).
tff(192,plain,
store(a_797,i1,e_798) = a_799,
inference(symmetry,[status(thm)],[191]) ).
tff(193,plain,
store(a_818,i1,e_819) = store(a_797,i1,e_798),
inference(monotonicity,[status(thm)],[183,188]) ).
tff(194,plain,
( ( a_820 = store(a_818,i1,e_819) )
<=> ( a_820 = store(a_818,i1,e_819) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(195,axiom,
a_820 = store(a_818,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
tff(196,plain,
a_820 = store(a_818,i1,e_819),
inference(modus_ponens,[status(thm)],[195,194]) ).
tff(197,plain,
a_820 = a_799,
inference(transitivity,[status(thm)],[196,193,192]) ).
tff(198,plain,
store(a_820,i1,e_819) = store(a_799,i1,e_798),
inference(monotonicity,[status(thm)],[197,188]) ).
tff(199,plain,
( ( a_821 = store(a_820,i1,e_819) )
<=> ( a_821 = store(a_820,i1,e_819) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(200,axiom,
a_821 = store(a_820,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
tff(201,plain,
a_821 = store(a_820,i1,e_819),
inference(modus_ponens,[status(thm)],[200,199]) ).
tff(202,plain,
a_821 = a_800,
inference(transitivity,[status(thm)],[201,198,20]) ).
tff(203,plain,
select(a_821,i5) = select(a_800,i5),
inference(monotonicity,[status(thm)],[202]) ).
tff(204,plain,
( ( e_824 = select(a_821,i5) )
<=> ( e_824 = select(a_821,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(205,axiom,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
tff(206,plain,
e_824 = select(a_821,i5),
inference(modus_ponens,[status(thm)],[205,204]) ).
tff(207,plain,
e_824 = e_803,
inference(transitivity,[status(thm)],[206,203,16]) ).
tff(208,plain,
( ( a_802 = store(a_800,i5,e_801) )
<=> ( a_802 = store(a_800,i5,e_801) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(209,axiom,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
tff(210,plain,
a_802 = store(a_800,i5,e_801),
inference(modus_ponens,[status(thm)],[209,208]) ).
tff(211,plain,
store(a_800,i5,e_801) = a_802,
inference(symmetry,[status(thm)],[210]) ).
tff(212,plain,
( ( e_801 = select(a_800,i2) )
<=> ( e_801 = select(a_800,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(213,axiom,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
tff(214,plain,
e_801 = select(a_800,i2),
inference(modus_ponens,[status(thm)],[213,212]) ).
tff(215,plain,
select(a_800,i2) = e_801,
inference(symmetry,[status(thm)],[214]) ).
tff(216,plain,
select(a_821,i2) = select(a_800,i2),
inference(monotonicity,[status(thm)],[202]) ).
tff(217,plain,
( ( e_822 = select(a_821,i2) )
<=> ( e_822 = select(a_821,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(218,axiom,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
tff(219,plain,
e_822 = select(a_821,i2),
inference(modus_ponens,[status(thm)],[218,217]) ).
tff(220,plain,
e_822 = e_801,
inference(transitivity,[status(thm)],[219,216,215]) ).
tff(221,plain,
store(a_821,i5,e_822) = store(a_800,i5,e_801),
inference(monotonicity,[status(thm)],[202,220]) ).
tff(222,plain,
( ( a_823 = store(a_821,i5,e_822) )
<=> ( a_823 = store(a_821,i5,e_822) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(223,axiom,
a_823 = store(a_821,i5,e_822),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
tff(224,plain,
a_823 = store(a_821,i5,e_822),
inference(modus_ponens,[status(thm)],[223,222]) ).
tff(225,plain,
a_823 = a_802,
inference(transitivity,[status(thm)],[224,221,211]) ).
tff(226,plain,
store(a_823,i2,e_824) = store(a_802,i2,e_803),
inference(monotonicity,[status(thm)],[225,207]) ).
tff(227,plain,
( ( a_825 = store(a_823,i2,e_824) )
<=> ( a_825 = store(a_823,i2,e_824) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(228,axiom,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
tff(229,plain,
a_825 = store(a_823,i2,e_824),
inference(modus_ponens,[status(thm)],[228,227]) ).
tff(230,plain,
a_825 = a_804,
inference(transitivity,[status(thm)],[229,226,12]) ).
tff(231,plain,
select(a_825,i5) = select(a_804,i5),
inference(monotonicity,[status(thm)],[230]) ).
tff(232,plain,
( ( e_828 = select(a_825,i5) )
<=> ( e_828 = select(a_825,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(233,axiom,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
tff(234,plain,
e_828 = select(a_825,i5),
inference(modus_ponens,[status(thm)],[233,232]) ).
tff(235,plain,
e_828 = e_807,
inference(transitivity,[status(thm)],[234,231,8]) ).
tff(236,plain,
( ( a_806 = store(a_804,i5,e_805) )
<=> ( a_806 = store(a_804,i5,e_805) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(237,axiom,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
tff(238,plain,
a_806 = store(a_804,i5,e_805),
inference(modus_ponens,[status(thm)],[237,236]) ).
tff(239,plain,
store(a_804,i5,e_805) = a_806,
inference(symmetry,[status(thm)],[238]) ).
tff(240,plain,
( ( e_805 = select(a_804,i2) )
<=> ( e_805 = select(a_804,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(241,axiom,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
tff(242,plain,
e_805 = select(a_804,i2),
inference(modus_ponens,[status(thm)],[241,240]) ).
tff(243,plain,
select(a_804,i2) = e_805,
inference(symmetry,[status(thm)],[242]) ).
tff(244,plain,
store(store(a_800,i5,e_801),i2,select(a_800,i5)) = store(a_802,i2,e_803),
inference(monotonicity,[status(thm)],[211,16]) ).
tff(245,plain,
store(a_802,i2,e_803) = store(store(a_800,i5,e_801),i2,select(a_800,i5)),
inference(symmetry,[status(thm)],[244]) ).
tff(246,plain,
a_804 = store(store(a_800,i5,e_801),i2,select(a_800,i5)),
inference(transitivity,[status(thm)],[11,245]) ).
tff(247,plain,
select(a_804,i2) = select(store(store(a_800,i5,e_801),i2,select(a_800,i5)),i2),
inference(monotonicity,[status(thm)],[246]) ).
tff(248,plain,
select(store(store(a_800,i5,e_801),i2,select(a_800,i5)),i2) = select(a_804,i2),
inference(symmetry,[status(thm)],[247]) ).
tff(249,plain,
( ! [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 ) ),
inference(rewrite,[status(thm)],[]) ).
tff(250,plain,
( ! [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 ) ),
inference(rewrite,[status(thm)],[]) ).
tff(251,axiom,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
tff(252,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(modus_ponens,[status(thm)],[251,250]) ).
tff(253,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(skolemize,[status(sab)],[252]) ).
tff(254,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(modus_ponens,[status(thm)],[253,249]) ).
tff(255,plain,
( ~ ! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E )
| ( select(store(store(a_800,i5,e_801),i2,select(a_800,i5)),i2) = select(a_800,i5) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(256,plain,
select(store(store(a_800,i5,e_801),i2,select(a_800,i5)),i2) = select(a_800,i5),
inference(unit_resolution,[status(thm)],[255,254]) ).
tff(257,plain,
select(a_800,i5) = select(store(store(a_800,i5,e_801),i2,select(a_800,i5)),i2),
inference(symmetry,[status(thm)],[256]) ).
tff(258,plain,
( ~ ! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E )
| ( select(store(store(a_821,i5,e_822),i2,select(a_821,i5)),i2) = select(a_821,i5) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(259,plain,
select(store(store(a_821,i5,e_822),i2,select(a_821,i5)),i2) = select(a_821,i5),
inference(unit_resolution,[status(thm)],[258,254]) ).
tff(260,plain,
select(a_821,i5) = e_824,
inference(symmetry,[status(thm)],[206]) ).
tff(261,plain,
store(a_821,i5,e_822) = a_823,
inference(symmetry,[status(thm)],[224]) ).
tff(262,plain,
store(store(a_821,i5,e_822),i2,select(a_821,i5)) = store(a_823,i2,e_824),
inference(monotonicity,[status(thm)],[261,260]) ).
tff(263,plain,
store(a_823,i2,e_824) = store(store(a_821,i5,e_822),i2,select(a_821,i5)),
inference(symmetry,[status(thm)],[262]) ).
tff(264,plain,
a_825 = store(store(a_821,i5,e_822),i2,select(a_821,i5)),
inference(transitivity,[status(thm)],[229,263]) ).
tff(265,plain,
select(a_825,i2) = select(store(store(a_821,i5,e_822),i2,select(a_821,i5)),i2),
inference(monotonicity,[status(thm)],[264]) ).
tff(266,plain,
( ( e_826 = select(a_825,i2) )
<=> ( e_826 = select(a_825,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(267,axiom,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
tff(268,plain,
e_826 = select(a_825,i2),
inference(modus_ponens,[status(thm)],[267,266]) ).
tff(269,plain,
e_826 = e_805,
inference(transitivity,[status(thm)],[268,265,259,203,257,248,243]) ).
tff(270,plain,
store(a_825,i5,e_826) = store(a_804,i5,e_805),
inference(monotonicity,[status(thm)],[230,269]) ).
tff(271,plain,
( ( a_827 = store(a_825,i5,e_826) )
<=> ( a_827 = store(a_825,i5,e_826) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(272,axiom,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
tff(273,plain,
a_827 = store(a_825,i5,e_826),
inference(modus_ponens,[status(thm)],[272,271]) ).
tff(274,plain,
a_827 = a_806,
inference(transitivity,[status(thm)],[273,270,239]) ).
tff(275,plain,
store(a_827,i2,e_828) = store(a_806,i2,e_807),
inference(monotonicity,[status(thm)],[274,235]) ).
tff(276,plain,
store(a_806,i2,e_807) = store(a_827,i2,e_828),
inference(symmetry,[status(thm)],[275]) ).
tff(277,plain,
( ( a_808 = store(a_806,i2,e_807) )
<=> ( a_808 = store(a_806,i2,e_807) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(278,axiom,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
tff(279,plain,
a_808 = store(a_806,i2,e_807),
inference(modus_ponens,[status(thm)],[278,277]) ).
tff(280,plain,
a_808 = a_829,
inference(transitivity,[status(thm)],[279,276,4]) ).
tff(281,plain,
( ( a_808 != a_829 )
<=> ( a_808 != a_829 ) ),
inference(rewrite,[status(thm)],[]) ).
tff(282,axiom,
a_808 != a_829,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tff(283,plain,
a_808 != a_829,
inference(modus_ponens,[status(thm)],[282,281]) ).
tff(284,plain,
$false,
inference(unit_resolution,[status(thm)],[283,280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV543-1.007 : TPTP v9.0.0. Released v4.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n005.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 10:14:35 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.19/0.37 % SZS status Unsatisfiable
% 0.19/0.37 % SZS output start Proof
% See solution above
% 0.19/0.40 % E exiting
%------------------------------------------------------------------------------