%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV543-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 SAT
% Computer : n017.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:25:15 PM UTC 2026
% Result : Unsatisfiable 9.21s 1.84s
% Output : Refutation 9.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 80
% Syntax : Number of formulae : 212 ( 131 unt; 1 def)
% Number of atoms : 293 ( 204 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 163 ( 82 ~; 80 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 2 prp; 0-2 aty)
% Number of functors : 89 ( 89 usr; 87 con; 0-3 aty)
% Number of variables : 13 ( 0 sgn 13 !; 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,
! [X2,X0,X1] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f5,axiom,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f6,axiom,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f23,axiom,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f24,axiom,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f25,axiom,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f26,axiom,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f27,axiom,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f28,axiom,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f29,axiom,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f30,axiom,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f31,axiom,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f32,axiom,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f33,axiom,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f34,axiom,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f35,axiom,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f36,axiom,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f37,axiom,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f38,axiom,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f39,axiom,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f40,axiom,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f41,axiom,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f42,axiom,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f43,axiom,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f44,axiom,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f45,axiom,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f47,axiom,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f48,axiom,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f49,axiom,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f50,axiom,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f51,axiom,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f52,axiom,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f53,axiom,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f54,axiom,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
fof(f55,axiom,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f56,axiom,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
fof(f57,axiom,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).
fof(f58,axiom,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
fof(f59,axiom,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp55) ).
fof(f60,axiom,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
fof(f61,axiom,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).
fof(f62,axiom,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
fof(f63,axiom,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).
fof(f64,axiom,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).
fof(f65,axiom,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).
fof(f66,axiom,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).
fof(f67,axiom,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).
fof(f68,axiom,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).
fof(f69,axiom,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
fof(f70,axiom,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).
fof(f71,axiom,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
fof(f72,axiom,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp68) ).
fof(f73,axiom,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
fof(f74,axiom,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).
fof(f75,axiom,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp71) ).
fof(f76,axiom,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f77,axiom,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp73) ).
fof(f78,axiom,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp74) ).
fof(f79,axiom,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).
fof(f80,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f85,plain,
e_1250 = select(a_1251,i8),
inference(superposition,[],[f1,f7]) ).
fof(f102,plain,
e_1244 = select(a_1284,i8),
inference(superposition,[],[f1,f25]) ).
fof(f104,plain,
e_1287 = select(a_1288,i8),
inference(superposition,[],[f1,f27]) ).
fof(f164,plain,
! [X0] : store(store(a1,i7,select(a1,X0)),X0,e_1244) = store(store(a1,X0,e_1244),i7,select(a1,X0)),
inference(superposition,[],[f3,f44]) ).
fof(f169,plain,
! [X0] : store(store(a_1251,i5,select(a_1251,X0)),X0,e_1252) = store(store(a_1251,X0,e_1252),i5,select(a_1251,X0)),
inference(superposition,[],[f3,f48]) ).
fof(f175,plain,
! [X0] : store(store(a_1263,i5,select(a_1263,X0)),X0,e_1264) = store(store(a_1263,X0,e_1264),i5,select(a_1263,X0)),
inference(superposition,[],[f3,f54]) ).
fof(f190,plain,
! [X0] : store(store(a_1296,i7,select(a_1296,X0)),X0,e_1297) = store(store(a_1296,X0,e_1297),i7,select(a_1296,X0)),
inference(superposition,[],[f3,f69]) ).
fof(f192,plain,
! [X0] : store(store(a_1300,i5,select(a_1300,X0)),X0,e_1301) = store(store(a_1300,X0,e_1301),i5,select(a_1300,X0)),
inference(superposition,[],[f3,f71]) ).
fof(f195,plain,
! [X0] : store(store(a_1307,i1,select(a_1307,X0)),X0,e_1308) = store(store(a_1307,X0,e_1308),i1,select(a_1307,X0)),
inference(superposition,[],[f3,f74]) ).
fof(f200,plain,
! [X0] : store(store(a_1315,i5,select(a_1315,X0)),X0,e_1318) = store(store(a_1315,X0,e_1318),i5,select(a_1315,X0)),
inference(superposition,[],[f3,f79]) ).
fof(f249,plain,
e_1250 = e_1254,
inference(superposition,[],[f85,f49]) ).
fof(f255,plain,
a_1255 = store(a_1253,i5,e_1250),
inference(superposition,[],[f9,f249]) ).
fof(f285,plain,
e_1244 = e_1285,
inference(superposition,[],[f102,f63]) ).
fof(f291,plain,
e_1287 = e_1289,
inference(superposition,[],[f104,f65]) ).
fof(f295,plain,
a_1290 = store(a_1288,i5,e_1287),
inference(superposition,[],[f28,f291]) ).
fof(f356,definition,
( spl0_2
<=> e_1244 = select(a_1247,i8) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f357,plain,
( e_1244 != select(a_1247,i8)
| spl0_2 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( e_1244 = select(a_1247,i8)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f366,plain,
( e_1244 = e_1248
| ~ spl0_2 ),
inference(superposition,[],[f358,f46]) ).
fof(f372,plain,
( a_1249 = store(a_1247,i6,e_1244)
| ~ spl0_2 ),
inference(superposition,[],[f6,f366]) ).
fof(f961,plain,
store(store(a1,i7,e_1246),i8,e_1244) = store(store(a1,i8,e_1244),i7,e_1246),
inference(superposition,[],[f164,f45]) ).
fof(f966,plain,
store(a_1245,i7,e_1246) = store(store(a1,i7,e_1246),i8,e_1244),
inference(forward_demodulation,[],[f961,f4]) ).
fof(f1078,plain,
store(store(a_1263,i5,e_1266),i4,e_1264) = store(store(a_1263,i4,e_1264),i5,e_1266),
inference(superposition,[],[f175,f55]) ).
fof(f1082,plain,
store(a_1265,i5,e_1266) = store(store(a_1263,i5,e_1266),i4,e_1264),
inference(forward_demodulation,[],[f1078,f14]) ).
fof(f1083,plain,
a_1267 = store(store(a_1263,i5,e_1266),i4,e_1264),
inference(forward_demodulation,[],[f1082,f15]) ).
fof(f1198,plain,
store(store(a_1296,i7,e_1299),i1,e_1297) = store(store(a_1296,i1,e_1297),i7,e_1299),
inference(superposition,[],[f190,f70]) ).
fof(f1203,plain,
store(a_1298,i7,e_1299) = store(store(a_1296,i7,e_1299),i1,e_1297),
inference(forward_demodulation,[],[f1198,f32]) ).
fof(f1205,plain,
a_1300 = store(store(a_1296,i7,e_1299),i1,e_1297),
inference(forward_demodulation,[],[f1203,f33]) ).
fof(f1221,plain,
store(store(a_1300,i5,e_1303),i4,e_1301) = store(store(a_1300,i4,e_1301),i5,e_1303),
inference(superposition,[],[f192,f72]) ).
fof(f1225,plain,
store(a_1302,i5,e_1303) = store(store(a_1300,i5,e_1303),i4,e_1301),
inference(forward_demodulation,[],[f1221,f34]) ).
fof(f1226,plain,
a_1304 = store(store(a_1300,i5,e_1303),i4,e_1301),
inference(forward_demodulation,[],[f1225,f35]) ).
fof(f1245,plain,
store(store(a_1307,i1,e_1310),i2,e_1308) = store(store(a_1307,i2,e_1308),i1,e_1310),
inference(superposition,[],[f195,f75]) ).
fof(f1249,plain,
store(a_1309,i1,e_1310) = store(store(a_1307,i1,e_1310),i2,e_1308),
inference(forward_demodulation,[],[f1245,f38]) ).
fof(f1250,plain,
a_1311 = store(store(a_1307,i1,e_1310),i2,e_1308),
inference(forward_demodulation,[],[f1249,f39]) ).
fof(f1289,plain,
store(store(a_1315,i5,e_1316),i9,e_1318) = store(store(a_1315,i9,e_1318),i5,e_1316),
inference(superposition,[],[f200,f78]) ).
fof(f3224,plain,
store(a_1245,i7,e_1246) = store(a_1283,i8,e_1244),
inference(forward_demodulation,[],[f966,f24]) ).
fof(f3319,plain,
store(a_1245,i7,e_1246) = a_1284,
inference(forward_demodulation,[],[f3224,f25]) ).
fof(f3350,plain,
a_1247 = a_1284,
inference(forward_demodulation,[],[f3319,f5]) ).
fof(f3379,plain,
a_1286 = store(a_1247,i6,e_1285),
inference(superposition,[],[f26,f3350]) ).
fof(f3380,plain,
e_1285 = select(a_1247,i8),
inference(superposition,[],[f63,f3350]) ).
fof(f3381,plain,
e_1287 = select(a_1247,i6),
inference(superposition,[],[f64,f3350]) ).
fof(f3385,plain,
e_1250 = e_1287,
inference(forward_demodulation,[],[f3381,f47]) ).
fof(f3386,plain,
e_1248 = e_1285,
inference(forward_demodulation,[],[f3380,f46]) ).
fof(f3387,plain,
a_1286 = store(a_1247,i6,e_1244),
inference(forward_demodulation,[],[f3379,f285]) ).
fof(f3388,plain,
e_1244 = e_1248,
inference(forward_demodulation,[],[f3386,f285]) ).
fof(f3389,plain,
( a_1249 = a_1286
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3387,f372]) ).
fof(f3435,plain,
a_1290 = store(a_1288,i5,e_1250),
inference(superposition,[],[f295,f3385]) ).
fof(f3437,plain,
store(store(a_1251,i5,e_1250),i8,e_1252) = store(store(a_1251,i8,e_1252),i5,e_1250),
inference(superposition,[],[f169,f85]) ).
fof(f3444,plain,
store(a_1253,i5,e_1250) = store(store(a_1251,i5,e_1250),i8,e_1252),
inference(forward_demodulation,[],[f3437,f8]) ).
fof(f3446,plain,
a_1255 = store(store(a_1251,i5,e_1250),i8,e_1252),
inference(forward_demodulation,[],[f3444,f255]) ).
fof(f3451,plain,
( a_1288 = store(a_1249,i8,e_1287)
| ~ spl0_2 ),
inference(superposition,[],[f27,f3389]) ).
fof(f3452,plain,
( store(a_1249,i8,e_1250) = a_1288
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3451,f3385]) ).
fof(f3454,plain,
( a_1251 = a_1288
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3452,f7]) ).
fof(f3474,plain,
( e_1291 = select(a_1251,i5)
| ~ spl0_2 ),
inference(superposition,[],[f66,f3454]) ).
fof(f3480,plain,
( e_1252 = e_1291
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3474,f48]) ).
fof(f3691,plain,
( e_1244 != e_1248
| spl0_2 ),
inference(superposition,[],[f357,f46]) ).
fof(f3692,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f3691,f3388]) ).
fof(f3693,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f3692]) ).
fof(f3747,plain,
( a_1292 = store(a_1290,i8,e_1252)
| ~ spl0_2 ),
inference(superposition,[],[f29,f3480]) ).
fof(f8555,plain,
( a_1290 = store(a_1251,i5,e_1250)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3435,f3454]) ).
fof(f9903,plain,
( a_1255 = store(a_1290,i8,e_1252)
| ~ spl0_2 ),
inference(superposition,[],[f3446,f8555]) ).
fof(f9970,plain,
( a_1255 = a_1292
| ~ spl0_2 ),
inference(superposition,[],[f9903,f3747]) ).
fof(f9979,plain,
( e_1293 = select(a_1255,i9)
| ~ spl0_2 ),
inference(superposition,[],[f67,f9970]) ).
fof(f9980,plain,
( e_1295 = select(a_1255,i4)
| ~ spl0_2 ),
inference(superposition,[],[f68,f9970]) ).
fof(f9996,plain,
( e_1258 = e_1295
| ~ spl0_2 ),
inference(forward_demodulation,[],[f9980,f51]) ).
fof(f9997,plain,
( e_1256 = e_1293
| ~ spl0_2 ),
inference(forward_demodulation,[],[f9979,f50]) ).
fof(f17302,plain,
store(a_1317,i9,e_1318) = store(store(a_1315,i9,e_1318),i5,e_1316),
inference(forward_demodulation,[],[f1289,f42]) ).
fof(f17319,plain,
a_1319 = store(store(a_1315,i9,e_1318),i5,e_1316),
inference(forward_demodulation,[],[f17302,f43]) ).
fof(f17359,plain,
( a_1294 = store(a_1292,i4,e_1256)
| ~ spl0_2 ),
inference(superposition,[],[f30,f9997]) ).
fof(f17360,plain,
( store(a_1255,i4,e_1256) = a_1294
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17359,f9970]) ).
fof(f17361,plain,
( a_1257 = a_1294
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17360,f10]) ).
fof(f17372,plain,
( a_1296 = store(a_1257,i9,e_1295)
| ~ spl0_2 ),
inference(superposition,[],[f31,f17361]) ).
fof(f17378,plain,
( store(a_1257,i9,e_1258) = a_1296
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17372,f9996]) ).
fof(f17379,plain,
( a_1259 = a_1296
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17378,f11]) ).
fof(f17381,plain,
( e_1297 = select(a_1259,i7)
| ~ spl0_2 ),
inference(superposition,[],[f69,f17379]) ).
fof(f17382,plain,
( e_1299 = select(a_1259,i1)
| ~ spl0_2 ),
inference(superposition,[],[f70,f17379]) ).
fof(f17389,plain,
( e_1260 = e_1299
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17382,f52]) ).
fof(f17390,plain,
( e_1262 = e_1297
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17381,f53]) ).
fof(f17867,plain,
( a_1300 = store(store(a_1296,i7,e_1299),i1,e_1262)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1205,f17390]) ).
fof(f17882,plain,
( a_1300 = store(store(a_1296,i7,e_1260),i1,e_1262)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17867,f17389]) ).
fof(f17886,plain,
( a_1300 = store(store(a_1259,i7,e_1260),i1,e_1262)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17882,f17379]) ).
fof(f17889,plain,
( store(a_1261,i1,e_1262) = a_1300
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17886,f12]) ).
fof(f17891,plain,
( a_1263 = a_1300
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17889,f13]) ).
fof(f17894,plain,
( e_1301 = select(a_1263,i5)
| ~ spl0_2 ),
inference(superposition,[],[f71,f17891]) ).
fof(f17895,plain,
( e_1303 = select(a_1263,i4)
| ~ spl0_2 ),
inference(superposition,[],[f72,f17891]) ).
fof(f17903,plain,
( e_1266 = e_1303
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17895,f55]) ).
fof(f17904,plain,
( e_1264 = e_1301
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17894,f54]) ).
fof(f17928,plain,
( a_1304 = store(store(a_1300,i5,e_1303),i4,e_1264)
| ~ spl0_2 ),
inference(superposition,[],[f1226,f17904]) ).
fof(f17930,plain,
( a_1304 = store(store(a_1300,i5,e_1266),i4,e_1264)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17928,f17903]) ).
fof(f17934,plain,
( a_1304 = store(store(a_1263,i5,e_1266),i4,e_1264)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17930,f17891]) ).
fof(f17936,plain,
( a_1267 = a_1304
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17934,f1083]) ).
fof(f17950,plain,
( e_1305 = select(a_1267,i0)
| ~ spl0_2 ),
inference(superposition,[],[f73,f17936]) ).
fof(f17964,plain,
( e_1268 = e_1305
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17950,f56]) ).
fof(f17969,plain,
( a_1306 = store(a_1304,i0,e_1268)
| ~ spl0_2 ),
inference(superposition,[],[f36,f17964]) ).
fof(f17979,plain,
( store(a_1267,i0,e_1268) = a_1306
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17969,f17936]) ).
fof(f17980,plain,
( a_1269 = a_1306
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17979,f16]) ).
fof(f17985,plain,
( a_1307 = store(a_1269,i0,e_1305)
| ~ spl0_2 ),
inference(superposition,[],[f37,f17980]) ).
fof(f17995,plain,
( store(a_1269,i0,e_1268) = a_1307
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17985,f17964]) ).
fof(f17996,plain,
( a_1270 = a_1307
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17995,f17]) ).
fof(f17998,plain,
( e_1308 = select(a_1270,i1)
| ~ spl0_2 ),
inference(superposition,[],[f74,f17996]) ).
fof(f17999,plain,
( e_1310 = select(a_1270,i2)
| ~ spl0_2 ),
inference(superposition,[],[f75,f17996]) ).
fof(f18011,plain,
( e_1271 = e_1310
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17999,f57]) ).
fof(f18012,plain,
( e_1273 = e_1308
| ~ spl0_2 ),
inference(forward_demodulation,[],[f17998,f58]) ).
fof(f18234,plain,
( a_1311 = store(store(a_1307,i1,e_1271),i2,e_1308)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1250,f18011]) ).
fof(f18259,plain,
( a_1311 = store(store(a_1270,i1,e_1271),i2,e_1308)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18234,f17996]) ).
fof(f18266,plain,
( a_1311 = store(a_1272,i2,e_1308)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18259,f18]) ).
fof(f18275,plain,
( store(a_1272,i2,e_1273) = a_1311
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18266,f18012]) ).
fof(f18276,plain,
( a_1274 = a_1311
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18275,f19]) ).
fof(f18278,plain,
( e_1312 = select(a_1274,i0)
| ~ spl0_2 ),
inference(superposition,[],[f76,f18276]) ).
fof(f18279,plain,
( e_1314 = select(a_1274,i3)
| ~ spl0_2 ),
inference(superposition,[],[f77,f18276]) ).
fof(f18285,plain,
( e_1277 = e_1314
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18279,f60]) ).
fof(f18286,plain,
( e_1275 = e_1312
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18278,f59]) ).
fof(f18370,plain,
( a_1313 = store(a_1311,i3,e_1275)
| ~ spl0_2 ),
inference(superposition,[],[f40,f18286]) ).
fof(f18371,plain,
( store(a_1274,i3,e_1275) = a_1313
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18370,f18276]) ).
fof(f18374,plain,
( a_1276 = a_1313
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18371,f20]) ).
fof(f18380,plain,
( a_1315 = store(a_1276,i0,e_1314)
| ~ spl0_2 ),
inference(superposition,[],[f41,f18374]) ).
fof(f18388,plain,
( store(a_1276,i0,e_1277) = a_1315
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18380,f18285]) ).
fof(f18389,plain,
( a_1278 = a_1315
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18388,f21]) ).
fof(f18391,plain,
( e_1316 = select(a_1278,i9)
| ~ spl0_2 ),
inference(superposition,[],[f78,f18389]) ).
fof(f18392,plain,
( e_1318 = select(a_1278,i5)
| ~ spl0_2 ),
inference(superposition,[],[f79,f18389]) ).
fof(f18404,plain,
( e_1279 = e_1318
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18392,f61]) ).
fof(f18405,plain,
( e_1281 = e_1316
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18391,f62]) ).
fof(f18508,plain,
( a_1319 = store(store(a_1315,i9,e_1318),i5,e_1281)
| ~ spl0_2 ),
inference(superposition,[],[f17319,f18405]) ).
fof(f18509,plain,
( a_1319 = store(store(a_1315,i9,e_1279),i5,e_1281)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18508,f18404]) ).
fof(f18513,plain,
( a_1319 = store(store(a_1278,i9,e_1279),i5,e_1281)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18509,f18389]) ).
fof(f18514,plain,
( store(a_1280,i5,e_1281) = a_1319
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18513,f22]) ).
fof(f18515,plain,
( a_1282 = a_1319
| ~ spl0_2 ),
inference(forward_demodulation,[],[f18514,f23]) ).
fof(f18516,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f18515,f80]) ).
fof(f18517,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f18516]) ).
cnf(s11,plain,
spl0_2,
inference(sat_conversion,[],[f3693]) ).
cnf(s40,plain,
~ spl0_2,
inference(sat_conversion,[],[f18517]) ).
cnf(s41,plain,
$false,
inference(rat,[],[s11,s40]) ).
fof(f18518,plain,
$false,
inference(avatar_sat_refutation,[],[s41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n017.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:35:36 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.21/1.84 % (3492564)Will run a generic schedule for satisfiability detection.
% 9.21/1.84 % (3492571)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2077764682:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.21/1.84 % (3492570)% WARNING: option uhcvi not known.
% 9.21/1.84 % (3492569)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3123448732_2999 on theBenchmark for (2999ds/0Mi)
% 9.21/1.84 % (3492575)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2813867401:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.21/1.84 % (3492572)dis+10_1_sil=32000:sp=arity:random_seed=817899056:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.21/1.84 % (3492573)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4254568847:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.21/1.84 % (3492574)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1372252999:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.21/1.84 % (3492570)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2069348024:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.21/1.84 % TRYING [1]
% 9.21/1.84 % TRYING [2]
% 9.21/1.84 % TRYING [3]
% 9.21/1.84 % TRYING [4]
% 9.21/1.84 % TRYING [5]
% 9.21/1.84 % (3492572)Instruction limit reached!
% 9.21/1.84 % (3492572)------------------------------
% 9.21/1.84 % (3492572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492572)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492572)Termination reason: Instruction limit
% 9.21/1.84 % (3492572)Termination phase: Saturation
% 9.21/1.84 % (3492572)Time elapsed: 0.056 s
% 9.21/1.84 % (3492572)Peak memory usage: 12 MB
% 9.21/1.84 % (3492572)Instructions burned: 103 (million)
% 9.21/1.84 % (3492573)Instruction limit reached!
% 9.21/1.84 % (3492573)------------------------------
% 9.21/1.84 % (3492573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492573)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492573)Termination reason: Instruction limit
% 9.21/1.84 % (3492573)Termination phase: Saturation
% 9.21/1.84 % (3492573)Time elapsed: 0.064 s
% 9.21/1.84 % (3492573)Peak memory usage: 13 MB
% 9.21/1.84 % (3492573)Instructions burned: 117 (million)
% 9.21/1.84 % (3492574)Instruction limit reached!
% 9.21/1.84 % (3492574)------------------------------
% 9.21/1.84 % (3492574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492574)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492574)Termination reason: Instruction limit
% 9.21/1.84 % (3492574)Termination phase: Saturation
% 9.21/1.84 % (3492574)Time elapsed: 0.072 s
% 9.21/1.84 % (3492574)Peak memory usage: 13 MB
% 9.21/1.84 % (3492574)Instructions burned: 131 (million)
% 9.21/1.84 % (3492583)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=643681966:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 9.21/1.84 % TRYING [1]
% 9.21/1.84 % TRYING [2]
% 9.21/1.84 % (3492584)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2145766123:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 9.21/1.84 % TRYING [3]
% 9.21/1.84 % (3492585)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1590932602:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.21/1.84 % (3492575)Instruction limit reached!
% 9.21/1.84 % (3492575)------------------------------
% 9.21/1.84 % (3492575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492575)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492575)Termination reason: Instruction limit
% 9.21/1.84 % (3492575)Termination phase: Saturation
% 9.21/1.84 % (3492575)Time elapsed: 0.101 s
% 9.21/1.84 % (3492575)Peak memory usage: 13 MB
% 9.21/1.84 % (3492575)Instructions burned: 159 (million)
% 9.21/1.84 % TRYING [4]
% 9.21/1.84 % (3492589)ott-21_1_sil=16000:fs=off:random_seed=121949848:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.21/1.84 % TRYING [5]
% 9.21/1.84 % TRYING [6]
% 9.21/1.84 % (3492584)Instruction limit reached!
% 9.21/1.84 % (3492584)------------------------------
% 9.21/1.84 % (3492584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492584)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492584)Termination reason: Instruction limit
% 9.21/1.84 % (3492584)Termination phase: Saturation
% 9.21/1.84 % (3492584)Time elapsed: 0.078 s
% 9.21/1.84 % (3492584)Peak memory usage: 12 MB
% 9.21/1.84 % (3492584)Instructions burned: 131 (million)
% 9.21/1.84 % (3492591)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=383169158:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 9.21/1.84 % (3492589)Instruction limit reached!
% 9.21/1.84 % (3492589)------------------------------
% 9.21/1.84 % (3492589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492589)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492589)Termination reason: Instruction limit
% 9.21/1.84 % (3492589)Termination phase: Saturation
% 9.21/1.84 % (3492589)Time elapsed: 0.088 s
% 9.21/1.84 % (3492589)Peak memory usage: 13 MB
% 9.21/1.84 % (3492589)Instructions burned: 182 (million)
% 9.21/1.84 % (3492593)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=47657565:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 9.21/1.84 % TRYING [1]
% 9.21/1.84 % TRYING [2]
% 9.21/1.84 % TRYING [3]
% 9.21/1.84 % TRYING [4]
% 9.21/1.84 % TRYING [6]
% 9.21/1.84 % (3492583)Instruction limit reached!
% 9.21/1.84 % (3492583)------------------------------
% 9.21/1.84 % (3492583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492583)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492583)Termination reason: Instruction limit
% 9.21/1.84 % (3492583)Termination phase: Finite model building constraint generation
% 9.21/1.84 % (3492583)Time elapsed: 0.315 s
% 9.21/1.84 % (3492583)Peak memory usage: 31 MB
% 9.21/1.84 % (3492583)Instructions burned: 718 (million)
% 9.21/1.84 % (3492595)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4056777495:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 9.21/1.84 % TRYING [7]
% 9.21/1.84 % TRYING [5]
% 9.21/1.84 % (3492591)Instruction limit reached!
% 9.21/1.84 % (3492591)------------------------------
% 9.21/1.84 % (3492591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492591)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492591)Termination reason: Instruction limit
% 9.21/1.84 % (3492591)Termination phase: Saturation
% 9.21/1.84 % (3492591)Time elapsed: 0.259 s
% 9.21/1.84 % (3492591)Peak memory usage: 13 MB
% 9.21/1.84 % (3492591)Instructions burned: 478 (million)
% 9.21/1.84 % (3492597)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2571304539:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 9.21/1.84 % (3492585)Instruction limit reached!
% 9.21/1.84 % (3492585)------------------------------
% 9.21/1.84 % (3492585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492585)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492585)Termination reason: Instruction limit
% 9.21/1.84 % (3492585)Termination phase: Saturation
% 9.21/1.84 % (3492585)Time elapsed: 0.382 s
% 9.21/1.84 % (3492585)Peak memory usage: 18 MB
% 9.21/1.84 % (3492585)Instructions burned: 684 (million)
% 9.21/1.84 % (3492599)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3230264293:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 9.21/1.84 % (3492593)Instruction limit reached!
% 9.21/1.84 % (3492593)------------------------------
% 9.21/1.84 % (3492593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492593)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492593)Termination reason: Instruction limit
% 9.21/1.84 % (3492593)Termination phase: Finite model building SAT solving
% 9.21/1.84 % (3492593)Time elapsed: 0.312 s
% 9.21/1.84 % (3492593)Peak memory usage: 22 MB
% 9.21/1.84 % (3492593)Instructions burned: 867 (million)
% 9.21/1.84 % (3492601)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=624646402:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 9.21/1.84 % TRYING [14]
% 9.21/1.84 % (3492597)Instruction limit reached!
% 9.21/1.84 % (3492597)------------------------------
% 9.21/1.84 % (3492597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492597)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492597)Termination reason: Instruction limit
% 9.21/1.84 % (3492597)Termination phase: Finite model building constraint generation
% 9.21/1.84 % (3492597)Time elapsed: 0.395 s
% 9.21/1.84 % (3492597)Peak memory usage: 99 MB
% 9.21/1.84 % (3492597)Instructions burned: 892 (million)
% 9.21/1.84 % (3492599)Instruction limit reached!
% 9.21/1.84 % (3492599)------------------------------
% 9.21/1.84 % (3492599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492599)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492599)Termination reason: Instruction limit
% 9.21/1.84 % (3492599)Termination phase: Saturation
% 9.21/1.84 % (3492599)Time elapsed: 0.372 s
% 9.21/1.84 % (3492599)Peak memory usage: 22 MB
% 9.21/1.84 % (3492599)Instructions burned: 692 (million)
% 9.21/1.84 % (3492603)fmb+10_1_sil=64000:random_seed=1918854589:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 9.21/1.84 % (3492604)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1346573265:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 9.21/1.84 % TRYING [1]
% 9.21/1.84 % TRYING [2]
% 9.21/1.84 % TRYING [20]
% 9.21/1.84 % TRYING [3]
% 9.21/1.84 % TRYING [4]
% 9.21/1.84 % (3492601)Instruction limit reached!
% 9.21/1.84 % (3492601)------------------------------
% 9.21/1.84 % (3492601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492601)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492601)Termination reason: Instruction limit
% 9.21/1.84 % (3492601)Termination phase: Saturation
% 9.21/1.84 % (3492601)Time elapsed: 0.432 s
% 9.21/1.84 % (3492601)Peak memory usage: 22 MB
% 9.21/1.84 % (3492601)Instructions burned: 881 (million)
% 9.21/1.84 % (3492607)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3319022386:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 9.21/1.84 % TRYING [8]
% 9.21/1.84 % (3492595)Instruction limit reached!
% 9.21/1.84 % (3492595)------------------------------
% 9.21/1.84 % (3492595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492595)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492595)Termination reason: Instruction limit
% 9.21/1.84 % (3492595)Termination phase: Saturation
% 9.21/1.84 % (3492595)Time elapsed: 0.667 s
% 9.21/1.84 % (3492595)Peak memory usage: 27 MB
% 9.21/1.84 % (3492595)Instructions burned: 1180 (million)
% 9.21/1.84 % (3492609)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2642677148:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 9.21/1.84 % TRYING [5]
% 9.21/1.84 % TRYING [8]
% 9.21/1.84 % (3492607)Instruction limit reached!
% 9.21/1.84 % (3492607)------------------------------
% 9.21/1.84 % (3492607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492607)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492607)Termination reason: Instruction limit
% 9.21/1.84 % (3492607)Termination phase: Finite model building constraint generation
% 9.21/1.84 % (3492607)Time elapsed: 0.335 s
% 9.21/1.84 % (3492607)Peak memory usage: 78 MB
% 9.21/1.84 % (3492607)Instructions burned: 922 (million)
% 9.21/1.84 % (3492611)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=367212290:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 9.21/1.84 % (3492609) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3492564-3492609"...
% 9.21/1.84 % (3492609)...printing done.
% 9.21/1.84 % (3492609)Refutation found. Thanks to Tanya!
% 9.21/1.84 % SZS status Unsatisfiable for theBenchmark
% 9.21/1.84 % SZS output start Proof for theBenchmark
% See solution above
% 9.21/1.84 % (3492609)------------------------------
% 9.21/1.84 % (3492609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.21/1.84 % (3492609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.21/1.84 % (3492609)CaDiCaL version: 2.1.3
% 9.21/1.84 % (3492609)Termination reason: Refutation
% 9.21/1.84 % (3492609)Time elapsed: 0.473 s
% 9.21/1.84 % (3492609)Peak memory usage: 19 MB
% 9.21/1.84 % (3492609)Instructions burned: 872 (million)
% 9.21/1.84 % (3492564)Success in time 1.627 s
% 9.21/1.84 % Vampire exiting
%------------------------------------------------------------------------------