%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV547-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 : n026.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:16 AM UTC 2026
% Result : Unsatisfiable 11.43s 1.82s
% Output : CNFRefutation 11.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 81
% Syntax : Number of formulae : 404 ( 404 unt; 0 def)
% Number of atoms : 404 ( 403 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 : 92 ( 92 usr; 90 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_1296 = store(a1,i8,e_1295),
file('theBenchmark.p',hyp0) ).
cnf(c_4,plain,
a_1296 = store(a1,i8,e_1295),
inference(clausify,[status(thm)],[hyp0]) ).
cnf(c_5,plain,
store(a1,i8,e_1295) = a_1296,
inference(copy,[status(thm)],[c_4]) ).
fof(hyp1,axiom,
a_1298 = store(a_1296,i7,e_1297),
file('theBenchmark.p',hyp1) ).
cnf(c_6,plain,
a_1298 = store(a_1296,i7,e_1297),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_7,plain,
store(a_1296,i7,e_1297) = a_1298,
inference(copy,[status(thm)],[c_6]) ).
fof(hyp2,axiom,
a_1300 = store(a_1298,i6,e_1299),
file('theBenchmark.p',hyp2) ).
cnf(c_8,plain,
a_1300 = store(a_1298,i6,e_1299),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_9,plain,
store(a_1298,i6,e_1299) = a_1300,
inference(copy,[status(thm)],[c_8]) ).
fof(hyp3,axiom,
a_1302 = store(a_1300,i8,e_1301),
file('theBenchmark.p',hyp3) ).
cnf(c_10,plain,
a_1302 = store(a_1300,i8,e_1301),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_11,plain,
store(a_1300,i8,e_1301) = a_1302,
inference(copy,[status(thm)],[c_10]) ).
fof(hyp4,axiom,
a_1304 = store(a_1302,i8,e_1303),
file('theBenchmark.p',hyp4) ).
cnf(c_12,plain,
a_1304 = store(a_1302,i8,e_1303),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_13,plain,
store(a_1302,i8,e_1303) = a_1304,
inference(copy,[status(thm)],[c_12]) ).
fof(hyp5,axiom,
a_1306 = store(a_1304,i5,e_1305),
file('theBenchmark.p',hyp5) ).
cnf(c_14,plain,
a_1306 = store(a_1304,i5,e_1305),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_15,plain,
store(a_1304,i5,e_1305) = a_1306,
inference(copy,[status(thm)],[c_14]) ).
fof(hyp6,axiom,
a_1308 = store(a_1306,i4,e_1307),
file('theBenchmark.p',hyp6) ).
cnf(c_16,plain,
a_1308 = store(a_1306,i4,e_1307),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_17,plain,
store(a_1306,i4,e_1307) = a_1308,
inference(copy,[status(thm)],[c_16]) ).
fof(hyp7,axiom,
a_1310 = store(a_1308,i9,e_1309),
file('theBenchmark.p',hyp7) ).
cnf(c_18,plain,
a_1310 = store(a_1308,i9,e_1309),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_19,plain,
store(a_1308,i9,e_1309) = a_1310,
inference(copy,[status(thm)],[c_18]) ).
fof(hyp8,axiom,
a_1312 = store(a_1310,i7,e_1311),
file('theBenchmark.p',hyp8) ).
cnf(c_20,plain,
a_1312 = store(a_1310,i7,e_1311),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_21,plain,
store(a_1310,i7,e_1311) = a_1312,
inference(copy,[status(thm)],[c_20]) ).
fof(hyp9,axiom,
a_1314 = store(a_1312,i1,e_1313),
file('theBenchmark.p',hyp9) ).
cnf(c_22,plain,
a_1314 = store(a_1312,i1,e_1313),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_23,plain,
store(a_1312,i1,e_1313) = a_1314,
inference(copy,[status(thm)],[c_22]) ).
fof(hyp10,axiom,
a_1316 = store(a_1314,i4,e_1315),
file('theBenchmark.p',hyp10) ).
cnf(c_24,plain,
a_1316 = store(a_1314,i4,e_1315),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_25,plain,
store(a_1314,i4,e_1315) = a_1316,
inference(copy,[status(thm)],[c_24]) ).
fof(hyp11,axiom,
a_1318 = store(a_1316,i5,e_1317),
file('theBenchmark.p',hyp11) ).
cnf(c_26,plain,
a_1318 = store(a_1316,i5,e_1317),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_27,plain,
store(a_1316,i5,e_1317) = a_1318,
inference(copy,[status(thm)],[c_26]) ).
fof(hyp12,axiom,
a_1320 = store(a_1318,i0,e_1319),
file('theBenchmark.p',hyp12) ).
cnf(c_28,plain,
a_1320 = store(a_1318,i0,e_1319),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_29,plain,
store(a_1318,i0,e_1319) = a_1320,
inference(copy,[status(thm)],[c_28]) ).
fof(hyp13,axiom,
a_1321 = store(a_1320,i0,e_1319),
file('theBenchmark.p',hyp13) ).
cnf(c_30,plain,
a_1321 = store(a_1320,i0,e_1319),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_31,plain,
store(a_1320,i0,e_1319) = a_1321,
inference(copy,[status(thm)],[c_30]) ).
fof(hyp14,axiom,
a_1323 = store(a_1321,i1,e_1322),
file('theBenchmark.p',hyp14) ).
cnf(c_32,plain,
a_1323 = store(a_1321,i1,e_1322),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_33,plain,
store(a_1321,i1,e_1322) = a_1323,
inference(copy,[status(thm)],[c_32]) ).
fof(hyp15,axiom,
a_1325 = store(a_1323,i2,e_1324),
file('theBenchmark.p',hyp15) ).
cnf(c_34,plain,
a_1325 = store(a_1323,i2,e_1324),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_35,plain,
store(a_1323,i2,e_1324) = a_1325,
inference(copy,[status(thm)],[c_34]) ).
fof(hyp16,axiom,
a_1327 = store(a_1325,i3,e_1326),
file('theBenchmark.p',hyp16) ).
cnf(c_36,plain,
a_1327 = store(a_1325,i3,e_1326),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_37,plain,
store(a_1325,i3,e_1326) = a_1327,
inference(copy,[status(thm)],[c_36]) ).
fof(hyp17,axiom,
a_1329 = store(a_1327,i0,e_1328),
file('theBenchmark.p',hyp17) ).
cnf(c_38,plain,
a_1329 = store(a_1327,i0,e_1328),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_39,plain,
store(a_1327,i0,e_1328) = a_1329,
inference(copy,[status(thm)],[c_38]) ).
fof(hyp18,axiom,
a_1331 = store(a_1329,i9,e_1330),
file('theBenchmark.p',hyp18) ).
cnf(c_40,plain,
a_1331 = store(a_1329,i9,e_1330),
inference(clausify,[status(thm)],[hyp18]) ).
cnf(c_41,plain,
store(a_1329,i9,e_1330) = a_1331,
inference(copy,[status(thm)],[c_40]) ).
fof(hyp19,axiom,
a_1333 = store(a_1331,i5,e_1332),
file('theBenchmark.p',hyp19) ).
cnf(c_42,plain,
a_1333 = store(a_1331,i5,e_1332),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_43,plain,
store(a_1331,i5,e_1332) = a_1333,
inference(copy,[status(thm)],[c_42]) ).
fof(hyp20,axiom,
a_1334 = store(a1,i7,e_1297),
file('theBenchmark.p',hyp20) ).
cnf(c_44,plain,
a_1334 = store(a1,i7,e_1297),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_45,plain,
store(a1,i7,e_1297) = a_1334,
inference(copy,[status(thm)],[c_44]) ).
fof(hyp21,axiom,
a_1335 = store(a_1334,i8,e_1295),
file('theBenchmark.p',hyp21) ).
cnf(c_46,plain,
a_1335 = store(a_1334,i8,e_1295),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_47,plain,
store(a_1334,i8,e_1295) = a_1335,
inference(copy,[status(thm)],[c_46]) ).
fof(hyp22,axiom,
a_1337 = store(a_1335,i6,e_1336),
file('theBenchmark.p',hyp22) ).
cnf(c_48,plain,
a_1337 = store(a_1335,i6,e_1336),
inference(clausify,[status(thm)],[hyp22]) ).
cnf(c_49,plain,
store(a_1335,i6,e_1336) = a_1337,
inference(copy,[status(thm)],[c_48]) ).
fof(hyp23,axiom,
a_1339 = store(a_1337,i8,e_1338),
file('theBenchmark.p',hyp23) ).
cnf(c_50,plain,
a_1339 = store(a_1337,i8,e_1338),
inference(clausify,[status(thm)],[hyp23]) ).
cnf(c_51,plain,
store(a_1337,i8,e_1338) = a_1339,
inference(copy,[status(thm)],[c_50]) ).
fof(hyp24,axiom,
a_1341 = store(a_1339,i5,e_1340),
file('theBenchmark.p',hyp24) ).
cnf(c_52,plain,
a_1341 = store(a_1339,i5,e_1340),
inference(clausify,[status(thm)],[hyp24]) ).
cnf(c_53,plain,
store(a_1339,i5,e_1340) = a_1341,
inference(copy,[status(thm)],[c_52]) ).
fof(hyp25,axiom,
a_1343 = store(a_1341,i8,e_1342),
file('theBenchmark.p',hyp25) ).
cnf(c_54,plain,
a_1343 = store(a_1341,i8,e_1342),
inference(clausify,[status(thm)],[hyp25]) ).
cnf(c_55,plain,
store(a_1341,i8,e_1342) = a_1343,
inference(copy,[status(thm)],[c_54]) ).
fof(hyp26,axiom,
a_1345 = store(a_1343,i4,e_1344),
file('theBenchmark.p',hyp26) ).
cnf(c_56,plain,
a_1345 = store(a_1343,i4,e_1344),
inference(clausify,[status(thm)],[hyp26]) ).
cnf(c_57,plain,
store(a_1343,i4,e_1344) = a_1345,
inference(copy,[status(thm)],[c_56]) ).
fof(hyp27,axiom,
a_1347 = store(a_1345,i9,e_1346),
file('theBenchmark.p',hyp27) ).
cnf(c_58,plain,
a_1347 = store(a_1345,i9,e_1346),
inference(clausify,[status(thm)],[hyp27]) ).
cnf(c_59,plain,
store(a_1345,i9,e_1346) = a_1347,
inference(copy,[status(thm)],[c_58]) ).
fof(hyp28,axiom,
a_1349 = store(a_1347,i1,e_1348),
file('theBenchmark.p',hyp28) ).
cnf(c_60,plain,
a_1349 = store(a_1347,i1,e_1348),
inference(clausify,[status(thm)],[hyp28]) ).
cnf(c_61,plain,
store(a_1347,i1,e_1348) = a_1349,
inference(copy,[status(thm)],[c_60]) ).
fof(hyp29,axiom,
a_1351 = store(a_1349,i7,e_1350),
file('theBenchmark.p',hyp29) ).
cnf(c_62,plain,
a_1351 = store(a_1349,i7,e_1350),
inference(clausify,[status(thm)],[hyp29]) ).
cnf(c_63,plain,
store(a_1349,i7,e_1350) = a_1351,
inference(copy,[status(thm)],[c_62]) ).
fof(hyp30,axiom,
a_1353 = store(a_1351,i4,e_1352),
file('theBenchmark.p',hyp30) ).
cnf(c_64,plain,
a_1353 = store(a_1351,i4,e_1352),
inference(clausify,[status(thm)],[hyp30]) ).
cnf(c_65,plain,
store(a_1351,i4,e_1352) = a_1353,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp31,axiom,
a_1355 = store(a_1353,i5,e_1354),
file('theBenchmark.p',hyp31) ).
cnf(c_66,plain,
a_1355 = store(a_1353,i5,e_1354),
inference(clausify,[status(thm)],[hyp31]) ).
cnf(c_67,plain,
store(a_1353,i5,e_1354) = a_1355,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp32,axiom,
a_1357 = store(a_1355,i0,e_1356),
file('theBenchmark.p',hyp32) ).
cnf(c_68,plain,
a_1357 = store(a_1355,i0,e_1356),
inference(clausify,[status(thm)],[hyp32]) ).
cnf(c_69,plain,
store(a_1355,i0,e_1356) = a_1357,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp33,axiom,
a_1358 = store(a_1357,i0,e_1356),
file('theBenchmark.p',hyp33) ).
cnf(c_70,plain,
a_1358 = store(a_1357,i0,e_1356),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_71,plain,
store(a_1357,i0,e_1356) = a_1358,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp34,axiom,
a_1360 = store(a_1358,i2,e_1359),
file('theBenchmark.p',hyp34) ).
cnf(c_72,plain,
a_1360 = store(a_1358,i2,e_1359),
inference(clausify,[status(thm)],[hyp34]) ).
cnf(c_73,plain,
store(a_1358,i2,e_1359) = a_1360,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp35,axiom,
a_1362 = store(a_1360,i1,e_1361),
file('theBenchmark.p',hyp35) ).
cnf(c_74,plain,
a_1362 = store(a_1360,i1,e_1361),
inference(clausify,[status(thm)],[hyp35]) ).
cnf(c_75,plain,
store(a_1360,i1,e_1361) = a_1362,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp36,axiom,
a_1364 = store(a_1362,i3,e_1363),
file('theBenchmark.p',hyp36) ).
cnf(c_76,plain,
a_1364 = store(a_1362,i3,e_1363),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_77,plain,
store(a_1362,i3,e_1363) = a_1364,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp37,axiom,
a_1366 = store(a_1364,i0,e_1365),
file('theBenchmark.p',hyp37) ).
cnf(c_78,plain,
a_1366 = store(a_1364,i0,e_1365),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_79,plain,
store(a_1364,i0,e_1365) = a_1366,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp38,axiom,
a_1368 = store(a_1366,i5,e_1367),
file('theBenchmark.p',hyp38) ).
cnf(c_80,plain,
a_1368 = store(a_1366,i5,e_1367),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_81,plain,
store(a_1366,i5,e_1367) = a_1368,
inference(copy,[status(thm)],[c_80]) ).
fof(hyp39,axiom,
a_1370 = store(a_1368,i9,e_1369),
file('theBenchmark.p',hyp39) ).
cnf(c_82,plain,
a_1370 = store(a_1368,i9,e_1369),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_83,plain,
store(a_1368,i9,e_1369) = a_1370,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp40,axiom,
e_1295 = select(a1,i7),
file('theBenchmark.p',hyp40) ).
cnf(c_84,plain,
e_1295 = select(a1,i7),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_85,plain,
select(a1,i7) = e_1295,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp41,axiom,
e_1297 = select(a1,i8),
file('theBenchmark.p',hyp41) ).
cnf(c_86,plain,
e_1297 = select(a1,i8),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_87,plain,
select(a1,i8) = e_1297,
inference(copy,[status(thm)],[c_86]) ).
fof(hyp42,axiom,
e_1299 = select(a_1298,i8),
file('theBenchmark.p',hyp42) ).
cnf(c_88,plain,
e_1299 = select(a_1298,i8),
inference(clausify,[status(thm)],[hyp42]) ).
cnf(c_89,plain,
select(a_1298,i8) = e_1299,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp43,axiom,
e_1301 = select(a_1298,i6),
file('theBenchmark.p',hyp43) ).
cnf(c_90,plain,
e_1301 = select(a_1298,i6),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_91,plain,
select(a_1298,i6) = e_1301,
inference(copy,[status(thm)],[c_90]) ).
fof(hyp44,axiom,
e_1303 = select(a_1302,i5),
file('theBenchmark.p',hyp44) ).
cnf(c_92,plain,
e_1303 = select(a_1302,i5),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_93,plain,
select(a_1302,i5) = e_1303,
inference(copy,[status(thm)],[c_92]) ).
fof(hyp45,axiom,
e_1305 = select(a_1302,i8),
file('theBenchmark.p',hyp45) ).
cnf(c_94,plain,
e_1305 = select(a_1302,i8),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_95,plain,
select(a_1302,i8) = e_1305,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp46,axiom,
e_1307 = select(a_1306,i9),
file('theBenchmark.p',hyp46) ).
cnf(c_96,plain,
e_1307 = select(a_1306,i9),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_97,plain,
select(a_1306,i9) = e_1307,
inference(copy,[status(thm)],[c_96]) ).
fof(hyp47,axiom,
e_1309 = select(a_1306,i4),
file('theBenchmark.p',hyp47) ).
cnf(c_98,plain,
e_1309 = select(a_1306,i4),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_99,plain,
select(a_1306,i4) = e_1309,
inference(copy,[status(thm)],[c_98]) ).
fof(hyp48,axiom,
e_1311 = select(a_1310,i1),
file('theBenchmark.p',hyp48) ).
cnf(c_100,plain,
e_1311 = select(a_1310,i1),
inference(clausify,[status(thm)],[hyp48]) ).
cnf(c_101,plain,
select(a_1310,i1) = e_1311,
inference(copy,[status(thm)],[c_100]) ).
fof(hyp49,axiom,
e_1313 = select(a_1310,i7),
file('theBenchmark.p',hyp49) ).
cnf(c_102,plain,
e_1313 = select(a_1310,i7),
inference(clausify,[status(thm)],[hyp49]) ).
cnf(c_103,plain,
select(a_1310,i7) = e_1313,
inference(copy,[status(thm)],[c_102]) ).
fof(hyp50,axiom,
e_1315 = select(a_1314,i5),
file('theBenchmark.p',hyp50) ).
cnf(c_104,plain,
e_1315 = select(a_1314,i5),
inference(clausify,[status(thm)],[hyp50]) ).
cnf(c_105,plain,
select(a_1314,i5) = e_1315,
inference(copy,[status(thm)],[c_104]) ).
fof(hyp51,axiom,
e_1317 = select(a_1314,i4),
file('theBenchmark.p',hyp51) ).
cnf(c_106,plain,
e_1317 = select(a_1314,i4),
inference(clausify,[status(thm)],[hyp51]) ).
cnf(c_107,plain,
select(a_1314,i4) = e_1317,
inference(copy,[status(thm)],[c_106]) ).
fof(hyp52,axiom,
e_1319 = select(a_1318,i0),
file('theBenchmark.p',hyp52) ).
cnf(c_108,plain,
e_1319 = select(a_1318,i0),
inference(clausify,[status(thm)],[hyp52]) ).
cnf(c_109,plain,
select(a_1318,i0) = e_1319,
inference(copy,[status(thm)],[c_108]) ).
fof(hyp53,axiom,
e_1322 = select(a_1321,i2),
file('theBenchmark.p',hyp53) ).
cnf(c_110,plain,
e_1322 = select(a_1321,i2),
inference(clausify,[status(thm)],[hyp53]) ).
cnf(c_111,plain,
select(a_1321,i2) = e_1322,
inference(copy,[status(thm)],[c_110]) ).
fof(hyp54,axiom,
e_1324 = select(a_1321,i1),
file('theBenchmark.p',hyp54) ).
cnf(c_112,plain,
e_1324 = select(a_1321,i1),
inference(clausify,[status(thm)],[hyp54]) ).
cnf(c_113,plain,
select(a_1321,i1) = e_1324,
inference(copy,[status(thm)],[c_112]) ).
fof(hyp55,axiom,
e_1326 = select(a_1325,i0),
file('theBenchmark.p',hyp55) ).
cnf(c_114,plain,
e_1326 = select(a_1325,i0),
inference(clausify,[status(thm)],[hyp55]) ).
cnf(c_115,plain,
select(a_1325,i0) = e_1326,
inference(copy,[status(thm)],[c_114]) ).
fof(hyp56,axiom,
e_1328 = select(a_1325,i3),
file('theBenchmark.p',hyp56) ).
cnf(c_116,plain,
e_1328 = select(a_1325,i3),
inference(clausify,[status(thm)],[hyp56]) ).
cnf(c_117,plain,
select(a_1325,i3) = e_1328,
inference(copy,[status(thm)],[c_116]) ).
fof(hyp57,axiom,
e_1330 = select(a_1329,i5),
file('theBenchmark.p',hyp57) ).
cnf(c_118,plain,
e_1330 = select(a_1329,i5),
inference(clausify,[status(thm)],[hyp57]) ).
cnf(c_119,plain,
select(a_1329,i5) = e_1330,
inference(copy,[status(thm)],[c_118]) ).
fof(hyp58,axiom,
e_1332 = select(a_1329,i9),
file('theBenchmark.p',hyp58) ).
cnf(c_120,plain,
e_1332 = select(a_1329,i9),
inference(clausify,[status(thm)],[hyp58]) ).
cnf(c_121,plain,
select(a_1329,i9) = e_1332,
inference(copy,[status(thm)],[c_120]) ).
fof(hyp59,axiom,
e_1336 = select(a_1335,i8),
file('theBenchmark.p',hyp59) ).
cnf(c_122,plain,
e_1336 = select(a_1335,i8),
inference(clausify,[status(thm)],[hyp59]) ).
cnf(c_123,plain,
select(a_1335,i8) = e_1336,
inference(copy,[status(thm)],[c_122]) ).
fof(hyp60,axiom,
e_1338 = select(a_1335,i6),
file('theBenchmark.p',hyp60) ).
cnf(c_124,plain,
e_1338 = select(a_1335,i6),
inference(clausify,[status(thm)],[hyp60]) ).
cnf(c_125,plain,
select(a_1335,i6) = e_1338,
inference(copy,[status(thm)],[c_124]) ).
fof(hyp61,axiom,
e_1340 = select(a_1339,i8),
file('theBenchmark.p',hyp61) ).
cnf(c_126,plain,
e_1340 = select(a_1339,i8),
inference(clausify,[status(thm)],[hyp61]) ).
cnf(c_127,plain,
select(a_1339,i8) = e_1340,
inference(copy,[status(thm)],[c_126]) ).
fof(hyp62,axiom,
e_1342 = select(a_1339,i5),
file('theBenchmark.p',hyp62) ).
cnf(c_128,plain,
e_1342 = select(a_1339,i5),
inference(clausify,[status(thm)],[hyp62]) ).
cnf(c_129,plain,
select(a_1339,i5) = e_1342,
inference(copy,[status(thm)],[c_128]) ).
fof(hyp63,axiom,
e_1344 = select(a_1343,i9),
file('theBenchmark.p',hyp63) ).
cnf(c_130,plain,
e_1344 = select(a_1343,i9),
inference(clausify,[status(thm)],[hyp63]) ).
cnf(c_131,plain,
select(a_1343,i9) = e_1344,
inference(copy,[status(thm)],[c_130]) ).
fof(hyp64,axiom,
e_1346 = select(a_1343,i4),
file('theBenchmark.p',hyp64) ).
cnf(c_132,plain,
e_1346 = select(a_1343,i4),
inference(clausify,[status(thm)],[hyp64]) ).
cnf(c_133,plain,
select(a_1343,i4) = e_1346,
inference(copy,[status(thm)],[c_132]) ).
fof(hyp65,axiom,
e_1348 = select(a_1347,i7),
file('theBenchmark.p',hyp65) ).
cnf(c_134,plain,
e_1348 = select(a_1347,i7),
inference(clausify,[status(thm)],[hyp65]) ).
cnf(c_135,plain,
select(a_1347,i7) = e_1348,
inference(copy,[status(thm)],[c_134]) ).
fof(hyp66,axiom,
e_1350 = select(a_1347,i1),
file('theBenchmark.p',hyp66) ).
cnf(c_136,plain,
e_1350 = select(a_1347,i1),
inference(clausify,[status(thm)],[hyp66]) ).
cnf(c_137,plain,
select(a_1347,i1) = e_1350,
inference(copy,[status(thm)],[c_136]) ).
fof(hyp67,axiom,
e_1352 = select(a_1351,i5),
file('theBenchmark.p',hyp67) ).
cnf(c_138,plain,
e_1352 = select(a_1351,i5),
inference(clausify,[status(thm)],[hyp67]) ).
cnf(c_139,plain,
select(a_1351,i5) = e_1352,
inference(copy,[status(thm)],[c_138]) ).
fof(hyp68,axiom,
e_1354 = select(a_1351,i4),
file('theBenchmark.p',hyp68) ).
cnf(c_140,plain,
e_1354 = select(a_1351,i4),
inference(clausify,[status(thm)],[hyp68]) ).
cnf(c_141,plain,
select(a_1351,i4) = e_1354,
inference(copy,[status(thm)],[c_140]) ).
fof(hyp69,axiom,
e_1356 = select(a_1355,i0),
file('theBenchmark.p',hyp69) ).
cnf(c_142,plain,
e_1356 = select(a_1355,i0),
inference(clausify,[status(thm)],[hyp69]) ).
cnf(c_143,plain,
select(a_1355,i0) = e_1356,
inference(copy,[status(thm)],[c_142]) ).
fof(hyp70,axiom,
e_1359 = select(a_1358,i1),
file('theBenchmark.p',hyp70) ).
cnf(c_144,plain,
e_1359 = select(a_1358,i1),
inference(clausify,[status(thm)],[hyp70]) ).
cnf(c_145,plain,
select(a_1358,i1) = e_1359,
inference(copy,[status(thm)],[c_144]) ).
fof(hyp71,axiom,
e_1361 = select(a_1358,i2),
file('theBenchmark.p',hyp71) ).
cnf(c_146,plain,
e_1361 = select(a_1358,i2),
inference(clausify,[status(thm)],[hyp71]) ).
cnf(c_147,plain,
select(a_1358,i2) = e_1361,
inference(copy,[status(thm)],[c_146]) ).
fof(hyp72,axiom,
e_1363 = select(a_1362,i0),
file('theBenchmark.p',hyp72) ).
cnf(c_148,plain,
e_1363 = select(a_1362,i0),
inference(clausify,[status(thm)],[hyp72]) ).
cnf(c_149,plain,
select(a_1362,i0) = e_1363,
inference(copy,[status(thm)],[c_148]) ).
fof(hyp73,axiom,
e_1365 = select(a_1362,i3),
file('theBenchmark.p',hyp73) ).
cnf(c_150,plain,
e_1365 = select(a_1362,i3),
inference(clausify,[status(thm)],[hyp73]) ).
cnf(c_151,plain,
select(a_1362,i3) = e_1365,
inference(copy,[status(thm)],[c_150]) ).
fof(hyp74,axiom,
e_1367 = select(a_1366,i9),
file('theBenchmark.p',hyp74) ).
cnf(c_152,plain,
e_1367 = select(a_1366,i9),
inference(clausify,[status(thm)],[hyp74]) ).
cnf(c_153,plain,
select(a_1366,i9) = e_1367,
inference(copy,[status(thm)],[c_152]) ).
fof(hyp75,axiom,
e_1369 = select(a_1366,i5),
file('theBenchmark.p',hyp75) ).
cnf(c_154,plain,
e_1369 = select(a_1366,i5),
inference(clausify,[status(thm)],[hyp75]) ).
cnf(c_155,plain,
select(a_1366,i5) = e_1369,
inference(copy,[status(thm)],[c_154]) ).
fof(hyp76,axiom,
e_1372 = select(a_1333,i_1371),
file('theBenchmark.p',hyp76) ).
cnf(c_156,plain,
e_1372 = select(a_1333,i_1371),
inference(clausify,[status(thm)],[hyp76]) ).
cnf(c_157,plain,
select(a_1333,i_1371) = e_1372,
inference(copy,[status(thm)],[c_156]) ).
fof(hyp77,axiom,
e_1373 = select(a_1370,i_1371),
file('theBenchmark.p',hyp77) ).
cnf(c_158,plain,
e_1373 = select(a_1370,i_1371),
inference(clausify,[status(thm)],[hyp77]) ).
cnf(c_159,plain,
select(a_1370,i_1371) = e_1373,
inference(copy,[status(thm)],[c_158]) ).
fof(goal,axiom,
e_1372 != e_1373,
file('theBenchmark.p',goal) ).
cnf(c_162,plain,
e_1372 != e_1373,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_163,plain,
e_1373 != e_1372,
inference(copy,[status(thm)],[c_162]) ).
cnf(c_164,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_612,plain,
select(a_1302,i8) = e_1301,
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_169,plain,
e_1305 = e_1301,
inference(paramod,[status(thm)],[c_95,c_612]) ).
cnf(c_170,plain,
select(a_1302,i8) = e_1301,
inference(paramod,[status(thm)],[c_169,c_95]) ).
cnf(c_171,plain,
store(a_1304,i5,e_1301) = a_1306,
inference(paramod,[status(thm)],[c_169,c_15]) ).
cnf(c_613,plain,
select(a_1335,i8) = e_1295,
inference(paramod,[status(thm)],[c_47,c_1]) ).
cnf(c_188,plain,
e_1336 = e_1295,
inference(paramod,[status(thm)],[c_123,c_613]) ).
cnf(c_190,plain,
store(a_1335,i6,e_1295) = a_1337,
inference(paramod,[status(thm)],[c_188,c_49]) ).
cnf(c_614,plain,
select(a_1339,i8) = e_1338,
inference(paramod,[status(thm)],[c_51,c_1]) ).
cnf(c_191,plain,
e_1340 = e_1338,
inference(paramod,[status(thm)],[c_127,c_614]) ).
cnf(c_193,plain,
store(a_1339,i5,e_1338) = a_1341,
inference(paramod,[status(thm)],[c_191,c_53]) ).
cnf(c_615,plain,
store(store(a1,A,e_1295),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_616,plain,
store(store(a1,A,e_1295),i7,select(a1,A)) = store(store(a1,i7,select(a1,A)),A,e_1295),
inference(paramod,[status(thm)],[c_85,c_615]) ).
cnf(c_209,plain,
store(store(a1,i7,select(a1,A)),A,e_1295) = store(store(a1,A,e_1295),i7,select(a1,A)),
inference(copy,[status(thm)],[c_616]) ).
cnf(c_617,plain,
store(store(a_1302,A,e_1303),i5,select(a_1302,A)) = store(store(a_1302,i5,select(a_1302,A)),A,select(a_1302,i5)),
inference(paramod,[status(thm)],[c_93,c_3]) ).
cnf(c_618,plain,
store(store(a_1302,A,e_1303),i5,select(a_1302,A)) = store(store(a_1302,i5,select(a_1302,A)),A,e_1303),
inference(paramod,[status(thm)],[c_93,c_617]) ).
cnf(c_213,plain,
store(store(a_1302,i5,select(a_1302,A)),A,e_1303) = store(store(a_1302,A,e_1303),i5,select(a_1302,A)),
inference(copy,[status(thm)],[c_618]) ).
cnf(c_619,plain,
store(store(a_1310,A,e_1311),i1,select(a_1310,A)) = store(store(a_1310,i1,select(a_1310,A)),A,select(a_1310,i1)),
inference(paramod,[status(thm)],[c_101,c_3]) ).
cnf(c_620,plain,
store(store(a_1310,A,e_1311),i1,select(a_1310,A)) = store(store(a_1310,i1,select(a_1310,A)),A,e_1311),
inference(paramod,[status(thm)],[c_101,c_619]) ).
cnf(c_216,plain,
store(store(a_1310,i1,select(a_1310,A)),A,e_1311) = store(store(a_1310,A,e_1311),i1,select(a_1310,A)),
inference(copy,[status(thm)],[c_620]) ).
cnf(c_621,plain,
store(store(a_1321,A,e_1322),i2,select(a_1321,A)) = store(store(a_1321,i2,select(a_1321,A)),A,select(a_1321,i2)),
inference(paramod,[status(thm)],[c_111,c_3]) ).
cnf(c_622,plain,
store(store(a_1321,A,e_1322),i2,select(a_1321,A)) = store(store(a_1321,i2,select(a_1321,A)),A,e_1322),
inference(paramod,[status(thm)],[c_111,c_621]) ).
cnf(c_221,plain,
store(store(a_1321,i2,select(a_1321,A)),A,e_1322) = store(store(a_1321,A,e_1322),i2,select(a_1321,A)),
inference(copy,[status(thm)],[c_622]) ).
cnf(c_623,plain,
store(store(a_1329,A,e_1330),i5,select(a_1329,A)) = store(store(a_1329,i5,select(a_1329,A)),A,select(a_1329,i5)),
inference(paramod,[status(thm)],[c_119,c_3]) ).
cnf(c_624,plain,
store(store(a_1329,A,e_1330),i5,select(a_1329,A)) = store(store(a_1329,i5,select(a_1329,A)),A,e_1330),
inference(paramod,[status(thm)],[c_119,c_623]) ).
cnf(c_225,plain,
store(store(a_1329,i5,select(a_1329,A)),A,e_1330) = store(store(a_1329,A,e_1330),i5,select(a_1329,A)),
inference(copy,[status(thm)],[c_624]) ).
cnf(c_625,plain,
select(store(store(a1,A,e_1295),i7,select(a1,A)),A) = select(a1,i7),
inference(paramod,[status(thm)],[c_85,c_164]) ).
cnf(c_246,plain,
select(store(store(a1,A,e_1295),i7,select(a1,A)),A) = e_1295,
inference(paramod,[status(thm)],[c_85,c_625]) ).
cnf(c_626,plain,
select(store(a_1296,i7,select(a1,i8)),i8) = e_1295,
inference(paramod,[status(thm)],[c_5,c_246]) ).
cnf(c_627,plain,
select(store(a_1296,i7,e_1297),i8) = e_1295,
inference(paramod,[status(thm)],[c_87,c_626]) ).
cnf(c_628,plain,
select(a_1298,i8) = e_1295,
inference(paramod,[status(thm)],[c_7,c_627]) ).
cnf(c_371,plain,
e_1299 = e_1295,
inference(paramod,[status(thm)],[c_89,c_628]) ).
cnf(c_380,plain,
store(a_1298,i6,e_1295) = a_1300,
inference(paramod,[status(thm)],[c_371,c_9]) ).
cnf(c_629,plain,
store(store(a1,i7,select(a1,i8)),i8,e_1295) = store(a_1296,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_5,c_209]) ).
cnf(c_630,plain,
store(store(a1,i7,e_1297),i8,e_1295) = store(a_1296,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_87,c_629]) ).
cnf(c_631,plain,
store(a_1334,i8,e_1295) = store(a_1296,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_45,c_630]) ).
cnf(c_632,plain,
a_1335 = store(a_1296,i7,select(a1,i8)),
inference(paramod,[status(thm)],[c_47,c_631]) ).
cnf(c_633,plain,
a_1335 = store(a_1296,i7,e_1297),
inference(paramod,[status(thm)],[c_87,c_632]) ).
cnf(c_381,plain,
a_1335 = a_1298,
inference(paramod,[status(thm)],[c_7,c_633]) ).
cnf(c_634,plain,
store(a_1298,i6,e_1295) = a_1337,
inference(paramod,[status(thm)],[c_381,c_190]) ).
cnf(c_635,plain,
a_1300 = a_1337,
inference(paramod,[status(thm)],[c_380,c_634]) ).
cnf(c_384,plain,
a_1337 = a_1300,
inference(copy,[status(thm)],[c_635]) ).
cnf(c_636,plain,
select(a_1298,i6) = e_1338,
inference(paramod,[status(thm)],[c_381,c_125]) ).
cnf(c_637,plain,
e_1301 = e_1338,
inference(paramod,[status(thm)],[c_91,c_636]) ).
cnf(c_385,plain,
e_1338 = e_1301,
inference(copy,[status(thm)],[c_637]) ).
cnf(c_638,plain,
store(a_1300,i8,e_1338) = a_1339,
inference(paramod,[status(thm)],[c_384,c_51]) ).
cnf(c_639,plain,
store(a_1300,i8,e_1301) = a_1339,
inference(paramod,[status(thm)],[c_385,c_638]) ).
cnf(c_640,plain,
a_1302 = a_1339,
inference(paramod,[status(thm)],[c_11,c_639]) ).
cnf(c_387,plain,
a_1339 = a_1302,
inference(copy,[status(thm)],[c_640]) ).
cnf(c_641,plain,
store(a_1302,i5,e_1338) = a_1341,
inference(paramod,[status(thm)],[c_387,c_193]) ).
cnf(c_391,plain,
store(a_1302,i5,e_1301) = a_1341,
inference(paramod,[status(thm)],[c_385,c_641]) ).
cnf(c_642,plain,
select(a_1302,i5) = e_1342,
inference(paramod,[status(thm)],[c_387,c_129]) ).
cnf(c_643,plain,
e_1303 = e_1342,
inference(paramod,[status(thm)],[c_93,c_642]) ).
cnf(c_395,plain,
e_1342 = e_1303,
inference(copy,[status(thm)],[c_643]) ).
cnf(c_399,plain,
store(a_1341,i8,e_1303) = a_1343,
inference(paramod,[status(thm)],[c_395,c_55]) ).
cnf(c_644,plain,
store(store(a_1302,i5,select(a_1302,i8)),i8,e_1303) = store(a_1304,i5,select(a_1302,i8)),
inference(paramod,[status(thm)],[c_13,c_213]) ).
cnf(c_645,plain,
store(store(a_1302,i5,e_1301),i8,e_1303) = store(a_1304,i5,select(a_1302,i8)),
inference(paramod,[status(thm)],[c_170,c_644]) ).
cnf(c_646,plain,
store(a_1341,i8,e_1303) = store(a_1304,i5,select(a_1302,i8)),
inference(paramod,[status(thm)],[c_391,c_645]) ).
cnf(c_647,plain,
a_1343 = store(a_1304,i5,select(a_1302,i8)),
inference(paramod,[status(thm)],[c_399,c_646]) ).
cnf(c_648,plain,
a_1343 = store(a_1304,i5,e_1301),
inference(paramod,[status(thm)],[c_170,c_647]) ).
cnf(c_409,plain,
a_1343 = a_1306,
inference(paramod,[status(thm)],[c_171,c_648]) ).
cnf(c_649,plain,
select(a_1306,i4) = e_1346,
inference(paramod,[status(thm)],[c_409,c_133]) ).
cnf(c_650,plain,
e_1309 = e_1346,
inference(paramod,[status(thm)],[c_99,c_649]) ).
cnf(c_420,plain,
e_1346 = e_1309,
inference(copy,[status(thm)],[c_650]) ).
cnf(c_651,plain,
select(a_1306,i9) = e_1344,
inference(paramod,[status(thm)],[c_409,c_131]) ).
cnf(c_652,plain,
e_1307 = e_1344,
inference(paramod,[status(thm)],[c_97,c_651]) ).
cnf(c_421,plain,
e_1344 = e_1307,
inference(copy,[status(thm)],[c_652]) ).
cnf(c_653,plain,
store(a_1306,i4,e_1344) = a_1345,
inference(paramod,[status(thm)],[c_409,c_57]) ).
cnf(c_654,plain,
store(a_1306,i4,e_1307) = a_1345,
inference(paramod,[status(thm)],[c_421,c_653]) ).
cnf(c_655,plain,
a_1308 = a_1345,
inference(paramod,[status(thm)],[c_17,c_654]) ).
cnf(c_422,plain,
a_1345 = a_1308,
inference(copy,[status(thm)],[c_655]) ).
cnf(c_656,plain,
store(a_1308,i9,e_1346) = a_1347,
inference(paramod,[status(thm)],[c_422,c_59]) ).
cnf(c_657,plain,
store(a_1308,i9,e_1309) = a_1347,
inference(paramod,[status(thm)],[c_420,c_656]) ).
cnf(c_658,plain,
a_1310 = a_1347,
inference(paramod,[status(thm)],[c_19,c_657]) ).
cnf(c_426,plain,
a_1347 = a_1310,
inference(copy,[status(thm)],[c_658]) ).
cnf(c_659,plain,
select(a_1310,i1) = e_1350,
inference(paramod,[status(thm)],[c_426,c_137]) ).
cnf(c_660,plain,
e_1311 = e_1350,
inference(paramod,[status(thm)],[c_101,c_659]) ).
cnf(c_431,plain,
e_1350 = e_1311,
inference(copy,[status(thm)],[c_660]) ).
cnf(c_661,plain,
select(a_1310,i7) = e_1348,
inference(paramod,[status(thm)],[c_426,c_135]) ).
cnf(c_662,plain,
e_1313 = e_1348,
inference(paramod,[status(thm)],[c_103,c_661]) ).
cnf(c_432,plain,
e_1348 = e_1313,
inference(copy,[status(thm)],[c_662]) ).
cnf(c_663,plain,
store(a_1310,i1,e_1348) = a_1349,
inference(paramod,[status(thm)],[c_426,c_61]) ).
cnf(c_433,plain,
store(a_1310,i1,e_1313) = a_1349,
inference(paramod,[status(thm)],[c_432,c_663]) ).
cnf(c_437,plain,
store(a_1349,i7,e_1311) = a_1351,
inference(paramod,[status(thm)],[c_431,c_63]) ).
cnf(c_664,plain,
store(store(a_1310,i1,select(a_1310,i7)),i7,e_1311) = store(a_1312,i1,select(a_1310,i7)),
inference(paramod,[status(thm)],[c_21,c_216]) ).
cnf(c_665,plain,
store(store(a_1310,i1,e_1313),i7,e_1311) = store(a_1312,i1,select(a_1310,i7)),
inference(paramod,[status(thm)],[c_103,c_664]) ).
cnf(c_666,plain,
store(a_1349,i7,e_1311) = store(a_1312,i1,select(a_1310,i7)),
inference(paramod,[status(thm)],[c_433,c_665]) ).
cnf(c_667,plain,
a_1351 = store(a_1312,i1,select(a_1310,i7)),
inference(paramod,[status(thm)],[c_437,c_666]) ).
cnf(c_668,plain,
a_1351 = store(a_1312,i1,e_1313),
inference(paramod,[status(thm)],[c_103,c_667]) ).
cnf(c_457,plain,
a_1351 = a_1314,
inference(paramod,[status(thm)],[c_23,c_668]) ).
cnf(c_669,plain,
select(a_1314,i4) = e_1354,
inference(paramod,[status(thm)],[c_457,c_141]) ).
cnf(c_670,plain,
e_1317 = e_1354,
inference(paramod,[status(thm)],[c_107,c_669]) ).
cnf(c_469,plain,
e_1354 = e_1317,
inference(copy,[status(thm)],[c_670]) ).
cnf(c_671,plain,
select(a_1314,i5) = e_1352,
inference(paramod,[status(thm)],[c_457,c_139]) ).
cnf(c_672,plain,
e_1315 = e_1352,
inference(paramod,[status(thm)],[c_105,c_671]) ).
cnf(c_470,plain,
e_1352 = e_1315,
inference(copy,[status(thm)],[c_672]) ).
cnf(c_673,plain,
store(a_1314,i4,e_1352) = a_1353,
inference(paramod,[status(thm)],[c_457,c_65]) ).
cnf(c_674,plain,
store(a_1314,i4,e_1315) = a_1353,
inference(paramod,[status(thm)],[c_470,c_673]) ).
cnf(c_675,plain,
a_1316 = a_1353,
inference(paramod,[status(thm)],[c_25,c_674]) ).
cnf(c_471,plain,
a_1353 = a_1316,
inference(copy,[status(thm)],[c_675]) ).
cnf(c_676,plain,
store(a_1316,i5,e_1354) = a_1355,
inference(paramod,[status(thm)],[c_471,c_67]) ).
cnf(c_677,plain,
store(a_1316,i5,e_1317) = a_1355,
inference(paramod,[status(thm)],[c_469,c_676]) ).
cnf(c_678,plain,
a_1318 = a_1355,
inference(paramod,[status(thm)],[c_27,c_677]) ).
cnf(c_475,plain,
a_1355 = a_1318,
inference(copy,[status(thm)],[c_678]) ).
cnf(c_679,plain,
select(a_1318,i0) = e_1356,
inference(paramod,[status(thm)],[c_475,c_143]) ).
cnf(c_680,plain,
e_1319 = e_1356,
inference(paramod,[status(thm)],[c_109,c_679]) ).
cnf(c_478,plain,
e_1356 = e_1319,
inference(copy,[status(thm)],[c_680]) ).
cnf(c_681,plain,
store(a_1318,i0,e_1356) = a_1357,
inference(paramod,[status(thm)],[c_475,c_69]) ).
cnf(c_682,plain,
store(a_1318,i0,e_1319) = a_1357,
inference(paramod,[status(thm)],[c_478,c_681]) ).
cnf(c_683,plain,
a_1320 = a_1357,
inference(paramod,[status(thm)],[c_29,c_682]) ).
cnf(c_479,plain,
a_1357 = a_1320,
inference(copy,[status(thm)],[c_683]) ).
cnf(c_684,plain,
store(a_1320,i0,e_1356) = a_1358,
inference(paramod,[status(thm)],[c_479,c_71]) ).
cnf(c_685,plain,
store(a_1320,i0,e_1319) = a_1358,
inference(paramod,[status(thm)],[c_478,c_684]) ).
cnf(c_686,plain,
a_1321 = a_1358,
inference(paramod,[status(thm)],[c_31,c_685]) ).
cnf(c_483,plain,
a_1358 = a_1321,
inference(copy,[status(thm)],[c_686]) ).
cnf(c_687,plain,
select(a_1321,i2) = e_1361,
inference(paramod,[status(thm)],[c_483,c_147]) ).
cnf(c_688,plain,
e_1322 = e_1361,
inference(paramod,[status(thm)],[c_111,c_687]) ).
cnf(c_488,plain,
e_1361 = e_1322,
inference(copy,[status(thm)],[c_688]) ).
cnf(c_689,plain,
select(a_1321,i1) = e_1359,
inference(paramod,[status(thm)],[c_483,c_145]) ).
cnf(c_690,plain,
e_1324 = e_1359,
inference(paramod,[status(thm)],[c_113,c_689]) ).
cnf(c_489,plain,
e_1359 = e_1324,
inference(copy,[status(thm)],[c_690]) ).
cnf(c_691,plain,
store(a_1321,i2,e_1359) = a_1360,
inference(paramod,[status(thm)],[c_483,c_73]) ).
cnf(c_490,plain,
store(a_1321,i2,e_1324) = a_1360,
inference(paramod,[status(thm)],[c_489,c_691]) ).
cnf(c_494,plain,
store(a_1360,i1,e_1322) = a_1362,
inference(paramod,[status(thm)],[c_488,c_75]) ).
cnf(c_692,plain,
store(store(a_1321,i2,select(a_1321,i1)),i1,e_1322) = store(a_1323,i2,select(a_1321,i1)),
inference(paramod,[status(thm)],[c_33,c_221]) ).
cnf(c_693,plain,
store(store(a_1321,i2,e_1324),i1,e_1322) = store(a_1323,i2,select(a_1321,i1)),
inference(paramod,[status(thm)],[c_113,c_692]) ).
cnf(c_694,plain,
store(a_1360,i1,e_1322) = store(a_1323,i2,select(a_1321,i1)),
inference(paramod,[status(thm)],[c_490,c_693]) ).
cnf(c_695,plain,
a_1362 = store(a_1323,i2,select(a_1321,i1)),
inference(paramod,[status(thm)],[c_494,c_694]) ).
cnf(c_696,plain,
a_1362 = store(a_1323,i2,e_1324),
inference(paramod,[status(thm)],[c_113,c_695]) ).
cnf(c_538,plain,
a_1362 = a_1325,
inference(paramod,[status(thm)],[c_35,c_696]) ).
cnf(c_697,plain,
select(a_1325,i3) = e_1365,
inference(paramod,[status(thm)],[c_538,c_151]) ).
cnf(c_698,plain,
e_1328 = e_1365,
inference(paramod,[status(thm)],[c_117,c_697]) ).
cnf(c_549,plain,
e_1365 = e_1328,
inference(copy,[status(thm)],[c_698]) ).
cnf(c_699,plain,
select(a_1325,i0) = e_1363,
inference(paramod,[status(thm)],[c_538,c_149]) ).
cnf(c_700,plain,
e_1326 = e_1363,
inference(paramod,[status(thm)],[c_115,c_699]) ).
cnf(c_550,plain,
e_1363 = e_1326,
inference(copy,[status(thm)],[c_700]) ).
cnf(c_701,plain,
store(a_1325,i3,e_1363) = a_1364,
inference(paramod,[status(thm)],[c_538,c_77]) ).
cnf(c_702,plain,
store(a_1325,i3,e_1326) = a_1364,
inference(paramod,[status(thm)],[c_550,c_701]) ).
cnf(c_703,plain,
a_1327 = a_1364,
inference(paramod,[status(thm)],[c_37,c_702]) ).
cnf(c_551,plain,
a_1364 = a_1327,
inference(copy,[status(thm)],[c_703]) ).
cnf(c_704,plain,
store(a_1327,i0,e_1365) = a_1366,
inference(paramod,[status(thm)],[c_551,c_79]) ).
cnf(c_705,plain,
store(a_1327,i0,e_1328) = a_1366,
inference(paramod,[status(thm)],[c_549,c_704]) ).
cnf(c_706,plain,
a_1329 = a_1366,
inference(paramod,[status(thm)],[c_39,c_705]) ).
cnf(c_555,plain,
a_1366 = a_1329,
inference(copy,[status(thm)],[c_706]) ).
cnf(c_707,plain,
select(a_1329,i5) = e_1369,
inference(paramod,[status(thm)],[c_555,c_155]) ).
cnf(c_708,plain,
e_1330 = e_1369,
inference(paramod,[status(thm)],[c_119,c_707]) ).
cnf(c_560,plain,
e_1369 = e_1330,
inference(copy,[status(thm)],[c_708]) ).
cnf(c_709,plain,
select(a_1329,i9) = e_1367,
inference(paramod,[status(thm)],[c_555,c_153]) ).
cnf(c_710,plain,
e_1332 = e_1367,
inference(paramod,[status(thm)],[c_121,c_709]) ).
cnf(c_561,plain,
e_1367 = e_1332,
inference(copy,[status(thm)],[c_710]) ).
cnf(c_711,plain,
store(a_1329,i5,e_1367) = a_1368,
inference(paramod,[status(thm)],[c_555,c_81]) ).
cnf(c_562,plain,
store(a_1329,i5,e_1332) = a_1368,
inference(paramod,[status(thm)],[c_561,c_711]) ).
cnf(c_566,plain,
store(a_1368,i9,e_1330) = a_1370,
inference(paramod,[status(thm)],[c_560,c_83]) ).
cnf(c_712,plain,
store(store(a_1329,i5,select(a_1329,i9)),i9,e_1330) = store(a_1331,i5,select(a_1329,i9)),
inference(paramod,[status(thm)],[c_41,c_225]) ).
cnf(c_713,plain,
store(store(a_1329,i5,e_1332),i9,e_1330) = store(a_1331,i5,select(a_1329,i9)),
inference(paramod,[status(thm)],[c_121,c_712]) ).
cnf(c_714,plain,
store(a_1368,i9,e_1330) = store(a_1331,i5,select(a_1329,i9)),
inference(paramod,[status(thm)],[c_562,c_713]) ).
cnf(c_715,plain,
a_1370 = store(a_1331,i5,select(a_1329,i9)),
inference(paramod,[status(thm)],[c_566,c_714]) ).
cnf(c_716,plain,
a_1370 = store(a_1331,i5,e_1332),
inference(paramod,[status(thm)],[c_121,c_715]) ).
cnf(c_600,plain,
a_1370 = a_1333,
inference(paramod,[status(thm)],[c_43,c_716]) ).
cnf(c_717,plain,
select(a_1333,i_1371) = e_1373,
inference(paramod,[status(thm)],[c_600,c_159]) ).
cnf(c_718,plain,
e_1372 = e_1373,
inference(paramod,[status(thm)],[c_157,c_717]) ).
cnf(c_719,plain,
e_1373 = e_1372,
inference(copy,[status(thm)],[c_718]) ).
cnf(c_611,plain,
$false,
inference(resolve,[status(thm)],[c_163,c_719]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV547-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 14:25:41 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 1226092 was started by sandbox on n026,
% 0.12/0.36 % Sat Sep 26 14:25:41 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 11.43/1.82
% 11.43/1.82 % SZS status Unsatisfiable for theBenchmark
% 11.43/1.82
% 11.43/1.82 % Proof 1 at 1.30 (+ 0.03) seconds.
% 11.43/1.82 % Length of proof is 215.
% 11.43/1.82 % Level of proof is 31.
% 11.43/1.82 % Maximum clause weight is 43.000.
% 11.43/1.82 % Given clauses 232.
% 11.43/1.82
% 11.43/1.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------