%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV543-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:38 PM UTC 2026
% Result : Unsatisfiable 1.39s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n003.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 09:06:15 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 1.39/0.63 % Refutation found
% 1.39/0.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.39/0.63 % SZS output start CNFRefutation for theBenchmark
% 1.39/0.63 fof(f1,axiom,(
% 1.39/0.63 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f3,axiom,(
% 1.39/0.63 (![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)) ))),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f6,hypothesis,(
% 1.39/0.63 a_420 = store(a_418,i0,e_419) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f7,hypothesis,(
% 1.39/0.63 a_422 = store(a_420,i3,e_421) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f8,hypothesis,(
% 1.39/0.63 a_424 = store(a_422,i3,e_423) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f9,hypothesis,(
% 1.39/0.63 a_426 = store(a_424,i2,e_425) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f10,hypothesis,(
% 1.39/0.63 a_428 = store(a_426,i2,e_427) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f11,hypothesis,(
% 1.39/0.63 a_430 = store(a_428,i0,e_429) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f12,hypothesis,(
% 1.39/0.63 a_431 = store(a_418,i3,e_421) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f13,hypothesis,(
% 1.39/0.63 a_432 = store(a_431,i0,e_419) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f14,hypothesis,(
% 1.39/0.63 a_434 = store(a_432,i3,e_433) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f15,hypothesis,(
% 1.39/0.63 a_436 = store(a_434,i2,e_435) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f16,hypothesis,(
% 1.39/0.63 a_438 = store(a_436,i0,e_437) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f17,hypothesis,(
% 1.39/0.63 a_440 = store(a_438,i2,e_439) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f19,hypothesis,(
% 1.39/0.63 e_419 = select(a_418,i3) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f20,hypothesis,(
% 1.39/0.63 e_421 = select(a_418,i0) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f21,hypothesis,(
% 1.39/0.63 e_423 = select(a_422,i2) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f22,hypothesis,(
% 1.39/0.63 e_425 = select(a_422,i3) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f23,hypothesis,(
% 1.39/0.63 e_427 = select(a_426,i0) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f24,hypothesis,(
% 1.39/0.63 e_429 = select(a_426,i2) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f25,hypothesis,(
% 1.39/0.63 e_433 = select(a_432,i2) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f26,hypothesis,(
% 1.39/0.63 e_435 = select(a_432,i3) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f27,hypothesis,(
% 1.39/0.63 e_437 = select(a_436,i2) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f28,hypothesis,(
% 1.39/0.63 e_439 = select(a_436,i0) ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f29,negated_conjecture,(
% 1.39/0.63 a_430 != a_440 ),
% 1.39/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.39/0.63 fof(f30,plain,(
% 1.39/0.63 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f1])).
% 1.39/0.63 fof(f33,plain,(
% 1.39/0.63 ![X0,X1,X2]: (store(store(X0,X1,select(X0,X2)),X2,select(X0,X1))=store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)))),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f3])).
% 1.39/0.63 fof(f36,plain,(
% 1.39/0.63 a_420=store(a_418,i0,e_419)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f6])).
% 1.39/0.63 fof(f37,plain,(
% 1.39/0.63 a_422=store(a_420,i3,e_421)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f7])).
% 1.39/0.63 fof(f38,plain,(
% 1.39/0.63 a_424=store(a_422,i3,e_423)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f8])).
% 1.39/0.63 fof(f39,plain,(
% 1.39/0.63 a_426=store(a_424,i2,e_425)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f9])).
% 1.39/0.63 fof(f40,plain,(
% 1.39/0.63 a_428=store(a_426,i2,e_427)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f10])).
% 1.39/0.63 fof(f41,plain,(
% 1.39/0.63 a_430=store(a_428,i0,e_429)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f11])).
% 1.39/0.63 fof(f42,plain,(
% 1.39/0.63 a_431=store(a_418,i3,e_421)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f12])).
% 1.39/0.63 fof(f43,plain,(
% 1.39/0.63 a_432=store(a_431,i0,e_419)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f13])).
% 1.39/0.63 fof(f44,plain,(
% 1.39/0.63 a_434=store(a_432,i3,e_433)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f14])).
% 1.39/0.63 fof(f45,plain,(
% 1.39/0.63 a_436=store(a_434,i2,e_435)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f15])).
% 1.39/0.63 fof(f46,plain,(
% 1.39/0.63 a_438=store(a_436,i0,e_437)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f16])).
% 1.39/0.63 fof(f47,plain,(
% 1.39/0.63 a_440=store(a_438,i2,e_439)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f17])).
% 1.39/0.63 fof(f49,plain,(
% 1.39/0.63 e_419=select(a_418,i3)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f19])).
% 1.39/0.63 fof(f50,plain,(
% 1.39/0.63 e_421=select(a_418,i0)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f20])).
% 1.39/0.63 fof(f51,plain,(
% 1.39/0.63 e_423=select(a_422,i2)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f21])).
% 1.39/0.63 fof(f52,plain,(
% 1.39/0.63 e_425=select(a_422,i3)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f22])).
% 1.39/0.63 fof(f53,plain,(
% 1.39/0.63 e_427=select(a_426,i0)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f23])).
% 1.39/0.63 fof(f54,plain,(
% 1.39/0.63 e_429=select(a_426,i2)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f24])).
% 1.39/0.63 fof(f55,plain,(
% 1.39/0.63 e_433=select(a_432,i2)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f25])).
% 1.39/0.63 fof(f56,plain,(
% 1.39/0.63 e_435=select(a_432,i3)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f26])).
% 1.39/0.63 fof(f57,plain,(
% 1.39/0.63 e_437=select(a_436,i2)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f27])).
% 1.39/0.63 fof(f58,plain,(
% 1.39/0.63 e_439=select(a_436,i0)),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f28])).
% 1.39/0.63 fof(f59,plain,(
% 1.39/0.63 ~a_430=a_440),
% 1.39/0.63 inference(cnf_transformation,[status(thm)],[f29])).
% 1.39/0.63 fof(f74,plain,(
% 1.39/0.63 ![X0]: (store(store(a_418,X0,e_421),i0,select(a_418,X0))=store(store(a_418,i0,select(a_418,X0)),X0,select(a_418,i0)))),
% 1.39/0.63 inference(paramodulation,[status(thm)],[f50,f33])).
% 1.39/0.63 fof(f115,plain,(
% 1.39/0.63 ![X0]: (store(store(a_418,X0,e_421),i0,select(a_418,X0))=store(store(a_418,i0,select(a_418,X0)),X0,e_421))),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f50,f74])).
% 1.39/0.63 fof(f149,plain,(
% 1.39/0.63 select(a_422,i3)=e_421),
% 1.39/0.63 inference(paramodulation,[status(thm)],[f37,f30])).
% 1.39/0.63 fof(f202,plain,(
% 1.39/0.63 ![X0]: (store(store(a_426,X0,select(a_426,i2)),i2,select(a_426,X0))=store(store(a_426,i2,select(a_426,X0)),X0,e_429))),
% 1.39/0.63 inference(paramodulation,[status(thm)],[f54,f33])).
% 1.39/0.63 fof(f206,plain,(
% 1.39/0.63 ![X0]: (store(store(a_426,X0,e_429),i2,select(a_426,X0))=store(store(a_426,i2,select(a_426,X0)),X0,e_429))),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f54,f202])).
% 1.39/0.63 fof(f219,plain,(
% 1.39/0.63 select(a_426,i2)=e_425),
% 1.39/0.63 inference(paramodulation,[status(thm)],[f39,f30])).
% 1.39/0.63 fof(f845,plain,(
% 1.39/0.63 store(store(a_418,i3,e_421),i0,select(a_418,i3))=store(store(a_418,i0,e_419),i3,e_421)),
% 1.39/0.63 inference(paramodulation,[status(thm)],[f49,f115])).
% 1.39/0.63 fof(f853,plain,(
% 1.39/0.63 store(a_431,i0,select(a_418,i3))=store(store(a_418,i0,e_419),i3,e_421)),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f42,f845])).
% 1.39/0.63 fof(f854,plain,(
% 1.39/0.63 store(a_431,i0,e_419)=store(store(a_418,i0,e_419),i3,e_421)),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f49,f853])).
% 1.39/0.63 fof(f855,plain,(
% 1.39/0.63 a_432=store(store(a_418,i0,e_419),i3,e_421)),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f43,f854])).
% 1.39/0.63 fof(f856,plain,(
% 1.39/0.63 a_432=store(a_420,i3,e_421)),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f36,f855])).
% 1.39/0.63 fof(f857,plain,(
% 1.39/0.63 a_432=a_422),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f37,f856])).
% 1.39/0.63 fof(f999,plain,(
% 1.39/0.63 e_435=select(a_422,i3)),
% 1.39/0.63 inference(backward_demodulation,[status(thm)],[f857,f56])).
% 1.39/0.63 fof(f1000,plain,(
% 1.39/0.63 a_434=store(a_422,i3,e_433)),
% 1.39/0.63 inference(backward_demodulation,[status(thm)],[f857,f44])).
% 1.39/0.63 fof(f1002,plain,(
% 1.39/0.63 e_433=select(a_422,i2)),
% 1.39/0.63 inference(backward_demodulation,[status(thm)],[f857,f55])).
% 1.39/0.63 fof(f1003,plain,(
% 1.39/0.63 e_435=e_425),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f52,f999])).
% 1.39/0.63 fof(f1004,plain,(
% 1.39/0.63 e_433=e_423),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f51,f1002])).
% 1.39/0.63 fof(f1005,plain,(
% 1.39/0.63 a_436=store(a_434,i2,e_425)),
% 1.39/0.63 inference(backward_demodulation,[status(thm)],[f1003,f45])).
% 1.39/0.63 fof(f1006,plain,(
% 1.39/0.63 a_434=store(a_422,i3,e_423)),
% 1.39/0.63 inference(forward_demodulation,[status(thm)],[f1004,f1000])).
% 1.39/0.63 fof(f1007,plain,(
% 1.39/0.65 a_434=a_424),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f38,f1006])).
% 1.39/0.65 fof(f1033,plain,(
% 1.39/0.65 a_436=store(a_424,i2,e_425)),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f1007,f1005])).
% 1.39/0.65 fof(f1034,plain,(
% 1.39/0.65 a_438=store(a_426,i0,e_437)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f1037,f46])).
% 1.39/0.65 fof(f1035,plain,(
% 1.39/0.65 e_439=select(a_426,i0)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f1037,f58])).
% 1.39/0.65 fof(f1036,plain,(
% 1.39/0.65 e_437=select(a_426,i2)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f1037,f57])).
% 1.39/0.65 fof(f1037,plain,(
% 1.39/0.65 a_436=a_426),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f39,f1033])).
% 1.39/0.65 fof(f1038,plain,(
% 1.39/0.65 e_439=e_427),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f53,f1035])).
% 1.39/0.65 fof(f1039,plain,(
% 1.39/0.65 e_437=e_429),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f54,f1036])).
% 1.39/0.65 fof(f1069,plain,(
% 1.39/0.65 a_440=store(a_438,i2,e_427)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f1038,f47])).
% 1.39/0.65 fof(f1073,plain,(
% 1.39/0.65 a_438=store(a_426,i0,e_429)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f1039,f1034])).
% 1.39/0.65 fof(f1742,plain,(
% 1.39/0.65 e_425=e_421),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f149,f52])).
% 1.39/0.65 fof(f2042,plain,(
% 1.39/0.65 e_429=e_421),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f2043,f54])).
% 1.39/0.65 fof(f2043,plain,(
% 1.39/0.65 select(a_426,i2)=e_421),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f1742,f219])).
% 1.39/0.65 fof(f2054,plain,(
% 1.39/0.65 a_438=store(a_426,i0,e_421)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f2042,f1073])).
% 1.39/0.65 fof(f2060,plain,(
% 1.39/0.65 a_430=store(a_428,i0,e_421)),
% 1.39/0.65 inference(backward_demodulation,[status(thm)],[f2042,f41])).
% 1.39/0.65 fof(f3141,plain,(
% 1.39/0.65 ![X0]: (store(store(a_426,X0,e_421),i2,select(a_426,X0))=store(store(a_426,i2,select(a_426,X0)),X0,e_429))),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f2042,f206])).
% 1.39/0.65 fof(f3142,plain,(
% 1.39/0.65 ![X0]: (store(store(a_426,X0,e_421),i2,select(a_426,X0))=store(store(a_426,i2,select(a_426,X0)),X0,e_421))),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f2042,f3141])).
% 1.39/0.65 fof(f3144,plain,(
% 1.39/0.65 store(store(a_426,i0,e_421),i2,select(a_426,i0))=store(store(a_426,i2,e_427),i0,e_421)),
% 1.39/0.65 inference(paramodulation,[status(thm)],[f53,f3142])).
% 1.39/0.65 fof(f3155,plain,(
% 1.39/0.65 store(a_438,i2,select(a_426,i0))=store(store(a_426,i2,e_427),i0,e_421)),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f2054,f3144])).
% 1.39/0.65 fof(f3156,plain,(
% 1.39/0.65 store(a_438,i2,e_427)=store(store(a_426,i2,e_427),i0,e_421)),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f53,f3155])).
% 1.39/0.65 fof(f3157,plain,(
% 1.39/0.65 a_440=store(store(a_426,i2,e_427),i0,e_421)),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f1069,f3156])).
% 1.39/0.65 fof(f3158,plain,(
% 1.39/0.65 a_440=store(a_428,i0,e_421)),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f40,f3157])).
% 1.39/0.65 fof(f3159,plain,(
% 1.39/0.65 a_440=a_430),
% 1.39/0.65 inference(forward_demodulation,[status(thm)],[f2060,f3158])).
% 1.39/0.65 fof(f3160,plain,(
% 1.39/0.65 $false),
% 1.39/0.65 inference(forward_subsumption_resolution,[status(thm)],[f3159,f59])).
% 1.39/0.65 % SZS output end CNFRefutation for theBenchmark.p
% 1.39/0.67 % Elapsed time: 0.302874 seconds
% 1.39/0.67 % CPU time: 2.109652 seconds
% 1.39/0.67 % Total memory used: 150.496 MB
% 1.39/0.67 % Net memory used: 147.027 MB
%------------------------------------------------------------------------------