%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 02:51:37 PM UTC 2026
% Result : Unsatisfiable 7.71s 1.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:04:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 7.71/1.47 % Refutation found
% 7.71/1.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.71/1.47 % SZS output start CNFRefutation for theBenchmark
% 7.71/1.47 fof(f1,axiom,(
% 7.71/1.47 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f3,axiom,(
% 7.71/1.47 (![A,I]: (store(A,I,select(A,I)) = A ))),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f4,axiom,(
% 7.71/1.47 (![A,I,E,F]: (store(store(A,I,E),I,F) = store(A,I,F) ))),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f5,axiom,(
% 7.71/1.47 (![I,J,A,E,F]: (( I = J| store(store(A,I,E),J,F) = store(store(A,J,F),I,E) ) ))),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f8,hypothesis,(
% 7.71/1.47 a_420 = store(a_418,i0,e_419) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f9,hypothesis,(
% 7.71/1.47 a_422 = store(a_420,i3,e_421) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f10,hypothesis,(
% 7.71/1.47 a_424 = store(a_422,i3,e_423) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f11,hypothesis,(
% 7.71/1.47 a_426 = store(a_424,i2,e_425) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f12,hypothesis,(
% 7.71/1.47 a_428 = store(a_426,i2,e_427) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f13,hypothesis,(
% 7.71/1.47 a_430 = store(a_428,i0,e_429) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f14,hypothesis,(
% 7.71/1.47 a_431 = store(a_418,i3,e_421) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f15,hypothesis,(
% 7.71/1.47 a_432 = store(a_431,i0,e_419) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f16,hypothesis,(
% 7.71/1.47 a_434 = store(a_432,i3,e_433) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f17,hypothesis,(
% 7.71/1.47 a_436 = store(a_434,i2,e_435) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f18,hypothesis,(
% 7.71/1.47 a_438 = store(a_436,i0,e_437) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f19,hypothesis,(
% 7.71/1.47 a_440 = store(a_438,i2,e_439) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f21,hypothesis,(
% 7.71/1.47 e_419 = select(a_418,i3) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f22,hypothesis,(
% 7.71/1.47 e_421 = select(a_418,i0) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f23,hypothesis,(
% 7.71/1.47 e_423 = select(a_422,i2) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f24,hypothesis,(
% 7.71/1.47 e_425 = select(a_422,i3) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f25,hypothesis,(
% 7.71/1.47 e_427 = select(a_426,i0) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f26,hypothesis,(
% 7.71/1.47 e_429 = select(a_426,i2) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f27,hypothesis,(
% 7.71/1.47 e_433 = select(a_432,i2) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f28,hypothesis,(
% 7.71/1.47 e_435 = select(a_432,i3) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f29,hypothesis,(
% 7.71/1.47 e_437 = select(a_436,i2) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f30,hypothesis,(
% 7.71/1.47 e_439 = select(a_436,i0) ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f31,negated_conjecture,(
% 7.71/1.47 a_430 != a_440 ),
% 7.71/1.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.71/1.47 fof(f32,plain,(
% 7.71/1.47 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f1])).
% 7.71/1.47 fof(f35,plain,(
% 7.71/1.47 ![X0,X1]: (store(X0,X1,select(X0,X1))=X0)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f3])).
% 7.71/1.47 fof(f36,plain,(
% 7.71/1.47 ![X0,X1,X2,X3]: (store(store(X0,X1,X2),X1,X3)=store(X0,X1,X3))),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f4])).
% 7.71/1.47 fof(f37,plain,(
% 7.71/1.47 ![I,J]: (I=J|(![A,E,F]: store(store(A,I,E),J,F)=store(store(A,J,F),I,E)))),
% 7.71/1.47 inference(miniscoping,[status(thm)],[f5])).
% 7.71/1.47 fof(f38,plain,(
% 7.71/1.47 ![X0,X1,X2,X3,X4]: (X0=X1|store(store(X2,X0,X3),X1,X4)=store(store(X2,X1,X4),X0,X3))),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f37])).
% 7.71/1.47 fof(f41,plain,(
% 7.71/1.47 a_420=store(a_418,i0,e_419)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f8])).
% 7.71/1.47 fof(f42,plain,(
% 7.71/1.47 a_422=store(a_420,i3,e_421)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f9])).
% 7.71/1.47 fof(f43,plain,(
% 7.71/1.47 a_424=store(a_422,i3,e_423)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f10])).
% 7.71/1.47 fof(f44,plain,(
% 7.71/1.47 a_426=store(a_424,i2,e_425)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f11])).
% 7.71/1.47 fof(f45,plain,(
% 7.71/1.47 a_428=store(a_426,i2,e_427)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f12])).
% 7.71/1.47 fof(f46,plain,(
% 7.71/1.47 a_430=store(a_428,i0,e_429)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f13])).
% 7.71/1.47 fof(f47,plain,(
% 7.71/1.47 a_431=store(a_418,i3,e_421)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f14])).
% 7.71/1.47 fof(f48,plain,(
% 7.71/1.47 a_432=store(a_431,i0,e_419)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f15])).
% 7.71/1.47 fof(f49,plain,(
% 7.71/1.47 a_434=store(a_432,i3,e_433)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f16])).
% 7.71/1.47 fof(f50,plain,(
% 7.71/1.47 a_436=store(a_434,i2,e_435)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f17])).
% 7.71/1.47 fof(f51,plain,(
% 7.71/1.47 a_438=store(a_436,i0,e_437)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f18])).
% 7.71/1.47 fof(f52,plain,(
% 7.71/1.47 a_440=store(a_438,i2,e_439)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f19])).
% 7.71/1.47 fof(f54,plain,(
% 7.71/1.47 e_419=select(a_418,i3)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f21])).
% 7.71/1.47 fof(f55,plain,(
% 7.71/1.47 e_421=select(a_418,i0)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f22])).
% 7.71/1.47 fof(f56,plain,(
% 7.71/1.47 e_423=select(a_422,i2)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f23])).
% 7.71/1.47 fof(f57,plain,(
% 7.71/1.47 e_425=select(a_422,i3)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f24])).
% 7.71/1.47 fof(f58,plain,(
% 7.71/1.47 e_427=select(a_426,i0)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f25])).
% 7.71/1.47 fof(f59,plain,(
% 7.71/1.47 e_429=select(a_426,i2)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f26])).
% 7.71/1.47 fof(f60,plain,(
% 7.71/1.47 e_433=select(a_432,i2)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f27])).
% 7.71/1.47 fof(f61,plain,(
% 7.71/1.47 e_435=select(a_432,i3)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f28])).
% 7.71/1.47 fof(f62,plain,(
% 7.71/1.47 e_437=select(a_436,i2)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f29])).
% 7.71/1.47 fof(f63,plain,(
% 7.71/1.47 e_439=select(a_436,i0)),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f30])).
% 7.71/1.47 fof(f64,plain,(
% 7.71/1.47 ~a_430=a_440),
% 7.71/1.47 inference(cnf_transformation,[status(thm)],[f31])).
% 7.71/1.47 fof(f65,plain,(
% 7.71/1.47 select(a_440,i2)=e_439),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f52,f32])).
% 7.71/1.47 fof(f66,plain,(
% 7.71/1.47 select(a_430,i0)=e_429),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f46,f32])).
% 7.71/1.47 fof(f72,plain,(
% 7.71/1.47 store(a_436,i2,e_437)=a_436),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f62,f35])).
% 7.71/1.47 fof(f78,plain,(
% 7.71/1.47 store(a_422,i3,e_425)=a_422),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f57,f35])).
% 7.71/1.47 fof(f80,plain,(
% 7.71/1.47 store(a_418,i0,e_421)=a_418),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f55,f35])).
% 7.71/1.47 fof(f81,plain,(
% 7.71/1.47 store(a_418,i3,e_419)=a_418),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f54,f35])).
% 7.71/1.47 fof(f82,plain,(
% 7.71/1.47 store(a_430,i0,e_429)=a_430),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f66,f35])).
% 7.71/1.47 fof(f83,plain,(
% 7.71/1.47 store(a_440,i2,e_439)=a_440),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f65,f35])).
% 7.71/1.47 fof(f96,plain,(
% 7.71/1.47 select(a_420,i0)=e_419),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f41,f32])).
% 7.71/1.47 fof(f97,plain,(
% 7.71/1.47 store(a_420,i0,e_419)=a_420),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f96,f35])).
% 7.71/1.47 fof(f99,plain,(
% 7.71/1.47 select(a_422,i3)=e_421),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f42,f32])).
% 7.71/1.47 fof(f100,plain,(
% 7.71/1.47 e_425=e_421),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f57,f99])).
% 7.71/1.47 fof(f103,plain,(
% 7.71/1.47 ![X0]: (store(a_422,i3,X0)=store(a_420,i3,X0))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f42,f36])).
% 7.71/1.47 fof(f104,plain,(
% 7.71/1.47 ![X0]: (store(a_420,i0,X0)=store(a_418,i0,X0))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f41,f36])).
% 7.71/1.47 fof(f107,plain,(
% 7.71/1.47 ![X0]: (store(a_440,i2,X0)=store(a_438,i2,X0))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f52,f36])).
% 7.71/1.47 fof(f108,plain,(
% 7.71/1.47 ![X0]: (store(a_430,i0,X0)=store(a_428,i0,X0))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f46,f36])).
% 7.71/1.47 fof(f121,plain,(
% 7.71/1.47 ![X0,X1]: (i0=X0|store(a_420,X0,X1)=store(store(a_418,X0,X1),i0,e_419))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f41,f38])).
% 7.71/1.47 fof(f174,plain,(
% 7.71/1.47 store(a_430,i0,select(a_428,i0))=a_428),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f35,f108])).
% 7.71/1.47 fof(f275,plain,(
% 7.71/1.47 e_425=select(a_418,i0)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f100,f55])).
% 7.71/1.47 fof(f282,plain,(
% 7.71/1.47 select(a_426,i2)=e_425),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f44,f32])).
% 7.71/1.47 fof(f283,plain,(
% 7.71/1.47 e_429=e_425),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f59,f282])).
% 7.71/1.47 fof(f284,plain,(
% 7.71/1.47 a_426=store(a_424,i2,e_429)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f283,f44])).
% 7.71/1.47 fof(f285,plain,(
% 7.71/1.47 e_429=select(a_418,i0)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f283,f275])).
% 7.71/1.47 fof(f286,plain,(
% 7.71/1.47 e_429=e_421),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f283,f100])).
% 7.71/1.47 fof(f287,plain,(
% 7.71/1.47 e_429=select(a_422,i3)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f283,f57])).
% 7.71/1.47 fof(f290,plain,(
% 7.71/1.47 ![X0,X1]: (X0=i2|store(store(a_426,X0,X1),i2,e_427)=store(a_428,X0,X1))),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f45,f38])).
% 7.71/1.47 fof(f294,plain,(
% 7.71/1.47 select(a_428,i2)=e_427),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f45,f32])).
% 7.71/1.47 fof(f298,plain,(
% 7.71/1.47 a_431=store(a_418,i3,e_429)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f286,f47])).
% 7.71/1.47 fof(f309,plain,(
% 7.71/1.47 select(a_432,i0)=e_419),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f48,f32])).
% 7.71/1.47 fof(f319,plain,(
% 7.71/1.47 select(a_436,i2)=e_435),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f50,f32])).
% 7.71/1.47 fof(f320,plain,(
% 7.71/1.47 e_437=e_435),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f62,f319])).
% 7.71/1.47 fof(f441,plain,(
% 7.71/1.47 a_436=store(a_434,i2,e_437)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f320,f50])).
% 7.71/1.47 fof(f442,plain,(
% 7.71/1.47 e_437=select(a_432,i3)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f320,f61])).
% 7.71/1.47 fof(f450,plain,(
% 7.71/1.47 select(a_438,i0)=e_437),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f51,f32])).
% 7.71/1.47 fof(f715,plain,(
% 7.71/1.47 store(a_422,i3,e_429)=a_422),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f283,f78])).
% 7.71/1.47 fof(f726,plain,(
% 7.71/1.47 store(a_418,i0,e_429)=a_418),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f286,f80])).
% 7.71/1.47 fof(f1208,plain,(
% 7.71/1.47 store(a_420,i0,e_429)=a_418),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f104,f726])).
% 7.71/1.47 fof(f3327,plain,(
% 7.71/1.47 i0=i3|store(a_420,i3,e_429)=store(a_431,i0,e_419)),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f298,f121])).
% 7.71/1.47 fof(f3370,plain,(
% 7.71/1.47 i0=i3|store(a_422,i3,e_429)=store(a_431,i0,e_419)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f103,f3327])).
% 7.71/1.47 fof(f3371,plain,(
% 7.71/1.47 i0=i3|a_422=store(a_431,i0,e_419)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f715,f3370])).
% 7.71/1.47 fof(f3372,plain,(
% 7.71/1.47 i0=i3|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f48,f3371])).
% 7.71/1.47 fof(f3755,plain,(
% 7.71/1.47 store(a_420,i3,e_429)=a_418|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3372,f1208])).
% 7.71/1.47 fof(f3780,plain,(
% 7.71/1.47 select(a_432,i3)=e_419|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3372,f309])).
% 7.71/1.47 fof(f3784,plain,(
% 7.71/1.47 e_429=select(a_418,i3)|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3372,f285])).
% 7.71/1.47 fof(f3797,plain,(
% 7.71/1.47 store(a_422,i3,e_429)=a_418|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f103,f3755])).
% 7.71/1.47 fof(f3798,plain,(
% 7.71/1.47 a_422=a_418|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f715,f3797])).
% 7.71/1.47 fof(f3800,plain,(
% 7.71/1.47 e_437=e_419|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f442,f3780])).
% 7.71/1.47 fof(f3801,plain,(
% 7.71/1.47 e_429=e_419|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f54,f3784])).
% 7.71/1.47 fof(f3810,plain,(
% 7.71/1.47 a_431=store(a_422,i3,e_429)|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3798,f298])).
% 7.71/1.47 fof(f3814,plain,(
% 7.71/1.47 a_431=a_422|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f715,f3810])).
% 7.71/1.47 fof(f3843,plain,(
% 7.71/1.47 e_429=e_437|a_422=a_432|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3800,f3801])).
% 7.71/1.47 fof(f3869,plain,(
% 7.71/1.47 store(a_420,i0,e_429)=a_420|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3801,f97])).
% 7.71/1.47 fof(f3870,plain,(
% 7.71/1.47 store(a_418,i3,e_429)=a_418|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3801,f81])).
% 7.71/1.47 fof(f3872,plain,(
% 7.71/1.47 e_429=e_437|a_422=a_432),
% 7.71/1.47 inference(duplicate_literals_removal,[status(thm)],[f3843])).
% 7.71/1.47 fof(f3878,plain,(
% 7.71/1.47 a_418=a_420|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f1208,f3869])).
% 7.71/1.47 fof(f3879,plain,(
% 7.71/1.47 a_431=a_418|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f298,f3870])).
% 7.71/1.47 fof(f3887,plain,(
% 7.71/1.47 ~a_431=a_432|a_422=a_432),
% 7.71/1.47 inference(equality_factoring,[status(thm)],[f3814])).
% 7.71/1.47 fof(f3895,plain,(
% 7.71/1.47 e_429=select(a_432,i3)|e_429=e_437),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3872,f287])).
% 7.71/1.47 fof(f3898,plain,(
% 7.71/1.47 e_429=e_437|e_429=e_437),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f442,f3895])).
% 7.71/1.47 fof(f3899,plain,(
% 7.71/1.47 e_429=e_437),
% 7.71/1.47 inference(duplicate_literals_removal,[status(thm)],[f3898])).
% 7.71/1.47 fof(f3929,plain,(
% 7.71/1.47 a_426=store(a_424,i2,e_437)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f3899,f284])).
% 7.71/1.47 fof(f3940,plain,(
% 7.71/1.47 store(a_430,i0,e_437)=a_430),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f3899,f82])).
% 7.71/1.47 fof(f4283,plain,(
% 7.71/1.47 a_431=a_420|a_422=a_432|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f3878,f3879])).
% 7.71/1.47 fof(f4298,plain,(
% 7.71/1.47 a_431=a_420|a_422=a_432),
% 7.71/1.47 inference(duplicate_literals_removal,[status(thm)],[f4283])).
% 7.71/1.47 fof(f4335,plain,(
% 7.71/1.47 store(a_431,i0,e_419)=a_420|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f4298,f97])).
% 7.71/1.47 fof(f4340,plain,(
% 7.71/1.47 a_432=a_420|a_422=a_432),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f48,f4335])).
% 7.71/1.47 fof(f4729,plain,(
% 7.71/1.47 a_432=a_431|a_422=a_432|a_422=a_432),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f4298,f4340])).
% 7.71/1.47 fof(f4739,plain,(
% 7.71/1.47 a_432=a_431|a_422=a_432),
% 7.71/1.47 inference(duplicate_literals_removal,[status(thm)],[f4729])).
% 7.71/1.47 fof(f4740,plain,(
% 7.71/1.47 a_422=a_432),
% 7.71/1.47 inference(forward_subsumption_resolution,[status(thm)],[f4739,f3887])).
% 7.71/1.47 fof(f4775,plain,(
% 7.71/1.47 a_424=store(a_432,i3,e_423)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4740,f43])).
% 7.71/1.47 fof(f4776,plain,(
% 7.71/1.47 e_423=select(a_432,i2)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4740,f56])).
% 7.71/1.47 fof(f4778,plain,(
% 7.71/1.47 e_423=e_433),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f60,f4776])).
% 7.71/1.47 fof(f4829,plain,(
% 7.71/1.47 a_424=store(a_432,i3,e_433)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f4778,f4775])).
% 7.71/1.47 fof(f4831,plain,(
% 7.71/1.47 a_426=store(a_434,i2,e_437)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4834,f3929])).
% 7.71/1.47 fof(f4834,plain,(
% 7.71/1.47 a_424=a_434),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f49,f4829])).
% 7.71/1.47 fof(f4835,plain,(
% 7.71/1.47 a_426=a_436),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f441,f4831])).
% 7.71/1.47 fof(f4840,plain,(
% 7.71/1.47 a_428=store(a_436,i2,e_427)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4835,f45])).
% 7.71/1.47 fof(f4841,plain,(
% 7.71/1.47 e_427=select(a_436,i0)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4835,f58])).
% 7.71/1.47 fof(f4844,plain,(
% 7.71/1.47 e_427=e_439),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f63,f4841])).
% 7.71/1.47 fof(f5249,plain,(
% 7.71/1.47 a_428=store(a_436,i2,e_439)),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4844,f4840])).
% 7.71/1.47 fof(f5275,plain,(
% 7.71/1.47 select(a_428,i2)=e_439),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f4844,f294])).
% 7.71/1.47 fof(f8500,plain,(
% 7.71/1.47 ![X0,X1]: (X0=i2|store(store(a_436,X0,X1),i2,e_427)=store(a_428,X0,X1))),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f4835,f290])).
% 7.71/1.47 fof(f8501,plain,(
% 7.71/1.47 ![X0,X1]: (X0=i2|store(store(a_436,X0,X1),i2,e_439)=store(a_428,X0,X1))),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f4844,f8500])).
% 7.71/1.47 fof(f8508,plain,(
% 7.71/1.47 i0=i2|store(a_438,i2,e_439)=store(a_428,i0,e_437)),
% 7.71/1.47 inference(paramodulation,[status(thm)],[f51,f8501])).
% 7.71/1.47 fof(f8535,plain,(
% 7.71/1.47 i0=i2|store(a_440,i2,e_439)=store(a_428,i0,e_437)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f107,f8508])).
% 7.71/1.47 fof(f8536,plain,(
% 7.71/1.47 i0=i2|a_440=store(a_428,i0,e_437)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f83,f8535])).
% 7.71/1.47 fof(f8537,plain,(
% 7.71/1.47 i0=i2|a_440=store(a_430,i0,e_437)),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f108,f8536])).
% 7.71/1.47 fof(f8538,plain,(
% 7.71/1.47 i0=i2|a_440=a_430),
% 7.71/1.47 inference(forward_demodulation,[status(thm)],[f3940,f8537])).
% 7.71/1.47 fof(f8539,plain,(
% 7.71/1.47 i0=i2),
% 7.71/1.47 inference(forward_subsumption_resolution,[status(thm)],[f8538,f64])).
% 7.71/1.47 fof(f8590,plain,(
% 7.71/1.47 store(a_430,i2,e_437)=a_430),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f8539,f3940])).
% 7.71/1.47 fof(f8615,plain,(
% 7.71/1.47 select(a_438,i2)=e_437),
% 7.71/1.47 inference(backward_demodulation,[status(thm)],[f8539,f450])).
% 7.71/1.48 fof(f8616,plain,(
% 7.71/1.48 a_438=store(a_436,i2,e_437)),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8539,f51])).
% 7.71/1.48 fof(f8622,plain,(
% 7.71/1.48 store(a_430,i0,select(a_428,i2))=a_428),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8539,f174])).
% 7.71/1.48 fof(f8626,plain,(
% 7.71/1.48 e_439=select(a_436,i2)),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8539,f63])).
% 7.71/1.48 fof(f8674,plain,(
% 7.71/1.48 store(a_430,i2,select(a_428,i2))=a_428),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f8539,f8622])).
% 7.71/1.48 fof(f8675,plain,(
% 7.71/1.48 store(a_430,i2,e_439)=a_428),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f5275,f8674])).
% 7.71/1.48 fof(f8734,plain,(
% 7.71/1.48 a_438=a_436),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8616,f72])).
% 7.71/1.48 fof(f8759,plain,(
% 7.71/1.48 a_428=store(a_438,i2,e_439)),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8734,f5249])).
% 7.71/1.48 fof(f8764,plain,(
% 7.71/1.48 a_428=store(a_440,i2,e_439)),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f107,f8759])).
% 7.71/1.48 fof(f8765,plain,(
% 7.71/1.48 a_428=a_440),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f83,f8764])).
% 7.71/1.48 fof(f8784,plain,(
% 7.71/1.48 e_439=e_437),
% 7.71/1.48 inference(backward_demodulation,[status(thm)],[f8785,f8615])).
% 7.71/1.48 fof(f8785,plain,(
% 7.71/1.48 e_439=select(a_438,i2)),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f8734,f8626])).
% 7.71/1.48 fof(f8912,plain,(
% 7.71/1.48 store(a_430,i2,e_439)=a_430),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f8784,f8590])).
% 7.71/1.48 fof(f8950,plain,(
% 7.71/1.48 a_430=a_428),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f8912,f8675])).
% 7.71/1.48 fof(f8951,plain,(
% 7.71/1.48 a_430=a_440),
% 7.71/1.48 inference(forward_demodulation,[status(thm)],[f8765,f8950])).
% 7.71/1.48 fof(f8952,plain,(
% 7.71/1.48 $false),
% 7.71/1.48 inference(forward_subsumption_resolution,[status(thm)],[f8951,f64])).
% 7.71/1.48 % SZS output end CNFRefutation for theBenchmark.p
% 3.41/1.51 % Elapsed time: 1.131563 seconds
% 3.41/1.51 % CPU time: 8.696574 seconds
% 3.41/1.51 % Total memory used: 195.978 MB
% 3.41/1.51 % Net memory used: 173.273 MB
%------------------------------------------------------------------------------