%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:13:36 PM UTC 2026
% Result : Unsatisfiable 12.75s 2.28s
% Output : Proof 12.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 101
% Number of leaves : 79
% Syntax : Number of formulae : 604 ( 604 unt; 0 def)
% Number of atoms : 604 ( 603 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 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 : 57 ( 4 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f2,axiom,
store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f2_nnf,plain,
! [A,I,J] : store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,I,J] : store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t86,plain,
store(store(X1,X2,select(X1,X3)),X3,select(X1,X2)) = store(store(X1,X3,select(X1,X2)),X2,select(X1,X3)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t341,plain,
store(store(X1,X2,select(X1,X3)),X3,select(X1,X2)) = store(store(X1,X3,select(X1,X2)),X2,select(X1,X3)),
inference(orient,[status(thm)],[t86]) ).
cnf(f60,hypothesis,
e_1279 = select(a_1278,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).
fof(f60_nnf,plain,
e_1279 = select(a_1278,i5),
inference(nnf_transformation,[status(thm)],[f60]) ).
cnf(c60,plain,
e_1279 = select(a_1278,i5),
inference(cnf_transformation,[status(esa)],[f60_nnf]) ).
cnf(t23,plain,
select(a_1278,i5) = e_1279,
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(t110,plain,
select(a_1278,i5) = e_1279,
inference(orient,[status(thm)],[t23]) ).
cnf(t359,plain,
store(store(a_1278,i5,select(a_1278,X1)),X1,select(a_1278,i5)) = store(store(a_1278,X1,e_1279),i5,select(a_1278,X1)),
inference(cp,[status(thm)],[t341,t110]) ).
cnf(t1071,plain,
store(store(a_1278,i5,select(a_1278,X1)),X1,e_1279) = store(store(a_1278,X1,e_1279),i5,select(a_1278,X1)),
inference(step,[status(thm)],[t359,t110]) ).
cnf(t652,plain,
store(store(a_1278,i5,select(a_1278,X1)),X1,e_1279) = store(store(a_1278,X1,e_1279),i5,select(a_1278,X1)),
inference(orient,[status(thm)],[t1071]) ).
cnf(f61,hypothesis,
e_1281 = select(a_1278,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
fof(f61_nnf,plain,
e_1281 = select(a_1278,i9),
inference(nnf_transformation,[status(thm)],[f61]) ).
cnf(c61,plain,
e_1281 = select(a_1278,i9),
inference(cnf_transformation,[status(esa)],[f61_nnf]) ).
cnf(t24,plain,
select(a_1278,i9) = e_1281,
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(t111,plain,
select(a_1278,i9) = e_1281,
inference(orient,[status(thm)],[t24]) ).
cnf(t653,plain,
store(store(a_1278,i9,e_1279),i5,select(a_1278,i9)) = store(store(a_1278,i5,e_1281),i9,e_1279),
inference(cp,[status(thm)],[t652,t111]) ).
cnf(f21,hypothesis,
a_1280 = store(a_1278,i9,e_1279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f21_nnf,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
a_1280 = store(a_1278,i9,e_1279),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t61,plain,
store(a_1278,i9,e_1279) = a_1280,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t148,plain,
store(a_1278,i9,e_1279) = a_1280,
inference(orient,[status(thm)],[t61]) ).
cnf(t1072,plain,
store(a_1280,i5,select(a_1278,i9)) = store(store(a_1278,i5,e_1281),i9,e_1279),
inference(step,[status(thm)],[t653,t148]) ).
cnf(t1073,plain,
store(a_1280,i5,e_1281) = store(store(a_1278,i5,e_1281),i9,e_1279),
inference(step,[status(thm)],[t1072,t111]) ).
cnf(f22,hypothesis,
a_1282 = store(a_1280,i5,e_1281),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f22_nnf,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
a_1282 = store(a_1280,i5,e_1281),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(t62,plain,
store(a_1280,i5,e_1281) = a_1282,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t149,plain,
store(a_1280,i5,e_1281) = a_1282,
inference(orient,[status(thm)],[t62]) ).
cnf(t1074,plain,
a_1282 = store(store(a_1278,i5,e_1281),i9,e_1279),
inference(step,[status(thm)],[t1073,t149]) ).
cnf(t659,plain,
store(store(a_1278,i5,e_1281),i9,e_1279) = a_1282,
inference(orient,[status(thm)],[t1074]) ).
cnf(f20,hypothesis,
a_1278 = store(a_1276,i0,e_1277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f20_nnf,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
a_1278 = store(a_1276,i0,e_1277),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(t60,plain,
store(a_1276,i0,e_1277) = a_1278,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t147,plain,
store(a_1276,i0,e_1277) = a_1278,
inference(orient,[status(thm)],[t60]) ).
cnf(f59,hypothesis,
e_1277 = select(a_1274,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
fof(f59_nnf,plain,
e_1277 = select(a_1274,i3),
inference(nnf_transformation,[status(thm)],[f59]) ).
cnf(c59,plain,
e_1277 = select(a_1274,i3),
inference(cnf_transformation,[status(esa)],[f59_nnf]) ).
cnf(t22,plain,
select(a_1274,i3) = e_1277,
inference(equality_encoding,[status(esa)],[c59]) ).
cnf(t109,plain,
select(a_1274,i3) = e_1277,
inference(orient,[status(thm)],[t22]) ).
cnf(t869,plain,
select(a_1311,i3) = e_1277,
inference(rw,[status(thm)],[t109]) ).
cnf(f76,hypothesis,
e_1314 = select(a_1311,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp73) ).
fof(f76_nnf,plain,
e_1314 = select(a_1311,i3),
inference(nnf_transformation,[status(thm)],[f76]) ).
cnf(c76,plain,
e_1314 = select(a_1311,i3),
inference(cnf_transformation,[status(esa)],[f76_nnf]) ).
cnf(t39,plain,
select(a_1311,i3) = e_1314,
inference(equality_encoding,[status(esa)],[c76]) ).
cnf(t126,plain,
select(a_1311,i3) = e_1314,
inference(orient,[status(thm)],[t39]) ).
cnf(t1198,plain,
e_1314 = e_1277,
inference(step,[status(thm)],[t869,t126]) ).
cnf(t886,plain,
e_1277 = e_1314,
inference(orient,[status(thm)],[t1198]) ).
cnf(t1199,plain,
store(a_1276,i0,e_1314) = a_1278,
inference(step,[status(thm)],[t147,t886]) ).
cnf(t887,plain,
store(a_1276,i0,e_1314) = a_1278,
inference(rw,[status(thm)],[t1199]) ).
cnf(f19,hypothesis,
a_1276 = store(a_1274,i3,e_1275),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f19_nnf,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
a_1276 = store(a_1274,i3,e_1275),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(t59,plain,
store(a_1274,i3,e_1275) = a_1276,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t146,plain,
store(a_1274,i3,e_1275) = a_1276,
inference(orient,[status(thm)],[t59]) ).
cnf(f57,hypothesis,
e_1273 = select(a_1270,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
fof(f57_nnf,plain,
e_1273 = select(a_1270,i1),
inference(nnf_transformation,[status(thm)],[f57]) ).
cnf(c57,plain,
e_1273 = select(a_1270,i1),
inference(cnf_transformation,[status(esa)],[f57_nnf]) ).
cnf(t19,plain,
select(a_1270,i1) = e_1273,
inference(equality_encoding,[status(esa)],[c57]) ).
cnf(t106,plain,
select(a_1270,i1) = e_1273,
inference(orient,[status(thm)],[t19]) ).
cnf(t355,plain,
store(store(a_1270,i1,select(a_1270,X1)),X1,select(a_1270,i1)) = store(store(a_1270,X1,e_1273),i1,select(a_1270,X1)),
inference(cp,[status(thm)],[t341,t106]) ).
cnf(t1053,plain,
store(store(a_1270,i1,select(a_1270,X1)),X1,e_1273) = store(store(a_1270,X1,e_1273),i1,select(a_1270,X1)),
inference(step,[status(thm)],[t355,t106]) ).
cnf(t595,plain,
store(store(a_1270,i1,select(a_1270,X1)),X1,e_1273) = store(store(a_1270,X1,e_1273),i1,select(a_1270,X1)),
inference(orient,[status(thm)],[t1053]) ).
cnf(f56,hypothesis,
e_1271 = select(a_1270,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).
fof(f56_nnf,plain,
e_1271 = select(a_1270,i2),
inference(nnf_transformation,[status(thm)],[f56]) ).
cnf(c56,plain,
e_1271 = select(a_1270,i2),
inference(cnf_transformation,[status(esa)],[f56_nnf]) ).
cnf(t20,plain,
select(a_1270,i2) = e_1271,
inference(equality_encoding,[status(esa)],[c56]) ).
cnf(t107,plain,
select(a_1270,i2) = e_1271,
inference(orient,[status(thm)],[t20]) ).
cnf(t596,plain,
store(store(a_1270,i2,e_1273),i1,select(a_1270,i2)) = store(store(a_1270,i1,e_1271),i2,e_1273),
inference(cp,[status(thm)],[t595,t107]) ).
cnf(t1054,plain,
store(store(a_1270,i2,e_1273),i1,e_1271) = store(store(a_1270,i1,e_1271),i2,e_1273),
inference(step,[status(thm)],[t596,t107]) ).
cnf(f17,hypothesis,
a_1272 = store(a_1270,i1,e_1271),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f17_nnf,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
a_1272 = store(a_1270,i1,e_1271),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t57,plain,
store(a_1270,i1,e_1271) = a_1272,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t144,plain,
store(a_1270,i1,e_1271) = a_1272,
inference(orient,[status(thm)],[t57]) ).
cnf(t1055,plain,
store(store(a_1270,i2,e_1273),i1,e_1271) = store(a_1272,i2,e_1273),
inference(step,[status(thm)],[t1054,t144]) ).
cnf(f18,hypothesis,
a_1274 = store(a_1272,i2,e_1273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f18_nnf,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
a_1274 = store(a_1272,i2,e_1273),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(t58,plain,
store(a_1272,i2,e_1273) = a_1274,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t145,plain,
store(a_1272,i2,e_1273) = a_1274,
inference(orient,[status(thm)],[t58]) ).
cnf(t1056,plain,
store(store(a_1270,i2,e_1273),i1,e_1271) = a_1274,
inference(step,[status(thm)],[t1055,t145]) ).
cnf(t601,plain,
store(store(a_1270,i2,e_1273),i1,e_1271) = a_1274,
inference(orient,[status(thm)],[t1056]) ).
cnf(f16,hypothesis,
a_1270 = store(a_1269,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f16_nnf,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
a_1270 = store(a_1269,i0,e_1268),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t56,plain,
store(a_1269,i0,e_1268) = a_1270,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t143,plain,
store(a_1269,i0,e_1268) = a_1270,
inference(orient,[status(thm)],[t56]) ).
cnf(f55,hypothesis,
e_1268 = select(a_1267,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
fof(f55_nnf,plain,
e_1268 = select(a_1267,i0),
inference(nnf_transformation,[status(thm)],[f55]) ).
cnf(c55,plain,
e_1268 = select(a_1267,i0),
inference(cnf_transformation,[status(esa)],[f55_nnf]) ).
cnf(t18,plain,
select(a_1267,i0) = e_1268,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t105,plain,
select(a_1267,i0) = e_1268,
inference(orient,[status(thm)],[t18]) ).
cnf(t791,plain,
select(a_1304,i0) = e_1268,
inference(rw,[status(thm)],[t105]) ).
cnf(f72,hypothesis,
e_1305 = select(a_1304,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
fof(f72_nnf,plain,
e_1305 = select(a_1304,i0),
inference(nnf_transformation,[status(thm)],[f72]) ).
cnf(c72,plain,
e_1305 = select(a_1304,i0),
inference(cnf_transformation,[status(esa)],[f72_nnf]) ).
cnf(t35,plain,
select(a_1304,i0) = e_1305,
inference(equality_encoding,[status(esa)],[c72]) ).
cnf(t122,plain,
select(a_1304,i0) = e_1305,
inference(orient,[status(thm)],[t35]) ).
cnf(t1128,plain,
e_1305 = e_1268,
inference(step,[status(thm)],[t791,t122]) ).
cnf(t797,plain,
e_1268 = e_1305,
inference(orient,[status(thm)],[t1128]) ).
cnf(t1129,plain,
store(a_1269,i0,e_1305) = a_1270,
inference(step,[status(thm)],[t143,t797]) ).
cnf(t798,plain,
store(a_1269,i0,e_1305) = a_1270,
inference(rw,[status(thm)],[t1129]) ).
cnf(f15,hypothesis,
a_1269 = store(a_1267,i0,e_1268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f15_nnf,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
a_1269 = store(a_1267,i0,e_1268),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t55,plain,
store(a_1267,i0,e_1268) = a_1269,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t142,plain,
store(a_1267,i0,e_1268) = a_1269,
inference(orient,[status(thm)],[t55]) ).
cnf(f14,hypothesis,
a_1267 = store(a_1265,i5,e_1266),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f14_nnf,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
a_1267 = store(a_1265,i5,e_1266),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t54,plain,
store(a_1265,i5,e_1266) = a_1267,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t141,plain,
store(a_1265,i5,e_1266) = a_1267,
inference(orient,[status(thm)],[t54]) ).
cnf(f54,hypothesis,
e_1266 = select(a_1263,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f54_nnf,plain,
e_1266 = select(a_1263,i4),
inference(nnf_transformation,[status(thm)],[f54]) ).
cnf(c54,plain,
e_1266 = select(a_1263,i4),
inference(cnf_transformation,[status(esa)],[f54_nnf]) ).
cnf(t16,plain,
select(a_1263,i4) = e_1266,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t103,plain,
select(a_1263,i4) = e_1266,
inference(orient,[status(thm)],[t16]) ).
cnf(t760,plain,
select(a_1300,i4) = e_1266,
inference(rw,[status(thm)],[t103]) ).
cnf(f71,hypothesis,
e_1303 = select(a_1300,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp68) ).
fof(f71_nnf,plain,
e_1303 = select(a_1300,i4),
inference(nnf_transformation,[status(thm)],[f71]) ).
cnf(c71,plain,
e_1303 = select(a_1300,i4),
inference(cnf_transformation,[status(esa)],[f71_nnf]) ).
cnf(t33,plain,
select(a_1300,i4) = e_1303,
inference(equality_encoding,[status(esa)],[c71]) ).
cnf(t120,plain,
select(a_1300,i4) = e_1303,
inference(orient,[status(thm)],[t33]) ).
cnf(t1112,plain,
e_1303 = e_1266,
inference(step,[status(thm)],[t760,t120]) ).
cnf(t773,plain,
e_1266 = e_1303,
inference(orient,[status(thm)],[t1112]) ).
cnf(t1113,plain,
store(a_1265,i5,e_1303) = a_1267,
inference(step,[status(thm)],[t141,t773]) ).
cnf(t774,plain,
store(a_1265,i5,e_1303) = a_1267,
inference(rw,[status(thm)],[t1113]) ).
cnf(f13,hypothesis,
a_1265 = store(a_1263,i4,e_1264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f13_nnf,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
a_1265 = store(a_1263,i4,e_1264),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t53,plain,
store(a_1263,i4,e_1264) = a_1265,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t140,plain,
store(a_1263,i4,e_1264) = a_1265,
inference(orient,[status(thm)],[t53]) ).
cnf(f69,hypothesis,
e_1299 = select(a_1296,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).
fof(f69_nnf,plain,
e_1299 = select(a_1296,i1),
inference(nnf_transformation,[status(thm)],[f69]) ).
cnf(c69,plain,
e_1299 = select(a_1296,i1),
inference(cnf_transformation,[status(esa)],[f69_nnf]) ).
cnf(t31,plain,
select(a_1296,i1) = e_1299,
inference(equality_encoding,[status(esa)],[c69]) ).
cnf(t118,plain,
select(a_1296,i1) = e_1299,
inference(orient,[status(thm)],[t31]) ).
cnf(t367,plain,
store(store(a_1296,i1,select(a_1296,X1)),X1,select(a_1296,i1)) = store(store(a_1296,X1,e_1299),i1,select(a_1296,X1)),
inference(cp,[status(thm)],[t341,t118]) ).
cnf(t1099,plain,
store(store(a_1296,i1,select(a_1296,X1)),X1,e_1299) = store(store(a_1296,X1,e_1299),i1,select(a_1296,X1)),
inference(step,[status(thm)],[t367,t118]) ).
cnf(t752,plain,
store(store(a_1296,i1,select(a_1296,X1)),X1,e_1299) = store(store(a_1296,X1,e_1299),i1,select(a_1296,X1)),
inference(orient,[status(thm)],[t1099]) ).
cnf(f68,hypothesis,
e_1297 = select(a_1296,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
fof(f68_nnf,plain,
e_1297 = select(a_1296,i7),
inference(nnf_transformation,[status(thm)],[f68]) ).
cnf(c68,plain,
e_1297 = select(a_1296,i7),
inference(cnf_transformation,[status(esa)],[f68_nnf]) ).
cnf(t32,plain,
select(a_1296,i7) = e_1297,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(t119,plain,
select(a_1296,i7) = e_1297,
inference(orient,[status(thm)],[t32]) ).
cnf(t753,plain,
store(store(a_1296,i7,e_1299),i1,select(a_1296,i7)) = store(store(a_1296,i1,e_1297),i7,e_1299),
inference(cp,[status(thm)],[t752,t119]) ).
cnf(f11,hypothesis,
a_1261 = store(a_1259,i7,e_1260),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f11_nnf,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
a_1261 = store(a_1259,i7,e_1260),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t51,plain,
store(a_1259,i7,e_1260) = a_1261,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t138,plain,
store(a_1259,i7,e_1260) = a_1261,
inference(orient,[status(thm)],[t51]) ).
cnf(f10,hypothesis,
a_1259 = store(a_1257,i9,e_1258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f10_nnf,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
a_1259 = store(a_1257,i9,e_1258),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t50,plain,
store(a_1257,i9,e_1258) = a_1259,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t137,plain,
store(a_1257,i9,e_1258) = a_1259,
inference(orient,[status(thm)],[t50]) ).
cnf(f50,hypothesis,
e_1258 = select(a_1255,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f50_nnf,plain,
e_1258 = select(a_1255,i4),
inference(nnf_transformation,[status(thm)],[f50]) ).
cnf(c50,plain,
e_1258 = select(a_1255,i4),
inference(cnf_transformation,[status(esa)],[f50_nnf]) ).
cnf(t12,plain,
select(a_1255,i4) = e_1258,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t99,plain,
select(a_1255,i4) = e_1258,
inference(orient,[status(thm)],[t12]) ).
cnf(t522,plain,
select(a_1292,i4) = e_1258,
inference(rw,[status(thm)],[t99]) ).
cnf(f67,hypothesis,
e_1295 = select(a_1292,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).
fof(f67_nnf,plain,
e_1295 = select(a_1292,i4),
inference(nnf_transformation,[status(thm)],[f67]) ).
cnf(c67,plain,
e_1295 = select(a_1292,i4),
inference(cnf_transformation,[status(esa)],[f67_nnf]) ).
cnf(t29,plain,
select(a_1292,i4) = e_1295,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(t116,plain,
select(a_1292,i4) = e_1295,
inference(orient,[status(thm)],[t29]) ).
cnf(t1023,plain,
e_1295 = e_1258,
inference(step,[status(thm)],[t522,t116]) ).
cnf(t528,plain,
e_1258 = e_1295,
inference(orient,[status(thm)],[t1023]) ).
cnf(t1024,plain,
store(a_1257,i9,e_1295) = a_1259,
inference(step,[status(thm)],[t137,t528]) ).
cnf(t529,plain,
store(a_1257,i9,e_1295) = a_1259,
inference(rw,[status(thm)],[t1024]) ).
cnf(f9,hypothesis,
a_1257 = store(a_1255,i4,e_1256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f9_nnf,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
a_1257 = store(a_1255,i4,e_1256),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t49,plain,
store(a_1255,i4,e_1256) = a_1257,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t136,plain,
store(a_1255,i4,e_1256) = a_1257,
inference(orient,[status(thm)],[t49]) ).
cnf(f48,hypothesis,
e_1254 = select(a_1251,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f48_nnf,plain,
e_1254 = select(a_1251,i8),
inference(nnf_transformation,[status(thm)],[f48]) ).
cnf(c48,plain,
e_1254 = select(a_1251,i8),
inference(cnf_transformation,[status(esa)],[f48_nnf]) ).
cnf(t11,plain,
select(a_1251,i8) = e_1254,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t98,plain,
select(a_1251,i8) = e_1254,
inference(orient,[status(thm)],[t11]) ).
cnf(t347,plain,
store(store(a_1251,i8,select(a_1251,X1)),X1,select(a_1251,i8)) = store(store(a_1251,X1,e_1254),i8,select(a_1251,X1)),
inference(cp,[status(thm)],[t341,t98]) ).
cnf(f6,hypothesis,
a_1251 = store(a_1249,i8,e_1250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f6_nnf,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
a_1251 = store(a_1249,i8,e_1250),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t46,plain,
store(a_1249,i8,e_1250) = a_1251,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t133,plain,
store(a_1249,i8,e_1250) = a_1251,
inference(orient,[status(thm)],[t46]) ).
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f0_nnf,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t83,plain,
select(store(X1,X2,X3),X2) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t170,plain,
select(store(X1,X2,X3),X2) = X3,
inference(orient,[status(thm)],[t83]) ).
cnf(t175,plain,
e_1250 = select(a_1251,i8),
inference(cp,[status(thm)],[t170,t133]) ).
cnf(t960,plain,
e_1250 = e_1254,
inference(step,[status(thm)],[t175,t98]) ).
cnf(t211,plain,
e_1250 = e_1254,
inference(orient,[status(thm)],[t960]) ).
cnf(t963,plain,
store(a_1249,i8,e_1254) = a_1251,
inference(step,[status(thm)],[t133,t211]) ).
cnf(t214,plain,
store(a_1249,i8,e_1254) = a_1251,
inference(rw,[status(thm)],[t963]) ).
cnf(t449,plain,
store(a_1249,i8,e_1254) = a_1251,
inference(orient,[status(thm)],[t214]) ).
cnf(f46,hypothesis,
e_1250 = select(a_1247,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f46_nnf,plain,
e_1250 = select(a_1247,i6),
inference(nnf_transformation,[status(thm)],[f46]) ).
cnf(c46,plain,
e_1250 = select(a_1247,i6),
inference(cnf_transformation,[status(esa)],[f46_nnf]) ).
cnf(t8,plain,
select(a_1247,i6) = e_1250,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(t95,plain,
select(a_1247,i6) = e_1250,
inference(orient,[status(thm)],[t8]) ).
cnf(t961,plain,
select(a_1247,i6) = e_1254,
inference(step,[status(thm)],[t95,t211]) ).
cnf(t212,plain,
select(a_1247,i6) = e_1254,
inference(orient,[status(thm)],[t961]) ).
cnf(t467,plain,
select(a_1284,i6) = e_1254,
inference(rw,[status(thm)],[t212]) ).
cnf(f63,hypothesis,
e_1287 = select(a_1284,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).
fof(f63_nnf,plain,
e_1287 = select(a_1284,i6),
inference(nnf_transformation,[status(thm)],[f63]) ).
cnf(c63,plain,
e_1287 = select(a_1284,i6),
inference(cnf_transformation,[status(esa)],[f63_nnf]) ).
cnf(t25,plain,
select(a_1284,i6) = e_1287,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(t112,plain,
select(a_1284,i6) = e_1287,
inference(orient,[status(thm)],[t25]) ).
cnf(f26,hypothesis,
a_1288 = store(a_1286,i8,e_1287),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f26_nnf,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
a_1288 = store(a_1286,i8,e_1287),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t65,plain,
store(a_1286,i8,e_1287) = a_1288,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t152,plain,
store(a_1286,i8,e_1287) = a_1288,
inference(orient,[status(thm)],[t65]) ).
cnf(t194,plain,
e_1287 = select(a_1288,i8),
inference(cp,[status(thm)],[t170,t152]) ).
cnf(f64,hypothesis,
e_1289 = select(a_1288,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).
fof(f64_nnf,plain,
e_1289 = select(a_1288,i8),
inference(nnf_transformation,[status(thm)],[f64]) ).
cnf(c64,plain,
e_1289 = select(a_1288,i8),
inference(cnf_transformation,[status(esa)],[f64_nnf]) ).
cnf(t28,plain,
select(a_1288,i8) = e_1289,
inference(equality_encoding,[status(esa)],[c64]) ).
cnf(t115,plain,
select(a_1288,i8) = e_1289,
inference(orient,[status(thm)],[t28]) ).
cnf(t969,plain,
e_1287 = e_1289,
inference(step,[status(thm)],[t194,t115]) ).
cnf(t220,plain,
e_1287 = e_1289,
inference(orient,[status(thm)],[t969]) ).
cnf(t970,plain,
select(a_1284,i6) = e_1289,
inference(step,[status(thm)],[t112,t220]) ).
cnf(t221,plain,
select(a_1284,i6) = e_1289,
inference(orient,[status(thm)],[t970]) ).
cnf(t983,plain,
e_1289 = e_1254,
inference(step,[status(thm)],[t467,t221]) ).
cnf(t473,plain,
e_1254 = e_1289,
inference(orient,[status(thm)],[t983]) ).
cnf(t991,plain,
store(a_1249,i8,e_1289) = a_1251,
inference(step,[status(thm)],[t449,t473]) ).
cnf(t481,plain,
store(a_1249,i8,e_1289) = a_1251,
inference(rw,[status(thm)],[t991]) ).
cnf(f5,hypothesis,
a_1249 = store(a_1247,i6,e_1248),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f5_nnf,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
a_1249 = store(a_1247,i6,e_1248),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t45,plain,
store(a_1247,i6,e_1248) = a_1249,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t132,plain,
store(a_1247,i6,e_1248) = a_1249,
inference(orient,[status(thm)],[t45]) ).
cnf(f43,hypothesis,
e_1244 = select(a1,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f43_nnf,plain,
e_1244 = select(a1,i7),
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c43,plain,
e_1244 = select(a1,i7),
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(t6,plain,
select(a1,i7) = e_1244,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t93,plain,
select(a1,i7) = e_1244,
inference(orient,[status(thm)],[t6]) ).
cnf(f24,hypothesis,
a_1284 = store(a_1283,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f24_nnf,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
a_1284 = store(a_1283,i8,e_1244),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t63,plain,
store(a_1283,i8,e_1244) = a_1284,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t150,plain,
store(a_1283,i8,e_1244) = a_1284,
inference(orient,[status(thm)],[t63]) ).
cnf(t192,plain,
e_1244 = select(a_1284,i8),
inference(cp,[status(thm)],[t170,t150]) ).
cnf(f62,hypothesis,
e_1285 = select(a_1284,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).
fof(f62_nnf,plain,
e_1285 = select(a_1284,i8),
inference(nnf_transformation,[status(thm)],[f62]) ).
cnf(c62,plain,
e_1285 = select(a_1284,i8),
inference(cnf_transformation,[status(esa)],[f62_nnf]) ).
cnf(t26,plain,
select(a_1284,i8) = e_1285,
inference(equality_encoding,[status(esa)],[c62]) ).
cnf(t113,plain,
select(a_1284,i8) = e_1285,
inference(orient,[status(thm)],[t26]) ).
cnf(t964,plain,
e_1244 = e_1285,
inference(step,[status(thm)],[t192,t113]) ).
cnf(t215,plain,
e_1244 = e_1285,
inference(orient,[status(thm)],[t964]) ).
cnf(t965,plain,
select(a1,i7) = e_1285,
inference(step,[status(thm)],[t93,t215]) ).
cnf(t216,plain,
select(a1,i7) = e_1285,
inference(orient,[status(thm)],[t965]) ).
cnf(t342,plain,
store(store(a1,i7,select(a1,X1)),X1,select(a1,i7)) = store(store(a1,X1,e_1285),i7,select(a1,X1)),
inference(cp,[status(thm)],[t341,t216]) ).
cnf(t973,plain,
store(store(a1,i7,select(a1,X1)),X1,e_1285) = store(store(a1,X1,e_1285),i7,select(a1,X1)),
inference(step,[status(thm)],[t342,t216]) ).
cnf(t462,plain,
store(store(a1,i7,select(a1,X1)),X1,e_1285) = store(store(a1,X1,e_1285),i7,select(a1,X1)),
inference(orient,[status(thm)],[t973]) ).
cnf(f44,hypothesis,
e_1246 = select(a1,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f44_nnf,plain,
e_1246 = select(a1,i8),
inference(nnf_transformation,[status(thm)],[f44]) ).
cnf(c44,plain,
e_1246 = select(a1,i8),
inference(cnf_transformation,[status(esa)],[f44_nnf]) ).
cnf(t7,plain,
select(a1,i8) = e_1246,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(t94,plain,
select(a1,i8) = e_1246,
inference(orient,[status(thm)],[t7]) ).
cnf(t463,plain,
store(store(a1,i8,e_1285),i7,select(a1,i8)) = store(store(a1,i7,e_1246),i8,e_1285),
inference(cp,[status(thm)],[t462,t94]) ).
cnf(f3,hypothesis,
a_1245 = store(a1,i8,e_1244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f3_nnf,plain,
a_1245 = store(a1,i8,e_1244),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
a_1245 = store(a1,i8,e_1244),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(t43,plain,
store(a1,i8,e_1244) = a_1245,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t130,plain,
store(a1,i8,e_1244) = a_1245,
inference(orient,[status(thm)],[t43]) ).
cnf(t967,plain,
store(a1,i8,e_1285) = a_1245,
inference(step,[status(thm)],[t130,t215]) ).
cnf(t218,plain,
store(a1,i8,e_1285) = a_1245,
inference(rw,[status(thm)],[t967]) ).
cnf(t451,plain,
store(a1,i8,e_1285) = a_1245,
inference(orient,[status(thm)],[t218]) ).
cnf(t974,plain,
store(a_1245,i7,select(a1,i8)) = store(store(a1,i7,e_1246),i8,e_1285),
inference(step,[status(thm)],[t463,t451]) ).
cnf(t975,plain,
store(a_1245,i7,e_1246) = store(store(a1,i7,e_1246),i8,e_1285),
inference(step,[status(thm)],[t974,t94]) ).
cnf(f4,hypothesis,
a_1247 = store(a_1245,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f4_nnf,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
a_1247 = store(a_1245,i7,e_1246),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(t44,plain,
store(a_1245,i7,e_1246) = a_1247,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t131,plain,
store(a_1245,i7,e_1246) = a_1247,
inference(orient,[status(thm)],[t44]) ).
cnf(t976,plain,
a_1247 = store(store(a1,i7,e_1246),i8,e_1285),
inference(step,[status(thm)],[t975,t131]) ).
cnf(f23,hypothesis,
a_1283 = store(a1,i7,e_1246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f23_nnf,plain,
a_1283 = store(a1,i7,e_1246),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
a_1283 = store(a1,i7,e_1246),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(t42,plain,
store(a1,i7,e_1246) = a_1283,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t129,plain,
store(a1,i7,e_1246) = a_1283,
inference(orient,[status(thm)],[t42]) ).
cnf(t977,plain,
a_1247 = store(a_1283,i8,e_1285),
inference(step,[status(thm)],[t976,t129]) ).
cnf(t968,plain,
store(a_1283,i8,e_1285) = a_1284,
inference(step,[status(thm)],[t150,t215]) ).
cnf(t219,plain,
store(a_1283,i8,e_1285) = a_1284,
inference(rw,[status(thm)],[t968]) ).
cnf(t457,plain,
store(a_1283,i8,e_1285) = a_1284,
inference(orient,[status(thm)],[t219]) ).
cnf(t978,plain,
a_1247 = a_1284,
inference(step,[status(thm)],[t977,t457]) ).
cnf(t466,plain,
a_1247 = a_1284,
inference(orient,[status(thm)],[t978]) ).
cnf(t981,plain,
store(a_1284,i6,e_1248) = a_1249,
inference(step,[status(thm)],[t132,t466]) ).
cnf(t471,plain,
store(a_1284,i6,e_1248) = a_1249,
inference(rw,[status(thm)],[t981]) ).
cnf(f45,hypothesis,
e_1248 = select(a_1247,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f45_nnf,plain,
e_1248 = select(a_1247,i8),
inference(nnf_transformation,[status(thm)],[f45]) ).
cnf(c45,plain,
e_1248 = select(a_1247,i8),
inference(cnf_transformation,[status(esa)],[f45_nnf]) ).
cnf(t9,plain,
select(a_1247,i8) = e_1248,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t96,plain,
select(a_1247,i8) = e_1248,
inference(orient,[status(thm)],[t9]) ).
cnf(t468,plain,
select(a_1284,i8) = e_1248,
inference(rw,[status(thm)],[t96]) ).
cnf(t992,plain,
e_1285 = e_1248,
inference(step,[status(thm)],[t468,t113]) ).
cnf(t482,plain,
e_1248 = e_1285,
inference(orient,[status(thm)],[t992]) ).
cnf(t995,plain,
store(a_1284,i6,e_1285) = a_1249,
inference(step,[status(thm)],[t471,t482]) ).
cnf(f25,hypothesis,
a_1286 = store(a_1284,i6,e_1285),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f25_nnf,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
a_1286 = store(a_1284,i6,e_1285),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(t64,plain,
store(a_1284,i6,e_1285) = a_1286,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t151,plain,
store(a_1284,i6,e_1285) = a_1286,
inference(orient,[status(thm)],[t64]) ).
cnf(t996,plain,
a_1286 = a_1249,
inference(step,[status(thm)],[t995,t151]) ).
cnf(t488,plain,
a_1249 = a_1286,
inference(orient,[status(thm)],[t996]) ).
cnf(t997,plain,
store(a_1286,i8,e_1289) = a_1251,
inference(step,[status(thm)],[t481,t488]) ).
cnf(t972,plain,
store(a_1286,i8,e_1289) = a_1288,
inference(step,[status(thm)],[t152,t220]) ).
cnf(t223,plain,
store(a_1286,i8,e_1289) = a_1288,
inference(rw,[status(thm)],[t972]) ).
cnf(t459,plain,
store(a_1286,i8,e_1289) = a_1288,
inference(orient,[status(thm)],[t223]) ).
cnf(t998,plain,
a_1288 = a_1251,
inference(step,[status(thm)],[t997,t459]) ).
cnf(t492,plain,
a_1251 = a_1288,
inference(orient,[status(thm)],[t998]) ).
cnf(t1007,plain,
store(store(a_1288,i8,select(a_1251,X1)),X1,select(a_1251,i8)) = store(store(a_1251,X1,e_1254),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t347,t492]) ).
cnf(t1008,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,select(a_1251,i8)) = store(store(a_1251,X1,e_1254),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t1007,t492]) ).
cnf(t1009,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,select(a_1288,i8)) = store(store(a_1251,X1,e_1254),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t1008,t492]) ).
cnf(t1010,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,e_1289) = store(store(a_1251,X1,e_1254),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t1009,t115]) ).
cnf(t1011,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,e_1289) = store(store(a_1288,X1,e_1254),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t1010,t492]) ).
cnf(t1012,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,e_1289) = store(store(a_1288,X1,e_1289),i8,select(a_1251,X1)),
inference(step,[status(thm)],[t1011,t473]) ).
cnf(t1013,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,e_1289) = store(store(a_1288,X1,e_1289),i8,select(a_1288,X1)),
inference(step,[status(thm)],[t1012,t492]) ).
cnf(t516,plain,
store(store(a_1288,i8,select(a_1288,X1)),X1,e_1289) = store(store(a_1288,X1,e_1289),i8,select(a_1288,X1)),
inference(orient,[status(thm)],[t1013]) ).
cnf(f65,hypothesis,
e_1291 = select(a_1288,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).
fof(f65_nnf,plain,
e_1291 = select(a_1288,i5),
inference(nnf_transformation,[status(thm)],[f65]) ).
cnf(c65,plain,
e_1291 = select(a_1288,i5),
inference(cnf_transformation,[status(esa)],[f65_nnf]) ).
cnf(t27,plain,
select(a_1288,i5) = e_1291,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t114,plain,
select(a_1288,i5) = e_1291,
inference(orient,[status(thm)],[t27]) ).
cnf(t517,plain,
store(store(a_1288,i5,e_1289),i8,select(a_1288,i5)) = store(store(a_1288,i8,e_1291),i5,e_1289),
inference(cp,[status(thm)],[t516,t114]) ).
cnf(f27,hypothesis,
a_1290 = store(a_1288,i5,e_1289),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f27_nnf,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
a_1290 = store(a_1288,i5,e_1289),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(t66,plain,
store(a_1288,i5,e_1289) = a_1290,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t153,plain,
store(a_1288,i5,e_1289) = a_1290,
inference(orient,[status(thm)],[t66]) ).
cnf(t1014,plain,
store(a_1290,i8,select(a_1288,i5)) = store(store(a_1288,i8,e_1291),i5,e_1289),
inference(step,[status(thm)],[t517,t153]) ).
cnf(t1015,plain,
store(a_1290,i8,e_1291) = store(store(a_1288,i8,e_1291),i5,e_1289),
inference(step,[status(thm)],[t1014,t114]) ).
cnf(f28,hypothesis,
a_1292 = store(a_1290,i8,e_1291),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f28_nnf,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
a_1292 = store(a_1290,i8,e_1291),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(t67,plain,
store(a_1290,i8,e_1291) = a_1292,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t154,plain,
store(a_1290,i8,e_1291) = a_1292,
inference(orient,[status(thm)],[t67]) ).
cnf(t1016,plain,
a_1292 = store(store(a_1288,i8,e_1291),i5,e_1289),
inference(step,[status(thm)],[t1015,t154]) ).
cnf(f7,hypothesis,
a_1253 = store(a_1251,i8,e_1252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f7_nnf,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
a_1253 = store(a_1251,i8,e_1252),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t47,plain,
store(a_1251,i8,e_1252) = a_1253,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t134,plain,
store(a_1251,i8,e_1252) = a_1253,
inference(orient,[status(thm)],[t47]) ).
cnf(t999,plain,
store(a_1288,i8,e_1252) = a_1253,
inference(step,[status(thm)],[t134,t492]) ).
cnf(t495,plain,
store(a_1288,i8,e_1252) = a_1253,
inference(rw,[status(thm)],[t999]) ).
cnf(f47,hypothesis,
e_1252 = select(a_1251,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f47_nnf,plain,
e_1252 = select(a_1251,i5),
inference(nnf_transformation,[status(thm)],[f47]) ).
cnf(c47,plain,
e_1252 = select(a_1251,i5),
inference(cnf_transformation,[status(esa)],[f47_nnf]) ).
cnf(t10,plain,
select(a_1251,i5) = e_1252,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t97,plain,
select(a_1251,i5) = e_1252,
inference(orient,[status(thm)],[t10]) ).
cnf(t493,plain,
select(a_1288,i5) = e_1252,
inference(rw,[status(thm)],[t97]) ).
cnf(t1000,plain,
e_1291 = e_1252,
inference(step,[status(thm)],[t493,t114]) ).
cnf(t496,plain,
e_1252 = e_1291,
inference(orient,[status(thm)],[t1000]) ).
cnf(t1004,plain,
store(a_1288,i8,e_1291) = a_1253,
inference(step,[status(thm)],[t495,t496]) ).
cnf(t504,plain,
store(a_1288,i8,e_1291) = a_1253,
inference(orient,[status(thm)],[t1004]) ).
cnf(t1017,plain,
a_1292 = store(a_1253,i5,e_1289),
inference(step,[status(thm)],[t1016,t504]) ).
cnf(f8,hypothesis,
a_1255 = store(a_1253,i5,e_1254),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f8_nnf,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
a_1255 = store(a_1253,i5,e_1254),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t48,plain,
store(a_1253,i5,e_1254) = a_1255,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t135,plain,
store(a_1253,i5,e_1254) = a_1255,
inference(orient,[status(thm)],[t48]) ).
cnf(t986,plain,
store(a_1253,i5,e_1289) = a_1255,
inference(step,[status(thm)],[t135,t473]) ).
cnf(t476,plain,
store(a_1253,i5,e_1289) = a_1255,
inference(rw,[status(thm)],[t986]) ).
cnf(t490,plain,
store(a_1253,i5,e_1289) = a_1255,
inference(orient,[status(thm)],[t476]) ).
cnf(t1018,plain,
a_1292 = a_1255,
inference(step,[status(thm)],[t1017,t490]) ).
cnf(t521,plain,
a_1255 = a_1292,
inference(orient,[status(thm)],[t1018]) ).
cnf(t1019,plain,
store(a_1292,i4,e_1256) = a_1257,
inference(step,[status(thm)],[t136,t521]) ).
cnf(t524,plain,
store(a_1292,i4,e_1256) = a_1257,
inference(rw,[status(thm)],[t1019]) ).
cnf(f49,hypothesis,
e_1256 = select(a_1255,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f49_nnf,plain,
e_1256 = select(a_1255,i9),
inference(nnf_transformation,[status(thm)],[f49]) ).
cnf(c49,plain,
e_1256 = select(a_1255,i9),
inference(cnf_transformation,[status(esa)],[f49_nnf]) ).
cnf(t13,plain,
select(a_1255,i9) = e_1256,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t100,plain,
select(a_1255,i9) = e_1256,
inference(orient,[status(thm)],[t13]) ).
cnf(t523,plain,
select(a_1292,i9) = e_1256,
inference(rw,[status(thm)],[t100]) ).
cnf(f66,hypothesis,
e_1293 = select(a_1292,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).
fof(f66_nnf,plain,
e_1293 = select(a_1292,i9),
inference(nnf_transformation,[status(thm)],[f66]) ).
cnf(c66,plain,
e_1293 = select(a_1292,i9),
inference(cnf_transformation,[status(esa)],[f66_nnf]) ).
cnf(t30,plain,
select(a_1292,i9) = e_1293,
inference(equality_encoding,[status(esa)],[c66]) ).
cnf(t117,plain,
select(a_1292,i9) = e_1293,
inference(orient,[status(thm)],[t30]) ).
cnf(t1027,plain,
e_1293 = e_1256,
inference(step,[status(thm)],[t523,t117]) ).
cnf(t532,plain,
e_1256 = e_1293,
inference(orient,[status(thm)],[t1027]) ).
cnf(t1030,plain,
store(a_1292,i4,e_1293) = a_1257,
inference(step,[status(thm)],[t524,t532]) ).
cnf(f29,hypothesis,
a_1294 = store(a_1292,i4,e_1293),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f29_nnf,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
a_1294 = store(a_1292,i4,e_1293),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(t68,plain,
store(a_1292,i4,e_1293) = a_1294,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t155,plain,
store(a_1292,i4,e_1293) = a_1294,
inference(orient,[status(thm)],[t68]) ).
cnf(t1031,plain,
a_1294 = a_1257,
inference(step,[status(thm)],[t1030,t155]) ).
cnf(t540,plain,
a_1257 = a_1294,
inference(orient,[status(thm)],[t1031]) ).
cnf(t1032,plain,
store(a_1294,i9,e_1295) = a_1259,
inference(step,[status(thm)],[t529,t540]) ).
cnf(f30,hypothesis,
a_1296 = store(a_1294,i9,e_1295),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f30_nnf,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
a_1296 = store(a_1294,i9,e_1295),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(t69,plain,
store(a_1294,i9,e_1295) = a_1296,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t156,plain,
store(a_1294,i9,e_1295) = a_1296,
inference(orient,[status(thm)],[t69]) ).
cnf(t1033,plain,
a_1296 = a_1259,
inference(step,[status(thm)],[t1032,t156]) ).
cnf(t542,plain,
a_1259 = a_1296,
inference(orient,[status(thm)],[t1033]) ).
cnf(t1034,plain,
store(a_1296,i7,e_1260) = a_1261,
inference(step,[status(thm)],[t138,t542]) ).
cnf(t545,plain,
store(a_1296,i7,e_1260) = a_1261,
inference(rw,[status(thm)],[t1034]) ).
cnf(f51,hypothesis,
e_1260 = select(a_1259,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f51_nnf,plain,
e_1260 = select(a_1259,i1),
inference(nnf_transformation,[status(thm)],[f51]) ).
cnf(c51,plain,
e_1260 = select(a_1259,i1),
inference(cnf_transformation,[status(esa)],[f51_nnf]) ).
cnf(t14,plain,
select(a_1259,i1) = e_1260,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t101,plain,
select(a_1259,i1) = e_1260,
inference(orient,[status(thm)],[t14]) ).
cnf(t543,plain,
select(a_1296,i1) = e_1260,
inference(rw,[status(thm)],[t101]) ).
cnf(t1035,plain,
e_1299 = e_1260,
inference(step,[status(thm)],[t543,t118]) ).
cnf(t547,plain,
e_1260 = e_1299,
inference(orient,[status(thm)],[t1035]) ).
cnf(t1042,plain,
store(a_1296,i7,e_1299) = a_1261,
inference(step,[status(thm)],[t545,t547]) ).
cnf(t554,plain,
store(a_1296,i7,e_1299) = a_1261,
inference(orient,[status(thm)],[t1042]) ).
cnf(t1100,plain,
store(a_1261,i1,select(a_1296,i7)) = store(store(a_1296,i1,e_1297),i7,e_1299),
inference(step,[status(thm)],[t753,t554]) ).
cnf(t1101,plain,
store(a_1261,i1,e_1297) = store(store(a_1296,i1,e_1297),i7,e_1299),
inference(step,[status(thm)],[t1100,t119]) ).
cnf(f12,hypothesis,
a_1263 = store(a_1261,i1,e_1262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f12_nnf,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
a_1263 = store(a_1261,i1,e_1262),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t52,plain,
store(a_1261,i1,e_1262) = a_1263,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t139,plain,
store(a_1261,i1,e_1262) = a_1263,
inference(orient,[status(thm)],[t52]) ).
cnf(f52,hypothesis,
e_1262 = select(a_1259,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f52_nnf,plain,
e_1262 = select(a_1259,i7),
inference(nnf_transformation,[status(thm)],[f52]) ).
cnf(c52,plain,
e_1262 = select(a_1259,i7),
inference(cnf_transformation,[status(esa)],[f52_nnf]) ).
cnf(t15,plain,
select(a_1259,i7) = e_1262,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t102,plain,
select(a_1259,i7) = e_1262,
inference(orient,[status(thm)],[t15]) ).
cnf(t544,plain,
select(a_1296,i7) = e_1262,
inference(rw,[status(thm)],[t102]) ).
cnf(t1038,plain,
e_1297 = e_1262,
inference(step,[status(thm)],[t544,t119]) ).
cnf(t550,plain,
e_1262 = e_1297,
inference(orient,[status(thm)],[t1038]) ).
cnf(t1039,plain,
store(a_1261,i1,e_1297) = a_1263,
inference(step,[status(thm)],[t139,t550]) ).
cnf(t551,plain,
store(a_1261,i1,e_1297) = a_1263,
inference(rw,[status(thm)],[t1039]) ).
cnf(t556,plain,
store(a_1261,i1,e_1297) = a_1263,
inference(orient,[status(thm)],[t551]) ).
cnf(t1102,plain,
a_1263 = store(store(a_1296,i1,e_1297),i7,e_1299),
inference(step,[status(thm)],[t1101,t556]) ).
cnf(f31,hypothesis,
a_1298 = store(a_1296,i1,e_1297),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f31_nnf,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
a_1298 = store(a_1296,i1,e_1297),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t70,plain,
store(a_1296,i1,e_1297) = a_1298,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t157,plain,
store(a_1296,i1,e_1297) = a_1298,
inference(orient,[status(thm)],[t70]) ).
cnf(t1103,plain,
a_1263 = store(a_1298,i7,e_1299),
inference(step,[status(thm)],[t1102,t157]) ).
cnf(f32,hypothesis,
a_1300 = store(a_1298,i7,e_1299),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f32_nnf,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
a_1300 = store(a_1298,i7,e_1299),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t71,plain,
store(a_1298,i7,e_1299) = a_1300,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t158,plain,
store(a_1298,i7,e_1299) = a_1300,
inference(orient,[status(thm)],[t71]) ).
cnf(t1104,plain,
a_1263 = a_1300,
inference(step,[status(thm)],[t1103,t158]) ).
cnf(t759,plain,
a_1263 = a_1300,
inference(orient,[status(thm)],[t1104]) ).
cnf(t1105,plain,
store(a_1300,i4,e_1264) = a_1265,
inference(step,[status(thm)],[t140,t759]) ).
cnf(t762,plain,
store(a_1300,i4,e_1264) = a_1265,
inference(rw,[status(thm)],[t1105]) ).
cnf(f53,hypothesis,
e_1264 = select(a_1263,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
fof(f53_nnf,plain,
e_1264 = select(a_1263,i5),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
e_1264 = select(a_1263,i5),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(t17,plain,
select(a_1263,i5) = e_1264,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t104,plain,
select(a_1263,i5) = e_1264,
inference(orient,[status(thm)],[t17]) ).
cnf(t761,plain,
select(a_1300,i5) = e_1264,
inference(rw,[status(thm)],[t104]) ).
cnf(f70,hypothesis,
e_1301 = select(a_1300,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
fof(f70_nnf,plain,
e_1301 = select(a_1300,i5),
inference(nnf_transformation,[status(thm)],[f70]) ).
cnf(c70,plain,
e_1301 = select(a_1300,i5),
inference(cnf_transformation,[status(esa)],[f70_nnf]) ).
cnf(t34,plain,
select(a_1300,i5) = e_1301,
inference(equality_encoding,[status(esa)],[c70]) ).
cnf(t121,plain,
select(a_1300,i5) = e_1301,
inference(orient,[status(thm)],[t34]) ).
cnf(t1116,plain,
e_1301 = e_1264,
inference(step,[status(thm)],[t761,t121]) ).
cnf(t779,plain,
e_1264 = e_1301,
inference(orient,[status(thm)],[t1116]) ).
cnf(t1121,plain,
store(a_1300,i4,e_1301) = a_1265,
inference(step,[status(thm)],[t762,t779]) ).
cnf(f33,hypothesis,
a_1302 = store(a_1300,i4,e_1301),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f33_nnf,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
a_1302 = store(a_1300,i4,e_1301),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(t72,plain,
store(a_1300,i4,e_1301) = a_1302,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t159,plain,
store(a_1300,i4,e_1301) = a_1302,
inference(orient,[status(thm)],[t72]) ).
cnf(t1122,plain,
a_1302 = a_1265,
inference(step,[status(thm)],[t1121,t159]) ).
cnf(t788,plain,
a_1265 = a_1302,
inference(orient,[status(thm)],[t1122]) ).
cnf(t1123,plain,
store(a_1302,i5,e_1303) = a_1267,
inference(step,[status(thm)],[t774,t788]) ).
cnf(f34,hypothesis,
a_1304 = store(a_1302,i5,e_1303),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f34_nnf,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
a_1304 = store(a_1302,i5,e_1303),
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(t73,plain,
store(a_1302,i5,e_1303) = a_1304,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t160,plain,
store(a_1302,i5,e_1303) = a_1304,
inference(orient,[status(thm)],[t73]) ).
cnf(t1124,plain,
a_1304 = a_1267,
inference(step,[status(thm)],[t1123,t160]) ).
cnf(t790,plain,
a_1267 = a_1304,
inference(orient,[status(thm)],[t1124]) ).
cnf(t1125,plain,
store(a_1304,i0,e_1268) = a_1269,
inference(step,[status(thm)],[t142,t790]) ).
cnf(t792,plain,
store(a_1304,i0,e_1268) = a_1269,
inference(rw,[status(thm)],[t1125]) ).
cnf(t1134,plain,
store(a_1304,i0,e_1305) = a_1269,
inference(step,[status(thm)],[t792,t797]) ).
cnf(f35,hypothesis,
a_1306 = store(a_1304,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f35_nnf,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
a_1306 = store(a_1304,i0,e_1305),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(t74,plain,
store(a_1304,i0,e_1305) = a_1306,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t161,plain,
store(a_1304,i0,e_1305) = a_1306,
inference(orient,[status(thm)],[t74]) ).
cnf(t1135,plain,
a_1306 = a_1269,
inference(step,[status(thm)],[t1134,t161]) ).
cnf(t808,plain,
a_1269 = a_1306,
inference(orient,[status(thm)],[t1135]) ).
cnf(t1136,plain,
store(a_1306,i0,e_1305) = a_1270,
inference(step,[status(thm)],[t798,t808]) ).
cnf(f36,hypothesis,
a_1307 = store(a_1306,i0,e_1305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f36_nnf,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c36,plain,
a_1307 = store(a_1306,i0,e_1305),
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(t75,plain,
store(a_1306,i0,e_1305) = a_1307,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t162,plain,
store(a_1306,i0,e_1305) = a_1307,
inference(orient,[status(thm)],[t75]) ).
cnf(t1137,plain,
a_1307 = a_1270,
inference(step,[status(thm)],[t1136,t162]) ).
cnf(t812,plain,
a_1270 = a_1307,
inference(orient,[status(thm)],[t1137]) ).
cnf(t1139,plain,
store(store(a_1307,i2,e_1273),i1,e_1271) = a_1274,
inference(step,[status(thm)],[t601,t812]) ).
cnf(t818,plain,
store(store(a_1307,i2,e_1273),i1,e_1271) = a_1274,
inference(rw,[status(thm)],[t1139]) ).
cnf(t813,plain,
select(a_1307,i1) = e_1273,
inference(rw,[status(thm)],[t106]) ).
cnf(f73,hypothesis,
e_1308 = select(a_1307,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).
fof(f73_nnf,plain,
e_1308 = select(a_1307,i1),
inference(nnf_transformation,[status(thm)],[f73]) ).
cnf(c73,plain,
e_1308 = select(a_1307,i1),
inference(cnf_transformation,[status(esa)],[f73_nnf]) ).
cnf(t36,plain,
select(a_1307,i1) = e_1308,
inference(equality_encoding,[status(esa)],[c73]) ).
cnf(t123,plain,
select(a_1307,i1) = e_1308,
inference(orient,[status(thm)],[t36]) ).
cnf(t1142,plain,
e_1308 = e_1273,
inference(step,[status(thm)],[t813,t123]) ).
cnf(t822,plain,
e_1273 = e_1308,
inference(orient,[status(thm)],[t1142]) ).
cnf(t1183,plain,
store(store(a_1307,i2,e_1308),i1,e_1271) = a_1274,
inference(step,[status(thm)],[t818,t822]) ).
cnf(f37,hypothesis,
a_1309 = store(a_1307,i2,e_1308),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f37_nnf,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(nnf_transformation,[status(thm)],[f37]) ).
cnf(c37,plain,
a_1309 = store(a_1307,i2,e_1308),
inference(cnf_transformation,[status(esa)],[f37_nnf]) ).
cnf(t76,plain,
store(a_1307,i2,e_1308) = a_1309,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t163,plain,
store(a_1307,i2,e_1308) = a_1309,
inference(orient,[status(thm)],[t76]) ).
cnf(t1184,plain,
store(a_1309,i1,e_1271) = a_1274,
inference(step,[status(thm)],[t1183,t163]) ).
cnf(t814,plain,
select(a_1307,i2) = e_1271,
inference(rw,[status(thm)],[t107]) ).
cnf(f74,hypothesis,
e_1310 = select(a_1307,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp71) ).
fof(f74_nnf,plain,
e_1310 = select(a_1307,i2),
inference(nnf_transformation,[status(thm)],[f74]) ).
cnf(c74,plain,
e_1310 = select(a_1307,i2),
inference(cnf_transformation,[status(esa)],[f74_nnf]) ).
cnf(t37,plain,
select(a_1307,i2) = e_1310,
inference(equality_encoding,[status(esa)],[c74]) ).
cnf(t124,plain,
select(a_1307,i2) = e_1310,
inference(orient,[status(thm)],[t37]) ).
cnf(t1146,plain,
e_1310 = e_1271,
inference(step,[status(thm)],[t814,t124]) ).
cnf(t828,plain,
e_1271 = e_1310,
inference(orient,[status(thm)],[t1146]) ).
cnf(t1185,plain,
store(a_1309,i1,e_1310) = a_1274,
inference(step,[status(thm)],[t1184,t828]) ).
cnf(f38,hypothesis,
a_1311 = store(a_1309,i1,e_1310),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f38_nnf,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
a_1311 = store(a_1309,i1,e_1310),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
cnf(t77,plain,
store(a_1309,i1,e_1310) = a_1311,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t164,plain,
store(a_1309,i1,e_1310) = a_1311,
inference(orient,[status(thm)],[t77]) ).
cnf(t1186,plain,
a_1311 = a_1274,
inference(step,[status(thm)],[t1185,t164]) ).
cnf(t867,plain,
a_1274 = a_1311,
inference(orient,[status(thm)],[t1186]) ).
cnf(t1187,plain,
store(a_1311,i3,e_1275) = a_1276,
inference(step,[status(thm)],[t146,t867]) ).
cnf(t870,plain,
store(a_1311,i3,e_1275) = a_1276,
inference(rw,[status(thm)],[t1187]) ).
cnf(f58,hypothesis,
e_1275 = select(a_1274,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp55) ).
fof(f58_nnf,plain,
e_1275 = select(a_1274,i0),
inference(nnf_transformation,[status(thm)],[f58]) ).
cnf(c58,plain,
e_1275 = select(a_1274,i0),
inference(cnf_transformation,[status(esa)],[f58_nnf]) ).
cnf(t21,plain,
select(a_1274,i0) = e_1275,
inference(equality_encoding,[status(esa)],[c58]) ).
cnf(t108,plain,
select(a_1274,i0) = e_1275,
inference(orient,[status(thm)],[t21]) ).
cnf(t868,plain,
select(a_1311,i0) = e_1275,
inference(rw,[status(thm)],[t108]) ).
cnf(f75,hypothesis,
e_1312 = select(a_1311,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f75_nnf,plain,
e_1312 = select(a_1311,i0),
inference(nnf_transformation,[status(thm)],[f75]) ).
cnf(c75,plain,
e_1312 = select(a_1311,i0),
inference(cnf_transformation,[status(esa)],[f75_nnf]) ).
cnf(t38,plain,
select(a_1311,i0) = e_1312,
inference(equality_encoding,[status(esa)],[c75]) ).
cnf(t125,plain,
select(a_1311,i0) = e_1312,
inference(orient,[status(thm)],[t38]) ).
cnf(t1193,plain,
e_1312 = e_1275,
inference(step,[status(thm)],[t868,t125]) ).
cnf(t879,plain,
e_1275 = e_1312,
inference(orient,[status(thm)],[t1193]) ).
cnf(t1202,plain,
store(a_1311,i3,e_1312) = a_1276,
inference(step,[status(thm)],[t870,t879]) ).
cnf(f39,hypothesis,
a_1313 = store(a_1311,i3,e_1312),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f39_nnf,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c39,plain,
a_1313 = store(a_1311,i3,e_1312),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(t78,plain,
store(a_1311,i3,e_1312) = a_1313,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t165,plain,
store(a_1311,i3,e_1312) = a_1313,
inference(orient,[status(thm)],[t78]) ).
cnf(t1203,plain,
a_1313 = a_1276,
inference(step,[status(thm)],[t1202,t165]) ).
cnf(t897,plain,
a_1276 = a_1313,
inference(orient,[status(thm)],[t1203]) ).
cnf(t1204,plain,
store(a_1313,i0,e_1314) = a_1278,
inference(step,[status(thm)],[t887,t897]) ).
cnf(f40,hypothesis,
a_1315 = store(a_1313,i0,e_1314),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f40_nnf,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
a_1315 = store(a_1313,i0,e_1314),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(t79,plain,
store(a_1313,i0,e_1314) = a_1315,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t166,plain,
store(a_1313,i0,e_1314) = a_1315,
inference(orient,[status(thm)],[t79]) ).
cnf(t1205,plain,
a_1315 = a_1278,
inference(step,[status(thm)],[t1204,t166]) ).
cnf(t899,plain,
a_1278 = a_1315,
inference(orient,[status(thm)],[t1205]) ).
cnf(t1208,plain,
store(store(a_1315,i5,e_1281),i9,e_1279) = a_1282,
inference(step,[status(thm)],[t659,t899]) ).
cnf(t906,plain,
store(store(a_1315,i5,e_1281),i9,e_1279) = a_1282,
inference(rw,[status(thm)],[t1208]) ).
cnf(t901,plain,
select(a_1315,i9) = e_1281,
inference(rw,[status(thm)],[t111]) ).
cnf(f77,hypothesis,
e_1316 = select(a_1315,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp74) ).
fof(f77_nnf,plain,
e_1316 = select(a_1315,i9),
inference(nnf_transformation,[status(thm)],[f77]) ).
cnf(c77,plain,
e_1316 = select(a_1315,i9),
inference(cnf_transformation,[status(esa)],[f77_nnf]) ).
cnf(t41,plain,
select(a_1315,i9) = e_1316,
inference(equality_encoding,[status(esa)],[c77]) ).
cnf(t128,plain,
select(a_1315,i9) = e_1316,
inference(orient,[status(thm)],[t41]) ).
cnf(t1215,plain,
e_1316 = e_1281,
inference(step,[status(thm)],[t901,t128]) ).
cnf(t914,plain,
e_1281 = e_1316,
inference(orient,[status(thm)],[t1215]) ).
cnf(t1263,plain,
store(store(a_1315,i5,e_1316),i9,e_1279) = a_1282,
inference(step,[status(thm)],[t906,t914]) ).
cnf(f41,hypothesis,
a_1317 = store(a_1315,i5,e_1316),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f41_nnf,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
a_1317 = store(a_1315,i5,e_1316),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(t80,plain,
store(a_1315,i5,e_1316) = a_1317,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t167,plain,
store(a_1315,i5,e_1316) = a_1317,
inference(orient,[status(thm)],[t80]) ).
cnf(t1264,plain,
store(a_1317,i9,e_1279) = a_1282,
inference(step,[status(thm)],[t1263,t167]) ).
cnf(t900,plain,
select(a_1315,i5) = e_1279,
inference(rw,[status(thm)],[t110]) ).
cnf(f78,hypothesis,
e_1318 = select(a_1315,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).
fof(f78_nnf,plain,
e_1318 = select(a_1315,i5),
inference(nnf_transformation,[status(thm)],[f78]) ).
cnf(c78,plain,
e_1318 = select(a_1315,i5),
inference(cnf_transformation,[status(esa)],[f78_nnf]) ).
cnf(t40,plain,
select(a_1315,i5) = e_1318,
inference(equality_encoding,[status(esa)],[c78]) ).
cnf(t127,plain,
select(a_1315,i5) = e_1318,
inference(orient,[status(thm)],[t40]) ).
cnf(t1210,plain,
e_1318 = e_1279,
inference(step,[status(thm)],[t900,t127]) ).
cnf(t909,plain,
e_1279 = e_1318,
inference(orient,[status(thm)],[t1210]) ).
cnf(t1265,plain,
store(a_1317,i9,e_1318) = a_1282,
inference(step,[status(thm)],[t1264,t909]) ).
cnf(f42,hypothesis,
a_1319 = store(a_1317,i9,e_1318),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f42_nnf,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c42,plain,
a_1319 = store(a_1317,i9,e_1318),
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(t81,plain,
store(a_1317,i9,e_1318) = a_1319,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(t168,plain,
store(a_1317,i9,e_1318) = a_1319,
inference(orient,[status(thm)],[t81]) ).
cnf(t1266,plain,
a_1319 = a_1282,
inference(step,[status(thm)],[t1265,t168]) ).
cnf(t952,plain,
a_1282 = a_1319,
inference(orient,[status(thm)],[t1266]) ).
cnf(f79,negated_conjecture,
a_1282 != a_1319,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f79_nnf,plain,
a_1282 != a_1319,
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
a_1282 != a_1319,
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c79,plain,
a_1282 != a_1319,
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(goal_0,negated_conjecture,
a_1319 != a_1282,
inference(equality_encoding,[status(esa)],[c79]) ).
cnf(g0_0,plain,
a_1319 != a_1319,
inference(rw,[status(thm)],[goal_0,t952]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV543-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.58 % Computer : n004.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Thu Sep 24 20:24:40 UTC 2026
% 0.11/0.58 % CPUTime :
% 0.11/0.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 12.75/2.28 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.75/2.28 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------