%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV540-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 : Tue Sep 29 01:17:33 PM UTC 2026
% Result : Unsatisfiable 39.53s 6.74s
% Output : Refutation 43.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 95
% Syntax : Number of formulae : 442 ( 170 unt; 14 def)
% Number of atoms : 863 ( 430 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 773 ( 352 ~; 407 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 89 ( 89 usr; 87 con; 0-3 aty)
% Number of variables : 85 ( 0 sgn 85 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] :
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f6,axiom,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f7,axiom,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f8,axiom,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f20,axiom,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f21,axiom,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f23,axiom,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f24,axiom,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f25,axiom,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f26,axiom,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f27,axiom,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f28,axiom,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f29,axiom,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f30,axiom,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f31,axiom,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f32,axiom,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f33,axiom,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f34,axiom,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f35,axiom,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f36,axiom,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f37,axiom,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f38,axiom,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f39,axiom,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f40,axiom,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f41,axiom,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f42,axiom,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f43,axiom,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f44,axiom,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f45,axiom,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f46,axiom,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f47,axiom,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f48,axiom,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f49,axiom,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f50,axiom,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f51,axiom,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f52,axiom,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f53,axiom,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f54,axiom,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f55,axiom,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f56,axiom,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
fof(f57,axiom,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f58,axiom,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
fof(f59,axiom,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).
fof(f60,axiom,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
fof(f61,axiom,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp55) ).
fof(f62,axiom,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
fof(f63,axiom,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).
fof(f64,axiom,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
fof(f65,axiom,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).
fof(f66,axiom,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).
fof(f67,axiom,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).
fof(f68,axiom,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).
fof(f69,axiom,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).
fof(f70,axiom,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).
fof(f71,axiom,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
fof(f72,axiom,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).
fof(f73,axiom,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
fof(f74,axiom,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp68) ).
fof(f75,axiom,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
fof(f76,axiom,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).
fof(f77,axiom,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp71) ).
fof(f78,axiom,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f79,axiom,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp73) ).
fof(f80,axiom,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp74) ).
fof(f81,axiom,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).
fof(f82,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f90,plain,
e_1244 = select(a_1284,i8),
inference(superposition,[],[f1,f27]) ).
fof(f91,plain,
e_1244 = e_1285,
inference(forward_demodulation,[],[f90,f65]) ).
fof(f93,plain,
a_1245 = store(a1,i8,e_1285),
inference(backward_demodulation,[],[f6,f91]) ).
fof(f94,plain,
a_1284 = store(a_1283,i8,e_1285),
inference(backward_demodulation,[],[f27,f91]) ).
fof(f95,plain,
e_1285 = select(a1,i7),
inference(backward_demodulation,[],[f46,f91]) ).
fof(f110,plain,
! [X0] : store(a1,i7,X0) = store(a_1283,i7,X0),
inference(superposition,[],[f4,f26]) ).
fof(f111,plain,
! [X0] : store(a1,i8,X0) = store(a_1245,i8,X0),
inference(superposition,[],[f4,f93]) ).
fof(f112,plain,
! [X0] : store(a_1247,i6,X0) = store(a_1249,i6,X0),
inference(superposition,[],[f4,f8]) ).
fof(f113,plain,
! [X0] : store(a_1251,i8,X0) = store(a_1253,i8,X0),
inference(superposition,[],[f4,f10]) ).
fof(f114,plain,
! [X0] : store(a_1255,i4,X0) = store(a_1257,i4,X0),
inference(superposition,[],[f4,f12]) ).
fof(f115,plain,
! [X0] : store(a_1259,i7,X0) = store(a_1261,i7,X0),
inference(superposition,[],[f4,f14]) ).
fof(f116,plain,
! [X0] : store(a_1263,i4,X0) = store(a_1265,i4,X0),
inference(superposition,[],[f4,f16]) ).
fof(f118,plain,
! [X0] : store(a_1267,i0,X0) = store(a_1269,i0,X0),
inference(superposition,[],[f4,f18]) ).
fof(f119,plain,
! [X0] : store(a_1274,i3,X0) = store(a_1276,i3,X0),
inference(superposition,[],[f4,f22]) ).
fof(f121,plain,
! [X0] : store(a_1283,i8,X0) = store(a_1284,i8,X0),
inference(superposition,[],[f4,f94]) ).
fof(f122,plain,
! [X0] : store(a_1284,i6,X0) = store(a_1286,i6,X0),
inference(superposition,[],[f4,f28]) ).
fof(f123,plain,
! [X0] : store(a_1288,i5,X0) = store(a_1290,i5,X0),
inference(superposition,[],[f4,f30]) ).
fof(f124,plain,
! [X0] : store(a_1292,i4,X0) = store(a_1294,i4,X0),
inference(superposition,[],[f4,f32]) ).
fof(f125,plain,
! [X0] : store(a_1300,i4,X0) = store(a_1302,i4,X0),
inference(superposition,[],[f4,f36]) ).
fof(f126,plain,
! [X0] : store(a_1307,i2,X0) = store(a_1309,i2,X0),
inference(superposition,[],[f4,f40]) ).
fof(f127,plain,
! [X0] : store(a_1311,i3,X0) = store(a_1313,i3,X0),
inference(superposition,[],[f4,f42]) ).
fof(f128,plain,
! [X0] : store(a_1317,i9,X0) = store(a_1319,i9,X0),
inference(superposition,[],[f4,f45]) ).
fof(f130,plain,
a_1313 = store(a_1313,i3,e_1312),
inference(backward_demodulation,[],[f42,f127]) ).
fof(f131,plain,
a_1309 = store(a_1309,i2,e_1308),
inference(backward_demodulation,[],[f40,f126]) ).
fof(f132,plain,
a_1302 = store(a_1302,i4,e_1301),
inference(backward_demodulation,[],[f36,f125]) ).
fof(f133,plain,
a_1294 = store(a_1294,i4,e_1293),
inference(backward_demodulation,[],[f32,f124]) ).
fof(f134,plain,
a_1290 = store(a_1290,i5,e_1289),
inference(backward_demodulation,[],[f30,f123]) ).
fof(f135,plain,
a_1286 = store(a_1286,i6,e_1285),
inference(backward_demodulation,[],[f28,f122]) ).
fof(f136,plain,
a_1276 = store(a_1276,i3,e_1275),
inference(backward_demodulation,[],[f22,f119]) ).
fof(f137,plain,
a_1269 = store(a_1269,i0,e_1268),
inference(backward_demodulation,[],[f18,f118]) ).
fof(f138,plain,
a_1265 = store(a_1265,i4,e_1264),
inference(backward_demodulation,[],[f16,f116]) ).
fof(f139,plain,
a_1261 = store(a_1261,i7,e_1260),
inference(backward_demodulation,[],[f14,f115]) ).
fof(f140,plain,
a_1257 = store(a_1257,i4,e_1256),
inference(backward_demodulation,[],[f12,f114]) ).
fof(f141,plain,
a_1253 = store(a_1253,i8,e_1252),
inference(backward_demodulation,[],[f10,f113]) ).
fof(f142,plain,
a_1249 = store(a_1249,i6,e_1248),
inference(backward_demodulation,[],[f8,f112]) ).
fof(f143,plain,
a_1245 = store(a_1245,i8,e_1285),
inference(backward_demodulation,[],[f93,f111]) ).
fof(f144,plain,
a_1283 = store(a_1283,i7,e_1246),
inference(backward_demodulation,[],[f26,f110]) ).
fof(f146,plain,
a_1269 = a_1270,
inference(backward_demodulation,[],[f19,f137]) ).
fof(f147,plain,
a_1272 = store(a_1269,i1,e_1271),
inference(backward_demodulation,[],[f20,f146]) ).
fof(f148,plain,
e_1271 = select(a_1269,i2),
inference(backward_demodulation,[],[f59,f146]) ).
fof(f149,plain,
e_1273 = select(a_1269,i1),
inference(backward_demodulation,[],[f60,f146]) ).
fof(f152,plain,
! [X0] : store(a_1278,i9,X0) = store(a_1280,i9,X0),
inference(superposition,[],[f4,f24]) ).
fof(f154,plain,
a_1280 = store(a_1280,i9,e_1279),
inference(backward_demodulation,[],[f24,f152]) ).
fof(f155,plain,
! [X0] : store(a_1296,i1,X0) = store(a_1298,i1,X0),
inference(superposition,[],[f4,f34]) ).
fof(f157,plain,
a_1298 = store(a_1298,i1,e_1297),
inference(backward_demodulation,[],[f34,f155]) ).
fof(f158,plain,
! [X0] : store(a_1304,i0,X0) = store(a_1306,i0,X0),
inference(superposition,[],[f4,f38]) ).
fof(f160,plain,
a_1306 = store(a_1306,i0,e_1305),
inference(backward_demodulation,[],[f38,f158]) ).
fof(f161,plain,
a_1306 = a_1307,
inference(backward_demodulation,[],[f39,f160]) ).
fof(f162,plain,
! [X0] : store(a_1309,i2,X0) = store(a_1306,i2,X0),
inference(backward_demodulation,[],[f126,f161]) ).
fof(f163,plain,
e_1308 = select(a_1306,i1),
inference(backward_demodulation,[],[f76,f161]) ).
fof(f164,plain,
e_1310 = select(a_1306,i2),
inference(backward_demodulation,[],[f77,f161]) ).
fof(f165,plain,
a_1309 = store(a_1306,i2,e_1308),
inference(backward_demodulation,[],[f131,f162]) ).
fof(f169,plain,
e_1246 = select(a_1247,i7),
inference(superposition,[],[f1,f7]) ).
fof(f170,plain,
! [X0] : store(a_1315,i5,X0) = store(a_1317,i5,X0),
inference(superposition,[],[f4,f44]) ).
fof(f172,plain,
a_1317 = store(a_1317,i5,e_1316),
inference(backward_demodulation,[],[f44,f170]) ).
fof(f182,plain,
e_1287 = select(a_1288,i8),
inference(superposition,[],[f1,f29]) ).
fof(f183,plain,
e_1287 = e_1289,
inference(backward_demodulation,[],[f67,f182]) ).
fof(f184,plain,
a_1290 = store(a_1290,i5,e_1287),
inference(backward_demodulation,[],[f134,f183]) ).
fof(f192,plain,
! [X0] : store(a_1251,i8,X0) = store(a_1249,i8,X0),
inference(superposition,[],[f4,f9]) ).
fof(f193,plain,
e_1250 = select(a_1251,i8),
inference(superposition,[],[f1,f9]) ).
fof(f194,plain,
e_1250 = e_1254,
inference(backward_demodulation,[],[f51,f193]) ).
fof(f195,plain,
! [X0] : store(a_1253,i8,X0) = store(a_1249,i8,X0),
inference(backward_demodulation,[],[f113,f192]) ).
fof(f197,plain,
a_1255 = store(a_1253,i5,e_1250),
inference(backward_demodulation,[],[f11,f194]) ).
fof(f198,plain,
a_1253 = store(a_1249,i8,e_1252),
inference(backward_demodulation,[],[f141,f195]) ).
fof(f210,plain,
a1 = store(a1,i7,e_1285),
inference(superposition,[],[f3,f95]) ).
fof(f212,plain,
a_1269 = store(a_1269,i2,e_1271),
inference(superposition,[],[f3,f148]) ).
fof(f214,plain,
a_1306 = store(a_1306,i1,e_1308),
inference(superposition,[],[f3,f163]) ).
fof(f218,plain,
a1 = store(a_1283,i7,e_1285),
inference(forward_demodulation,[],[f210,f110]) ).
fof(f220,plain,
a_1278 = store(a_1278,i9,e_1281),
inference(superposition,[],[f3,f64]) ).
fof(f221,plain,
a_1278 = store(a_1280,i9,e_1281),
inference(forward_demodulation,[],[f220,f152]) ).
fof(f231,plain,
a_1259 = store(a_1259,i1,e_1260),
inference(superposition,[],[f3,f54]) ).
fof(f250,plain,
a_1251 = store(a_1251,i5,e_1252),
inference(superposition,[],[f3,f50]) ).
fof(f251,plain,
a_1278 = store(a_1278,i5,e_1279),
inference(superposition,[],[f3,f63]) ).
fof(f252,plain,
a_1259 = store(a_1259,i7,e_1262),
inference(superposition,[],[f3,f55]) ).
fof(f253,plain,
a_1259 = store(a_1261,i7,e_1262),
inference(forward_demodulation,[],[f252,f115]) ).
fof(f260,plain,
a_1267 = store(a_1267,i0,e_1268),
inference(superposition,[],[f3,f58]) ).
fof(f261,plain,
a_1267 = store(a_1269,i0,e_1268),
inference(forward_demodulation,[],[f260,f118]) ).
fof(f262,plain,
a_1267 = a_1269,
inference(forward_demodulation,[],[f261,f137]) ).
fof(f265,plain,
store(a_1265,i5,e_1266) = a_1269,
inference(backward_demodulation,[],[f17,f262]) ).
fof(f267,plain,
a_1304 = store(a_1304,i0,e_1305),
inference(superposition,[],[f3,f75]) ).
fof(f268,plain,
a_1304 = store(a_1306,i0,e_1305),
inference(forward_demodulation,[],[f267,f158]) ).
fof(f269,plain,
a_1304 = a_1306,
inference(forward_demodulation,[],[f268,f160]) ).
fof(f272,plain,
store(a_1302,i5,e_1303) = a_1306,
inference(backward_demodulation,[],[f37,f269]) ).
fof(f416,plain,
! [X0,X1] :
( store(store(a_1269,X0,X1),i1,e_1271) = store(a_1272,X0,X1)
| i1 = X0 ),
inference(superposition,[],[f5,f147]) ).
fof(f425,plain,
! [X0,X1] :
( store(store(a_1283,X0,X1),i8,e_1285) = store(a_1284,X0,X1)
| i8 = X0 ),
inference(superposition,[],[f5,f94]) ).
fof(f426,plain,
! [X0,X1] :
( store(a_1283,X0,X1) = store(store(a_1283,X0,X1),i7,e_1246)
| i7 = X0 ),
inference(superposition,[],[f5,f144]) ).
fof(f431,plain,
! [X0,X1] :
( store(store(a_1290,X0,X1),i8,e_1291) = store(a_1292,X0,X1)
| i8 = X0 ),
inference(superposition,[],[f5,f31]) ).
fof(f437,plain,
! [X0,X1] :
( store(store(a_1298,X0,X1),i7,e_1299) = store(a_1300,X0,X1)
| i7 = X0 ),
inference(superposition,[],[f5,f35]) ).
fof(f438,plain,
! [X0,X1] :
( store(a_1298,X0,X1) = store(store(a_1298,X0,X1),i1,e_1297)
| i1 = X0 ),
inference(superposition,[],[f5,f157]) ).
fof(f449,plain,
! [X0,X1] :
( store(store(a_1317,X0,X1),i9,e_1318) = store(a_1319,X0,X1)
| i9 = X0 ),
inference(superposition,[],[f5,f45]) ).
fof(f450,plain,
! [X0,X1] :
( store(a_1317,X0,X1) = store(store(a_1317,X0,X1),i5,e_1316)
| i5 = X0 ),
inference(superposition,[],[f5,f172]) ).
fof(f2147,definition,
( spl0_7
<=> i7 = i1 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f2149,plain,
( i7 = i1
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f2147]) ).
fof(f2391,definition,
( spl0_10
<=> e_1248 = e_1285 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f2393,plain,
( e_1248 = e_1285
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f2391]) ).
fof(f5163,plain,
( a_1300 = store(a_1300,i1,e_1297)
| i7 = i1 ),
inference(superposition,[],[f438,f35]) ).
fof(f5247,definition,
( spl0_24
<=> i1 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f5249,plain,
( i1 = i2
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f5247]) ).
fof(f5260,plain,
( a_1284 = store(a_1284,i7,e_1246)
| i8 = i7 ),
inference(superposition,[],[f426,f94]) ).
fof(f5278,definition,
( spl0_26
<=> i8 = i7 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f5280,plain,
( i8 = i7
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f5278]) ).
fof(f5282,definition,
( spl0_27
<=> a_1284 = store(a_1284,i7,e_1246) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f5283,plain,
( a_1284 != store(a_1284,i7,e_1246)
| spl0_27 ),
inference(avatar_component_clause,[],[f5282]) ).
fof(f5284,plain,
( a_1284 = store(a_1284,i7,e_1246)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f5282]) ).
fof(f5285,plain,
( spl0_26
| spl0_27 ),
inference(avatar_split_clause,[],[f5260,f5282,f5278]) ).
fof(f5292,plain,
( store(a1,i8,e_1285) = store(a_1284,i7,e_1285)
| i8 = i7 ),
inference(superposition,[],[f425,f218]) ).
fof(f5312,plain,
( store(a_1245,i8,e_1285) = store(a_1284,i7,e_1285)
| i8 = i7 ),
inference(forward_demodulation,[],[f5292,f111]) ).
fof(f5314,plain,
( a_1245 = store(a_1284,i7,e_1285)
| i8 = i7 ),
inference(forward_demodulation,[],[f5312,f143]) ).
fof(f5316,definition,
( spl0_28
<=> a_1245 = store(a_1284,i7,e_1285) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f5317,plain,
( a_1245 != store(a_1284,i7,e_1285)
| spl0_28 ),
inference(avatar_component_clause,[],[f5316]) ).
fof(f5318,plain,
( a_1245 = store(a_1284,i7,e_1285)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f5316]) ).
fof(f5319,plain,
( spl0_26
| spl0_28 ),
inference(avatar_split_clause,[],[f5314,f5316,f5278]) ).
fof(f5322,plain,
( ! [X0] : store(a_1245,i7,X0) = store(a_1284,i7,X0)
| ~ spl0_28 ),
inference(superposition,[],[f4,f5318]) ).
fof(f5327,plain,
( store(a_1245,i7,e_1246) = a_1284
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f5284,f5322]) ).
fof(f5329,plain,
( a_1247 = a_1284
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5327,f7]) ).
fof(f5330,plain,
( e_1285 = select(a_1247,i8)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f65,f5329]) ).
fof(f5331,plain,
( e_1287 = select(a_1247,i6)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f66,f5329]) ).
fof(f5334,plain,
( ! [X0] : store(a_1247,i6,X0) = store(a_1286,i6,X0)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f122,f5329]) ).
fof(f5365,plain,
( ! [X0] : store(a_1249,i6,X0) = store(a_1286,i6,X0)
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5334,f112]) ).
fof(f5367,plain,
( e_1250 = e_1287
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5331,f49]) ).
fof(f5368,plain,
( e_1248 = e_1285
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5330,f48]) ).
fof(f5369,plain,
( a_1286 = store(a_1249,i6,e_1285)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f135,f5365]) ).
fof(f5372,plain,
( a_1288 = store(a_1286,i8,e_1250)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f29,f5367]) ).
fof(f5375,plain,
( a_1290 = store(a_1290,i5,e_1250)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f184,f5367]) ).
fof(f5416,plain,
( a_1286 = store(a_1249,i6,e_1248)
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5369,f5368]) ).
fof(f5417,plain,
( a_1249 = a_1286
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5416,f142]) ).
fof(f5423,plain,
( store(a_1249,i8,e_1250) = a_1288
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f5372,f5417]) ).
fof(f5432,plain,
( a_1251 = a_1288
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5423,f9]) ).
fof(f5433,plain,
( e_1291 = select(a_1251,i5)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f68,f5432]) ).
fof(f5434,plain,
( ! [X0] : store(a_1290,i5,X0) = store(a_1251,i5,X0)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f123,f5432]) ).
fof(f5454,plain,
( a_1251 = store(a_1290,i5,e_1252)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f250,f5434]) ).
fof(f5455,plain,
( e_1252 = e_1291
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f5433,f50]) ).
fof(f5456,plain,
( a_1292 = store(a_1290,i8,e_1252)
| ~ spl0_27
| ~ spl0_28 ),
inference(backward_demodulation,[],[f31,f5455]) ).
fof(f5464,plain,
( spl0_10
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f5368,f5316,f5282,f2391]) ).
fof(f5631,plain,
( a_1272 = store(a_1269,i2,e_1271)
| ~ spl0_24 ),
inference(backward_demodulation,[],[f147,f5249]) ).
fof(f5632,plain,
( e_1273 = select(a_1269,i2)
| ~ spl0_24 ),
inference(backward_demodulation,[],[f149,f5249]) ).
fof(f5640,plain,
( a_1306 = store(a_1306,i2,e_1308)
| ~ spl0_24 ),
inference(backward_demodulation,[],[f214,f5249]) ).
fof(f5678,plain,
( e_1246 = select(a1,i7)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f47,f5280]) ).
fof(f5679,plain,
( e_1248 = select(a_1247,i7)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f48,f5280]) ).
fof(f5681,plain,
( ! [X0] : store(a1,i7,X0) = store(a_1245,i7,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f111,f5280]) ).
fof(f5710,plain,
( a_1284 = store(a_1283,i7,e_1285)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f94,f5280]) ).
fof(f5711,plain,
( ! [X0] : store(a_1283,i7,X0) = store(a_1284,i7,X0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f121,f5280]) ).
fof(f5731,plain,
( a_1245 = store(a_1245,i7,e_1285)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f143,f5280]) ).
fof(f5889,plain,
( a_1306 = a_1309
| ~ spl0_24 ),
inference(backward_demodulation,[],[f165,f5640]) ).
fof(f5896,plain,
( e_1271 = e_1273
| ~ spl0_24 ),
inference(forward_demodulation,[],[f5632,f148]) ).
fof(f5897,plain,
( a_1269 = a_1272
| ~ spl0_24 ),
inference(forward_demodulation,[],[f5631,f212]) ).
fof(f5914,plain,
( ! [X0] : store(a_1283,i7,X0) = store(a_1245,i7,X0)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f110,f5681]) ).
fof(f5915,plain,
( e_1246 = e_1248
| ~ spl0_26 ),
inference(backward_demodulation,[],[f169,f5679]) ).
fof(f5916,plain,
( e_1246 = e_1285
| ~ spl0_26 ),
inference(forward_demodulation,[],[f5678,f95]) ).
fof(f5917,plain,
( a1 = a_1284
| ~ spl0_26 ),
inference(forward_demodulation,[],[f5710,f218]) ).
fof(f5918,plain,
( a_1284 != store(a_1283,i7,e_1246)
| ~ spl0_26
| spl0_27 ),
inference(backward_demodulation,[],[f5283,f5711]) ).
fof(f6105,plain,
( a1 = store(a_1245,i7,e_1285)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f218,f5914]) ).
fof(f6114,plain,
( e_1248 = e_1285
| ~ spl0_26 ),
inference(forward_demodulation,[],[f5916,f5915]) ).
fof(f6128,plain,
( store(a_1245,i7,e_1246) != a_1284
| ~ spl0_26
| spl0_27 ),
inference(forward_demodulation,[],[f5918,f5914]) ).
fof(f6260,plain,
( a_1245 = a1
| ~ spl0_26 ),
inference(forward_demodulation,[],[f6105,f5731]) ).
fof(f6278,plain,
( a_1245 = store(a_1245,i7,e_1248)
| ~ spl0_26 ),
inference(backward_demodulation,[],[f5731,f6114]) ).
fof(f6286,plain,
( a1 != store(a_1245,i7,e_1246)
| ~ spl0_26
| spl0_27 ),
inference(forward_demodulation,[],[f6128,f5917]) ).
fof(f6339,plain,
( a_1245 = a_1284
| ~ spl0_26 ),
inference(backward_demodulation,[],[f5917,f6260]) ).
fof(f6381,plain,
( a1 != store(a_1245,i7,e_1248)
| ~ spl0_26
| spl0_27 ),
inference(forward_demodulation,[],[f6286,f5915]) ).
fof(f6454,plain,
( a_1245 != a1
| ~ spl0_26
| spl0_27 ),
inference(forward_demodulation,[],[f6381,f6278]) ).
fof(f6492,plain,
( $false
| ~ spl0_26
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f6454,f6260]) ).
fof(f6493,plain,
( ~ spl0_26
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f6492]) ).
fof(f6660,plain,
( spl0_10
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f6114,f5278,f2391]) ).
fof(f9778,plain,
( a_1245 = store(a_1245,i8,e_1248)
| ~ spl0_10 ),
inference(forward_demodulation,[],[f143,f2393]) ).
fof(f9842,plain,
( ! [X0,X1] :
( store(a_1292,X0,X1) = store(store(a_1290,X0,X1),i8,e_1252)
| i8 = X0 )
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f431,f5455]) ).
fof(f11299,plain,
( store(a_1290,i8,e_1252) = store(a_1292,i5,e_1250)
| i8 = i5
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f9842,f5375]) ).
fof(f11300,plain,
( store(a_1251,i8,e_1252) = store(a_1292,i5,e_1252)
| i8 = i5
| ~ spl0_27
| ~ spl0_28 ),
inference(superposition,[],[f9842,f5454]) ).
fof(f11320,plain,
( store(a_1249,i8,e_1252) = store(a_1292,i5,e_1252)
| i8 = i5
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f11300,f192]) ).
fof(f11321,plain,
( a_1292 = store(a_1292,i5,e_1250)
| i8 = i5
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f11299,f5456]) ).
fof(f11322,plain,
( a_1253 = store(a_1292,i5,e_1252)
| i8 = i5
| ~ spl0_27
| ~ spl0_28 ),
inference(forward_demodulation,[],[f11320,f198]) ).
fof(f11324,definition,
( spl0_33
<=> i8 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f11326,plain,
( i8 = i5
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f11324]) ).
fof(f11328,definition,
( spl0_34
<=> a_1253 = store(a_1292,i5,e_1252) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f11330,plain,
( a_1253 = store(a_1292,i5,e_1252)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f11328]) ).
fof(f11331,plain,
( spl0_33
| spl0_34
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f11322,f5316,f5282,f11328,f11324]) ).
fof(f11334,plain,
( ! [X0] : store(a_1253,i5,X0) = store(a_1292,i5,X0)
| ~ spl0_34 ),
inference(superposition,[],[f4,f11330]) ).
fof(f11339,plain,
( a_1292 = store(a_1253,i5,e_1250)
| i8 = i5
| ~ spl0_27
| ~ spl0_28
| ~ spl0_34 ),
inference(backward_demodulation,[],[f11321,f11334]) ).
fof(f11341,plain,
( a_1255 = a_1292
| i8 = i5
| ~ spl0_27
| ~ spl0_28
| ~ spl0_34 ),
inference(forward_demodulation,[],[f11339,f197]) ).
fof(f11343,definition,
( spl0_35
<=> a_1255 = a_1292 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f11344,plain,
( a_1255 != a_1292
| spl0_35 ),
inference(avatar_component_clause,[],[f11343]) ).
fof(f11345,plain,
( a_1255 = a_1292
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f11343]) ).
fof(f11346,plain,
( spl0_33
| spl0_35
| ~ spl0_27
| ~ spl0_28
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f11341,f11328,f5316,f5282,f11343,f11324]) ).
fof(f11347,plain,
( e_1293 = select(a_1255,i9)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f69,f11345]) ).
fof(f11348,plain,
( e_1295 = select(a_1255,i4)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f70,f11345]) ).
fof(f11349,plain,
( ! [X0] : store(a_1255,i4,X0) = store(a_1294,i4,X0)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f124,f11345]) ).
fof(f11383,plain,
( ! [X0] : store(a_1257,i4,X0) = store(a_1294,i4,X0)
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11349,f114]) ).
fof(f11384,plain,
( e_1258 = e_1295
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11348,f53]) ).
fof(f11385,plain,
( e_1256 = e_1293
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11347,f52]) ).
fof(f11386,plain,
( a_1294 = store(a_1257,i4,e_1293)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f133,f11383]) ).
fof(f11389,plain,
( a_1296 = store(a_1294,i9,e_1258)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f33,f11384]) ).
fof(f11408,plain,
( a_1294 = store(a_1257,i4,e_1256)
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11386,f11385]) ).
fof(f11409,plain,
( a_1257 = a_1294
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11408,f140]) ).
fof(f11415,plain,
( store(a_1257,i9,e_1258) = a_1296
| ~ spl0_35 ),
inference(backward_demodulation,[],[f11389,f11409]) ).
fof(f11424,plain,
( a_1259 = a_1296
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11415,f13]) ).
fof(f11425,plain,
( e_1297 = select(a_1259,i7)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f71,f11424]) ).
fof(f11426,plain,
( e_1299 = select(a_1259,i1)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f72,f11424]) ).
fof(f11427,plain,
( ! [X0] : store(a_1298,i1,X0) = store(a_1259,i1,X0)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f155,f11424]) ).
fof(f11452,plain,
( a_1259 = store(a_1298,i1,e_1260)
| ~ spl0_35 ),
inference(backward_demodulation,[],[f231,f11427]) ).
fof(f11453,plain,
( e_1260 = e_1299
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11426,f54]) ).
fof(f11454,plain,
( e_1262 = e_1297
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11425,f55]) ).
fof(f11457,plain,
( ! [X0,X1] :
( store(a_1300,X0,X1) = store(store(a_1298,X0,X1),i7,e_1260)
| i7 = X0 )
| ~ spl0_35 ),
inference(backward_demodulation,[],[f437,f11453]) ).
fof(f11468,plain,
( a_1300 = store(a_1300,i1,e_1262)
| i7 = i1
| ~ spl0_35 ),
inference(backward_demodulation,[],[f5163,f11454]) ).
fof(f11523,plain,
( store(a_1259,i7,e_1260) = store(a_1300,i1,e_1260)
| i7 = i1
| ~ spl0_35 ),
inference(superposition,[],[f11457,f11452]) ).
fof(f11543,plain,
( store(a_1261,i7,e_1260) = store(a_1300,i1,e_1260)
| i7 = i1
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11523,f115]) ).
fof(f11545,plain,
( a_1261 = store(a_1300,i1,e_1260)
| i7 = i1
| ~ spl0_35 ),
inference(forward_demodulation,[],[f11543,f139]) ).
fof(f11547,definition,
( spl0_36
<=> a_1261 = store(a_1300,i1,e_1260) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f11549,plain,
( a_1261 = store(a_1300,i1,e_1260)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f11547]) ).
fof(f11550,plain,
( spl0_7
| spl0_36
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f11545,f11343,f11547,f2147]) ).
fof(f11553,plain,
( ! [X0] : store(a_1261,i1,X0) = store(a_1300,i1,X0)
| ~ spl0_36 ),
inference(superposition,[],[f4,f11549]) ).
fof(f11558,plain,
( store(a_1261,i1,e_1262) = a_1300
| i7 = i1
| ~ spl0_35
| ~ spl0_36 ),
inference(backward_demodulation,[],[f11468,f11553]) ).
fof(f11560,plain,
( a_1263 = a_1300
| i7 = i1
| ~ spl0_35
| ~ spl0_36 ),
inference(forward_demodulation,[],[f11558,f15]) ).
fof(f11562,definition,
( spl0_37
<=> a_1263 = a_1300 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f11563,plain,
( a_1263 != a_1300
| spl0_37 ),
inference(avatar_component_clause,[],[f11562]) ).
fof(f11564,plain,
( a_1263 = a_1300
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f11562]) ).
fof(f11565,plain,
( spl0_7
| spl0_37
| ~ spl0_35
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f11560,f11547,f11343,f11562,f2147]) ).
fof(f11566,plain,
( e_1301 = select(a_1263,i5)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f73,f11564]) ).
fof(f11567,plain,
( e_1303 = select(a_1263,i4)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f74,f11564]) ).
fof(f11568,plain,
( ! [X0] : store(a_1263,i4,X0) = store(a_1302,i4,X0)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f125,f11564]) ).
fof(f11605,plain,
( ! [X0] : store(a_1265,i4,X0) = store(a_1302,i4,X0)
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11568,f116]) ).
fof(f11606,plain,
( e_1266 = e_1303
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11567,f57]) ).
fof(f11607,plain,
( e_1264 = e_1301
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11566,f56]) ).
fof(f11608,plain,
( a_1302 = store(a_1265,i4,e_1301)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f132,f11605]) ).
fof(f11612,plain,
( a_1306 = store(a_1302,i5,e_1266)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f272,f11606]) ).
fof(f11634,plain,
( a_1302 = store(a_1265,i4,e_1264)
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11608,f11607]) ).
fof(f11636,plain,
( a_1265 = a_1302
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11634,f138]) ).
fof(f11654,plain,
( store(a_1265,i5,e_1266) = a_1306
| ~ spl0_37 ),
inference(backward_demodulation,[],[f11612,f11636]) ).
fof(f11665,plain,
( a_1269 = a_1306
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11654,f265]) ).
fof(f11672,plain,
( e_1308 = select(a_1269,i1)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f163,f11665]) ).
fof(f11673,plain,
( e_1310 = select(a_1269,i2)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f164,f11665]) ).
fof(f11674,plain,
( a_1309 = store(a_1269,i2,e_1308)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f165,f11665]) ).
fof(f11709,plain,
( e_1271 = e_1310
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11673,f148]) ).
fof(f11710,plain,
( e_1273 = e_1308
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11672,f149]) ).
fof(f11712,plain,
( a_1311 = store(a_1309,i1,e_1271)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f41,f11709]) ).
fof(f11722,plain,
( a_1309 = store(a_1269,i2,e_1273)
| ~ spl0_37 ),
inference(backward_demodulation,[],[f11674,f11710]) ).
fof(f11743,plain,
( store(a_1272,i2,e_1273) = store(a_1309,i1,e_1271)
| i1 = i2
| ~ spl0_37 ),
inference(superposition,[],[f416,f11722]) ).
fof(f11751,plain,
( store(a_1272,i2,e_1273) = a_1311
| i1 = i2
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11743,f11712]) ).
fof(f11752,plain,
( a_1274 = a_1311
| i1 = i2
| ~ spl0_37 ),
inference(forward_demodulation,[],[f11751,f21]) ).
fof(f11754,definition,
( spl0_38
<=> a_1274 = a_1311 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f11755,plain,
( a_1274 != a_1311
| spl0_38 ),
inference(avatar_component_clause,[],[f11754]) ).
fof(f11756,plain,
( a_1274 = a_1311
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f11754]) ).
fof(f11757,plain,
( spl0_24
| spl0_38
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f11752,f11562,f11754,f5247]) ).
fof(f11758,plain,
( e_1312 = select(a_1274,i0)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f78,f11756]) ).
fof(f11759,plain,
( e_1314 = select(a_1274,i3)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f79,f11756]) ).
fof(f11760,plain,
( ! [X0] : store(a_1274,i3,X0) = store(a_1313,i3,X0)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f127,f11756]) ).
fof(f11783,plain,
( ! [X0] : store(a_1276,i3,X0) = store(a_1313,i3,X0)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11760,f119]) ).
fof(f11784,plain,
( e_1277 = e_1314
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11759,f62]) ).
fof(f11785,plain,
( e_1275 = e_1312
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11758,f61]) ).
fof(f11787,plain,
( a_1313 = store(a_1276,i3,e_1312)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f130,f11783]) ).
fof(f11789,plain,
( a_1315 = store(a_1313,i0,e_1277)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f43,f11784]) ).
fof(f11805,plain,
( a_1313 = store(a_1276,i3,e_1275)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11787,f11785]) ).
fof(f11806,plain,
( a_1276 = a_1313
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11805,f136]) ).
fof(f11812,plain,
( store(a_1276,i0,e_1277) = a_1315
| ~ spl0_38 ),
inference(backward_demodulation,[],[f11789,f11806]) ).
fof(f11821,plain,
( a_1278 = a_1315
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11812,f23]) ).
fof(f11822,plain,
( e_1316 = select(a_1278,i9)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f80,f11821]) ).
fof(f11823,plain,
( e_1318 = select(a_1278,i5)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f81,f11821]) ).
fof(f11824,plain,
( ! [X0] : store(a_1317,i5,X0) = store(a_1278,i5,X0)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f170,f11821]) ).
fof(f11846,plain,
( a_1278 = store(a_1317,i5,e_1279)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f251,f11824]) ).
fof(f11847,plain,
( e_1279 = e_1318
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11823,f63]) ).
fof(f11848,plain,
( e_1281 = e_1316
| ~ spl0_38 ),
inference(forward_demodulation,[],[f11822,f64]) ).
fof(f11849,plain,
( a_1319 = store(a_1317,i9,e_1279)
| ~ spl0_38 ),
inference(backward_demodulation,[],[f45,f11847]) ).
fof(f11851,plain,
( ! [X0,X1] :
( store(a_1319,X0,X1) = store(store(a_1317,X0,X1),i9,e_1279)
| i9 = X0 )
| ~ spl0_38 ),
inference(backward_demodulation,[],[f449,f11847]) ).
fof(f11858,plain,
( ! [X0,X1] :
( store(a_1317,X0,X1) = store(store(a_1317,X0,X1),i5,e_1281)
| i5 = X0 )
| ~ spl0_38 ),
inference(backward_demodulation,[],[f450,f11848]) ).
fof(f12057,definition,
( spl0_44
<=> i5 = i9 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f12059,plain,
( i5 = i9
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f12057]) ).
fof(f12352,plain,
( a_1319 = store(a_1319,i5,e_1281)
| i5 = i9
| ~ spl0_38 ),
inference(superposition,[],[f11858,f11849]) ).
fof(f12376,plain,
( store(a_1278,i9,e_1279) = store(a_1319,i5,e_1279)
| i5 = i9
| ~ spl0_38 ),
inference(superposition,[],[f11851,f11846]) ).
fof(f12396,plain,
( store(a_1280,i9,e_1279) = store(a_1319,i5,e_1279)
| i5 = i9
| ~ spl0_38 ),
inference(forward_demodulation,[],[f12376,f152]) ).
fof(f12398,plain,
( a_1280 = store(a_1319,i5,e_1279)
| i5 = i9
| ~ spl0_38 ),
inference(forward_demodulation,[],[f12396,f154]) ).
fof(f12400,definition,
( spl0_50
<=> a_1280 = store(a_1319,i5,e_1279) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f12402,plain,
( a_1280 = store(a_1319,i5,e_1279)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f12400]) ).
fof(f12403,plain,
( spl0_44
| spl0_50
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f12398,f11754,f12400,f12057]) ).
fof(f12406,plain,
( ! [X0] : store(a_1280,i5,X0) = store(a_1319,i5,X0)
| ~ spl0_50 ),
inference(superposition,[],[f4,f12402]) ).
fof(f12411,plain,
( store(a_1280,i5,e_1281) = a_1319
| i5 = i9
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f12352,f12406]) ).
fof(f12413,plain,
( a_1282 = a_1319
| i5 = i9
| ~ spl0_38
| ~ spl0_50 ),
inference(forward_demodulation,[],[f12411,f25]) ).
fof(f12414,plain,
( i5 = i9
| ~ spl0_38
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f12413,f82]) ).
fof(f12415,plain,
( a_1282 = store(a_1280,i9,e_1281)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f25,f12414]) ).
fof(f12418,plain,
( e_1279 = select(a_1278,i9)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f63,f12414]) ).
fof(f12512,plain,
( ! [X0] : store(a_1319,i9,X0) = store(a_1280,i9,X0)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f12406,f12414]) ).
fof(f12520,plain,
( ! [X0] : store(a_1317,i9,X0) = store(a_1280,i9,X0)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f128,f12512]) ).
fof(f12582,plain,
( e_1279 = e_1281
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f64,f12418]) ).
fof(f12585,plain,
( a_1319 = store(a_1280,i9,e_1279)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f11849,f12520]) ).
fof(f12652,plain,
( a_1282 = store(a_1280,i9,e_1279)
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f12415,f12582]) ).
fof(f12661,plain,
( a_1280 = a_1319
| ~ spl0_38
| ~ spl0_50 ),
inference(forward_demodulation,[],[f12585,f154]) ).
fof(f12710,plain,
( a_1280 = a_1282
| ~ spl0_38
| ~ spl0_50 ),
inference(forward_demodulation,[],[f12652,f154]) ).
fof(f12714,plain,
( a_1280 != a_1282
| ~ spl0_38
| ~ spl0_50 ),
inference(backward_demodulation,[],[f82,f12661]) ).
fof(f12775,plain,
( $false
| ~ spl0_38
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f12714,f12710]) ).
fof(f12776,plain,
( ~ spl0_38
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f12775]) ).
fof(f12879,plain,
( a_1282 = store(a_1280,i9,e_1281)
| ~ spl0_44 ),
inference(forward_demodulation,[],[f25,f12059]) ).
fof(f12954,plain,
( a_1278 = store(a_1317,i9,e_1279)
| ~ spl0_38
| ~ spl0_44 ),
inference(forward_demodulation,[],[f11846,f12059]) ).
fof(f12975,plain,
( a_1278 = a_1282
| ~ spl0_44 ),
inference(backward_demodulation,[],[f221,f12879]) ).
fof(f13026,plain,
( a_1278 = a_1319
| ~ spl0_38
| ~ spl0_44 ),
inference(forward_demodulation,[],[f12954,f11849]) ).
fof(f13099,plain,
( a_1282 = a_1319
| ~ spl0_38
| ~ spl0_44 ),
inference(forward_demodulation,[],[f13026,f12975]) ).
fof(f13116,plain,
( $false
| ~ spl0_38
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f13099,f82]) ).
fof(f13117,plain,
( ~ spl0_38
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f13116]) ).
fof(f13180,plain,
( a_1255 = store(a_1253,i8,e_1250)
| ~ spl0_33 ),
inference(forward_demodulation,[],[f197,f11326]) ).
fof(f13225,plain,
( a_1251 = store(a_1290,i8,e_1252)
| ~ spl0_27
| ~ spl0_28
| ~ spl0_33 ),
inference(forward_demodulation,[],[f5454,f11326]) ).
fof(f13292,plain,
( store(a_1249,i8,e_1250) = a_1255
| ~ spl0_33 ),
inference(forward_demodulation,[],[f13180,f195]) ).
fof(f13324,plain,
( a_1251 = a_1292
| ~ spl0_27
| ~ spl0_28
| ~ spl0_33 ),
inference(backward_demodulation,[],[f5456,f13225]) ).
fof(f13367,plain,
( a_1251 = a_1255
| ~ spl0_33 ),
inference(forward_demodulation,[],[f13292,f9]) ).
fof(f13395,plain,
( a_1251 != a_1255
| ~ spl0_27
| ~ spl0_28
| ~ spl0_33
| spl0_35 ),
inference(backward_demodulation,[],[f11344,f13324]) ).
fof(f13446,plain,
( $false
| ~ spl0_27
| ~ spl0_28
| ~ spl0_33
| spl0_35 ),
inference(forward_subsumption_resolution,[],[f13395,f13367]) ).
fof(f13447,plain,
( ~ spl0_27
| ~ spl0_28
| ~ spl0_33
| spl0_35 ),
inference(avatar_contradiction_clause,[],[f13446]) ).
fof(f13694,plain,
( a_1245 != store(a_1284,i7,e_1248)
| ~ spl0_10
| spl0_28 ),
inference(forward_demodulation,[],[f5317,f2393]) ).
fof(f13780,plain,
( a_1245 = store(a_1245,i7,e_1248)
| ~ spl0_10
| ~ spl0_26 ),
inference(forward_demodulation,[],[f9778,f5280]) ).
fof(f13829,plain,
( a_1245 != store(a_1245,i7,e_1248)
| ~ spl0_10
| ~ spl0_26
| spl0_28 ),
inference(forward_demodulation,[],[f13694,f6339]) ).
fof(f13911,plain,
( $false
| ~ spl0_10
| ~ spl0_26
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f13829,f13780]) ).
fof(f13912,plain,
( ~ spl0_10
| ~ spl0_26
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f13911]) ).
fof(f17488,plain,
( a_1300 = store(a_1298,i7,e_1260)
| ~ spl0_35 ),
inference(forward_demodulation,[],[f35,f11453]) ).
fof(f17547,plain,
( a_1311 = store(a_1309,i2,e_1310)
| ~ spl0_24 ),
inference(forward_demodulation,[],[f41,f5249]) ).
fof(f17562,plain,
( a_1274 = store(a_1272,i2,e_1271)
| ~ spl0_24 ),
inference(backward_demodulation,[],[f21,f5896]) ).
fof(f17608,plain,
( a_1269 = a_1309
| ~ spl0_24
| ~ spl0_37 ),
inference(backward_demodulation,[],[f5889,f11665]) ).
fof(f17788,plain,
( a_1311 = store(a_1309,i2,e_1271)
| ~ spl0_24
| ~ spl0_37 ),
inference(forward_demodulation,[],[f17547,f11709]) ).
fof(f17800,plain,
( a_1274 = store(a_1269,i2,e_1271)
| ~ spl0_24 ),
inference(forward_demodulation,[],[f17562,f5897]) ).
fof(f17861,plain,
( a_1311 = store(a_1269,i2,e_1271)
| ~ spl0_24
| ~ spl0_37 ),
inference(forward_demodulation,[],[f17788,f17608]) ).
fof(f17870,plain,
( a_1269 = a_1274
| ~ spl0_24 ),
inference(forward_demodulation,[],[f17800,f212]) ).
fof(f17885,plain,
( a_1269 = a_1311
| ~ spl0_24
| ~ spl0_37 ),
inference(forward_demodulation,[],[f17861,f212]) ).
fof(f17900,plain,
( a_1269 != a_1311
| ~ spl0_24
| spl0_38 ),
inference(backward_demodulation,[],[f11755,f17870]) ).
fof(f17935,plain,
( $false
| ~ spl0_24
| ~ spl0_37
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f17900,f17885]) ).
fof(f17936,plain,
( ~ spl0_24
| ~ spl0_37
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f17935]) ).
fof(f18029,plain,
( a_1259 = store(a_1259,i7,e_1260)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f231,f2149]) ).
fof(f18033,plain,
( ! [X0] : store(a_1298,i7,X0) = store(a_1296,i7,X0)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f155,f2149]) ).
fof(f18056,plain,
( a_1263 = store(a_1261,i7,e_1262)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f15,f2149]) ).
fof(f18104,plain,
( a_1259 = store(a_1261,i7,e_1260)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f18029,f115]) ).
fof(f18108,plain,
( ! [X0] : store(a_1259,i7,X0) = store(a_1298,i7,X0)
| ~ spl0_7
| ~ spl0_35 ),
inference(forward_demodulation,[],[f18033,f11424]) ).
fof(f18127,plain,
( a_1259 = a_1263
| ~ spl0_7 ),
inference(forward_demodulation,[],[f18056,f253]) ).
fof(f18159,plain,
( a_1259 = a_1261
| ~ spl0_7 ),
inference(forward_demodulation,[],[f18104,f139]) ).
fof(f18161,plain,
( ! [X0] : store(a_1261,i7,X0) = store(a_1298,i7,X0)
| ~ spl0_7
| ~ spl0_35 ),
inference(forward_demodulation,[],[f18108,f115]) ).
fof(f18187,plain,
( a_1259 != a_1300
| ~ spl0_7
| spl0_37 ),
inference(backward_demodulation,[],[f11563,f18127]) ).
fof(f18233,plain,
( a_1300 = store(a_1261,i7,e_1260)
| ~ spl0_7
| ~ spl0_35 ),
inference(backward_demodulation,[],[f17488,f18161]) ).
fof(f18246,plain,
( a_1261 != a_1300
| ~ spl0_7
| spl0_37 ),
inference(forward_demodulation,[],[f18187,f18159]) ).
fof(f18269,plain,
( a_1261 = a_1300
| ~ spl0_7
| ~ spl0_35 ),
inference(forward_demodulation,[],[f18233,f139]) ).
fof(f18285,plain,
( $false
| ~ spl0_7
| ~ spl0_35
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f18269,f18246]) ).
fof(f18286,plain,
( ~ spl0_7
| ~ spl0_35
| spl0_37 ),
inference(avatar_contradiction_clause,[],[f18285]) ).
cnf(s19,plain,
( spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f5285]) ).
cnf(s20,plain,
( spl0_26
| spl0_28 ),
inference(sat_conversion,[],[f5319]) ).
cnf(s21,plain,
( spl0_10
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f5464]) ).
cnf(s25,plain,
( ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f6493]) ).
cnf(s27,plain,
( spl0_10
| ~ spl0_26 ),
inference(sat_conversion,[],[f6660]) ).
cnf(s37,plain,
( ~ spl0_27
| ~ spl0_28
| spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f11331]) ).
cnf(s38,plain,
( ~ spl0_27
| ~ spl0_28
| spl0_33
| ~ spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f11346]) ).
cnf(s39,plain,
( spl0_7
| ~ spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f11550]) ).
cnf(s40,plain,
( spl0_7
| ~ spl0_35
| ~ spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f11565]) ).
cnf(s41,plain,
( spl0_24
| ~ spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f11757]) ).
cnf(s48,plain,
( ~ spl0_38
| spl0_44
| spl0_50 ),
inference(sat_conversion,[],[f12403]) ).
cnf(s50,plain,
( ~ spl0_38
| ~ spl0_50 ),
inference(sat_conversion,[],[f12776]) ).
cnf(s51,plain,
( ~ spl0_38
| ~ spl0_44 ),
inference(sat_conversion,[],[f13117]) ).
cnf(s53,plain,
( ~ spl0_27
| ~ spl0_28
| ~ spl0_33
| spl0_35 ),
inference(sat_conversion,[],[f13447]) ).
cnf(s54,plain,
( ~ spl0_10
| ~ spl0_26
| spl0_28 ),
inference(sat_conversion,[],[f13912]) ).
cnf(s62,plain,
( ~ spl0_24
| ~ spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f17936]) ).
cnf(s63,plain,
( ~ spl0_7
| ~ spl0_35
| spl0_37 ),
inference(sat_conversion,[],[f18286]) ).
cnf(s64,plain,
spl0_10,
inference(rat,[],[s21,s19,s20,s27]) ).
cnf(s65,plain,
~ spl0_38,
inference(rat,[],[s48,s50,s51]) ).
cnf(s66,plain,
( ~ spl0_35
| spl0_37
| spl0_7 ),
inference(rat,[],[s40,s39]) ).
cnf(s67,plain,
( spl0_35
| spl0_33
| ~ spl0_28
| ~ spl0_27 ),
inference(rat,[],[s37,s38]) ).
cnf(s68,plain,
( spl0_35
| ~ spl0_27
| ~ spl0_28 ),
inference(rat,[],[s67,s53]) ).
cnf(s69,plain,
( spl0_26
| spl0_35 ),
inference(rat,[],[s68,s19,s20]) ).
cnf(s70,plain,
spl0_35,
inference(rat,[],[s68,s25,s54,s69,s64]) ).
cnf(s71,plain,
~ spl0_37,
inference(rat,[],[s62,s41,s65]) ).
cnf(s72,plain,
~ spl0_7,
inference(rat,[],[s63,s71,s70]) ).
cnf(s74,plain,
$false,
inference(rat,[],[s66,s72,s71,s70]) ).
fof(f18316,plain,
$false,
inference(avatar_sat_refutation,[],[s74]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV540-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n010.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:38:47 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.11/2.23 % (1872107)Input is clausal, will run a generic CNF schedule.
% 11.11/2.23 % (1872112)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2723516000:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.11/2.23 % (1872117)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2952850455:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.11/2.23 % (1872115)lrs+10_1_sil=8000:sp=occurrence:random_seed=4123937544:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.11/2.23 % (1872113)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3939384942:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.11/2.23 % (1872116)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=669157026:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.11/2.23 % (1872118)dis-21_1_sil=8000:lcm=predicate:random_seed=2627564264:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.11/2.23 % (1872114)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1148213394:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.11/2.23 % (1872118)Refutation not found, incomplete strategy
% 11.11/2.23 % (1872118)------------------------------
% 11.11/2.23 % (1872118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.23 % (1872118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.23 % (1872118)CaDiCaL version: 2.1.3
% 11.11/2.23 % (1872118)Termination reason: Refutation not found, incomplete strategy
% 11.11/2.23 % (1872118)Time elapsed: 0.002 s
% 11.11/2.23 % (1872118)Peak memory usage: 88 MB
% 11.11/2.23 % (1872118)Instructions burned: 2 (million)
% 11.11/2.23 % (1872115)Instruction limit reached!
% 11.11/2.23 % (1872115)------------------------------
% 11.11/2.23 % (1872115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.23 % (1872115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.23 % (1872115)CaDiCaL version: 2.1.3
% 11.11/2.23 % (1872115)Termination reason: Instruction limit
% 11.11/2.23 % (1872115)Termination phase: Saturation
% 11.11/2.23 % (1872115)Time elapsed: 0.060 s
% 11.11/2.23 % (1872115)Peak memory usage: 89 MB
% 11.11/2.23 % (1872115)Instructions burned: 107 (million)
% 11.11/2.23 % (1872116)Instruction limit reached!
% 11.11/2.23 % (1872116)------------------------------
% 11.11/2.23 % (1872116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.23 % (1872116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.23 % (1872116)CaDiCaL version: 2.1.3
% 11.11/2.23 % (1872116)Termination reason: Instruction limit
% 11.11/2.23 % (1872116)Termination phase: Saturation
% 11.11/2.23 % (1872116)Time elapsed: 0.062 s
% 11.11/2.23 % (1872116)Peak memory usage: 88 MB
% 11.11/2.23 % (1872116)Instructions burned: 115 (million)
% 11.11/2.23 % (1872117)Instruction limit reached!
% 11.11/2.23 % (1872117)------------------------------
% 11.11/2.23 % (1872117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.11/2.23 % (1872117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.11/2.23 % (1872117)CaDiCaL version: 2.1.3
% 11.11/2.23 % (1872117)Termination reason: Instruction limit
% 11.11/2.23 % (1872117)Termination phase: Saturation
% 11.11/2.23 % (1872117)Time elapsed: 0.105 s
% 11.11/2.23 % (1872117)Peak memory usage: 90 MB
% 11.11/2.23 % (1872117)Instructions burned: 180 (million)
% 11.11/2.23 % (1872126)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3722137863:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.11/2.23 % (1872127)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2154199687:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.11/2.23 % (1872118)------------------------------
% 11.11/2.23 % (1872118)------------------------------
% 11.11/2.23 % (1872128)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2091523586:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.11/2.23 % (1872127)Instruction limit reached!
% 11.11/2.23 % (1872127)------------------------------
% 22.19/3.91 % (1872127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872127)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872127)Termination reason: Instruction limit
% 22.19/3.91 % (1872127)Termination phase: Saturation
% 22.19/3.91 % (1872127)Time elapsed: 0.085 s
% 22.19/3.91 % (1872127)Peak memory usage: 98 MB
% 22.19/3.91 % (1872127)Instructions burned: 189 (million)
% 22.19/3.91 % (1872126)Instruction limit reached!
% 22.19/3.91 % (1872126)------------------------------
% 22.19/3.91 % (1872126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872126)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872126)Termination reason: Instruction limit
% 22.19/3.91 % (1872126)Termination phase: Saturation
% 22.19/3.91 % (1872126)Time elapsed: 0.088 s
% 22.19/3.91 % (1872126)Peak memory usage: 89 MB
% 22.19/3.91 % (1872126)Instructions burned: 143 (million)
% 22.19/3.91 % (1872128)Instruction limit reached!
% 22.19/3.91 % (1872128)------------------------------
% 22.19/3.91 % (1872128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872128)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872128)Termination reason: Instruction limit
% 22.19/3.91 % (1872128)Termination phase: Saturation
% 22.19/3.91 % (1872128)Time elapsed: 0.094 s
% 22.19/3.91 % (1872128)Peak memory usage: 91 MB
% 22.19/3.91 % (1872128)Instructions burned: 221 (million)
% 22.19/3.91 % (1872131)lrs+10_64_to=lpo:sil=8000:random_seed=751609429:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 22.19/3.91 % (1872133)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1965916743:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 22.19/3.91 % (1872134)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3599626781:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 22.19/3.91 % (1872131)Instruction limit reached!
% 22.19/3.91 % (1872131)------------------------------
% 22.19/3.91 % (1872131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872131)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872131)Termination reason: Instruction limit
% 22.19/3.91 % (1872131)Termination phase: Saturation
% 22.19/3.91 % (1872131)Time elapsed: 0.063 s
% 22.19/3.91 % (1872131)Peak memory usage: 98 MB
% 22.19/3.91 % (1872131)Instructions burned: 127 (million)
% 22.19/3.91 % (1872135)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1668786287:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 22.19/3.91 % (1872134)Instruction limit reached!
% 22.19/3.91 % (1872134)------------------------------
% 22.19/3.91 % (1872134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872134)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872134)Termination reason: Instruction limit
% 22.19/3.91 % (1872134)Termination phase: Saturation
% 22.19/3.91 % (1872134)Time elapsed: 0.101 s
% 22.19/3.91 % (1872134)Peak memory usage: 91 MB
% 22.19/3.91 % (1872134)Instructions burned: 158 (million)
% 22.19/3.91 % (1872133)Instruction limit reached!
% 22.19/3.91 % (1872133)------------------------------
% 22.19/3.91 % (1872133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.91 % (1872133)CaDiCaL version: 2.1.3
% 22.19/3.91 % (1872133)Termination reason: Instruction limit
% 22.19/3.91 % (1872133)Termination phase: Saturation
% 22.19/3.91 % (1872133)Time elapsed: 0.109 s
% 22.19/3.91 % (1872133)Peak memory usage: 89 MB
% 22.19/3.91 % (1872133)Instructions burned: 195 (million)
% 22.19/3.91 % (1872139)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3432227953:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 22.19/3.91 % (1872139)Instruction limit reached!
% 22.19/3.91 % (1872139)------------------------------
% 22.19/3.91 % (1872139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.19/3.91 % (1872139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872139)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872139)Termination reason: Instruction limit
% 35.40/5.72 % (1872139)Termination phase: Saturation
% 35.40/5.72 % (1872139)Time elapsed: 0.037 s
% 35.40/5.72 % (1872139)Peak memory usage: 89 MB
% 35.40/5.72 % (1872139)Instructions burned: 110 (million)
% 35.40/5.72 % (1872141)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2988072454:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 35.40/5.72 % (1872142)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=376049154:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 35.40/5.72 % (1872141)Instruction limit reached!
% 35.40/5.72 % (1872141)------------------------------
% 35.40/5.72 % (1872141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.40/5.72 % (1872141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872141)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872141)Termination reason: Instruction limit
% 35.40/5.72 % (1872141)Termination phase: Saturation
% 35.40/5.72 % (1872141)Time elapsed: 0.062 s
% 35.40/5.72 % (1872141)Peak memory usage: 89 MB
% 35.40/5.72 % (1872141)Instructions burned: 107 (million)
% 35.40/5.72 % (1872144)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=683295150:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 35.40/5.72 % (1872142)Instruction limit reached!
% 35.40/5.72 % (1872142)------------------------------
% 35.40/5.72 % (1872142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.40/5.72 % (1872142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872142)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872142)Termination reason: Instruction limit
% 35.40/5.72 % (1872142)Termination phase: Saturation
% 35.40/5.72 % (1872142)Time elapsed: 0.131 s
% 35.40/5.72 % (1872142)Peak memory usage: 90 MB
% 35.40/5.72 % (1872142)Instructions burned: 243 (million)
% 35.40/5.72 % (1872147)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1534624876:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 35.40/5.72 % (1872147)Instruction limit reached!
% 35.40/5.72 % (1872147)------------------------------
% 35.40/5.72 % (1872147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.40/5.72 % (1872147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872147)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872147)Termination reason: Instruction limit
% 35.40/5.72 % (1872147)Termination phase: Saturation
% 35.40/5.72 % (1872147)Time elapsed: 0.076 s
% 35.40/5.72 % (1872147)Peak memory usage: 89 MB
% 35.40/5.72 % (1872147)Instructions burned: 134 (million)
% 35.40/5.72 % (1872149)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1677791186:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 35.40/5.72 % (1872151)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1944085572:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 35.40/5.72 % (1872149)Instruction limit reached!
% 35.40/5.72 % (1872149)------------------------------
% 35.40/5.72 % (1872149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.40/5.72 % (1872149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872149)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872149)Termination reason: Instruction limit
% 35.40/5.72 % (1872149)Termination phase: Saturation
% 35.40/5.72 % (1872149)Time elapsed: 0.227 s
% 35.40/5.72 % (1872149)Peak memory usage: 98 MB
% 35.40/5.72 % (1872149)Instructions burned: 500 (million)
% 35.40/5.72 % (1872151)Instruction limit reached!
% 35.40/5.72 % (1872151)------------------------------
% 35.40/5.72 % (1872151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.40/5.72 % (1872151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.40/5.72 % (1872151)CaDiCaL version: 2.1.3
% 35.40/5.72 % (1872151)Termination reason: Instruction limit
% 35.40/5.72 % (1872151)Termination phase: Saturation
% 35.40/5.72 % (1872151)Time elapsed: 0.109 s
% 35.40/5.72 % (1872151)Peak memory usage: 89 MB
% 35.40/5.72 % (1872151)Instructions burned: 193 (million)
% 35.40/5.72 % (1872154)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1724120264:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 39.53/6.74 % (1872155)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3673209035:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 39.53/6.74 % (1872155)Instruction limit reached!
% 39.53/6.74 % (1872155)------------------------------
% 39.53/6.74 % (1872155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872155)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872155)Termination reason: Instruction limit
% 39.53/6.74 % (1872155)Termination phase: Saturation
% 39.53/6.74 % (1872155)Time elapsed: 0.090 s
% 39.53/6.74 % (1872155)Peak memory usage: 90 MB
% 39.53/6.74 % (1872155)Instructions burned: 156 (million)
% 39.53/6.74 % (1872154)Instruction limit reached!
% 39.53/6.74 % (1872154)------------------------------
% 39.53/6.74 % (1872154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872154)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872154)Termination reason: Instruction limit
% 39.53/6.74 % (1872154)Termination phase: Saturation
% 39.53/6.74 % (1872154)Time elapsed: 0.135 s
% 39.53/6.74 % (1872154)Peak memory usage: 90 MB
% 39.53/6.74 % (1872154)Instructions burned: 264 (million)
% 39.53/6.74 % (1872158)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2266747661:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 39.53/6.74 % (1872159)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1962870862:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 39.53/6.74 % (1872159)Instruction limit reached!
% 39.53/6.74 % (1872159)------------------------------
% 39.53/6.74 % (1872159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872159)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872159)Termination reason: Instruction limit
% 39.53/6.74 % (1872159)Termination phase: Saturation
% 39.53/6.74 % (1872159)Time elapsed: 0.280 s
% 39.53/6.74 % (1872159)Peak memory usage: 91 MB
% 39.53/6.74 % (1872159)Instructions burned: 538 (million)
% 39.53/6.74 % (1872162)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3004295202:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 39.53/6.74 % (1872162)Instruction limit reached!
% 39.53/6.74 % (1872162)------------------------------
% 39.53/6.74 % (1872162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872162)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872162)Termination reason: Instruction limit
% 39.53/6.74 % (1872162)Termination phase: Saturation
% 39.53/6.74 % (1872162)Time elapsed: 0.081 s
% 39.53/6.74 % (1872162)Peak memory usage: 97 MB
% 39.53/6.74 % (1872162)Instructions burned: 182 (million)
% 39.53/6.74 % (1872164)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4220421469:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 39.53/6.74 % (1872135)Instruction limit reached!
% 39.53/6.74 % (1872135)------------------------------
% 39.53/6.74 % (1872135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872135)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872135)Termination reason: Instruction limit
% 39.53/6.74 % (1872135)Termination phase: Saturation
% 39.53/6.74 % (1872135)Time elapsed: 2.204 s
% 39.53/6.74 % (1872135)Peak memory usage: 151 MB
% 39.53/6.74 % (1872135)Instructions burned: 3394 (million)
% 39.53/6.74 % (1872166)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1651532791:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 39.53/6.74 % (1872166)Instruction limit reached!
% 39.53/6.74 % (1872166)------------------------------
% 39.53/6.74 % (1872166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872166)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872166)Termination reason: Instruction limit
% 39.53/6.74 % (1872166)Termination phase: Saturation
% 39.53/6.74 % (1872166)Time elapsed: 0.175 s
% 39.53/6.74 % (1872166)Peak memory usage: 91 MB
% 39.53/6.74 % (1872166)Instructions burned: 413 (million)
% 39.53/6.74 % (1872168)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1176718900:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 39.53/6.74 % (1872144)Instruction limit reached!
% 39.53/6.74 % (1872144)------------------------------
% 39.53/6.74 % (1872144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872144)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872144)Termination reason: Instruction limit
% 39.53/6.74 % (1872144)Termination phase: Saturation
% 39.53/6.74 % (1872144)Time elapsed: 2.984 s
% 39.53/6.74 % (1872144)Peak memory usage: 147 MB
% 39.53/6.74 % (1872144)Instructions burned: 5210 (million)
% 39.53/6.74 % (1872158)Instruction limit reached!
% 39.53/6.74 % (1872158)------------------------------
% 39.53/6.74 % (1872158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872158)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872158)Termination reason: Instruction limit
% 39.53/6.74 % (1872158)Termination phase: Saturation
% 39.53/6.74 % (1872158)Time elapsed: 2.157 s
% 39.53/6.74 % (1872158)Peak memory usage: 148 MB
% 39.53/6.74 % (1872158)Instructions burned: 3257 (million)
% 39.53/6.74 % (1872170)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3399520037:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 39.53/6.74 % (1872170)Refutation not found, incomplete strategy
% 39.53/6.74 % (1872170)------------------------------
% 39.53/6.74 % (1872170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872170)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872170)Termination reason: Refutation not found, incomplete strategy
% 39.53/6.74 % (1872170)Time elapsed: 0.005 s
% 39.53/6.74 % (1872170)Peak memory usage: 88 MB
% 39.53/6.74 % (1872170)Instructions burned: 7 (million)
% 39.53/6.74 % (1872171)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2276727485:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 39.53/6.74 % (1872170)------------------------------
% 39.53/6.74 % (1872170)------------------------------
% 39.53/6.74 % (1872171)Instruction limit reached!
% 39.53/6.74 % (1872171)------------------------------
% 39.53/6.74 % (1872171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872171)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872171)Termination reason: Instruction limit
% 39.53/6.74 % (1872171)Termination phase: Saturation
% 39.53/6.74 % (1872171)Time elapsed: 0.326 s
% 39.53/6.74 % (1872171)Peak memory usage: 97 MB
% 39.53/6.74 % (1872171)Instructions burned: 721 (million)
% 39.53/6.74 % (1872174)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3734218082:i=598:bs=on:bd=preordered:av=off:ss=axioms_2956 on theBenchmark for (2956ds/598Mi)
% 39.53/6.74 % (1872175)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1696491039:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi)
% 39.53/6.74 % (1872174)Instruction limit reached!
% 39.53/6.74 % (1872174)------------------------------
% 39.53/6.74 % (1872174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.53/6.74 % (1872174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.53/6.74 % (1872174)CaDiCaL version: 2.1.3
% 39.53/6.74 % (1872174)Termination reason: Instruction limit
% 39.53/6.74 % (1872174)Termination phase: Saturation
% 39.53/6.74 % (1872174)Time elapsed: 0.338 s
% 39.53/6.74 % (1872174)Peak memory usage: 93 MB
% 39.53/6.74 % (1872174)Instructions burned: 599 (million)
% 39.53/6.74 % (1872178)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3400233231:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi)
% 39.53/6.74 % (1872164)First to succeed.
% 39.53/6.74 % (1872164)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1872107"
% 39.53/6.74 % (1872164)Refutation found. Thanks to Tanya!
% 39.53/6.74 % SZS status Unsatisfiable for theBenchmark
% 39.53/6.74 % SZS output start Proof for theBenchmark
% See solution above
% 43.59/6.94 % (1872164)------------------------------
% 43.59/6.94 % (1872164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.59/6.94 % (1872164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.59/6.94 % (1872164)CaDiCaL version: 2.1.3
% 43.59/6.94 % (1872164)Termination reason: Refutation
% 43.59/6.94 % (1872164)Time elapsed: 3.208 s
% 43.59/6.94 % (1872164)Peak memory usage: 142 MB
% 43.59/6.94 % (1872164)Instructions burned: 5616 (million)
% 43.59/6.94 % (1872164)------------------------------
% 43.59/6.94 % (1872164)------------------------------
% 43.59/6.94 % (1872107)Success in time 6.079 s
% 43.59/6.94 % Vampire exiting
%------------------------------------------------------------------------------