%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV558-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:40 PM UTC 2026
% Result : Unsatisfiable 9.23s 1.79s
% Output : Proof 9.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 31
% Syntax : Number of formulae : 335 ( 335 unt; 0 def)
% Number of atoms : 335 ( 334 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 12 ( 12 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 37 con; 0-3 aty)
% Number of variables : 60 ( 8 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/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(t36,plain,
select(store(X1,X2,X3),X2) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t43,plain,
select(store(X1,X2,X3),X2) = X3,
inference(orient,[status(thm)],[t36]) ).
cnf(f6,hypothesis,
a_31 = store(a2,i1,e_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f6_nnf,plain,
a_31 = store(a2,i1,e_30),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
a_31 = store(a2,i1,e_30),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t22,plain,
store(a2,i1,e_30) = a_31,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t89,plain,
store(a2,i1,e_30) = a_31,
inference(orient,[status(thm)],[t22]) ).
cnf(t91,plain,
e_30 = select(a_31,i1),
inference(cp,[status(thm)],[t43,t89]) ).
cnf(t243,plain,
select(a_31,i1) = e_30,
inference(orient,[status(thm)],[t91]) ).
cnf(f2,axiom,
store(A,I,select(A,I)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
fof(f2_nnf,plain,
! [A,I] : store(A,I,select(A,I)) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,I] : store(A,I,select(A,I)) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t37,plain,
store(X1,X2,select(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t42,plain,
store(X1,X2,select(X1,X2)) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(f21,hypothesis,
e_32 = select(a_31,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f21_nnf,plain,
e_32 = select(a_31,i2),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
e_32 = select(a_31,i2),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t10,plain,
select(a_31,i2) = e_32,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t114,plain,
select(a_31,i2) = e_32,
inference(orient,[status(thm)],[t10]) ).
cnf(t115,plain,
a_31 = store(a_31,i2,e_32),
inference(cp,[status(thm)],[t42,t114]) ).
cnf(t300,plain,
store(a_31,i2,e_32) = a_31,
inference(orient,[status(thm)],[t115]) ).
cnf(f7,hypothesis,
a_33 = store(a_29,i2,e_32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f7_nnf,plain,
a_33 = store(a_29,i2,e_32),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
a_33 = store(a_29,i2,e_32),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t23,plain,
store(a_29,i2,e_32) = a_33,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t80,plain,
store(a_29,i2,e_32) = a_33,
inference(orient,[status(thm)],[t23]) ).
cnf(t82,plain,
e_32 = select(a_33,i2),
inference(cp,[status(thm)],[t43,t80]) ).
cnf(t234,plain,
select(a_33,i2) = e_32,
inference(orient,[status(thm)],[t82]) ).
cnf(f9,hypothesis,
a_37 = store(a_33,i3,e_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f9_nnf,plain,
a_37 = store(a_33,i3,e_36),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
a_37 = store(a_33,i3,e_36),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t25,plain,
store(a_33,i3,e_36) = a_37,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t56,plain,
store(a_33,i3,e_36) = a_37,
inference(orient,[status(thm)],[t25]) ).
cnf(f11,hypothesis,
a_41 = store(a_37,i4,e_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f11_nnf,plain,
a_41 = store(a_37,i4,e_40),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
a_41 = store(a_37,i4,e_40),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t27,plain,
store(a_37,i4,e_40) = a_41,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t62,plain,
store(a_37,i4,e_40) = a_41,
inference(orient,[status(thm)],[t27]) ).
cnf(f13,hypothesis,
a_45 = store(a_41,i5,e_44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f13_nnf,plain,
a_45 = store(a_41,i5,e_44),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
a_45 = store(a_41,i5,e_44),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t29,plain,
store(a_41,i5,e_44) = a_45,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t68,plain,
store(a_41,i5,e_44) = a_45,
inference(orient,[status(thm)],[t29]) ).
cnf(f15,hypothesis,
a_49 = store(a_45,i6,e_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f15_nnf,plain,
a_49 = store(a_45,i6,e_48),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
a_49 = store(a_45,i6,e_48),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t31,plain,
store(a_45,i6,e_48) = a_49,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t74,plain,
store(a_45,i6,e_48) = a_49,
inference(orient,[status(thm)],[t31]) ).
cnf(f18,hypothesis,
a_55 = store(a_51,i7,e_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f18_nnf,plain,
a_55 = store(a_51,i7,e_54),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
a_55 = store(a_51,i7,e_54),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(t34,plain,
store(a_51,i7,e_54) = a_55,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t53,plain,
store(a_51,i7,e_54) = a_55,
inference(orient,[status(thm)],[t34]) ).
cnf(f31,hypothesis,
e_52 = select(a_51,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f31_nnf,plain,
e_52 = select(a_51,i7),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
e_52 = select(a_51,i7),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t20,plain,
select(a_51,i7) = e_52,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t94,plain,
select(a_51,i7) = e_52,
inference(orient,[status(thm)],[t20]) ).
cnf(t95,plain,
a_51 = store(a_51,i7,e_52),
inference(cp,[status(thm)],[t42,t94]) ).
cnf(t55,plain,
e_54 = select(a_55,i7),
inference(cp,[status(thm)],[t43,t53]) ).
cnf(f17,hypothesis,
a_53 = store(a_49,i7,e_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f17_nnf,plain,
a_53 = store(a_49,i7,e_52),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
a_53 = store(a_49,i7,e_52),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t33,plain,
store(a_49,i7,e_52) = a_53,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t50,plain,
store(a_49,i7,e_52) = a_53,
inference(orient,[status(thm)],[t33]) ).
cnf(t52,plain,
e_52 = select(a_53,i7),
inference(cp,[status(thm)],[t43,t50]) ).
cnf(f33,hypothesis,
a_53 = a_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f33_nnf,plain,
a_53 = a_55,
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
a_53 = a_55,
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(t0,plain,
a_55 = a_53,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t193,plain,
a_53 = a_55,
inference(orient,[status(thm)],[t0]) ).
cnf(t437,plain,
e_52 = select(a_55,i7),
inference(step,[status(thm)],[t52,t193]) ).
cnf(t196,plain,
select(a_55,i7) = e_52,
inference(orient,[status(thm)],[t437]) ).
cnf(t438,plain,
e_54 = e_52,
inference(step,[status(thm)],[t55,t196]) ).
cnf(t199,plain,
e_52 = e_54,
inference(orient,[status(thm)],[t438]) ).
cnf(t446,plain,
a_51 = store(a_51,i7,e_54),
inference(step,[status(thm)],[t95,t199]) ).
cnf(t447,plain,
a_51 = a_55,
inference(step,[status(thm)],[t446,t53]) ).
cnf(t250,plain,
a_51 = a_55,
inference(orient,[status(thm)],[t447]) ).
cnf(t451,plain,
store(a_55,i7,e_54) = a_55,
inference(step,[status(thm)],[t53,t250]) ).
cnf(f32,hypothesis,
e_54 = select(a_49,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f32_nnf,plain,
e_54 = select(a_49,i7),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
e_54 = select(a_49,i7),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t19,plain,
select(a_49,i7) = e_54,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t92,plain,
select(a_49,i7) = e_54,
inference(orient,[status(thm)],[t19]) ).
cnf(t93,plain,
a_49 = store(a_49,i7,e_54),
inference(cp,[status(thm)],[t42,t92]) ).
cnf(f3,axiom,
store(store(A,I,E),I,F) = store(A,I,F),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4) ).
fof(f3_nnf,plain,
! [A,I,E,F] : store(store(A,I,E),I,F) = store(A,I,F),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,I,E,F] : store(store(A,I,E),I,F) = store(A,I,F),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t39,plain,
store(store(X1,X2,X3),X2,X4) = store(X1,X2,X4),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t49,plain,
store(store(X1,X2,X3),X2,X4) = store(X1,X2,X4),
inference(orient,[status(thm)],[t39]) ).
cnf(t51,plain,
store(a_49,i7,X1) = store(a_53,i7,X1),
inference(cp,[status(thm)],[t49,t50]) ).
cnf(t444,plain,
store(a_49,i7,X1) = store(a_55,i7,X1),
inference(step,[status(thm)],[t51,t193]) ).
cnf(t226,plain,
store(a_49,i7,X1) = store(a_55,i7,X1),
inference(orient,[status(thm)],[t444]) ).
cnf(t445,plain,
a_49 = store(a_55,i7,e_54),
inference(step,[status(thm)],[t93,t226]) ).
cnf(t246,plain,
store(a_55,i7,e_54) = a_49,
inference(orient,[status(thm)],[t445]) ).
cnf(t452,plain,
a_49 = a_55,
inference(step,[status(thm)],[t451,t246]) ).
cnf(t254,plain,
a_49 = a_55,
inference(rw,[status(thm)],[t452]) ).
cnf(t255,plain,
a_49 = a_55,
inference(orient,[status(thm)],[t254]) ).
cnf(t453,plain,
store(a_45,i6,e_48) = a_55,
inference(step,[status(thm)],[t74,t255]) ).
cnf(t256,plain,
store(a_45,i6,e_48) = a_55,
inference(orient,[status(thm)],[t453]) ).
cnf(t76,plain,
e_48 = select(a_49,i6),
inference(cp,[status(thm)],[t43,t74]) ).
cnf(t223,plain,
select(a_49,i6) = e_48,
inference(orient,[status(thm)],[t76]) ).
cnf(t457,plain,
select(a_55,i6) = e_48,
inference(step,[status(thm)],[t223,t255]) ).
cnf(t260,plain,
select(a_55,i6) = e_48,
inference(rw,[status(thm)],[t457]) ).
cnf(f16,hypothesis,
a_51 = store(a_47,i6,e_50),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f16_nnf,plain,
a_51 = store(a_47,i6,e_50),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
a_51 = store(a_47,i6,e_50),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t32,plain,
store(a_47,i6,e_50) = a_51,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t77,plain,
store(a_47,i6,e_50) = a_51,
inference(orient,[status(thm)],[t32]) ).
cnf(t79,plain,
e_50 = select(a_51,i6),
inference(cp,[status(thm)],[t43,t77]) ).
cnf(t231,plain,
select(a_51,i6) = e_50,
inference(orient,[status(thm)],[t79]) ).
cnf(t450,plain,
select(a_55,i6) = e_50,
inference(step,[status(thm)],[t231,t250]) ).
cnf(t253,plain,
select(a_55,i6) = e_50,
inference(rw,[status(thm)],[t450]) ).
cnf(t261,plain,
select(a_55,i6) = e_50,
inference(orient,[status(thm)],[t253]) ).
cnf(t458,plain,
e_50 = e_48,
inference(step,[status(thm)],[t260,t261]) ).
cnf(t264,plain,
e_48 = e_50,
inference(orient,[status(thm)],[t458]) ).
cnf(t461,plain,
store(a_45,i6,e_50) = a_55,
inference(step,[status(thm)],[t256,t264]) ).
cnf(t267,plain,
store(a_45,i6,e_50) = a_55,
inference(rw,[status(thm)],[t461]) ).
cnf(f30,hypothesis,
e_50 = select(a_45,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f30_nnf,plain,
e_50 = select(a_45,i6),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
e_50 = select(a_45,i6),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(t17,plain,
select(a_45,i6) = e_50,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t108,plain,
select(a_45,i6) = e_50,
inference(orient,[status(thm)],[t17]) ).
cnf(t109,plain,
a_45 = store(a_45,i6,e_50),
inference(cp,[status(thm)],[t42,t108]) ).
cnf(t286,plain,
store(a_45,i6,e_50) = a_45,
inference(orient,[status(thm)],[t109]) ).
cnf(t468,plain,
a_45 = a_55,
inference(step,[status(thm)],[t267,t286]) ).
cnf(t339,plain,
a_45 = a_55,
inference(orient,[status(thm)],[t468]) ).
cnf(t469,plain,
store(a_41,i5,e_44) = a_55,
inference(step,[status(thm)],[t68,t339]) ).
cnf(t340,plain,
store(a_41,i5,e_44) = a_55,
inference(orient,[status(thm)],[t469]) ).
cnf(t70,plain,
e_44 = select(a_45,i5),
inference(cp,[status(thm)],[t43,t68]) ).
cnf(t217,plain,
select(a_45,i5) = e_44,
inference(orient,[status(thm)],[t70]) ).
cnf(t473,plain,
select(a_55,i5) = e_44,
inference(step,[status(thm)],[t217,t339]) ).
cnf(f14,hypothesis,
a_47 = store(a_43,i5,e_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f14_nnf,plain,
a_47 = store(a_43,i5,e_46),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
a_47 = store(a_43,i5,e_46),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t30,plain,
store(a_43,i5,e_46) = a_47,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t71,plain,
store(a_43,i5,e_46) = a_47,
inference(orient,[status(thm)],[t30]) ).
cnf(t73,plain,
e_46 = select(a_47,i5),
inference(cp,[status(thm)],[t43,t71]) ).
cnf(t220,plain,
select(a_47,i5) = e_46,
inference(orient,[status(thm)],[t73]) ).
cnf(f29,hypothesis,
e_48 = select(a_47,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f29_nnf,plain,
e_48 = select(a_47,i6),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
e_48 = select(a_47,i6),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(t18,plain,
select(a_47,i6) = e_48,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t110,plain,
select(a_47,i6) = e_48,
inference(orient,[status(thm)],[t18]) ).
cnf(t111,plain,
a_47 = store(a_47,i6,e_48),
inference(cp,[status(thm)],[t42,t110]) ).
cnf(t462,plain,
a_47 = store(a_47,i6,e_50),
inference(step,[status(thm)],[t111,t264]) ).
cnf(t448,plain,
store(a_47,i6,e_50) = a_55,
inference(step,[status(thm)],[t77,t250]) ).
cnf(t251,plain,
store(a_47,i6,e_50) = a_55,
inference(orient,[status(thm)],[t448]) ).
cnf(t463,plain,
a_47 = a_55,
inference(step,[status(thm)],[t462,t251]) ).
cnf(t289,plain,
a_47 = a_55,
inference(orient,[status(thm)],[t463]) ).
cnf(t466,plain,
select(a_55,i5) = e_46,
inference(step,[status(thm)],[t220,t289]) ).
cnf(t292,plain,
select(a_55,i5) = e_46,
inference(rw,[status(thm)],[t466]) ).
cnf(t294,plain,
select(a_55,i5) = e_46,
inference(orient,[status(thm)],[t292]) ).
cnf(t474,plain,
e_46 = e_44,
inference(step,[status(thm)],[t473,t294]) ).
cnf(t343,plain,
e_46 = e_44,
inference(rw,[status(thm)],[t474]) ).
cnf(t344,plain,
e_44 = e_46,
inference(orient,[status(thm)],[t343]) ).
cnf(t479,plain,
store(a_41,i5,e_46) = a_55,
inference(step,[status(thm)],[t340,t344]) ).
cnf(f28,hypothesis,
e_46 = select(a_41,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f28_nnf,plain,
e_46 = select(a_41,i5),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
e_46 = select(a_41,i5),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(t15,plain,
select(a_41,i5) = e_46,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t104,plain,
select(a_41,i5) = e_46,
inference(orient,[status(thm)],[t15]) ).
cnf(t105,plain,
a_41 = store(a_41,i5,e_46),
inference(cp,[status(thm)],[t42,t104]) ).
cnf(t280,plain,
store(a_41,i5,e_46) = a_41,
inference(orient,[status(thm)],[t105]) ).
cnf(t480,plain,
a_41 = a_55,
inference(step,[status(thm)],[t479,t280]) ).
cnf(t348,plain,
a_41 = a_55,
inference(rw,[status(thm)],[t480]) ).
cnf(t355,plain,
a_41 = a_55,
inference(orient,[status(thm)],[t348]) ).
cnf(t487,plain,
store(a_37,i4,e_40) = a_55,
inference(step,[status(thm)],[t62,t355]) ).
cnf(t356,plain,
store(a_37,i4,e_40) = a_55,
inference(orient,[status(thm)],[t487]) ).
cnf(t64,plain,
e_40 = select(a_41,i4),
inference(cp,[status(thm)],[t43,t62]) ).
cnf(t211,plain,
select(a_41,i4) = e_40,
inference(orient,[status(thm)],[t64]) ).
cnf(t493,plain,
select(a_55,i4) = e_40,
inference(step,[status(thm)],[t211,t355]) ).
cnf(t360,plain,
select(a_55,i4) = e_40,
inference(rw,[status(thm)],[t493]) ).
cnf(f12,hypothesis,
a_43 = store(a_39,i4,e_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f12_nnf,plain,
a_43 = store(a_39,i4,e_42),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
a_43 = store(a_39,i4,e_42),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t28,plain,
store(a_39,i4,e_42) = a_43,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t65,plain,
store(a_39,i4,e_42) = a_43,
inference(orient,[status(thm)],[t28]) ).
cnf(t67,plain,
e_42 = select(a_43,i4),
inference(cp,[status(thm)],[t43,t65]) ).
cnf(t214,plain,
select(a_43,i4) = e_42,
inference(orient,[status(thm)],[t67]) ).
cnf(f27,hypothesis,
e_44 = select(a_43,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f27_nnf,plain,
e_44 = select(a_43,i5),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
e_44 = select(a_43,i5),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(t16,plain,
select(a_43,i5) = e_44,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t106,plain,
select(a_43,i5) = e_44,
inference(orient,[status(thm)],[t16]) ).
cnf(t107,plain,
a_43 = store(a_43,i5,e_44),
inference(cp,[status(thm)],[t42,t106]) ).
cnf(t283,plain,
store(a_43,i5,e_44) = a_43,
inference(orient,[status(thm)],[t107]) ).
cnf(t477,plain,
store(a_43,i5,e_46) = a_43,
inference(step,[status(thm)],[t283,t344]) ).
cnf(t464,plain,
store(a_43,i5,e_46) = a_55,
inference(step,[status(thm)],[t71,t289]) ).
cnf(t290,plain,
store(a_43,i5,e_46) = a_55,
inference(orient,[status(thm)],[t464]) ).
cnf(t478,plain,
a_55 = a_43,
inference(step,[status(thm)],[t477,t290]) ).
cnf(t347,plain,
a_55 = a_43,
inference(rw,[status(thm)],[t478]) ).
cnf(t349,plain,
a_43 = a_55,
inference(orient,[status(thm)],[t347]) ).
cnf(t485,plain,
select(a_55,i4) = e_42,
inference(step,[status(thm)],[t214,t349]) ).
cnf(t353,plain,
select(a_55,i4) = e_42,
inference(rw,[status(thm)],[t485]) ).
cnf(t361,plain,
select(a_55,i4) = e_42,
inference(orient,[status(thm)],[t353]) ).
cnf(t494,plain,
e_42 = e_40,
inference(step,[status(thm)],[t360,t361]) ).
cnf(t364,plain,
e_40 = e_42,
inference(orient,[status(thm)],[t494]) ).
cnf(t499,plain,
store(a_37,i4,e_42) = a_55,
inference(step,[status(thm)],[t356,t364]) ).
cnf(f26,hypothesis,
e_42 = select(a_37,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f26_nnf,plain,
e_42 = select(a_37,i4),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
e_42 = select(a_37,i4),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t13,plain,
select(a_37,i4) = e_42,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t100,plain,
select(a_37,i4) = e_42,
inference(orient,[status(thm)],[t13]) ).
cnf(t101,plain,
a_37 = store(a_37,i4,e_42),
inference(cp,[status(thm)],[t42,t100]) ).
cnf(t274,plain,
store(a_37,i4,e_42) = a_37,
inference(orient,[status(thm)],[t101]) ).
cnf(t500,plain,
a_37 = a_55,
inference(step,[status(thm)],[t499,t274]) ).
cnf(t368,plain,
a_37 = a_55,
inference(rw,[status(thm)],[t500]) ).
cnf(t375,plain,
a_37 = a_55,
inference(orient,[status(thm)],[t368]) ).
cnf(t507,plain,
store(a_33,i3,e_36) = a_55,
inference(step,[status(thm)],[t56,t375]) ).
cnf(t376,plain,
store(a_33,i3,e_36) = a_55,
inference(orient,[status(thm)],[t507]) ).
cnf(t58,plain,
e_36 = select(a_37,i3),
inference(cp,[status(thm)],[t43,t56]) ).
cnf(t205,plain,
select(a_37,i3) = e_36,
inference(orient,[status(thm)],[t58]) ).
cnf(t513,plain,
select(a_55,i3) = e_36,
inference(step,[status(thm)],[t205,t375]) ).
cnf(t380,plain,
select(a_55,i3) = e_36,
inference(rw,[status(thm)],[t513]) ).
cnf(f10,hypothesis,
a_39 = store(a_35,i3,e_38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f10_nnf,plain,
a_39 = store(a_35,i3,e_38),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
a_39 = store(a_35,i3,e_38),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t26,plain,
store(a_35,i3,e_38) = a_39,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t59,plain,
store(a_35,i3,e_38) = a_39,
inference(orient,[status(thm)],[t26]) ).
cnf(t61,plain,
e_38 = select(a_39,i3),
inference(cp,[status(thm)],[t43,t59]) ).
cnf(t208,plain,
select(a_39,i3) = e_38,
inference(orient,[status(thm)],[t61]) ).
cnf(f25,hypothesis,
e_40 = select(a_39,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f25_nnf,plain,
e_40 = select(a_39,i4),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
e_40 = select(a_39,i4),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(t14,plain,
select(a_39,i4) = e_40,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t102,plain,
select(a_39,i4) = e_40,
inference(orient,[status(thm)],[t14]) ).
cnf(t103,plain,
a_39 = store(a_39,i4,e_40),
inference(cp,[status(thm)],[t42,t102]) ).
cnf(t277,plain,
store(a_39,i4,e_40) = a_39,
inference(orient,[status(thm)],[t103]) ).
cnf(t497,plain,
store(a_39,i4,e_42) = a_39,
inference(step,[status(thm)],[t277,t364]) ).
cnf(t481,plain,
store(a_39,i4,e_42) = a_55,
inference(step,[status(thm)],[t65,t349]) ).
cnf(t350,plain,
store(a_39,i4,e_42) = a_55,
inference(orient,[status(thm)],[t481]) ).
cnf(t498,plain,
a_55 = a_39,
inference(step,[status(thm)],[t497,t350]) ).
cnf(t367,plain,
a_55 = a_39,
inference(rw,[status(thm)],[t498]) ).
cnf(t369,plain,
a_39 = a_55,
inference(orient,[status(thm)],[t367]) ).
cnf(t505,plain,
select(a_55,i3) = e_38,
inference(step,[status(thm)],[t208,t369]) ).
cnf(t373,plain,
select(a_55,i3) = e_38,
inference(rw,[status(thm)],[t505]) ).
cnf(t381,plain,
select(a_55,i3) = e_38,
inference(orient,[status(thm)],[t373]) ).
cnf(t514,plain,
e_38 = e_36,
inference(step,[status(thm)],[t380,t381]) ).
cnf(t384,plain,
e_36 = e_38,
inference(orient,[status(thm)],[t514]) ).
cnf(t519,plain,
store(a_33,i3,e_38) = a_55,
inference(step,[status(thm)],[t376,t384]) ).
cnf(f24,hypothesis,
e_38 = select(a_33,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f24_nnf,plain,
e_38 = select(a_33,i3),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
e_38 = select(a_33,i3),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t11,plain,
select(a_33,i3) = e_38,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t96,plain,
select(a_33,i3) = e_38,
inference(orient,[status(thm)],[t11]) ).
cnf(t97,plain,
a_33 = store(a_33,i3,e_38),
inference(cp,[status(thm)],[t42,t96]) ).
cnf(t268,plain,
store(a_33,i3,e_38) = a_33,
inference(orient,[status(thm)],[t97]) ).
cnf(t520,plain,
a_33 = a_55,
inference(step,[status(thm)],[t519,t268]) ).
cnf(t388,plain,
a_33 = a_55,
inference(rw,[status(thm)],[t520]) ).
cnf(t395,plain,
a_33 = a_55,
inference(orient,[status(thm)],[t388]) ).
cnf(t533,plain,
select(a_55,i2) = e_32,
inference(step,[status(thm)],[t234,t395]) ).
cnf(t400,plain,
select(a_55,i2) = e_32,
inference(rw,[status(thm)],[t533]) ).
cnf(f8,hypothesis,
a_35 = store(a_31,i2,e_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f8_nnf,plain,
a_35 = store(a_31,i2,e_34),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
a_35 = store(a_31,i2,e_34),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t24,plain,
store(a_31,i2,e_34) = a_35,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t83,plain,
store(a_31,i2,e_34) = a_35,
inference(orient,[status(thm)],[t24]) ).
cnf(t85,plain,
e_34 = select(a_35,i2),
inference(cp,[status(thm)],[t43,t83]) ).
cnf(t237,plain,
select(a_35,i2) = e_34,
inference(orient,[status(thm)],[t85]) ).
cnf(f23,hypothesis,
e_36 = select(a_35,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f23_nnf,plain,
e_36 = select(a_35,i3),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
e_36 = select(a_35,i3),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(t12,plain,
select(a_35,i3) = e_36,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t98,plain,
select(a_35,i3) = e_36,
inference(orient,[status(thm)],[t12]) ).
cnf(t99,plain,
a_35 = store(a_35,i3,e_36),
inference(cp,[status(thm)],[t42,t98]) ).
cnf(t271,plain,
store(a_35,i3,e_36) = a_35,
inference(orient,[status(thm)],[t99]) ).
cnf(t517,plain,
store(a_35,i3,e_38) = a_35,
inference(step,[status(thm)],[t271,t384]) ).
cnf(t501,plain,
store(a_35,i3,e_38) = a_55,
inference(step,[status(thm)],[t59,t369]) ).
cnf(t370,plain,
store(a_35,i3,e_38) = a_55,
inference(orient,[status(thm)],[t501]) ).
cnf(t518,plain,
a_55 = a_35,
inference(step,[status(thm)],[t517,t370]) ).
cnf(t387,plain,
a_55 = a_35,
inference(rw,[status(thm)],[t518]) ).
cnf(t389,plain,
a_35 = a_55,
inference(orient,[status(thm)],[t387]) ).
cnf(t525,plain,
select(a_55,i2) = e_34,
inference(step,[status(thm)],[t237,t389]) ).
cnf(t393,plain,
select(a_55,i2) = e_34,
inference(rw,[status(thm)],[t525]) ).
cnf(t401,plain,
select(a_55,i2) = e_34,
inference(orient,[status(thm)],[t393]) ).
cnf(t534,plain,
e_34 = e_32,
inference(step,[status(thm)],[t400,t401]) ).
cnf(t404,plain,
e_32 = e_34,
inference(orient,[status(thm)],[t534]) ).
cnf(t537,plain,
store(a_31,i2,e_34) = a_31,
inference(step,[status(thm)],[t300,t404]) ).
cnf(t521,plain,
store(a_31,i2,e_34) = a_55,
inference(step,[status(thm)],[t83,t389]) ).
cnf(t390,plain,
store(a_31,i2,e_34) = a_55,
inference(orient,[status(thm)],[t521]) ).
cnf(t538,plain,
a_55 = a_31,
inference(step,[status(thm)],[t537,t390]) ).
cnf(t407,plain,
a_55 = a_31,
inference(rw,[status(thm)],[t538]) ).
cnf(t409,plain,
a_31 = a_55,
inference(orient,[status(thm)],[t407]) ).
cnf(t545,plain,
select(a_55,i1) = e_30,
inference(step,[status(thm)],[t243,t409]) ).
cnf(t413,plain,
select(a_55,i1) = e_30,
inference(rw,[status(thm)],[t545]) ).
cnf(t421,plain,
select(a_55,i1) = e_30,
inference(orient,[status(thm)],[t413]) ).
cnf(f5,hypothesis,
a_29 = store(a1,i1,e_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f5_nnf,plain,
a_29 = store(a1,i1,e_28),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
a_29 = store(a1,i1,e_28),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t21,plain,
store(a1,i1,e_28) = a_29,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t86,plain,
store(a1,i1,e_28) = a_29,
inference(orient,[status(thm)],[t21]) ).
cnf(t87,plain,
store(a1,i1,X1) = store(a_29,i1,X1),
inference(cp,[status(thm)],[t49,t86]) ).
cnf(t527,plain,
store(a_29,i2,e_32) = a_55,
inference(step,[status(thm)],[t80,t395]) ).
cnf(t396,plain,
store(a_29,i2,e_32) = a_55,
inference(orient,[status(thm)],[t527]) ).
cnf(t539,plain,
store(a_29,i2,e_34) = a_55,
inference(step,[status(thm)],[t396,t404]) ).
cnf(f22,hypothesis,
e_34 = select(a_29,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f22_nnf,plain,
e_34 = select(a_29,i2),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
e_34 = select(a_29,i2),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(t9,plain,
select(a_29,i2) = e_34,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t112,plain,
select(a_29,i2) = e_34,
inference(orient,[status(thm)],[t9]) ).
cnf(t113,plain,
a_29 = store(a_29,i2,e_34),
inference(cp,[status(thm)],[t42,t112]) ).
cnf(t297,plain,
store(a_29,i2,e_34) = a_29,
inference(orient,[status(thm)],[t113]) ).
cnf(t540,plain,
a_29 = a_55,
inference(step,[status(thm)],[t539,t297]) ).
cnf(t408,plain,
a_29 = a_55,
inference(rw,[status(thm)],[t540]) ).
cnf(t415,plain,
a_29 = a_55,
inference(orient,[status(thm)],[t408]) ).
cnf(t554,plain,
store(a1,i1,X1) = store(a_55,i1,X1),
inference(step,[status(thm)],[t87,t415]) ).
cnf(t424,plain,
store(a1,i1,X1) = store(a_55,i1,X1),
inference(orient,[status(thm)],[t554]) ).
cnf(t88,plain,
e_28 = select(a_29,i1),
inference(cp,[status(thm)],[t43,t86]) ).
cnf(t240,plain,
select(a_29,i1) = e_28,
inference(orient,[status(thm)],[t88]) ).
cnf(t553,plain,
select(a_55,i1) = e_28,
inference(step,[status(thm)],[t240,t415]) ).
cnf(t420,plain,
select(a_55,i1) = e_28,
inference(rw,[status(thm)],[t553]) ).
cnf(t557,plain,
e_30 = e_28,
inference(step,[status(thm)],[t420,t421]) ).
cnf(t431,plain,
e_28 = e_30,
inference(orient,[status(thm)],[t557]) ).
cnf(t541,plain,
store(a2,i1,e_30) = a_55,
inference(step,[status(thm)],[t89,t409]) ).
cnf(t410,plain,
store(a2,i1,e_30) = a_55,
inference(orient,[status(thm)],[t541]) ).
cnf(f34,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f34_nnf,plain,
a1 != a2,
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
a1 != a2,
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
a1 != a2,
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(goal_0,negated_conjecture,
a2 != a1,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(g0_0,plain,
store(a1,i1,e_30) != a1,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
store(a1,i1,select(a_55,i1)) != a1,
inference(rw,[status(thm)],[g0_0,t421]) ).
cnf(g0_2,plain,
store(a_55,i1,select(a_55,i1)) != a1,
inference(rw,[status(thm)],[g0_1,t424]) ).
cnf(g0_3,plain,
a_55 != a1,
inference(rw,[status(thm)],[g0_2,t42]) ).
cnf(g0_4,plain,
a_55 != store(a2,i1,e_28),
inference(rw,[status(thm)],[g0_3]) ).
cnf(g0_5,plain,
a_55 != store(a2,i1,e_30),
inference(rw,[status(thm)],[g0_4,t431]) ).
cnf(g0_6,plain,
a_55 != a_55,
inference(rw,[status(thm)],[g0_5,t410]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV558-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/0.45 % Computer : n015.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Thu Sep 24 20:34:11 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.23/1.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.23/1.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------