%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:13:36 PM UTC 2026
% Result : Unsatisfiable 13.05s 22.24s
% Output : Proof 13.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 18
% Syntax : Number of formulae : 145 ( 145 unt; 0 def)
% Number of atoms : 145 ( 144 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 : 22 ( 22 usr; 20 con; 0-3 aty)
% Number of variables : 39 ( 4 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f16,hypothesis,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f16_nnf,plain,
a_808 = store(a_806,i2,e_807),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
a_808 = store(a_806,i2,e_807),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t42,plain,
store(a_806,i2,e_807) = a_808,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t101,plain,
store(a_806,i2,e_807) = a_808,
inference(orient,[status(thm)],[t42]) ).
cnf(f38,hypothesis,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f38_nnf,plain,
e_801 = select(a_800,i2),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
e_801 = select(a_800,i2),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
cnf(t15,plain,
select(a_800,i2) = e_801,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t74,plain,
select(a_800,i2) = e_801,
inference(orient,[status(thm)],[t15]) ).
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(t55,plain,
select(store(X1,X2,X3),X2) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t114,plain,
select(store(X1,X2,X3),X2) = X3,
inference(orient,[status(thm)],[t55]) ).
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(t58,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(t255,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)],[t58]) ).
cnf(t265,plain,
store(store(a_800,i2,select(a_800,X1)),X1,select(a_800,i2)) = store(store(a_800,X1,e_801),i2,select(a_800,X1)),
inference(cp,[status(thm)],[t255,t74]) ).
cnf(t651,plain,
store(store(a_800,i2,select(a_800,X1)),X1,e_801) = store(store(a_800,X1,e_801),i2,select(a_800,X1)),
inference(step,[status(thm)],[t265,t74]) ).
cnf(t414,plain,
store(store(a_800,i2,select(a_800,X1)),X1,e_801) = store(store(a_800,X1,e_801),i2,select(a_800,X1)),
inference(orient,[status(thm)],[t651]) ).
cnf(f39,hypothesis,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f39_nnf,plain,
e_803 = select(a_800,i5),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c39,plain,
e_803 = select(a_800,i5),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(t16,plain,
select(a_800,i5) = e_803,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t75,plain,
select(a_800,i5) = e_803,
inference(orient,[status(thm)],[t16]) ).
cnf(f14,hypothesis,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f14_nnf,plain,
a_804 = store(a_802,i2,e_803),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
a_804 = store(a_802,i2,e_803),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t40,plain,
store(a_802,i2,e_803) = a_804,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t99,plain,
store(a_802,i2,e_803) = a_804,
inference(orient,[status(thm)],[t40]) ).
cnf(t127,plain,
e_803 = select(a_804,i2),
inference(cp,[status(thm)],[t114,t99]) ).
cnf(f40,hypothesis,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f40_nnf,plain,
e_805 = select(a_804,i2),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
e_805 = select(a_804,i2),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(t17,plain,
select(a_804,i2) = e_805,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t76,plain,
select(a_804,i2) = e_805,
inference(orient,[status(thm)],[t17]) ).
cnf(t599,plain,
e_803 = e_805,
inference(step,[status(thm)],[t127,t76]) ).
cnf(t145,plain,
e_803 = e_805,
inference(orient,[status(thm)],[t599]) ).
cnf(t600,plain,
select(a_800,i5) = e_805,
inference(step,[status(thm)],[t75,t145]) ).
cnf(t146,plain,
select(a_800,i5) = e_805,
inference(orient,[status(thm)],[t600]) ).
cnf(t415,plain,
store(store(a_800,i5,e_801),i2,select(a_800,i5)) = store(store(a_800,i2,e_805),i5,e_801),
inference(cp,[status(thm)],[t414,t146]) ).
cnf(f13,hypothesis,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f13_nnf,plain,
a_802 = store(a_800,i5,e_801),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
a_802 = store(a_800,i5,e_801),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t39,plain,
store(a_800,i5,e_801) = a_802,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t98,plain,
store(a_800,i5,e_801) = a_802,
inference(orient,[status(thm)],[t39]) ).
cnf(t652,plain,
store(a_802,i2,select(a_800,i5)) = store(store(a_800,i2,e_805),i5,e_801),
inference(step,[status(thm)],[t415,t98]) ).
cnf(t653,plain,
store(a_802,i2,e_805) = store(store(a_800,i2,e_805),i5,e_801),
inference(step,[status(thm)],[t652,t146]) ).
cnf(t602,plain,
store(a_802,i2,e_805) = a_804,
inference(step,[status(thm)],[t99,t145]) ).
cnf(t148,plain,
store(a_802,i2,e_805) = a_804,
inference(rw,[status(thm)],[t602]) ).
cnf(t251,plain,
store(a_802,i2,e_805) = a_804,
inference(orient,[status(thm)],[t148]) ).
cnf(t654,plain,
a_804 = store(store(a_800,i2,e_805),i5,e_801),
inference(step,[status(thm)],[t653,t251]) ).
cnf(t420,plain,
store(store(a_800,i2,e_805),i5,e_801) = a_804,
inference(orient,[status(thm)],[t654]) ).
cnf(t421,plain,
e_801 = select(a_804,i5),
inference(cp,[status(thm)],[t114,t420]) ).
cnf(f41,hypothesis,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f41_nnf,plain,
e_807 = select(a_804,i5),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
e_807 = select(a_804,i5),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(t18,plain,
select(a_804,i5) = e_807,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t77,plain,
select(a_804,i5) = e_807,
inference(orient,[status(thm)],[t18]) ).
cnf(t655,plain,
e_801 = e_807,
inference(step,[status(thm)],[t421,t77]) ).
cnf(t423,plain,
e_801 = e_807,
inference(orient,[status(thm)],[t655]) ).
cnf(t656,plain,
select(a_800,i2) = e_807,
inference(step,[status(thm)],[t74,t423]) ).
cnf(t424,plain,
select(a_800,i2) = e_807,
inference(orient,[status(thm)],[t656]) ).
cnf(t530,plain,
select(a_821,i2) = e_807,
inference(rw,[status(thm)],[t424]) ).
cnf(f47,hypothesis,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f47_nnf,plain,
e_822 = select(a_821,i2),
inference(nnf_transformation,[status(thm)],[f47]) ).
cnf(c47,plain,
e_822 = select(a_821,i2),
inference(cnf_transformation,[status(esa)],[f47_nnf]) ).
cnf(t24,plain,
select(a_821,i2) = e_822,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t83,plain,
select(a_821,i2) = e_822,
inference(orient,[status(thm)],[t24]) ).
cnf(t719,plain,
e_822 = e_807,
inference(step,[status(thm)],[t530,t83]) ).
cnf(t536,plain,
e_807 = e_822,
inference(orient,[status(thm)],[t719]) ).
cnf(t722,plain,
store(a_806,i2,e_822) = a_808,
inference(step,[status(thm)],[t101,t536]) ).
cnf(t539,plain,
store(a_806,i2,e_822) = a_808,
inference(rw,[status(thm)],[t722]) ).
cnf(t562,plain,
store(a_806,i2,e_822) = a_808,
inference(orient,[status(thm)],[t539]) ).
cnf(t720,plain,
select(a_804,i5) = e_822,
inference(step,[status(thm)],[t77,t536]) ).
cnf(t537,plain,
select(a_804,i5) = e_822,
inference(orient,[status(thm)],[t720]) ).
cnf(t570,plain,
select(a_825,i5) = e_822,
inference(rw,[status(thm)],[t537]) ).
cnf(f50,hypothesis,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f50_nnf,plain,
e_828 = select(a_825,i5),
inference(nnf_transformation,[status(thm)],[f50]) ).
cnf(c50,plain,
e_828 = select(a_825,i5),
inference(cnf_transformation,[status(esa)],[f50_nnf]) ).
cnf(t27,plain,
select(a_825,i5) = e_828,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t86,plain,
select(a_825,i5) = e_828,
inference(orient,[status(thm)],[t27]) ).
cnf(t747,plain,
e_828 = e_822,
inference(step,[status(thm)],[t570,t86]) ).
cnf(t572,plain,
e_822 = e_828,
inference(orient,[status(thm)],[t747]) ).
cnf(t759,plain,
store(a_806,i2,e_828) = a_808,
inference(step,[status(thm)],[t562,t572]) ).
cnf(t584,plain,
store(a_806,i2,e_828) = a_808,
inference(rw,[status(thm)],[t759]) ).
cnf(f15,hypothesis,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f15_nnf,plain,
a_806 = store(a_804,i5,e_805),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
a_806 = store(a_804,i5,e_805),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t41,plain,
store(a_804,i5,e_805) = a_806,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t100,plain,
store(a_804,i5,e_805) = a_806,
inference(orient,[status(thm)],[t41]) ).
cnf(t531,plain,
select(a_821,i5) = e_805,
inference(rw,[status(thm)],[t146]) ).
cnf(f48,hypothesis,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f48_nnf,plain,
e_824 = select(a_821,i5),
inference(nnf_transformation,[status(thm)],[f48]) ).
cnf(c48,plain,
e_824 = select(a_821,i5),
inference(cnf_transformation,[status(esa)],[f48_nnf]) ).
cnf(t25,plain,
select(a_821,i5) = e_824,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t84,plain,
select(a_821,i5) = e_824,
inference(orient,[status(thm)],[t25]) ).
cnf(f26,hypothesis,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f26_nnf,plain,
a_825 = store(a_823,i2,e_824),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
a_825 = store(a_823,i2,e_824),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t51,plain,
store(a_823,i2,e_824) = a_825,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t110,plain,
store(a_823,i2,e_824) = a_825,
inference(orient,[status(thm)],[t51]) ).
cnf(t138,plain,
e_824 = select(a_825,i2),
inference(cp,[status(thm)],[t114,t110]) ).
cnf(f49,hypothesis,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f49_nnf,plain,
e_826 = select(a_825,i2),
inference(nnf_transformation,[status(thm)],[f49]) ).
cnf(c49,plain,
e_826 = select(a_825,i2),
inference(cnf_transformation,[status(esa)],[f49_nnf]) ).
cnf(t26,plain,
select(a_825,i2) = e_826,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(t85,plain,
select(a_825,i2) = e_826,
inference(orient,[status(thm)],[t26]) ).
cnf(t603,plain,
e_824 = e_826,
inference(step,[status(thm)],[t138,t85]) ).
cnf(t149,plain,
e_824 = e_826,
inference(orient,[status(thm)],[t603]) ).
cnf(t604,plain,
select(a_821,i5) = e_826,
inference(step,[status(thm)],[t84,t149]) ).
cnf(t150,plain,
select(a_821,i5) = e_826,
inference(orient,[status(thm)],[t604]) ).
cnf(t730,plain,
e_826 = e_805,
inference(step,[status(thm)],[t531,t150]) ).
cnf(t548,plain,
e_805 = e_826,
inference(orient,[status(thm)],[t730]) ).
cnf(t733,plain,
store(a_804,i5,e_826) = a_806,
inference(step,[status(thm)],[t100,t548]) ).
cnf(t551,plain,
store(a_804,i5,e_826) = a_806,
inference(rw,[status(thm)],[t733]) ).
cnf(t564,plain,
store(a_804,i5,e_826) = a_806,
inference(orient,[status(thm)],[t551]) ).
cnf(t571,plain,
store(a_825,i5,e_826) = a_806,
inference(rw,[status(thm)],[t564]) ).
cnf(f27,hypothesis,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f27_nnf,plain,
a_827 = store(a_825,i5,e_826),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
a_827 = store(a_825,i5,e_826),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(t52,plain,
store(a_825,i5,e_826) = a_827,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t111,plain,
store(a_825,i5,e_826) = a_827,
inference(orient,[status(thm)],[t52]) ).
cnf(t760,plain,
a_827 = a_806,
inference(step,[status(thm)],[t571,t111]) ).
cnf(t585,plain,
a_806 = a_827,
inference(orient,[status(thm)],[t760]) ).
cnf(t761,plain,
store(a_827,i2,e_828) = a_808,
inference(step,[status(thm)],[t584,t585]) ).
cnf(f28,hypothesis,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f28_nnf,plain,
a_829 = store(a_827,i2,e_828),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
a_829 = store(a_827,i2,e_828),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(t53,plain,
store(a_827,i2,e_828) = a_829,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t112,plain,
store(a_827,i2,e_828) = a_829,
inference(orient,[status(thm)],[t53]) ).
cnf(t762,plain,
a_829 = a_808,
inference(step,[status(thm)],[t761,t112]) ).
cnf(t589,plain,
a_808 = a_829,
inference(orient,[status(thm)],[t762]) ).
cnf(f51,negated_conjecture,
a_808 != a_829,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f51_nnf,plain,
a_808 != a_829,
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
a_808 != a_829,
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
a_808 != a_829,
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(goal_0,negated_conjecture,
a_829 != a_808,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(g0_0,plain,
a_829 != a_829,
inference(rw,[status(thm)],[goal_0,t589]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/20.38 % Computer : n017.cluster.edu
% 0.08/20.38 % Model : x86_64 x86_64
% 0.08/20.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/20.38 % Memory : 8046.5625MB
% 0.08/20.38 % OS : Linux 6.8.0-71-generic
% 0.08/20.38 % CPULimit : 300
% 0.08/20.38 % WCLimit : 300
% 0.08/20.38 % DateTime : Thu Sep 24 20:20:08 UTC 2026
% 0.08/20.39 % CPUTime :
% 0.08/20.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.05/22.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.05/22.24 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------