%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV543-1.007 : 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 : n001.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 5.44s 1.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:10:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 5.44/1.27 % Refutation found
% 5.44/1.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.44/1.27 % SZS output start CNFRefutation for theBenchmark
% 5.44/1.27 fof(f1,axiom,(
% 5.44/1.27 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f3,axiom,(
% 5.44/1.27 (![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)) ))),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f6,hypothesis,(
% 5.44/1.27 a_787 = store(a_785,i2,e_786) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f7,hypothesis,(
% 5.44/1.27 a_789 = store(a_787,i1,e_788) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f8,hypothesis,(
% 5.44/1.27 a_791 = store(a_789,i0,e_790) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f9,hypothesis,(
% 5.44/1.27 a_793 = store(a_791,i5,e_792) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f10,hypothesis,(
% 5.44/1.27 a_795 = store(a_793,i2,e_794) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f11,hypothesis,(
% 5.44/1.27 a_797 = store(a_795,i5,e_796) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f12,hypothesis,(
% 5.44/1.27 a_799 = store(a_797,i1,e_798) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f13,hypothesis,(
% 5.44/1.27 a_800 = store(a_799,i1,e_798) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f14,hypothesis,(
% 5.44/1.27 a_802 = store(a_800,i5,e_801) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f15,hypothesis,(
% 5.44/1.27 a_804 = store(a_802,i2,e_803) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f16,hypothesis,(
% 5.44/1.27 a_806 = store(a_804,i5,e_805) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f17,hypothesis,(
% 5.44/1.27 a_808 = store(a_806,i2,e_807) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f18,hypothesis,(
% 5.44/1.27 a_809 = store(a_785,i1,e_788) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f19,hypothesis,(
% 5.44/1.27 a_810 = store(a_809,i2,e_786) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f20,hypothesis,(
% 5.44/1.27 a_812 = store(a_810,i5,e_811) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f21,hypothesis,(
% 5.44/1.27 a_814 = store(a_812,i0,e_813) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f22,hypothesis,(
% 5.44/1.27 a_816 = store(a_814,i5,e_815) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f23,hypothesis,(
% 5.44/1.27 a_818 = store(a_816,i2,e_817) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f24,hypothesis,(
% 5.44/1.27 a_820 = store(a_818,i1,e_819) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f25,hypothesis,(
% 5.44/1.27 a_821 = store(a_820,i1,e_819) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f26,hypothesis,(
% 5.44/1.27 a_823 = store(a_821,i5,e_822) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f27,hypothesis,(
% 5.44/1.27 a_825 = store(a_823,i2,e_824) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f28,hypothesis,(
% 5.44/1.27 a_827 = store(a_825,i5,e_826) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f29,hypothesis,(
% 5.44/1.27 a_829 = store(a_827,i2,e_828) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f32,hypothesis,(
% 5.44/1.27 e_786 = select(a_785,i1) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f33,hypothesis,(
% 5.44/1.27 e_788 = select(a_785,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f34,hypothesis,(
% 5.44/1.27 e_790 = select(a_789,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f35,hypothesis,(
% 5.44/1.27 e_792 = select(a_789,i0) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f36,hypothesis,(
% 5.44/1.27 e_794 = select(a_793,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f37,hypothesis,(
% 5.44/1.27 e_796 = select(a_793,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f38,hypothesis,(
% 5.44/1.27 e_798 = select(a_797,i1) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f39,hypothesis,(
% 5.44/1.27 e_801 = select(a_800,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f40,hypothesis,(
% 5.44/1.27 e_803 = select(a_800,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f41,hypothesis,(
% 5.44/1.27 e_805 = select(a_804,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f42,hypothesis,(
% 5.44/1.27 e_807 = select(a_804,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f43,hypothesis,(
% 5.44/1.27 e_811 = select(a_810,i0) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f44,hypothesis,(
% 5.44/1.27 e_813 = select(a_810,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f45,hypothesis,(
% 5.44/1.27 e_815 = select(a_814,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f46,hypothesis,(
% 5.44/1.27 e_817 = select(a_814,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f47,hypothesis,(
% 5.44/1.27 e_819 = select(a_818,i1) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f48,hypothesis,(
% 5.44/1.27 e_822 = select(a_821,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f49,hypothesis,(
% 5.44/1.27 e_824 = select(a_821,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f50,hypothesis,(
% 5.44/1.27 e_826 = select(a_825,i2) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f51,hypothesis,(
% 5.44/1.27 e_828 = select(a_825,i5) ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f52,negated_conjecture,(
% 5.44/1.27 a_808 != a_829 ),
% 5.44/1.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.44/1.27 fof(f53,plain,(
% 5.44/1.27 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f1])).
% 5.44/1.27 fof(f56,plain,(
% 5.44/1.27 ![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)))),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f3])).
% 5.44/1.27 fof(f59,plain,(
% 5.44/1.27 a_787=store(a_785,i2,e_786)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f6])).
% 5.44/1.27 fof(f60,plain,(
% 5.44/1.27 a_789=store(a_787,i1,e_788)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f7])).
% 5.44/1.27 fof(f61,plain,(
% 5.44/1.27 a_791=store(a_789,i0,e_790)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f8])).
% 5.44/1.27 fof(f62,plain,(
% 5.44/1.27 a_793=store(a_791,i5,e_792)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f9])).
% 5.44/1.27 fof(f63,plain,(
% 5.44/1.27 a_795=store(a_793,i2,e_794)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f10])).
% 5.44/1.27 fof(f64,plain,(
% 5.44/1.27 a_797=store(a_795,i5,e_796)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f11])).
% 5.44/1.27 fof(f65,plain,(
% 5.44/1.27 a_799=store(a_797,i1,e_798)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f12])).
% 5.44/1.27 fof(f66,plain,(
% 5.44/1.27 a_800=store(a_799,i1,e_798)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f13])).
% 5.44/1.27 fof(f67,plain,(
% 5.44/1.27 a_802=store(a_800,i5,e_801)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f14])).
% 5.44/1.27 fof(f68,plain,(
% 5.44/1.27 a_804=store(a_802,i2,e_803)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f15])).
% 5.44/1.27 fof(f69,plain,(
% 5.44/1.27 a_806=store(a_804,i5,e_805)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f16])).
% 5.44/1.27 fof(f70,plain,(
% 5.44/1.27 a_808=store(a_806,i2,e_807)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f17])).
% 5.44/1.27 fof(f71,plain,(
% 5.44/1.27 a_809=store(a_785,i1,e_788)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f18])).
% 5.44/1.27 fof(f72,plain,(
% 5.44/1.27 a_810=store(a_809,i2,e_786)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f19])).
% 5.44/1.27 fof(f73,plain,(
% 5.44/1.27 a_812=store(a_810,i5,e_811)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f20])).
% 5.44/1.27 fof(f74,plain,(
% 5.44/1.27 a_814=store(a_812,i0,e_813)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f21])).
% 5.44/1.27 fof(f75,plain,(
% 5.44/1.27 a_816=store(a_814,i5,e_815)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f22])).
% 5.44/1.27 fof(f76,plain,(
% 5.44/1.27 a_818=store(a_816,i2,e_817)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f23])).
% 5.44/1.27 fof(f77,plain,(
% 5.44/1.27 a_820=store(a_818,i1,e_819)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f24])).
% 5.44/1.27 fof(f78,plain,(
% 5.44/1.27 a_821=store(a_820,i1,e_819)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f25])).
% 5.44/1.27 fof(f79,plain,(
% 5.44/1.27 a_823=store(a_821,i5,e_822)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f26])).
% 5.44/1.27 fof(f80,plain,(
% 5.44/1.27 a_825=store(a_823,i2,e_824)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f27])).
% 5.44/1.27 fof(f81,plain,(
% 5.44/1.27 a_827=store(a_825,i5,e_826)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f28])).
% 5.44/1.27 fof(f82,plain,(
% 5.44/1.27 a_829=store(a_827,i2,e_828)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f29])).
% 5.44/1.27 fof(f85,plain,(
% 5.44/1.27 e_786=select(a_785,i1)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f32])).
% 5.44/1.27 fof(f86,plain,(
% 5.44/1.27 e_788=select(a_785,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f33])).
% 5.44/1.27 fof(f87,plain,(
% 5.44/1.27 e_790=select(a_789,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f34])).
% 5.44/1.27 fof(f88,plain,(
% 5.44/1.27 e_792=select(a_789,i0)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f35])).
% 5.44/1.27 fof(f89,plain,(
% 5.44/1.27 e_794=select(a_793,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f36])).
% 5.44/1.27 fof(f90,plain,(
% 5.44/1.27 e_796=select(a_793,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f37])).
% 5.44/1.27 fof(f91,plain,(
% 5.44/1.27 e_798=select(a_797,i1)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f38])).
% 5.44/1.27 fof(f92,plain,(
% 5.44/1.27 e_801=select(a_800,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f39])).
% 5.44/1.27 fof(f93,plain,(
% 5.44/1.27 e_803=select(a_800,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f40])).
% 5.44/1.27 fof(f94,plain,(
% 5.44/1.27 e_805=select(a_804,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f41])).
% 5.44/1.27 fof(f95,plain,(
% 5.44/1.27 e_807=select(a_804,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f42])).
% 5.44/1.27 fof(f96,plain,(
% 5.44/1.27 e_811=select(a_810,i0)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f43])).
% 5.44/1.27 fof(f97,plain,(
% 5.44/1.27 e_813=select(a_810,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f44])).
% 5.44/1.27 fof(f98,plain,(
% 5.44/1.27 e_815=select(a_814,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f45])).
% 5.44/1.27 fof(f99,plain,(
% 5.44/1.27 e_817=select(a_814,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f46])).
% 5.44/1.27 fof(f100,plain,(
% 5.44/1.27 e_819=select(a_818,i1)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f47])).
% 5.44/1.27 fof(f101,plain,(
% 5.44/1.27 e_822=select(a_821,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f48])).
% 5.44/1.27 fof(f102,plain,(
% 5.44/1.27 e_824=select(a_821,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f49])).
% 5.44/1.27 fof(f103,plain,(
% 5.44/1.27 e_826=select(a_825,i2)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f50])).
% 5.44/1.27 fof(f104,plain,(
% 5.44/1.27 e_828=select(a_825,i5)),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f51])).
% 5.44/1.27 fof(f105,plain,(
% 5.44/1.27 ~a_808=a_829),
% 5.44/1.27 inference(cnf_transformation,[status(thm)],[f52])).
% 5.44/1.27 fof(f128,plain,(
% 5.44/1.27 ![X0]: (store(store(a_825,X0,e_828),i5,select(a_825,X0))=store(store(a_825,i5,select(a_825,X0)),X0,select(a_825,i5)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f104,f56])).
% 5.44/1.27 fof(f130,plain,(
% 5.44/1.27 ![X0]: (store(store(a_821,X0,e_824),i5,select(a_821,X0))=store(store(a_821,i5,select(a_821,X0)),X0,select(a_821,i5)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f102,f56])).
% 5.44/1.27 fof(f135,plain,(
% 5.44/1.27 ![X0]: (store(store(a_810,X0,e_813),i5,select(a_810,X0))=store(store(a_810,i5,select(a_810,X0)),X0,select(a_810,i5)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f97,f56])).
% 5.44/1.27 fof(f137,plain,(
% 5.44/1.27 ![X0]: (store(store(a_804,X0,e_807),i5,select(a_804,X0))=store(store(a_804,i5,select(a_804,X0)),X0,select(a_804,i5)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f95,f56])).
% 5.44/1.27 fof(f139,plain,(
% 5.44/1.27 ![X0]: (store(store(a_800,X0,e_803),i5,select(a_800,X0))=store(store(a_800,i5,select(a_800,X0)),X0,select(a_800,i5)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f93,f56])).
% 5.44/1.27 fof(f142,plain,(
% 5.44/1.27 ![X0]: (store(store(a_793,X0,e_796),i2,select(a_793,X0))=store(store(a_793,i2,select(a_793,X0)),X0,select(a_793,i2)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f90,f56])).
% 5.44/1.27 fof(f145,plain,(
% 5.44/1.27 ![X0]: (store(store(a_789,X0,e_792),i0,select(a_789,X0))=store(store(a_789,i0,select(a_789,X0)),X0,select(a_789,i0)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f88,f56])).
% 5.44/1.27 fof(f153,plain,(
% 5.44/1.27 ![X0]: (store(store(a_785,X0,e_788),i2,select(a_785,X0))=store(store(a_785,i2,select(a_785,X0)),X0,select(a_785,i2)))),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f86,f56])).
% 5.44/1.27 fof(f258,plain,(
% 5.44/1.27 ![X0]: (store(store(a_825,X0,e_828),i5,select(a_825,X0))=store(store(a_825,i5,select(a_825,X0)),X0,e_828))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f104,f128])).
% 5.44/1.27 fof(f260,plain,(
% 5.44/1.27 ![X0]: (store(store(a_821,X0,e_824),i5,select(a_821,X0))=store(store(a_821,i5,select(a_821,X0)),X0,e_824))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f102,f130])).
% 5.44/1.27 fof(f265,plain,(
% 5.44/1.27 ![X0]: (store(store(a_810,X0,e_813),i5,select(a_810,X0))=store(store(a_810,i5,select(a_810,X0)),X0,e_813))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f97,f135])).
% 5.44/1.27 fof(f267,plain,(
% 5.44/1.27 ![X0]: (store(store(a_804,X0,e_807),i5,select(a_804,X0))=store(store(a_804,i5,select(a_804,X0)),X0,e_807))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f95,f137])).
% 5.44/1.27 fof(f269,plain,(
% 5.44/1.27 ![X0]: (store(store(a_800,X0,e_803),i5,select(a_800,X0))=store(store(a_800,i5,select(a_800,X0)),X0,e_803))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f93,f139])).
% 5.44/1.27 fof(f272,plain,(
% 5.44/1.27 ![X0]: (store(store(a_793,X0,e_796),i2,select(a_793,X0))=store(store(a_793,i2,select(a_793,X0)),X0,e_796))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f90,f142])).
% 5.44/1.27 fof(f275,plain,(
% 5.44/1.27 ![X0]: (store(store(a_789,X0,e_792),i0,select(a_789,X0))=store(store(a_789,i0,select(a_789,X0)),X0,e_792))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f88,f145])).
% 5.44/1.27 fof(f281,plain,(
% 5.44/1.27 ![X0]: (store(store(a_785,X0,e_788),i2,select(a_785,X0))=store(store(a_785,i2,select(a_785,X0)),X0,e_788))),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f86,f153])).
% 5.44/1.27 fof(f373,plain,(
% 5.44/1.27 select(a_793,i5)=e_792),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f62,f53])).
% 5.44/1.27 fof(f540,plain,(
% 5.44/1.27 e_794=e_792),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f373,f89])).
% 5.44/1.27 fof(f549,plain,(
% 5.44/1.27 a_795=store(a_793,i2,e_792)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f540,f63])).
% 5.44/1.27 fof(f600,plain,(
% 5.44/1.27 select(a_804,i2)=e_803),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f68,f53])).
% 5.44/1.27 fof(f601,plain,(
% 5.44/1.27 e_805=e_803),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f600,f94])).
% 5.44/1.27 fof(f610,plain,(
% 5.44/1.27 a_806=store(a_804,i5,e_803)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f601,f69])).
% 5.44/1.27 fof(f942,plain,(
% 5.44/1.27 select(a_825,i2)=e_824),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f80,f53])).
% 5.44/1.27 fof(f943,plain,(
% 5.44/1.27 e_826=e_824),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f942,f103])).
% 5.44/1.27 fof(f952,plain,(
% 5.44/1.27 a_827=store(a_825,i5,e_824)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f943,f81])).
% 5.44/1.27 fof(f1303,plain,(
% 5.44/1.27 store(store(a_825,i2,e_828),i5,select(a_825,i2))=store(store(a_825,i5,e_824),i2,e_828)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f942,f258])).
% 5.44/1.27 fof(f1306,plain,(
% 5.44/1.27 store(store(a_825,i2,e_828),i5,e_824)=store(store(a_825,i5,e_824),i2,e_828)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f942,f1303])).
% 5.44/1.27 fof(f1307,plain,(
% 5.44/1.27 store(store(a_825,i2,e_828),i5,e_824)=store(a_827,i2,e_828)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f952,f1306])).
% 5.44/1.27 fof(f1308,plain,(
% 5.44/1.27 store(store(a_825,i2,e_828),i5,e_824)=a_829),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f82,f1307])).
% 5.44/1.27 fof(f1320,plain,(
% 5.44/1.27 store(store(a_821,i2,e_824),i5,select(a_821,i2))=store(store(a_821,i5,e_822),i2,e_824)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f101,f260])).
% 5.44/1.27 fof(f1324,plain,(
% 5.44/1.27 store(store(a_821,i2,e_824),i5,e_822)=store(store(a_821,i5,e_822),i2,e_824)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f101,f1320])).
% 5.44/1.27 fof(f1325,plain,(
% 5.44/1.27 store(store(a_821,i2,e_824),i5,e_822)=store(a_823,i2,e_824)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f79,f1324])).
% 5.44/1.27 fof(f1326,plain,(
% 5.44/1.27 store(store(a_821,i2,e_824),i5,e_822)=a_825),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f80,f1325])).
% 5.44/1.27 fof(f2088,plain,(
% 5.44/1.27 store(store(a_810,i0,e_813),i5,select(a_810,i0))=store(store(a_810,i5,e_811),i0,e_813)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f96,f265])).
% 5.44/1.27 fof(f2093,plain,(
% 5.44/1.27 store(store(a_810,i0,e_813),i5,e_811)=store(store(a_810,i5,e_811),i0,e_813)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f96,f2088])).
% 5.44/1.27 fof(f2094,plain,(
% 5.44/1.27 store(store(a_810,i0,e_813),i5,e_811)=store(a_812,i0,e_813)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f73,f2093])).
% 5.44/1.27 fof(f2095,plain,(
% 5.44/1.27 store(store(a_810,i0,e_813),i5,e_811)=a_814),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f74,f2094])).
% 5.44/1.27 fof(f2391,plain,(
% 5.44/1.27 store(store(a_804,i2,e_807),i5,select(a_804,i2))=store(store(a_804,i5,e_803),i2,e_807)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f600,f267])).
% 5.44/1.27 fof(f2397,plain,(
% 5.44/1.27 store(store(a_804,i2,e_807),i5,e_803)=store(store(a_804,i5,e_803),i2,e_807)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f600,f2391])).
% 5.44/1.27 fof(f2398,plain,(
% 5.44/1.27 store(store(a_804,i2,e_807),i5,e_803)=store(a_806,i2,e_807)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f610,f2397])).
% 5.44/1.27 fof(f2399,plain,(
% 5.44/1.27 store(store(a_804,i2,e_807),i5,e_803)=a_808),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f70,f2398])).
% 5.44/1.27 fof(f2413,plain,(
% 5.44/1.27 store(store(a_800,i2,e_803),i5,select(a_800,i2))=store(store(a_800,i5,e_801),i2,e_803)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f92,f269])).
% 5.44/1.27 fof(f2419,plain,(
% 5.44/1.27 store(store(a_800,i2,e_803),i5,e_801)=store(store(a_800,i5,e_801),i2,e_803)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f92,f2413])).
% 5.44/1.27 fof(f2420,plain,(
% 5.44/1.27 store(store(a_800,i2,e_803),i5,e_801)=store(a_802,i2,e_803)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f67,f2419])).
% 5.44/1.27 fof(f2421,plain,(
% 5.44/1.27 store(store(a_800,i2,e_803),i5,e_801)=a_804),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f68,f2420])).
% 5.44/1.27 fof(f2724,plain,(
% 5.44/1.27 select(a_825,i5)=e_822),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f1326,f53])).
% 5.44/1.27 fof(f2725,plain,(
% 5.44/1.27 e_828=e_822),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f2724,f104])).
% 5.44/1.27 fof(f2752,plain,(
% 5.44/1.27 store(store(a_825,i2,e_822),i5,e_824)=a_829),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f2725,f1308])).
% 5.44/1.27 fof(f2857,plain,(
% 5.44/1.27 store(store(a_793,i5,e_796),i2,select(a_793,i5))=store(store(a_793,i2,e_792),i5,e_796)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f373,f272])).
% 5.44/1.27 fof(f2861,plain,(
% 5.44/1.27 store(store(a_793,i5,e_796),i2,e_792)=store(store(a_793,i2,e_792),i5,e_796)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f373,f2857])).
% 5.44/1.27 fof(f2862,plain,(
% 5.44/1.27 store(store(a_793,i5,e_796),i2,e_792)=store(a_795,i5,e_796)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f549,f2861])).
% 5.44/1.27 fof(f2863,plain,(
% 5.44/1.27 store(store(a_793,i5,e_796),i2,e_792)=a_797),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f64,f2862])).
% 5.44/1.27 fof(f3066,plain,(
% 5.44/1.27 select(a_814,i5)=e_811),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f2095,f53])).
% 5.44/1.27 fof(f3081,plain,(
% 5.44/1.27 store(store(a_789,i5,e_792),i0,select(a_789,i5))=store(store(a_789,i0,e_790),i5,e_792)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f87,f275])).
% 5.44/1.27 fof(f3086,plain,(
% 5.44/1.27 store(store(a_789,i5,e_792),i0,e_790)=store(store(a_789,i0,e_790),i5,e_792)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f87,f3081])).
% 5.44/1.27 fof(f3087,plain,(
% 5.44/1.27 store(store(a_789,i5,e_792),i0,e_790)=store(a_791,i5,e_792)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f61,f3086])).
% 5.44/1.27 fof(f3088,plain,(
% 5.44/1.27 store(store(a_789,i5,e_792),i0,e_790)=a_793),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f62,f3087])).
% 5.44/1.27 fof(f3187,plain,(
% 5.44/1.27 e_817=e_811),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f3066,f99])).
% 5.44/1.27 fof(f3212,plain,(
% 5.44/1.27 a_818=store(a_816,i2,e_811)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f3187,f76])).
% 5.44/1.27 fof(f3260,plain,(
% 5.44/1.27 select(a_804,i5)=e_801),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f2421,f53])).
% 5.44/1.27 fof(f3261,plain,(
% 5.44/1.27 e_807=e_801),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f3260,f95])).
% 5.44/1.27 fof(f3282,plain,(
% 5.44/1.27 store(store(a_804,i2,e_801),i5,e_803)=a_808),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f3261,f2399])).
% 5.44/1.27 fof(f4771,plain,(
% 5.44/1.27 store(store(a_785,i1,e_788),i2,select(a_785,i1))=store(store(a_785,i2,e_786),i1,e_788)),
% 5.44/1.27 inference(paramodulation,[status(thm)],[f85,f281])).
% 5.44/1.27 fof(f4781,plain,(
% 5.44/1.27 store(a_809,i2,select(a_785,i1))=store(store(a_785,i2,e_786),i1,e_788)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f71,f4771])).
% 5.44/1.27 fof(f4782,plain,(
% 5.44/1.27 store(a_809,i2,e_786)=store(store(a_785,i2,e_786),i1,e_788)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f85,f4781])).
% 5.44/1.27 fof(f4783,plain,(
% 5.44/1.27 a_810=store(store(a_785,i2,e_786),i1,e_788)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f72,f4782])).
% 5.44/1.27 fof(f4784,plain,(
% 5.44/1.27 a_810=store(a_787,i1,e_788)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f59,f4783])).
% 5.44/1.27 fof(f4785,plain,(
% 5.44/1.27 a_810=a_789),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f60,f4784])).
% 5.44/1.27 fof(f4997,plain,(
% 5.44/1.27 a_812=store(a_789,i5,e_811)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f4785,f73])).
% 5.44/1.27 fof(f4999,plain,(
% 5.44/1.27 e_813=select(a_789,i5)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f4785,f97])).
% 5.44/1.27 fof(f5000,plain,(
% 5.44/1.27 e_811=select(a_789,i0)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f4785,f96])).
% 5.44/1.27 fof(f5007,plain,(
% 5.44/1.27 e_813=e_790),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f87,f4999])).
% 5.44/1.27 fof(f5008,plain,(
% 5.44/1.27 e_811=e_792),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f88,f5000])).
% 5.44/1.27 fof(f5013,plain,(
% 5.44/1.27 a_814=store(a_812,i0,e_790)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5007,f74])).
% 5.44/1.27 fof(f5019,plain,(
% 5.44/1.27 a_818=store(a_816,i2,e_792)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5008,f3212])).
% 5.44/1.27 fof(f5100,plain,(
% 5.44/1.27 a_812=store(a_789,i5,e_792)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5008,f4997])).
% 5.44/1.27 fof(f5518,plain,(
% 5.44/1.27 a_814=a_793),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5519,f5013])).
% 5.44/1.27 fof(f5519,plain,(
% 5.44/1.27 store(a_812,i0,e_790)=a_793),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5100,f3088])).
% 5.44/1.27 fof(f5551,plain,(
% 5.44/1.27 a_816=store(a_793,i5,e_815)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5518,f75])).
% 5.44/1.27 fof(f5552,plain,(
% 5.44/1.27 e_815=select(a_793,i2)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5518,f98])).
% 5.44/1.27 fof(f5556,plain,(
% 5.44/1.27 e_815=e_796),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f90,f5552])).
% 5.44/1.27 fof(f5583,plain,(
% 5.44/1.27 a_816=store(a_793,i5,e_796)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5556,f5551])).
% 5.44/1.27 fof(f5829,plain,(
% 5.44/1.27 store(a_816,i2,e_792)=a_797),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5583,f2863])).
% 5.44/1.27 fof(f5856,plain,(
% 5.44/1.27 a_818=a_797),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5829,f5019])).
% 5.44/1.27 fof(f5887,plain,(
% 5.44/1.27 a_820=store(a_797,i1,e_819)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5856,f77])).
% 5.44/1.27 fof(f5888,plain,(
% 5.44/1.27 e_819=select(a_797,i1)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5856,f100])).
% 5.44/1.27 fof(f5892,plain,(
% 5.44/1.27 e_819=e_798),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f91,f5888])).
% 5.44/1.27 fof(f5895,plain,(
% 5.44/1.27 a_821=store(a_820,i1,e_798)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5892,f78])).
% 5.44/1.27 fof(f5919,plain,(
% 5.44/1.27 a_820=store(a_797,i1,e_798)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5892,f5887])).
% 5.44/1.27 fof(f5924,plain,(
% 5.44/1.27 a_820=a_799),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f65,f5919])).
% 5.44/1.27 fof(f5925,plain,(
% 5.44/1.27 a_821=store(a_799,i1,e_798)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5924,f5895])).
% 5.44/1.27 fof(f5935,plain,(
% 5.44/1.27 a_823=store(a_800,i5,e_822)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5938,f79])).
% 5.44/1.27 fof(f5936,plain,(
% 5.44/1.27 e_824=select(a_800,i5)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5938,f102])).
% 5.44/1.27 fof(f5937,plain,(
% 5.44/1.27 e_822=select(a_800,i2)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5938,f101])).
% 5.44/1.27 fof(f5938,plain,(
% 5.44/1.27 a_821=a_800),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f66,f5925])).
% 5.44/1.27 fof(f5945,plain,(
% 5.44/1.27 e_824=e_803),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f93,f5936])).
% 5.44/1.27 fof(f5946,plain,(
% 5.44/1.27 e_822=e_801),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f92,f5937])).
% 5.44/1.27 fof(f5954,plain,(
% 5.44/1.27 store(store(a_825,i2,e_822),i5,e_803)=a_829),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5945,f2752])).
% 5.44/1.27 fof(f5969,plain,(
% 5.44/1.27 a_825=store(a_823,i2,e_803)),
% 5.44/1.27 inference(backward_demodulation,[status(thm)],[f5945,f80])).
% 5.44/1.27 fof(f6042,plain,(
% 5.44/1.27 a_823=store(a_800,i5,e_801)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5946,f5935])).
% 5.44/1.27 fof(f6046,plain,(
% 5.44/1.27 a_823=a_802),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f67,f6042])).
% 5.44/1.27 fof(f6073,plain,(
% 5.44/1.27 a_825=store(a_802,i2,e_803)),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f6046,f5969])).
% 5.44/1.27 fof(f6080,plain,(
% 5.44/1.27 a_825=a_804),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f68,f6073])).
% 5.44/1.27 fof(f6219,plain,(
% 5.44/1.27 store(store(a_804,i2,e_822),i5,e_803)=a_829),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f6080,f5954])).
% 5.44/1.27 fof(f6220,plain,(
% 5.44/1.27 store(store(a_804,i2,e_801),i5,e_803)=a_829),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f5946,f6219])).
% 5.44/1.27 fof(f6221,plain,(
% 5.44/1.27 a_808=a_829),
% 5.44/1.27 inference(forward_demodulation,[status(thm)],[f3282,f6220])).
% 5.44/1.27 fof(f6222,plain,(
% 5.44/1.27 $false),
% 5.44/1.27 inference(forward_subsumption_resolution,[status(thm)],[f6221,f105])).
% 5.44/1.28 % SZS output end CNFRefutation for theBenchmark.p
% 5.44/1.31 % Elapsed time: 0.931897 seconds
% 5.44/1.31 % CPU time: 6.981663 seconds
% 5.44/1.31 % Total memory used: 189.147 MB
% 5.44/1.31 % Net memory used: 183.596 MB
%------------------------------------------------------------------------------