%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV534-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:51:36 PM UTC 2026
% Result : Satisfiable 0.13s 0.61s
% Output : Saturation 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,hypothesis,
a_1246 = store(a1,i8,e_1245),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_1248 = store(a_1246,i7,e_1247),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_1250 = store(a_1248,i6,e_1249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_1252 = store(a_1250,i8,e_1251),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_1254 = store(a_1252,i8,e_1253),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_1256 = store(a_1254,i5,e_1255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_1258 = store(a_1256,i4,e_1257),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_1260 = store(a_1258,i9,e_1259),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_1262 = store(a_1260,i7,e_1261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_1264 = store(a_1262,i1,e_1263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_1266 = store(a_1264,i4,e_1265),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_1268 = store(a_1266,i5,e_1267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_1270 = store(a_1268,i0,e_1269),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_1271 = store(a_1270,i0,e_1269),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_1273 = store(a_1271,i1,e_1272),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_1275 = store(a_1273,i2,e_1274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_1277 = store(a_1275,i3,e_1276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
a_1279 = store(a_1277,i0,e_1278),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
a_1281 = store(a_1279,i9,e_1280),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
a_1283 = store(a_1281,i5,e_1282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
a_1284 = store(a1,i7,e_1247),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
a_1285 = store(a_1284,i8,e_1245),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
a_1287 = store(a_1285,i6,e_1286),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
a_1289 = store(a_1287,i8,e_1288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
a_1291 = store(a_1289,i5,e_1290),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
a_1293 = store(a_1291,i8,e_1292),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
a_1295 = store(a_1293,i4,e_1294),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
a_1297 = store(a_1295,i9,e_1296),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
a_1299 = store(a_1297,i1,e_1298),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
a_1301 = store(a_1299,i7,e_1300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
a_1303 = store(a_1301,i4,e_1302),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
a_1305 = store(a_1303,i5,e_1304),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
a_1307 = store(a_1305,i0,e_1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
a_1308 = store(a_1307,i0,e_1306),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
a_1310 = store(a_1308,i2,e_1309),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
a_1312 = store(a_1310,i1,e_1311),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
a_1314 = store(a_1312,i3,e_1313),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
a_1316 = store(a_1314,i0,e_1315),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
a_1318 = store(a_1316,i6,e_1317),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
a_1320 = store(a_1318,i9,e_1319),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
e_1245 = select(a1,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
e_1247 = select(a1,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
e_1249 = select(a_1248,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
e_1251 = select(a_1248,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
e_1253 = select(a_1252,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
e_1255 = select(a_1252,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
e_1257 = select(a_1256,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
e_1259 = select(a_1256,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
e_1261 = select(a_1260,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
e_1263 = select(a_1260,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
e_1265 = select(a_1264,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
e_1267 = select(a_1264,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
e_1269 = select(a_1268,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
e_1272 = select(a_1271,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
e_1274 = select(a_1271,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,hypothesis,
e_1276 = select(a_1275,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,hypothesis,
e_1278 = select(a_1275,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,hypothesis,
e_1280 = select(a_1279,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,hypothesis,
e_1282 = select(a_1279,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,hypothesis,
e_1286 = select(a_1285,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,hypothesis,
e_1288 = select(a_1285,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,hypothesis,
e_1290 = select(a_1289,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
e_1292 = select(a_1289,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,hypothesis,
e_1294 = select(a_1293,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
e_1296 = select(a_1293,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,hypothesis,
e_1298 = select(a_1297,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
e_1300 = select(a_1297,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
e_1302 = select(a_1301,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
e_1304 = select(a_1301,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
e_1306 = select(a_1305,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
e_1309 = select(a_1308,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
e_1311 = select(a_1308,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
e_1313 = select(a_1312,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
e_1315 = select(a_1312,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
e_1317 = select(a_1316,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
e_1319 = select(a_1316,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
a_1283 != a_1320,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f81,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
a_1246 = store(a1,i8,e_1245),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f84,plain,
a_1248 = store(a_1246,i7,e_1247),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f85,plain,
a_1250 = store(a_1248,i6,e_1249),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f86,plain,
a_1252 = store(a_1250,i8,e_1251),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f87,plain,
a_1254 = store(a_1252,i8,e_1253),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f88,plain,
a_1256 = store(a_1254,i5,e_1255),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f89,plain,
a_1258 = store(a_1256,i4,e_1257),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f90,plain,
a_1260 = store(a_1258,i9,e_1259),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f91,plain,
a_1262 = store(a_1260,i7,e_1261),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f92,plain,
a_1264 = store(a_1262,i1,e_1263),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f93,plain,
a_1266 = store(a_1264,i4,e_1265),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f94,plain,
a_1268 = store(a_1266,i5,e_1267),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f95,plain,
a_1270 = store(a_1268,i0,e_1269),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f96,plain,
a_1271 = store(a_1270,i0,e_1269),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f97,plain,
a_1273 = store(a_1271,i1,e_1272),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f98,plain,
a_1275 = store(a_1273,i2,e_1274),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f99,plain,
a_1277 = store(a_1275,i3,e_1276),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f100,plain,
a_1279 = store(a_1277,i0,e_1278),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f101,plain,
a_1281 = store(a_1279,i9,e_1280),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f102,plain,
a_1283 = store(a_1281,i5,e_1282),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f103,plain,
a_1284 = store(a1,i7,e_1247),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f104,plain,
a_1285 = store(a_1284,i8,e_1245),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f105,plain,
a_1287 = store(a_1285,i6,e_1286),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f106,plain,
a_1289 = store(a_1287,i8,e_1288),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f107,plain,
a_1291 = store(a_1289,i5,e_1290),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f108,plain,
a_1293 = store(a_1291,i8,e_1292),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f109,plain,
a_1295 = store(a_1293,i4,e_1294),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f110,plain,
a_1297 = store(a_1295,i9,e_1296),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f111,plain,
a_1299 = store(a_1297,i1,e_1298),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f112,plain,
a_1301 = store(a_1299,i7,e_1300),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f113,plain,
a_1303 = store(a_1301,i4,e_1302),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f114,plain,
a_1305 = store(a_1303,i5,e_1304),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f115,plain,
a_1307 = store(a_1305,i0,e_1306),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f116,plain,
a_1308 = store(a_1307,i0,e_1306),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f117,plain,
a_1310 = store(a_1308,i2,e_1309),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f118,plain,
a_1312 = store(a_1310,i1,e_1311),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f119,plain,
a_1314 = store(a_1312,i3,e_1313),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f120,plain,
a_1316 = store(a_1314,i0,e_1315),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f121,plain,
a_1318 = store(a_1316,i6,e_1317),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f122,plain,
a_1320 = store(a_1318,i9,e_1319),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f123,plain,
e_1245 = select(a1,i7),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f124,plain,
e_1247 = select(a1,i8),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f125,plain,
e_1249 = select(a_1248,i8),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f126,plain,
e_1251 = select(a_1248,i6),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f127,plain,
e_1253 = select(a_1252,i5),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f128,plain,
e_1255 = select(a_1252,i8),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f129,plain,
e_1257 = select(a_1256,i9),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f130,plain,
e_1259 = select(a_1256,i4),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f131,plain,
e_1261 = select(a_1260,i1),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f132,plain,
e_1263 = select(a_1260,i7),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f133,plain,
e_1265 = select(a_1264,i5),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f134,plain,
e_1267 = select(a_1264,i4),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f135,plain,
e_1269 = select(a_1268,i0),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f136,plain,
e_1272 = select(a_1271,i2),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f137,plain,
e_1274 = select(a_1271,i1),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f138,plain,
e_1276 = select(a_1275,i0),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f139,plain,
e_1278 = select(a_1275,i3),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f140,plain,
e_1280 = select(a_1279,i5),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f141,plain,
e_1282 = select(a_1279,i9),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f142,plain,
e_1286 = select(a_1285,i8),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f143,plain,
e_1288 = select(a_1285,i6),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f144,plain,
e_1290 = select(a_1289,i8),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f145,plain,
e_1292 = select(a_1289,i5),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f146,plain,
e_1294 = select(a_1293,i9),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f147,plain,
e_1296 = select(a_1293,i4),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f148,plain,
e_1298 = select(a_1297,i7),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f149,plain,
e_1300 = select(a_1297,i1),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f150,plain,
e_1302 = select(a_1301,i5),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f151,plain,
e_1304 = select(a_1301,i4),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f152,plain,
e_1306 = select(a_1305,i0),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f153,plain,
e_1309 = select(a_1308,i1),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f154,plain,
e_1311 = select(a_1308,i2),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f155,plain,
e_1313 = select(a_1312,i0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f156,plain,
e_1315 = select(a_1312,i3),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f157,plain,
e_1317 = select(a_1316,i9),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f158,plain,
e_1319 = select(a_1316,i6),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f159,plain,
a_1283 != a_1320,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f160,plain,
select(a_1320,i9) = e_1319,
inference(paramodulation,[status(thm)],[f122,f80]) ).
fof(f161,plain,
select(a_1283,i5) = e_1282,
inference(paramodulation,[status(thm)],[f102,f80]) ).
fof(f163,plain,
! [X0] :
( select(a_1320,X0) = select(a_1318,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f122,f82]) ).
fof(f164,plain,
! [X0] :
( select(a_1283,X0) = select(a_1281,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f102,f82]) ).
fof(f166,plain,
! [X0] :
( select(a_1246,X0) = select(a1,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f83,f82]) ).
fof(f167,plain,
select(a_1246,i8) = e_1245,
inference(paramodulation,[status(thm)],[f83,f80]) ).
fof(f168,plain,
! [X0] :
( select(a_1248,X0) = select(a_1246,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f84,f82]) ).
fof(f169,plain,
select(a_1248,i7) = e_1247,
inference(paramodulation,[status(thm)],[f84,f80]) ).
fof(f174,plain,
! [X0] :
( select(a_1250,X0) = select(a_1248,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f85,f82]) ).
fof(f175,plain,
select(a_1250,i6) = e_1249,
inference(paramodulation,[status(thm)],[f85,f80]) ).
fof(f176,plain,
! [X0] :
( select(a_1252,X0) = select(a_1250,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f86,f82]) ).
fof(f177,plain,
select(a_1252,i8) = e_1251,
inference(paramodulation,[status(thm)],[f86,f80]) ).
fof(f178,plain,
e_1255 = e_1251,
inference(backward_demodulation,[status(thm)],[f177,f128]) ).
fof(f179,plain,
a_1256 = store(a_1254,i5,e_1251),
inference(backward_demodulation,[status(thm)],[f178,f88]) ).
fof(f180,plain,
! [X0] :
( select(a_1254,X0) = select(a_1252,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f87,f82]) ).
fof(f181,plain,
select(a_1254,i8) = e_1253,
inference(paramodulation,[status(thm)],[f87,f80]) ).
fof(f182,plain,
! [X0] :
( select(a_1258,X0) = select(a_1256,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f89,f82]) ).
fof(f183,plain,
select(a_1258,i4) = e_1257,
inference(paramodulation,[status(thm)],[f89,f80]) ).
fof(f184,plain,
! [X0] :
( select(a_1260,X0) = select(a_1258,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f90,f82]) ).
fof(f185,plain,
select(a_1260,i9) = e_1259,
inference(paramodulation,[status(thm)],[f90,f80]) ).
fof(f186,plain,
! [X0] :
( select(a_1262,X0) = select(a_1260,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f91,f82]) ).
fof(f187,plain,
select(a_1262,i7) = e_1261,
inference(paramodulation,[status(thm)],[f91,f80]) ).
fof(f188,plain,
! [X0] :
( select(a_1264,X0) = select(a_1262,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f92,f82]) ).
fof(f189,plain,
select(a_1264,i1) = e_1263,
inference(paramodulation,[status(thm)],[f92,f80]) ).
fof(f190,plain,
! [X0] :
( select(a_1266,X0) = select(a_1264,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f93,f82]) ).
fof(f191,plain,
select(a_1266,i4) = e_1265,
inference(paramodulation,[status(thm)],[f93,f80]) ).
fof(f192,plain,
! [X0] :
( select(a_1268,X0) = select(a_1266,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f94,f82]) ).
fof(f193,plain,
select(a_1268,i5) = e_1267,
inference(paramodulation,[status(thm)],[f94,f80]) ).
fof(f194,plain,
! [X0] :
( select(a_1270,X0) = select(a_1268,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f95,f82]) ).
fof(f195,plain,
select(a_1270,i0) = e_1269,
inference(paramodulation,[status(thm)],[f95,f80]) ).
fof(f196,plain,
! [X0] :
( select(a_1271,X0) = select(a_1270,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f96,f82]) ).
fof(f197,plain,
select(a_1271,i0) = e_1269,
inference(paramodulation,[status(thm)],[f96,f80]) ).
fof(f198,plain,
! [X0] :
( select(a_1273,X0) = select(a_1271,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f97,f82]) ).
fof(f199,plain,
select(a_1273,i1) = e_1272,
inference(paramodulation,[status(thm)],[f97,f80]) ).
fof(f200,plain,
! [X0] :
( select(a_1275,X0) = select(a_1273,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f98,f82]) ).
fof(f201,plain,
select(a_1275,i2) = e_1274,
inference(paramodulation,[status(thm)],[f98,f80]) ).
fof(f202,plain,
! [X0] :
( select(a_1277,X0) = select(a_1275,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f99,f82]) ).
fof(f203,plain,
select(a_1277,i3) = e_1276,
inference(paramodulation,[status(thm)],[f99,f80]) ).
fof(f204,plain,
! [X0] :
( select(a_1279,X0) = select(a_1277,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f100,f82]) ).
fof(f205,plain,
select(a_1279,i0) = e_1278,
inference(paramodulation,[status(thm)],[f100,f80]) ).
fof(f206,plain,
! [X0] :
( select(a_1281,X0) = select(a_1279,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f101,f82]) ).
fof(f207,plain,
select(a_1281,i9) = e_1280,
inference(paramodulation,[status(thm)],[f101,f80]) ).
fof(f208,plain,
! [X0] :
( select(a_1284,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f103,f82]) ).
fof(f209,plain,
select(a_1284,i7) = e_1247,
inference(paramodulation,[status(thm)],[f103,f80]) ).
fof(f210,plain,
! [X0] :
( select(a_1285,X0) = select(a_1284,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f104,f82]) ).
fof(f211,plain,
select(a_1285,i8) = e_1245,
inference(paramodulation,[status(thm)],[f104,f80]) ).
fof(f212,plain,
e_1286 = e_1245,
inference(backward_demodulation,[status(thm)],[f211,f142]) ).
fof(f213,plain,
a_1287 = store(a_1285,i6,e_1245),
inference(backward_demodulation,[status(thm)],[f212,f105]) ).
fof(f214,plain,
! [X0] :
( select(a_1289,X0) = select(a_1287,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f106,f82]) ).
fof(f215,plain,
select(a_1289,i8) = e_1288,
inference(paramodulation,[status(thm)],[f106,f80]) ).
fof(f216,plain,
e_1290 = e_1288,
inference(backward_demodulation,[status(thm)],[f215,f144]) ).
fof(f217,plain,
a_1291 = store(a_1289,i5,e_1288),
inference(backward_demodulation,[status(thm)],[f216,f107]) ).
fof(f218,plain,
! [X0] :
( select(a_1293,X0) = select(a_1291,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f108,f82]) ).
fof(f219,plain,
select(a_1293,i8) = e_1292,
inference(paramodulation,[status(thm)],[f108,f80]) ).
fof(f220,plain,
! [X0] :
( select(a_1295,X0) = select(a_1293,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f109,f82]) ).
fof(f221,plain,
select(a_1295,i4) = e_1294,
inference(paramodulation,[status(thm)],[f109,f80]) ).
fof(f222,plain,
! [X0] :
( select(a_1297,X0) = select(a_1295,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f110,f82]) ).
fof(f223,plain,
select(a_1297,i9) = e_1296,
inference(paramodulation,[status(thm)],[f110,f80]) ).
fof(f224,plain,
! [X0] :
( select(a_1299,X0) = select(a_1297,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f111,f82]) ).
fof(f225,plain,
select(a_1299,i1) = e_1298,
inference(paramodulation,[status(thm)],[f111,f80]) ).
fof(f226,plain,
! [X0] :
( select(a_1301,X0) = select(a_1299,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f112,f82]) ).
fof(f227,plain,
select(a_1301,i7) = e_1300,
inference(paramodulation,[status(thm)],[f112,f80]) ).
fof(f228,plain,
! [X0] :
( select(a_1303,X0) = select(a_1301,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f113,f82]) ).
fof(f229,plain,
select(a_1303,i4) = e_1302,
inference(paramodulation,[status(thm)],[f113,f80]) ).
fof(f230,plain,
! [X0] :
( select(a_1305,X0) = select(a_1303,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f114,f82]) ).
fof(f231,plain,
select(a_1305,i5) = e_1304,
inference(paramodulation,[status(thm)],[f114,f80]) ).
fof(f232,plain,
! [X0] :
( select(a_1307,X0) = select(a_1305,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f115,f82]) ).
fof(f233,plain,
select(a_1307,i0) = e_1306,
inference(paramodulation,[status(thm)],[f115,f80]) ).
fof(f234,plain,
! [X0] :
( select(a_1308,X0) = select(a_1307,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f116,f82]) ).
fof(f235,plain,
select(a_1308,i0) = e_1306,
inference(paramodulation,[status(thm)],[f116,f80]) ).
fof(f236,plain,
! [X0] :
( select(a_1310,X0) = select(a_1308,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f117,f82]) ).
fof(f237,plain,
select(a_1310,i2) = e_1309,
inference(paramodulation,[status(thm)],[f117,f80]) ).
fof(f238,plain,
! [X0] :
( select(a_1312,X0) = select(a_1310,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f118,f82]) ).
fof(f239,plain,
select(a_1312,i1) = e_1311,
inference(paramodulation,[status(thm)],[f118,f80]) ).
fof(f240,plain,
! [X0] :
( select(a_1314,X0) = select(a_1312,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f119,f82]) ).
fof(f241,plain,
select(a_1314,i3) = e_1313,
inference(paramodulation,[status(thm)],[f119,f80]) ).
fof(f242,plain,
! [X0] :
( select(a_1316,X0) = select(a_1314,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f120,f82]) ).
fof(f243,plain,
select(a_1316,i0) = e_1315,
inference(paramodulation,[status(thm)],[f120,f80]) ).
fof(f244,plain,
! [X0] :
( select(a_1318,X0) = select(a_1316,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f121,f82]) ).
fof(f245,plain,
select(a_1318,i6) = e_1317,
inference(paramodulation,[status(thm)],[f121,f80]) ).
fof(f246,plain,
! [X0] :
( select(a_1256,X0) = select(a_1254,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f179,f82]) ).
fof(f247,plain,
select(a_1256,i5) = e_1251,
inference(paramodulation,[status(thm)],[f179,f80]) ).
fof(f248,plain,
! [X0] :
( select(a_1287,X0) = select(a_1285,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f213,f82]) ).
fof(f249,plain,
select(a_1287,i6) = e_1245,
inference(paramodulation,[status(thm)],[f213,f80]) ).
fof(f250,plain,
! [X0] :
( select(a_1291,X0) = select(a_1289,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f217,f82]) ).
fof(f251,plain,
select(a_1291,i5) = e_1288,
inference(paramodulation,[status(thm)],[f217,f80]) ).
fof(f253,plain,
( select(a_1246,i7) = e_1245
| i8 = i7 ),
inference(paramodulation,[status(thm)],[f123,f166]) ).
fof(f257,plain,
( e_1251 = select(a_1246,i6)
| i7 = i6 ),
inference(paramodulation,[status(thm)],[f126,f168]) ).
fof(f258,plain,
( e_1249 = select(a_1246,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f125,f168]) ).
fof(f262,plain,
( e_1249 = e_1245
| i7 = i8 ),
inference(forward_demodulation,[status(thm)],[f167,f258]) ).
fof(f266,plain,
( i7 = i8
| a_1250 = store(a_1248,i6,e_1245) ),
inference(paramodulation,[status(thm)],[f262,f85]) ).
fof(f268,plain,
( e_1253 = select(a_1250,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f127,f176]) ).
fof(f271,plain,
( i6 = i5
| e_1253 = select(a_1248,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f174,f268]) ).
fof(f278,plain,
( e_1263 = select(a_1258,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f132,f184]) ).
fof(f279,plain,
( e_1261 = select(a_1258,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f131,f184]) ).
fof(f283,plain,
( i4 = i7
| e_1263 = select(a_1256,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f182,f278]) ).
fof(f285,plain,
( i4 = i1
| e_1261 = select(a_1256,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f182,f279]) ).
fof(f290,plain,
( e_1267 = select(a_1262,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f134,f188]) ).
fof(f291,plain,
( e_1265 = select(a_1262,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f133,f188]) ).
fof(f295,plain,
( i7 = i4
| e_1267 = select(a_1260,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f186,f290]) ).
fof(f297,plain,
( i7 = i5
| e_1265 = select(a_1260,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f186,f291]) ).
fof(f302,plain,
( e_1269 = select(a_1266,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f135,f192]) ).
fof(f307,plain,
( i4 = i0
| e_1269 = select(a_1264,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f190,f302]) ).
fof(f310,plain,
( e_1274 = select(a_1270,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f137,f196]) ).
fof(f311,plain,
( e_1272 = select(a_1270,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f136,f196]) ).
fof(f317,plain,
( i0 = i1
| e_1274 = select(a_1268,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f194,f310]) ).
fof(f319,plain,
( e_1274 = select(a_1268,i1)
| i0 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f317]) ).
fof(f321,plain,
( i0 = i2
| e_1272 = select(a_1268,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f194,f311]) ).
fof(f323,plain,
( e_1272 = select(a_1268,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f321]) ).
fof(f325,plain,
( i5 = i1
| e_1274 = select(a_1266,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f192,f319]) ).
fof(f327,plain,
( i5 = i2
| e_1272 = select(a_1266,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f192,f323]) ).
fof(f330,plain,
( e_1278 = select(a_1273,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f139,f200]) ).
fof(f331,plain,
( e_1276 = select(a_1273,i0)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f138,f200]) ).
fof(f337,plain,
( i1 = i3
| e_1278 = select(a_1271,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f198,f330]) ).
fof(f339,plain,
( i1 = i0
| e_1276 = select(a_1271,i0)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f198,f331]) ).
fof(f341,plain,
( i1 = i0
| e_1276 = e_1269
| i2 = i0 ),
inference(forward_demodulation,[status(thm)],[f197,f339]) ).
fof(f343,plain,
( i1 = i0
| i2 = i0
| a_1277 = store(a_1275,i3,e_1269) ),
inference(paramodulation,[status(thm)],[f341,f99]) ).
fof(f345,plain,
( e_1282 = select(a_1277,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f141,f204]) ).
fof(f346,plain,
( e_1280 = select(a_1277,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f140,f204]) ).
fof(f350,plain,
( i3 = i9
| e_1282 = select(a_1275,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f202,f345]) ).
fof(f352,plain,
( i3 = i5
| e_1280 = select(a_1275,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f202,f346]) ).
fof(f359,plain,
( e_1288 = select(a_1284,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f143,f210]) ).
fof(f362,plain,
( i7 = i6
| e_1288 = select(a1,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f208,f359]) ).
fof(f365,plain,
( e_1292 = select(a_1287,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f145,f214]) ).
fof(f369,plain,
( e_1296 = select(a_1291,i4)
| i8 = i4 ),
inference(paramodulation,[status(thm)],[f147,f218]) ).
fof(f370,plain,
( e_1294 = select(a_1291,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f146,f218]) ).
fof(f377,plain,
( e_1300 = select(a_1295,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f149,f222]) ).
fof(f378,plain,
( e_1298 = select(a_1295,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f148,f222]) ).
fof(f384,plain,
( i4 = i1
| e_1300 = select(a_1293,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f220,f377]) ).
fof(f386,plain,
( i4 = i7
| e_1298 = select(a_1293,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f220,f378]) ).
fof(f389,plain,
( e_1304 = select(a_1299,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f151,f226]) ).
fof(f390,plain,
( e_1302 = select(a_1299,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f150,f226]) ).
fof(f394,plain,
( i1 = i4
| e_1304 = select(a_1297,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f224,f389]) ).
fof(f396,plain,
( i1 = i5
| e_1302 = select(a_1297,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f224,f390]) ).
fof(f401,plain,
( e_1306 = select(a_1303,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f152,f230]) ).
fof(f407,plain,
( e_1311 = select(a_1307,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f154,f234]) ).
fof(f408,plain,
( e_1309 = select(a_1307,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f153,f234]) ).
fof(f412,plain,
( i4 = i0
| e_1306 = select(a_1301,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f228,f401]) ).
fof(f414,plain,
( i0 = i2
| e_1311 = select(a_1305,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f232,f407]) ).
fof(f416,plain,
( e_1311 = select(a_1305,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f414]) ).
fof(f420,plain,
( i0 = i1
| e_1309 = select(a_1305,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f232,f408]) ).
fof(f422,plain,
( e_1309 = select(a_1305,i1)
| i0 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f420]) ).
fof(f424,plain,
( i5 = i2
| e_1311 = select(a_1303,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f230,f416]) ).
fof(f426,plain,
( i5 = i1
| e_1309 = select(a_1303,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f230,f422]) ).
fof(f429,plain,
( e_1315 = select(a_1310,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f156,f238]) ).
fof(f430,plain,
( e_1313 = select(a_1310,i0)
| i1 = i0 ),
inference(paramodulation,[status(thm)],[f155,f238]) ).
fof(f437,plain,
( e_1319 = select(a_1314,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f158,f242]) ).
fof(f438,plain,
( e_1317 = select(a_1314,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f157,f242]) ).
fof(f442,plain,
( i2 = i3
| e_1315 = select(a_1308,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f236,f429]) ).
fof(f444,plain,
( i2 = i0
| e_1313 = select(a_1308,i0)
| i1 = i0 ),
inference(paramodulation,[status(thm)],[f236,f430]) ).
fof(f446,plain,
( i2 = i0
| e_1313 = e_1306
| i1 = i0 ),
inference(forward_demodulation,[status(thm)],[f235,f444]) ).
fof(f448,plain,
( i3 = i6
| e_1319 = select(a_1312,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f240,f437]) ).
fof(f450,plain,
( i3 = i9
| e_1317 = select(a_1312,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f240,f438]) ).
fof(f452,plain,
( i2 = i0
| i1 = i0
| a_1314 = store(a_1312,i3,e_1306) ),
inference(paramodulation,[status(thm)],[f446,f119]) ).
fof(f456,plain,
( e_1259 = select(a_1254,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f130,f246]) ).
fof(f457,plain,
( e_1257 = select(a_1254,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f129,f246]) ).
fof(f461,plain,
( i8 = i5
| e_1292 = select(a_1285,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f365,f248]) ).
fof(f465,plain,
( i8 = i9
| e_1294 = select(a_1289,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f370,f250]) ).
fof(f466,plain,
( i8 = i4
| e_1296 = select(a_1289,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f369,f250]) ).
fof(f471,plain,
( i8 = i4
| e_1259 = select(a_1252,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f180,f456]) ).
fof(f473,plain,
( i8 = i9
| e_1257 = select(a_1252,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f180,f457]) ).
fof(f478,plain,
( i7 = i5
| i6 = i5
| e_1253 = select(a_1246,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f168,f271]) ).
fof(f480,plain,
( i5 = i7
| i4 = i7
| e_1263 = select(a_1254,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f246,f283]) ).
fof(f482,plain,
( i5 = i1
| i4 = i1
| e_1261 = select(a_1254,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f246,f285]) ).
fof(f484,plain,
( i9 = i4
| i7 = i4
| e_1267 = select(a_1258,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f184,f295]) ).
fof(f486,plain,
( i9 = i4
| i7 = i4
| e_1267 = e_1257
| i1 = i4 ),
inference(forward_demodulation,[status(thm)],[f183,f484]) ).
fof(f488,plain,
( i9 = i5
| i7 = i5
| e_1265 = select(a_1258,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f184,f297]) ).
fof(f490,plain,
( i1 = i0
| i4 = i0
| e_1269 = select(a_1262,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f188,f307]) ).
fof(f492,plain,
( i4 = i1
| i5 = i1
| e_1274 = select(a_1264,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f190,f325]) ).
fof(f494,plain,
( i4 = i1
| i5 = i1
| e_1274 = e_1263
| i0 = i1 ),
inference(forward_demodulation,[status(thm)],[f189,f492]) ).
fof(f496,plain,
( i4 = i2
| i5 = i2
| e_1272 = select(a_1264,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f190,f327]) ).
fof(f498,plain,
( i0 = i3
| i1 = i3
| e_1278 = select(a_1270,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f196,f337]) ).
fof(f500,plain,
( i2 = i9
| i3 = i9
| e_1282 = select(a_1273,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f200,f350]) ).
fof(f502,plain,
( i2 = i5
| i3 = i5
| e_1280 = select(a_1273,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f200,f352]) ).
fof(f504,plain,
( i8 = i6
| i7 = i6
| e_1288 = select(a_1246,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f166,f362]) ).
fof(f506,plain,
( i7 = i6
| e_1288 = select(a_1246,i6)
| i8 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f504]) ).
fof(f508,plain,
( i8 = i1
| i4 = i1
| e_1300 = select(a_1291,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f218,f384]) ).
fof(f510,plain,
( i8 = i7
| i4 = i7
| e_1298 = select(a_1291,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f218,f386]) ).
fof(f512,plain,
( i9 = i4
| i1 = i4
| e_1304 = select(a_1295,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f222,f394]) ).
fof(f514,plain,
( i9 = i4
| i1 = i4
| e_1304 = e_1294
| i7 = i4 ),
inference(forward_demodulation,[status(thm)],[f221,f512]) ).
fof(f516,plain,
( i9 = i5
| i1 = i5
| e_1302 = select(a_1295,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f222,f396]) ).
fof(f518,plain,
( i7 = i0
| i4 = i0
| e_1306 = select(a_1299,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f226,f412]) ).
fof(f520,plain,
( i0 = i3
| i2 = i3
| e_1315 = select(a_1307,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f234,f442]) ).
fof(f522,plain,
( i4 = i2
| i5 = i2
| e_1311 = select(a_1301,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f228,f424]) ).
fof(f524,plain,
( i4 = i1
| i5 = i1
| e_1309 = select(a_1301,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f228,f426]) ).
fof(f526,plain,
( i1 = i6
| i3 = i6
| e_1319 = select(a_1310,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f238,f448]) ).
fof(f528,plain,
( i1 = i9
| i3 = i9
| e_1317 = select(a_1310,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f238,f450]) ).
fof(f530,plain,
( i8 = i5
| i8 = i5
| e_1292 = select(a_1284,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f210,f461]) ).
fof(f532,plain,
( i8 = i5
| e_1292 = select(a_1284,i5)
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f530]) ).
fof(f534,plain,
( i8 = i9
| i8 = i9
| e_1294 = select(a_1287,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f214,f465]) ).
fof(f536,plain,
( i8 = i9
| e_1294 = select(a_1287,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f534]) ).
fof(f538,plain,
( i8 = i4
| i8 = i4
| e_1296 = select(a_1287,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f214,f466]) ).
fof(f540,plain,
( i8 = i4
| e_1296 = select(a_1287,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f538]) ).
fof(f542,plain,
( i8 = i4
| i8 = i4
| e_1259 = select(a_1250,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f176,f471]) ).
fof(f544,plain,
( i8 = i4
| e_1259 = select(a_1250,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f542]) ).
fof(f546,plain,
( i8 = i9
| i8 = i9
| e_1257 = select(a_1250,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f176,f473]) ).
fof(f548,plain,
( i8 = i9
| e_1257 = select(a_1250,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f546]) ).
fof(f550,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| a_1268 = store(a_1266,i5,e_1257) ),
inference(paramodulation,[status(thm)],[f486,f94]) ).
fof(f551,plain,
( i4 = i1
| i5 = i1
| i0 = i1
| a_1275 = store(a_1273,i2,e_1263) ),
inference(paramodulation,[status(thm)],[f494,f98]) ).
fof(f552,plain,
( i7 = i6
| i7 = i6
| e_1288 = e_1251
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f257,f506]) ).
fof(f554,plain,
( i7 = i6
| e_1288 = e_1251
| i8 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f552]) ).
fof(f562,plain,
( i7 = i6
| i8 = i6
| a_1291 = store(a_1289,i5,e_1251) ),
inference(paramodulation,[status(thm)],[f554,f217]) ).
fof(f563,plain,
( i7 = i6
| i8 = i6
| a_1289 = store(a_1287,i8,e_1251) ),
inference(paramodulation,[status(thm)],[f554,f106]) ).
fof(f564,plain,
( i9 = i4
| i1 = i4
| i7 = i4
| a_1305 = store(a_1303,i5,e_1294) ),
inference(paramodulation,[status(thm)],[f514,f114]) ).
fof(f565,plain,
( i8 = i7
| i5 = i7
| i4 = i7
| e_1263 = select(a_1252,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f180,f480]) ).
fof(f567,plain,
( i7 = i5
| i8 = i5
| e_1292 = select(a1,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f208,f532]) ).
fof(f569,plain,
( i6 = i9
| i8 = i9
| e_1294 = select(a_1285,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f248,f536]) ).
fof(f571,plain,
( i6 = i4
| i8 = i4
| e_1296 = select(a_1285,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f248,f540]) ).
fof(f573,plain,
( i6 = i4
| i8 = i4
| e_1259 = select(a_1248,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f174,f544]) ).
fof(f575,plain,
( i8 = i1
| i5 = i1
| i4 = i1
| e_1261 = select(a_1252,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f180,f482]) ).
fof(f577,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| e_1265 = select(a_1256,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f182,f488]) ).
fof(f579,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| e_1265 = e_1251
| i1 = i5 ),
inference(forward_demodulation,[status(thm)],[f247,f577]) ).
fof(f581,plain,
( i6 = i9
| i8 = i9
| e_1257 = select(a_1248,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f174,f548]) ).
fof(f589,plain,
( i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1260,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f186,f490]) ).
fof(f591,plain,
( i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1262,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f188,f496]) ).
fof(f593,plain,
( i0 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1268,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f194,f498]) ).
fof(f595,plain,
( i0 = i3
| i1 = i3
| e_1278 = select(a_1268,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f593]) ).
fof(f597,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1271,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f198,f500]) ).
fof(f599,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = select(a_1271,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f198,f502]) ).
fof(f601,plain,
( i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1289,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f250,f508]) ).
fof(f603,plain,
( i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = select(a_1289,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f250,f510]) ).
fof(f605,plain,
( i4 = i5
| i9 = i5
| i1 = i5
| e_1302 = select(a_1293,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f220,f516]) ).
fof(f607,plain,
( i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1297,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f224,f518]) ).
fof(f609,plain,
( i0 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1305,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f232,f520]) ).
fof(f611,plain,
( i0 = i3
| i2 = i3
| e_1315 = select(a_1305,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f609]) ).
fof(f613,plain,
( i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1299,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f226,f522]) ).
fof(f615,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| e_1309 = select(a_1299,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f226,f524]) ).
fof(f617,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| e_1309 = e_1298
| i0 = i1 ),
inference(forward_demodulation,[status(thm)],[f225,f615]) ).
fof(f619,plain,
( i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1308,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f236,f526]) ).
fof(f621,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1308,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f236,f528]) ).
fof(f626,plain,
( i8 = i5
| i7 = i5
| i8 = i5
| e_1292 = select(a_1246,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f166,f567]) ).
fof(f628,plain,
( i7 = i5
| i8 = i5
| e_1292 = select(a_1246,i5)
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f626]) ).
fof(f630,plain,
( i8 = i9
| i6 = i9
| i8 = i9
| e_1294 = select(a_1284,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f210,f569]) ).
fof(f632,plain,
( i6 = i9
| i8 = i9
| e_1294 = select(a_1284,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f630]) ).
fof(f634,plain,
( i8 = i4
| i6 = i4
| i8 = i4
| e_1296 = select(a_1284,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f210,f571]) ).
fof(f636,plain,
( i6 = i4
| i8 = i4
| e_1296 = select(a_1284,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f634]) ).
fof(f638,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1259 = select(a_1246,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f168,f573]) ).
fof(f640,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| i1 = i5
| a_1266 = store(a_1264,i4,e_1251) ),
inference(paramodulation,[status(thm)],[f579,f93]) ).
fof(f641,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1257 = select(a_1246,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f168,f581]) ).
fof(f646,plain,
( i8 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1263 = select(a_1250,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f176,f565]) ).
fof(f648,plain,
( i8 = i7
| i5 = i7
| i4 = i7
| e_1263 = select(a_1250,i7)
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f646]) ).
fof(f650,plain,
( i8 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1261 = select(a_1250,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f176,f575]) ).
fof(f652,plain,
( i8 = i1
| i5 = i1
| i4 = i1
| e_1261 = select(a_1250,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f650]) ).
fof(f654,plain,
( i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1266,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f192,f595]) ).
fof(f656,plain,
( i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1303,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f230,f611]) ).
fof(f658,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1258,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f184,f589]) ).
fof(f660,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| a_1310 = store(a_1308,i2,e_1298) ),
inference(paramodulation,[status(thm)],[f617,f117]) ).
fof(f661,plain,
( i7 = i5
| i6 = i5
| i8 = i5
| i7 = i5
| i8 = i5
| e_1292 = e_1253
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f478,f628]) ).
fof(f663,plain,
( i7 = i5
| i8 = i5
| e_1292 = e_1253
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f661]) ).
fof(f665,plain,
( i7 = i5
| i8 = i5
| i6 = i5
| a_1293 = store(a_1291,i8,e_1253) ),
inference(paramodulation,[status(thm)],[f663,f108]) ).
fof(f666,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1294 = select(a1,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f208,f632]) ).
fof(f668,plain,
( i0 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1270,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f196,f597]) ).
fof(f670,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1270,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f668]) ).
fof(f672,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = select(a_1270,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f196,f599]) ).
fof(f674,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = select(a_1270,i5)
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f672]) ).
fof(f676,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1296 = select(a1,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f208,f636]) ).
fof(f684,plain,
( i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1260,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f186,f591]) ).
fof(f686,plain,
( i8 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1287,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f214,f601]) ).
fof(f688,plain,
( i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1287,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f686]) ).
fof(f690,plain,
( i8 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = select(a_1287,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f214,f603]) ).
fof(f692,plain,
( i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = select(a_1287,i7)
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f690]) ).
fof(f694,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| e_1302 = select(a_1291,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f218,f605]) ).
fof(f696,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| e_1302 = e_1288
| i7 = i5 ),
inference(forward_demodulation,[status(thm)],[f251,f694]) ).
fof(f698,plain,
( i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1295,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f222,f607]) ).
fof(f700,plain,
( i0 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1307,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f234,f619]) ).
fof(f702,plain,
( i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1307,i6)
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f700]) ).
fof(f704,plain,
( i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1297,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f224,f613]) ).
fof(f706,plain,
( i0 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1307,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f234,f621]) ).
fof(f708,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1307,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f706]) ).
fof(f710,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1263 = select(a_1248,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f174,f648]) ).
fof(f712,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1263 = e_1247
| i9 = i7 ),
inference(forward_demodulation,[status(thm)],[f169,f710]) ).
fof(f714,plain,
( i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1261 = select(a_1248,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f174,f652]) ).
fof(f716,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1264,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f190,f654]) ).
fof(f721,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1301,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f228,f656]) ).
fof(f723,plain,
( i8 = i9
| i7 = i9
| i6 = i9
| i8 = i9
| e_1294 = select(a_1246,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f166,f666]) ).
fof(f725,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1294 = select(a_1246,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f723]) ).
fof(f727,plain,
( i0 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1268,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f194,f670]) ).
fof(f729,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1268,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f727]) ).
fof(f731,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = select(a_1268,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f194,f674]) ).
fof(f733,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = e_1267
| i0 = i5 ),
inference(forward_demodulation,[status(thm)],[f193,f731]) ).
fof(f734,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1280 = e_1267
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f733]) ).
fof(f737,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| a_1281 = store(a_1279,i9,e_1267) ),
inference(paramodulation,[status(thm)],[f734,f101]) ).
fof(f738,plain,
( i8 = i4
| i7 = i4
| i6 = i4
| i8 = i4
| e_1296 = select(a_1246,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f166,f676]) ).
fof(f740,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1296 = select(a_1246,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f738]) ).
fof(f742,plain,
( i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1285,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f248,f688]) ).
fof(f744,plain,
( i4 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1256,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f182,f658]) ).
fof(f746,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1256,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f744]) ).
fof(f748,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = select(a_1285,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f248,f692]) ).
fof(f750,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| a_1303 = store(a_1301,i4,e_1288) ),
inference(paramodulation,[status(thm)],[f696,f113]) ).
fof(f751,plain,
( i0 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1305,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f232,f702]) ).
fof(f753,plain,
( i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1305,i6)
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f751]) ).
fof(f755,plain,
( i0 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1305,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f232,f708]) ).
fof(f757,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1305,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f755]) ).
fof(f759,plain,
( i4 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1293,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f220,f698]) ).
fof(f761,plain,
( i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1293,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f759]) ).
fof(f763,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| a_1275 = store(a_1273,i2,e_1247) ),
inference(paramodulation,[status(thm)],[f712,f551]) ).
fof(f764,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| a_1264 = store(a_1262,i1,e_1247) ),
inference(paramodulation,[status(thm)],[f712,f92]) ).
fof(f765,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i7 = i9
| i6 = i9
| i8 = i9
| e_1294 = e_1257
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f641,f725]) ).
fof(f767,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1294 = e_1257
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f765]) ).
fof(f769,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| a_1305 = store(a_1303,i5,e_1257) ),
inference(paramodulation,[status(thm)],[f767,f564]) ).
fof(f770,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| a_1295 = store(a_1293,i4,e_1257) ),
inference(paramodulation,[status(thm)],[f767,f109]) ).
fof(f771,plain,
( i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1266,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f192,f729]) ).
fof(f776,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1258,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f184,f684]) ).
fof(f778,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i4
| i6 = i4
| i8 = i4
| e_1296 = e_1259
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f638,f740]) ).
fof(f780,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1296 = e_1259
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f778]) ).
fof(f782,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| a_1297 = store(a_1295,i9,e_1259) ),
inference(paramodulation,[status(thm)],[f780,f110]) ).
fof(f783,plain,
( i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1303,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f230,f753]) ).
fof(f785,plain,
( i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1303,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f230,f757]) ).
fof(f787,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| a_1281 = store(a_1279,i9,e_1257) ),
inference(paramodulation,[status(thm)],[f486,f737]) ).
fof(f794,plain,
( i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1295,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f222,f704]) ).
fof(f796,plain,
( i7 = i1
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1261 = select(a_1246,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f168,f714]) ).
fof(f798,plain,
( i1 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1262,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f188,f716]) ).
fof(f800,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1262,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f798]) ).
fof(f805,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1299,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f226,f721]) ).
fof(f807,plain,
( i8 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1284,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f210,f742]) ).
fof(f809,plain,
( i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1284,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f807]) ).
fof(f811,plain,
( i5 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1254,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f246,f746]) ).
fof(f813,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1254,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f811]) ).
fof(f815,plain,
( i8 = i7
| i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = select(a_1284,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f210,f748]) ).
fof(f817,plain,
( i8 = i7
| i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = e_1247
| i9 = i7 ),
inference(forward_demodulation,[status(thm)],[f209,f815]) ).
fof(f818,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1298 = e_1247
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f817]) ).
fof(f821,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| a_1310 = store(a_1308,i2,e_1247) ),
inference(paramodulation,[status(thm)],[f818,f660]) ).
fof(f822,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| a_1299 = store(a_1297,i1,e_1247) ),
inference(paramodulation,[status(thm)],[f818,f111]) ).
fof(f823,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1291,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f218,f761]) ).
fof(f825,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| a_1303 = store(a_1301,i4,e_1251) ),
inference(paramodulation,[status(thm)],[f554,f750]) ).
fof(f830,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| select(a_1275,i2) = e_1247 ),
inference(paramodulation,[status(thm)],[f763,f80]) ).
fof(f831,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| e_1274 = e_1247 ),
inference(forward_demodulation,[status(thm)],[f201,f830]) ).
fof(f832,plain,
( i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1264,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f190,f771]) ).
fof(f834,plain,
( i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1301,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f228,f783]) ).
fof(f836,plain,
( i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1301,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f228,f785]) ).
fof(f838,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1260,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f186,f800]) ).
fof(f840,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a1,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f208,f809]) ).
fof(f842,plain,
( i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1252,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f180,f813]) ).
fof(f847,plain,
( i4 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1256,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f182,f776]) ).
fof(f849,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1256,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f847]) ).
fof(f851,plain,
( i4 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1293,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f220,f794]) ).
fof(f853,plain,
( i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1293,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f851]) ).
fof(f858,plain,
( i1 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1297,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f224,f805]) ).
fof(f860,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1297,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f858]) ).
fof(f862,plain,
( i5 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1289,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f250,f823]) ).
fof(f864,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1289,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f862]) ).
fof(f866,plain,
( i1 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1262,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f188,f832]) ).
fof(f868,plain,
( i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1262,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f866]) ).
fof(f870,plain,
( i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1299,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f226,f834]) ).
fof(f872,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1299,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f226,f836]) ).
fof(f875,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| select(a_1303,i4) = e_1251 ),
inference(paramodulation,[status(thm)],[f825,f80]) ).
fof(f876,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| e_1302 = e_1251 ),
inference(forward_demodulation,[status(thm)],[f229,f875]) ).
fof(f878,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| select(a_1281,i9) = e_1257 ),
inference(paramodulation,[status(thm)],[f787,f80]) ).
fof(f879,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| e_1280 = e_1257 ),
inference(forward_demodulation,[status(thm)],[f207,f878]) ).
fof(f880,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1258,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f184,f838]) ).
fof(f882,plain,
( i8 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1246,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f166,f840]) ).
fof(f884,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = select(a_1246,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f882]) ).
fof(f886,plain,
( i8 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1250,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f176,f842]) ).
fof(f888,plain,
( i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1250,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f886]) ).
fof(f890,plain,
( i5 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1254,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f246,f849]) ).
fof(f892,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1254,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f890]) ).
fof(f894,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1291,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f218,f853]) ).
fof(f896,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1295,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f222,f860]) ).
fof(f899,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| select(a_1310,i2) = e_1247 ),
inference(paramodulation,[status(thm)],[f821,f80]) ).
fof(f900,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| e_1309 = e_1247 ),
inference(forward_demodulation,[status(thm)],[f237,f899]) ).
fof(f906,plain,
( i8 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1287,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f214,f864]) ).
fof(f908,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1287,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f906]) ).
fof(f910,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = select(a_1260,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f186,f868]) ).
fof(f912,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1282 = e_1259
| i0 = i9 ),
inference(forward_demodulation,[status(thm)],[f185,f910]) ).
fof(f920,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| select(a_1305,i5) = e_1257 ),
inference(paramodulation,[status(thm)],[f769,f80]) ).
fof(f921,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| e_1304 = e_1257 ),
inference(forward_demodulation,[status(thm)],[f231,f920]) ).
fof(f927,plain,
( i7 = i1
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| i9 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = e_1261
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f796,f884]) ).
fof(f929,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1300 = e_1261
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f927]) ).
fof(f931,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| i9 = i1
| a_1301 = store(a_1299,i7,e_1261) ),
inference(paramodulation,[status(thm)],[f929,f112]) ).
fof(f932,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1248,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f174,f888]) ).
fof(f934,plain,
( i1 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1297,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f224,f870]) ).
fof(f936,plain,
( i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1297,i6)
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f934]) ).
fof(f938,plain,
( i1 = i9
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = select(a_1297,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f224,f872]) ).
fof(f940,plain,
( i1 = i9
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = e_1296
| i0 = i9 ),
inference(forward_demodulation,[status(thm)],[f223,f938]) ).
fof(f941,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1317 = e_1296
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f940]) ).
fof(f944,plain,
( i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1252,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f180,f892]) ).
fof(f946,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1285,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f248,f908]) ).
fof(f948,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| i0 = i9
| a_1283 = store(a_1281,i5,e_1259) ),
inference(paramodulation,[status(thm)],[f912,f102]) ).
fof(f954,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| a_1318 = store(a_1316,i6,e_1296) ),
inference(paramodulation,[status(thm)],[f941,f121]) ).
fof(f958,plain,
( i4 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1256,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f182,f880]) ).
fof(f960,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1256,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f958]) ).
fof(f962,plain,
( i5 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1289,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f250,f894]) ).
fof(f964,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1289,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f962]) ).
fof(f966,plain,
( i4 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1293,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f220,f896]) ).
fof(f968,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1293,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f966]) ).
fof(f973,plain,
( i7 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1246,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f168,f932]) ).
fof(f975,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1269 = select(a_1246,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f973]) ).
fof(f982,plain,
( i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1295,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f222,f936]) ).
fof(f984,plain,
( i8 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1250,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f176,f944]) ).
fof(f986,plain,
( i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1250,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f984]) ).
fof(f988,plain,
( i8 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1284,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f210,f946]) ).
fof(f990,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1284,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f988]) ).
fof(f992,plain,
( i5 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1254,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f246,f960]) ).
fof(f994,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1254,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f992]) ).
fof(f996,plain,
( i8 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1287,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f214,f964]) ).
fof(f998,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1287,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f996]) ).
fof(f1000,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1291,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f218,f968]) ).
fof(f1002,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1248,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f174,f986]) ).
fof(f1004,plain,
( i7 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a1,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f208,f990]) ).
fof(f1006,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a1,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1004]) ).
fof(f1008,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1252,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f180,f994]) ).
fof(f1010,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1285,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f248,f998]) ).
fof(f1012,plain,
( i8 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1246,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f166,f1006]) ).
fof(f1014,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = select(a_1246,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1012]) ).
fof(f1016,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| a_1318 = store(a_1316,i6,e_1259) ),
inference(paramodulation,[status(thm)],[f780,f954]) ).
fof(f1020,plain,
( i4 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1293,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f220,f982]) ).
fof(f1022,plain,
( i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1293,i6)
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f1020]) ).
fof(f1024,plain,
( i5 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1289,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f250,f1000]) ).
fof(f1026,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1289,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1024]) ).
fof(f1028,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| i5 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = e_1269
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f975,f1014]) ).
fof(f1030,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1306 = e_1269
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1028]) ).
fof(f1032,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| a_1314 = store(a_1312,i3,e_1269) ),
inference(paramodulation,[status(thm)],[f1030,f452]) ).
fof(f1033,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| a_1308 = store(a_1307,i0,e_1269) ),
inference(paramodulation,[status(thm)],[f1030,f116]) ).
fof(f1034,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| a_1307 = store(a_1305,i0,e_1269) ),
inference(paramodulation,[status(thm)],[f1030,f115]) ).
fof(f1035,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| a_1314 = store(a_1312,i3,e_1269) ),
inference(duplicate_literals_removal,[status(thm)],[f1032]) ).
fof(f1036,plain,
( i7 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1246,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f168,f1002]) ).
fof(f1038,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1272 = select(a_1246,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1036]) ).
fof(f1046,plain,
( i8 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1250,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f176,f1008]) ).
fof(f1048,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1250,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1046]) ).
fof(f1050,plain,
( i8 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1284,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f210,f1010]) ).
fof(f1052,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1284,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1050]) ).
fof(f1055,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| select(a_1318,i6) = e_1259 ),
inference(paramodulation,[status(thm)],[f1016,f80]) ).
fof(f1056,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| e_1317 = e_1259 ),
inference(forward_demodulation,[status(thm)],[f245,f1055]) ).
fof(f1057,plain,
( i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1291,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f218,f1022]) ).
fof(f1059,plain,
( i8 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1287,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f214,f1026]) ).
fof(f1061,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1287,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1059]) ).
fof(f1063,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1248,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f174,f1048]) ).
fof(f1065,plain,
( i7 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a1,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f208,f1052]) ).
fof(f1067,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a1,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1065]) ).
fof(f1069,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1285,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f248,f1061]) ).
fof(f1071,plain,
( i8 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1246,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f166,f1067]) ).
fof(f1073,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = select(a_1246,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1071]) ).
fof(f1080,plain,
( i5 = i6
| i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1289,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f250,f1057]) ).
fof(f1082,plain,
( i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1289,i6)
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f1080]) ).
fof(f1084,plain,
( i7 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1246,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f168,f1063]) ).
fof(f1086,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1278 = select(a_1246,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1084]) ).
fof(f1088,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| i0 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = e_1272
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f1038,f1073]) ).
fof(f1090,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1311 = e_1272
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1088]) ).
fof(f1092,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| i0 = i2
| a_1312 = store(a_1310,i1,e_1272) ),
inference(paramodulation,[status(thm)],[f1090,f118]) ).
fof(f1093,plain,
( i8 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1284,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f210,f1069]) ).
fof(f1095,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1284,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1093]) ).
fof(f1098,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| select(a_1314,i3) = e_1269 ),
inference(paramodulation,[status(thm)],[f1035,f80]) ).
fof(f1099,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| e_1313 = e_1269 ),
inference(forward_demodulation,[status(thm)],[f241,f1098]) ).
fof(f1108,plain,
( i8 = i6
| i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = select(a_1287,i6)
| i0 = i6 ),
inference(paramodulation,[status(thm)],[f214,f1082]) ).
fof(f1110,plain,
( i8 = i6
| i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = e_1245
| i0 = i6 ),
inference(forward_demodulation,[status(thm)],[f249,f1108]) ).
fof(f1111,plain,
( i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| e_1319 = e_1245
| i0 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f1110]) ).
fof(f1114,plain,
( i7 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a1,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f208,f1095]) ).
fof(f1116,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a1,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1114]) ).
fof(f1118,plain,
( i8 = i6
| i9 = i6
| i7 = i6
| i4 = i6
| i5 = i6
| i2 = i6
| i1 = i6
| i3 = i6
| i0 = i6
| a_1320 = store(a_1318,i9,e_1245) ),
inference(paramodulation,[status(thm)],[f1111,f122]) ).
fof(f1119,plain,
( i8 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1246,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f166,f1116]) ).
fof(f1121,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = select(a_1246,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1119]) ).
fof(f1123,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| i2 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = e_1278
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f1086,f1121]) ).
fof(f1125,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1315 = e_1278
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1123]) ).
fof(f1127,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| i1 = i3
| a_1316 = store(a_1314,i0,e_1278) ),
inference(paramodulation,[status(thm)],[f1125,f120]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV534-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:03:12 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.13/0.61 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.13/0.61 % SZS output start Saturation for theBenchmark
% See solution above
% 1.34/0.68 % Elapsed time: 0.301317 seconds
% 1.34/0.68 % CPU time: 1.668225 seconds
% 1.34/0.68 % Total memory used: 121.993 MB
% 1.34/0.68 % Net memory used: 121.135 MB
%------------------------------------------------------------------------------