%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 : Sun Sep 27 09:08:15 AM UTC 2026
% Result : Unsatisfiable 8.29s 1.60s
% Output : CNFRefutation 8.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 79
% Syntax : Number of formulae : 395 ( 395 unt; 0 def)
% Number of atoms : 395 ( 394 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 89 ( 89 usr; 87 con; 0-3 aty)
% Number of variables : 32 ( 1 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : select(store(VAR_0,VAR_1,VAR_2),VAR_1) = VAR_2,
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
select(store(A,B,C),B) = C,
inference(clausify,[status(thm)],[a1]) ).
fof(a3,axiom,
! [VAR_0,VAR_1,VAR_2] : store(store(VAR_0,VAR_1,select(VAR_0,VAR_2)),VAR_2,select(VAR_0,VAR_1)) = store(store(VAR_0,VAR_2,select(VAR_0,VAR_1)),VAR_1,select(VAR_0,VAR_2)),
file('theBenchmark.p',a3) ).
cnf(c_3,plain,
store(store(A,B,select(A,C)),C,select(A,B)) = store(store(A,C,select(A,B)),B,select(A,C)),
inference(clausify,[status(thm)],[a3]) ).
fof(hyp0,axiom,
a_1245 = store(a1,i8,e_1244),
file('theBenchmark.p',hyp0) ).
cnf(c_4,plain,
a_1245 = store(a1,i8,e_1244),
inference(clausify,[status(thm)],[hyp0]) ).
cnf(c_5,plain,
store(a1,i8,e_1244) = a_1245,
inference(copy,[status(thm)],[c_4]) ).
fof(hyp1,axiom,
a_1247 = store(a_1245,i7,e_1246),
file('theBenchmark.p',hyp1) ).
cnf(c_6,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_7,plain,
store(a_1245,i7,e_1246) = a_1247,
inference(copy,[status(thm)],[c_6]) ).
fof(hyp2,axiom,
a_1249 = store(a_1247,i6,e_1248),
file('theBenchmark.p',hyp2) ).
cnf(c_8,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_9,plain,
store(a_1247,i6,e_1248) = a_1249,
inference(copy,[status(thm)],[c_8]) ).
fof(hyp3,axiom,
a_1251 = store(a_1249,i8,e_1250),
file('theBenchmark.p',hyp3) ).
cnf(c_10,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_11,plain,
store(a_1249,i8,e_1250) = a_1251,
inference(copy,[status(thm)],[c_10]) ).
fof(hyp4,axiom,
a_1253 = store(a_1251,i8,e_1252),
file('theBenchmark.p',hyp4) ).
cnf(c_12,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_13,plain,
store(a_1251,i8,e_1252) = a_1253,
inference(copy,[status(thm)],[c_12]) ).
fof(hyp5,axiom,
a_1255 = store(a_1253,i5,e_1254),
file('theBenchmark.p',hyp5) ).
cnf(c_14,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_15,plain,
store(a_1253,i5,e_1254) = a_1255,
inference(copy,[status(thm)],[c_14]) ).
fof(hyp6,axiom,
a_1257 = store(a_1255,i4,e_1256),
file('theBenchmark.p',hyp6) ).
cnf(c_16,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_17,plain,
store(a_1255,i4,e_1256) = a_1257,
inference(copy,[status(thm)],[c_16]) ).
fof(hyp7,axiom,
a_1259 = store(a_1257,i9,e_1258),
file('theBenchmark.p',hyp7) ).
cnf(c_18,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_19,plain,
store(a_1257,i9,e_1258) = a_1259,
inference(copy,[status(thm)],[c_18]) ).
fof(hyp8,axiom,
a_1261 = store(a_1259,i7,e_1260),
file('theBenchmark.p',hyp8) ).
cnf(c_20,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_21,plain,
store(a_1259,i7,e_1260) = a_1261,
inference(copy,[status(thm)],[c_20]) ).
fof(hyp9,axiom,
a_1263 = store(a_1261,i1,e_1262),
file('theBenchmark.p',hyp9) ).
cnf(c_22,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_23,plain,
store(a_1261,i1,e_1262) = a_1263,
inference(copy,[status(thm)],[c_22]) ).
fof(hyp10,axiom,
a_1265 = store(a_1263,i4,e_1264),
file('theBenchmark.p',hyp10) ).
cnf(c_24,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_25,plain,
store(a_1263,i4,e_1264) = a_1265,
inference(copy,[status(thm)],[c_24]) ).
fof(hyp11,axiom,
a_1267 = store(a_1265,i5,e_1266),
file('theBenchmark.p',hyp11) ).
cnf(c_26,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_27,plain,
store(a_1265,i5,e_1266) = a_1267,
inference(copy,[status(thm)],[c_26]) ).
fof(hyp12,axiom,
a_1269 = store(a_1267,i0,e_1268),
file('theBenchmark.p',hyp12) ).
cnf(c_28,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_29,plain,
store(a_1267,i0,e_1268) = a_1269,
inference(copy,[status(thm)],[c_28]) ).
fof(hyp13,axiom,
a_1270 = store(a_1269,i0,e_1268),
file('theBenchmark.p',hyp13) ).
cnf(c_30,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_31,plain,
store(a_1269,i0,e_1268) = a_1270,
inference(copy,[status(thm)],[c_30]) ).
fof(hyp14,axiom,
a_1272 = store(a_1270,i1,e_1271),
file('theBenchmark.p',hyp14) ).
cnf(c_32,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_33,plain,
store(a_1270,i1,e_1271) = a_1272,
inference(copy,[status(thm)],[c_32]) ).
fof(hyp15,axiom,
a_1274 = store(a_1272,i2,e_1273),
file('theBenchmark.p',hyp15) ).
cnf(c_34,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_35,plain,
store(a_1272,i2,e_1273) = a_1274,
inference(copy,[status(thm)],[c_34]) ).
fof(hyp16,axiom,
a_1276 = store(a_1274,i3,e_1275),
file('theBenchmark.p',hyp16) ).
cnf(c_36,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_37,plain,
store(a_1274,i3,e_1275) = a_1276,
inference(copy,[status(thm)],[c_36]) ).
fof(hyp17,axiom,
a_1278 = store(a_1276,i0,e_1277),
file('theBenchmark.p',hyp17) ).
cnf(c_38,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_39,plain,
store(a_1276,i0,e_1277) = a_1278,
inference(copy,[status(thm)],[c_38]) ).
fof(hyp18,axiom,
a_1280 = store(a_1278,i9,e_1279),
file('theBenchmark.p',hyp18) ).
cnf(c_40,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(clausify,[status(thm)],[hyp18]) ).
cnf(c_41,plain,
store(a_1278,i9,e_1279) = a_1280,
inference(copy,[status(thm)],[c_40]) ).
fof(hyp19,axiom,
a_1282 = store(a_1280,i5,e_1281),
file('theBenchmark.p',hyp19) ).
cnf(c_42,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_43,plain,
store(a_1280,i5,e_1281) = a_1282,
inference(copy,[status(thm)],[c_42]) ).
fof(hyp20,axiom,
a_1283 = store(a1,i7,e_1246),
file('theBenchmark.p',hyp20) ).
cnf(c_44,plain,
a_1283 = store(a1,i7,e_1246),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_45,plain,
store(a1,i7,e_1246) = a_1283,
inference(copy,[status(thm)],[c_44]) ).
fof(hyp21,axiom,
a_1284 = store(a_1283,i8,e_1244),
file('theBenchmark.p',hyp21) ).
cnf(c_46,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_47,plain,
store(a_1283,i8,e_1244) = a_1284,
inference(copy,[status(thm)],[c_46]) ).
fof(hyp22,axiom,
a_1286 = store(a_1284,i6,e_1285),
file('theBenchmark.p',hyp22) ).
cnf(c_48,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(clausify,[status(thm)],[hyp22]) ).
cnf(c_49,plain,
store(a_1284,i6,e_1285) = a_1286,
inference(copy,[status(thm)],[c_48]) ).
fof(hyp23,axiom,
a_1288 = store(a_1286,i8,e_1287),
file('theBenchmark.p',hyp23) ).
cnf(c_50,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(clausify,[status(thm)],[hyp23]) ).
cnf(c_51,plain,
store(a_1286,i8,e_1287) = a_1288,
inference(copy,[status(thm)],[c_50]) ).
fof(hyp24,axiom,
a_1290 = store(a_1288,i5,e_1289),
file('theBenchmark.p',hyp24) ).
cnf(c_52,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(clausify,[status(thm)],[hyp24]) ).
cnf(c_53,plain,
store(a_1288,i5,e_1289) = a_1290,
inference(copy,[status(thm)],[c_52]) ).
fof(hyp25,axiom,
a_1292 = store(a_1290,i8,e_1291),
file('theBenchmark.p',hyp25) ).
cnf(c_54,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(clausify,[status(thm)],[hyp25]) ).
cnf(c_55,plain,
store(a_1290,i8,e_1291) = a_1292,
inference(copy,[status(thm)],[c_54]) ).
fof(hyp26,axiom,
a_1294 = store(a_1292,i4,e_1293),
file('theBenchmark.p',hyp26) ).
cnf(c_56,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(clausify,[status(thm)],[hyp26]) ).
cnf(c_57,plain,
store(a_1292,i4,e_1293) = a_1294,
inference(copy,[status(thm)],[c_56]) ).
fof(hyp27,axiom,
a_1296 = store(a_1294,i9,e_1295),
file('theBenchmark.p',hyp27) ).
cnf(c_58,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(clausify,[status(thm)],[hyp27]) ).
cnf(c_59,plain,
store(a_1294,i9,e_1295) = a_1296,
inference(copy,[status(thm)],[c_58]) ).
fof(hyp28,axiom,
a_1298 = store(a_1296,i1,e_1297),
file('theBenchmark.p',hyp28) ).
cnf(c_60,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(clausify,[status(thm)],[hyp28]) ).
cnf(c_61,plain,
store(a_1296,i1,e_1297) = a_1298,
inference(copy,[status(thm)],[c_60]) ).
fof(hyp29,axiom,
a_1300 = store(a_1298,i7,e_1299),
file('theBenchmark.p',hyp29) ).
cnf(c_62,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(clausify,[status(thm)],[hyp29]) ).
cnf(c_63,plain,
store(a_1298,i7,e_1299) = a_1300,
inference(copy,[status(thm)],[c_62]) ).
fof(hyp30,axiom,
a_1302 = store(a_1300,i4,e_1301),
file('theBenchmark.p',hyp30) ).
cnf(c_64,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(clausify,[status(thm)],[hyp30]) ).
cnf(c_65,plain,
store(a_1300,i4,e_1301) = a_1302,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp31,axiom,
a_1304 = store(a_1302,i5,e_1303),
file('theBenchmark.p',hyp31) ).
cnf(c_66,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(clausify,[status(thm)],[hyp31]) ).
cnf(c_67,plain,
store(a_1302,i5,e_1303) = a_1304,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp32,axiom,
a_1306 = store(a_1304,i0,e_1305),
file('theBenchmark.p',hyp32) ).
cnf(c_68,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(clausify,[status(thm)],[hyp32]) ).
cnf(c_69,plain,
store(a_1304,i0,e_1305) = a_1306,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp33,axiom,
a_1307 = store(a_1306,i0,e_1305),
file('theBenchmark.p',hyp33) ).
cnf(c_70,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_71,plain,
store(a_1306,i0,e_1305) = a_1307,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp34,axiom,
a_1309 = store(a_1307,i2,e_1308),
file('theBenchmark.p',hyp34) ).
cnf(c_72,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(clausify,[status(thm)],[hyp34]) ).
cnf(c_73,plain,
store(a_1307,i2,e_1308) = a_1309,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp35,axiom,
a_1311 = store(a_1309,i1,e_1310),
file('theBenchmark.p',hyp35) ).
cnf(c_74,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(clausify,[status(thm)],[hyp35]) ).
cnf(c_75,plain,
store(a_1309,i1,e_1310) = a_1311,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp36,axiom,
a_1313 = store(a_1311,i3,e_1312),
file('theBenchmark.p',hyp36) ).
cnf(c_76,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_77,plain,
store(a_1311,i3,e_1312) = a_1313,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp37,axiom,
a_1315 = store(a_1313,i0,e_1314),
file('theBenchmark.p',hyp37) ).
cnf(c_78,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_79,plain,
store(a_1313,i0,e_1314) = a_1315,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp38,axiom,
a_1317 = store(a_1315,i5,e_1316),
file('theBenchmark.p',hyp38) ).
cnf(c_80,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_81,plain,
store(a_1315,i5,e_1316) = a_1317,
inference(copy,[status(thm)],[c_80]) ).
fof(hyp39,axiom,
a_1319 = store(a_1317,i9,e_1318),
file('theBenchmark.p',hyp39) ).
cnf(c_82,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_83,plain,
store(a_1317,i9,e_1318) = a_1319,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp40,axiom,
e_1244 = select(a1,i7),
file('theBenchmark.p',hyp40) ).
cnf(c_84,plain,
e_1244 = select(a1,i7),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_85,plain,
select(a1,i7) = e_1244,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp41,axiom,
e_1246 = select(a1,i8),
file('theBenchmark.p',hyp41) ).
cnf(c_86,plain,
e_1246 = select(a1,i8),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_87,plain,
select(a1,i8) = e_1246,
inference(copy,[status(thm)],[c_86]) ).
fof(hyp42,axiom,
e_1248 = select(a_1247,i8),
file('theBenchmark.p',hyp42) ).
cnf(c_88,plain,
e_1248 = select(a_1247,i8),
inference(clausify,[status(thm)],[hyp42]) ).
cnf(c_89,plain,
select(a_1247,i8) = e_1248,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp43,axiom,
e_1250 = select(a_1247,i6),
file('theBenchmark.p',hyp43) ).
cnf(c_90,plain,
e_1250 = select(a_1247,i6),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_91,plain,
select(a_1247,i6) = e_1250,
inference(copy,[status(thm)],[c_90]) ).
fof(hyp44,axiom,
e_1252 = select(a_1251,i5),
file('theBenchmark.p',hyp44) ).
cnf(c_92,plain,
e_1252 = select(a_1251,i5),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_93,plain,
select(a_1251,i5) = e_1252,
inference(copy,[status(thm)],[c_92]) ).
fof(hyp45,axiom,
e_1254 = select(a_1251,i8),
file('theBenchmark.p',hyp45) ).
cnf(c_94,plain,
e_1254 = select(a_1251,i8),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_95,plain,
select(a_1251,i8) = e_1254,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp46,axiom,
e_1256 = select(a_1255,i9),
file('theBenchmark.p',hyp46) ).
cnf(c_96,plain,
e_1256 = select(a_1255,i9),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_97,plain,
select(a_1255,i9) = e_1256,
inference(copy,[status(thm)],[c_96]) ).
fof(hyp47,axiom,
e_1258 = select(a_1255,i4),
file('theBenchmark.p',hyp47) ).
cnf(c_98,plain,
e_1258 = select(a_1255,i4),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_99,plain,
select(a_1255,i4) = e_1258,
inference(copy,[status(thm)],[c_98]) ).
fof(hyp48,axiom,
e_1260 = select(a_1259,i1),
file('theBenchmark.p',hyp48) ).
cnf(c_100,plain,
e_1260 = select(a_1259,i1),
inference(clausify,[status(thm)],[hyp48]) ).
cnf(c_101,plain,
select(a_1259,i1) = e_1260,
inference(copy,[status(thm)],[c_100]) ).
fof(hyp49,axiom,
e_1262 = select(a_1259,i7),
file('theBenchmark.p',hyp49) ).
cnf(c_102,plain,
e_1262 = select(a_1259,i7),
inference(clausify,[status(thm)],[hyp49]) ).
cnf(c_103,plain,
select(a_1259,i7) = e_1262,
inference(copy,[status(thm)],[c_102]) ).
fof(hyp50,axiom,
e_1264 = select(a_1263,i5),
file('theBenchmark.p',hyp50) ).
cnf(c_104,plain,
e_1264 = select(a_1263,i5),
inference(clausify,[status(thm)],[hyp50]) ).
cnf(c_105,plain,
select(a_1263,i5) = e_1264,
inference(copy,[status(thm)],[c_104]) ).
fof(hyp51,axiom,
e_1266 = select(a_1263,i4),
file('theBenchmark.p',hyp51) ).
cnf(c_106,plain,
e_1266 = select(a_1263,i4),
inference(clausify,[status(thm)],[hyp51]) ).
cnf(c_107,plain,
select(a_1263,i4) = e_1266,
inference(copy,[status(thm)],[c_106]) ).
fof(hyp52,axiom,
e_1268 = select(a_1267,i0),
file('theBenchmark.p',hyp52) ).
cnf(c_108,plain,
e_1268 = select(a_1267,i0),
inference(clausify,[status(thm)],[hyp52]) ).
cnf(c_109,plain,
select(a_1267,i0) = e_1268,
inference(copy,[status(thm)],[c_108]) ).
fof(hyp53,axiom,
e_1271 = select(a_1270,i2),
file('theBenchmark.p',hyp53) ).
cnf(c_110,plain,
e_1271 = select(a_1270,i2),
inference(clausify,[status(thm)],[hyp53]) ).
cnf(c_111,plain,
select(a_1270,i2) = e_1271,
inference(copy,[status(thm)],[c_110]) ).
fof(hyp54,axiom,
e_1273 = select(a_1270,i1),
file('theBenchmark.p',hyp54) ).
cnf(c_112,plain,
e_1273 = select(a_1270,i1),
inference(clausify,[status(thm)],[hyp54]) ).
cnf(c_113,plain,
select(a_1270,i1) = e_1273,
inference(copy,[status(thm)],[c_112]) ).
fof(hyp55,axiom,
e_1275 = select(a_1274,i0),
file('theBenchmark.p',hyp55) ).
cnf(c_114,plain,
e_1275 = select(a_1274,i0),
inference(clausify,[status(thm)],[hyp55]) ).
cnf(c_115,plain,
select(a_1274,i0) = e_1275,
inference(copy,[status(thm)],[c_114]) ).
fof(hyp56,axiom,
e_1277 = select(a_1274,i3),
file('theBenchmark.p',hyp56) ).
cnf(c_116,plain,
e_1277 = select(a_1274,i3),
inference(clausify,[status(thm)],[hyp56]) ).
cnf(c_117,plain,
select(a_1274,i3) = e_1277,
inference(copy,[status(thm)],[c_116]) ).
fof(hyp57,axiom,
e_1279 = select(a_1278,i5),
file('theBenchmark.p',hyp57) ).
cnf(c_118,plain,
e_1279 = select(a_1278,i5),
inference(clausify,[status(thm)],[hyp57]) ).
cnf(c_119,plain,
select(a_1278,i5) = e_1279,
inference(copy,[status(thm)],[c_118]) ).
fof(hyp58,axiom,
e_1281 = select(a_1278,i9),
file('theBenchmark.p',hyp58) ).
cnf(c_120,plain,
e_1281 = select(a_1278,i9),
inference(clausify,[status(thm)],[hyp58]) ).
cnf(c_121,plain,
select(a_1278,i9) = e_1281,
inference(copy,[status(thm)],[c_120]) ).
fof(hyp59,axiom,
e_1285 = select(a_1284,i8),
file('theBenchmark.p',hyp59) ).
cnf(c_122,plain,
e_1285 = select(a_1284,i8),
inference(clausify,[status(thm)],[hyp59]) ).
cnf(c_123,plain,
select(a_1284,i8) = e_1285,
inference(copy,[status(thm)],[c_122]) ).
fof(hyp60,axiom,
e_1287 = select(a_1284,i6),
file('theBenchmark.p',hyp60) ).
cnf(c_124,plain,
e_1287 = select(a_1284,i6),
inference(clausify,[status(thm)],[hyp60]) ).
cnf(c_125,plain,
select(a_1284,i6) = e_1287,
inference(copy,[status(thm)],[c_124]) ).
fof(hyp61,axiom,
e_1289 = select(a_1288,i8),
file('theBenchmark.p',hyp61) ).
cnf(c_126,plain,
e_1289 = select(a_1288,i8),
inference(clausify,[status(thm)],[hyp61]) ).
cnf(c_127,plain,
select(a_1288,i8) = e_1289,
inference(copy,[status(thm)],[c_126]) ).
fof(hyp62,axiom,
e_1291 = select(a_1288,i5),
file('theBenchmark.p',hyp62) ).
cnf(c_128,plain,
e_1291 = select(a_1288,i5),
inference(clausify,[status(thm)],[hyp62]) ).
cnf(c_129,plain,
select(a_1288,i5) = e_1291,
inference(copy,[status(thm)],[c_128]) ).
fof(hyp63,axiom,
e_1293 = select(a_1292,i9),
file('theBenchmark.p',hyp63) ).
cnf(c_130,plain,
e_1293 = select(a_1292,i9),
inference(clausify,[status(thm)],[hyp63]) ).
cnf(c_131,plain,
select(a_1292,i9) = e_1293,
inference(copy,[status(thm)],[c_130]) ).
fof(hyp64,axiom,
e_1295 = select(a_1292,i4),
file('theBenchmark.p',hyp64) ).
cnf(c_132,plain,
e_1295 = select(a_1292,i4),
inference(clausify,[status(thm)],[hyp64]) ).
cnf(c_133,plain,
select(a_1292,i4) = e_1295,
inference(copy,[status(thm)],[c_132]) ).
fof(hyp65,axiom,
e_1297 = select(a_1296,i7),
file('theBenchmark.p',hyp65) ).
cnf(c_134,plain,
e_1297 = select(a_1296,i7),
inference(clausify,[status(thm)],[hyp65]) ).
cnf(c_135,plain,
select(a_1296,i7) = e_1297,
inference(copy,[status(thm)],[c_134]) ).
fof(hyp66,axiom,
e_1299 = select(a_1296,i1),
file('theBenchmark.p',hyp66) ).
cnf(c_136,plain,
e_1299 = select(a_1296,i1),
inference(clausify,[status(thm)],[hyp66]) ).
cnf(c_137,plain,
select(a_1296,i1) = e_1299,
inference(copy,[status(thm)],[c_136]) ).
fof(hyp67,axiom,
e_1301 = select(a_1300,i5),
file('theBenchmark.p',hyp67) ).
cnf(c_138,plain,
e_1301 = select(a_1300,i5),
inference(clausify,[status(thm)],[hyp67]) ).
cnf(c_139,plain,
select(a_1300,i5) = e_1301,
inference(copy,[status(thm)],[c_138]) ).
fof(hyp68,axiom,
e_1303 = select(a_1300,i4),
file('theBenchmark.p',hyp68) ).
cnf(c_140,plain,
e_1303 = select(a_1300,i4),
inference(clausify,[status(thm)],[hyp68]) ).
cnf(c_141,plain,
select(a_1300,i4) = e_1303,
inference(copy,[status(thm)],[c_140]) ).
fof(hyp69,axiom,
e_1305 = select(a_1304,i0),
file('theBenchmark.p',hyp69) ).
cnf(c_142,plain,
e_1305 = select(a_1304,i0),
inference(clausify,[status(thm)],[hyp69]) ).
cnf(c_143,plain,
select(a_1304,i0) = e_1305,
inference(copy,[status(thm)],[c_142]) ).
fof(hyp70,axiom,
e_1308 = select(a_1307,i1),
file('theBenchmark.p',hyp70) ).
cnf(c_144,plain,
e_1308 = select(a_1307,i1),
inference(clausify,[status(thm)],[hyp70]) ).
cnf(c_145,plain,
select(a_1307,i1) = e_1308,
inference(copy,[status(thm)],[c_144]) ).
fof(hyp71,axiom,
e_1310 = select(a_1307,i2),
file('theBenchmark.p',hyp71) ).
cnf(c_146,plain,
e_1310 = select(a_1307,i2),
inference(clausify,[status(thm)],[hyp71]) ).
cnf(c_147,plain,
select(a_1307,i2) = e_1310,
inference(copy,[status(thm)],[c_146]) ).
fof(hyp72,axiom,
e_1312 = select(a_1311,i0),
file('theBenchmark.p',hyp72) ).
cnf(c_148,plain,
e_1312 = select(a_1311,i0),
inference(clausify,[status(thm)],[hyp72]) ).
cnf(c_149,plain,
select(a_1311,i0) = e_1312,
inference(copy,[status(thm)],[c_148]) ).
fof(hyp73,axiom,
e_1314 = select(a_1311,i3),
file('theBenchmark.p',hyp73) ).
cnf(c_150,plain,
e_1314 = select(a_1311,i3),
inference(clausify,[status(thm)],[hyp73]) ).
cnf(c_151,plain,
select(a_1311,i3) = e_1314,
inference(copy,[status(thm)],[c_150]) ).
fof(hyp74,axiom,
e_1316 = select(a_1315,i9),
file('theBenchmark.p',hyp74) ).
cnf(c_152,plain,
e_1316 = select(a_1315,i9),
inference(clausify,[status(thm)],[hyp74]) ).
cnf(c_153,plain,
select(a_1315,i9) = e_1316,
inference(copy,[status(thm)],[c_152]) ).
fof(hyp75,axiom,
e_1318 = select(a_1315,i5),
file('theBenchmark.p',hyp75) ).
cnf(c_154,plain,
e_1318 = select(a_1315,i5),
inference(clausify,[status(thm)],[hyp75]) ).
cnf(c_155,plain,
select(a_1315,i5) = e_1318,
inference(copy,[status(thm)],[c_154]) ).
fof(goal,axiom,
a_1282 != a_1319,
file('theBenchmark.p',goal) ).
cnf(c_156,plain,
a_1282 != a_1319,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_157,plain,
a_1319 != a_1282,
inference(copy,[status(thm)],[c_156]) ).
cnf(c_158,plain,
select(store(store(A,B,select(A,C)),C,select(A,B)),B) = select(A,C),
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_591,plain,
select(a_1251,i8) = e_1250,
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_163,plain,
e_1254 = e_1250,
inference(paramod,[status(thm)],[c_95,c_591]) ).
cnf(c_164,plain,
select(a_1251,i8) = e_1250,
inference(paramod,[status(thm)],[c_163,c_95]) ).
cnf(c_165,plain,
store(a_1253,i5,e_1250) = a_1255,
inference(paramod,[status(thm)],[c_163,c_15]) ).
cnf(c_592,plain,
select(a_1284,i8) = e_1244,
inference(paramod,[status(thm)],[c_47,c_1]) ).
cnf(c_182,plain,
e_1285 = e_1244,
inference(paramod,[status(thm)],[c_123,c_592]) ).
cnf(c_184,plain,
store(a_1284,i6,e_1244) = a_1286,
inference(paramod,[status(thm)],[c_182,c_49]) ).
cnf(c_593,plain,
select(a_1288,i8) = e_1287,
inference(paramod,[status(thm)],[c_51,c_1]) ).
cnf(c_185,plain,
e_1289 = e_1287,
inference(paramod,[status(thm)],[c_127,c_593]) ).
cnf(c_187,plain,
store(a_1288,i5,e_1287) = a_1290,
inference(paramod,[status(thm)],[c_185,c_53]) ).
cnf(c_594,plain,
store(store(a1,A,e_1244),i7,select(a1,A)) = store(store(a1,i7,select(a1,A)),A,select(a1,i7)),
inference(paramod,[status(thm)],[c_85,c_3]) ).
cnf(c_595,plain,
store(store(a1,A,e_1244),i7,select(a1,A)) = store(store(a1,i7,select(a1,A)),A,e_1244),
inference(paramod,[status(thm)],[c_85,c_594]) ).
cnf(c_203,plain,
store(store(a1,i7,select(a1,A)),A,e_1244) = store(store(a1,A,e_1244),i7,select(a1,A)),
inference(copy,[status(thm)],[c_595]) ).
cnf(c_596,plain,
store(store(a_1251,A,e_1252),i5,select(a_1251,A)) = store(store(a_1251,i5,select(a_1251,A)),A,select(a_1251,i5)),
inference(paramod,[status(thm)],[c_93,c_3]) ).
cnf(c_597,plain,
store(store(a_1251,A,e_1252),i5,select(a_1251,A)) = store(store(a_1251,i5,select(a_1251,A)),A,e_1252),
inference(paramod,[status(thm)],[c_93,c_596]) ).
cnf(c_207,plain,
store(store(a_1251,i5,select(a_1251,A)),A,e_1252) = store(store(a_1251,A,e_1252),i5,select(a_1251,A)),
inference(copy,[status(thm)],[c_597]) ).
cnf(c_598,plain,
store(store(a_1259,A,e_1260),i1,select(a_1259,A)) = store(store(a_1259,i1,select(a_1259,A)),A,select(a_1259,i1)),
inference(paramod,[status(thm)],[c_101,c_3]) ).
cnf(c_599,plain,
store(store(a_1259,A,e_1260),i1,select(a_1259,A)) = store(store(a_1259,i1,select(a_1259,A)),A,e_1260),
inference(paramod,[status(thm)],[c_101,c_598]) ).
cnf(c_210,plain,
store(store(a_1259,i1,select(a_1259,A)),A,e_1260) = store(store(a_1259,A,e_1260),i1,select(a_1259,A)),
inference(copy,[status(thm)],[c_599]) ).
cnf(c_600,plain,
store(store(a_1270,A,e_1271),i2,select(a_1270,A)) = store(store(a_1270,i2,select(a_1270,A)),A,select(a_1270,i2)),
inference(paramod,[status(thm)],[c_111,c_3]) ).
cnf(c_601,plain,
store(store(a_1270,A,e_1271),i2,select(a_1270,A)) = store(store(a_1270,i2,select(a_1270,A)),A,e_1271),
inference(paramod,[status(thm)],[c_111,c_600]) ).
cnf(c_215,plain,
store(store(a_1270,i2,select(a_1270,A)),A,e_1271) = store(store(a_1270,A,e_1271),i2,select(a_1270,A)),
inference(copy,[status(thm)],[c_601]) ).
cnf(c_602,plain,
store(store(a_1278,A,e_1279),i5,select(a_1278,A)) = store(store(a_1278,i5,select(a_1278,A)),A,select(a_1278,i5)),
inference(paramod,[status(thm)],[c_119,c_3]) ).
cnf(c_603,plain,
store(store(a_1278,A,e_1279),i5,select(a_1278,A)) = store(store(a_1278,i5,select(a_1278,A)),A,e_1279),
inference(paramod,[status(thm)],[c_119,c_602]) ).
cnf(c_219,plain,
store(store(a_1278,i5,select(a_1278,A)),A,e_1279) = store(store(a_1278,A,e_1279),i5,select(a_1278,A)),
inference(copy,[status(thm)],[c_603]) ).
cnf(c_604,plain,
select(store(store(a1,A,e_1244),i7,select(a1,A)),A) = select(a1,i7),
inference(paramod,[status(thm)],[c_85,c_158]) ).
cnf(c_238,plain,
select(store(store(a1,A,e_1244),i7,select(a1,A)),A) = e_1244,
inference(paramod,[status(thm)],[c_85,c_604]) ).
cnf(c_605,plain,
select(store(a_1245,i7,select(a1,i8)),i8) = e_1244,
inference(paramod,[status(thm)],[c_5,c_238]) ).
cnf(c_606,plain,
select(store(a_1245,i7,e_1246),i8) = e_1244,
inference(paramod,[status(thm)],[c_87,c_605]) ).
cnf(c_607,plain,
select(a_1247,i8) = e_1244,
inference(paramod,[status(thm)],[c_7,c_606]) ).
cnf(c_361,plain,
e_1248 = e_1244,
inference(paramod,[status(thm)],[c_89,c_607]) ).
cnf(c_370,plain,
store(a_1247,i6,e_1244) = a_1249,
inference(paramod,[status(thm)],[c_361,c_9]) ).
cnf(c_608,plain,
store(store(a1,i7,select(a1,i8)),i8,e_1244) = store(a_1245,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_5,c_203]) ).
cnf(c_609,plain,
store(store(a1,i7,e_1246),i8,e_1244) = store(a_1245,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_87,c_608]) ).
cnf(c_610,plain,
store(a_1283,i8,e_1244) = store(a_1245,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_45,c_609]) ).
cnf(c_611,plain,
a_1284 = store(a_1245,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_47,c_610]) ).
cnf(c_612,plain,
a_1284 = store(a_1245,i7,e_1246),
inference(paramod,[status(thm)],[c_87,c_611]) ).
cnf(c_371,plain,
a_1284 = a_1247,
inference(paramod,[status(thm)],[c_7,c_612]) ).
cnf(c_613,plain,
store(a_1247,i6,e_1244) = a_1286,
inference(paramod,[status(thm)],[c_371,c_184]) ).
cnf(c_614,plain,
a_1249 = a_1286,
inference(paramod,[status(thm)],[c_370,c_613]) ).
cnf(c_374,plain,
a_1286 = a_1249,
inference(copy,[status(thm)],[c_614]) ).
cnf(c_615,plain,
select(a_1247,i6) = e_1287,
inference(paramod,[status(thm)],[c_371,c_125]) ).
cnf(c_616,plain,
e_1250 = e_1287,
inference(paramod,[status(thm)],[c_91,c_615]) ).
cnf(c_375,plain,
e_1287 = e_1250,
inference(copy,[status(thm)],[c_616]) ).
cnf(c_617,plain,
store(a_1249,i8,e_1287) = a_1288,
inference(paramod,[status(thm)],[c_374,c_51]) ).
cnf(c_618,plain,
store(a_1249,i8,e_1250) = a_1288,
inference(paramod,[status(thm)],[c_375,c_617]) ).
cnf(c_619,plain,
a_1251 = a_1288,
inference(paramod,[status(thm)],[c_11,c_618]) ).
cnf(c_377,plain,
a_1288 = a_1251,
inference(copy,[status(thm)],[c_619]) ).
cnf(c_620,plain,
store(a_1251,i5,e_1287) = a_1290,
inference(paramod,[status(thm)],[c_377,c_187]) ).
cnf(c_381,plain,
store(a_1251,i5,e_1250) = a_1290,
inference(paramod,[status(thm)],[c_375,c_620]) ).
cnf(c_621,plain,
select(a_1251,i5) = e_1291,
inference(paramod,[status(thm)],[c_377,c_129]) ).
cnf(c_622,plain,
e_1252 = e_1291,
inference(paramod,[status(thm)],[c_93,c_621]) ).
cnf(c_385,plain,
e_1291 = e_1252,
inference(copy,[status(thm)],[c_622]) ).
cnf(c_389,plain,
store(a_1290,i8,e_1252) = a_1292,
inference(paramod,[status(thm)],[c_385,c_55]) ).
cnf(c_623,plain,
store(store(a_1251,i5,select(a_1251,i8)),i8,e_1252) = store(a_1253,i5,select(a_1251,i8)),
inference(paramod,[status(thm)],[c_13,c_207]) ).
cnf(c_624,plain,
store(store(a_1251,i5,e_1250),i8,e_1252) = store(a_1253,i5,select(a_1251,i8)),
inference(paramod,[status(thm)],[c_164,c_623]) ).
cnf(c_625,plain,
store(a_1290,i8,e_1252) = store(a_1253,i5,select(a_1251,i8)),
inference(paramod,[status(thm)],[c_381,c_624]) ).
cnf(c_626,plain,
a_1292 = store(a_1253,i5,select(a_1251,i8)),
inference(paramod,[status(thm)],[c_389,c_625]) ).
cnf(c_627,plain,
a_1292 = store(a_1253,i5,e_1250),
inference(paramod,[status(thm)],[c_164,c_626]) ).
cnf(c_399,plain,
a_1292 = a_1255,
inference(paramod,[status(thm)],[c_165,c_627]) ).
cnf(c_628,plain,
select(a_1255,i4) = e_1295,
inference(paramod,[status(thm)],[c_399,c_133]) ).
cnf(c_629,plain,
e_1258 = e_1295,
inference(paramod,[status(thm)],[c_99,c_628]) ).
cnf(c_410,plain,
e_1295 = e_1258,
inference(copy,[status(thm)],[c_629]) ).
cnf(c_630,plain,
select(a_1255,i9) = e_1293,
inference(paramod,[status(thm)],[c_399,c_131]) ).
cnf(c_631,plain,
e_1256 = e_1293,
inference(paramod,[status(thm)],[c_97,c_630]) ).
cnf(c_411,plain,
e_1293 = e_1256,
inference(copy,[status(thm)],[c_631]) ).
cnf(c_632,plain,
store(a_1255,i4,e_1293) = a_1294,
inference(paramod,[status(thm)],[c_399,c_57]) ).
cnf(c_633,plain,
store(a_1255,i4,e_1256) = a_1294,
inference(paramod,[status(thm)],[c_411,c_632]) ).
cnf(c_634,plain,
a_1257 = a_1294,
inference(paramod,[status(thm)],[c_17,c_633]) ).
cnf(c_412,plain,
a_1294 = a_1257,
inference(copy,[status(thm)],[c_634]) ).
cnf(c_635,plain,
store(a_1257,i9,e_1295) = a_1296,
inference(paramod,[status(thm)],[c_412,c_59]) ).
cnf(c_636,plain,
store(a_1257,i9,e_1258) = a_1296,
inference(paramod,[status(thm)],[c_410,c_635]) ).
cnf(c_637,plain,
a_1259 = a_1296,
inference(paramod,[status(thm)],[c_19,c_636]) ).
cnf(c_416,plain,
a_1296 = a_1259,
inference(copy,[status(thm)],[c_637]) ).
cnf(c_638,plain,
select(a_1259,i1) = e_1299,
inference(paramod,[status(thm)],[c_416,c_137]) ).
cnf(c_639,plain,
e_1260 = e_1299,
inference(paramod,[status(thm)],[c_101,c_638]) ).
cnf(c_421,plain,
e_1299 = e_1260,
inference(copy,[status(thm)],[c_639]) ).
cnf(c_640,plain,
select(a_1259,i7) = e_1297,
inference(paramod,[status(thm)],[c_416,c_135]) ).
cnf(c_641,plain,
e_1262 = e_1297,
inference(paramod,[status(thm)],[c_103,c_640]) ).
cnf(c_422,plain,
e_1297 = e_1262,
inference(copy,[status(thm)],[c_641]) ).
cnf(c_642,plain,
store(a_1259,i1,e_1297) = a_1298,
inference(paramod,[status(thm)],[c_416,c_61]) ).
cnf(c_423,plain,
store(a_1259,i1,e_1262) = a_1298,
inference(paramod,[status(thm)],[c_422,c_642]) ).
cnf(c_427,plain,
store(a_1298,i7,e_1260) = a_1300,
inference(paramod,[status(thm)],[c_421,c_63]) ).
cnf(c_643,plain,
store(store(a_1259,i1,select(a_1259,i7)),i7,e_1260) = store(a_1261,i1,select(a_1259,i7)),
inference(paramod,[status(thm)],[c_21,c_210]) ).
cnf(c_644,plain,
store(store(a_1259,i1,e_1262),i7,e_1260) = store(a_1261,i1,select(a_1259,i7)),
inference(paramod,[status(thm)],[c_103,c_643]) ).
cnf(c_645,plain,
store(a_1298,i7,e_1260) = store(a_1261,i1,select(a_1259,i7)),
inference(paramod,[status(thm)],[c_423,c_644]) ).
cnf(c_646,plain,
a_1300 = store(a_1261,i1,select(a_1259,i7)),
inference(paramod,[status(thm)],[c_427,c_645]) ).
cnf(c_647,plain,
a_1300 = store(a_1261,i1,e_1262),
inference(paramod,[status(thm)],[c_103,c_646]) ).
cnf(c_447,plain,
a_1300 = a_1263,
inference(paramod,[status(thm)],[c_23,c_647]) ).
cnf(c_648,plain,
select(a_1263,i4) = e_1303,
inference(paramod,[status(thm)],[c_447,c_141]) ).
cnf(c_649,plain,
e_1266 = e_1303,
inference(paramod,[status(thm)],[c_107,c_648]) ).
cnf(c_459,plain,
e_1303 = e_1266,
inference(copy,[status(thm)],[c_649]) ).
cnf(c_650,plain,
select(a_1263,i5) = e_1301,
inference(paramod,[status(thm)],[c_447,c_139]) ).
cnf(c_651,plain,
e_1264 = e_1301,
inference(paramod,[status(thm)],[c_105,c_650]) ).
cnf(c_460,plain,
e_1301 = e_1264,
inference(copy,[status(thm)],[c_651]) ).
cnf(c_652,plain,
store(a_1263,i4,e_1301) = a_1302,
inference(paramod,[status(thm)],[c_447,c_65]) ).
cnf(c_653,plain,
store(a_1263,i4,e_1264) = a_1302,
inference(paramod,[status(thm)],[c_460,c_652]) ).
cnf(c_654,plain,
a_1265 = a_1302,
inference(paramod,[status(thm)],[c_25,c_653]) ).
cnf(c_461,plain,
a_1302 = a_1265,
inference(copy,[status(thm)],[c_654]) ).
cnf(c_655,plain,
store(a_1265,i5,e_1303) = a_1304,
inference(paramod,[status(thm)],[c_461,c_67]) ).
cnf(c_656,plain,
store(a_1265,i5,e_1266) = a_1304,
inference(paramod,[status(thm)],[c_459,c_655]) ).
cnf(c_657,plain,
a_1267 = a_1304,
inference(paramod,[status(thm)],[c_27,c_656]) ).
cnf(c_465,plain,
a_1304 = a_1267,
inference(copy,[status(thm)],[c_657]) ).
cnf(c_658,plain,
select(a_1267,i0) = e_1305,
inference(paramod,[status(thm)],[c_465,c_143]) ).
cnf(c_659,plain,
e_1268 = e_1305,
inference(paramod,[status(thm)],[c_109,c_658]) ).
cnf(c_468,plain,
e_1305 = e_1268,
inference(copy,[status(thm)],[c_659]) ).
cnf(c_660,plain,
store(a_1267,i0,e_1305) = a_1306,
inference(paramod,[status(thm)],[c_465,c_69]) ).
cnf(c_661,plain,
store(a_1267,i0,e_1268) = a_1306,
inference(paramod,[status(thm)],[c_468,c_660]) ).
cnf(c_662,plain,
a_1269 = a_1306,
inference(paramod,[status(thm)],[c_29,c_661]) ).
cnf(c_469,plain,
a_1306 = a_1269,
inference(copy,[status(thm)],[c_662]) ).
cnf(c_663,plain,
store(a_1269,i0,e_1305) = a_1307,
inference(paramod,[status(thm)],[c_469,c_71]) ).
cnf(c_664,plain,
store(a_1269,i0,e_1268) = a_1307,
inference(paramod,[status(thm)],[c_468,c_663]) ).
cnf(c_665,plain,
a_1270 = a_1307,
inference(paramod,[status(thm)],[c_31,c_664]) ).
cnf(c_473,plain,
a_1307 = a_1270,
inference(copy,[status(thm)],[c_665]) ).
cnf(c_666,plain,
select(a_1270,i2) = e_1310,
inference(paramod,[status(thm)],[c_473,c_147]) ).
cnf(c_667,plain,
e_1271 = e_1310,
inference(paramod,[status(thm)],[c_111,c_666]) ).
cnf(c_478,plain,
e_1310 = e_1271,
inference(copy,[status(thm)],[c_667]) ).
cnf(c_668,plain,
select(a_1270,i1) = e_1308,
inference(paramod,[status(thm)],[c_473,c_145]) ).
cnf(c_669,plain,
e_1273 = e_1308,
inference(paramod,[status(thm)],[c_113,c_668]) ).
cnf(c_479,plain,
e_1308 = e_1273,
inference(copy,[status(thm)],[c_669]) ).
cnf(c_670,plain,
store(a_1270,i2,e_1308) = a_1309,
inference(paramod,[status(thm)],[c_473,c_73]) ).
cnf(c_480,plain,
store(a_1270,i2,e_1273) = a_1309,
inference(paramod,[status(thm)],[c_479,c_670]) ).
cnf(c_484,plain,
store(a_1309,i1,e_1271) = a_1311,
inference(paramod,[status(thm)],[c_478,c_75]) ).
cnf(c_671,plain,
store(store(a_1270,i2,select(a_1270,i1)),i1,e_1271) = store(a_1272,i2,select(a_1270,i1)),
inference(paramod,[status(thm)],[c_33,c_215]) ).
cnf(c_672,plain,
store(store(a_1270,i2,e_1273),i1,e_1271) = store(a_1272,i2,select(a_1270,i1)),
inference(paramod,[status(thm)],[c_113,c_671]) ).
cnf(c_673,plain,
store(a_1309,i1,e_1271) = store(a_1272,i2,select(a_1270,i1)),
inference(paramod,[status(thm)],[c_480,c_672]) ).
cnf(c_674,plain,
a_1311 = store(a_1272,i2,select(a_1270,i1)),
inference(paramod,[status(thm)],[c_484,c_673]) ).
cnf(c_675,plain,
a_1311 = store(a_1272,i2,e_1273),
inference(paramod,[status(thm)],[c_113,c_674]) ).
cnf(c_528,plain,
a_1311 = a_1274,
inference(paramod,[status(thm)],[c_35,c_675]) ).
cnf(c_676,plain,
select(a_1274,i3) = e_1314,
inference(paramod,[status(thm)],[c_528,c_151]) ).
cnf(c_677,plain,
e_1277 = e_1314,
inference(paramod,[status(thm)],[c_117,c_676]) ).
cnf(c_539,plain,
e_1314 = e_1277,
inference(copy,[status(thm)],[c_677]) ).
cnf(c_678,plain,
select(a_1274,i0) = e_1312,
inference(paramod,[status(thm)],[c_528,c_149]) ).
cnf(c_679,plain,
e_1275 = e_1312,
inference(paramod,[status(thm)],[c_115,c_678]) ).
cnf(c_540,plain,
e_1312 = e_1275,
inference(copy,[status(thm)],[c_679]) ).
cnf(c_680,plain,
store(a_1274,i3,e_1312) = a_1313,
inference(paramod,[status(thm)],[c_528,c_77]) ).
cnf(c_681,plain,
store(a_1274,i3,e_1275) = a_1313,
inference(paramod,[status(thm)],[c_540,c_680]) ).
cnf(c_682,plain,
a_1276 = a_1313,
inference(paramod,[status(thm)],[c_37,c_681]) ).
cnf(c_541,plain,
a_1313 = a_1276,
inference(copy,[status(thm)],[c_682]) ).
cnf(c_683,plain,
store(a_1276,i0,e_1314) = a_1315,
inference(paramod,[status(thm)],[c_541,c_79]) ).
cnf(c_684,plain,
store(a_1276,i0,e_1277) = a_1315,
inference(paramod,[status(thm)],[c_539,c_683]) ).
cnf(c_685,plain,
a_1278 = a_1315,
inference(paramod,[status(thm)],[c_39,c_684]) ).
cnf(c_545,plain,
a_1315 = a_1278,
inference(copy,[status(thm)],[c_685]) ).
cnf(c_686,plain,
select(a_1278,i5) = e_1318,
inference(paramod,[status(thm)],[c_545,c_155]) ).
cnf(c_687,plain,
e_1279 = e_1318,
inference(paramod,[status(thm)],[c_119,c_686]) ).
cnf(c_550,plain,
e_1318 = e_1279,
inference(copy,[status(thm)],[c_687]) ).
cnf(c_688,plain,
select(a_1278,i9) = e_1316,
inference(paramod,[status(thm)],[c_545,c_153]) ).
cnf(c_689,plain,
e_1281 = e_1316,
inference(paramod,[status(thm)],[c_121,c_688]) ).
cnf(c_551,plain,
e_1316 = e_1281,
inference(copy,[status(thm)],[c_689]) ).
cnf(c_690,plain,
store(a_1278,i5,e_1316) = a_1317,
inference(paramod,[status(thm)],[c_545,c_81]) ).
cnf(c_552,plain,
store(a_1278,i5,e_1281) = a_1317,
inference(paramod,[status(thm)],[c_551,c_690]) ).
cnf(c_556,plain,
store(a_1317,i9,e_1279) = a_1319,
inference(paramod,[status(thm)],[c_550,c_83]) ).
cnf(c_691,plain,
store(store(a_1278,i5,select(a_1278,i9)),i9,e_1279) = store(a_1280,i5,select(a_1278,i9)),
inference(paramod,[status(thm)],[c_41,c_219]) ).
cnf(c_692,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = store(a_1280,i5,select(a_1278,i9)),
inference(paramod,[status(thm)],[c_121,c_691]) ).
cnf(c_693,plain,
store(a_1317,i9,e_1279) = store(a_1280,i5,select(a_1278,i9)),
inference(paramod,[status(thm)],[c_552,c_692]) ).
cnf(c_694,plain,
a_1319 = store(a_1280,i5,select(a_1278,i9)),
inference(paramod,[status(thm)],[c_556,c_693]) ).
cnf(c_695,plain,
a_1319 = store(a_1280,i5,e_1281),
inference(paramod,[status(thm)],[c_121,c_694]) ).
cnf(c_696,plain,
a_1319 = a_1282,
inference(paramod,[status(thm)],[c_43,c_695]) ).
cnf(c_590,plain,
$false,
inference(resolve,[status(thm)],[c_157,c_696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n011.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 14:21:14 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 770543 was started by sandbox on n011,
% 0.17/0.45 % Sat Sep 26 14:21:14 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.46
% 0.17/0.46 % From the command line: assign(max_seconds, 300).
% 8.29/1.60
% 8.29/1.60 % SZS status Unsatisfiable for theBenchmark
% 8.29/1.60
% 8.29/1.60 % Proof 1 at 1.06 (+ 0.05) seconds.
% 8.29/1.60 % Length of proof is 210.
% 8.29/1.60 % Level of proof is 30.
% 8.29/1.60 % Maximum clause weight is 43.000.
% 8.29/1.60 % Given clauses 229.
% 8.29/1.60
% 8.29/1.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------