%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV533-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:35 PM UTC 2026
% Result : Satisfiable 0.13s 0.49s
% 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,hypothesis,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,hypothesis,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,hypothesis,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,hypothesis,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,hypothesis,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,hypothesis,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,hypothesis,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,hypothesis,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,hypothesis,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,hypothesis,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,hypothesis,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,hypothesis,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox/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_1245 = store(a1,i8,e_1244),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f84,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f85,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f86,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f87,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f88,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f89,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f90,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f91,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f92,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f93,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f94,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f95,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f96,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f97,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f98,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f99,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f100,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f101,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f102,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f103,plain,
a_1283 = store(a1,i7,e_1246),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f104,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f105,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f106,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f107,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f108,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f109,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f110,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f111,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f112,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f113,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f114,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f115,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f116,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f117,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f118,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f119,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f120,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f121,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f122,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f123,plain,
e_1244 = select(a1,i7),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f124,plain,
e_1246 = select(a1,i8),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f125,plain,
e_1248 = select(a_1247,i8),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f126,plain,
e_1250 = select(a_1247,i6),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f127,plain,
e_1252 = select(a_1251,i5),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f128,plain,
e_1254 = select(a_1251,i8),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f129,plain,
e_1256 = select(a_1255,i9),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f130,plain,
e_1258 = select(a_1255,i4),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f131,plain,
e_1260 = select(a_1259,i1),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f132,plain,
e_1262 = select(a_1259,i7),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f133,plain,
e_1264 = select(a_1263,i5),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f134,plain,
e_1266 = select(a_1263,i4),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f135,plain,
e_1268 = select(a_1267,i0),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f136,plain,
e_1271 = select(a_1270,i2),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f137,plain,
e_1273 = select(a_1270,i1),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f138,plain,
e_1275 = select(a_1274,i0),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f139,plain,
e_1277 = select(a_1274,i3),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f140,plain,
e_1279 = select(a_1278,i5),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f141,plain,
e_1281 = select(a_1278,i9),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f142,plain,
e_1285 = select(a_1284,i8),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f143,plain,
e_1287 = select(a_1284,i6),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f144,plain,
e_1289 = select(a_1288,i8),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f145,plain,
e_1291 = select(a_1288,i5),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f146,plain,
e_1293 = select(a_1292,i9),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f147,plain,
e_1295 = select(a_1292,i4),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f148,plain,
e_1297 = select(a_1296,i7),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f149,plain,
e_1299 = select(a_1296,i1),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f150,plain,
e_1301 = select(a_1300,i5),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f151,plain,
e_1303 = select(a_1300,i4),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f152,plain,
e_1305 = select(a_1304,i0),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f153,plain,
e_1308 = select(a_1307,i1),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f154,plain,
e_1310 = select(a_1307,i2),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f155,plain,
e_1312 = select(a_1311,i0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f156,plain,
e_1314 = select(a_1311,i3),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f157,plain,
e_1316 = select(a_1315,i9),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f158,plain,
e_1318 = select(a_1315,i5),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f159,plain,
a_1282 != a_1319,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f160,plain,
select(a_1319,i9) = e_1318,
inference(paramodulation,[status(thm)],[f122,f80]) ).
fof(f161,plain,
select(a_1282,i5) = e_1281,
inference(paramodulation,[status(thm)],[f102,f80]) ).
fof(f163,plain,
! [X0] :
( select(a_1319,X0) = select(a_1317,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f122,f82]) ).
fof(f164,plain,
! [X0] :
( select(a_1282,X0) = select(a_1280,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f102,f82]) ).
fof(f166,plain,
! [X0] :
( select(a_1245,X0) = select(a1,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f83,f82]) ).
fof(f167,plain,
select(a_1245,i8) = e_1244,
inference(paramodulation,[status(thm)],[f83,f80]) ).
fof(f168,plain,
! [X0] :
( select(a_1247,X0) = select(a_1245,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f84,f82]) ).
fof(f169,plain,
select(a_1247,i7) = e_1246,
inference(paramodulation,[status(thm)],[f84,f80]) ).
fof(f174,plain,
! [X0] :
( select(a_1249,X0) = select(a_1247,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f85,f82]) ).
fof(f175,plain,
select(a_1249,i6) = e_1248,
inference(paramodulation,[status(thm)],[f85,f80]) ).
fof(f176,plain,
! [X0] :
( select(a_1251,X0) = select(a_1249,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f86,f82]) ).
fof(f177,plain,
select(a_1251,i8) = e_1250,
inference(paramodulation,[status(thm)],[f86,f80]) ).
fof(f178,plain,
e_1254 = e_1250,
inference(backward_demodulation,[status(thm)],[f177,f128]) ).
fof(f179,plain,
a_1255 = store(a_1253,i5,e_1250),
inference(backward_demodulation,[status(thm)],[f178,f88]) ).
fof(f180,plain,
! [X0] :
( select(a_1253,X0) = select(a_1251,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f87,f82]) ).
fof(f181,plain,
select(a_1253,i8) = e_1252,
inference(paramodulation,[status(thm)],[f87,f80]) ).
fof(f182,plain,
! [X0] :
( select(a_1257,X0) = select(a_1255,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f89,f82]) ).
fof(f183,plain,
select(a_1257,i4) = e_1256,
inference(paramodulation,[status(thm)],[f89,f80]) ).
fof(f184,plain,
! [X0] :
( select(a_1259,X0) = select(a_1257,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f90,f82]) ).
fof(f185,plain,
select(a_1259,i9) = e_1258,
inference(paramodulation,[status(thm)],[f90,f80]) ).
fof(f186,plain,
! [X0] :
( select(a_1261,X0) = select(a_1259,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f91,f82]) ).
fof(f187,plain,
select(a_1261,i7) = e_1260,
inference(paramodulation,[status(thm)],[f91,f80]) ).
fof(f188,plain,
! [X0] :
( select(a_1263,X0) = select(a_1261,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f92,f82]) ).
fof(f189,plain,
select(a_1263,i1) = e_1262,
inference(paramodulation,[status(thm)],[f92,f80]) ).
fof(f190,plain,
! [X0] :
( select(a_1265,X0) = select(a_1263,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f93,f82]) ).
fof(f191,plain,
select(a_1265,i4) = e_1264,
inference(paramodulation,[status(thm)],[f93,f80]) ).
fof(f192,plain,
! [X0] :
( select(a_1267,X0) = select(a_1265,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f94,f82]) ).
fof(f193,plain,
select(a_1267,i5) = e_1266,
inference(paramodulation,[status(thm)],[f94,f80]) ).
fof(f194,plain,
! [X0] :
( select(a_1269,X0) = select(a_1267,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f95,f82]) ).
fof(f195,plain,
select(a_1269,i0) = e_1268,
inference(paramodulation,[status(thm)],[f95,f80]) ).
fof(f196,plain,
! [X0] :
( select(a_1270,X0) = select(a_1269,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f96,f82]) ).
fof(f197,plain,
select(a_1270,i0) = e_1268,
inference(paramodulation,[status(thm)],[f96,f80]) ).
fof(f198,plain,
! [X0] :
( select(a_1272,X0) = select(a_1270,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f97,f82]) ).
fof(f199,plain,
select(a_1272,i1) = e_1271,
inference(paramodulation,[status(thm)],[f97,f80]) ).
fof(f200,plain,
! [X0] :
( select(a_1274,X0) = select(a_1272,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f98,f82]) ).
fof(f201,plain,
select(a_1274,i2) = e_1273,
inference(paramodulation,[status(thm)],[f98,f80]) ).
fof(f202,plain,
! [X0] :
( select(a_1276,X0) = select(a_1274,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f99,f82]) ).
fof(f203,plain,
select(a_1276,i3) = e_1275,
inference(paramodulation,[status(thm)],[f99,f80]) ).
fof(f204,plain,
! [X0] :
( select(a_1278,X0) = select(a_1276,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f100,f82]) ).
fof(f205,plain,
select(a_1278,i0) = e_1277,
inference(paramodulation,[status(thm)],[f100,f80]) ).
fof(f206,plain,
! [X0] :
( select(a_1280,X0) = select(a_1278,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f101,f82]) ).
fof(f207,plain,
select(a_1280,i9) = e_1279,
inference(paramodulation,[status(thm)],[f101,f80]) ).
fof(f208,plain,
! [X0] :
( select(a_1283,X0) = select(a1,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f103,f82]) ).
fof(f209,plain,
select(a_1283,i7) = e_1246,
inference(paramodulation,[status(thm)],[f103,f80]) ).
fof(f210,plain,
! [X0] :
( select(a_1284,X0) = select(a_1283,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f104,f82]) ).
fof(f211,plain,
select(a_1284,i8) = e_1244,
inference(paramodulation,[status(thm)],[f104,f80]) ).
fof(f212,plain,
e_1285 = e_1244,
inference(backward_demodulation,[status(thm)],[f211,f142]) ).
fof(f213,plain,
a_1286 = store(a_1284,i6,e_1244),
inference(backward_demodulation,[status(thm)],[f212,f105]) ).
fof(f214,plain,
! [X0] :
( select(a_1288,X0) = select(a_1286,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f106,f82]) ).
fof(f215,plain,
select(a_1288,i8) = e_1287,
inference(paramodulation,[status(thm)],[f106,f80]) ).
fof(f216,plain,
e_1289 = e_1287,
inference(backward_demodulation,[status(thm)],[f215,f144]) ).
fof(f217,plain,
a_1290 = store(a_1288,i5,e_1287),
inference(backward_demodulation,[status(thm)],[f216,f107]) ).
fof(f218,plain,
! [X0] :
( select(a_1292,X0) = select(a_1290,X0)
| i8 = X0 ),
inference(paramodulation,[status(thm)],[f108,f82]) ).
fof(f219,plain,
select(a_1292,i8) = e_1291,
inference(paramodulation,[status(thm)],[f108,f80]) ).
fof(f220,plain,
! [X0] :
( select(a_1294,X0) = select(a_1292,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f109,f82]) ).
fof(f221,plain,
select(a_1294,i4) = e_1293,
inference(paramodulation,[status(thm)],[f109,f80]) ).
fof(f222,plain,
! [X0] :
( select(a_1296,X0) = select(a_1294,X0)
| i9 = X0 ),
inference(paramodulation,[status(thm)],[f110,f82]) ).
fof(f223,plain,
select(a_1296,i9) = e_1295,
inference(paramodulation,[status(thm)],[f110,f80]) ).
fof(f224,plain,
! [X0] :
( select(a_1298,X0) = select(a_1296,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f111,f82]) ).
fof(f225,plain,
select(a_1298,i1) = e_1297,
inference(paramodulation,[status(thm)],[f111,f80]) ).
fof(f226,plain,
! [X0] :
( select(a_1300,X0) = select(a_1298,X0)
| i7 = X0 ),
inference(paramodulation,[status(thm)],[f112,f82]) ).
fof(f227,plain,
select(a_1300,i7) = e_1299,
inference(paramodulation,[status(thm)],[f112,f80]) ).
fof(f228,plain,
! [X0] :
( select(a_1302,X0) = select(a_1300,X0)
| i4 = X0 ),
inference(paramodulation,[status(thm)],[f113,f82]) ).
fof(f229,plain,
select(a_1302,i4) = e_1301,
inference(paramodulation,[status(thm)],[f113,f80]) ).
fof(f230,plain,
! [X0] :
( select(a_1304,X0) = select(a_1302,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f114,f82]) ).
fof(f231,plain,
select(a_1304,i5) = e_1303,
inference(paramodulation,[status(thm)],[f114,f80]) ).
fof(f232,plain,
! [X0] :
( select(a_1306,X0) = select(a_1304,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f115,f82]) ).
fof(f233,plain,
select(a_1306,i0) = e_1305,
inference(paramodulation,[status(thm)],[f115,f80]) ).
fof(f234,plain,
! [X0] :
( select(a_1307,X0) = select(a_1306,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f116,f82]) ).
fof(f235,plain,
select(a_1307,i0) = e_1305,
inference(paramodulation,[status(thm)],[f116,f80]) ).
fof(f236,plain,
! [X0] :
( select(a_1309,X0) = select(a_1307,X0)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f117,f82]) ).
fof(f237,plain,
select(a_1309,i2) = e_1308,
inference(paramodulation,[status(thm)],[f117,f80]) ).
fof(f238,plain,
! [X0] :
( select(a_1311,X0) = select(a_1309,X0)
| i1 = X0 ),
inference(paramodulation,[status(thm)],[f118,f82]) ).
fof(f239,plain,
select(a_1311,i1) = e_1310,
inference(paramodulation,[status(thm)],[f118,f80]) ).
fof(f240,plain,
! [X0] :
( select(a_1313,X0) = select(a_1311,X0)
| i3 = X0 ),
inference(paramodulation,[status(thm)],[f119,f82]) ).
fof(f241,plain,
select(a_1313,i3) = e_1312,
inference(paramodulation,[status(thm)],[f119,f80]) ).
fof(f242,plain,
! [X0] :
( select(a_1315,X0) = select(a_1313,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f120,f82]) ).
fof(f243,plain,
select(a_1315,i0) = e_1314,
inference(paramodulation,[status(thm)],[f120,f80]) ).
fof(f244,plain,
! [X0] :
( select(a_1317,X0) = select(a_1315,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f121,f82]) ).
fof(f245,plain,
select(a_1317,i5) = e_1316,
inference(paramodulation,[status(thm)],[f121,f80]) ).
fof(f246,plain,
! [X0] :
( select(a_1255,X0) = select(a_1253,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f179,f82]) ).
fof(f247,plain,
select(a_1255,i5) = e_1250,
inference(paramodulation,[status(thm)],[f179,f80]) ).
fof(f248,plain,
! [X0] :
( select(a_1286,X0) = select(a_1284,X0)
| i6 = X0 ),
inference(paramodulation,[status(thm)],[f213,f82]) ).
fof(f249,plain,
select(a_1286,i6) = e_1244,
inference(paramodulation,[status(thm)],[f213,f80]) ).
fof(f250,plain,
! [X0] :
( select(a_1290,X0) = select(a_1288,X0)
| i5 = X0 ),
inference(paramodulation,[status(thm)],[f217,f82]) ).
fof(f251,plain,
select(a_1290,i5) = e_1287,
inference(paramodulation,[status(thm)],[f217,f80]) ).
fof(f253,plain,
( select(a_1245,i7) = e_1244
| i8 = i7 ),
inference(paramodulation,[status(thm)],[f123,f166]) ).
fof(f257,plain,
( e_1250 = select(a_1245,i6)
| i7 = i6 ),
inference(paramodulation,[status(thm)],[f126,f168]) ).
fof(f258,plain,
( e_1248 = select(a_1245,i8)
| i7 = i8 ),
inference(paramodulation,[status(thm)],[f125,f168]) ).
fof(f262,plain,
( e_1248 = e_1244
| i7 = i8 ),
inference(forward_demodulation,[status(thm)],[f167,f258]) ).
fof(f266,plain,
( i7 = i8
| a_1249 = store(a_1247,i6,e_1244) ),
inference(paramodulation,[status(thm)],[f262,f85]) ).
fof(f268,plain,
( e_1252 = select(a_1249,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f127,f176]) ).
fof(f271,plain,
( i6 = i5
| e_1252 = select(a_1247,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f174,f268]) ).
fof(f278,plain,
( e_1262 = select(a_1257,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f132,f184]) ).
fof(f279,plain,
( e_1260 = select(a_1257,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f131,f184]) ).
fof(f283,plain,
( i4 = i7
| e_1262 = select(a_1255,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f182,f278]) ).
fof(f285,plain,
( i4 = i1
| e_1260 = select(a_1255,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f182,f279]) ).
fof(f290,plain,
( e_1266 = select(a_1261,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f134,f188]) ).
fof(f291,plain,
( e_1264 = select(a_1261,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f133,f188]) ).
fof(f295,plain,
( i7 = i4
| e_1266 = select(a_1259,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f186,f290]) ).
fof(f297,plain,
( i7 = i5
| e_1264 = select(a_1259,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f186,f291]) ).
fof(f302,plain,
( e_1268 = select(a_1265,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f135,f192]) ).
fof(f307,plain,
( i4 = i0
| e_1268 = select(a_1263,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f190,f302]) ).
fof(f310,plain,
( e_1273 = select(a_1269,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f137,f196]) ).
fof(f311,plain,
( e_1271 = select(a_1269,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f136,f196]) ).
fof(f317,plain,
( i0 = i1
| e_1273 = select(a_1267,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f194,f310]) ).
fof(f319,plain,
( e_1273 = select(a_1267,i1)
| i0 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f317]) ).
fof(f321,plain,
( i0 = i2
| e_1271 = select(a_1267,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f194,f311]) ).
fof(f323,plain,
( e_1271 = select(a_1267,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f321]) ).
fof(f325,plain,
( i5 = i1
| e_1273 = select(a_1265,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f192,f319]) ).
fof(f327,plain,
( i5 = i2
| e_1271 = select(a_1265,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f192,f323]) ).
fof(f330,plain,
( e_1277 = select(a_1272,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f139,f200]) ).
fof(f331,plain,
( e_1275 = select(a_1272,i0)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f138,f200]) ).
fof(f337,plain,
( i1 = i3
| e_1277 = select(a_1270,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f198,f330]) ).
fof(f339,plain,
( i1 = i0
| e_1275 = select(a_1270,i0)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f198,f331]) ).
fof(f341,plain,
( i1 = i0
| e_1275 = e_1268
| i2 = i0 ),
inference(forward_demodulation,[status(thm)],[f197,f339]) ).
fof(f343,plain,
( i1 = i0
| i2 = i0
| a_1276 = store(a_1274,i3,e_1268) ),
inference(paramodulation,[status(thm)],[f341,f99]) ).
fof(f345,plain,
( e_1281 = select(a_1276,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f141,f204]) ).
fof(f346,plain,
( e_1279 = select(a_1276,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f140,f204]) ).
fof(f350,plain,
( i3 = i9
| e_1281 = select(a_1274,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f202,f345]) ).
fof(f352,plain,
( i3 = i5
| e_1279 = select(a_1274,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f202,f346]) ).
fof(f359,plain,
( e_1287 = select(a_1283,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f143,f210]) ).
fof(f362,plain,
( i7 = i6
| e_1287 = select(a1,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f208,f359]) ).
fof(f365,plain,
( e_1291 = select(a_1286,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f145,f214]) ).
fof(f369,plain,
( e_1295 = select(a_1290,i4)
| i8 = i4 ),
inference(paramodulation,[status(thm)],[f147,f218]) ).
fof(f370,plain,
( e_1293 = select(a_1290,i9)
| i8 = i9 ),
inference(paramodulation,[status(thm)],[f146,f218]) ).
fof(f377,plain,
( e_1299 = select(a_1294,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f149,f222]) ).
fof(f378,plain,
( e_1297 = select(a_1294,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f148,f222]) ).
fof(f384,plain,
( i4 = i1
| e_1299 = select(a_1292,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f220,f377]) ).
fof(f386,plain,
( i4 = i7
| e_1297 = select(a_1292,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f220,f378]) ).
fof(f389,plain,
( e_1303 = select(a_1298,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f151,f226]) ).
fof(f390,plain,
( e_1301 = select(a_1298,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f150,f226]) ).
fof(f394,plain,
( i1 = i4
| e_1303 = select(a_1296,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f224,f389]) ).
fof(f396,plain,
( i1 = i5
| e_1301 = select(a_1296,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f224,f390]) ).
fof(f401,plain,
( e_1305 = select(a_1302,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f152,f230]) ).
fof(f407,plain,
( e_1310 = select(a_1306,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f154,f234]) ).
fof(f408,plain,
( e_1308 = select(a_1306,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f153,f234]) ).
fof(f412,plain,
( i4 = i0
| e_1305 = select(a_1300,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f228,f401]) ).
fof(f414,plain,
( i0 = i2
| e_1310 = select(a_1304,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f232,f407]) ).
fof(f416,plain,
( e_1310 = select(a_1304,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f414]) ).
fof(f420,plain,
( i0 = i1
| e_1308 = select(a_1304,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f232,f408]) ).
fof(f422,plain,
( e_1308 = select(a_1304,i1)
| i0 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f420]) ).
fof(f424,plain,
( i5 = i2
| e_1310 = select(a_1302,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f230,f416]) ).
fof(f426,plain,
( i5 = i1
| e_1308 = select(a_1302,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f230,f422]) ).
fof(f429,plain,
( e_1314 = select(a_1309,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f156,f238]) ).
fof(f430,plain,
( e_1312 = select(a_1309,i0)
| i1 = i0 ),
inference(paramodulation,[status(thm)],[f155,f238]) ).
fof(f437,plain,
( e_1318 = select(a_1313,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f158,f242]) ).
fof(f438,plain,
( e_1316 = select(a_1313,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f157,f242]) ).
fof(f442,plain,
( i2 = i3
| e_1314 = select(a_1307,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f236,f429]) ).
fof(f444,plain,
( i2 = i0
| e_1312 = select(a_1307,i0)
| i1 = i0 ),
inference(paramodulation,[status(thm)],[f236,f430]) ).
fof(f446,plain,
( i2 = i0
| e_1312 = e_1305
| i1 = i0 ),
inference(forward_demodulation,[status(thm)],[f235,f444]) ).
fof(f448,plain,
( i3 = i5
| e_1318 = select(a_1311,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f240,f437]) ).
fof(f450,plain,
( i3 = i9
| e_1316 = select(a_1311,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f240,f438]) ).
fof(f452,plain,
( i2 = i0
| i1 = i0
| a_1313 = store(a_1311,i3,e_1305) ),
inference(paramodulation,[status(thm)],[f446,f119]) ).
fof(f456,plain,
( e_1258 = select(a_1253,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f130,f246]) ).
fof(f457,plain,
( e_1256 = select(a_1253,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f129,f246]) ).
fof(f461,plain,
( i8 = i5
| e_1291 = select(a_1284,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f365,f248]) ).
fof(f465,plain,
( i8 = i9
| e_1293 = select(a_1288,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f370,f250]) ).
fof(f466,plain,
( i8 = i4
| e_1295 = select(a_1288,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f369,f250]) ).
fof(f471,plain,
( i8 = i4
| e_1258 = select(a_1251,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f180,f456]) ).
fof(f473,plain,
( i8 = i9
| e_1256 = select(a_1251,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f180,f457]) ).
fof(f478,plain,
( i7 = i5
| i6 = i5
| e_1252 = select(a_1245,i5)
| i8 = i5 ),
inference(paramodulation,[status(thm)],[f168,f271]) ).
fof(f480,plain,
( i5 = i7
| i4 = i7
| e_1262 = select(a_1253,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f246,f283]) ).
fof(f482,plain,
( i5 = i1
| i4 = i1
| e_1260 = select(a_1253,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f246,f285]) ).
fof(f484,plain,
( i9 = i4
| i7 = i4
| e_1266 = select(a_1257,i4)
| i1 = i4 ),
inference(paramodulation,[status(thm)],[f184,f295]) ).
fof(f486,plain,
( i9 = i4
| i7 = i4
| e_1266 = e_1256
| i1 = i4 ),
inference(forward_demodulation,[status(thm)],[f183,f484]) ).
fof(f488,plain,
( i9 = i5
| i7 = i5
| e_1264 = select(a_1257,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f184,f297]) ).
fof(f490,plain,
( i1 = i0
| i4 = i0
| e_1268 = select(a_1261,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f188,f307]) ).
fof(f492,plain,
( i4 = i1
| i5 = i1
| e_1273 = select(a_1263,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f190,f325]) ).
fof(f494,plain,
( i4 = i1
| i5 = i1
| e_1273 = e_1262
| i0 = i1 ),
inference(forward_demodulation,[status(thm)],[f189,f492]) ).
fof(f496,plain,
( i4 = i2
| i5 = i2
| e_1271 = select(a_1263,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f190,f327]) ).
fof(f498,plain,
( i0 = i3
| i1 = i3
| e_1277 = select(a_1269,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f196,f337]) ).
fof(f500,plain,
( i2 = i9
| i3 = i9
| e_1281 = select(a_1272,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f200,f350]) ).
fof(f502,plain,
( i2 = i5
| i3 = i5
| e_1279 = select(a_1272,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f200,f352]) ).
fof(f504,plain,
( i8 = i6
| i7 = i6
| e_1287 = select(a_1245,i6)
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f166,f362]) ).
fof(f506,plain,
( i7 = i6
| e_1287 = select(a_1245,i6)
| i8 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f504]) ).
fof(f508,plain,
( i8 = i1
| i4 = i1
| e_1299 = select(a_1290,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f218,f384]) ).
fof(f510,plain,
( i8 = i7
| i4 = i7
| e_1297 = select(a_1290,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f218,f386]) ).
fof(f512,plain,
( i9 = i4
| i1 = i4
| e_1303 = select(a_1294,i4)
| i7 = i4 ),
inference(paramodulation,[status(thm)],[f222,f394]) ).
fof(f514,plain,
( i9 = i4
| i1 = i4
| e_1303 = e_1293
| i7 = i4 ),
inference(forward_demodulation,[status(thm)],[f221,f512]) ).
fof(f516,plain,
( i9 = i5
| i1 = i5
| e_1301 = select(a_1294,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f222,f396]) ).
fof(f518,plain,
( i7 = i0
| i4 = i0
| e_1305 = select(a_1298,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f226,f412]) ).
fof(f520,plain,
( i0 = i3
| i2 = i3
| e_1314 = select(a_1306,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f234,f442]) ).
fof(f522,plain,
( i4 = i2
| i5 = i2
| e_1310 = select(a_1300,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f228,f424]) ).
fof(f524,plain,
( i4 = i1
| i5 = i1
| e_1308 = select(a_1300,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f228,f426]) ).
fof(f526,plain,
( i1 = i5
| i3 = i5
| e_1318 = select(a_1309,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f238,f448]) ).
fof(f528,plain,
( i1 = i9
| i3 = i9
| e_1316 = select(a_1309,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f238,f450]) ).
fof(f530,plain,
( i8 = i5
| i8 = i5
| e_1291 = select(a_1283,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f210,f461]) ).
fof(f532,plain,
( i8 = i5
| e_1291 = select(a_1283,i5)
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f530]) ).
fof(f534,plain,
( i8 = i9
| i8 = i9
| e_1293 = select(a_1286,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f214,f465]) ).
fof(f536,plain,
( i8 = i9
| e_1293 = select(a_1286,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f534]) ).
fof(f538,plain,
( i8 = i4
| i8 = i4
| e_1295 = select(a_1286,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f214,f466]) ).
fof(f540,plain,
( i8 = i4
| e_1295 = select(a_1286,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f538]) ).
fof(f542,plain,
( i8 = i4
| i8 = i4
| e_1258 = select(a_1249,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f176,f471]) ).
fof(f544,plain,
( i8 = i4
| e_1258 = select(a_1249,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f542]) ).
fof(f546,plain,
( i8 = i9
| i8 = i9
| e_1256 = select(a_1249,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f176,f473]) ).
fof(f548,plain,
( i8 = i9
| e_1256 = select(a_1249,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f546]) ).
fof(f550,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| a_1267 = store(a_1265,i5,e_1256) ),
inference(paramodulation,[status(thm)],[f486,f94]) ).
fof(f551,plain,
( i4 = i1
| i5 = i1
| i0 = i1
| a_1274 = store(a_1272,i2,e_1262) ),
inference(paramodulation,[status(thm)],[f494,f98]) ).
fof(f552,plain,
( i7 = i6
| i7 = i6
| e_1287 = e_1250
| i8 = i6 ),
inference(paramodulation,[status(thm)],[f257,f506]) ).
fof(f554,plain,
( i7 = i6
| e_1287 = e_1250
| i8 = i6 ),
inference(duplicate_literals_removal,[status(thm)],[f552]) ).
fof(f562,plain,
( i7 = i6
| i8 = i6
| a_1290 = store(a_1288,i5,e_1250) ),
inference(paramodulation,[status(thm)],[f554,f217]) ).
fof(f563,plain,
( i7 = i6
| i8 = i6
| a_1288 = store(a_1286,i8,e_1250) ),
inference(paramodulation,[status(thm)],[f554,f106]) ).
fof(f564,plain,
( i9 = i4
| i1 = i4
| i7 = i4
| a_1304 = store(a_1302,i5,e_1293) ),
inference(paramodulation,[status(thm)],[f514,f114]) ).
fof(f565,plain,
( i8 = i7
| i5 = i7
| i4 = i7
| e_1262 = select(a_1251,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f180,f480]) ).
fof(f567,plain,
( i7 = i5
| i8 = i5
| e_1291 = select(a1,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f208,f532]) ).
fof(f569,plain,
( i6 = i9
| i8 = i9
| e_1293 = select(a_1284,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f248,f536]) ).
fof(f571,plain,
( i6 = i4
| i8 = i4
| e_1295 = select(a_1284,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f248,f540]) ).
fof(f573,plain,
( i6 = i4
| i8 = i4
| e_1258 = select(a_1247,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f174,f544]) ).
fof(f575,plain,
( i8 = i1
| i5 = i1
| i4 = i1
| e_1260 = select(a_1251,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f180,f482]) ).
fof(f577,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| e_1264 = select(a_1255,i5)
| i1 = i5 ),
inference(paramodulation,[status(thm)],[f182,f488]) ).
fof(f579,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| e_1264 = e_1250
| i1 = i5 ),
inference(forward_demodulation,[status(thm)],[f247,f577]) ).
fof(f581,plain,
( i6 = i9
| i8 = i9
| e_1256 = select(a_1247,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f174,f548]) ).
fof(f589,plain,
( i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1259,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f186,f490]) ).
fof(f591,plain,
( i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1261,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f188,f496]) ).
fof(f593,plain,
( i0 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1267,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f194,f498]) ).
fof(f595,plain,
( i0 = i3
| i1 = i3
| e_1277 = select(a_1267,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f593]) ).
fof(f597,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1270,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f198,f500]) ).
fof(f599,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = select(a_1270,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f198,f502]) ).
fof(f601,plain,
( i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1288,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f250,f508]) ).
fof(f603,plain,
( i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = select(a_1288,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f250,f510]) ).
fof(f605,plain,
( i4 = i5
| i9 = i5
| i1 = i5
| e_1301 = select(a_1292,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f220,f516]) ).
fof(f607,plain,
( i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1296,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f224,f518]) ).
fof(f609,plain,
( i0 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1304,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f232,f520]) ).
fof(f611,plain,
( i0 = i3
| i2 = i3
| e_1314 = select(a_1304,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f609]) ).
fof(f613,plain,
( i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1298,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f226,f522]) ).
fof(f615,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| e_1308 = select(a_1298,i1)
| i0 = i1 ),
inference(paramodulation,[status(thm)],[f226,f524]) ).
fof(f617,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| e_1308 = e_1297
| i0 = i1 ),
inference(forward_demodulation,[status(thm)],[f225,f615]) ).
fof(f619,plain,
( i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = select(a_1307,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f236,f526]) ).
fof(f621,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1307,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f236,f528]) ).
fof(f626,plain,
( i8 = i5
| i7 = i5
| i8 = i5
| e_1291 = select(a_1245,i5)
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f166,f567]) ).
fof(f628,plain,
( i7 = i5
| i8 = i5
| e_1291 = select(a_1245,i5)
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f626]) ).
fof(f630,plain,
( i8 = i9
| i6 = i9
| i8 = i9
| e_1293 = select(a_1283,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f210,f569]) ).
fof(f632,plain,
( i6 = i9
| i8 = i9
| e_1293 = select(a_1283,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f630]) ).
fof(f634,plain,
( i8 = i4
| i6 = i4
| i8 = i4
| e_1295 = select(a_1283,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f210,f571]) ).
fof(f636,plain,
( i6 = i4
| i8 = i4
| e_1295 = select(a_1283,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f634]) ).
fof(f638,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1258 = select(a_1245,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f168,f573]) ).
fof(f640,plain,
( i4 = i5
| i9 = i5
| i7 = i5
| i1 = i5
| a_1265 = store(a_1263,i4,e_1250) ),
inference(paramodulation,[status(thm)],[f579,f93]) ).
fof(f641,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1256 = select(a_1245,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f168,f581]) ).
fof(f646,plain,
( i8 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1262 = select(a_1249,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f176,f565]) ).
fof(f648,plain,
( i8 = i7
| i5 = i7
| i4 = i7
| e_1262 = select(a_1249,i7)
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f646]) ).
fof(f650,plain,
( i8 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1260 = select(a_1249,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f176,f575]) ).
fof(f652,plain,
( i8 = i1
| i5 = i1
| i4 = i1
| e_1260 = select(a_1249,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f650]) ).
fof(f654,plain,
( i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1265,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f192,f595]) ).
fof(f656,plain,
( i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1302,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f230,f611]) ).
fof(f658,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1257,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f184,f589]) ).
fof(f660,plain,
( i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| a_1309 = store(a_1307,i2,e_1297) ),
inference(paramodulation,[status(thm)],[f617,f117]) ).
fof(f661,plain,
( i7 = i5
| i6 = i5
| i8 = i5
| i7 = i5
| i8 = i5
| e_1291 = e_1252
| i6 = i5 ),
inference(paramodulation,[status(thm)],[f478,f628]) ).
fof(f663,plain,
( i7 = i5
| i8 = i5
| e_1291 = e_1252
| i6 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f661]) ).
fof(f665,plain,
( i7 = i5
| i8 = i5
| i6 = i5
| a_1292 = store(a_1290,i8,e_1252) ),
inference(paramodulation,[status(thm)],[f663,f108]) ).
fof(f666,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1293 = select(a1,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f208,f632]) ).
fof(f668,plain,
( i0 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1269,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f196,f597]) ).
fof(f670,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1269,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f668]) ).
fof(f672,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = select(a_1269,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f196,f599]) ).
fof(f674,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = select(a_1269,i5)
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f672]) ).
fof(f676,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1295 = select(a1,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f208,f636]) ).
fof(f684,plain,
( i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1259,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f186,f591]) ).
fof(f686,plain,
( i8 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1286,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f214,f601]) ).
fof(f688,plain,
( i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1286,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f686]) ).
fof(f690,plain,
( i8 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = select(a_1286,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f214,f603]) ).
fof(f692,plain,
( i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = select(a_1286,i7)
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f690]) ).
fof(f694,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| e_1301 = select(a_1290,i5)
| i7 = i5 ),
inference(paramodulation,[status(thm)],[f218,f605]) ).
fof(f696,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| e_1301 = e_1287
| i7 = i5 ),
inference(forward_demodulation,[status(thm)],[f251,f694]) ).
fof(f698,plain,
( i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1294,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f222,f607]) ).
fof(f700,plain,
( i0 = i5
| i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = select(a_1306,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f234,f619]) ).
fof(f702,plain,
( i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = select(a_1306,i5)
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f700]) ).
fof(f704,plain,
( i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1296,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f224,f613]) ).
fof(f706,plain,
( i0 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1306,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f234,f621]) ).
fof(f708,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1306,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f706]) ).
fof(f710,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1262 = select(a_1247,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f174,f648]) ).
fof(f712,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| e_1262 = e_1246
| i9 = i7 ),
inference(forward_demodulation,[status(thm)],[f169,f710]) ).
fof(f714,plain,
( i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1260 = select(a_1247,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f174,f652]) ).
fof(f716,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1263,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f190,f654]) ).
fof(f721,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1300,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f228,f656]) ).
fof(f723,plain,
( i8 = i9
| i7 = i9
| i6 = i9
| i8 = i9
| e_1293 = select(a_1245,i9)
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f166,f666]) ).
fof(f725,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1293 = select(a_1245,i9)
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f723]) ).
fof(f727,plain,
( i0 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1267,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f194,f670]) ).
fof(f729,plain,
( i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1267,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f727]) ).
fof(f731,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = select(a_1267,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f194,f674]) ).
fof(f733,plain,
( i0 = i5
| i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = e_1266
| i0 = i5 ),
inference(forward_demodulation,[status(thm)],[f193,f731]) ).
fof(f734,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| e_1279 = e_1266
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f733]) ).
fof(f737,plain,
( i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| a_1280 = store(a_1278,i9,e_1266) ),
inference(paramodulation,[status(thm)],[f734,f101]) ).
fof(f738,plain,
( i8 = i4
| i7 = i4
| i6 = i4
| i8 = i4
| e_1295 = select(a_1245,i4)
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f166,f676]) ).
fof(f740,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1295 = select(a_1245,i4)
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f738]) ).
fof(f742,plain,
( i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1284,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f248,f688]) ).
fof(f744,plain,
( i4 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1255,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f182,f658]) ).
fof(f746,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1255,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f744]) ).
fof(f748,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = select(a_1284,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f248,f692]) ).
fof(f750,plain,
( i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| a_1302 = store(a_1300,i4,e_1287) ),
inference(paramodulation,[status(thm)],[f696,f113]) ).
fof(f751,plain,
( i0 = i5
| i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = select(a_1304,i5)
| i0 = i5 ),
inference(paramodulation,[status(thm)],[f232,f702]) ).
fof(f753,plain,
( i0 = i5
| i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = e_1303
| i0 = i5 ),
inference(forward_demodulation,[status(thm)],[f231,f751]) ).
fof(f754,plain,
( i2 = i5
| i1 = i5
| i3 = i5
| e_1318 = e_1303
| i0 = i5 ),
inference(duplicate_literals_removal,[status(thm)],[f753]) ).
fof(f757,plain,
( i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| a_1319 = store(a_1317,i9,e_1303) ),
inference(paramodulation,[status(thm)],[f754,f122]) ).
fof(f758,plain,
( i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| a_1319 = store(a_1317,i9,e_1293) ),
inference(paramodulation,[status(thm)],[f514,f757]) ).
fof(f763,plain,
( i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| select(a_1319,i9) = e_1293 ),
inference(paramodulation,[status(thm)],[f758,f80]) ).
fof(f764,plain,
( i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| e_1318 = e_1293 ),
inference(forward_demodulation,[status(thm)],[f160,f763]) ).
fof(f770,plain,
( i0 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1304,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f232,f708]) ).
fof(f772,plain,
( i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1304,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f770]) ).
fof(f774,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| a_1274 = store(a_1272,i2,e_1246) ),
inference(paramodulation,[status(thm)],[f712,f551]) ).
fof(f775,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| a_1263 = store(a_1261,i1,e_1246) ),
inference(paramodulation,[status(thm)],[f712,f92]) ).
fof(f776,plain,
( i4 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1292,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f220,f698]) ).
fof(f778,plain,
( i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1292,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f776]) ).
fof(f783,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i7 = i9
| i6 = i9
| i8 = i9
| e_1293 = e_1256
| i5 = i9 ),
inference(paramodulation,[status(thm)],[f641,f725]) ).
fof(f785,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| e_1293 = e_1256
| i5 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f783]) ).
fof(f787,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| a_1319 = store(a_1317,i9,e_1256) ),
inference(paramodulation,[status(thm)],[f785,f758]) ).
fof(f788,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| a_1304 = store(a_1302,i5,e_1256) ),
inference(paramodulation,[status(thm)],[f785,f564]) ).
fof(f789,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| a_1294 = store(a_1292,i4,e_1256) ),
inference(paramodulation,[status(thm)],[f785,f109]) ).
fof(f790,plain,
( i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1265,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f192,f729]) ).
fof(f792,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i4
| i6 = i4
| i8 = i4
| e_1295 = e_1258
| i5 = i4 ),
inference(paramodulation,[status(thm)],[f638,f740]) ).
fof(f794,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| e_1295 = e_1258
| i5 = i4 ),
inference(duplicate_literals_removal,[status(thm)],[f792]) ).
fof(f796,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| a_1296 = store(a_1294,i9,e_1258) ),
inference(paramodulation,[status(thm)],[f794,f110]) ).
fof(f797,plain,
( i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1302,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f230,f772]) ).
fof(f799,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1257,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f184,f684]) ).
fof(f801,plain,
( i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1294,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f222,f704]) ).
fof(f803,plain,
( i7 = i1
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| e_1260 = select(a_1245,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f168,f714]) ).
fof(f806,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| select(a_1319,i9) = e_1256 ),
inference(paramodulation,[status(thm)],[f787,f80]) ).
fof(f807,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| i2 = i5
| i1 = i5
| i3 = i5
| i0 = i5
| e_1318 = e_1256 ),
inference(forward_demodulation,[status(thm)],[f160,f806]) ).
fof(f824,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| a_1280 = store(a_1278,i9,e_1256) ),
inference(paramodulation,[status(thm)],[f486,f737]) ).
fof(f834,plain,
( i1 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1261,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f188,f716]) ).
fof(f836,plain,
( i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1261,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f834]) ).
fof(f838,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1298,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f226,f721]) ).
fof(f840,plain,
( i8 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1283,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f210,f742]) ).
fof(f842,plain,
( i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1283,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f840]) ).
fof(f844,plain,
( i5 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1253,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f246,f746]) ).
fof(f846,plain,
( i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1253,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f844]) ).
fof(f848,plain,
( i8 = i7
| i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = select(a_1283,i7)
| i9 = i7 ),
inference(paramodulation,[status(thm)],[f210,f748]) ).
fof(f850,plain,
( i8 = i7
| i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = e_1246
| i9 = i7 ),
inference(forward_demodulation,[status(thm)],[f209,f848]) ).
fof(f851,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| e_1297 = e_1246
| i9 = i7 ),
inference(duplicate_literals_removal,[status(thm)],[f850]) ).
fof(f854,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| a_1309 = store(a_1307,i2,e_1246) ),
inference(paramodulation,[status(thm)],[f851,f660]) ).
fof(f855,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| a_1298 = store(a_1296,i1,e_1246) ),
inference(paramodulation,[status(thm)],[f851,f111]) ).
fof(f856,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1290,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f218,f778]) ).
fof(f858,plain,
( i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1263,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f190,f790]) ).
fof(f860,plain,
( i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1300,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f228,f797]) ).
fof(f862,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| a_1302 = store(a_1300,i4,e_1250) ),
inference(paramodulation,[status(thm)],[f554,f750]) ).
fof(f867,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| select(a_1274,i2) = e_1246 ),
inference(paramodulation,[status(thm)],[f774,f80]) ).
fof(f868,plain,
( i6 = i7
| i8 = i7
| i5 = i7
| i4 = i7
| i9 = i7
| i4 = i1
| i5 = i1
| i0 = i1
| e_1273 = e_1246 ),
inference(forward_demodulation,[status(thm)],[f201,f867]) ).
fof(f872,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1259,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f186,f836]) ).
fof(f874,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a1,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f208,f842]) ).
fof(f876,plain,
( i4 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1255,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f182,f799]) ).
fof(f878,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1255,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f876]) ).
fof(f880,plain,
( i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1251,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f180,f846]) ).
fof(f885,plain,
( i4 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1292,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f220,f801]) ).
fof(f887,plain,
( i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1292,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f885]) ).
fof(f889,plain,
( i1 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1296,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f224,f838]) ).
fof(f891,plain,
( i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1296,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f889]) ).
fof(f893,plain,
( i5 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1288,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f250,f856]) ).
fof(f895,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1288,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f893]) ).
fof(f897,plain,
( i1 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1261,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f188,f858]) ).
fof(f899,plain,
( i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1261,i9)
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f897]) ).
fof(f901,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1298,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f226,f860]) ).
fof(f903,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1257,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f184,f872]) ).
fof(f905,plain,
( i8 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1245,i1)
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f166,f874]) ).
fof(f907,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = select(a_1245,i1)
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f905]) ).
fof(f909,plain,
( i5 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1253,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f246,f878]) ).
fof(f911,plain,
( i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1253,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f909]) ).
fof(f913,plain,
( i8 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1249,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f176,f880]) ).
fof(f915,plain,
( i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1249,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f913]) ).
fof(f918,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| select(a_1302,i4) = e_1250 ),
inference(paramodulation,[status(thm)],[f862,f80]) ).
fof(f919,plain,
( i7 = i6
| i8 = i6
| i8 = i5
| i4 = i5
| i9 = i5
| i1 = i5
| i7 = i5
| e_1301 = e_1250 ),
inference(forward_demodulation,[status(thm)],[f229,f918]) ).
fof(f921,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| select(a_1280,i9) = e_1256 ),
inference(paramodulation,[status(thm)],[f824,f80]) ).
fof(f922,plain,
( i9 = i4
| i7 = i4
| i1 = i4
| i1 = i5
| i2 = i5
| i3 = i5
| i0 = i5
| e_1279 = e_1256 ),
inference(forward_demodulation,[status(thm)],[f207,f921]) ).
fof(f924,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| select(a_1309,i2) = e_1246 ),
inference(paramodulation,[status(thm)],[f854,f80]) ).
fof(f925,plain,
( i6 = i7
| i5 = i7
| i8 = i7
| i4 = i7
| i9 = i7
| i7 = i1
| i4 = i1
| i5 = i1
| i0 = i1
| e_1308 = e_1246 ),
inference(forward_demodulation,[status(thm)],[f237,f924]) ).
fof(f926,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1290,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f218,f887]) ).
fof(f928,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1294,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f222,f891]) ).
fof(f935,plain,
( i8 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1286,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f214,f895]) ).
fof(f937,plain,
( i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1286,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f935]) ).
fof(f939,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = select(a_1259,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f186,f899]) ).
fof(f941,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| e_1281 = e_1258
| i0 = i9 ),
inference(forward_demodulation,[status(thm)],[f185,f939]) ).
fof(f943,plain,
( i7 = i1
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| i9 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = e_1260
| i9 = i1 ),
inference(paramodulation,[status(thm)],[f803,f907]) ).
fof(f945,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| e_1299 = e_1260
| i9 = i1 ),
inference(duplicate_literals_removal,[status(thm)],[f943]) ).
fof(f947,plain,
( i7 = i1
| i6 = i1
| i5 = i1
| i8 = i1
| i4 = i1
| i9 = i1
| a_1300 = store(a_1298,i7,e_1260) ),
inference(paramodulation,[status(thm)],[f945,f112]) ).
fof(f954,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| select(a_1304,i5) = e_1256 ),
inference(paramodulation,[status(thm)],[f788,f80]) ).
fof(f955,plain,
( i7 = i9
| i6 = i9
| i8 = i9
| i5 = i9
| i9 = i4
| i1 = i4
| i7 = i4
| e_1303 = e_1256 ),
inference(forward_demodulation,[status(thm)],[f231,f954]) ).
fof(f956,plain,
( i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1251,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f180,f911]) ).
fof(f958,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1247,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f174,f915]) ).
fof(f965,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1284,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f248,f937]) ).
fof(f967,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i1 = i9
| i2 = i9
| i3 = i9
| i0 = i9
| a_1282 = store(a_1280,i5,e_1258) ),
inference(paramodulation,[status(thm)],[f941,f102]) ).
fof(f974,plain,
( i1 = i9
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = select(a_1296,i9)
| i0 = i9 ),
inference(paramodulation,[status(thm)],[f224,f901]) ).
fof(f976,plain,
( i1 = i9
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = e_1295
| i0 = i9 ),
inference(forward_demodulation,[status(thm)],[f223,f974]) ).
fof(f977,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| e_1316 = e_1295
| i0 = i9 ),
inference(duplicate_literals_removal,[status(thm)],[f976]) ).
fof(f980,plain,
( i4 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1255,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f182,f903]) ).
fof(f982,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1255,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f980]) ).
fof(f992,plain,
( i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| a_1317 = store(a_1315,i5,e_1295) ),
inference(paramodulation,[status(thm)],[f977,f121]) ).
fof(f993,plain,
( i5 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1288,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f250,f926]) ).
fof(f995,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1288,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f993]) ).
fof(f1000,plain,
( i4 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1292,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f220,f928]) ).
fof(f1002,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1292,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1000]) ).
fof(f1004,plain,
( i8 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1249,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f176,f956]) ).
fof(f1006,plain,
( i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1249,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1004]) ).
fof(f1008,plain,
( i7 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1245,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f168,f958]) ).
fof(f1010,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i4 = i0
| e_1268 = select(a_1245,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1008]) ).
fof(f1012,plain,
( i8 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1283,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f210,f965]) ).
fof(f1014,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1283,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1012]) ).
fof(f1016,plain,
( i5 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1253,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f246,f982]) ).
fof(f1018,plain,
( i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1253,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1016]) ).
fof(f1020,plain,
( i8 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1286,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f214,f995]) ).
fof(f1022,plain,
( i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1286,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1020]) ).
fof(f1024,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1290,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f218,f1002]) ).
fof(f1026,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1247,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f174,f1006]) ).
fof(f1028,plain,
( i7 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a1,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f208,f1014]) ).
fof(f1030,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a1,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1028]) ).
fof(f1032,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1251,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f180,f1018]) ).
fof(f1034,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| a_1317 = store(a_1315,i5,e_1258) ),
inference(paramodulation,[status(thm)],[f794,f992]) ).
fof(f1038,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1284,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f248,f1022]) ).
fof(f1040,plain,
( i5 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1288,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f250,f1024]) ).
fof(f1042,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1288,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1040]) ).
fof(f1044,plain,
( i8 = i0
| i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1245,i0)
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f166,f1030]) ).
fof(f1046,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = select(a_1245,i0)
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1044]) ).
fof(f1048,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_1305 = e_1268
| i5 = i0 ),
inference(paramodulation,[status(thm)],[f1010,f1046]) ).
fof(f1050,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| e_1305 = e_1268
| i5 = i0 ),
inference(duplicate_literals_removal,[status(thm)],[f1048]) ).
fof(f1052,plain,
( i7 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1245,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f168,f1026]) ).
fof(f1054,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i4 = i2
| i5 = i2
| e_1271 = select(a_1245,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1052]) ).
fof(f1056,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| a_1313 = store(a_1311,i3,e_1268) ),
inference(paramodulation,[status(thm)],[f1050,f452]) ).
fof(f1057,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| a_1307 = store(a_1306,i0,e_1268) ),
inference(paramodulation,[status(thm)],[f1050,f116]) ).
fof(f1058,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| a_1306 = store(a_1304,i0,e_1268) ),
inference(paramodulation,[status(thm)],[f1050,f115]) ).
fof(f1059,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| a_1313 = store(a_1311,i3,e_1268) ),
inference(duplicate_literals_removal,[status(thm)],[f1056]) ).
fof(f1066,plain,
( i8 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1249,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f176,f1032]) ).
fof(f1068,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1249,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1066]) ).
fof(f1071,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_1317,i5) = e_1258 ),
inference(paramodulation,[status(thm)],[f1034,f80]) ).
fof(f1072,plain,
( i7 = i4
| i6 = i4
| i8 = i4
| i5 = i4
| i7 = i9
| i4 = i9
| i5 = i9
| i2 = i9
| i1 = i9
| i3 = i9
| i0 = i9
| e_1316 = e_1258 ),
inference(forward_demodulation,[status(thm)],[f245,f1071]) ).
fof(f1073,plain,
( i8 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1283,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f210,f1038]) ).
fof(f1075,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1283,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1073]) ).
fof(f1077,plain,
( i8 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1286,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f214,f1042]) ).
fof(f1079,plain,
( i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1286,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1077]) ).
fof(f1081,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1247,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f174,f1068]) ).
fof(f1083,plain,
( i7 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a1,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f208,f1075]) ).
fof(f1085,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a1,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1083]) ).
fof(f1087,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1284,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f248,f1079]) ).
fof(f1089,plain,
( i8 = i2
| i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1245,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f166,f1085]) ).
fof(f1091,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = select(a_1245,i2)
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1089]) ).
fof(f1098,plain,
( i7 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1245,i3)
| i2 = i3 ),
inference(paramodulation,[status(thm)],[f168,f1081]) ).
fof(f1100,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i1 = i3
| e_1277 = select(a_1245,i3)
| i2 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1098]) ).
fof(f1102,plain,
( i8 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1283,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f210,f1087]) ).
fof(f1104,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1283,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1102]) ).
fof(f1106,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_1310 = e_1271
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f1054,f1091]) ).
fof(f1108,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| e_1310 = e_1271
| i0 = i2 ),
inference(duplicate_literals_removal,[status(thm)],[f1106]) ).
fof(f1110,plain,
( i6 = i2
| i8 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i4 = i2
| i5 = i2
| i0 = i2
| a_1311 = store(a_1309,i1,e_1271) ),
inference(paramodulation,[status(thm)],[f1108,f118]) ).
fof(f1112,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| select(a_1313,i3) = e_1268 ),
inference(paramodulation,[status(thm)],[f1059,f80]) ).
fof(f1113,plain,
( i6 = i0
| i8 = i0
| i9 = i0
| i7 = i0
| i4 = i0
| i5 = i0
| i2 = i0
| i1 = i0
| e_1312 = e_1268 ),
inference(forward_demodulation,[status(thm)],[f241,f1112]) ).
fof(f1122,plain,
( i7 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a1,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f208,f1104]) ).
fof(f1124,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a1,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1122]) ).
fof(f1126,plain,
( i8 = i3
| i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1245,i3)
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f166,f1124]) ).
fof(f1128,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = select(a_1245,i3)
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1126]) ).
fof(f1130,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_1314 = e_1277
| i1 = i3 ),
inference(paramodulation,[status(thm)],[f1100,f1128]) ).
fof(f1132,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| e_1314 = e_1277
| i1 = i3 ),
inference(duplicate_literals_removal,[status(thm)],[f1130]) ).
fof(f1134,plain,
( i6 = i3
| i8 = i3
| i9 = i3
| i7 = i3
| i4 = i3
| i5 = i3
| i0 = i3
| i2 = i3
| i1 = i3
| a_1315 = store(a_1313,i0,e_1277) ),
inference(paramodulation,[status(thm)],[f1132,f120]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV533-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:03:04 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.49 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.13/0.49 % SZS output start Saturation for theBenchmark
% See solution above
% 0.15/0.52 % Elapsed time: 0.157256 seconds
% 0.15/0.52 % CPU time: 0.957879 seconds
% 0.15/0.52 % Total memory used: 121.767 MB
% 0.15/0.52 % Net memory used: 120.844 MB
%------------------------------------------------------------------------------