%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV540-1.007 : 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 : n013.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 84.28s 11.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV540-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:03:50 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 84.28/11.07 % Refutation found
% 84.28/11.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 84.28/11.07 % SZS output start CNFRefutation for theBenchmark
% 84.28/11.07 fof(f1,axiom,(
% 84.28/11.07 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f2,axiom,(
% 84.28/11.07 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f3,axiom,(
% 84.28/11.07 (![A,I]: (store(A,I,select(A,I)) = A ))),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f4,axiom,(
% 84.28/11.07 (![A,I,E,F]: (store(store(A,I,E),I,F) = store(A,I,F) ))),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f5,axiom,(
% 84.28/11.07 (![I,J,A,E,F]: (( I = J| store(store(A,I,E),J,F) = store(store(A,J,F),I,E) ) ))),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f8,hypothesis,(
% 84.28/11.07 a_787 = store(a_785,i2,e_786) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f9,hypothesis,(
% 84.28/11.07 a_789 = store(a_787,i1,e_788) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f10,hypothesis,(
% 84.28/11.07 a_791 = store(a_789,i0,e_790) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f11,hypothesis,(
% 84.28/11.07 a_793 = store(a_791,i5,e_792) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f12,hypothesis,(
% 84.28/11.07 a_795 = store(a_793,i2,e_794) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f13,hypothesis,(
% 84.28/11.07 a_797 = store(a_795,i5,e_796) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f14,hypothesis,(
% 84.28/11.07 a_799 = store(a_797,i1,e_798) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f15,hypothesis,(
% 84.28/11.07 a_800 = store(a_799,i1,e_798) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f16,hypothesis,(
% 84.28/11.07 a_802 = store(a_800,i5,e_801) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f17,hypothesis,(
% 84.28/11.07 a_804 = store(a_802,i2,e_803) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f18,hypothesis,(
% 84.28/11.07 a_806 = store(a_804,i5,e_805) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f19,hypothesis,(
% 84.28/11.07 a_808 = store(a_806,i2,e_807) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f20,hypothesis,(
% 84.28/11.07 a_809 = store(a_785,i1,e_788) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f21,hypothesis,(
% 84.28/11.07 a_810 = store(a_809,i2,e_786) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f22,hypothesis,(
% 84.28/11.07 a_812 = store(a_810,i5,e_811) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f23,hypothesis,(
% 84.28/11.07 a_814 = store(a_812,i0,e_813) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f24,hypothesis,(
% 84.28/11.07 a_816 = store(a_814,i5,e_815) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f25,hypothesis,(
% 84.28/11.07 a_818 = store(a_816,i2,e_817) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f26,hypothesis,(
% 84.28/11.07 a_820 = store(a_818,i1,e_819) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f27,hypothesis,(
% 84.28/11.07 a_821 = store(a_820,i1,e_819) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f28,hypothesis,(
% 84.28/11.07 a_823 = store(a_821,i5,e_822) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f29,hypothesis,(
% 84.28/11.07 a_825 = store(a_823,i2,e_824) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f30,hypothesis,(
% 84.28/11.07 a_827 = store(a_825,i5,e_826) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f31,hypothesis,(
% 84.28/11.07 a_829 = store(a_827,i2,e_828) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f34,hypothesis,(
% 84.28/11.07 e_786 = select(a_785,i1) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f35,hypothesis,(
% 84.28/11.07 e_788 = select(a_785,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f36,hypothesis,(
% 84.28/11.07 e_790 = select(a_789,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f37,hypothesis,(
% 84.28/11.07 e_792 = select(a_789,i0) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f38,hypothesis,(
% 84.28/11.07 e_794 = select(a_793,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f39,hypothesis,(
% 84.28/11.07 e_796 = select(a_793,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f40,hypothesis,(
% 84.28/11.07 e_798 = select(a_797,i1) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f41,hypothesis,(
% 84.28/11.07 e_801 = select(a_800,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f42,hypothesis,(
% 84.28/11.07 e_803 = select(a_800,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f43,hypothesis,(
% 84.28/11.07 e_805 = select(a_804,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f44,hypothesis,(
% 84.28/11.07 e_807 = select(a_804,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f45,hypothesis,(
% 84.28/11.07 e_811 = select(a_810,i0) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f46,hypothesis,(
% 84.28/11.07 e_813 = select(a_810,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f47,hypothesis,(
% 84.28/11.07 e_815 = select(a_814,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f48,hypothesis,(
% 84.28/11.07 e_817 = select(a_814,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f49,hypothesis,(
% 84.28/11.07 e_819 = select(a_818,i1) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f50,hypothesis,(
% 84.28/11.07 e_822 = select(a_821,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f51,hypothesis,(
% 84.28/11.07 e_824 = select(a_821,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f52,hypothesis,(
% 84.28/11.07 e_826 = select(a_825,i2) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f53,hypothesis,(
% 84.28/11.07 e_828 = select(a_825,i5) ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f54,negated_conjecture,(
% 84.28/11.07 a_808 != a_829 ),
% 84.28/11.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 84.28/11.07 fof(f55,plain,(
% 84.28/11.07 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f1])).
% 84.28/11.07 fof(f56,plain,(
% 84.28/11.07 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 84.28/11.07 inference(miniscoping,[status(thm)],[f2])).
% 84.28/11.07 fof(f57,plain,(
% 84.28/11.07 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f56])).
% 84.28/11.07 fof(f58,plain,(
% 84.28/11.07 ![X0,X1]: (store(X0,X1,select(X0,X1))=X0)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f3])).
% 84.28/11.07 fof(f59,plain,(
% 84.28/11.07 ![X0,X1,X2,X3]: (store(store(X0,X1,X2),X1,X3)=store(X0,X1,X3))),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f4])).
% 84.28/11.07 fof(f60,plain,(
% 84.28/11.07 ![I,J]: (I=J|(![A,E,F]: store(store(A,I,E),J,F)=store(store(A,J,F),I,E)))),
% 84.28/11.07 inference(miniscoping,[status(thm)],[f5])).
% 84.28/11.07 fof(f61,plain,(
% 84.28/11.07 ![X0,X1,X2,X3,X4]: (X0=X1|store(store(X2,X0,X3),X1,X4)=store(store(X2,X1,X4),X0,X3))),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f60])).
% 84.28/11.07 fof(f64,plain,(
% 84.28/11.07 a_787=store(a_785,i2,e_786)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f8])).
% 84.28/11.07 fof(f65,plain,(
% 84.28/11.07 a_789=store(a_787,i1,e_788)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f9])).
% 84.28/11.07 fof(f66,plain,(
% 84.28/11.07 a_791=store(a_789,i0,e_790)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f10])).
% 84.28/11.07 fof(f67,plain,(
% 84.28/11.07 a_793=store(a_791,i5,e_792)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f11])).
% 84.28/11.07 fof(f68,plain,(
% 84.28/11.07 a_795=store(a_793,i2,e_794)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f12])).
% 84.28/11.07 fof(f69,plain,(
% 84.28/11.07 a_797=store(a_795,i5,e_796)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f13])).
% 84.28/11.07 fof(f70,plain,(
% 84.28/11.07 a_799=store(a_797,i1,e_798)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f14])).
% 84.28/11.07 fof(f71,plain,(
% 84.28/11.07 a_800=store(a_799,i1,e_798)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f15])).
% 84.28/11.07 fof(f72,plain,(
% 84.28/11.07 a_802=store(a_800,i5,e_801)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f16])).
% 84.28/11.07 fof(f73,plain,(
% 84.28/11.07 a_804=store(a_802,i2,e_803)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f17])).
% 84.28/11.07 fof(f74,plain,(
% 84.28/11.07 a_806=store(a_804,i5,e_805)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f18])).
% 84.28/11.07 fof(f75,plain,(
% 84.28/11.07 a_808=store(a_806,i2,e_807)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f19])).
% 84.28/11.07 fof(f76,plain,(
% 84.28/11.07 a_809=store(a_785,i1,e_788)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f20])).
% 84.28/11.07 fof(f77,plain,(
% 84.28/11.07 a_810=store(a_809,i2,e_786)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f21])).
% 84.28/11.07 fof(f78,plain,(
% 84.28/11.07 a_812=store(a_810,i5,e_811)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f22])).
% 84.28/11.07 fof(f79,plain,(
% 84.28/11.07 a_814=store(a_812,i0,e_813)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f23])).
% 84.28/11.07 fof(f80,plain,(
% 84.28/11.07 a_816=store(a_814,i5,e_815)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f24])).
% 84.28/11.07 fof(f81,plain,(
% 84.28/11.07 a_818=store(a_816,i2,e_817)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f25])).
% 84.28/11.07 fof(f82,plain,(
% 84.28/11.07 a_820=store(a_818,i1,e_819)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f26])).
% 84.28/11.07 fof(f83,plain,(
% 84.28/11.07 a_821=store(a_820,i1,e_819)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f27])).
% 84.28/11.07 fof(f84,plain,(
% 84.28/11.07 a_823=store(a_821,i5,e_822)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f28])).
% 84.28/11.07 fof(f85,plain,(
% 84.28/11.07 a_825=store(a_823,i2,e_824)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f29])).
% 84.28/11.07 fof(f86,plain,(
% 84.28/11.07 a_827=store(a_825,i5,e_826)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f30])).
% 84.28/11.07 fof(f87,plain,(
% 84.28/11.07 a_829=store(a_827,i2,e_828)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f31])).
% 84.28/11.07 fof(f90,plain,(
% 84.28/11.07 e_786=select(a_785,i1)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f34])).
% 84.28/11.07 fof(f91,plain,(
% 84.28/11.07 e_788=select(a_785,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f35])).
% 84.28/11.07 fof(f92,plain,(
% 84.28/11.07 e_790=select(a_789,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f36])).
% 84.28/11.07 fof(f93,plain,(
% 84.28/11.07 e_792=select(a_789,i0)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f37])).
% 84.28/11.07 fof(f94,plain,(
% 84.28/11.07 e_794=select(a_793,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f38])).
% 84.28/11.07 fof(f95,plain,(
% 84.28/11.07 e_796=select(a_793,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f39])).
% 84.28/11.07 fof(f96,plain,(
% 84.28/11.07 e_798=select(a_797,i1)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f40])).
% 84.28/11.07 fof(f97,plain,(
% 84.28/11.07 e_801=select(a_800,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f41])).
% 84.28/11.07 fof(f98,plain,(
% 84.28/11.07 e_803=select(a_800,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f42])).
% 84.28/11.07 fof(f99,plain,(
% 84.28/11.07 e_805=select(a_804,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f43])).
% 84.28/11.07 fof(f100,plain,(
% 84.28/11.07 e_807=select(a_804,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f44])).
% 84.28/11.07 fof(f101,plain,(
% 84.28/11.07 e_811=select(a_810,i0)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f45])).
% 84.28/11.07 fof(f102,plain,(
% 84.28/11.07 e_813=select(a_810,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f46])).
% 84.28/11.07 fof(f103,plain,(
% 84.28/11.07 e_815=select(a_814,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f47])).
% 84.28/11.07 fof(f104,plain,(
% 84.28/11.07 e_817=select(a_814,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f48])).
% 84.28/11.07 fof(f105,plain,(
% 84.28/11.07 e_819=select(a_818,i1)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f49])).
% 84.28/11.07 fof(f106,plain,(
% 84.28/11.07 e_822=select(a_821,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f50])).
% 84.28/11.07 fof(f107,plain,(
% 84.28/11.07 e_824=select(a_821,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f51])).
% 84.28/11.07 fof(f108,plain,(
% 84.28/11.07 e_826=select(a_825,i2)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f52])).
% 84.28/11.07 fof(f109,plain,(
% 84.28/11.07 e_828=select(a_825,i5)),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f53])).
% 84.28/11.07 fof(f110,plain,(
% 84.28/11.07 ~a_808=a_829),
% 84.28/11.07 inference(cnf_transformation,[status(thm)],[f54])).
% 84.28/11.07 fof(f111,plain,(
% 84.28/11.07 select(a_829,i2)=e_828),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f87,f55])).
% 84.28/11.07 fof(f112,plain,(
% 84.28/11.07 select(a_808,i2)=e_807),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f75,f55])).
% 84.28/11.07 fof(f115,plain,(
% 84.28/11.07 ![X0]: (i2=X0|select(a_808,X0)=select(a_806,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f75,f57])).
% 84.28/11.07 fof(f117,plain,(
% 84.28/11.07 store(a_821,i2,e_822)=a_821),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f106,f58])).
% 84.28/11.07 fof(f118,plain,(
% 84.28/11.07 store(a_818,i1,e_819)=a_818),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f105,f58])).
% 84.28/11.07 fof(f119,plain,(
% 84.28/11.07 store(a_814,i5,e_817)=a_814),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f104,f58])).
% 84.28/11.07 fof(f120,plain,(
% 84.28/11.07 store(a_814,i2,e_815)=a_814),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f103,f58])).
% 84.28/11.07 fof(f121,plain,(
% 84.28/11.07 store(a_810,i5,e_813)=a_810),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f102,f58])).
% 84.28/11.07 fof(f122,plain,(
% 84.28/11.07 store(a_810,i0,e_811)=a_810),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f101,f58])).
% 84.28/11.07 fof(f123,plain,(
% 84.28/11.07 store(a_804,i5,e_807)=a_804),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f100,f58])).
% 84.28/11.07 fof(f124,plain,(
% 84.28/11.07 store(a_804,i2,e_805)=a_804),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f99,f58])).
% 84.28/11.07 fof(f125,plain,(
% 84.28/11.07 store(a_800,i5,e_803)=a_800),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f98,f58])).
% 84.28/11.07 fof(f126,plain,(
% 84.28/11.07 store(a_800,i2,e_801)=a_800),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f97,f58])).
% 84.28/11.07 fof(f127,plain,(
% 84.28/11.07 store(a_797,i1,e_798)=a_797),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f96,f58])).
% 84.28/11.07 fof(f129,plain,(
% 84.28/11.07 store(a_793,i2,e_796)=a_793),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f95,f58])).
% 84.28/11.07 fof(f131,plain,(
% 84.28/11.07 store(a_789,i0,e_792)=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f93,f58])).
% 84.28/11.07 fof(f133,plain,(
% 84.28/11.07 store(a_785,i2,e_788)=a_785),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f91,f58])).
% 84.28/11.07 fof(f134,plain,(
% 84.28/11.07 store(a_785,i1,e_786)=a_785),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f90,f58])).
% 84.28/11.07 fof(f135,plain,(
% 84.28/11.07 store(a_808,i2,e_807)=a_808),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f112,f58])).
% 84.28/11.07 fof(f136,plain,(
% 84.28/11.07 store(a_829,i2,e_828)=a_829),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f111,f58])).
% 84.28/11.07 fof(f145,plain,(
% 84.28/11.07 ![X0]: (store(a_829,i2,X0)=store(a_827,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f87,f59])).
% 84.28/11.07 fof(f146,plain,(
% 84.28/11.07 ![X0]: (store(a_808,i2,X0)=store(a_806,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f75,f59])).
% 84.28/11.07 fof(f299,plain,(
% 84.28/11.07 store(a_821,i5,e_824)=a_821),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f107,f58])).
% 84.28/11.07 fof(f300,plain,(
% 84.28/11.07 store(a_825,i2,e_826)=a_825),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f108,f58])).
% 84.28/11.07 fof(f314,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i2|store(store(a_785,X0,X1),i2,e_786)=store(a_787,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f64,f61])).
% 84.28/11.07 fof(f326,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i0|store(store(a_789,X0,X1),i0,e_790)=store(a_791,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f66,f61])).
% 84.28/11.07 fof(f333,plain,(
% 84.28/11.07 ![X0]: (store(a_793,i5,X0)=store(a_791,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f67,f59])).
% 84.28/11.07 fof(f335,plain,(
% 84.28/11.07 select(a_793,i5)=e_792),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f67,f55])).
% 84.28/11.07 fof(f336,plain,(
% 84.28/11.07 e_794=e_792),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f94,f335])).
% 84.28/11.07 fof(f339,plain,(
% 84.28/11.07 ![X0]: (store(a_795,i2,X0)=store(a_793,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f68,f59])).
% 84.28/11.07 fof(f340,plain,(
% 84.28/11.07 ![X0]: (i2=X0|select(a_795,X0)=select(a_793,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f68,f57])).
% 84.28/11.07 fof(f341,plain,(
% 84.28/11.07 select(a_795,i2)=e_794),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f68,f55])).
% 84.28/11.07 fof(f345,plain,(
% 84.28/11.07 ![X0]: (i5=X0|select(a_797,X0)=select(a_795,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f69,f57])).
% 84.28/11.07 fof(f475,plain,(
% 84.28/11.07 a_793=store(a_791,i5,e_794)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f336,f67])).
% 84.28/11.07 fof(f476,plain,(
% 84.28/11.07 e_794=select(a_789,i0)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f336,f93])).
% 84.28/11.07 fof(f478,plain,(
% 84.28/11.07 store(a_795,i2,e_794)=a_795),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f341,f58])).
% 84.28/11.07 fof(f495,plain,(
% 84.28/11.07 ![X0]: (store(a_802,i5,X0)=store(a_800,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f72,f59])).
% 84.28/11.07 fof(f497,plain,(
% 84.28/11.07 select(a_802,i5)=e_801),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f72,f55])).
% 84.28/11.07 fof(f498,plain,(
% 84.28/11.07 store(a_802,i5,e_801)=a_802),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f497,f58])).
% 84.28/11.07 fof(f501,plain,(
% 84.28/11.07 ![X0]: (store(a_804,i2,X0)=store(a_802,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f73,f59])).
% 84.28/11.07 fof(f502,plain,(
% 84.28/11.07 ![X0]: (i2=X0|select(a_804,X0)=select(a_802,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f73,f57])).
% 84.28/11.07 fof(f503,plain,(
% 84.28/11.07 select(a_804,i2)=e_803),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f73,f55])).
% 84.28/11.07 fof(f504,plain,(
% 84.28/11.07 e_805=e_803),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f99,f503])).
% 84.28/11.07 fof(f505,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i5|store(store(a_804,X0,X1),i5,e_805)=store(a_806,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f74,f61])).
% 84.28/11.07 fof(f507,plain,(
% 84.28/11.07 ![X0]: (store(a_806,i5,X0)=store(a_804,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f74,f59])).
% 84.28/11.07 fof(f509,plain,(
% 84.28/11.07 select(a_806,i5)=e_805),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f74,f55])).
% 84.28/11.07 fof(f519,plain,(
% 84.28/11.07 select(a_810,i2)=e_786),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f77,f55])).
% 84.28/11.07 fof(f733,plain,(
% 84.28/11.07 e_805=select(a_800,i5)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f504,f98])).
% 84.28/11.07 fof(f734,plain,(
% 84.28/11.07 select(a_808,i5)=e_805|i2=i5),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f115,f509])).
% 84.28/11.07 fof(f738,plain,(
% 84.28/11.07 store(a_806,i5,e_805)=a_806),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f509,f58])).
% 84.28/11.07 fof(f746,plain,(
% 84.28/11.07 select(a_812,i5)=e_811),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f78,f55])).
% 84.28/11.07 fof(f747,plain,(
% 84.28/11.07 store(a_812,i5,e_811)=a_812),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f746,f58])).
% 84.28/11.07 fof(f750,plain,(
% 84.28/11.07 ![X0]: (store(a_814,i0,X0)=store(a_812,i0,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f79,f59])).
% 84.28/11.07 fof(f751,plain,(
% 84.28/11.07 ![X0]: (i0=X0|select(a_814,X0)=select(a_812,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f79,f57])).
% 84.28/11.07 fof(f752,plain,(
% 84.28/11.07 select(a_814,i0)=e_813),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f79,f55])).
% 84.28/11.07 fof(f753,plain,(
% 84.28/11.07 store(a_814,i0,e_813)=a_814),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f752,f58])).
% 84.28/11.07 fof(f754,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i5|store(store(a_814,X0,X1),i5,e_815)=store(a_816,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f80,f61])).
% 84.28/11.07 fof(f756,plain,(
% 84.28/11.07 ![X0]: (store(a_816,i5,X0)=store(a_814,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f80,f59])).
% 84.28/11.07 fof(f758,plain,(
% 84.28/11.07 select(a_816,i5)=e_815),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f80,f55])).
% 84.28/11.07 fof(f759,plain,(
% 84.28/11.07 store(a_816,i5,e_815)=a_816),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f758,f58])).
% 84.28/11.07 fof(f762,plain,(
% 84.28/11.07 ![X0]: (store(a_818,i2,X0)=store(a_816,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f81,f59])).
% 84.28/11.07 fof(f763,plain,(
% 84.28/11.07 ![X0]: (i2=X0|select(a_818,X0)=select(a_816,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f81,f57])).
% 84.28/11.07 fof(f764,plain,(
% 84.28/11.07 select(a_818,i2)=e_817),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f81,f55])).
% 84.28/11.07 fof(f769,plain,(
% 84.28/11.07 select(a_820,i1)=e_819),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f82,f55])).
% 84.28/11.07 fof(f775,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i5|store(store(a_821,X0,X1),i5,e_822)=store(a_823,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f84,f61])).
% 84.28/11.07 fof(f777,plain,(
% 84.28/11.07 ![X0]: (store(a_823,i5,X0)=store(a_821,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f84,f59])).
% 84.28/11.07 fof(f779,plain,(
% 84.28/11.07 select(a_823,i5)=e_822),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f84,f55])).
% 84.28/11.07 fof(f972,plain,(
% 84.28/11.07 store(a_820,i1,e_819)=a_820),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f769,f58])).
% 84.28/11.07 fof(f973,plain,(
% 84.28/11.07 a_821=a_820),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f83,f972])).
% 84.28/11.07 fof(f976,plain,(
% 84.28/11.07 a_821=store(a_818,i1,e_819)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f973,f82])).
% 84.28/11.07 fof(f978,plain,(
% 84.28/11.07 store(a_823,i5,e_822)=a_823),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f779,f58])).
% 84.28/11.07 fof(f981,plain,(
% 84.28/11.07 ![X0]: (store(a_825,i2,X0)=store(a_823,i2,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f85,f59])).
% 84.28/11.07 fof(f982,plain,(
% 84.28/11.07 ![X0]: (i2=X0|select(a_825,X0)=select(a_823,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f85,f57])).
% 84.28/11.07 fof(f983,plain,(
% 84.28/11.07 select(a_825,i2)=e_824),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f85,f55])).
% 84.28/11.07 fof(f984,plain,(
% 84.28/11.07 e_826=e_824),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f108,f983])).
% 84.28/11.07 fof(f986,plain,(
% 84.28/11.07 e_826=select(a_821,i5)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f984,f107])).
% 84.28/11.07 fof(f988,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i5|store(store(a_825,X0,X1),i5,e_826)=store(a_827,X0,X1))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f86,f61])).
% 84.28/11.07 fof(f990,plain,(
% 84.28/11.07 ![X0]: (store(a_827,i5,X0)=store(a_825,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f86,f59])).
% 84.28/11.07 fof(f992,plain,(
% 84.28/11.07 select(a_827,i5)=e_826),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f86,f55])).
% 84.28/11.07 fof(f997,plain,(
% 84.28/11.07 store(a_827,i5,e_826)=a_827),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f992,f58])).
% 84.28/11.07 fof(f1258,plain,(
% 84.28/11.07 store(a_800,i5,e_805)=a_800),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f504,f125])).
% 84.28/11.07 fof(f1269,plain,(
% 84.28/11.07 a_799=store(a_799,i1,e_798)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1273,f70])).
% 84.28/11.07 fof(f1271,plain,(
% 84.28/11.07 a_799=store(a_795,i5,e_796)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1273,f69])).
% 84.28/11.07 fof(f1273,plain,(
% 84.28/11.07 a_799=a_797),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f70,f127])).
% 84.28/11.07 fof(f1274,plain,(
% 84.28/11.07 a_799=a_800),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f71,f1269])).
% 84.28/11.07 fof(f1275,plain,(
% 84.28/11.07 a_800=a_797),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1274,f1273])).
% 84.28/11.07 fof(f1278,plain,(
% 84.28/11.07 a_821=a_818),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f976,f118])).
% 84.28/11.07 fof(f1289,plain,(
% 84.28/11.07 a_800=store(a_795,i5,e_796)),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f1274,f1271])).
% 84.28/11.07 fof(f1292,plain,(
% 84.28/11.07 ![X0]: (store(a_800,i5,X0)=store(a_795,i5,X0))),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f1289,f59])).
% 84.28/11.07 fof(f1294,plain,(
% 84.28/11.07 select(a_800,i5)=e_796),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f1289,f55])).
% 84.28/11.07 fof(f1295,plain,(
% 84.28/11.07 e_805=e_796),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f733,f1294])).
% 84.28/11.07 fof(f1457,plain,(
% 84.28/11.07 select(a_821,i2)=e_817),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1278,f764])).
% 84.28/11.07 fof(f1460,plain,(
% 84.28/11.07 e_822=e_817),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f106,f1457])).
% 84.28/11.07 fof(f1462,plain,(
% 84.28/11.07 e_805=select(a_793,i2)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1295,f95])).
% 84.28/11.07 fof(f1463,plain,(
% 84.28/11.07 store(a_814,i5,e_822)=a_814),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1460,f119])).
% 84.28/11.07 fof(f1464,plain,(
% 84.28/11.07 e_822=select(a_814,i5)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f1460,f104])).
% 84.28/11.07 fof(f1469,plain,(
% 84.28/11.07 store(a_793,i2,e_805)=a_793),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f1295,f129])).
% 84.28/11.07 fof(f1480,plain,(
% 84.28/11.07 store(a_789,i0,e_794)=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f336,f131])).
% 84.28/11.07 fof(f1833,plain,(
% 84.28/11.07 store(a_821,i5,e_826)=a_821),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f984,f299])).
% 84.28/11.07 fof(f5011,plain,(
% 84.28/11.07 i2=i5|select(a_795,i5)=e_794),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f94,f340])).
% 84.28/11.07 fof(f5018,plain,(
% 84.28/11.07 store(a_795,i5,e_794)=a_795|i2=i5),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f5011,f58])).
% 84.28/11.07 fof(f5019,plain,(
% 84.28/11.07 ![X0]: (i5=X0|select(a_800,X0)=select(a_795,X0))),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f1275,f345])).
% 84.28/11.07 fof(f5021,plain,(
% 84.28/11.07 i5=i2|select(a_800,i2)=e_794),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f341,f5019])).
% 84.28/11.07 fof(f5026,plain,(
% 84.28/11.07 i5=i2|e_801=e_794),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f97,f5021])).
% 84.28/11.07 fof(f5050,plain,(
% 84.28/11.07 e_805=select(a_793,i5)|e_801=e_794),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f5026,f1462])).
% 84.28/11.07 fof(f5111,plain,(
% 84.28/11.07 e_801=select(a_800,i5)|e_801=e_794),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f5026,f97])).
% 84.28/11.07 fof(f5117,plain,(
% 84.28/11.07 e_805=e_794|e_801=e_794),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f94,f5050])).
% 84.28/11.07 fof(f5138,plain,(
% 84.28/11.07 e_801=e_805|e_801=e_794),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f733,f5111])).
% 84.28/11.07 fof(f8308,plain,(
% 84.28/11.07 i1=i2|store(a_809,i2,e_786)=store(a_787,i1,e_788)),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f76,f314])).
% 84.28/11.07 fof(f8347,plain,(
% 84.28/11.07 i1=i2|a_810=store(a_787,i1,e_788)),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f77,f8308])).
% 84.28/11.07 fof(f8348,plain,(
% 84.28/11.07 i1=i2|a_810=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f65,f8347])).
% 84.28/11.07 fof(f9121,plain,(
% 84.28/11.07 store(a_785,i1,e_788)=a_785|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f8348,f133])).
% 84.28/11.07 fof(f9159,plain,(
% 84.28/11.07 a_787=store(a_785,i1,e_786)|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f8348,f64])).
% 84.28/11.07 fof(f9181,plain,(
% 84.28/11.07 a_809=a_785|a_810=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f76,f9121])).
% 84.28/11.07 fof(f9182,plain,(
% 84.28/11.07 a_787=a_785|a_810=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f134,f9159])).
% 84.28/11.07 fof(f9198,plain,(
% 84.28/11.07 a_787=store(a_809,i2,e_786)|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f9181,f64])).
% 84.28/11.07 fof(f9202,plain,(
% 84.28/11.07 a_787=a_810|a_810=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f77,f9198])).
% 84.28/11.07 fof(f9204,plain,(
% 84.28/11.07 a_787=a_809|a_810=a_789|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f9181,f9182])).
% 84.28/11.07 fof(f9217,plain,(
% 84.28/11.07 a_809=store(a_787,i1,e_788)|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f9182,f76])).
% 84.28/11.07 fof(f9222,plain,(
% 84.28/11.07 a_787=a_809|a_810=a_789),
% 84.28/11.07 inference(duplicate_literals_removal,[status(thm)],[f9204])).
% 84.28/11.07 fof(f9224,plain,(
% 84.28/11.07 a_809=a_789|a_810=a_789),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f65,f9217])).
% 84.28/11.07 fof(f9283,plain,(
% 84.28/11.07 a_810=a_809|a_810=a_789|a_810=a_789),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f9202,f9222])).
% 84.28/11.07 fof(f9296,plain,(
% 84.28/11.07 a_810=a_809|a_810=a_789),
% 84.28/11.07 inference(duplicate_literals_removal,[status(thm)],[f9283])).
% 84.28/11.07 fof(f9314,plain,(
% 84.28/11.07 ~a_809=a_810|a_789=a_810),
% 84.28/11.07 inference(equality_factoring,[status(thm)],[f9224])).
% 84.28/11.07 fof(f9884,plain,(
% 84.28/11.07 store(a_789,i0,e_794)=a_810),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9890,f1480])).
% 84.28/11.07 fof(f9885,plain,(
% 84.28/11.07 e_794=select(a_810,i0)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9890,f476])).
% 84.28/11.07 fof(f9886,plain,(
% 84.28/11.07 a_791=store(a_810,i0,e_790)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9890,f66])).
% 84.28/11.07 fof(f9889,plain,(
% 84.28/11.07 e_790=select(a_810,i5)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9890,f92])).
% 84.28/11.07 fof(f9890,plain,(
% 84.28/11.07 a_789=a_810),
% 84.28/11.07 inference(forward_subsumption_resolution,[status(thm)],[f9314,f9296])).
% 84.28/11.07 fof(f9893,plain,(
% 84.28/11.07 store(a_810,i0,e_794)=a_810),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9890,f9884])).
% 84.28/11.07 fof(f9894,plain,(
% 84.28/11.07 e_794=e_811),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f101,f9885])).
% 84.28/11.07 fof(f9895,plain,(
% 84.28/11.07 e_790=e_813),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f102,f9889])).
% 84.28/11.07 fof(f9942,plain,(
% 84.28/11.07 e_801=e_805|e_801=e_811),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f5138])).
% 84.28/11.07 fof(f9963,plain,(
% 84.28/11.07 e_805=e_794|e_801=e_811),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f5117])).
% 84.28/11.07 fof(f9967,plain,(
% 84.28/11.07 store(a_795,i2,e_811)=a_795),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f478])).
% 84.28/11.07 fof(f9969,plain,(
% 84.28/11.07 a_793=store(a_791,i5,e_811)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f475])).
% 84.28/11.07 fof(f9970,plain,(
% 84.28/11.07 select(a_795,i2)=e_811),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f341])).
% 84.28/11.07 fof(f9973,plain,(
% 84.28/11.07 e_811=select(a_793,i5)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f9894,f94])).
% 84.28/11.07 fof(f9975,plain,(
% 84.28/11.07 e_805=e_811|e_801=e_811),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9894,f9963])).
% 84.28/11.07 fof(f9982,plain,(
% 84.28/11.07 a_791=store(a_810,i0,e_813)),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9895,f9886])).
% 84.28/11.07 fof(f10321,plain,(
% 84.28/11.07 ~e_805=e_811|e_801=e_811),
% 84.28/11.07 inference(equality_factoring,[status(thm)],[f9942])).
% 84.28/11.07 fof(f10783,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i0|store(store(a_810,X0,X1),i0,e_790)=store(a_791,X0,X1))),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9890,f326])).
% 84.28/11.07 fof(f10784,plain,(
% 84.28/11.07 ![X0,X1]: (X0=i0|store(store(a_810,X0,X1),i0,e_813)=store(a_791,X0,X1))),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9895,f10783])).
% 84.28/11.07 fof(f10793,plain,(
% 84.28/11.07 i5=i0|store(a_812,i0,e_813)=store(a_791,i5,e_811)),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f78,f10784])).
% 84.28/11.07 fof(f10821,plain,(
% 84.28/11.07 i5=i0|a_814=store(a_791,i5,e_811)),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f79,f10793])).
% 84.28/11.07 fof(f10822,plain,(
% 84.28/11.07 i5=i0|a_814=a_793),
% 84.28/11.07 inference(forward_demodulation,[status(thm)],[f9969,f10821])).
% 84.28/11.07 fof(f11119,plain,(
% 84.28/11.07 store(a_802,i5,e_811)=a_802),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f11124,f498])).
% 84.28/11.07 fof(f11120,plain,(
% 84.28/11.07 store(a_800,i2,e_811)=a_800),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f11124,f126])).
% 84.28/11.07 fof(f11121,plain,(
% 84.28/11.07 select(a_802,i5)=e_811),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f11124,f497])).
% 84.28/11.07 fof(f11123,plain,(
% 84.28/11.07 e_811=select(a_800,i2)),
% 84.28/11.07 inference(backward_demodulation,[status(thm)],[f11124,f97])).
% 84.28/11.07 fof(f11124,plain,(
% 84.28/11.07 e_801=e_811),
% 84.28/11.07 inference(forward_subsumption_resolution,[status(thm)],[f10321,f9975])).
% 84.28/11.07 fof(f11127,plain,(
% 84.28/11.07 a_791=store(a_810,i5,e_813)|a_814=a_793),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f10822,f9982])).
% 84.28/11.07 fof(f11129,plain,(
% 84.28/11.07 store(a_810,i5,e_811)=a_810|a_814=a_793),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f10822,f122])).
% 84.28/11.07 fof(f11130,plain,(
% 84.28/11.07 select(a_814,i5)=e_813|a_814=a_793),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f10822,f752])).
% 84.28/11.07 fof(f11132,plain,(
% 84.28/11.07 e_811=select(a_810,i5)|a_814=a_793),
% 84.28/11.07 inference(paramodulation,[status(thm)],[f10822,f101])).
% 84.28/11.08 fof(f11133,plain,(
% 84.28/11.08 a_791=a_810|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f121,f11127])).
% 84.28/11.08 fof(f11134,plain,(
% 84.28/11.08 a_812=a_810|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f78,f11129])).
% 84.28/11.08 fof(f11135,plain,(
% 84.28/11.08 e_822=e_813|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f1464,f11130])).
% 84.28/11.08 fof(f11136,plain,(
% 84.28/11.08 e_811=e_813|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f102,f11132])).
% 84.28/11.08 fof(f11142,plain,(
% 84.28/11.08 a_793=store(a_810,i5,e_811)|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11133,f9969])).
% 84.28/11.08 fof(f11146,plain,(
% 84.28/11.08 a_793=a_812|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f78,f11142])).
% 84.28/11.08 fof(f11156,plain,(
% 84.28/11.08 e_811=select(a_814,i5)|e_822=e_813),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11135,f9973])).
% 84.28/11.08 fof(f11161,plain,(
% 84.28/11.08 e_811=e_822|e_822=e_813),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f1464,f11156])).
% 84.28/11.08 fof(f11167,plain,(
% 84.28/11.08 e_811=select(a_814,i5)|e_811=e_813),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11136,f9973])).
% 84.28/11.08 fof(f11172,plain,(
% 84.28/11.08 e_811=e_822|e_811=e_813),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f1464,f11167])).
% 84.28/11.08 fof(f11184,plain,(
% 84.28/11.08 e_805=select(a_812,i2)|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11146,f1462])).
% 84.28/11.08 fof(f11185,plain,(
% 84.28/11.08 ~a_812=a_814|a_793=a_814),
% 84.28/11.08 inference(equality_factoring,[status(thm)],[f11146])).
% 84.28/11.08 fof(f11356,plain,(
% 84.28/11.08 ~e_813=e_822|e_811=e_822),
% 84.28/11.08 inference(equality_factoring,[status(thm)],[f11172])).
% 84.28/11.08 fof(f11361,plain,(
% 84.28/11.08 e_811=e_822),
% 84.28/11.08 inference(forward_subsumption_resolution,[status(thm)],[f11356,f11161])).
% 84.28/11.08 fof(f11371,plain,(
% 84.28/11.08 e_822=select(a_800,i2)),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f11123])).
% 84.28/11.08 fof(f11372,plain,(
% 84.28/11.08 select(a_802,i5)=e_822),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f11121])).
% 84.28/11.08 fof(f11374,plain,(
% 84.28/11.08 select(a_795,i2)=e_822),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f9970])).
% 84.28/11.08 fof(f11379,plain,(
% 84.28/11.08 e_794=e_822),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f9894])).
% 84.28/11.08 fof(f11380,plain,(
% 84.28/11.08 store(a_812,i5,e_822)=a_812),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f747])).
% 84.28/11.08 fof(f11382,plain,(
% 84.28/11.08 select(a_812,i5)=e_822),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f11361,f746])).
% 84.28/11.08 fof(f11934,plain,(
% 84.28/11.08 store(a_810,i0,e_822)=a_810),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f11379,f9893])).
% 84.28/11.08 fof(f11953,plain,(
% 84.28/11.08 store(a_795,i2,e_822)=a_795),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f11361,f9967])).
% 84.28/11.08 fof(f11996,plain,(
% 84.28/11.08 store(a_802,i5,e_822)=a_802),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f11361,f11119])).
% 84.28/11.08 fof(f12014,plain,(
% 84.28/11.08 store(a_800,i2,e_822)=a_800),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f11361,f11120])).
% 84.28/11.08 fof(f12166,plain,(
% 84.28/11.08 store(a_795,i2,e_805)=a_793),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f339,f1469])).
% 84.28/11.08 fof(f13245,plain,(
% 84.28/11.08 store(a_802,i5,e_805)=a_800),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f495,f1258])).
% 84.28/11.08 fof(f13523,plain,(
% 84.28/11.08 i2=i5|select(a_804,i5)=e_822),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11372,f502])).
% 84.28/11.08 fof(f13527,plain,(
% 84.28/11.08 i2=i5|e_807=e_822),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f100,f13523])).
% 84.28/11.08 fof(f13828,plain,(
% 84.28/11.08 e_822=select(a_800,i5)|e_807=e_822),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f13527,f11371])).
% 84.28/11.08 fof(f13916,plain,(
% 84.28/11.08 e_805=select(a_804,i5)|e_807=e_822),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f13527,f99])).
% 84.28/11.08 fof(f13924,plain,(
% 84.28/11.08 e_822=e_805|e_807=e_822),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f733,f13828])).
% 84.28/11.08 fof(f13944,plain,(
% 84.28/11.08 e_805=e_807|e_807=e_822),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f100,f13916])).
% 84.28/11.08 fof(f14057,plain,(
% 84.28/11.08 store(a_806,i5,e_807)=a_804),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f507,f123])).
% 84.28/11.08 fof(f14855,plain,(
% 84.28/11.08 e_822=e_807|e_807=e_822|e_807=e_822),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f13924,f13944])).
% 84.28/11.08 fof(f14877,plain,(
% 84.28/11.08 e_822=e_807),
% 84.28/11.08 inference(duplicate_literals_removal,[status(thm)],[f14855])).
% 84.28/11.08 fof(f14918,plain,(
% 84.28/11.08 store(a_808,i2,e_822)=a_808),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f14877,f135])).
% 84.28/11.08 fof(f14919,plain,(
% 84.28/11.08 e_822=select(a_804,i5)),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f14877,f100])).
% 84.28/11.08 fof(f14920,plain,(
% 84.28/11.08 select(a_808,i2)=e_822),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f14877,f112])).
% 84.28/11.08 fof(f14932,plain,(
% 84.28/11.08 store(a_806,i5,e_822)=a_804),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f14877,f14057])).
% 84.28/11.08 fof(f16253,plain,(
% 84.28/11.08 i0=i2|select(a_814,i2)=e_805|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f11184,f751])).
% 84.28/11.08 fof(f16259,plain,(
% 84.28/11.08 i0=i2|e_815=e_805|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f103,f16253])).
% 84.28/11.08 fof(f16327,plain,(
% 84.28/11.08 store(a_816,i5,e_822)=a_814),
% 84.28/11.08 inference(backward_demodulation,[status(thm)],[f756,f1463])).
% 84.28/11.08 fof(f16700,plain,(
% 84.28/11.08 select(a_808,i0)=e_822|e_815=e_805|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f16259,f14920])).
% 84.28/11.08 fof(f16866,plain,(
% 84.28/11.08 select(a_808,i5)=e_822|e_815=e_805|a_814=a_793|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f10822,f16700])).
% 84.28/11.08 fof(f16873,plain,(
% 84.28/11.08 select(a_808,i5)=e_822|e_815=e_805|a_814=a_793),
% 84.28/11.08 inference(duplicate_literals_removal,[status(thm)],[f16866])).
% 84.28/11.08 fof(f16884,plain,(
% 84.28/11.08 e_805=e_822|e_815=e_805|a_814=a_793|i2=i5),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f734,f16873])).
% 84.28/11.08 fof(f17015,plain,(
% 84.28/11.08 e_805=select(a_812,i5)|a_814=a_793|e_805=e_822|e_815=e_805|a_814=a_793),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f16884,f11184])).
% 84.28/11.08 fof(f17148,plain,(
% 84.28/11.08 e_805=e_822|a_814=a_793|e_805=e_822|e_815=e_805|a_814=a_793),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f11382,f17015])).
% 84.28/11.08 fof(f17149,plain,(
% 84.28/11.08 e_805=e_822|a_814=a_793|e_815=e_805),
% 84.28/11.08 inference(duplicate_literals_removal,[status(thm)],[f17148])).
% 84.28/11.08 fof(f17198,plain,(
% 84.28/11.08 e_805=select(a_814,i2)|e_805=e_822|e_815=e_805),
% 84.28/11.08 inference(paramodulation,[status(thm)],[f17149,f1462])).
% 84.28/11.08 fof(f17201,plain,(
% 84.28/11.08 e_805=e_815|e_805=e_822|e_815=e_805),
% 84.28/11.08 inference(forward_demodulation,[status(thm)],[f103,f17198])).
% 84.28/11.08 fof(f17202,plain,(
% 84.28/11.08 e_805=e_815|e_805=e_822),
% 84.28/11.08 inference(duplicate_literals_removal,[status(thm)],[f17201])).
% 84.28/11.08 fof(f17896,plain,(
% 84.28/11.08 ![X0]: (store(a_821,i2,X0)=store(a_816,i2,X0))),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f1278,f762])).
% 84.28/11.09 fof(f17922,plain,(
% 84.28/11.09 ![X0]: (i2=X0|select(a_821,X0)=select(a_816,X0))),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f1278,f763])).
% 84.28/11.09 fof(f17925,plain,(
% 84.28/11.09 i2=i5|select(a_821,i5)=e_815),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f758,f17922])).
% 84.28/11.09 fof(f17931,plain,(
% 84.28/11.09 i2=i5|e_826=e_815),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f986,f17925])).
% 84.28/11.09 fof(f19195,plain,(
% 84.28/11.09 e_822=select(a_821,i5)|e_826=e_815),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f17931,f106])).
% 84.28/11.09 fof(f19196,plain,(
% 84.28/11.09 e_815=select(a_814,i5)|e_826=e_815),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f17931,f103])).
% 84.28/11.09 fof(f19235,plain,(
% 84.28/11.09 e_822=e_826|e_826=e_815),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f986,f19195])).
% 84.28/11.09 fof(f19236,plain,(
% 84.28/11.09 e_815=e_822|e_826=e_815),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f1464,f19196])).
% 84.28/11.09 fof(f20117,plain,(
% 84.28/11.09 ~e_822=e_826|e_815=e_826),
% 84.28/11.09 inference(equality_factoring,[status(thm)],[f19236])).
% 84.28/11.09 fof(f20129,plain,(
% 84.28/11.09 e_815=e_826),
% 84.28/11.09 inference(forward_subsumption_resolution,[status(thm)],[f20117,f19235])).
% 84.28/11.09 fof(f20161,plain,(
% 84.28/11.09 e_805=e_826|e_805=e_822),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f20129,f17202])).
% 84.28/11.09 fof(f20167,plain,(
% 84.28/11.09 ![X0,X1]: (X0=i5|store(store(a_814,X0,X1),i5,e_826)=store(a_816,X0,X1))),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f20129,f754])).
% 84.28/11.09 fof(f20180,plain,(
% 84.28/11.09 store(a_816,i5,e_826)=a_816),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f20129,f759])).
% 84.28/11.09 fof(f20181,plain,(
% 84.28/11.09 store(a_814,i2,e_826)=a_814),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f20129,f120])).
% 84.28/11.09 fof(f20183,plain,(
% 84.28/11.09 e_826=select(a_814,i2)),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f20129,f103])).
% 84.28/11.09 fof(f20246,plain,(
% 84.28/11.09 store(a_795,i2,e_822)=a_793|e_805=e_826),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f20161,f12166])).
% 84.28/11.09 fof(f20255,plain,(
% 84.28/11.09 ~e_822=e_826|e_805=e_826),
% 84.28/11.09 inference(equality_factoring,[status(thm)],[f20161])).
% 84.28/11.09 fof(f20258,plain,(
% 84.28/11.09 a_795=a_793|e_805=e_826),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f11953,f20246])).
% 84.28/11.09 fof(f20281,plain,(
% 84.28/11.09 a_795=a_812|e_805=e_826|a_814=a_793),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f11146,f20258])).
% 84.28/11.09 fof(f20871,plain,(
% 84.28/11.09 e_805=select(a_814,i2)|a_795=a_812|e_805=e_826),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f20281,f1462])).
% 84.28/11.09 fof(f20876,plain,(
% 84.28/11.09 e_805=e_826|a_795=a_812|e_805=e_826),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20183,f20871])).
% 84.28/11.09 fof(f20877,plain,(
% 84.28/11.09 e_805=e_826|a_795=a_812),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f20876])).
% 84.28/11.09 fof(f20882,plain,(
% 84.28/11.09 select(a_812,i2)=e_822|e_805=e_826),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f20877,f11374])).
% 84.28/11.09 fof(f21709,plain,(
% 84.28/11.09 store(a_823,i5,e_826)=a_821),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f777,f1833])).
% 84.28/11.09 fof(f21757,plain,(
% 84.28/11.09 select(a_814,i2)=e_822|e_805=e_826|i0=i2),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f751,f20882])).
% 84.28/11.09 fof(f21766,plain,(
% 84.28/11.09 e_826=e_822|e_805=e_826|i0=i2),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20183,f21757])).
% 84.28/11.09 fof(f21767,plain,(
% 84.28/11.09 e_805=e_826|i0=i2),
% 84.28/11.09 inference(forward_subsumption_resolution,[status(thm)],[f21766,f20255])).
% 84.28/11.09 fof(f22017,plain,(
% 84.28/11.09 e_822=select(a_821,i0)|e_805=e_826),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f21767,f106])).
% 84.28/11.09 fof(f22313,plain,(
% 84.28/11.09 e_822=select(a_821,i5)|e_805=e_826|a_814=a_793),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f10822,f22017])).
% 84.28/11.09 fof(f22317,plain,(
% 84.28/11.09 e_822=e_826|e_805=e_826|a_814=a_793),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f986,f22313])).
% 84.28/11.09 fof(f22318,plain,(
% 84.28/11.09 e_805=e_826|a_814=a_793),
% 84.28/11.09 inference(forward_subsumption_resolution,[status(thm)],[f22317,f20255])).
% 84.28/11.09 fof(f22334,plain,(
% 84.28/11.09 e_805=select(a_814,i2)|e_805=e_826),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f22318,f1462])).
% 84.28/11.09 fof(f22341,plain,(
% 84.28/11.09 e_805=e_826|e_805=e_826),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20183,f22334])).
% 84.28/11.09 fof(f22342,plain,(
% 84.28/11.09 e_805=e_826),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f22341])).
% 84.28/11.09 fof(f22395,plain,(
% 84.28/11.09 ![X0,X1]: (X0=i5|store(store(a_804,X0,X1),i5,e_826)=store(a_806,X0,X1))),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f505])).
% 84.28/11.09 fof(f22397,plain,(
% 84.28/11.09 store(a_802,i5,e_826)=a_800),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f13245])).
% 84.28/11.09 fof(f22399,plain,(
% 84.28/11.09 store(a_795,i2,e_826)=a_793),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f12166])).
% 84.28/11.09 fof(f22404,plain,(
% 84.28/11.09 store(a_806,i5,e_826)=a_806),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f738])).
% 84.28/11.09 fof(f22408,plain,(
% 84.28/11.09 store(a_804,i2,e_826)=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f124])).
% 84.28/11.09 fof(f22417,plain,(
% 84.28/11.09 e_826=select(a_804,i2)),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f22342,f99])).
% 84.28/11.09 fof(f22576,plain,(
% 84.28/11.09 i2=i5|select(a_825,i5)=e_822),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f779,f982])).
% 84.28/11.09 fof(f22580,plain,(
% 84.28/11.09 i2=i5|e_828=e_822),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f109,f22576])).
% 84.28/11.09 fof(f22836,plain,(
% 84.28/11.09 e_826=select(a_804,i5)|e_828=e_822),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f22580,f22417])).
% 84.28/11.09 fof(f22956,plain,(
% 84.28/11.09 e_826=select(a_825,i5)|e_828=e_822),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f22580,f108])).
% 84.28/11.09 fof(f22972,plain,(
% 84.28/11.09 e_826=e_822|e_828=e_822),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f14919,f22836])).
% 84.28/11.09 fof(f22995,plain,(
% 84.28/11.09 e_826=e_828|e_828=e_822),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f109,f22956])).
% 84.28/11.09 fof(f23039,plain,(
% 84.28/11.09 ~e_826=e_828|e_822=e_828),
% 84.28/11.09 inference(equality_factoring,[status(thm)],[f22972])).
% 84.28/11.09 fof(f23550,plain,(
% 84.28/11.09 ![X0,X1]: (X0=i5|store(store(a_821,X0,X1),i5,e_828)=store(a_823,X0,X1))),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f775])).
% 84.28/11.09 fof(f23554,plain,(
% 84.28/11.09 store(a_816,i5,e_828)=a_814),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f16327])).
% 84.28/11.09 fof(f23570,plain,(
% 84.28/11.09 store(a_808,i2,e_828)=a_808),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f14918])).
% 84.28/11.09 fof(f23571,plain,(
% 84.28/11.09 store(a_806,i5,e_828)=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f14932])).
% 84.28/11.09 fof(f23579,plain,(
% 84.28/11.09 store(a_812,i5,e_828)=a_812),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11380])).
% 84.28/11.09 fof(f23581,plain,(
% 84.28/11.09 store(a_800,i2,e_828)=a_800),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f12014])).
% 84.28/11.09 fof(f23582,plain,(
% 84.28/11.09 store(a_802,i5,e_828)=a_802),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11996])).
% 84.28/11.09 fof(f23584,plain,(
% 84.28/11.09 store(a_795,i2,e_828)=a_795),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11953])).
% 84.28/11.09 fof(f23585,plain,(
% 84.28/11.09 store(a_810,i0,e_828)=a_810),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11934])).
% 84.28/11.09 fof(f23587,plain,(
% 84.28/11.09 select(a_812,i5)=e_828),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11382])).
% 84.28/11.09 fof(f23592,plain,(
% 84.28/11.09 e_794=e_828),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11379])).
% 84.28/11.09 fof(f23596,plain,(
% 84.28/11.09 e_828=e_813|a_814=a_793),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f11135])).
% 84.28/11.09 fof(f23597,plain,(
% 84.28/11.09 store(a_823,i5,e_828)=a_823),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f978])).
% 84.28/11.09 fof(f23600,plain,(
% 84.28/11.09 store(a_821,i2,e_828)=a_821),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f23603,f117])).
% 84.28/11.09 fof(f23603,plain,(
% 84.28/11.09 e_828=e_822),
% 84.28/11.09 inference(forward_subsumption_resolution,[status(thm)],[f22995,f23039])).
% 84.28/11.09 fof(f24081,plain,(
% 84.28/11.09 i2=i5|store(a_821,i5,e_828)=store(a_823,i2,e_828)),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f23600,f23550])).
% 84.28/11.09 fof(f24101,plain,(
% 84.28/11.09 i2=i5|store(a_823,i5,e_828)=store(a_823,i2,e_828)),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f777,f24081])).
% 84.28/11.09 fof(f24102,plain,(
% 84.28/11.09 i2=i5|a_823=store(a_823,i2,e_828)),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23597,f24101])).
% 84.28/11.09 fof(f24103,plain,(
% 84.28/11.09 i2=i5|a_823=store(a_825,i2,e_828)),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f981,f24102])).
% 84.28/11.09 fof(f26028,plain,(
% 84.28/11.09 ![X0]: (store(a_802,i5,X0)=store(a_795,i5,X0))),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f495,f1292])).
% 84.28/11.09 fof(f26264,plain,(
% 84.28/11.09 store(a_802,i5,e_794)=a_795|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f26028,f5018])).
% 84.28/11.09 fof(f26265,plain,(
% 84.28/11.09 store(a_802,i5,e_828)=a_795|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23592,f26264])).
% 84.28/11.09 fof(f26266,plain,(
% 84.28/11.09 a_802=a_795|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23582,f26265])).
% 84.28/11.09 fof(f26284,plain,(
% 84.28/11.09 store(a_795,i5,e_828)=a_795|a_802=a_795),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26266,f23584])).
% 84.28/11.09 fof(f26410,plain,(
% 84.28/11.09 store(a_802,i5,e_828)=a_795|a_802=a_795),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f26028,f26284])).
% 84.28/11.09 fof(f26411,plain,(
% 84.28/11.09 a_802=a_795|a_802=a_795),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23582,f26410])).
% 84.28/11.09 fof(f26412,plain,(
% 84.28/11.09 a_802=a_795),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f26411])).
% 84.28/11.09 fof(f26444,plain,(
% 84.28/11.09 store(a_795,i2,e_828)=a_802),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26412,f23584])).
% 84.28/11.09 fof(f26447,plain,(
% 84.28/11.09 store(a_802,i2,e_826)=a_793),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26412,f22399])).
% 84.28/11.09 fof(f26451,plain,(
% 84.28/11.09 store(a_802,i2,e_828)=a_802),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f26412,f26444])).
% 84.28/11.09 fof(f26452,plain,(
% 84.28/11.09 store(a_804,i2,e_828)=a_802),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f501,f26451])).
% 84.28/11.09 fof(f26453,plain,(
% 84.28/11.09 store(a_804,i2,e_826)=a_793),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f501,f26447])).
% 84.28/11.09 fof(f26454,plain,(
% 84.28/11.09 a_804=a_793),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f22408,f26453])).
% 84.28/11.09 fof(f26464,plain,(
% 84.28/11.09 e_828=e_813|a_814=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f23596])).
% 84.28/11.09 fof(f26479,plain,(
% 84.28/11.09 ![X0]: (store(a_804,i5,X0)=store(a_791,i5,X0))),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f333])).
% 84.28/11.09 fof(f26480,plain,(
% 84.28/11.09 ~a_812=a_814|a_804=a_814),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f11185])).
% 84.28/11.09 fof(f26481,plain,(
% 84.28/11.09 a_793=a_812|a_814=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f11146])).
% 84.28/11.09 fof(f26482,plain,(
% 84.28/11.09 a_812=a_810|a_814=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f11134])).
% 84.28/11.09 fof(f26484,plain,(
% 84.28/11.09 i5=i0|a_814=a_804),
% 84.28/11.09 inference(backward_demodulation,[status(thm)],[f26454,f10822])).
% 84.28/11.09 fof(f26491,plain,(
% 84.28/11.09 ![X0]: (store(a_806,i5,X0)=store(a_791,i5,X0))),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f26479])).
% 84.28/11.09 fof(f26492,plain,(
% 84.28/11.09 a_804=a_812|a_814=a_804),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f26454,f26481])).
% 84.28/11.09 fof(f26627,plain,(
% 84.28/11.09 store(a_814,i2,e_828)=a_802|a_812=a_810),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26482,f26452])).
% 84.28/11.09 fof(f26635,plain,(
% 84.28/11.09 i2=i5|store(a_802,i5,e_826)=store(a_806,i2,e_828)),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26452,f22395])).
% 84.28/11.09 fof(f26654,plain,(
% 84.28/11.09 i2=i5|a_800=store(a_806,i2,e_828)),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f22397,f26635])).
% 84.28/11.09 fof(f26655,plain,(
% 84.28/11.09 i2=i5|a_800=store(a_808,i2,e_828)),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f146,f26654])).
% 84.28/11.09 fof(f26656,plain,(
% 84.28/11.09 i2=i5|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23570,f26655])).
% 84.28/11.09 fof(f26661,plain,(
% 84.28/11.09 store(a_804,i5,e_828)=a_802|a_800=a_808),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26656,f26452])).
% 84.28/11.09 fof(f26674,plain,(
% 84.28/11.09 store(a_800,i5,e_828)=a_800|a_800=a_808),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26656,f23581])).
% 84.28/11.09 fof(f26681,plain,(
% 84.28/11.09 store(a_804,i5,e_826)=a_804|a_800=a_808),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26656,f22408])).
% 84.28/11.09 fof(f26789,plain,(
% 84.28/11.09 store(a_806,i5,e_828)=a_802|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f26661])).
% 84.28/11.09 fof(f26790,plain,(
% 84.28/11.09 a_804=a_802|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23571,f26789])).
% 84.28/11.09 fof(f26793,plain,(
% 84.28/11.09 store(a_802,i5,e_828)=a_800|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f495,f26674])).
% 84.28/11.09 fof(f26794,plain,(
% 84.28/11.09 a_802=a_800|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23582,f26793])).
% 84.28/11.09 fof(f26797,plain,(
% 84.28/11.09 store(a_806,i5,e_826)=a_804|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f26681])).
% 84.28/11.09 fof(f26798,plain,(
% 84.28/11.09 a_806=a_804|a_800=a_808),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f22404,f26797])).
% 84.28/11.09 fof(f26869,plain,(
% 84.28/11.09 ~a_802=a_808|a_800=a_808),
% 84.28/11.09 inference(equality_factoring,[status(thm)],[f26794])).
% 84.28/11.09 fof(f29374,plain,(
% 84.28/11.09 i2=i5|store(a_823,i5,e_826)=store(a_827,i2,e_828)|i2=i5),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f24103,f988])).
% 84.28/11.09 fof(f29398,plain,(
% 84.28/11.09 i2=i5|a_821=store(a_827,i2,e_828)|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f21709,f29374])).
% 84.28/11.09 fof(f29399,plain,(
% 84.28/11.09 i2=i5|a_821=store(a_829,i2,e_828)|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f145,f29398])).
% 84.28/11.09 fof(f29400,plain,(
% 84.28/11.09 i2=i5|a_821=a_829|i2=i5),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f136,f29399])).
% 84.28/11.09 fof(f29401,plain,(
% 84.28/11.09 i2=i5|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f29400])).
% 84.28/11.09 fof(f29419,plain,(
% 84.28/11.09 store(a_804,i5,e_828)=a_802|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29401,f26452])).
% 84.28/11.09 fof(f29432,plain,(
% 84.28/11.09 store(a_800,i5,e_828)=a_800|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29401,f23581])).
% 84.28/11.09 fof(f29439,plain,(
% 84.28/11.09 store(a_804,i5,e_826)=a_804|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29401,f22408])).
% 84.28/11.09 fof(f29447,plain,(
% 84.28/11.09 store(a_814,i5,e_826)=a_814|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29401,f20181])).
% 84.28/11.09 fof(f29552,plain,(
% 84.28/11.09 store(a_806,i5,e_828)=a_802|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f29419])).
% 84.28/11.09 fof(f29553,plain,(
% 84.28/11.09 a_804=a_802|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23571,f29552])).
% 84.28/11.09 fof(f29556,plain,(
% 84.28/11.09 store(a_802,i5,e_828)=a_800|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f495,f29432])).
% 84.28/11.09 fof(f29557,plain,(
% 84.28/11.09 a_802=a_800|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23582,f29556])).
% 84.28/11.09 fof(f29560,plain,(
% 84.28/11.09 store(a_806,i5,e_826)=a_804|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f29439])).
% 84.28/11.09 fof(f29561,plain,(
% 84.28/11.09 a_806=a_804|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f22404,f29560])).
% 84.28/11.09 fof(f29563,plain,(
% 84.28/11.09 store(a_816,i5,e_826)=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f756,f29447])).
% 84.28/11.09 fof(f29564,plain,(
% 84.28/11.09 a_816=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20180,f29563])).
% 84.28/11.09 fof(f29595,plain,(
% 84.28/11.09 store(a_804,i5,e_826)=a_800|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29553,f22397])).
% 84.28/11.09 fof(f29604,plain,(
% 84.28/11.09 store(a_806,i5,e_826)=a_800|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f507,f29595])).
% 84.28/11.09 fof(f29605,plain,(
% 84.28/11.09 a_806=a_800|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f22404,f29604])).
% 84.28/11.09 fof(f29857,plain,(
% 84.28/11.09 a_806=a_814|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26482,f29561])).
% 84.28/11.09 fof(f29859,plain,(
% 84.28/11.09 a_806=a_814|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26464,f29561])).
% 84.28/11.09 fof(f29870,plain,(
% 84.28/11.09 store(a_806,i2,e_828)=a_802|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29561,f26452])).
% 84.28/11.09 fof(f29884,plain,(
% 84.28/11.09 store(a_808,i2,e_828)=a_802|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f146,f29870])).
% 84.28/11.09 fof(f29885,plain,(
% 84.28/11.09 a_808=a_802|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23570,f29884])).
% 84.28/11.09 fof(f30164,plain,(
% 84.28/11.09 a_806=a_802|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29557,f29605])).
% 84.28/11.09 fof(f30196,plain,(
% 84.28/11.09 a_806=a_802|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f30164])).
% 84.28/11.09 fof(f30202,plain,(
% 84.28/11.09 a_808=a_804|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29553,f29885])).
% 84.28/11.09 fof(f30224,plain,(
% 84.28/11.09 a_808=a_804|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f30202])).
% 84.28/11.09 fof(f30227,plain,(
% 84.28/11.09 a_806=a_808|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29885,f30196])).
% 84.28/11.09 fof(f30251,plain,(
% 84.28/11.09 a_806=a_808|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f30227])).
% 84.28/11.09 fof(f30302,plain,(
% 84.28/11.09 a_808=a_812|a_821=a_829|a_814=a_804),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f26492,f30224])).
% 84.28/11.09 fof(f30856,plain,(
% 84.28/11.09 store(a_814,i5,e_826)=a_806|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29857,f22404])).
% 84.28/11.09 fof(f30895,plain,(
% 84.28/11.09 store(a_816,i5,e_826)=a_806|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f756,f30856])).
% 84.28/11.09 fof(f30896,plain,(
% 84.28/11.09 a_816=a_806|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20180,f30895])).
% 84.28/11.09 fof(f30955,plain,(
% 84.28/11.09 store(a_814,i5,e_826)=a_806|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29859,f22404])).
% 84.28/11.09 fof(f30994,plain,(
% 84.28/11.09 store(a_816,i5,e_826)=a_806|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f756,f30955])).
% 84.28/11.09 fof(f30995,plain,(
% 84.28/11.09 a_816=a_806|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20180,f30994])).
% 84.28/11.09 fof(f31364,plain,(
% 84.28/11.09 a_808=a_812|a_821=a_829|a_814=a_806|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29561,f30302])).
% 84.28/11.09 fof(f31403,plain,(
% 84.28/11.09 a_808=a_812|a_821=a_829|a_814=a_806),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f31364])).
% 84.28/11.09 fof(f31527,plain,(
% 84.28/11.09 a_816=a_808|a_821=a_829|a_812=a_810|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f30251,f30896])).
% 84.28/11.09 fof(f31581,plain,(
% 84.28/11.09 a_816=a_808|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f31527])).
% 84.28/11.09 fof(f31737,plain,(
% 84.28/11.09 a_816=a_808|a_821=a_829|e_828=e_813|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f30251,f30995])).
% 84.28/11.09 fof(f31796,plain,(
% 84.28/11.09 a_816=a_808|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f31737])).
% 84.28/11.09 fof(f32155,plain,(
% 84.28/11.09 store(a_814,i5,e_826)=a_806|a_808=a_812|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f31403,f22404])).
% 84.28/11.09 fof(f32205,plain,(
% 84.28/11.09 store(a_816,i5,e_826)=a_806|a_808=a_812|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f756,f32155])).
% 84.28/11.09 fof(f32206,plain,(
% 84.28/11.09 a_816=a_806|a_808=a_812|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f20180,f32205])).
% 84.28/11.09 fof(f32233,plain,(
% 84.28/11.09 store(a_816,i2,e_828)=a_808|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f31581,f23570])).
% 84.28/11.09 fof(f32278,plain,(
% 84.28/11.09 store(a_821,i2,e_828)=a_808|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f17896,f32233])).
% 84.28/11.09 fof(f32279,plain,(
% 84.28/11.09 a_821=a_808|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23600,f32278])).
% 84.28/11.09 fof(f32532,plain,(
% 84.28/11.09 store(a_816,i2,e_828)=a_808|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f31796,f23570])).
% 84.28/11.09 fof(f32577,plain,(
% 84.28/11.09 store(a_821,i2,e_828)=a_808|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f17896,f32532])).
% 84.28/11.09 fof(f32578,plain,(
% 84.28/11.09 a_821=a_808|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23600,f32577])).
% 84.28/11.09 fof(f32826,plain,(
% 84.28/11.09 a_816=a_808|a_808=a_812|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f30251,f32206])).
% 84.28/11.09 fof(f32890,plain,(
% 84.28/11.09 a_816=a_808|a_808=a_812|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f32826])).
% 84.28/11.09 fof(f33005,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829|a_812=a_810|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f31581,f32279])).
% 84.28/11.09 fof(f33068,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829|a_812=a_810),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f33005])).
% 84.28/11.09 fof(f33094,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829|e_828=e_813|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f31796,f32578])).
% 84.28/11.09 fof(f33158,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829|e_828=e_813),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f33094])).
% 84.28/11.09 fof(f33338,plain,(
% 84.28/11.09 a_821=a_829|~a_812=a_816|a_808=a_816),
% 84.28/11.09 inference(equality_factoring,[status(thm)],[f32890])).
% 84.28/11.09 fof(f33375,plain,(
% 84.28/11.09 a_791=store(a_812,i0,e_813)|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f33068,f9982])).
% 84.28/11.09 fof(f33380,plain,(
% 84.28/11.09 a_791=store(a_814,i0,e_813)|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f750,f33375])).
% 84.28/11.09 fof(f33381,plain,(
% 84.28/11.09 a_791=a_814|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f753,f33380])).
% 84.28/11.09 fof(f33721,plain,(
% 84.28/11.09 a_791=store(a_810,i0,e_828)|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f33158,f9982])).
% 84.28/11.09 fof(f33727,plain,(
% 84.28/11.09 a_791=a_810|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23585,f33721])).
% 84.28/11.09 fof(f34021,plain,(
% 84.28/11.09 a_814=a_810|a_821=a_816|a_821=a_829|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f33381,f33727])).
% 84.28/11.09 fof(f34037,plain,(
% 84.28/11.09 a_814=a_810|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f34021])).
% 84.28/11.09 fof(f34244,plain,(
% 84.28/11.09 a_814=a_812|a_821=a_816|a_821=a_829|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f33068,f34037])).
% 84.28/11.09 fof(f34264,plain,(
% 84.28/11.09 a_814=a_812|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f34244])).
% 84.28/11.09 fof(f34385,plain,(
% 84.28/11.09 a_821=a_829|~a_814=a_816|a_808=a_816|a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f34264,f33338])).
% 84.28/11.09 fof(f34403,plain,(
% 84.28/11.09 a_821=a_829|~a_814=a_816|a_808=a_816|a_821=a_816),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f34385])).
% 84.28/11.09 fof(f34404,plain,(
% 84.28/11.09 a_821=a_829|a_808=a_816|a_821=a_816),
% 84.28/11.09 inference(forward_subsumption_resolution,[status(thm)],[f34403,f29564])).
% 84.28/11.09 fof(f34783,plain,(
% 84.28/11.09 store(a_816,i2,e_828)=a_808|a_821=a_829|a_821=a_816),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f34404,f23570])).
% 84.28/11.09 fof(f34840,plain,(
% 84.28/11.09 store(a_821,i2,e_828)=a_808|a_821=a_829|a_821=a_816),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f17896,f34783])).
% 84.28/11.09 fof(f34841,plain,(
% 84.28/11.09 a_821=a_808|a_821=a_829|a_821=a_816),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23600,f34840])).
% 84.28/11.09 fof(f35048,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829|a_821=a_816|a_821=a_829|a_821=a_816),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f34404,f34841])).
% 84.28/11.09 fof(f35125,plain,(
% 84.28/11.09 a_821=a_816|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f35048])).
% 84.28/11.09 fof(f35166,plain,(
% 84.28/11.09 store(a_821,i5,e_828)=a_814|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f35125,f23554])).
% 84.28/11.09 fof(f35176,plain,(
% 84.28/11.09 store(a_823,i5,e_828)=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f777,f35166])).
% 84.28/11.09 fof(f35177,plain,(
% 84.28/11.09 a_823=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f23597,f35176])).
% 84.28/11.09 fof(f35193,plain,(
% 84.28/11.09 store(a_823,i2,e_826)=a_814|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f35177,f20181])).
% 84.28/11.09 fof(f35208,plain,(
% 84.28/11.09 store(a_825,i2,e_826)=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f981,f35193])).
% 84.28/11.09 fof(f35209,plain,(
% 84.28/11.09 a_825=a_814|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f300,f35208])).
% 84.28/11.09 fof(f35239,plain,(
% 84.28/11.09 a_825=a_816|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f29564,f35209])).
% 84.28/11.09 fof(f35260,plain,(
% 84.28/11.09 a_825=a_816|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f35239])).
% 84.28/11.09 fof(f35299,plain,(
% 84.28/11.09 store(a_825,i5,e_826)=a_816|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f35260,f20180])).
% 84.28/11.09 fof(f35314,plain,(
% 84.28/11.09 store(a_827,i5,e_826)=a_816|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f990,f35299])).
% 84.28/11.09 fof(f35315,plain,(
% 84.28/11.09 a_827=a_816|a_821=a_829),
% 84.28/11.09 inference(forward_demodulation,[status(thm)],[f997,f35314])).
% 84.28/11.09 fof(f35343,plain,(
% 84.28/11.09 a_827=a_821|a_821=a_829|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f35125,f35315])).
% 84.28/11.09 fof(f35362,plain,(
% 84.28/11.09 a_827=a_821|a_821=a_829),
% 84.28/11.09 inference(duplicate_literals_removal,[status(thm)],[f35343])).
% 84.28/11.09 fof(f35408,plain,(
% 84.28/11.09 store(a_827,i2,e_828)=a_821|a_821=a_829),
% 84.28/11.09 inference(paramodulation,[status(thm)],[f35362,f23600])).
% 84.28/11.10 fof(f35422,plain,(
% 84.28/11.10 store(a_829,i2,e_828)=a_821|a_821=a_829),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f145,f35408])).
% 84.28/11.10 fof(f35423,plain,(
% 84.28/11.10 a_829=a_821|a_821=a_829),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f136,f35422])).
% 84.28/11.10 fof(f35424,plain,(
% 84.28/11.10 a_829=a_821),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f35423])).
% 84.28/11.10 fof(f35526,plain,(
% 84.28/11.10 ![X0]: (store(a_823,i5,X0)=store(a_829,i5,X0))),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f35424,f777])).
% 84.28/11.10 fof(f35529,plain,(
% 84.28/11.10 ![X0]: (store(a_829,i2,X0)=store(a_816,i2,X0))),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f35424,f17896])).
% 84.28/11.10 fof(f35844,plain,(
% 84.28/11.10 store(a_829,i5,e_828)=a_823),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f35526,f23597])).
% 84.28/11.10 fof(f36829,plain,(
% 84.28/11.10 store(a_814,i5,e_828)=a_802|a_812=a_810|a_800=a_808),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f26656,f26627])).
% 84.28/11.10 fof(f36835,plain,(
% 84.28/11.10 i2=i5|store(a_802,i5,e_826)=store(a_816,i2,e_828)|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f26627,f20167])).
% 84.28/11.10 fof(f36852,plain,(
% 84.28/11.10 store(a_816,i5,e_828)=a_802|a_812=a_810|a_800=a_808),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f36829])).
% 84.28/11.10 fof(f36853,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810|a_800=a_808),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f36852])).
% 84.28/11.10 fof(f36859,plain,(
% 84.28/11.10 i2=i5|a_800=store(a_816,i2,e_828)|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f22397,f36835])).
% 84.28/11.10 fof(f36860,plain,(
% 84.28/11.10 i2=i5|a_800=store(a_829,i2,e_828)|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35529,f36859])).
% 84.28/11.10 fof(f36861,plain,(
% 84.28/11.10 i2=i5|a_800=a_829|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f136,f36860])).
% 84.28/11.10 fof(f36900,plain,(
% 84.28/11.10 store(a_814,i5,e_828)=a_802|a_812=a_810|a_800=a_829|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f36861,f26627])).
% 84.28/11.10 fof(f37051,plain,(
% 84.28/11.10 store(a_816,i5,e_828)=a_802|a_812=a_810|a_800=a_829|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f36900])).
% 84.28/11.10 fof(f37052,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810|a_800=a_829|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f37051])).
% 84.28/11.10 fof(f37053,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810|a_800=a_829),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f37052])).
% 84.28/11.10 fof(f37087,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810|a_808=a_829|a_814=a_802|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f36853,f37053])).
% 84.28/11.10 fof(f37120,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810|a_808=a_829),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f37087])).
% 84.28/11.10 fof(f37121,plain,(
% 84.28/11.10 a_814=a_802|a_812=a_810),
% 84.28/11.10 inference(forward_subsumption_resolution,[status(thm)],[f37120,f110])).
% 84.28/11.10 fof(f37164,plain,(
% 84.28/11.10 store(a_814,i5,e_826)=a_800|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f37121,f22397])).
% 84.28/11.10 fof(f37173,plain,(
% 84.28/11.10 store(a_816,i5,e_826)=a_800|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f37164])).
% 84.28/11.10 fof(f37174,plain,(
% 84.28/11.10 a_816=a_800|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f20180,f37173])).
% 84.28/11.10 fof(f37221,plain,(
% 84.28/11.10 store(a_816,i2,e_828)=a_800|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f37174,f23581])).
% 84.28/11.10 fof(f37230,plain,(
% 84.28/11.10 store(a_829,i2,e_828)=a_800|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35529,f37221])).
% 84.28/11.10 fof(f37231,plain,(
% 84.28/11.10 a_829=a_800|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f136,f37230])).
% 84.28/11.10 fof(f37269,plain,(
% 84.28/11.10 a_829=a_808|a_812=a_810|a_806=a_804),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f26798,f37231])).
% 84.28/11.10 fof(f37302,plain,(
% 84.28/11.10 a_812=a_810|a_806=a_804),
% 84.28/11.10 inference(forward_subsumption_resolution,[status(thm)],[f37269,f110])).
% 84.28/11.10 fof(f37456,plain,(
% 84.28/11.10 store(a_806,i2,e_828)=a_802|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f37302,f26452])).
% 84.28/11.10 fof(f37472,plain,(
% 84.28/11.10 store(a_808,i2,e_828)=a_802|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f146,f37456])).
% 84.28/11.10 fof(f37473,plain,(
% 84.28/11.10 a_808=a_802|a_812=a_810),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23570,f37472])).
% 84.28/11.10 fof(f37883,plain,(
% 84.28/11.10 a_812=a_810|a_800=a_808),
% 84.28/11.10 inference(resolution,[status(thm)],[f37473,f26869])).
% 84.28/11.10 fof(f38334,plain,(
% 84.28/11.10 a_812=a_810|a_829=a_808|a_812=a_810),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f37231,f37883])).
% 84.28/11.10 fof(f38371,plain,(
% 84.28/11.10 a_812=a_810|a_829=a_808),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f38334])).
% 84.28/11.10 fof(f38372,plain,(
% 84.28/11.10 a_812=a_810),
% 84.28/11.10 inference(forward_subsumption_resolution,[status(thm)],[f38371,f110])).
% 84.28/11.10 fof(f38410,plain,(
% 84.28/11.10 store(a_810,i0,e_828)=a_812),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38372,f23585])).
% 84.28/11.10 fof(f38419,plain,(
% 84.28/11.10 ![X0,X1]: (X0=i0|store(store(a_812,X0,X1),i0,e_813)=store(a_791,X0,X1))),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38372,f10784])).
% 84.28/11.10 fof(f38424,plain,(
% 84.28/11.10 a_791=store(a_812,i0,e_813)),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38372,f9982])).
% 84.28/11.10 fof(f38427,plain,(
% 84.28/11.10 select(a_812,i2)=e_786),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38372,f519])).
% 84.28/11.10 fof(f38428,plain,(
% 84.28/11.10 e_813=select(a_812,i5)),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38372,f102])).
% 84.28/11.10 fof(f38432,plain,(
% 84.28/11.10 store(a_812,i0,e_828)=a_812),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f38372,f38410])).
% 84.28/11.10 fof(f38433,plain,(
% 84.28/11.10 store(a_814,i0,e_828)=a_812),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f750,f38432])).
% 84.28/11.10 fof(f38436,plain,(
% 84.28/11.10 a_791=store(a_814,i0,e_813)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f750,f38424])).
% 84.28/11.10 fof(f38437,plain,(
% 84.28/11.10 a_791=a_814),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f753,f38436])).
% 84.28/11.10 fof(f38439,plain,(
% 84.28/11.10 e_813=e_828),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23587,f38428])).
% 84.28/11.10 fof(f38448,plain,(
% 84.28/11.10 ![X0]: (store(a_806,i5,X0)=store(a_814,i5,X0))),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38437,f26491])).
% 84.28/11.10 fof(f38455,plain,(
% 84.28/11.10 ![X0]: (store(a_806,i5,X0)=store(a_816,i5,X0))),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f38448])).
% 84.28/11.10 fof(f38754,plain,(
% 84.28/11.10 store(a_814,i5,e_828)=a_812|a_814=a_804),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f26484,f38433])).
% 84.28/11.10 fof(f38772,plain,(
% 84.28/11.10 store(a_816,i5,e_828)=a_812|a_814=a_804),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f38754])).
% 84.28/11.10 fof(f38773,plain,(
% 84.28/11.10 a_814=a_812|a_814=a_804),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f38772])).
% 84.28/11.10 fof(f38774,plain,(
% 84.28/11.10 a_814=a_804),
% 84.28/11.10 inference(forward_subsumption_resolution,[status(thm)],[f38773,f26480])).
% 84.28/11.10 fof(f38828,plain,(
% 84.28/11.10 a_814=a_802|a_800=a_808),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38774,f26790])).
% 84.28/11.10 fof(f38829,plain,(
% 84.28/11.10 store(a_814,i2,e_828)=a_802),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38774,f26452])).
% 84.28/11.10 fof(f38882,plain,(
% 84.28/11.10 store(a_812,i2,e_786)=a_812),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f38427,f58])).
% 84.28/11.10 fof(f39012,plain,(
% 84.28/11.10 ![X0,X1]: (X0=i0|store(store(a_812,X0,X1),i0,e_828)=store(a_791,X0,X1))),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f38439,f38419])).
% 84.28/11.10 fof(f39013,plain,(
% 84.28/11.10 ![X0,X1]: (X0=i0|store(store(a_812,X0,X1),i0,e_828)=store(a_814,X0,X1))),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f38437,f39012])).
% 84.28/11.10 fof(f39019,plain,(
% 84.28/11.10 i5=i0|store(a_812,i0,e_828)=store(a_814,i5,e_828)),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f23579,f39013])).
% 84.28/11.10 fof(f39059,plain,(
% 84.28/11.10 i5=i0|store(a_814,i0,e_828)=store(a_814,i5,e_828)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f750,f39019])).
% 84.28/11.10 fof(f39060,plain,(
% 84.28/11.10 i5=i0|a_812=store(a_814,i5,e_828)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f38433,f39059])).
% 84.28/11.10 fof(f39061,plain,(
% 84.28/11.10 i5=i0|a_812=store(a_816,i5,e_828)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f39060])).
% 84.28/11.10 fof(f39062,plain,(
% 84.28/11.10 i5=i0|a_812=a_814),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f39061])).
% 84.28/11.10 fof(f39332,plain,(
% 84.28/11.10 store(a_814,i5,e_828)=a_812|a_812=a_814),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f39062,f38433])).
% 84.28/11.10 fof(f39336,plain,(
% 84.28/11.10 store(a_816,i5,e_828)=a_812|a_812=a_814),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f39332])).
% 84.28/11.10 fof(f39337,plain,(
% 84.28/11.10 a_814=a_812|a_812=a_814),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f39336])).
% 84.28/11.10 fof(f39338,plain,(
% 84.28/11.10 a_814=a_812),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f39337])).
% 84.28/11.10 fof(f39346,plain,(
% 84.28/11.10 select(a_814,i2)=e_786),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39338,f38427])).
% 84.28/11.10 fof(f39365,plain,(
% 84.28/11.10 e_826=e_786),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f20183,f39346])).
% 84.28/11.10 fof(f39499,plain,(
% 84.28/11.10 i2=i5|store(a_802,i5,e_826)=store(a_816,i2,e_828)),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f38829,f20167])).
% 84.28/11.10 fof(f39517,plain,(
% 84.28/11.10 i2=i5|a_800=store(a_816,i2,e_828)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f22397,f39499])).
% 84.28/11.10 fof(f39518,plain,(
% 84.28/11.10 i2=i5|a_800=store(a_829,i2,e_828)),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35529,f39517])).
% 84.28/11.10 fof(f39519,plain,(
% 84.28/11.10 i2=i5|a_800=a_829),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f136,f39518])).
% 84.28/11.10 fof(f39522,plain,(
% 84.28/11.10 store(a_814,i5,e_828)=a_802|a_800=a_829),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f39519,f38829])).
% 84.28/11.10 fof(f39638,plain,(
% 84.28/11.10 store(a_816,i5,e_828)=a_802|a_800=a_829),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f39522])).
% 84.28/11.10 fof(f39639,plain,(
% 84.28/11.10 a_814=a_802|a_800=a_829),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f23554,f39638])).
% 84.28/11.10 fof(f39664,plain,(
% 84.28/11.10 a_814=a_802|a_808=a_829|a_814=a_802),
% 84.28/11.10 inference(paramodulation,[status(thm)],[f38828,f39639])).
% 84.28/11.10 fof(f39695,plain,(
% 84.28/11.10 a_814=a_802|a_808=a_829),
% 84.28/11.10 inference(duplicate_literals_removal,[status(thm)],[f39664])).
% 84.28/11.10 fof(f39696,plain,(
% 84.28/11.10 a_814=a_802),
% 84.28/11.10 inference(forward_subsumption_resolution,[status(thm)],[f39695,f110])).
% 84.28/11.10 fof(f39711,plain,(
% 84.28/11.10 store(a_816,i5,e_826)=a_806),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f38455,f22404])).
% 84.28/11.10 fof(f39756,plain,(
% 84.28/11.10 a_816=a_806),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f20180,f39711])).
% 84.28/11.10 fof(f39780,plain,(
% 84.28/11.10 a_814=a_800|a_800=a_808),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39696,f26794])).
% 84.28/11.10 fof(f39794,plain,(
% 84.28/11.10 store(a_814,i5,e_826)=a_800),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39696,f22397])).
% 84.28/11.10 fof(f39804,plain,(
% 84.28/11.10 store(a_816,i5,e_826)=a_800),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f756,f39794])).
% 84.28/11.10 fof(f39805,plain,(
% 84.28/11.10 a_816=a_800),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f20180,f39804])).
% 84.28/11.10 fof(f39854,plain,(
% 84.28/11.10 ![X0]: (store(a_808,i2,X0)=store(a_816,i2,X0))),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39756,f146])).
% 84.28/11.10 fof(f39868,plain,(
% 84.28/11.10 ![X0]: (store(a_808,i2,X0)=store(a_829,i2,X0))),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35529,f39854])).
% 84.28/11.10 fof(f39877,plain,(
% 84.28/11.10 i2=i5|a_816=a_808),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39805,f26656])).
% 84.28/11.10 fof(f39880,plain,(
% 84.28/11.10 store(a_800,i2,e_828)=a_816),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39805,f23581])).
% 84.28/11.10 fof(f39890,plain,(
% 84.28/11.10 store(a_816,i2,e_828)=a_816),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f39805,f39880])).
% 84.28/11.10 fof(f39891,plain,(
% 84.28/11.10 store(a_829,i2,e_828)=a_816),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35529,f39890])).
% 84.28/11.10 fof(f39892,plain,(
% 84.28/11.10 a_829=a_816),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f136,f39891])).
% 84.28/11.10 fof(f39895,plain,(
% 84.28/11.10 a_829=a_800),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39892,f39805])).
% 84.28/11.10 fof(f39904,plain,(
% 84.28/11.10 store(a_829,i5,e_828)=a_814),
% 84.28/11.10 inference(backward_demodulation,[status(thm)],[f39892,f23554])).
% 84.28/11.10 fof(f39910,plain,(
% 84.28/11.10 a_823=a_814),
% 84.28/11.10 inference(forward_demodulation,[status(thm)],[f35844,f39904])).
% 44.75/11.13 fof(f40010,plain,(
% 44.75/11.13 a_823=a_812),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f39910,f39338])).
% 44.75/11.13 fof(f40018,plain,(
% 44.75/11.13 store(a_814,i2,e_826)=a_823),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f39910,f20181])).
% 44.75/11.13 fof(f40025,plain,(
% 44.75/11.13 store(a_823,i2,e_826)=a_823),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f39910,f40018])).
% 44.75/11.13 fof(f40026,plain,(
% 44.75/11.13 store(a_825,i2,e_826)=a_823),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f981,f40025])).
% 44.75/11.13 fof(f40027,plain,(
% 44.75/11.13 a_825=a_823),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f300,f40026])).
% 44.75/11.13 fof(f40053,plain,(
% 44.75/11.13 a_825=a_812),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40027,f40010])).
% 44.75/11.13 fof(f40059,plain,(
% 44.75/11.13 a_825=a_814),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40027,f39910])).
% 44.75/11.13 fof(f40387,plain,(
% 44.75/11.13 a_825=a_800|a_800=a_808),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40059,f39780])).
% 44.75/11.13 fof(f40388,plain,(
% 44.75/11.13 a_825=a_829|a_800=a_808),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f39895,f40387])).
% 44.75/11.13 fof(f40389,plain,(
% 44.75/11.13 a_825=a_829|a_829=a_808),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f39895,f40388])).
% 44.75/11.13 fof(f40400,plain,(
% 44.75/11.13 a_829=a_812),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40413,f40053])).
% 44.75/11.13 fof(f40412,plain,(
% 44.75/11.13 e_826=select(a_829,i2)),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40413,f108])).
% 44.75/11.13 fof(f40413,plain,(
% 44.75/11.13 a_825=a_829),
% 44.75/11.13 inference(forward_subsumption_resolution,[status(thm)],[f40389,f110])).
% 44.75/11.13 fof(f40417,plain,(
% 44.75/11.13 e_826=e_828),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f111,f40412])).
% 44.75/11.13 fof(f40429,plain,(
% 44.75/11.13 e_828=e_786),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40417,f39365])).
% 44.75/11.13 fof(f40535,plain,(
% 44.75/11.13 i2=i5|a_829=a_808),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f39892,f39877])).
% 44.75/11.13 fof(f40538,plain,(
% 44.75/11.13 store(a_808,i5,e_828)=a_808),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f40549,f23570])).
% 44.75/11.13 fof(f40549,plain,(
% 44.75/11.13 i2=i5),
% 44.75/11.13 inference(forward_subsumption_resolution,[status(thm)],[f40535,f110])).
% 44.75/11.13 fof(f40584,plain,(
% 44.75/11.13 store(a_829,i2,e_786)=a_812),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40400,f38882])).
% 44.75/11.13 fof(f40585,plain,(
% 44.75/11.13 store(a_829,i5,e_786)=a_812),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40549,f40584])).
% 44.75/11.13 fof(f40586,plain,(
% 44.75/11.13 store(a_829,i5,e_828)=a_812),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40429,f40585])).
% 44.75/11.13 fof(f40587,plain,(
% 44.75/11.13 store(a_829,i5,e_828)=a_829),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40400,f40586])).
% 44.75/11.13 fof(f41079,plain,(
% 44.75/11.13 ![X0]: (store(a_808,i5,X0)=store(a_829,i2,X0))),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40549,f39868])).
% 44.75/11.13 fof(f41080,plain,(
% 44.75/11.13 store(a_829,i5,e_828)=a_808),
% 44.75/11.13 inference(backward_demodulation,[status(thm)],[f41081,f40538])).
% 44.75/11.13 fof(f41081,plain,(
% 44.75/11.13 ![X0]: (store(a_808,i5,X0)=store(a_829,i5,X0))),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40549,f41079])).
% 44.75/11.13 fof(f41098,plain,(
% 44.75/11.13 a_829=a_808),
% 44.75/11.13 inference(forward_demodulation,[status(thm)],[f40587,f41080])).
% 44.75/11.13 fof(f41099,plain,(
% 44.75/11.13 $false),
% 44.75/11.13 inference(forward_subsumption_resolution,[status(thm)],[f41098,f110])).
% 44.75/11.13 % SZS output end CNFRefutation for theBenchmark.p
% 44.75/11.15 % Elapsed time: 10.787124 seconds
% 44.75/11.15 % CPU time: 85.274650 seconds
% 44.75/11.15 % Total memory used: 581.758 MB
% 44.75/11.15 % Net memory used: 490.316 MB
%------------------------------------------------------------------------------