%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWV543-1.010 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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.13s 0.38s
% Output : Proof 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 167
% Syntax : Number of formulae : 453 ( 365 unt; 0 typ; 0 def)
% Number of atoms : 543 ( 541 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 100 ( 11 ~; 7 |; 0 &)
% ( 82 <=>; 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 : 89 ( 89 usr; 87 con; 0-3 aty)
% Number of variables : 72 ( 69 !; 0 ?; 72 :)
% Comments :
%------------------------------------------------------------------------------
tff(a_1319_type,type,
a_1319: $i ).
tff(a_1282_type,type,
a_1282: $i ).
tff(store_type,type,
store: ( $i * $i * $i ) > $i ).
tff(e_1318_type,type,
e_1318: $i ).
tff(i9_type,type,
i9: $i ).
tff(a_1317_type,type,
a_1317: $i ).
tff(select_type,type,
select: ( $i * $i ) > $i ).
tff(i5_type,type,
i5: $i ).
tff(e_1314_type,type,
e_1314: $i ).
tff(i0_type,type,
i0: $i ).
tff(a_1313_type,type,
a_1313: $i ).
tff(a_1315_type,type,
a_1315: $i ).
tff(e_1316_type,type,
e_1316: $i ).
tff(e_1281_type,type,
e_1281: $i ).
tff(a_1280_type,type,
a_1280: $i ).
tff(a_1278_type,type,
a_1278: $i ).
tff(e_1277_type,type,
e_1277: $i ).
tff(a_1276_type,type,
a_1276: $i ).
tff(i3_type,type,
i3: $i ).
tff(a_1311_type,type,
a_1311: $i ).
tff(a_1274_type,type,
a_1274: $i ).
tff(e_1310_type,type,
e_1310: $i ).
tff(i1_type,type,
i1: $i ).
tff(a_1309_type,type,
a_1309: $i ).
tff(i2_type,type,
i2: $i ).
tff(e_1268_type,type,
e_1268: $i ).
tff(a_1269_type,type,
a_1269: $i ).
tff(a_1307_type,type,
a_1307: $i ).
tff(a_1270_type,type,
a_1270: $i ).
tff(e_1305_type,type,
e_1305: $i ).
tff(a_1306_type,type,
a_1306: $i ).
tff(a_1267_type,type,
a_1267: $i ).
tff(a_1304_type,type,
a_1304: $i ).
tff(e_1266_type,type,
e_1266: $i ).
tff(a_1265_type,type,
a_1265: $i ).
tff(e_1303_type,type,
e_1303: $i ).
tff(a_1302_type,type,
a_1302: $i ).
tff(i4_type,type,
i4: $i ).
tff(a_1263_type,type,
a_1263: $i ).
tff(a_1300_type,type,
a_1300: $i ).
tff(e_1262_type,type,
e_1262: $i ).
tff(a_1261_type,type,
a_1261: $i ).
tff(i7_type,type,
i7: $i ).
tff(e_1295_type,type,
e_1295: $i ).
tff(a_1294_type,type,
a_1294: $i ).
tff(a_1259_type,type,
a_1259: $i ).
tff(a_1296_type,type,
a_1296: $i ).
tff(e_1258_type,type,
e_1258: $i ).
tff(a_1257_type,type,
a_1257: $i ).
tff(a_1292_type,type,
a_1292: $i ).
tff(a_1255_type,type,
a_1255: $i ).
tff(e_1291_type,type,
e_1291: $i ).
tff(i8_type,type,
i8: $i ).
tff(a_1290_type,type,
a_1290: $i ).
tff(e_1250_type,type,
e_1250: $i ).
tff(a_1249_type,type,
a_1249: $i ).
tff(a_1288_type,type,
a_1288: $i ).
tff(a_1251_type,type,
a_1251: $i ).
tff(e_1287_type,type,
e_1287: $i ).
tff(a_1286_type,type,
a_1286: $i ).
tff(i6_type,type,
i6: $i ).
tff(a_1284_type,type,
a_1284: $i ).
tff(a_1247_type,type,
a_1247: $i ).
tff(e_1246_type,type,
e_1246: $i ).
tff(a_1245_type,type,
a_1245: $i ).
tff(a1_type,type,
a1: $i ).
tff(e_1244_type,type,
e_1244: $i ).
tff(a_1283_type,type,
a_1283: $i ).
tff(e_1285_type,type,
e_1285: $i ).
tff(e_1248_type,type,
e_1248: $i ).
tff(e_1289_type,type,
e_1289: $i ).
tff(e_1254_type,type,
e_1254: $i ).
tff(a_1253_type,type,
a_1253: $i ).
tff(e_1252_type,type,
e_1252: $i ).
tff(e_1293_type,type,
e_1293: $i ).
tff(e_1256_type,type,
e_1256: $i ).
tff(e_1260_type,type,
e_1260: $i ).
tff(e_1299_type,type,
e_1299: $i ).
tff(a_1298_type,type,
a_1298: $i ).
tff(e_1297_type,type,
e_1297: $i ).
tff(e_1264_type,type,
e_1264: $i ).
tff(e_1301_type,type,
e_1301: $i ).
tff(e_1308_type,type,
e_1308: $i ).
tff(e_1273_type,type,
e_1273: $i ).
tff(a_1272_type,type,
a_1272: $i ).
tff(e_1271_type,type,
e_1271: $i ).
tff(e_1312_type,type,
e_1312: $i ).
tff(e_1275_type,type,
e_1275: $i ).
tff(e_1279_type,type,
e_1279: $i ).
tff(1,plain,
( ( a_1319 = store(a_1317,i9,e_1318) )
<=> ( a_1319 = store(a_1317,i9,e_1318) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(2,axiom,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
tff(3,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(modus_ponens,[status(thm)],[2,1]) ).
tff(4,plain,
store(a_1317,i9,e_1318) = a_1319,
inference(symmetry,[status(thm)],[3]) ).
tff(5,plain,
( ( a_1315 = store(a_1313,i0,e_1314) )
<=> ( a_1315 = store(a_1313,i0,e_1314) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(6,axiom,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
tff(7,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(modus_ponens,[status(thm)],[6,5]) ).
tff(8,plain,
store(a_1313,i0,e_1314) = a_1315,
inference(symmetry,[status(thm)],[7]) ).
tff(9,plain,
select(store(a_1313,i0,e_1314),i5) = select(a_1315,i5),
inference(monotonicity,[status(thm)],[8]) ).
tff(10,plain,
select(a_1315,i5) = select(store(a_1313,i0,e_1314),i5),
inference(symmetry,[status(thm)],[9]) ).
tff(11,plain,
( ( e_1318 = select(a_1315,i5) )
<=> ( e_1318 = select(a_1315,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(12,axiom,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).
tff(13,plain,
e_1318 = select(a_1315,i5),
inference(modus_ponens,[status(thm)],[12,11]) ).
tff(14,plain,
e_1318 = select(store(a_1313,i0,e_1314),i5),
inference(transitivity,[status(thm)],[13,10]) ).
tff(15,plain,
( ( e_1316 = select(a_1315,i9) )
<=> ( e_1316 = select(a_1315,i9) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(16,axiom,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp74) ).
tff(17,plain,
e_1316 = select(a_1315,i9),
inference(modus_ponens,[status(thm)],[16,15]) ).
tff(18,plain,
select(a_1315,i9) = e_1316,
inference(symmetry,[status(thm)],[17]) ).
tff(19,plain,
select(store(a_1313,i0,e_1314),i9) = select(a_1315,i9),
inference(monotonicity,[status(thm)],[8]) ).
tff(20,plain,
select(store(a_1313,i0,e_1314),i9) = e_1316,
inference(transitivity,[status(thm)],[19,18]) ).
tff(21,plain,
store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)) = store(a_1315,i5,e_1316),
inference(monotonicity,[status(thm)],[8,20]) ).
tff(22,plain,
store(a_1315,i5,e_1316) = store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),
inference(symmetry,[status(thm)],[21]) ).
tff(23,plain,
( ( a_1317 = store(a_1315,i5,e_1316) )
<=> ( a_1317 = store(a_1315,i5,e_1316) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(24,axiom,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
tff(25,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(modus_ponens,[status(thm)],[24,23]) ).
tff(26,plain,
a_1317 = store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),
inference(transitivity,[status(thm)],[25,22]) ).
tff(27,plain,
store(a_1317,i9,e_1318) = store(store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),i9,select(store(a_1313,i0,e_1314),i5)),
inference(monotonicity,[status(thm)],[26,14]) ).
tff(28,plain,
store(store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),i9,select(store(a_1313,i0,e_1314),i5)) = store(a_1317,i9,e_1318),
inference(symmetry,[status(thm)],[27]) ).
tff(29,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(30,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)],[29]) ).
tff(31,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(32,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(33,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)],[32,31]) ).
tff(34,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)],[33]) ).
tff(35,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)],[34,30]) ).
tff(36,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_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),i9,select(store(a_1313,i0,e_1314),i5)) = store(store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)),i5,select(store(a_1313,i0,e_1314),i9)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(37,plain,
store(store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),i9,select(store(a_1313,i0,e_1314),i5)) = store(store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)),i5,select(store(a_1313,i0,e_1314),i9)),
inference(unit_resolution,[status(thm)],[36,35]) ).
tff(38,plain,
store(store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)),i5,select(store(a_1313,i0,e_1314),i9)) = store(store(store(a_1313,i0,e_1314),i5,select(store(a_1313,i0,e_1314),i9)),i9,select(store(a_1313,i0,e_1314),i5)),
inference(symmetry,[status(thm)],[37]) ).
tff(39,plain,
( ( e_1281 = select(a_1278,i9) )
<=> ( e_1281 = select(a_1278,i9) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(40,axiom,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
tff(41,plain,
e_1281 = select(a_1278,i9),
inference(modus_ponens,[status(thm)],[40,39]) ).
tff(42,plain,
select(a_1278,i9) = e_1281,
inference(symmetry,[status(thm)],[41]) ).
tff(43,plain,
( ( e_1314 = select(a_1311,i3) )
<=> ( e_1314 = select(a_1311,i3) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(44,axiom,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp73) ).
tff(45,plain,
e_1314 = select(a_1311,i3),
inference(modus_ponens,[status(thm)],[44,43]) ).
tff(46,plain,
select(a_1311,i3) = e_1314,
inference(symmetry,[status(thm)],[45]) ).
tff(47,plain,
( ( a_1311 = store(a_1309,i1,e_1310) )
<=> ( a_1311 = store(a_1309,i1,e_1310) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(48,axiom,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
tff(49,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(modus_ponens,[status(thm)],[48,47]) ).
tff(50,plain,
store(a_1309,i1,e_1310) = a_1311,
inference(symmetry,[status(thm)],[49]) ).
tff(51,plain,
( ( e_1310 = select(a_1307,i2) )
<=> ( e_1310 = select(a_1307,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(52,axiom,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp71) ).
tff(53,plain,
e_1310 = select(a_1307,i2),
inference(modus_ponens,[status(thm)],[52,51]) ).
tff(54,plain,
select(a_1307,i2) = e_1310,
inference(symmetry,[status(thm)],[53]) ).
tff(55,plain,
( ( a_1270 = store(a_1269,i0,e_1268) )
<=> ( a_1270 = store(a_1269,i0,e_1268) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(56,axiom,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
tff(57,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(modus_ponens,[status(thm)],[56,55]) ).
tff(58,plain,
store(a_1269,i0,e_1268) = a_1270,
inference(symmetry,[status(thm)],[57]) ).
tff(59,plain,
( ( e_1268 = select(a_1267,i0) )
<=> ( e_1268 = select(a_1267,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(60,axiom,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
tff(61,plain,
e_1268 = select(a_1267,i0),
inference(modus_ponens,[status(thm)],[60,59]) ).
tff(62,plain,
select(a_1267,i0) = e_1268,
inference(symmetry,[status(thm)],[61]) ).
tff(63,plain,
( ( a_1267 = store(a_1265,i5,e_1266) )
<=> ( a_1267 = store(a_1265,i5,e_1266) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(64,axiom,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
tff(65,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(modus_ponens,[status(thm)],[64,63]) ).
tff(66,plain,
store(a_1265,i5,e_1266) = a_1267,
inference(symmetry,[status(thm)],[65]) ).
tff(67,plain,
( ( e_1266 = select(a_1263,i4) )
<=> ( e_1266 = select(a_1263,i4) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(68,axiom,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
tff(69,plain,
e_1266 = select(a_1263,i4),
inference(modus_ponens,[status(thm)],[68,67]) ).
tff(70,plain,
select(a_1263,i4) = e_1266,
inference(symmetry,[status(thm)],[69]) ).
tff(71,plain,
( ( a_1263 = store(a_1261,i1,e_1262) )
<=> ( a_1263 = store(a_1261,i1,e_1262) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(72,axiom,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
tff(73,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(modus_ponens,[status(thm)],[72,71]) ).
tff(74,plain,
store(a_1261,i1,e_1262) = a_1263,
inference(symmetry,[status(thm)],[73]) ).
tff(75,plain,
( ( e_1262 = select(a_1259,i7) )
<=> ( e_1262 = select(a_1259,i7) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(76,axiom,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
tff(77,plain,
e_1262 = select(a_1259,i7),
inference(modus_ponens,[status(thm)],[76,75]) ).
tff(78,plain,
select(a_1259,i7) = e_1262,
inference(symmetry,[status(thm)],[77]) ).
tff(79,plain,
( ( a_1296 = store(a_1294,i9,e_1295) )
<=> ( a_1296 = store(a_1294,i9,e_1295) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(80,axiom,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
tff(81,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(modus_ponens,[status(thm)],[80,79]) ).
tff(82,plain,
store(a_1294,i9,e_1295) = a_1296,
inference(symmetry,[status(thm)],[81]) ).
tff(83,plain,
( ( e_1295 = select(a_1292,i4) )
<=> ( e_1295 = select(a_1292,i4) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(84,axiom,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).
tff(85,plain,
e_1295 = select(a_1292,i4),
inference(modus_ponens,[status(thm)],[84,83]) ).
tff(86,plain,
select(a_1292,i4) = e_1295,
inference(symmetry,[status(thm)],[85]) ).
tff(87,plain,
( ( a_1292 = store(a_1290,i8,e_1291) )
<=> ( a_1292 = store(a_1290,i8,e_1291) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(88,axiom,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
tff(89,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(modus_ponens,[status(thm)],[88,87]) ).
tff(90,plain,
store(a_1290,i8,e_1291) = a_1292,
inference(symmetry,[status(thm)],[89]) ).
tff(91,plain,
( ( e_1291 = select(a_1288,i5) )
<=> ( e_1291 = select(a_1288,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(92,axiom,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).
tff(93,plain,
e_1291 = select(a_1288,i5),
inference(modus_ponens,[status(thm)],[92,91]) ).
tff(94,plain,
select(a_1288,i5) = e_1291,
inference(symmetry,[status(thm)],[93]) ).
tff(95,plain,
( ( a_1288 = store(a_1286,i8,e_1287) )
<=> ( a_1288 = store(a_1286,i8,e_1287) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(96,axiom,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
tff(97,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(modus_ponens,[status(thm)],[96,95]) ).
tff(98,plain,
store(a_1286,i8,e_1287) = a_1288,
inference(symmetry,[status(thm)],[97]) ).
tff(99,plain,
( ( e_1287 = select(a_1284,i6) )
<=> ( e_1287 = select(a_1284,i6) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(100,axiom,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).
tff(101,plain,
e_1287 = select(a_1284,i6),
inference(modus_ponens,[status(thm)],[100,99]) ).
tff(102,plain,
select(a_1284,i6) = e_1287,
inference(symmetry,[status(thm)],[101]) ).
tff(103,plain,
( ( a_1247 = store(a_1245,i7,e_1246) )
<=> ( a_1247 = store(a_1245,i7,e_1246) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(104,axiom,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
tff(105,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(modus_ponens,[status(thm)],[104,103]) ).
tff(106,plain,
store(a_1245,i7,e_1246) = a_1247,
inference(symmetry,[status(thm)],[105]) ).
tff(107,plain,
( ( e_1246 = select(a1,i8) )
<=> ( e_1246 = select(a1,i8) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(108,axiom,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
tff(109,plain,
e_1246 = select(a1,i8),
inference(modus_ponens,[status(thm)],[108,107]) ).
tff(110,plain,
select(a1,i8) = e_1246,
inference(symmetry,[status(thm)],[109]) ).
tff(111,plain,
( ( a_1245 = store(a1,i8,e_1244) )
<=> ( a_1245 = store(a1,i8,e_1244) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(112,axiom,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
tff(113,plain,
a_1245 = store(a1,i8,e_1244),
inference(modus_ponens,[status(thm)],[112,111]) ).
tff(114,plain,
store(a1,i8,e_1244) = a_1245,
inference(symmetry,[status(thm)],[113]) ).
tff(115,plain,
( ( e_1244 = select(a1,i7) )
<=> ( e_1244 = select(a1,i7) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(116,axiom,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
tff(117,plain,
e_1244 = select(a1,i7),
inference(modus_ponens,[status(thm)],[116,115]) ).
tff(118,plain,
select(a1,i7) = e_1244,
inference(symmetry,[status(thm)],[117]) ).
tff(119,plain,
store(a1,i8,select(a1,i7)) = store(a1,i8,e_1244),
inference(monotonicity,[status(thm)],[118]) ).
tff(120,plain,
store(a1,i8,select(a1,i7)) = a_1245,
inference(transitivity,[status(thm)],[119,114]) ).
tff(121,plain,
store(store(a1,i8,select(a1,i7)),i7,select(a1,i8)) = store(a_1245,i7,e_1246),
inference(monotonicity,[status(thm)],[120,110]) ).
tff(122,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(a1,i8,select(a1,i7)),i7,select(a1,i8)) = store(store(a1,i7,select(a1,i8)),i8,select(a1,i7)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(123,plain,
store(store(a1,i8,select(a1,i7)),i7,select(a1,i8)) = store(store(a1,i7,select(a1,i8)),i8,select(a1,i7)),
inference(unit_resolution,[status(thm)],[122,35]) ).
tff(124,plain,
store(store(a1,i7,select(a1,i8)),i8,select(a1,i7)) = store(store(a1,i8,select(a1,i7)),i7,select(a1,i8)),
inference(symmetry,[status(thm)],[123]) ).
tff(125,plain,
store(a1,i7,select(a1,i8)) = store(a1,i7,e_1246),
inference(monotonicity,[status(thm)],[110]) ).
tff(126,plain,
store(a1,i7,e_1246) = store(a1,i7,select(a1,i8)),
inference(symmetry,[status(thm)],[125]) ).
tff(127,plain,
( ( a_1283 = store(a1,i7,e_1246) )
<=> ( a_1283 = store(a1,i7,e_1246) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(128,axiom,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
tff(129,plain,
a_1283 = store(a1,i7,e_1246),
inference(modus_ponens,[status(thm)],[128,127]) ).
tff(130,plain,
a_1283 = store(a1,i7,select(a1,i8)),
inference(transitivity,[status(thm)],[129,126]) ).
tff(131,plain,
store(a_1283,i8,e_1244) = store(store(a1,i7,select(a1,i8)),i8,select(a1,i7)),
inference(monotonicity,[status(thm)],[130,117]) ).
tff(132,plain,
( ( a_1284 = store(a_1283,i8,e_1244) )
<=> ( a_1284 = store(a_1283,i8,e_1244) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(133,axiom,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
tff(134,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(modus_ponens,[status(thm)],[133,132]) ).
tff(135,plain,
a_1284 = a_1247,
inference(transitivity,[status(thm)],[134,131,124,121,106]) ).
tff(136,plain,
select(a_1284,i6) = select(a_1247,i6),
inference(monotonicity,[status(thm)],[135]) ).
tff(137,plain,
select(a_1247,i6) = select(a_1284,i6),
inference(symmetry,[status(thm)],[136]) ).
tff(138,plain,
( ( e_1250 = select(a_1247,i6) )
<=> ( e_1250 = select(a_1247,i6) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(139,axiom,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
tff(140,plain,
e_1250 = select(a_1247,i6),
inference(modus_ponens,[status(thm)],[139,138]) ).
tff(141,plain,
e_1250 = e_1287,
inference(transitivity,[status(thm)],[140,137,102]) ).
tff(142,plain,
( ( a_1286 = store(a_1284,i6,e_1285) )
<=> ( a_1286 = store(a_1284,i6,e_1285) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(143,axiom,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
tff(144,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(modus_ponens,[status(thm)],[143,142]) ).
tff(145,plain,
store(a_1284,i6,e_1285) = a_1286,
inference(symmetry,[status(thm)],[144]) ).
tff(146,plain,
( ( e_1285 = select(a_1284,i8) )
<=> ( e_1285 = select(a_1284,i8) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(147,axiom,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).
tff(148,plain,
e_1285 = select(a_1284,i8),
inference(modus_ponens,[status(thm)],[147,146]) ).
tff(149,plain,
select(a_1284,i8) = e_1285,
inference(symmetry,[status(thm)],[148]) ).
tff(150,plain,
store(a_1283,i8,e_1244) = a_1284,
inference(symmetry,[status(thm)],[134]) ).
tff(151,plain,
store(store(a1,i7,select(a1,i8)),i8,select(a1,i7)) = store(a_1283,i8,e_1244),
inference(symmetry,[status(thm)],[131]) ).
tff(152,plain,
store(a_1245,i7,e_1246) = store(store(a1,i8,select(a1,i7)),i7,select(a1,i8)),
inference(symmetry,[status(thm)],[121]) ).
tff(153,plain,
a_1247 = a_1284,
inference(transitivity,[status(thm)],[105,152,123,151,150]) ).
tff(154,plain,
select(a_1247,i8) = select(a_1284,i8),
inference(monotonicity,[status(thm)],[153]) ).
tff(155,plain,
( ( e_1248 = select(a_1247,i8) )
<=> ( e_1248 = select(a_1247,i8) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(156,axiom,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
tff(157,plain,
e_1248 = select(a_1247,i8),
inference(modus_ponens,[status(thm)],[156,155]) ).
tff(158,plain,
e_1248 = e_1285,
inference(transitivity,[status(thm)],[157,154,149]) ).
tff(159,plain,
store(a_1247,i6,e_1248) = store(a_1284,i6,e_1285),
inference(monotonicity,[status(thm)],[153,158]) ).
tff(160,plain,
( ( a_1249 = store(a_1247,i6,e_1248) )
<=> ( a_1249 = store(a_1247,i6,e_1248) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(161,axiom,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
tff(162,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(modus_ponens,[status(thm)],[161,160]) ).
tff(163,plain,
a_1249 = a_1286,
inference(transitivity,[status(thm)],[162,159,145]) ).
tff(164,plain,
store(a_1249,i8,e_1250) = store(a_1286,i8,e_1287),
inference(monotonicity,[status(thm)],[163,141]) ).
tff(165,plain,
( ( a_1251 = store(a_1249,i8,e_1250) )
<=> ( a_1251 = store(a_1249,i8,e_1250) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(166,axiom,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
tff(167,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(modus_ponens,[status(thm)],[166,165]) ).
tff(168,plain,
a_1251 = a_1288,
inference(transitivity,[status(thm)],[167,164,98]) ).
tff(169,plain,
select(a_1251,i5) = select(a_1288,i5),
inference(monotonicity,[status(thm)],[168]) ).
tff(170,plain,
store(a_1249,i8,e_1250) = a_1251,
inference(symmetry,[status(thm)],[167]) ).
tff(171,plain,
select(store(a_1249,i8,e_1250),i5) = select(a_1251,i5),
inference(monotonicity,[status(thm)],[170]) ).
tff(172,plain,
select(store(a_1249,i8,e_1250),i5) = e_1291,
inference(transitivity,[status(thm)],[171,169,94]) ).
tff(173,plain,
( ( a_1290 = store(a_1288,i5,e_1289) )
<=> ( a_1290 = store(a_1288,i5,e_1289) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(174,axiom,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
tff(175,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(modus_ponens,[status(thm)],[174,173]) ).
tff(176,plain,
store(a_1288,i5,e_1289) = a_1290,
inference(symmetry,[status(thm)],[175]) ).
tff(177,plain,
( ( e_1289 = select(a_1288,i8) )
<=> ( e_1289 = select(a_1288,i8) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(178,axiom,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).
tff(179,plain,
e_1289 = select(a_1288,i8),
inference(modus_ponens,[status(thm)],[178,177]) ).
tff(180,plain,
select(a_1288,i8) = e_1289,
inference(symmetry,[status(thm)],[179]) ).
tff(181,plain,
store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)) = store(a_1286,i8,e_1287),
inference(monotonicity,[status(thm)],[145,102]) ).
tff(182,plain,
store(a_1286,i8,e_1287) = store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),
inference(symmetry,[status(thm)],[181]) ).
tff(183,plain,
a_1288 = store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),
inference(transitivity,[status(thm)],[97,182]) ).
tff(184,plain,
select(a_1288,i8) = select(store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),i8),
inference(monotonicity,[status(thm)],[183]) ).
tff(185,plain,
select(store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),i8) = select(a_1288,i8),
inference(symmetry,[status(thm)],[184]) ).
tff(186,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(187,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(188,axiom,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
tff(189,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(modus_ponens,[status(thm)],[188,187]) ).
tff(190,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(skolemize,[status(sab)],[189]) ).
tff(191,plain,
! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E ),
inference(modus_ponens,[status(thm)],[190,186]) ).
tff(192,plain,
( ~ ! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E )
| ( select(store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),i8) = select(a_1284,i6) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(193,plain,
select(store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),i8) = select(a_1284,i6),
inference(unit_resolution,[status(thm)],[192,191]) ).
tff(194,plain,
select(a_1284,i6) = select(store(store(a_1284,i6,e_1285),i8,select(a_1284,i6)),i8),
inference(symmetry,[status(thm)],[193]) ).
tff(195,plain,
( ~ ! [I: $i,E: $i,A: $i] : ( select(store(A,I,E),I) = E )
| ( select(store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)),i8) = select(a_1247,i6) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(196,plain,
select(store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)),i8) = select(a_1247,i6),
inference(unit_resolution,[status(thm)],[195,191]) ).
tff(197,plain,
select(a_1247,i6) = e_1250,
inference(symmetry,[status(thm)],[140]) ).
tff(198,plain,
store(a_1247,i6,e_1248) = a_1249,
inference(symmetry,[status(thm)],[162]) ).
tff(199,plain,
store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)) = store(a_1249,i8,e_1250),
inference(monotonicity,[status(thm)],[198,197]) ).
tff(200,plain,
store(a_1249,i8,e_1250) = store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)),
inference(symmetry,[status(thm)],[199]) ).
tff(201,plain,
a_1251 = store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)),
inference(transitivity,[status(thm)],[167,200]) ).
tff(202,plain,
select(a_1251,i8) = select(store(store(a_1247,i6,e_1248),i8,select(a_1247,i6)),i8),
inference(monotonicity,[status(thm)],[201]) ).
tff(203,plain,
select(store(a_1249,i8,e_1250),i8) = select(a_1251,i8),
inference(monotonicity,[status(thm)],[170]) ).
tff(204,plain,
select(store(a_1249,i8,e_1250),i8) = e_1289,
inference(transitivity,[status(thm)],[203,202,196,137,194,185,180]) ).
tff(205,plain,
store(a_1249,i8,e_1250) = a_1288,
inference(transitivity,[status(thm)],[164,98]) ).
tff(206,plain,
store(store(a_1249,i8,e_1250),i5,select(store(a_1249,i8,e_1250),i8)) = store(a_1288,i5,e_1289),
inference(monotonicity,[status(thm)],[205,204]) ).
tff(207,plain,
store(store(a_1249,i8,e_1250),i5,select(store(a_1249,i8,e_1250),i8)) = a_1290,
inference(transitivity,[status(thm)],[206,176]) ).
tff(208,plain,
store(store(store(a_1249,i8,e_1250),i5,select(store(a_1249,i8,e_1250),i8)),i8,select(store(a_1249,i8,e_1250),i5)) = store(a_1290,i8,e_1291),
inference(monotonicity,[status(thm)],[207,172]) ).
tff(209,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_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)),i5,select(store(a_1249,i8,e_1250),i8)) = store(store(store(a_1249,i8,e_1250),i5,select(store(a_1249,i8,e_1250),i8)),i8,select(store(a_1249,i8,e_1250),i5)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(210,plain,
store(store(store(a_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)),i5,select(store(a_1249,i8,e_1250),i8)) = store(store(store(a_1249,i8,e_1250),i5,select(store(a_1249,i8,e_1250),i8)),i8,select(store(a_1249,i8,e_1250),i5)),
inference(unit_resolution,[status(thm)],[209,35]) ).
tff(211,plain,
select(a_1251,i8) = select(store(a_1249,i8,e_1250),i8),
inference(symmetry,[status(thm)],[203]) ).
tff(212,plain,
( ( e_1254 = select(a_1251,i8) )
<=> ( e_1254 = select(a_1251,i8) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(213,axiom,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
tff(214,plain,
e_1254 = select(a_1251,i8),
inference(modus_ponens,[status(thm)],[213,212]) ).
tff(215,plain,
e_1254 = select(store(a_1249,i8,e_1250),i8),
inference(transitivity,[status(thm)],[214,211]) ).
tff(216,plain,
( ( e_1252 = select(a_1251,i5) )
<=> ( e_1252 = select(a_1251,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(217,axiom,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
tff(218,plain,
e_1252 = select(a_1251,i5),
inference(modus_ponens,[status(thm)],[217,216]) ).
tff(219,plain,
select(a_1251,i5) = e_1252,
inference(symmetry,[status(thm)],[218]) ).
tff(220,plain,
select(store(a_1249,i8,e_1250),i5) = e_1252,
inference(transitivity,[status(thm)],[171,219]) ).
tff(221,plain,
store(store(a_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)) = store(a_1251,i8,e_1252),
inference(monotonicity,[status(thm)],[170,220]) ).
tff(222,plain,
store(a_1251,i8,e_1252) = store(store(a_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)),
inference(symmetry,[status(thm)],[221]) ).
tff(223,plain,
( ( a_1253 = store(a_1251,i8,e_1252) )
<=> ( a_1253 = store(a_1251,i8,e_1252) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(224,axiom,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
tff(225,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(modus_ponens,[status(thm)],[224,223]) ).
tff(226,plain,
a_1253 = store(store(a_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)),
inference(transitivity,[status(thm)],[225,222]) ).
tff(227,plain,
store(a_1253,i5,e_1254) = store(store(store(a_1249,i8,e_1250),i8,select(store(a_1249,i8,e_1250),i5)),i5,select(store(a_1249,i8,e_1250),i8)),
inference(monotonicity,[status(thm)],[226,215]) ).
tff(228,plain,
( ( a_1255 = store(a_1253,i5,e_1254) )
<=> ( a_1255 = store(a_1253,i5,e_1254) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(229,axiom,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
tff(230,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(modus_ponens,[status(thm)],[229,228]) ).
tff(231,plain,
a_1255 = a_1292,
inference(transitivity,[status(thm)],[230,227,210,208,90]) ).
tff(232,plain,
select(a_1255,i4) = select(a_1292,i4),
inference(monotonicity,[status(thm)],[231]) ).
tff(233,plain,
( ( e_1258 = select(a_1255,i4) )
<=> ( e_1258 = select(a_1255,i4) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(234,axiom,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
tff(235,plain,
e_1258 = select(a_1255,i4),
inference(modus_ponens,[status(thm)],[234,233]) ).
tff(236,plain,
e_1258 = e_1295,
inference(transitivity,[status(thm)],[235,232,86]) ).
tff(237,plain,
( ( a_1294 = store(a_1292,i4,e_1293) )
<=> ( a_1294 = store(a_1292,i4,e_1293) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(238,axiom,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
tff(239,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(modus_ponens,[status(thm)],[238,237]) ).
tff(240,plain,
store(a_1292,i4,e_1293) = a_1294,
inference(symmetry,[status(thm)],[239]) ).
tff(241,plain,
( ( e_1293 = select(a_1292,i9) )
<=> ( e_1293 = select(a_1292,i9) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(242,axiom,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).
tff(243,plain,
e_1293 = select(a_1292,i9),
inference(modus_ponens,[status(thm)],[242,241]) ).
tff(244,plain,
select(a_1292,i9) = e_1293,
inference(symmetry,[status(thm)],[243]) ).
tff(245,plain,
select(a_1255,i9) = select(a_1292,i9),
inference(monotonicity,[status(thm)],[231]) ).
tff(246,plain,
( ( e_1256 = select(a_1255,i9) )
<=> ( e_1256 = select(a_1255,i9) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(247,axiom,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
tff(248,plain,
e_1256 = select(a_1255,i9),
inference(modus_ponens,[status(thm)],[247,246]) ).
tff(249,plain,
e_1256 = e_1293,
inference(transitivity,[status(thm)],[248,245,244]) ).
tff(250,plain,
store(a_1255,i4,e_1256) = store(a_1292,i4,e_1293),
inference(monotonicity,[status(thm)],[231,249]) ).
tff(251,plain,
( ( a_1257 = store(a_1255,i4,e_1256) )
<=> ( a_1257 = store(a_1255,i4,e_1256) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(252,axiom,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
tff(253,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(modus_ponens,[status(thm)],[252,251]) ).
tff(254,plain,
a_1257 = a_1294,
inference(transitivity,[status(thm)],[253,250,240]) ).
tff(255,plain,
store(a_1257,i9,e_1258) = store(a_1294,i9,e_1295),
inference(monotonicity,[status(thm)],[254,236]) ).
tff(256,plain,
( ( a_1259 = store(a_1257,i9,e_1258) )
<=> ( a_1259 = store(a_1257,i9,e_1258) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(257,axiom,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
tff(258,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(modus_ponens,[status(thm)],[257,256]) ).
tff(259,plain,
a_1259 = a_1296,
inference(transitivity,[status(thm)],[258,255,82]) ).
tff(260,plain,
select(a_1259,i7) = select(a_1296,i7),
inference(monotonicity,[status(thm)],[259]) ).
tff(261,plain,
select(a_1296,i7) = select(a_1259,i7),
inference(symmetry,[status(thm)],[260]) ).
tff(262,plain,
select(store(a_1294,i9,e_1295),i7) = select(a_1296,i7),
inference(monotonicity,[status(thm)],[82]) ).
tff(263,plain,
select(store(a_1294,i9,e_1295),i7) = e_1262,
inference(transitivity,[status(thm)],[262,261,78]) ).
tff(264,plain,
( ( a_1261 = store(a_1259,i7,e_1260) )
<=> ( a_1261 = store(a_1259,i7,e_1260) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(265,axiom,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
tff(266,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(modus_ponens,[status(thm)],[265,264]) ).
tff(267,plain,
store(a_1259,i7,e_1260) = a_1261,
inference(symmetry,[status(thm)],[266]) ).
tff(268,plain,
( ( e_1260 = select(a_1259,i1) )
<=> ( e_1260 = select(a_1259,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(269,axiom,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
tff(270,plain,
e_1260 = select(a_1259,i1),
inference(modus_ponens,[status(thm)],[269,268]) ).
tff(271,plain,
select(a_1259,i1) = e_1260,
inference(symmetry,[status(thm)],[270]) ).
tff(272,plain,
select(a_1259,i1) = select(a_1296,i1),
inference(monotonicity,[status(thm)],[259]) ).
tff(273,plain,
select(a_1296,i1) = select(a_1259,i1),
inference(symmetry,[status(thm)],[272]) ).
tff(274,plain,
select(store(a_1294,i9,e_1295),i1) = select(a_1296,i1),
inference(monotonicity,[status(thm)],[82]) ).
tff(275,plain,
select(store(a_1294,i9,e_1295),i1) = e_1260,
inference(transitivity,[status(thm)],[274,273,271]) ).
tff(276,plain,
store(a_1257,i9,e_1258) = a_1259,
inference(symmetry,[status(thm)],[258]) ).
tff(277,plain,
store(a_1294,i9,e_1295) = store(a_1257,i9,e_1258),
inference(symmetry,[status(thm)],[255]) ).
tff(278,plain,
store(a_1294,i9,e_1295) = a_1259,
inference(transitivity,[status(thm)],[277,276]) ).
tff(279,plain,
store(store(a_1294,i9,e_1295),i7,select(store(a_1294,i9,e_1295),i1)) = store(a_1259,i7,e_1260),
inference(monotonicity,[status(thm)],[278,275]) ).
tff(280,plain,
store(store(a_1294,i9,e_1295),i7,select(store(a_1294,i9,e_1295),i1)) = a_1261,
inference(transitivity,[status(thm)],[279,267]) ).
tff(281,plain,
store(store(store(a_1294,i9,e_1295),i7,select(store(a_1294,i9,e_1295),i1)),i1,select(store(a_1294,i9,e_1295),i7)) = store(a_1261,i1,e_1262),
inference(monotonicity,[status(thm)],[280,263]) ).
tff(282,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_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)),i7,select(store(a_1294,i9,e_1295),i1)) = store(store(store(a_1294,i9,e_1295),i7,select(store(a_1294,i9,e_1295),i1)),i1,select(store(a_1294,i9,e_1295),i7)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(283,plain,
store(store(store(a_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)),i7,select(store(a_1294,i9,e_1295),i1)) = store(store(store(a_1294,i9,e_1295),i7,select(store(a_1294,i9,e_1295),i1)),i1,select(store(a_1294,i9,e_1295),i7)),
inference(unit_resolution,[status(thm)],[282,35]) ).
tff(284,plain,
select(a_1296,i1) = select(store(a_1294,i9,e_1295),i1),
inference(symmetry,[status(thm)],[274]) ).
tff(285,plain,
( ( e_1299 = select(a_1296,i1) )
<=> ( e_1299 = select(a_1296,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(286,axiom,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).
tff(287,plain,
e_1299 = select(a_1296,i1),
inference(modus_ponens,[status(thm)],[286,285]) ).
tff(288,plain,
e_1299 = select(store(a_1294,i9,e_1295),i1),
inference(transitivity,[status(thm)],[287,284]) ).
tff(289,plain,
( ( e_1297 = select(a_1296,i7) )
<=> ( e_1297 = select(a_1296,i7) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(290,axiom,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
tff(291,plain,
e_1297 = select(a_1296,i7),
inference(modus_ponens,[status(thm)],[290,289]) ).
tff(292,plain,
select(a_1296,i7) = e_1297,
inference(symmetry,[status(thm)],[291]) ).
tff(293,plain,
select(store(a_1294,i9,e_1295),i7) = e_1297,
inference(transitivity,[status(thm)],[262,292]) ).
tff(294,plain,
store(store(a_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)) = store(a_1296,i1,e_1297),
inference(monotonicity,[status(thm)],[82,293]) ).
tff(295,plain,
store(a_1296,i1,e_1297) = store(store(a_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)),
inference(symmetry,[status(thm)],[294]) ).
tff(296,plain,
( ( a_1298 = store(a_1296,i1,e_1297) )
<=> ( a_1298 = store(a_1296,i1,e_1297) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(297,axiom,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
tff(298,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(modus_ponens,[status(thm)],[297,296]) ).
tff(299,plain,
a_1298 = store(store(a_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)),
inference(transitivity,[status(thm)],[298,295]) ).
tff(300,plain,
store(a_1298,i7,e_1299) = store(store(store(a_1294,i9,e_1295),i1,select(store(a_1294,i9,e_1295),i7)),i7,select(store(a_1294,i9,e_1295),i1)),
inference(monotonicity,[status(thm)],[299,288]) ).
tff(301,plain,
( ( a_1300 = store(a_1298,i7,e_1299) )
<=> ( a_1300 = store(a_1298,i7,e_1299) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(302,axiom,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
tff(303,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(modus_ponens,[status(thm)],[302,301]) ).
tff(304,plain,
a_1300 = a_1263,
inference(transitivity,[status(thm)],[303,300,283,281,74]) ).
tff(305,plain,
select(a_1300,i4) = select(a_1263,i4),
inference(monotonicity,[status(thm)],[304]) ).
tff(306,plain,
( ( e_1303 = select(a_1300,i4) )
<=> ( e_1303 = select(a_1300,i4) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(307,axiom,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp68) ).
tff(308,plain,
e_1303 = select(a_1300,i4),
inference(modus_ponens,[status(thm)],[307,306]) ).
tff(309,plain,
e_1303 = e_1266,
inference(transitivity,[status(thm)],[308,305,70]) ).
tff(310,plain,
( ( a_1265 = store(a_1263,i4,e_1264) )
<=> ( a_1265 = store(a_1263,i4,e_1264) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(311,axiom,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
tff(312,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(modus_ponens,[status(thm)],[311,310]) ).
tff(313,plain,
store(a_1263,i4,e_1264) = a_1265,
inference(symmetry,[status(thm)],[312]) ).
tff(314,plain,
( ( e_1264 = select(a_1263,i5) )
<=> ( e_1264 = select(a_1263,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(315,axiom,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
tff(316,plain,
e_1264 = select(a_1263,i5),
inference(modus_ponens,[status(thm)],[315,314]) ).
tff(317,plain,
select(a_1263,i5) = e_1264,
inference(symmetry,[status(thm)],[316]) ).
tff(318,plain,
select(a_1300,i5) = select(a_1263,i5),
inference(monotonicity,[status(thm)],[304]) ).
tff(319,plain,
( ( e_1301 = select(a_1300,i5) )
<=> ( e_1301 = select(a_1300,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(320,axiom,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
tff(321,plain,
e_1301 = select(a_1300,i5),
inference(modus_ponens,[status(thm)],[320,319]) ).
tff(322,plain,
e_1301 = e_1264,
inference(transitivity,[status(thm)],[321,318,317]) ).
tff(323,plain,
store(a_1300,i4,e_1301) = store(a_1263,i4,e_1264),
inference(monotonicity,[status(thm)],[304,322]) ).
tff(324,plain,
( ( a_1302 = store(a_1300,i4,e_1301) )
<=> ( a_1302 = store(a_1300,i4,e_1301) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(325,axiom,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
tff(326,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(modus_ponens,[status(thm)],[325,324]) ).
tff(327,plain,
a_1302 = a_1265,
inference(transitivity,[status(thm)],[326,323,313]) ).
tff(328,plain,
store(a_1302,i5,e_1303) = store(a_1265,i5,e_1266),
inference(monotonicity,[status(thm)],[327,309]) ).
tff(329,plain,
( ( a_1304 = store(a_1302,i5,e_1303) )
<=> ( a_1304 = store(a_1302,i5,e_1303) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(330,axiom,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
tff(331,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(modus_ponens,[status(thm)],[330,329]) ).
tff(332,plain,
a_1304 = a_1267,
inference(transitivity,[status(thm)],[331,328,66]) ).
tff(333,plain,
select(a_1304,i0) = select(a_1267,i0),
inference(monotonicity,[status(thm)],[332]) ).
tff(334,plain,
( ( e_1305 = select(a_1304,i0) )
<=> ( e_1305 = select(a_1304,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(335,axiom,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
tff(336,plain,
e_1305 = select(a_1304,i0),
inference(modus_ponens,[status(thm)],[335,334]) ).
tff(337,plain,
e_1305 = e_1268,
inference(transitivity,[status(thm)],[336,333,62]) ).
tff(338,plain,
( ( a_1269 = store(a_1267,i0,e_1268) )
<=> ( a_1269 = store(a_1267,i0,e_1268) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(339,axiom,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
tff(340,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(modus_ponens,[status(thm)],[339,338]) ).
tff(341,plain,
store(a_1267,i0,e_1268) = a_1269,
inference(symmetry,[status(thm)],[340]) ).
tff(342,plain,
store(a_1304,i0,e_1305) = store(a_1267,i0,e_1268),
inference(monotonicity,[status(thm)],[332,337]) ).
tff(343,plain,
( ( a_1306 = store(a_1304,i0,e_1305) )
<=> ( a_1306 = store(a_1304,i0,e_1305) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(344,axiom,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
tff(345,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(modus_ponens,[status(thm)],[344,343]) ).
tff(346,plain,
a_1306 = a_1269,
inference(transitivity,[status(thm)],[345,342,341]) ).
tff(347,plain,
store(a_1306,i0,e_1305) = store(a_1269,i0,e_1268),
inference(monotonicity,[status(thm)],[346,337]) ).
tff(348,plain,
( ( a_1307 = store(a_1306,i0,e_1305) )
<=> ( a_1307 = store(a_1306,i0,e_1305) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(349,axiom,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
tff(350,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(modus_ponens,[status(thm)],[349,348]) ).
tff(351,plain,
a_1307 = a_1270,
inference(transitivity,[status(thm)],[350,347,58]) ).
tff(352,plain,
select(a_1307,i2) = select(a_1270,i2),
inference(monotonicity,[status(thm)],[351]) ).
tff(353,plain,
select(a_1270,i2) = select(a_1307,i2),
inference(symmetry,[status(thm)],[352]) ).
tff(354,plain,
select(store(a_1269,i0,e_1268),i2) = select(a_1270,i2),
inference(monotonicity,[status(thm)],[58]) ).
tff(355,plain,
select(store(a_1269,i0,e_1268),i2) = e_1310,
inference(transitivity,[status(thm)],[354,353,54]) ).
tff(356,plain,
( ( a_1309 = store(a_1307,i2,e_1308) )
<=> ( a_1309 = store(a_1307,i2,e_1308) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(357,axiom,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
tff(358,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(modus_ponens,[status(thm)],[357,356]) ).
tff(359,plain,
store(a_1307,i2,e_1308) = a_1309,
inference(symmetry,[status(thm)],[358]) ).
tff(360,plain,
( ( e_1308 = select(a_1307,i1) )
<=> ( e_1308 = select(a_1307,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(361,axiom,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).
tff(362,plain,
e_1308 = select(a_1307,i1),
inference(modus_ponens,[status(thm)],[361,360]) ).
tff(363,plain,
select(a_1307,i1) = e_1308,
inference(symmetry,[status(thm)],[362]) ).
tff(364,plain,
select(a_1307,i1) = select(a_1270,i1),
inference(monotonicity,[status(thm)],[351]) ).
tff(365,plain,
select(a_1270,i1) = select(a_1307,i1),
inference(symmetry,[status(thm)],[364]) ).
tff(366,plain,
select(store(a_1269,i0,e_1268),i1) = select(a_1270,i1),
inference(monotonicity,[status(thm)],[58]) ).
tff(367,plain,
select(store(a_1269,i0,e_1268),i1) = e_1308,
inference(transitivity,[status(thm)],[366,365,363]) ).
tff(368,plain,
store(a_1306,i0,e_1305) = a_1307,
inference(symmetry,[status(thm)],[350]) ).
tff(369,plain,
store(a_1269,i0,e_1268) = store(a_1306,i0,e_1305),
inference(symmetry,[status(thm)],[347]) ).
tff(370,plain,
store(a_1269,i0,e_1268) = a_1307,
inference(transitivity,[status(thm)],[369,368]) ).
tff(371,plain,
store(store(a_1269,i0,e_1268),i2,select(store(a_1269,i0,e_1268),i1)) = store(a_1307,i2,e_1308),
inference(monotonicity,[status(thm)],[370,367]) ).
tff(372,plain,
store(store(a_1269,i0,e_1268),i2,select(store(a_1269,i0,e_1268),i1)) = a_1309,
inference(transitivity,[status(thm)],[371,359]) ).
tff(373,plain,
store(store(store(a_1269,i0,e_1268),i2,select(store(a_1269,i0,e_1268),i1)),i1,select(store(a_1269,i0,e_1268),i2)) = store(a_1309,i1,e_1310),
inference(monotonicity,[status(thm)],[372,355]) ).
tff(374,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_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)),i2,select(store(a_1269,i0,e_1268),i1)) = store(store(store(a_1269,i0,e_1268),i2,select(store(a_1269,i0,e_1268),i1)),i1,select(store(a_1269,i0,e_1268),i2)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(375,plain,
store(store(store(a_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)),i2,select(store(a_1269,i0,e_1268),i1)) = store(store(store(a_1269,i0,e_1268),i2,select(store(a_1269,i0,e_1268),i1)),i1,select(store(a_1269,i0,e_1268),i2)),
inference(unit_resolution,[status(thm)],[374,35]) ).
tff(376,plain,
select(a_1270,i1) = select(store(a_1269,i0,e_1268),i1),
inference(symmetry,[status(thm)],[366]) ).
tff(377,plain,
( ( e_1273 = select(a_1270,i1) )
<=> ( e_1273 = select(a_1270,i1) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(378,axiom,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
tff(379,plain,
e_1273 = select(a_1270,i1),
inference(modus_ponens,[status(thm)],[378,377]) ).
tff(380,plain,
e_1273 = select(store(a_1269,i0,e_1268),i1),
inference(transitivity,[status(thm)],[379,376]) ).
tff(381,plain,
( ( e_1271 = select(a_1270,i2) )
<=> ( e_1271 = select(a_1270,i2) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(382,axiom,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).
tff(383,plain,
e_1271 = select(a_1270,i2),
inference(modus_ponens,[status(thm)],[382,381]) ).
tff(384,plain,
select(a_1270,i2) = e_1271,
inference(symmetry,[status(thm)],[383]) ).
tff(385,plain,
select(store(a_1269,i0,e_1268),i2) = e_1271,
inference(transitivity,[status(thm)],[354,384]) ).
tff(386,plain,
store(store(a_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)) = store(a_1270,i1,e_1271),
inference(monotonicity,[status(thm)],[58,385]) ).
tff(387,plain,
store(a_1270,i1,e_1271) = store(store(a_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)),
inference(symmetry,[status(thm)],[386]) ).
tff(388,plain,
( ( a_1272 = store(a_1270,i1,e_1271) )
<=> ( a_1272 = store(a_1270,i1,e_1271) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(389,axiom,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
tff(390,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(modus_ponens,[status(thm)],[389,388]) ).
tff(391,plain,
a_1272 = store(store(a_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)),
inference(transitivity,[status(thm)],[390,387]) ).
tff(392,plain,
store(a_1272,i2,e_1273) = store(store(store(a_1269,i0,e_1268),i1,select(store(a_1269,i0,e_1268),i2)),i2,select(store(a_1269,i0,e_1268),i1)),
inference(monotonicity,[status(thm)],[391,380]) ).
tff(393,plain,
( ( a_1274 = store(a_1272,i2,e_1273) )
<=> ( a_1274 = store(a_1272,i2,e_1273) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(394,axiom,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
tff(395,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(modus_ponens,[status(thm)],[394,393]) ).
tff(396,plain,
a_1274 = a_1311,
inference(transitivity,[status(thm)],[395,392,375,373,50]) ).
tff(397,plain,
select(a_1274,i3) = select(a_1311,i3),
inference(monotonicity,[status(thm)],[396]) ).
tff(398,plain,
( ( e_1277 = select(a_1274,i3) )
<=> ( e_1277 = select(a_1274,i3) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(399,axiom,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
tff(400,plain,
e_1277 = select(a_1274,i3),
inference(modus_ponens,[status(thm)],[399,398]) ).
tff(401,plain,
e_1277 = e_1314,
inference(transitivity,[status(thm)],[400,397,46]) ).
tff(402,plain,
( ( a_1313 = store(a_1311,i3,e_1312) )
<=> ( a_1313 = store(a_1311,i3,e_1312) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(403,axiom,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
tff(404,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(modus_ponens,[status(thm)],[403,402]) ).
tff(405,plain,
store(a_1311,i3,e_1312) = a_1313,
inference(symmetry,[status(thm)],[404]) ).
tff(406,plain,
( ( e_1312 = select(a_1311,i0) )
<=> ( e_1312 = select(a_1311,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(407,axiom,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
tff(408,plain,
e_1312 = select(a_1311,i0),
inference(modus_ponens,[status(thm)],[407,406]) ).
tff(409,plain,
select(a_1311,i0) = e_1312,
inference(symmetry,[status(thm)],[408]) ).
tff(410,plain,
select(a_1274,i0) = select(a_1311,i0),
inference(monotonicity,[status(thm)],[396]) ).
tff(411,plain,
( ( e_1275 = select(a_1274,i0) )
<=> ( e_1275 = select(a_1274,i0) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(412,axiom,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp55) ).
tff(413,plain,
e_1275 = select(a_1274,i0),
inference(modus_ponens,[status(thm)],[412,411]) ).
tff(414,plain,
e_1275 = e_1312,
inference(transitivity,[status(thm)],[413,410,409]) ).
tff(415,plain,
store(a_1274,i3,e_1275) = store(a_1311,i3,e_1312),
inference(monotonicity,[status(thm)],[396,414]) ).
tff(416,plain,
( ( a_1276 = store(a_1274,i3,e_1275) )
<=> ( a_1276 = store(a_1274,i3,e_1275) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(417,axiom,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
tff(418,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(modus_ponens,[status(thm)],[417,416]) ).
tff(419,plain,
a_1276 = a_1313,
inference(transitivity,[status(thm)],[418,415,405]) ).
tff(420,plain,
store(a_1276,i0,e_1277) = store(a_1313,i0,e_1314),
inference(monotonicity,[status(thm)],[419,401]) ).
tff(421,plain,
( ( a_1278 = store(a_1276,i0,e_1277) )
<=> ( a_1278 = store(a_1276,i0,e_1277) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(422,axiom,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
tff(423,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(modus_ponens,[status(thm)],[422,421]) ).
tff(424,plain,
a_1278 = a_1315,
inference(transitivity,[status(thm)],[423,420,8]) ).
tff(425,plain,
select(a_1278,i9) = select(a_1315,i9),
inference(monotonicity,[status(thm)],[424]) ).
tff(426,plain,
select(a_1315,i9) = select(a_1278,i9),
inference(symmetry,[status(thm)],[425]) ).
tff(427,plain,
select(store(a_1313,i0,e_1314),i9) = e_1281,
inference(transitivity,[status(thm)],[19,426,42]) ).
tff(428,plain,
( ( a_1280 = store(a_1278,i9,e_1279) )
<=> ( a_1280 = store(a_1278,i9,e_1279) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(429,axiom,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
tff(430,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(modus_ponens,[status(thm)],[429,428]) ).
tff(431,plain,
store(a_1278,i9,e_1279) = a_1280,
inference(symmetry,[status(thm)],[430]) ).
tff(432,plain,
( ( e_1279 = select(a_1278,i5) )
<=> ( e_1279 = select(a_1278,i5) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(433,axiom,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).
tff(434,plain,
e_1279 = select(a_1278,i5),
inference(modus_ponens,[status(thm)],[433,432]) ).
tff(435,plain,
select(a_1278,i5) = e_1279,
inference(symmetry,[status(thm)],[434]) ).
tff(436,plain,
select(a_1278,i5) = select(a_1315,i5),
inference(monotonicity,[status(thm)],[424]) ).
tff(437,plain,
select(a_1315,i5) = select(a_1278,i5),
inference(symmetry,[status(thm)],[436]) ).
tff(438,plain,
select(store(a_1313,i0,e_1314),i5) = e_1279,
inference(transitivity,[status(thm)],[9,437,435]) ).
tff(439,plain,
store(a_1276,i0,e_1277) = a_1278,
inference(symmetry,[status(thm)],[423]) ).
tff(440,plain,
store(a_1313,i0,e_1314) = store(a_1276,i0,e_1277),
inference(symmetry,[status(thm)],[420]) ).
tff(441,plain,
store(a_1313,i0,e_1314) = a_1278,
inference(transitivity,[status(thm)],[440,439]) ).
tff(442,plain,
store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)) = store(a_1278,i9,e_1279),
inference(monotonicity,[status(thm)],[441,438]) ).
tff(443,plain,
store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)) = a_1280,
inference(transitivity,[status(thm)],[442,431]) ).
tff(444,plain,
store(store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)),i5,select(store(a_1313,i0,e_1314),i9)) = store(a_1280,i5,e_1281),
inference(monotonicity,[status(thm)],[443,427]) ).
tff(445,plain,
store(a_1280,i5,e_1281) = store(store(store(a_1313,i0,e_1314),i9,select(store(a_1313,i0,e_1314),i5)),i5,select(store(a_1313,i0,e_1314),i9)),
inference(symmetry,[status(thm)],[444]) ).
tff(446,plain,
( ( a_1282 = store(a_1280,i5,e_1281) )
<=> ( a_1282 = store(a_1280,i5,e_1281) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(447,axiom,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
tff(448,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(modus_ponens,[status(thm)],[447,446]) ).
tff(449,plain,
a_1282 = a_1319,
inference(transitivity,[status(thm)],[448,445,38,28,4]) ).
tff(450,plain,
( ( a_1282 != a_1319 )
<=> ( a_1282 != a_1319 ) ),
inference(rewrite,[status(thm)],[]) ).
tff(451,axiom,
a_1282 != a_1319,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tff(452,plain,
a_1282 != a_1319,
inference(modus_ponens,[status(thm)],[451,450]) ).
tff(453,plain,
$false,
inference(unit_resolution,[status(thm)],[452,449]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV543-1.010 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.13/0.33 % Computer : n004.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri Jun 20 10:14:23 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.38 % SZS status Unsatisfiable
% 0.13/0.38 % SZS output start Proof
% See solution above
% 0.20/0.43 % E exiting
%------------------------------------------------------------------------------