%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV537-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 : n007.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:36 PM UTC 2026
% Result : Unsatisfiable 10.17s 1.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV537-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.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:01:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 10.17/1.71 % Refutation found
% 10.17/1.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.17/1.71 % SZS output start CNFRefutation for theBenchmark
% 10.17/1.71 fof(f1,axiom,(
% 10.17/1.71 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f2,axiom,(
% 10.17/1.71 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f5,hypothesis,(
% 10.17/1.71 a_838 = store(a_836,i2,e_837) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f6,hypothesis,(
% 10.17/1.71 a_840 = store(a_838,i1,e_839) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f7,hypothesis,(
% 10.17/1.71 a_842 = store(a_840,i0,e_841) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f8,hypothesis,(
% 10.17/1.71 a_844 = store(a_842,i5,e_843) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f9,hypothesis,(
% 10.17/1.71 a_846 = store(a_844,i2,e_845) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f10,hypothesis,(
% 10.17/1.71 a_848 = store(a_846,i5,e_847) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f11,hypothesis,(
% 10.17/1.71 a_850 = store(a_848,i1,e_849) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f12,hypothesis,(
% 10.17/1.71 a_851 = store(a_850,i1,e_849) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f13,hypothesis,(
% 10.17/1.71 a_853 = store(a_851,i5,e_852) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f14,hypothesis,(
% 10.17/1.71 a_855 = store(a_853,i2,e_854) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f15,hypothesis,(
% 10.17/1.71 a_857 = store(a_855,i5,e_856) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f16,hypothesis,(
% 10.17/1.71 a_859 = store(a_857,i2,e_858) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f17,hypothesis,(
% 10.17/1.71 a_860 = store(a_836,i1,e_839) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f18,hypothesis,(
% 10.17/1.71 a_861 = store(a_860,i2,e_837) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f19,hypothesis,(
% 10.17/1.71 a_863 = store(a_861,i5,e_862) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f20,hypothesis,(
% 10.17/1.71 a_865 = store(a_863,i0,e_864) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f21,hypothesis,(
% 10.17/1.71 a_867 = store(a_865,i5,e_866) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f22,hypothesis,(
% 10.17/1.71 a_869 = store(a_867,i2,e_868) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f23,hypothesis,(
% 10.17/1.71 a_871 = store(a_869,i1,e_870) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f24,hypothesis,(
% 10.17/1.71 a_872 = store(a_871,i1,e_870) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f25,hypothesis,(
% 10.17/1.71 a_874 = store(a_872,i5,e_873) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f26,hypothesis,(
% 10.17/1.71 a_876 = store(a_874,i2,e_875) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f27,hypothesis,(
% 10.17/1.71 a_878 = store(a_876,i5,e_877) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f28,hypothesis,(
% 10.17/1.71 a_880 = store(a_878,i2,e_879) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f31,hypothesis,(
% 10.17/1.71 e_837 = select(a_836,i1) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f32,hypothesis,(
% 10.17/1.71 e_839 = select(a_836,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f33,hypothesis,(
% 10.17/1.71 e_841 = select(a_840,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f34,hypothesis,(
% 10.17/1.71 e_843 = select(a_840,i0) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f35,hypothesis,(
% 10.17/1.71 e_845 = select(a_844,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f36,hypothesis,(
% 10.17/1.71 e_847 = select(a_844,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f37,hypothesis,(
% 10.17/1.71 e_849 = select(a_848,i1) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f38,hypothesis,(
% 10.17/1.71 e_852 = select(a_851,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f39,hypothesis,(
% 10.17/1.71 e_854 = select(a_851,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f40,hypothesis,(
% 10.17/1.71 e_856 = select(a_855,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f41,hypothesis,(
% 10.17/1.71 e_858 = select(a_855,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f42,hypothesis,(
% 10.17/1.71 e_862 = select(a_861,i0) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f43,hypothesis,(
% 10.17/1.71 e_864 = select(a_861,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f44,hypothesis,(
% 10.17/1.71 e_866 = select(a_865,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f45,hypothesis,(
% 10.17/1.71 e_868 = select(a_865,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f46,hypothesis,(
% 10.17/1.71 e_870 = select(a_869,i1) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f47,hypothesis,(
% 10.17/1.71 e_873 = select(a_872,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f48,hypothesis,(
% 10.17/1.71 e_875 = select(a_872,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f49,hypothesis,(
% 10.17/1.71 e_877 = select(a_876,i2) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f50,hypothesis,(
% 10.17/1.71 e_879 = select(a_876,i5) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f51,hypothesis,(
% 10.17/1.71 e_882 = select(a_859,i_881) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f52,hypothesis,(
% 10.17/1.71 e_883 = select(a_880,i_881) ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f54,negated_conjecture,(
% 10.17/1.71 e_882 != e_883 ),
% 10.17/1.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.17/1.71 fof(f55,plain,(
% 10.17/1.71 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f1])).
% 10.17/1.71 fof(f56,plain,(
% 10.17/1.71 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 10.17/1.71 inference(miniscoping,[status(thm)],[f2])).
% 10.17/1.71 fof(f57,plain,(
% 10.17/1.71 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f56])).
% 10.17/1.71 fof(f60,plain,(
% 10.17/1.71 a_838=store(a_836,i2,e_837)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f5])).
% 10.17/1.71 fof(f61,plain,(
% 10.17/1.71 a_840=store(a_838,i1,e_839)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f6])).
% 10.17/1.71 fof(f62,plain,(
% 10.17/1.71 a_842=store(a_840,i0,e_841)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f7])).
% 10.17/1.71 fof(f63,plain,(
% 10.17/1.71 a_844=store(a_842,i5,e_843)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f8])).
% 10.17/1.71 fof(f64,plain,(
% 10.17/1.71 a_846=store(a_844,i2,e_845)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f9])).
% 10.17/1.71 fof(f65,plain,(
% 10.17/1.71 a_848=store(a_846,i5,e_847)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f10])).
% 10.17/1.71 fof(f66,plain,(
% 10.17/1.71 a_850=store(a_848,i1,e_849)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f11])).
% 10.17/1.71 fof(f67,plain,(
% 10.17/1.71 a_851=store(a_850,i1,e_849)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f12])).
% 10.17/1.71 fof(f68,plain,(
% 10.17/1.71 a_853=store(a_851,i5,e_852)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f13])).
% 10.17/1.71 fof(f69,plain,(
% 10.17/1.71 a_855=store(a_853,i2,e_854)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f14])).
% 10.17/1.71 fof(f70,plain,(
% 10.17/1.71 a_857=store(a_855,i5,e_856)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f15])).
% 10.17/1.71 fof(f71,plain,(
% 10.17/1.71 a_859=store(a_857,i2,e_858)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f16])).
% 10.17/1.71 fof(f72,plain,(
% 10.17/1.71 a_860=store(a_836,i1,e_839)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f17])).
% 10.17/1.71 fof(f73,plain,(
% 10.17/1.71 a_861=store(a_860,i2,e_837)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f18])).
% 10.17/1.71 fof(f74,plain,(
% 10.17/1.71 a_863=store(a_861,i5,e_862)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f19])).
% 10.17/1.71 fof(f75,plain,(
% 10.17/1.71 a_865=store(a_863,i0,e_864)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f20])).
% 10.17/1.71 fof(f76,plain,(
% 10.17/1.71 a_867=store(a_865,i5,e_866)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f21])).
% 10.17/1.71 fof(f77,plain,(
% 10.17/1.71 a_869=store(a_867,i2,e_868)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f22])).
% 10.17/1.71 fof(f78,plain,(
% 10.17/1.71 a_871=store(a_869,i1,e_870)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f23])).
% 10.17/1.71 fof(f79,plain,(
% 10.17/1.71 a_872=store(a_871,i1,e_870)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f24])).
% 10.17/1.71 fof(f80,plain,(
% 10.17/1.71 a_874=store(a_872,i5,e_873)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f25])).
% 10.17/1.71 fof(f81,plain,(
% 10.17/1.71 a_876=store(a_874,i2,e_875)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f26])).
% 10.17/1.71 fof(f82,plain,(
% 10.17/1.71 a_878=store(a_876,i5,e_877)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f27])).
% 10.17/1.71 fof(f83,plain,(
% 10.17/1.71 a_880=store(a_878,i2,e_879)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f28])).
% 10.17/1.71 fof(f86,plain,(
% 10.17/1.71 e_837=select(a_836,i1)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f31])).
% 10.17/1.71 fof(f87,plain,(
% 10.17/1.71 e_839=select(a_836,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f32])).
% 10.17/1.71 fof(f88,plain,(
% 10.17/1.71 e_841=select(a_840,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f33])).
% 10.17/1.71 fof(f89,plain,(
% 10.17/1.71 e_843=select(a_840,i0)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f34])).
% 10.17/1.71 fof(f90,plain,(
% 10.17/1.71 e_845=select(a_844,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f35])).
% 10.17/1.71 fof(f91,plain,(
% 10.17/1.71 e_847=select(a_844,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f36])).
% 10.17/1.71 fof(f92,plain,(
% 10.17/1.71 e_849=select(a_848,i1)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f37])).
% 10.17/1.71 fof(f93,plain,(
% 10.17/1.71 e_852=select(a_851,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f38])).
% 10.17/1.71 fof(f94,plain,(
% 10.17/1.71 e_854=select(a_851,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f39])).
% 10.17/1.71 fof(f95,plain,(
% 10.17/1.71 e_856=select(a_855,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f40])).
% 10.17/1.71 fof(f96,plain,(
% 10.17/1.71 e_858=select(a_855,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f41])).
% 10.17/1.71 fof(f97,plain,(
% 10.17/1.71 e_862=select(a_861,i0)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f42])).
% 10.17/1.71 fof(f98,plain,(
% 10.17/1.71 e_864=select(a_861,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f43])).
% 10.17/1.71 fof(f99,plain,(
% 10.17/1.71 e_866=select(a_865,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f44])).
% 10.17/1.71 fof(f100,plain,(
% 10.17/1.71 e_868=select(a_865,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f45])).
% 10.17/1.71 fof(f101,plain,(
% 10.17/1.71 e_870=select(a_869,i1)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f46])).
% 10.17/1.71 fof(f102,plain,(
% 10.17/1.71 e_873=select(a_872,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f47])).
% 10.17/1.71 fof(f103,plain,(
% 10.17/1.71 e_875=select(a_872,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f48])).
% 10.17/1.71 fof(f104,plain,(
% 10.17/1.71 e_877=select(a_876,i2)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f49])).
% 10.17/1.71 fof(f105,plain,(
% 10.17/1.71 e_879=select(a_876,i5)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f50])).
% 10.17/1.71 fof(f106,plain,(
% 10.17/1.71 e_882=select(a_859,i_881)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f51])).
% 10.17/1.71 fof(f107,plain,(
% 10.17/1.71 e_883=select(a_880,i_881)),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f52])).
% 10.17/1.71 fof(f109,plain,(
% 10.17/1.71 ~e_882=e_883),
% 10.17/1.71 inference(cnf_transformation,[status(thm)],[f54])).
% 10.17/1.71 fof(f112,plain,(
% 10.17/1.71 select(a_838,i2)=e_837),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f60,f55])).
% 10.17/1.71 fof(f113,plain,(
% 10.17/1.71 select(a_840,i1)=e_839),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f61,f55])).
% 10.17/1.71 fof(f114,plain,(
% 10.17/1.71 select(a_842,i0)=e_841),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f62,f55])).
% 10.17/1.71 fof(f116,plain,(
% 10.17/1.71 ![X0]: (i0=X0|select(a_842,X0)=select(a_840,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f62,f57])).
% 10.17/1.71 fof(f117,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_840,X0)=select(a_838,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f61,f57])).
% 10.17/1.71 fof(f118,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_838,X0)=select(a_836,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f60,f57])).
% 10.17/1.71 fof(f122,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_840,X0)=select(a_836,X0)|i1=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f117,f118])).
% 10.17/1.71 fof(f126,plain,(
% 10.17/1.71 i2=i0|e_843=select(a_836,i0)|i1=i0),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f89,f122])).
% 10.17/1.71 fof(f127,plain,(
% 10.17/1.71 i2=i5|e_841=select(a_836,i5)|i1=i5),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f88,f122])).
% 10.17/1.71 fof(f134,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_844,X0)=select(a_842,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f63,f57])).
% 10.17/1.71 fof(f135,plain,(
% 10.17/1.71 select(a_844,i5)=e_843),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f63,f55])).
% 10.17/1.71 fof(f136,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_844,X0)=select(a_840,X0)|i0=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f116,f134])).
% 10.17/1.71 fof(f138,plain,(
% 10.17/1.71 i5=i2|e_847=select(a_840,i2)|i0=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f91,f136])).
% 10.17/1.71 fof(f149,plain,(
% 10.17/1.71 select(a_840,i2)=e_837|i1=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f117,f112])).
% 10.17/1.71 fof(f152,plain,(
% 10.17/1.71 e_847=e_837|i1=i2|i5=i2|i0=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f138,f149])).
% 10.17/1.71 fof(f158,plain,(
% 10.17/1.71 select(a_844,i0)=e_841|i5=i0),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f134,f114])).
% 10.17/1.71 fof(f164,plain,(
% 10.17/1.71 e_845=e_843),
% 10.17/1.71 inference(backward_demodulation,[status(thm)],[f135,f90])).
% 10.17/1.71 fof(f167,plain,(
% 10.17/1.71 a_846=store(a_844,i2,e_843)),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f164,f64])).
% 10.17/1.71 fof(f168,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_846,X0)=select(a_844,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f167,f57])).
% 10.17/1.71 fof(f169,plain,(
% 10.17/1.71 select(a_846,i2)=e_843),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f167,f55])).
% 10.17/1.71 fof(f172,plain,(
% 10.17/1.71 a_848=store(a_846,i5,e_837)|i1=i2|i5=i2|i0=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f152,f65])).
% 10.17/1.71 fof(f173,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_848,X0)=select(a_846,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f65,f57])).
% 10.17/1.71 fof(f174,plain,(
% 10.17/1.71 select(a_848,i5)=e_847),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f65,f55])).
% 10.17/1.71 fof(f175,plain,(
% 10.17/1.71 i5=i2|select(a_848,i2)=e_843),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f169,f173])).
% 10.17/1.71 fof(f176,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_848,X0)=select(a_844,X0)|i2=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f168,f173])).
% 10.17/1.71 fof(f180,plain,(
% 10.17/1.71 i5=i1|e_849=select(a_844,i1)|i2=i1),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f92,f176])).
% 10.17/1.71 fof(f183,plain,(
% 10.17/1.71 i5=i1|e_849=select(a_840,i1)|i2=i1|i5=i1|i0=i1),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f136,f180])).
% 10.17/1.71 fof(f185,plain,(
% 10.17/1.71 i5=i1|e_849=e_839|i2=i1|i5=i1|i0=i1),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f113,f183])).
% 10.17/1.71 fof(f186,plain,(
% 10.17/1.71 i5=i1|e_849=e_839|i2=i1|i0=i1),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f185])).
% 10.17/1.71 fof(f190,plain,(
% 10.17/1.71 select(a_848,i5)=e_837|i1=i2|i5=i2|i0=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f172,f55])).
% 10.17/1.71 fof(f194,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_850,X0)=select(a_848,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f66,f57])).
% 10.17/1.71 fof(f201,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_851,X0)=select(a_850,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f67,f57])).
% 10.17/1.71 fof(f202,plain,(
% 10.17/1.71 select(a_851,i1)=e_849),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f67,f55])).
% 10.17/1.71 fof(f204,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_851,X0)=select(a_848,X0)|i1=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f194,f201])).
% 10.17/1.71 fof(f207,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_851,X0)=select(a_848,X0))),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f204])).
% 10.17/1.71 fof(f209,plain,(
% 10.17/1.71 i1=i5|select(a_851,i5)=e_837|i1=i2|i5=i2|i0=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f190,f207])).
% 10.17/1.71 fof(f210,plain,(
% 10.17/1.71 i1=i2|select(a_851,i2)=e_843|i5=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f175,f207])).
% 10.17/1.71 fof(f212,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_851,X0)=select(a_844,X0)|i5=X0|i2=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f176,f207])).
% 10.17/1.71 fof(f217,plain,(
% 10.17/1.71 i1=i5|e_854=e_837|i1=i2|i5=i2|i0=i2),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f94,f209])).
% 10.17/1.71 fof(f218,plain,(
% 10.17/1.71 i1=i2|e_852=e_843|i5=i2),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f93,f210])).
% 10.17/1.71 fof(f230,plain,(
% 10.17/1.71 select(a_851,i5)=e_847|i1=i5),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f207,f174])).
% 10.17/1.71 fof(f234,plain,(
% 10.17/1.71 e_854=e_847|i1=i5),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f94,f230])).
% 10.17/1.71 fof(f249,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_853,X0)=select(a_851,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f68,f57])).
% 10.17/1.71 fof(f250,plain,(
% 10.17/1.71 select(a_853,i5)=e_852),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f68,f55])).
% 10.17/1.71 fof(f260,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_855,X0)=select(a_853,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f69,f57])).
% 10.17/1.71 fof(f261,plain,(
% 10.17/1.71 select(a_855,i2)=e_854),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f69,f55])).
% 10.17/1.71 fof(f262,plain,(
% 10.17/1.71 i2=i5|select(a_855,i5)=e_852),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f250,f260])).
% 10.17/1.71 fof(f263,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_855,X0)=select(a_851,X0)|i5=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f249,f260])).
% 10.17/1.71 fof(f266,plain,(
% 10.17/1.71 i2=i5|e_858=e_852),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f96,f262])).
% 10.17/1.71 fof(f283,plain,(
% 10.17/1.71 e_856=e_854),
% 10.17/1.71 inference(backward_demodulation,[status(thm)],[f261,f95])).
% 10.17/1.71 fof(f288,plain,(
% 10.17/1.71 a_857=store(a_855,i5,e_854)),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f283,f70])).
% 10.17/1.71 fof(f289,plain,(
% 10.17/1.71 a_857=store(a_855,i5,e_847)|i1=i5),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f234,f288])).
% 10.17/1.71 fof(f291,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_857,X0)=select(a_855,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f288,f57])).
% 10.17/1.71 fof(f292,plain,(
% 10.17/1.71 select(a_857,i5)=e_854),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f288,f55])).
% 10.17/1.71 fof(f310,plain,(
% 10.17/1.71 a_859=store(a_857,i2,e_852)|i2=i5),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f266,f71])).
% 10.17/1.71 fof(f311,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_859,X0)=select(a_857,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f71,f57])).
% 10.17/1.71 fof(f312,plain,(
% 10.17/1.71 select(a_859,i2)=e_858),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f71,f55])).
% 10.17/1.71 fof(f313,plain,(
% 10.17/1.71 i2=i5|select(a_859,i5)=e_854),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f292,f311])).
% 10.17/1.71 fof(f314,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_859,X0)=select(a_855,X0)|i5=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f291,f311])).
% 10.17/1.71 fof(f317,plain,(
% 10.17/1.71 a_859=store(a_857,i2,e_843)|i2=i5|i1=i2|i5=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f218,f310])).
% 10.17/1.71 fof(f320,plain,(
% 10.17/1.71 a_859=store(a_857,i2,e_843)|i2=i5|i1=i2),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f317])).
% 10.17/1.71 fof(f323,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_855,i_881)|i5=i_881),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f106,f314])).
% 10.17/1.71 fof(f327,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_851,i_881)|i5=i_881|i2=i_881|i5=i_881),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f263,f323])).
% 10.17/1.71 fof(f329,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_851,i_881)|i5=i_881),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f327])).
% 10.17/1.71 fof(f332,plain,(
% 10.17/1.71 select(a_859,i2)=e_843|i2=i5|i1=i2),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f320,f55])).
% 10.17/1.71 fof(f333,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_844,i_881)|i5=i_881|i1=i_881|i5=i_881|i2=i_881),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f212,f329])).
% 10.17/1.71 fof(f335,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_844,i_881)|i5=i_881|i1=i_881),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f333])).
% 10.17/1.71 fof(f343,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_840,i_881)|i5=i_881|i1=i_881|i5=i_881|i0=i_881),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f136,f335])).
% 10.17/1.71 fof(f345,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_840,i_881)|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f343])).
% 10.17/1.71 fof(f347,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_836,i_881)|i5=i_881|i1=i_881|i0=i_881|i2=i_881|i1=i_881),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f122,f345])).
% 10.17/1.71 fof(f349,plain,(
% 10.17/1.71 i2=i_881|e_882=select(a_836,i_881)|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.71 inference(duplicate_literals_removal,[status(thm)],[f347])).
% 10.17/1.71 fof(f351,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_860,X0)=select(a_836,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f72,f57])).
% 10.17/1.71 fof(f352,plain,(
% 10.17/1.71 select(a_860,i1)=e_839),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f72,f55])).
% 10.17/1.71 fof(f353,plain,(
% 10.17/1.71 e_858=e_843|i2=i5|i1=i2),
% 10.17/1.71 inference(backward_demodulation,[status(thm)],[f312,f332])).
% 10.17/1.71 fof(f357,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_861,X0)=select(a_860,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f73,f57])).
% 10.17/1.71 fof(f358,plain,(
% 10.17/1.71 select(a_861,i2)=e_837),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f73,f55])).
% 10.17/1.71 fof(f359,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_863,X0)=select(a_861,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f74,f57])).
% 10.17/1.71 fof(f360,plain,(
% 10.17/1.71 select(a_863,i5)=e_862),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f74,f55])).
% 10.17/1.71 fof(f361,plain,(
% 10.17/1.71 ![X0]: (i0=X0|select(a_865,X0)=select(a_863,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f75,f57])).
% 10.17/1.71 fof(f362,plain,(
% 10.17/1.71 select(a_865,i0)=e_864),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f75,f55])).
% 10.17/1.71 fof(f363,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_867,X0)=select(a_865,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f76,f57])).
% 10.17/1.71 fof(f364,plain,(
% 10.17/1.71 select(a_867,i5)=e_866),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f76,f55])).
% 10.17/1.71 fof(f365,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_869,X0)=select(a_867,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f77,f57])).
% 10.17/1.71 fof(f366,plain,(
% 10.17/1.71 select(a_869,i2)=e_868),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f77,f55])).
% 10.17/1.71 fof(f367,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_871,X0)=select(a_869,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f78,f57])).
% 10.17/1.71 fof(f369,plain,(
% 10.17/1.71 ![X0]: (i1=X0|select(a_872,X0)=select(a_871,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f79,f57])).
% 10.17/1.71 fof(f370,plain,(
% 10.17/1.71 select(a_872,i1)=e_870),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f79,f55])).
% 10.17/1.71 fof(f371,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_874,X0)=select(a_872,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f80,f57])).
% 10.17/1.71 fof(f372,plain,(
% 10.17/1.71 select(a_874,i5)=e_873),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f80,f55])).
% 10.17/1.71 fof(f373,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_876,X0)=select(a_874,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f81,f57])).
% 10.17/1.71 fof(f374,plain,(
% 10.17/1.71 select(a_876,i2)=e_875),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f81,f55])).
% 10.17/1.71 fof(f375,plain,(
% 10.17/1.71 e_877=e_875),
% 10.17/1.71 inference(backward_demodulation,[status(thm)],[f374,f104])).
% 10.17/1.71 fof(f376,plain,(
% 10.17/1.71 a_878=store(a_876,i5,e_875)),
% 10.17/1.71 inference(forward_demodulation,[status(thm)],[f375,f82])).
% 10.17/1.71 fof(f377,plain,(
% 10.17/1.71 ![X0]: (i5=X0|select(a_878,X0)=select(a_876,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f376,f57])).
% 10.17/1.71 fof(f378,plain,(
% 10.17/1.71 select(a_878,i5)=e_875),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f376,f55])).
% 10.17/1.71 fof(f379,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_880,X0)=select(a_878,X0))),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f83,f57])).
% 10.17/1.71 fof(f380,plain,(
% 10.17/1.71 select(a_880,i2)=e_879),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f83,f55])).
% 10.17/1.71 fof(f388,plain,(
% 10.17/1.71 i2=i1|select(a_861,i1)=e_839),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f352,f357])).
% 10.17/1.71 fof(f389,plain,(
% 10.17/1.71 ![X0]: (i2=X0|select(a_861,X0)=select(a_836,X0)|i1=X0)),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f351,f357])).
% 10.17/1.71 fof(f394,plain,(
% 10.17/1.71 i0=i5|select(a_865,i5)=e_862),
% 10.17/1.71 inference(paramodulation,[status(thm)],[f360,f361])).
% 10.17/1.71 fof(f395,plain,(
% 10.17/1.71 ![X0]: (i0=X0|select(a_865,X0)=select(a_861,X0)|i5=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f359,f361])).
% 10.17/1.72 fof(f398,plain,(
% 10.17/1.72 i0=i5|e_868=e_862),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f100,f394])).
% 10.17/1.72 fof(f400,plain,(
% 10.17/1.72 a_869=store(a_867,i2,e_862)|i0=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f398,f77])).
% 10.17/1.72 fof(f403,plain,(
% 10.17/1.72 i2=i5|select(a_869,i5)=e_866),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f364,f365])).
% 10.17/1.72 fof(f404,plain,(
% 10.17/1.72 ![X0]: (i2=X0|select(a_869,X0)=select(a_865,X0)|i5=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f363,f365])).
% 10.17/1.72 fof(f410,plain,(
% 10.17/1.72 ![X0]: (i1=X0|select(a_872,X0)=select(a_869,X0)|i1=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f367,f369])).
% 10.17/1.72 fof(f413,plain,(
% 10.17/1.72 ![X0]: (i1=X0|select(a_872,X0)=select(a_869,X0))),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f410])).
% 10.17/1.72 fof(f417,plain,(
% 10.17/1.72 i2=i5|select(a_876,i5)=e_873),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f372,f373])).
% 10.17/1.72 fof(f418,plain,(
% 10.17/1.72 ![X0]: (i2=X0|select(a_876,X0)=select(a_872,X0)|i5=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f371,f373])).
% 10.17/1.72 fof(f421,plain,(
% 10.17/1.72 i2=i5|e_879=e_873),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f105,f417])).
% 10.17/1.72 fof(f423,plain,(
% 10.17/1.72 a_880=store(a_878,i2,e_873)|i2=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f421,f83])).
% 10.17/1.72 fof(f426,plain,(
% 10.17/1.72 i2=i5|select(a_880,i5)=e_875),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f378,f379])).
% 10.17/1.72 fof(f427,plain,(
% 10.17/1.72 ![X0]: (i2=X0|select(a_880,X0)=select(a_876,X0)|i5=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f377,f379])).
% 10.17/1.72 fof(f432,plain,(
% 10.17/1.72 i2=i5|e_864=select(a_836,i5)|i1=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f98,f389])).
% 10.17/1.72 fof(f433,plain,(
% 10.17/1.72 i2=i0|e_862=select(a_836,i0)|i1=i0),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f97,f389])).
% 10.17/1.72 fof(f440,plain,(
% 10.17/1.72 i0=i2|e_866=select(a_861,i2)|i5=i2),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f99,f395])).
% 10.17/1.72 fof(f444,plain,(
% 10.17/1.72 i0=i2|e_866=e_837|i5=i2),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f358,f440])).
% 10.17/1.72 fof(f447,plain,(
% 10.17/1.72 i1=i5|select(a_872,i5)=e_866|i2=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f403,f413])).
% 10.17/1.72 fof(f448,plain,(
% 10.17/1.72 i1=i2|select(a_872,i2)=e_868),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f366,f413])).
% 10.17/1.72 fof(f453,plain,(
% 10.17/1.72 i1=i5|e_875=e_866|i2=i5),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f103,f447])).
% 10.17/1.72 fof(f454,plain,(
% 10.17/1.72 i1=i2|e_873=e_868),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f102,f448])).
% 10.17/1.72 fof(f457,plain,(
% 10.17/1.72 a_874=store(a_872,i5,e_868)|i1=i2),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f454,f80])).
% 10.17/1.72 fof(f458,plain,(
% 10.17/1.72 a_878=store(a_876,i5,e_866)|i1=i5|i2=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f453,f376])).
% 10.17/1.72 fof(f459,plain,(
% 10.17/1.72 a_876=store(a_874,i2,e_866)|i1=i5|i2=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f453,f81])).
% 10.17/1.72 fof(f463,plain,(
% 10.17/1.72 a_880=store(a_878,i2,e_868)|i2=i5|i1=i2),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f454,f423])).
% 10.17/1.72 fof(f467,plain,(
% 10.17/1.72 a_874=store(a_872,i5,e_862)|i1=i2|i0=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f398,f457])).
% 10.17/1.72 fof(f473,plain,(
% 10.17/1.72 i2=i1|e_870=select(a_865,i1)|i5=i1),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f101,f404])).
% 10.17/1.72 fof(f474,plain,(
% 10.17/1.72 ![X0]: (i2=X0|select(a_872,X0)=select(a_865,X0)|i5=X0|i1=X0)),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f413,f404])).
% 10.17/1.72 fof(f485,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_876,i_881)|i5=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f107,f427])).
% 10.17/1.72 fof(f489,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_872,i_881)|i5=i_881|i2=i_881|i5=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f418,f485])).
% 10.17/1.72 fof(f491,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_872,i_881)|i5=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f489])).
% 10.17/1.72 fof(f493,plain,(
% 10.17/1.72 i2=i5|e_864=e_841|i1=i5|i2=i5|i1=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f127,f432])).
% 10.17/1.72 fof(f495,plain,(
% 10.17/1.72 i2=i5|e_864=e_841|i1=i5),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f493])).
% 10.17/1.72 fof(f497,plain,(
% 10.17/1.72 a_865=store(a_863,i0,e_841)|i2=i5|i1=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f495,f75])).
% 10.17/1.72 fof(f498,plain,(
% 10.17/1.72 i2=i0|e_862=e_843|i1=i0|i2=i0|i1=i0),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f126,f433])).
% 10.17/1.72 fof(f500,plain,(
% 10.17/1.72 i2=i0|e_862=e_843|i1=i0),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f498])).
% 10.17/1.72 fof(f502,plain,(
% 10.17/1.72 a_869=store(a_867,i2,e_843)|i0=i5|i2=i0|i1=i0),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f500,f400])).
% 10.17/1.72 fof(f504,plain,(
% 10.17/1.72 i2=i1|e_870=select(a_861,i1)|i5=i1|i0=i1|i5=i1),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f395,f473])).
% 10.17/1.72 fof(f506,plain,(
% 10.17/1.72 i2=i1|e_870=select(a_861,i1)|i5=i1|i0=i1),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f504])).
% 10.17/1.72 fof(f508,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_865,i_881)|i5=i_881|i1=i_881|i2=i_881|i5=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f491,f474])).
% 10.17/1.72 fof(f516,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_865,i_881)|i5=i_881|i1=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f508])).
% 10.17/1.72 fof(f518,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_861,i_881)|i5=i_881|i1=i_881|i0=i_881|i5=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f395,f516])).
% 10.17/1.72 fof(f520,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_861,i_881)|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f518])).
% 10.17/1.72 fof(f522,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_836,i_881)|i5=i_881|i1=i_881|i0=i_881|i2=i_881|i1=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f389,f520])).
% 10.17/1.72 fof(f524,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_836,i_881)|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f522])).
% 10.17/1.72 fof(f526,plain,(
% 10.17/1.72 i2=i_881|e_883=e_882|i5=i_881|i1=i_881|i0=i_881|i2=i_881|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f349,f524])).
% 10.17/1.72 fof(f528,plain,(
% 10.17/1.72 i2=i_881|e_883=e_882|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f526])).
% 10.17/1.72 fof(f529,plain,(
% 10.17/1.72 i2=i_881|i5=i_881|i1=i_881|i0=i_881),
% 10.17/1.72 inference(forward_subsumption_resolution,[status(thm)],[f528,f109])).
% 10.17/1.72 fof(f532,plain,(
% 10.17/1.72 i2=i_881|e_883=select(a_865,i0)|i5=i_881|i1=i_881|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f529,f516])).
% 10.17/1.72 fof(f535,plain,(
% 10.17/1.72 i2=i_881|e_882=select(a_844,i0)|i5=i_881|i1=i_881|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f529,f335])).
% 10.17/1.72 fof(f541,plain,(
% 10.17/1.72 i2=i_881|i1=i_881|~i0=i5|i_881=i5),
% 10.17/1.72 inference(equality_factoring,[status(thm)],[f529])).
% 10.17/1.72 fof(f543,plain,(
% 10.17/1.72 i2=i_881|e_883=e_864|i5=i_881|i1=i_881|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.72 inference(forward_demodulation,[status(thm)],[f362,f532])).
% 10.17/1.72 fof(f544,plain,(
% 10.17/1.72 i2=i_881|e_883=e_864|i5=i_881|i1=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f543])).
% 10.17/1.72 fof(f547,plain,(
% 10.17/1.72 i2=i_881|e_882=select(a_844,i0)|i5=i_881|i1=i_881),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f535])).
% 10.17/1.72 fof(f550,plain,(
% 10.17/1.72 ~e_882=e_864|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f544,f109])).
% 10.17/1.72 fof(f554,plain,(
% 10.17/1.72 a_878=store(a_876,i5,e_837)|i1=i5|i2=i5|i0=i2|i5=i2),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f444,f458])).
% 10.17/1.72 fof(f557,plain,(
% 10.17/1.72 a_878=store(a_876,i5,e_837)|i1=i5|i2=i5|i0=i2),
% 10.17/1.72 inference(duplicate_literals_removal,[status(thm)],[f554])).
% 10.17/1.72 fof(f564,plain,(
% 10.17/1.72 a_880=store(a_878,i2,e_862)|i2=i5|i1=i2|i0=i5),
% 10.17/1.72 inference(paramodulation,[status(thm)],[f398,f463])).
% 10.17/1.72 fof(f573,plain,(
% 10.17/1.72 a_874=store(a_872,i5,e_843)|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f500,f467])).
% 10.17/1.73 fof(f575,plain,(
% 10.17/1.73 select(a_874,i5)=e_862|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f467,f55])).
% 10.17/1.73 fof(f576,plain,(
% 10.17/1.73 e_873=e_862|i1=i2|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f372,f575])).
% 10.17/1.73 fof(f589,plain,(
% 10.17/1.73 i2=i1|e_870=e_839|i5=i1|i0=i1|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f388,f506])).
% 10.17/1.73 fof(f593,plain,(
% 10.17/1.73 i2=i1|e_870=e_839|i5=i1|i0=i1),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f589])).
% 10.17/1.73 fof(f603,plain,(
% 10.17/1.73 i2=i_881|e_882=e_841|i5=i_881|i1=i_881|i5=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f158,f547])).
% 10.17/1.73 fof(f607,plain,(
% 10.17/1.73 i2=i_881|e_882=e_841|i5=i_881|i1=i_881),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f603,f541])).
% 10.17/1.73 fof(f609,plain,(
% 10.17/1.73 ~e_841=e_864|i2=i_881|i5=i_881|i1=i_881|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f607,f550])).
% 10.17/1.73 fof(f610,plain,(
% 10.17/1.73 ~e_841=e_864|i2=i_881|i5=i_881|i1=i_881),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f609])).
% 10.17/1.73 fof(f611,plain,(
% 10.17/1.73 i2=i_881|i5=i_881|i1=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(resolution,[status(thm)],[f610,f495])).
% 10.17/1.73 fof(f625,plain,(
% 10.17/1.73 i2=i_881|e_883=select(a_872,i1)|i5=i_881|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f611,f491])).
% 10.17/1.73 fof(f628,plain,(
% 10.17/1.73 i2=i_881|e_882=select(a_851,i1)|i5=i_881|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f611,f329])).
% 10.17/1.73 fof(f632,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5|~i1=i2|i_881=i2),
% 10.17/1.73 inference(equality_factoring,[status(thm)],[f611])).
% 10.17/1.73 fof(f637,plain,(
% 10.17/1.73 i2=i_881|e_883=e_870|i5=i_881|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f370,f625])).
% 10.17/1.73 fof(f638,plain,(
% 10.17/1.73 i2=i_881|e_883=e_870|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f637])).
% 10.17/1.73 fof(f641,plain,(
% 10.17/1.73 i2=i_881|e_882=e_849|i5=i_881|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f202,f628])).
% 10.17/1.73 fof(f642,plain,(
% 10.17/1.73 i2=i_881|e_882=e_849|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f641])).
% 10.17/1.73 fof(f646,plain,(
% 10.17/1.73 ~e_882=e_870|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f638,f109])).
% 10.17/1.73 fof(f655,plain,(
% 10.17/1.73 ~e_849=e_870|i2=i_881|i5=i_881|i2=i5|i1=i5|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f642,f646])).
% 10.17/1.73 fof(f657,plain,(
% 10.17/1.73 ~e_849=e_870|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f655])).
% 10.17/1.73 fof(f659,plain,(
% 10.17/1.73 ~e_849=e_839|i2=i_881|i5=i_881|i2=i5|i1=i5|i2=i1|i5=i1|i0=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f593,f657])).
% 10.17/1.73 fof(f660,plain,(
% 10.17/1.73 ~e_849=e_839|i2=i_881|i5=i_881|i2=i5|i1=i5|i2=i1|i0=i1),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f659])).
% 10.17/1.73 fof(f661,plain,(
% 10.17/1.73 i2=i_881|i5=i_881|i2=i5|i1=i5|i2=i1|i0=i1),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f660,f186])).
% 10.17/1.73 fof(f663,plain,(
% 10.17/1.73 select(a_869,i2)=e_843|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f502,f55])).
% 10.17/1.73 fof(f664,plain,(
% 10.17/1.73 e_868=e_843|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f366,f663])).
% 10.17/1.73 fof(f673,plain,(
% 10.17/1.73 select(a_878,i5)=e_837|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f557,f55])).
% 10.17/1.73 fof(f674,plain,(
% 10.17/1.73 e_875=e_837|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f378,f673])).
% 10.17/1.73 fof(f684,plain,(
% 10.17/1.73 a_880=store(a_878,i2,e_843)|i2=i5|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f500,f564])).
% 10.17/1.73 fof(f686,plain,(
% 10.17/1.73 select(a_880,i2)=e_862|i2=i5|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f564,f55])).
% 10.17/1.73 fof(f687,plain,(
% 10.17/1.73 e_879=e_862|i2=i5|i1=i2|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f686])).
% 10.17/1.73 fof(f704,plain,(
% 10.17/1.73 select(a_874,i5)=e_843|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f573,f55])).
% 10.17/1.73 fof(f705,plain,(
% 10.17/1.73 e_873=e_843|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f372,f704])).
% 10.17/1.73 fof(f707,plain,(
% 10.17/1.73 select(a_880,i2)=e_843|i2=i5|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f684,f55])).
% 10.17/1.73 fof(f708,plain,(
% 10.17/1.73 e_879=e_843|i2=i5|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f707])).
% 10.17/1.73 fof(f752,plain,(
% 10.17/1.73 i2=i_881|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f661,f632])).
% 10.17/1.73 fof(f763,plain,(
% 10.17/1.73 e_883=select(a_880,i2)|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f752,f107])).
% 10.17/1.73 fof(f764,plain,(
% 10.17/1.73 e_882=select(a_859,i2)|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f752,f106])).
% 10.17/1.73 fof(f782,plain,(
% 10.17/1.73 e_883=e_879|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f763])).
% 10.17/1.73 fof(f783,plain,(
% 10.17/1.73 e_882=e_858|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f764])).
% 10.17/1.73 fof(f788,plain,(
% 10.17/1.73 ~e_882=e_879|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f782,f109])).
% 10.17/1.73 fof(f805,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i_881|i2=i5|i1=i5|i0=i1|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f783,f788])).
% 10.17/1.73 fof(f808,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i_881|i2=i5|i1=i5|i0=i1),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f805])).
% 10.17/1.73 fof(f811,plain,(
% 10.17/1.73 ~e_858=e_843|i5=i_881|i2=i5|i1=i5|i0=i1|i2=i5|i1=i2|i0=i5|i2=i0|i1=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f708,f808])).
% 10.17/1.73 fof(f812,plain,(
% 10.17/1.73 ~e_858=e_862|i5=i_881|i2=i5|i1=i5|i0=i1|i2=i5|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f687,f808])).
% 10.17/1.73 fof(f815,plain,(
% 10.17/1.73 ~e_858=e_843|i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f811])).
% 10.17/1.73 fof(f816,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f815,f353])).
% 10.17/1.73 fof(f817,plain,(
% 10.17/1.73 ~e_858=e_862|i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f812])).
% 10.17/1.73 fof(f832,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f816,f107])).
% 10.17/1.73 fof(f833,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f816,f106])).
% 10.17/1.73 fof(f855,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f832])).
% 10.17/1.73 fof(f859,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f855])).
% 10.17/1.73 fof(f867,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f859,f109])).
% 10.17/1.73 fof(f872,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f833])).
% 10.17/1.73 fof(f876,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f872])).
% 10.17/1.73 fof(f886,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f876,f867])).
% 10.17/1.73 fof(f895,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f886])).
% 10.17/1.73 fof(f900,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f674,f895])).
% 10.17/1.73 fof(f902,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f900])).
% 10.17/1.73 fof(f903,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f902,f217])).
% 10.17/1.73 fof(f918,plain,(
% 10.17/1.73 select(a_865,i1)=e_864|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f903,f362])).
% 10.17/1.73 fof(f920,plain,(
% 10.17/1.73 select(a_844,i1)=e_841|i5=i0|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f903,f158])).
% 10.17/1.73 fof(f924,plain,(
% 10.17/1.73 e_862=select(a_861,i1)|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f903,f97])).
% 10.17/1.73 fof(f925,plain,(
% 10.17/1.73 e_843=select(a_840,i1)|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f903,f89])).
% 10.17/1.73 fof(f934,plain,(
% 10.17/1.73 select(a_844,i1)=e_841|i5=i0|i2=i5|i1=i5|i1=i2|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f920])).
% 10.17/1.73 fof(f937,plain,(
% 10.17/1.73 e_843=e_839|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f113,f925])).
% 10.17/1.73 fof(f942,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_839)|i2=i5|i1=i2|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f937,f320])).
% 10.17/1.73 fof(f950,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_839)|i2=i5|i1=i2|i1=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f942])).
% 10.17/1.73 fof(f952,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0|i2=i1|i5=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f473,f918])).
% 10.17/1.73 fof(f956,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f952])).
% 10.17/1.73 fof(f960,plain,(
% 10.17/1.73 e_870=e_841|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f495,f956])).
% 10.17/1.73 fof(f964,plain,(
% 10.17/1.73 e_870=e_841|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f960])).
% 10.17/1.73 fof(f979,plain,(
% 10.17/1.73 e_849=e_841|i5=i0|i2=i5|i1=i5|i1=i2|i2=i0|i5=i1|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f180,f934])).
% 10.17/1.73 fof(f983,plain,(
% 10.17/1.73 e_849=e_841|i5=i0|i2=i5|i1=i5|i1=i2|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f979])).
% 10.17/1.73 fof(f989,plain,(
% 10.17/1.73 e_849=e_870|i5=i0|i2=i5|i1=i5|i1=i2|i2=i0|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f964,f983])).
% 10.17/1.73 fof(f994,plain,(
% 10.17/1.73 e_849=e_870|i5=i0|i2=i5|i1=i5|i1=i2|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f989])).
% 10.17/1.73 fof(f998,plain,(
% 10.17/1.73 i5=i0|i2=i5|i1=i5|i1=i2|i2=i0|i2=i_881|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(resolution,[status(thm)],[f994,f657])).
% 10.17/1.73 fof(f1004,plain,(
% 10.17/1.73 i5=i0|i2=i5|i1=i5|i1=i2|i2=i0|i2=i_881|i5=i_881),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f998])).
% 10.17/1.73 fof(f1005,plain,(
% 10.17/1.73 i5=i0|i2=i5|i1=i5|i2=i0|i2=i_881|i5=i_881),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1004,f632])).
% 10.17/1.73 fof(f1023,plain,(
% 10.17/1.73 e_883=select(a_880,i2)|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1005,f107])).
% 10.17/1.73 fof(f1024,plain,(
% 10.17/1.73 e_882=select(a_859,i2)|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1005,f106])).
% 10.17/1.73 fof(f1042,plain,(
% 10.17/1.73 e_883=e_879|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f1023])).
% 10.17/1.73 fof(f1043,plain,(
% 10.17/1.73 e_882=e_858|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f1024])).
% 10.17/1.73 fof(f1050,plain,(
% 10.17/1.73 ~e_882=e_879|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1042,f109])).
% 10.17/1.73 fof(f1071,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1043,f1050])).
% 10.17/1.73 fof(f1075,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1071])).
% 10.17/1.73 fof(f1080,plain,(
% 10.17/1.73 ~e_858=e_862|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i2=i5|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f687,f1075])).
% 10.17/1.73 fof(f1084,plain,(
% 10.17/1.73 ~e_858=e_862|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1080])).
% 10.17/1.73 fof(f1101,plain,(
% 10.17/1.73 e_862=e_839|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f388,f924])).
% 10.17/1.73 fof(f1107,plain,(
% 10.17/1.73 e_862=e_839|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1101])).
% 10.17/1.73 fof(f1142,plain,(
% 10.17/1.73 select(a_859,i2)=e_839|i2=i5|i1=i2|i1=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f950,f55])).
% 10.17/1.73 fof(f1143,plain,(
% 10.17/1.73 e_858=e_839|i2=i5|i1=i2|i1=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f1142])).
% 10.17/1.73 fof(f1166,plain,(
% 10.17/1.73 ~e_858=e_839|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i1=i2|i2=i5|i1=i5|i1=i2|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1107,f1084])).
% 10.17/1.73 fof(f1168,plain,(
% 10.17/1.73 ~e_858=e_839|i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1166])).
% 10.17/1.73 fof(f1169,plain,(
% 10.17/1.73 i5=i0|i2=i5|i1=i5|i2=i0|i5=i_881|i1=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1168,f1143])).
% 10.17/1.73 fof(f1185,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1169,f107])).
% 10.17/1.73 fof(f1186,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1169,f106])).
% 10.17/1.73 fof(f1201,plain,(
% 10.17/1.73 e_883=e_875|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f1185])).
% 10.17/1.73 fof(f1205,plain,(
% 10.17/1.73 e_883=e_875|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1201])).
% 10.17/1.73 fof(f1215,plain,(
% 10.17/1.73 ~e_882=e_875|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1205,f109])).
% 10.17/1.73 fof(f1229,plain,(
% 10.17/1.73 e_882=e_854|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f1186])).
% 10.17/1.73 fof(f1233,plain,(
% 10.17/1.73 e_882=e_854|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1229])).
% 10.17/1.73 fof(f1239,plain,(
% 10.17/1.73 ~e_854=e_875|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1233,f1215])).
% 10.17/1.73 fof(f1251,plain,(
% 10.17/1.73 ~e_854=e_875|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1239])).
% 10.17/1.73 fof(f1258,plain,(
% 10.17/1.73 ~e_854=e_837|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f674,f1251])).
% 10.17/1.73 fof(f1260,plain,(
% 10.17/1.73 ~e_854=e_837|i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1258])).
% 10.17/1.73 fof(f1261,plain,(
% 10.17/1.73 i5=i0|i2=i5|i1=i5|i2=i0|i1=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1260,f217])).
% 10.17/1.73 fof(f1271,plain,(
% 10.17/1.73 a_865=store(a_863,i2,e_841)|i2=i5|i1=i5|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1261,f497])).
% 10.17/1.73 fof(f1278,plain,(
% 10.17/1.73 select(a_844,i2)=e_841|i5=i0|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1261,f158])).
% 10.17/1.73 fof(f1282,plain,(
% 10.17/1.73 e_862=select(a_861,i2)|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1261,f97])).
% 10.17/1.73 fof(f1283,plain,(
% 10.17/1.73 e_843=select(a_840,i2)|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1261,f89])).
% 10.17/1.73 fof(f1292,plain,(
% 10.17/1.73 a_865=store(a_863,i2,e_841)|i2=i5|i1=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1271])).
% 10.17/1.73 fof(f1296,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f91,f1278])).
% 10.17/1.73 fof(f1297,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1296])).
% 10.17/1.73 fof(f1299,plain,(
% 10.17/1.73 e_862=e_837|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f358,f1282])).
% 10.17/1.73 fof(f1310,plain,(
% 10.17/1.73 a_857=store(a_855,i5,e_841)|i1=i5|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1297,f289])).
% 10.17/1.73 fof(f1315,plain,(
% 10.17/1.73 a_857=store(a_855,i5,e_841)|i1=i5|i5=i0|i2=i5|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1310])).
% 10.17/1.73 fof(f1319,plain,(
% 10.17/1.73 ~e_858=e_837|i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1299,f817])).
% 10.17/1.73 fof(f1325,plain,(
% 10.17/1.73 ~e_858=e_837|i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1319])).
% 10.17/1.73 fof(f1337,plain,(
% 10.17/1.73 e_843=e_837|i5=i0|i2=i5|i1=i5|i1=i2|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f149,f1283])).
% 10.17/1.73 fof(f1343,plain,(
% 10.17/1.73 e_843=e_837|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1337])).
% 10.17/1.73 fof(f1351,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_837)|i2=i5|i1=i2|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1343,f320])).
% 10.17/1.73 fof(f1358,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_837)|i2=i5|i1=i2|i5=i0|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1351])).
% 10.17/1.73 fof(f1361,plain,(
% 10.17/1.73 select(a_865,i2)=e_841|i2=i5|i1=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1292,f55])).
% 10.17/1.73 fof(f1362,plain,(
% 10.17/1.73 e_866=e_841|i2=i5|i1=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f99,f1361])).
% 10.17/1.73 fof(f1366,plain,(
% 10.17/1.73 a_876=store(a_874,i2,e_841)|i1=i5|i2=i5|i2=i5|i1=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1362,f459])).
% 10.17/1.73 fof(f1373,plain,(
% 10.17/1.73 a_876=store(a_874,i2,e_841)|i1=i5|i2=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1366])).
% 10.17/1.73 fof(f1409,plain,(
% 10.17/1.73 select(a_857,i5)=e_841|i1=i5|i5=i0|i2=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1315,f55])).
% 10.17/1.73 fof(f1410,plain,(
% 10.17/1.73 e_854=e_841|i1=i5|i5=i0|i2=i5|i1=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f292,f1409])).
% 10.17/1.73 fof(f1495,plain,(
% 10.17/1.73 select(a_859,i2)=e_837|i2=i5|i1=i2|i5=i0|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1358,f55])).
% 10.17/1.73 fof(f1496,plain,(
% 10.17/1.73 e_858=e_837|i2=i5|i1=i2|i5=i0|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f1495])).
% 10.17/1.73 fof(f1523,plain,(
% 10.17/1.73 select(a_876,i2)=e_841|i1=i5|i2=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1373,f55])).
% 10.17/1.73 fof(f1524,plain,(
% 10.17/1.73 e_875=e_841|i1=i5|i2=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f374,f1523])).
% 10.17/1.73 fof(f1545,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1325,f1496])).
% 10.17/1.73 fof(f1560,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1545,f107])).
% 10.17/1.73 fof(f1561,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1545,f106])).
% 10.17/1.73 fof(f1576,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f1560])).
% 10.17/1.73 fof(f1580,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1576])).
% 10.17/1.73 fof(f1590,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1580,f109])).
% 10.17/1.73 fof(f1604,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f1561])).
% 10.17/1.73 fof(f1608,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1604])).
% 10.17/1.73 fof(f1614,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1608,f1590])).
% 10.17/1.73 fof(f1626,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1614])).
% 10.17/1.73 fof(f1633,plain,(
% 10.17/1.73 ~e_854=e_841|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5|i1=i5|i2=i5|i5=i0|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1524,f1626])).
% 10.17/1.73 fof(f1637,plain,(
% 10.17/1.73 ~e_854=e_841|i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1633])).
% 10.17/1.73 fof(f1638,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i1|i1=i2|i0=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1637,f1410])).
% 10.17/1.73 fof(f1643,plain,(
% 10.17/1.73 i2=i5|i1=i5|i2=i1|i1=i2|i0=i5|i5=i0|i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1261,f1638])).
% 10.17/1.73 fof(f1666,plain,(
% 10.17/1.73 i2=i5|i1=i5|i2=i1|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1643])).
% 10.17/1.73 fof(f1684,plain,(
% 10.17/1.73 a_865=store(a_863,i5,e_841)|i2=i5|i1=i5|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1666,f497])).
% 10.17/1.73 fof(f1696,plain,(
% 10.17/1.73 e_843=select(a_840,i5)|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1666,f89])).
% 10.17/1.73 fof(f1702,plain,(
% 10.17/1.73 a_865=store(a_863,i5,e_841)|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1684])).
% 10.17/1.73 fof(f1707,plain,(
% 10.17/1.73 e_843=e_841|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f88,f1696])).
% 10.17/1.73 fof(f1729,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_841)|i2=i5|i1=i2|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1707,f320])).
% 10.17/1.73 fof(f1735,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_841)|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1729])).
% 10.17/1.73 fof(f1750,plain,(
% 10.17/1.73 select(a_865,i5)=e_841|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1702,f55])).
% 10.17/1.73 fof(f1751,plain,(
% 10.17/1.73 e_868=e_841|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f100,f1750])).
% 10.17/1.73 fof(f1758,plain,(
% 10.17/1.73 a_880=store(a_878,i2,e_841)|i2=i5|i1=i2|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1751,f463])).
% 10.17/1.73 fof(f1765,plain,(
% 10.17/1.73 a_880=store(a_878,i2,e_841)|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1758])).
% 10.17/1.73 fof(f1846,plain,(
% 10.17/1.73 select(a_859,i2)=e_841|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1735,f55])).
% 10.17/1.73 fof(f1847,plain,(
% 10.17/1.73 e_858=e_841|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f1846])).
% 10.17/1.73 fof(f1877,plain,(
% 10.17/1.73 select(a_880,i2)=e_841|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1765,f55])).
% 10.17/1.73 fof(f1878,plain,(
% 10.17/1.73 e_879=e_841|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f1877])).
% 10.17/1.73 fof(f1886,plain,(
% 10.17/1.73 ~e_858=e_841|i5=i_881|i2=i5|i1=i5|i0=i1|i2=i5|i1=i2|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1878,f808])).
% 10.17/1.73 fof(f1899,plain,(
% 10.17/1.73 ~e_858=e_841|i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f1886])).
% 10.17/1.73 fof(f1900,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f1899,f1847])).
% 10.17/1.73 fof(f1943,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1900,f107])).
% 10.17/1.73 fof(f1944,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1900,f106])).
% 10.17/1.73 fof(f2062,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f1943])).
% 10.17/1.73 fof(f2066,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2062])).
% 10.17/1.73 fof(f2076,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2066,f109])).
% 10.17/1.73 fof(f2090,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f1944])).
% 10.17/1.73 fof(f2094,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2090])).
% 10.17/1.73 fof(f2100,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2094,f2076])).
% 10.17/1.73 fof(f2112,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i1|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2100])).
% 10.17/1.73 fof(f2119,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i1|i1=i2|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f674,f2112])).
% 10.17/1.73 fof(f2121,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i1|i1=i2|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2119])).
% 10.17/1.73 fof(f2122,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i1|i1=i2|i0=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f2121,f217])).
% 10.17/1.73 fof(f2125,plain,(
% 10.17/1.73 i2=i5|i1=i5|i5=i1|i1=i2|i0=i2|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1666,f2122])).
% 10.17/1.73 fof(f2149,plain,(
% 10.17/1.73 i2=i5|i1=i5|i1=i2|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2125])).
% 10.17/1.73 fof(f2162,plain,(
% 10.17/1.73 i2=i5|i1=i5|i1=i2|i5=i2|i2=i5|i1=i5|i2=i1),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f1666,f2149])).
% 10.17/1.73 fof(f2185,plain,(
% 10.17/1.73 i2=i5|i1=i5|i1=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2162])).
% 10.17/1.73 fof(f2202,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5|i_881=i2),
% 10.17/1.73 inference(backward_subsumption_resolution,[status(thm)],[f632,f2185])).
% 10.17/1.73 fof(f2212,plain,(
% 10.17/1.73 select(a_872,i2)=e_870|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f370])).
% 10.17/1.73 fof(f2217,plain,(
% 10.17/1.73 a_860=store(a_836,i2,e_839)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f72])).
% 10.17/1.73 fof(f2218,plain,(
% 10.17/1.73 select(a_851,i2)=e_849|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f202])).
% 10.17/1.73 fof(f2226,plain,(
% 10.17/1.73 a_840=store(a_838,i2,e_839)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f61])).
% 10.17/1.73 fof(f2227,plain,(
% 10.17/1.73 e_870=select(a_869,i2)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f101])).
% 10.17/1.73 fof(f2228,plain,(
% 10.17/1.73 e_849=select(a_848,i2)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f92])).
% 10.17/1.73 fof(f2229,plain,(
% 10.17/1.73 e_837=select(a_836,i2)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2185,f86])).
% 10.17/1.73 fof(f2246,plain,(
% 10.17/1.73 e_873=e_870|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f102,f2212])).
% 10.17/1.73 fof(f2247,plain,(
% 10.17/1.73 e_852=e_849|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f93,f2218])).
% 10.17/1.73 fof(f2252,plain,(
% 10.17/1.73 e_870=e_868|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f366,f2227])).
% 10.17/1.73 fof(f2253,plain,(
% 10.17/1.73 e_837=e_839|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f87,f2229])).
% 10.17/1.73 fof(f2262,plain,(
% 10.17/1.73 e_883=select(a_880,i2)|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2202,f107])).
% 10.17/1.73 fof(f2263,plain,(
% 10.17/1.73 e_882=select(a_859,i2)|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2202,f106])).
% 10.17/1.73 fof(f2279,plain,(
% 10.17/1.73 e_883=e_879|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f2262])).
% 10.17/1.73 fof(f2280,plain,(
% 10.17/1.73 e_882=e_858|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f2263])).
% 10.17/1.73 fof(f2283,plain,(
% 10.17/1.73 ~e_882=e_879|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2279,f109])).
% 10.17/1.73 fof(f2296,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i_881|i2=i5|i1=i5|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2280,f2283])).
% 10.17/1.73 fof(f2298,plain,(
% 10.17/1.73 ~e_858=e_879|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2296])).
% 10.17/1.73 fof(f2303,plain,(
% 10.17/1.73 ~e_858=e_873|i5=i_881|i2=i5|i1=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f421,f2298])).
% 10.17/1.73 fof(f2307,plain,(
% 10.17/1.73 ~e_858=e_873|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2303])).
% 10.17/1.73 fof(f2314,plain,(
% 10.17/1.73 ~e_858=e_870|i5=i_881|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2246,f2307])).
% 10.17/1.73 fof(f2320,plain,(
% 10.17/1.73 ~e_858=e_870|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2314])).
% 10.17/1.73 fof(f2330,plain,(
% 10.17/1.73 e_870=e_862|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f398,f2252])).
% 10.17/1.73 fof(f2373,plain,(
% 10.17/1.73 e_849=e_843|i2=i5|i1=i5|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f175,f2228])).
% 10.17/1.73 fof(f2379,plain,(
% 10.17/1.73 e_849=e_843|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2373])).
% 10.17/1.73 fof(f2395,plain,(
% 10.17/1.73 ~e_852=e_870|i5=i_881|i2=i5|i1=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f266,f2320])).
% 10.17/1.73 fof(f2397,plain,(
% 10.17/1.73 ~e_852=e_870|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2395])).
% 10.17/1.73 fof(f2416,plain,(
% 10.17/1.73 ~e_849=e_870|i5=i_881|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2247,f2397])).
% 10.17/1.73 fof(f2418,plain,(
% 10.17/1.73 ~e_849=e_870|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2416])).
% 10.17/1.73 fof(f2431,plain,(
% 10.17/1.73 a_860=store(a_836,i2,e_837)|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2253,f2217])).
% 10.17/1.73 fof(f2434,plain,(
% 10.17/1.73 a_860=a_838|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f60,f2431])).
% 10.17/1.73 fof(f2435,plain,(
% 10.17/1.73 a_860=a_838|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2434])).
% 10.17/1.73 fof(f2439,plain,(
% 10.17/1.73 a_861=store(a_838,i2,e_837)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2435,f73])).
% 10.17/1.73 fof(f2461,plain,(
% 10.17/1.73 a_840=store(a_838,i2,e_837)|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2253,f2226])).
% 10.17/1.73 fof(f2464,plain,(
% 10.17/1.73 a_840=store(a_838,i2,e_837)|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2461])).
% 10.17/1.73 fof(f2543,plain,(
% 10.17/1.73 a_840=a_861|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2439,f2464])).
% 10.17/1.73 fof(f2546,plain,(
% 10.17/1.73 select(a_840,i2)=e_837|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2464,f55])).
% 10.17/1.73 fof(f2547,plain,(
% 10.17/1.73 a_840=a_861|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2543])).
% 10.17/1.73 fof(f2556,plain,(
% 10.17/1.73 e_862=select(a_840,i0)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2547,f97])).
% 10.17/1.73 fof(f2560,plain,(
% 10.17/1.73 e_862=e_843|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f89,f2556])).
% 10.17/1.73 fof(f2561,plain,(
% 10.17/1.73 e_870=e_843|i2=i5|i1=i5|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2330,f2560])).
% 10.17/1.73 fof(f2568,plain,(
% 10.17/1.73 a_863=store(a_861,i5,e_843)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2560,f74])).
% 10.17/1.73 fof(f2569,plain,(
% 10.17/1.73 e_870=e_843|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2561])).
% 10.17/1.73 fof(f2574,plain,(
% 10.17/1.73 e_847=e_837|i2=i5|i1=i5|i5=i2|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f138,f2546])).
% 10.17/1.73 fof(f2581,plain,(
% 10.17/1.73 e_847=e_837|i2=i5|i1=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2574])).
% 10.17/1.73 fof(f2584,plain,(
% 10.17/1.73 e_870=e_849|i2=i5|i1=i5|i0=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2379,f2569])).
% 10.17/1.73 fof(f2594,plain,(
% 10.17/1.73 e_870=e_849|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2584])).
% 10.17/1.73 fof(f2612,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i5|i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(resolution,[status(thm)],[f2594,f2418])).
% 10.17/1.73 fof(f2623,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i5|i5=i_881),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2612])).
% 10.17/1.73 fof(f2643,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2623,f107])).
% 10.17/1.73 fof(f2644,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2623,f106])).
% 10.17/1.73 fof(f2665,plain,(
% 10.17/1.73 a_863=store(a_861,i5,e_849)|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2379,f2568])).
% 10.17/1.73 fof(f2671,plain,(
% 10.17/1.73 a_863=store(a_861,i5,e_849)|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2665])).
% 10.17/1.73 fof(f2683,plain,(
% 10.17/1.73 select(a_863,i5)=e_849|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2671,f55])).
% 10.17/1.73 fof(f2686,plain,(
% 10.17/1.73 e_862=e_849|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f360,f2683])).
% 10.17/1.73 fof(f2709,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f2643])).
% 10.17/1.73 fof(f2713,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2709])).
% 10.17/1.73 fof(f2719,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2713,f109])).
% 10.17/1.73 fof(f2725,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f2644])).
% 10.17/1.73 fof(f2729,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2725])).
% 10.17/1.73 fof(f2733,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i5|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2729,f2719])).
% 10.17/1.73 fof(f2739,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2733])).
% 10.17/1.73 fof(f2742,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i5|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f674,f2739])).
% 10.17/1.73 fof(f2743,plain,(
% 10.17/1.73 ~e_854=e_866|i2=i5|i1=i5|i0=i5|i1=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f453,f2739])).
% 10.17/1.73 fof(f2744,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2742])).
% 10.17/1.73 fof(f2745,plain,(
% 10.17/1.73 ~e_854=e_866|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2743])).
% 10.17/1.73 fof(f2748,plain,(
% 10.17/1.73 ~e_847=e_837|i2=i5|i1=i5|i0=i5|i0=i2|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f234,f2744])).
% 10.17/1.73 fof(f2749,plain,(
% 10.17/1.73 ~e_847=e_837|i2=i5|i1=i5|i0=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2748])).
% 10.17/1.73 fof(f2750,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i5|i0=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f2749,f2581])).
% 10.17/1.73 fof(f2764,plain,(
% 10.17/1.73 select(a_865,i2)=e_864|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2750,f362])).
% 10.17/1.73 fof(f2766,plain,(
% 10.17/1.73 select(a_844,i2)=e_841|i5=i0|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2750,f158])).
% 10.17/1.73 fof(f2783,plain,(
% 10.17/1.73 e_866=e_864|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f99,f2764])).
% 10.17/1.73 fof(f2784,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f91,f2766])).
% 10.17/1.73 fof(f2785,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2784])).
% 10.17/1.73 fof(f2789,plain,(
% 10.17/1.73 ~e_854=e_864|i2=i5|i1=i5|i0=i5|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2783,f2745])).
% 10.17/1.73 fof(f2795,plain,(
% 10.17/1.73 ~e_854=e_864|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2789])).
% 10.17/1.73 fof(f2839,plain,(
% 10.17/1.73 ~e_854=e_841|i2=i5|i1=i5|i0=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f495,f2795])).
% 10.17/1.73 fof(f2840,plain,(
% 10.17/1.73 ~e_854=e_841|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2839])).
% 10.17/1.73 fof(f2910,plain,(
% 10.17/1.73 ~e_847=e_841|i2=i5|i1=i5|i0=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f234,f2840])).
% 10.17/1.73 fof(f2911,plain,(
% 10.17/1.73 ~e_847=e_841|i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2910])).
% 10.17/1.73 fof(f2912,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f2911,f2785])).
% 10.17/1.73 fof(f2926,plain,(
% 10.17/1.73 select(a_865,i5)=e_864|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2912,f362])).
% 10.17/1.73 fof(f2932,plain,(
% 10.17/1.73 e_862=select(a_861,i5)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2912,f97])).
% 10.17/1.73 fof(f2941,plain,(
% 10.17/1.73 e_868=e_864|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f100,f2926])).
% 10.17/1.73 fof(f2943,plain,(
% 10.17/1.73 e_862=e_864|i2=i5|i1=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f98,f2932])).
% 10.17/1.73 fof(f2945,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2252,f2941])).
% 10.17/1.73 fof(f2954,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2945])).
% 10.17/1.73 fof(f2982,plain,(
% 10.17/1.73 e_870=e_862|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2943,f2954])).
% 10.17/1.73 fof(f2988,plain,(
% 10.17/1.73 e_870=e_862|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f2982])).
% 10.17/1.73 fof(f3013,plain,(
% 10.17/1.73 e_870=e_849|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2686,f2988])).
% 10.17/1.73 fof(f3026,plain,(
% 10.17/1.73 e_870=e_849|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3013])).
% 10.17/1.73 fof(f3040,plain,(
% 10.17/1.73 i5=i_881|i2=i5|i1=i5),
% 10.17/1.73 inference(backward_subsumption_resolution,[status(thm)],[f2418,f3026])).
% 10.17/1.73 fof(f3088,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3040,f107])).
% 10.17/1.73 fof(f3089,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3040,f106])).
% 10.17/1.73 fof(f3154,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f3088])).
% 10.17/1.73 fof(f3158,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3154])).
% 10.17/1.73 fof(f3162,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3158,f109])).
% 10.17/1.73 fof(f3164,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f3089])).
% 10.17/1.73 fof(f3168,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3164])).
% 10.17/1.73 fof(f3171,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3168,f3162])).
% 10.17/1.73 fof(f3174,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3171])).
% 10.17/1.73 fof(f3175,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i1=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f674,f3174])).
% 10.17/1.73 fof(f3177,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i1=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3175])).
% 10.17/1.73 fof(f3181,plain,(
% 10.17/1.73 ~e_847=e_837|i2=i5|i1=i5|i0=i2|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f234,f3177])).
% 10.17/1.73 fof(f3182,plain,(
% 10.17/1.73 ~e_847=e_837|i2=i5|i1=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3181])).
% 10.17/1.73 fof(f3183,plain,(
% 10.17/1.73 i2=i5|i1=i5|i0=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f3182,f2581])).
% 10.17/1.73 fof(f3185,plain,(
% 10.17/1.73 i2=i5|i1=i5|i5=i2|i2=i5|i1=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f2912,f3183])).
% 10.17/1.73 fof(f3207,plain,(
% 10.17/1.73 i2=i5|i1=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3185])).
% 10.17/1.73 fof(f3228,plain,(
% 10.17/1.73 select(a_872,i5)=e_870|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f370])).
% 10.17/1.73 fof(f3230,plain,(
% 10.17/1.73 a_872=store(a_871,i5,e_870)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f79])).
% 10.17/1.73 fof(f3231,plain,(
% 10.17/1.73 a_871=store(a_869,i5,e_870)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f78])).
% 10.17/1.73 fof(f3232,plain,(
% 10.17/1.73 select(a_860,i5)=e_839|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f352])).
% 10.17/1.73 fof(f3233,plain,(
% 10.17/1.73 a_860=store(a_836,i5,e_839)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f72])).
% 10.17/1.73 fof(f3234,plain,(
% 10.17/1.73 select(a_851,i5)=e_849|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f202])).
% 10.17/1.73 fof(f3237,plain,(
% 10.17/1.73 a_851=store(a_850,i5,e_849)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f67])).
% 10.17/1.73 fof(f3239,plain,(
% 10.17/1.73 a_850=store(a_848,i5,e_849)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f66])).
% 10.17/1.73 fof(f3241,plain,(
% 10.17/1.73 select(a_840,i5)=e_839|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f113])).
% 10.17/1.73 fof(f3242,plain,(
% 10.17/1.73 a_840=store(a_838,i5,e_839)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f61])).
% 10.17/1.73 fof(f3243,plain,(
% 10.17/1.73 e_870=select(a_869,i5)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f101])).
% 10.17/1.73 fof(f3244,plain,(
% 10.17/1.73 e_849=select(a_848,i5)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3207,f92])).
% 10.17/1.73 fof(f3249,plain,(
% 10.17/1.73 e_875=e_870|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f103,f3228])).
% 10.17/1.73 fof(f3250,plain,(
% 10.17/1.73 e_854=e_849|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f94,f3234])).
% 10.17/1.73 fof(f3252,plain,(
% 10.17/1.73 e_841=e_839|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f88,f3241])).
% 10.17/1.73 fof(f3253,plain,(
% 10.17/1.73 e_849=e_847|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f174,f3244])).
% 10.17/1.73 fof(f3258,plain,(
% 10.17/1.73 a_855=store(a_853,i2,e_849)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3250,f69])).
% 10.17/1.73 fof(f3277,plain,(
% 10.17/1.73 select(a_861,i5)=e_839|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f357,f3232])).
% 10.17/1.73 fof(f3281,plain,(
% 10.17/1.73 e_864=e_839|i2=i5|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f98,f3277])).
% 10.17/1.73 fof(f3282,plain,(
% 10.17/1.73 e_864=e_839|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3281])).
% 10.17/1.73 fof(f3285,plain,(
% 10.17/1.73 ~e_841=e_839|i2=i_881|i5=i_881|i1=i_881|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3282,f610])).
% 10.17/1.73 fof(f3287,plain,(
% 10.17/1.73 i2=i_881|i5=i_881|i1=i_881|i2=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f3285,f3252])).
% 10.17/1.73 fof(f3296,plain,(
% 10.17/1.73 e_870=e_866|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f403,f3243])).
% 10.17/1.73 fof(f3302,plain,(
% 10.17/1.73 e_870=e_866|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3296])).
% 10.17/1.73 fof(f3306,plain,(
% 10.17/1.73 e_870=e_837|i2=i5|i0=i2|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f444,f3302])).
% 10.17/1.73 fof(f3309,plain,(
% 10.17/1.73 e_870=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3306])).
% 10.17/1.73 fof(f3315,plain,(
% 10.17/1.73 a_872=store(a_871,i5,e_837)|i2=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3309,f3230])).
% 10.17/1.73 fof(f3317,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_872,X0)=select(a_871,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3230,f57])).
% 10.17/1.73 fof(f3319,plain,(
% 10.17/1.73 a_872=store(a_871,i5,e_837)|i2=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3315])).
% 10.17/1.73 fof(f3323,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_871,X0)=select(a_869,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3231,f57])).
% 10.17/1.73 fof(f3326,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_860,X0)=select(a_836,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3233,f57])).
% 10.17/1.73 fof(f3329,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_851,X0)=select(a_850,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3237,f57])).
% 10.17/1.73 fof(f3333,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_850,X0)=select(a_848,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3239,f57])).
% 10.17/1.73 fof(f3335,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_840,X0)=select(a_838,X0)|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3242,f57])).
% 10.17/1.73 fof(f3401,plain,(
% 10.17/1.73 i2=i_881|i2=i5|~i1=i5|i_881=i5),
% 10.17/1.73 inference(equality_factoring,[status(thm)],[f3287])).
% 10.17/1.73 fof(f3412,plain,(
% 10.17/1.73 i2=i_881|i2=i5|i_881=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f3401,f3207])).
% 10.17/1.73 fof(f3421,plain,(
% 10.17/1.73 e_883=select(a_880,i2)|i2=i5|i_881=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3412,f107])).
% 10.17/1.73 fof(f3422,plain,(
% 10.17/1.73 e_882=select(a_859,i2)|i2=i5|i_881=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3412,f106])).
% 10.17/1.73 fof(f3438,plain,(
% 10.17/1.73 e_883=e_879|i2=i5|i_881=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f380,f3421])).
% 10.17/1.73 fof(f3439,plain,(
% 10.17/1.73 e_882=e_858|i2=i5|i_881=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f3422])).
% 10.17/1.73 fof(f3442,plain,(
% 10.17/1.73 ~e_882=e_879|i2=i5|i_881=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3438,f109])).
% 10.17/1.73 fof(f3451,plain,(
% 10.17/1.73 ~e_858=e_879|i2=i5|i_881=i5|i2=i5|i_881=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3439,f3442])).
% 10.17/1.73 fof(f3453,plain,(
% 10.17/1.73 ~e_858=e_879|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3451])).
% 10.17/1.73 fof(f3458,plain,(
% 10.17/1.73 ~e_858=e_873|i2=i5|i_881=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f421,f3453])).
% 10.17/1.73 fof(f3463,plain,(
% 10.17/1.73 ~e_858=e_873|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3458])).
% 10.17/1.73 fof(f3481,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_872,X0)=select(a_869,X0)|i2=i5|i5=X0|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3317,f3323])).
% 10.17/1.73 fof(f3489,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_872,X0)=select(a_869,X0)|i2=i5)),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3481])).
% 10.17/1.73 fof(f3493,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_861,X0)=select(a_836,X0)|i2=i5|i2=X0)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f357,f3326])).
% 10.17/1.73 fof(f3511,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_851,X0)=select(a_848,X0)|i2=i5|i5=X0|i2=i5)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3329,f3333])).
% 10.17/1.73 fof(f3519,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_851,X0)=select(a_848,X0)|i2=i5)),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3511])).
% 10.17/1.73 fof(f3521,plain,(
% 10.17/1.73 i5=i2|select(a_840,i2)=e_837|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f112,f3335])).
% 10.17/1.73 fof(f3522,plain,(
% 10.17/1.73 ![X0]: (i5=X0|select(a_840,X0)=select(a_836,X0)|i2=i5|i2=X0)),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f118,f3335])).
% 10.17/1.73 fof(f3527,plain,(
% 10.17/1.73 i5=i2|select(a_840,i2)=e_837),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3521])).
% 10.17/1.73 fof(f3530,plain,(
% 10.17/1.73 i5=i2|e_847=e_837|i5=i2|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f138,f3527])).
% 10.17/1.73 fof(f3535,plain,(
% 10.17/1.73 i5=i2|e_847=e_837|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3530])).
% 10.17/1.73 fof(f3537,plain,(
% 10.17/1.73 i5=i2|e_849=e_837|i0=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3253,f3535])).
% 10.17/1.73 fof(f3542,plain,(
% 10.17/1.73 i5=i2|e_849=e_837|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3537])).
% 10.17/1.73 fof(f3546,plain,(
% 10.17/1.73 a_855=store(a_853,i2,e_837)|i2=i5|i5=i2|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3542,f3258])).
% 10.17/1.73 fof(f3554,plain,(
% 10.17/1.73 a_855=store(a_853,i2,e_837)|i2=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3546])).
% 10.17/1.73 fof(f3560,plain,(
% 10.17/1.73 i5=i2|select(a_872,i2)=e_868|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f366,f3489])).
% 10.17/1.73 fof(f3570,plain,(
% 10.17/1.73 i5=i2|e_873=e_868|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f102,f3560])).
% 10.17/1.73 fof(f3571,plain,(
% 10.17/1.73 i5=i2|e_873=e_868),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3570])).
% 10.17/1.73 fof(f3579,plain,(
% 10.17/1.73 ~e_858=e_868|i2=i5|i_881=i5|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3571,f3463])).
% 10.17/1.73 fof(f3585,plain,(
% 10.17/1.73 ~e_858=e_868|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3579])).
% 10.17/1.73 fof(f3588,plain,(
% 10.17/1.73 ~e_858=e_862|i2=i5|i_881=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f398,f3585])).
% 10.17/1.73 fof(f3618,plain,(
% 10.17/1.73 i5=i2|select(a_851,i2)=e_843|i2=i5|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f175,f3519])).
% 10.17/1.73 fof(f3627,plain,(
% 10.17/1.73 i5=i2|e_852=e_843|i2=i5|i5=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f93,f3618])).
% 10.17/1.73 fof(f3628,plain,(
% 10.17/1.73 i5=i2|e_852=e_843),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3627])).
% 10.17/1.73 fof(f3633,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_843)|i2=i5|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3628,f310])).
% 10.17/1.73 fof(f3635,plain,(
% 10.17/1.73 a_859=store(a_857,i2,e_843)|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3633])).
% 10.17/1.73 fof(f3637,plain,(
% 10.17/1.73 select(a_859,i2)=e_843|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3635,f55])).
% 10.17/1.73 fof(f3638,plain,(
% 10.17/1.73 e_858=e_843|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f312,f3637])).
% 10.17/1.73 fof(f3658,plain,(
% 10.17/1.73 select(a_872,i5)=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3319,f55])).
% 10.17/1.73 fof(f3659,plain,(
% 10.17/1.73 e_875=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f103,f3658])).
% 10.17/1.73 fof(f3692,plain,(
% 10.17/1.73 select(a_855,i2)=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3554,f55])).
% 10.17/1.73 fof(f3693,plain,(
% 10.17/1.73 e_854=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f261,f3692])).
% 10.17/1.73 fof(f3782,plain,(
% 10.17/1.73 i5=i0|e_862=select(a_836,i0)|i2=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f97,f3493])).
% 10.17/1.73 fof(f3802,plain,(
% 10.17/1.73 i5=i0|e_843=select(a_836,i0)|i2=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f89,f3522])).
% 10.17/1.73 fof(f3850,plain,(
% 10.17/1.73 i5=i0|e_843=e_862|i2=i5|i2=i0|i5=i0|i2=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3782,f3802])).
% 10.17/1.73 fof(f3856,plain,(
% 10.17/1.73 i5=i0|e_843=e_862|i2=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3850])).
% 10.17/1.73 fof(f3863,plain,(
% 10.17/1.73 ~e_858=e_843|i2=i5|i_881=i5|i0=i5|i5=i0|i2=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3856,f3588])).
% 10.17/1.73 fof(f3870,plain,(
% 10.17/1.73 ~e_858=e_843|i2=i5|i_881=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3863])).
% 10.17/1.73 fof(f3871,plain,(
% 10.17/1.73 i2=i5|i_881=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f3870,f3638])).
% 10.17/1.73 fof(f3884,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3871,f107])).
% 10.17/1.73 fof(f3885,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3871,f106])).
% 10.17/1.73 fof(f3896,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i0=i5|i2=i0|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f3884])).
% 10.17/1.73 fof(f3900,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3896])).
% 10.17/1.73 fof(f3906,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3900,f109])).
% 10.17/1.73 fof(f3912,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i0=i5|i2=i0|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f3885])).
% 10.17/1.73 fof(f3916,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3912])).
% 10.17/1.73 fof(f3920,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i0=i5|i2=i0|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3916,f3906])).
% 10.17/1.73 fof(f3926,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3920])).
% 10.17/1.73 fof(f3929,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i0=i5|i2=i0|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3659,f3926])).
% 10.17/1.73 fof(f3931,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3929])).
% 10.17/1.73 fof(f3932,plain,(
% 10.17/1.73 i2=i5|i0=i5|i2=i0),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f3931,f3693])).
% 10.17/1.73 fof(f3948,plain,(
% 10.17/1.73 select(a_865,i2)=e_864|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3932,f362])).
% 10.17/1.73 fof(f3950,plain,(
% 10.17/1.73 select(a_844,i2)=e_841|i5=i0|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3932,f158])).
% 10.17/1.73 fof(f3954,plain,(
% 10.17/1.73 e_862=select(a_861,i2)|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3932,f97])).
% 10.17/1.73 fof(f3955,plain,(
% 10.17/1.73 e_843=select(a_840,i2)|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3932,f89])).
% 10.17/1.73 fof(f3968,plain,(
% 10.17/1.73 e_866=e_864|i2=i5|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f99,f3948])).
% 10.17/1.73 fof(f3969,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i2=i5|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f91,f3950])).
% 10.17/1.73 fof(f3970,plain,(
% 10.17/1.73 e_847=e_841|i5=i0|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3969])).
% 10.17/1.73 fof(f3972,plain,(
% 10.17/1.73 e_862=e_837|i2=i5|i0=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f358,f3954])).
% 10.17/1.73 fof(f3973,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3302,f3968])).
% 10.17/1.73 fof(f3978,plain,(
% 10.17/1.73 e_870=e_864|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3973])).
% 10.17/1.73 fof(f3983,plain,(
% 10.17/1.73 e_849=e_841|i5=i0|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3253,f3970])).
% 10.17/1.73 fof(f3990,plain,(
% 10.17/1.73 e_849=e_841|i5=i0|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3983])).
% 10.17/1.73 fof(f3996,plain,(
% 10.17/1.73 ~e_858=e_837|i2=i5|i_881=i5|i0=i5|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3972,f3588])).
% 10.17/1.73 fof(f4003,plain,(
% 10.17/1.73 ~e_858=e_837|i2=i5|i_881=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f3996])).
% 10.17/1.73 fof(f4006,plain,(
% 10.17/1.73 e_870=e_839|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3282,f3978])).
% 10.17/1.73 fof(f4010,plain,(
% 10.17/1.73 e_870=e_839|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4006])).
% 10.17/1.73 fof(f4012,plain,(
% 10.17/1.73 e_849=e_839|i5=i0|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3252,f3990])).
% 10.17/1.73 fof(f4015,plain,(
% 10.17/1.73 e_849=e_839|i5=i0|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4012])).
% 10.17/1.73 fof(f4061,plain,(
% 10.17/1.73 e_843=e_837|i2=i5|i0=i5|i5=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3527,f3955])).
% 10.17/1.73 fof(f4071,plain,(
% 10.17/1.73 e_843=e_837|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4061])).
% 10.17/1.73 fof(f4086,plain,(
% 10.17/1.73 ~e_843=e_837|i2=i5|i_881=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3638,f4003])).
% 10.17/1.73 fof(f4088,plain,(
% 10.17/1.73 ~e_843=e_837|i2=i5|i_881=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4086])).
% 10.17/1.73 fof(f4089,plain,(
% 10.17/1.73 i2=i5|i_881=i5|i0=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f4088,f4071])).
% 10.17/1.73 fof(f4101,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4089,f107])).
% 10.17/1.73 fof(f4102,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4089,f106])).
% 10.17/1.73 fof(f4113,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f4101])).
% 10.17/1.73 fof(f4117,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4113])).
% 10.17/1.73 fof(f4123,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4117,f109])).
% 10.17/1.73 fof(f4129,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f4102])).
% 10.17/1.73 fof(f4133,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4129])).
% 10.17/1.73 fof(f4137,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i0=i5|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4133,f4123])).
% 10.17/1.73 fof(f4143,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4137])).
% 10.17/1.73 fof(f4147,plain,(
% 10.17/1.73 ~e_854=e_870|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3249,f4143])).
% 10.17/1.73 fof(f4149,plain,(
% 10.17/1.73 ~e_854=e_870|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4147])).
% 10.17/1.73 fof(f4151,plain,(
% 10.17/1.73 ~e_849=e_870|i2=i5|i0=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3250,f4149])).
% 10.17/1.73 fof(f4154,plain,(
% 10.17/1.73 ~e_849=e_870|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4151])).
% 10.17/1.73 fof(f4155,plain,(
% 10.17/1.73 ~e_849=e_839|i2=i5|i0=i5|i2=i5|i0=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4010,f4154])).
% 10.17/1.73 fof(f4158,plain,(
% 10.17/1.73 ~e_849=e_839|i2=i5|i0=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4155])).
% 10.17/1.73 fof(f4159,plain,(
% 10.17/1.73 i2=i5|i0=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f4158,f4015])).
% 10.17/1.73 fof(f4175,plain,(
% 10.17/1.73 select(a_865,i5)=e_864|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4159,f362])).
% 10.17/1.73 fof(f4182,plain,(
% 10.17/1.73 e_843=select(a_840,i5)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4159,f89])).
% 10.17/1.73 fof(f4191,plain,(
% 10.17/1.73 e_868=e_864|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f100,f4175])).
% 10.17/1.73 fof(f4194,plain,(
% 10.17/1.73 e_843=e_841|i2=i5),
% 10.17/1.73 inference(forward_demodulation,[status(thm)],[f88,f4182])).
% 10.17/1.73 fof(f4199,plain,(
% 10.17/1.73 ~e_858=e_864|i2=i5|i_881=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4191,f3585])).
% 10.17/1.73 fof(f4206,plain,(
% 10.17/1.73 ~e_858=e_864|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4199])).
% 10.17/1.73 fof(f4232,plain,(
% 10.17/1.73 ~e_858=e_839|i2=i5|i_881=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3282,f4206])).
% 10.17/1.73 fof(f4234,plain,(
% 10.17/1.73 ~e_858=e_839|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4232])).
% 10.17/1.73 fof(f4239,plain,(
% 10.17/1.73 ~e_843=e_839|i2=i5|i_881=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3638,f4234])).
% 10.17/1.73 fof(f4241,plain,(
% 10.17/1.73 ~e_843=e_839|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4239])).
% 10.17/1.73 fof(f4243,plain,(
% 10.17/1.73 ~e_841=e_839|i2=i5|i_881=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4194,f4241])).
% 10.17/1.73 fof(f4244,plain,(
% 10.17/1.73 ~e_841=e_839|i2=i5|i_881=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4243])).
% 10.17/1.73 fof(f4245,plain,(
% 10.17/1.73 i2=i5|i_881=i5),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f4244,f3252])).
% 10.17/1.73 fof(f4254,plain,(
% 10.17/1.73 e_883=select(a_880,i5)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4245,f107])).
% 10.17/1.73 fof(f4255,plain,(
% 10.17/1.73 e_882=select(a_859,i5)|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4245,f106])).
% 10.17/1.73 fof(f4262,plain,(
% 10.17/1.73 e_883=e_875|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f426,f4254])).
% 10.17/1.73 fof(f4266,plain,(
% 10.17/1.73 e_883=e_875|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4262])).
% 10.17/1.73 fof(f4270,plain,(
% 10.17/1.73 ~e_882=e_875|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4266,f109])).
% 10.17/1.73 fof(f4271,plain,(
% 10.17/1.73 e_882=e_854|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f313,f4255])).
% 10.17/1.73 fof(f4275,plain,(
% 10.17/1.73 e_882=e_854|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4271])).
% 10.17/1.73 fof(f4582,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4275,f4270])).
% 10.17/1.73 fof(f4584,plain,(
% 10.17/1.73 ~e_854=e_875|i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4582])).
% 10.17/1.73 fof(f4585,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i2=i5|i0=i2),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f3659,f4584])).
% 10.17/1.73 fof(f4587,plain,(
% 10.17/1.73 ~e_854=e_837|i2=i5|i0=i2),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4585])).
% 10.17/1.73 fof(f4588,plain,(
% 10.17/1.73 i2=i5|i0=i2),
% 10.17/1.73 inference(forward_subsumption_resolution,[status(thm)],[f4587,f3693])).
% 10.17/1.73 fof(f4601,plain,(
% 10.17/1.73 i2=i5|i5=i2|i2=i5),
% 10.17/1.73 inference(paramodulation,[status(thm)],[f4159,f4588])).
% 10.17/1.73 fof(f4625,plain,(
% 10.17/1.73 i2=i5),
% 10.17/1.73 inference(duplicate_literals_removal,[status(thm)],[f4601])).
% 10.17/1.73 fof(f4744,plain,(
% 10.17/1.73 e_873=e_843|i1=i2|i0=i5|i5=i0|i1=i0),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f705])).
% 10.17/1.73 fof(f4748,plain,(
% 10.17/1.73 e_868=e_843|i0=i5|i5=i0|i1=i0),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f664])).
% 10.17/1.73 fof(f4754,plain,(
% 10.17/1.73 ~e_841=e_864|i5=i_881|i5=i_881|i1=i_881),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f610])).
% 10.17/1.73 fof(f4755,plain,(
% 10.17/1.73 i5=i_881|e_882=e_841|i5=i_881|i1=i_881),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f607])).
% 10.17/1.73 fof(f4759,plain,(
% 10.17/1.73 i5=i1|e_870=e_839|i5=i1|i0=i1),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f593])).
% 10.17/1.73 fof(f4762,plain,(
% 10.17/1.73 e_873=e_862|i1=i5|i0=i5),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f576])).
% 10.17/1.73 fof(f4764,plain,(
% 10.17/1.73 ~e_882=e_864|i5=i_881|i5=i_881|i1=i_881),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f550])).
% 10.17/1.73 fof(f4772,plain,(
% 10.17/1.73 i5=i1|e_870=select(a_865,i1)|i5=i1),
% 10.17/1.73 inference(backward_demodulation,[status(thm)],[f4625,f473])).
% 10.17/1.74 fof(f4775,plain,(
% 10.17/1.74 i5=i_881|e_883=select(a_872,i_881)|i5=i_881),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f491])).
% 10.17/1.74 fof(f4783,plain,(
% 10.17/1.74 i1=i5|e_873=e_868),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f454])).
% 10.17/1.74 fof(f4791,plain,(
% 10.17/1.74 i5=i1|select(a_861,i1)=e_839),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f388])).
% 10.17/1.74 fof(f4793,plain,(
% 10.17/1.74 select(a_880,i5)=e_879),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f380])).
% 10.17/1.74 fof(f4795,plain,(
% 10.17/1.74 select(a_876,i5)=e_875),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f374])).
% 10.17/1.74 fof(f4797,plain,(
% 10.17/1.74 select(a_869,i5)=e_868),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f366])).
% 10.17/1.74 fof(f4799,plain,(
% 10.17/1.74 select(a_861,i5)=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f358])).
% 10.17/1.74 fof(f4801,plain,(
% 10.17/1.74 select(a_859,i5)=e_858),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f312])).
% 10.17/1.74 fof(f4803,plain,(
% 10.17/1.74 i5=i_881|e_882=select(a_851,i_881)|i5=i_881),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f329])).
% 10.17/1.74 fof(f4810,plain,(
% 10.17/1.74 select(a_855,i5)=e_854),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f261])).
% 10.17/1.74 fof(f4819,plain,(
% 10.17/1.74 i5=i1|e_849=e_839|i5=i1|i0=i1),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f186])).
% 10.17/1.74 fof(f4820,plain,(
% 10.17/1.74 i5=i1|e_849=select(a_844,i1)|i5=i1),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f180])).
% 10.17/1.74 fof(f4826,plain,(
% 10.17/1.74 select(a_840,i2)=e_837|i1=i5),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f149])).
% 10.17/1.74 fof(f4832,plain,(
% 10.17/1.74 e_873=select(a_872,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f102])).
% 10.17/1.74 fof(f4833,plain,(
% 10.17/1.74 e_866=select(a_865,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f99])).
% 10.17/1.74 fof(f4834,plain,(
% 10.17/1.74 e_852=select(a_851,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f93])).
% 10.17/1.74 fof(f4835,plain,(
% 10.17/1.74 e_847=select(a_844,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f91])).
% 10.17/1.74 fof(f4836,plain,(
% 10.17/1.74 e_839=select(a_836,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4625,f87])).
% 10.17/1.74 fof(f4837,plain,(
% 10.17/1.74 e_873=e_843|i1=i5|i0=i5|i5=i0|i1=i0),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4625,f4744])).
% 10.17/1.74 fof(f4838,plain,(
% 10.17/1.74 e_873=e_843|i1=i5|i0=i5|i1=i0),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4837])).
% 10.17/1.74 fof(f4843,plain,(
% 10.17/1.74 e_868=e_843|i0=i5|i1=i0),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4748])).
% 10.17/1.74 fof(f4850,plain,(
% 10.17/1.74 ~e_841=e_864|i5=i_881|i1=i_881),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4754])).
% 10.17/1.74 fof(f4851,plain,(
% 10.17/1.74 i5=i_881|e_882=e_841|i1=i_881),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4755])).
% 10.17/1.74 fof(f4855,plain,(
% 10.17/1.74 i5=i1|e_870=e_839|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4759])).
% 10.17/1.74 fof(f4857,plain,(
% 10.17/1.74 ~e_882=e_864|i5=i_881|i1=i_881),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4764])).
% 10.17/1.74 fof(f4866,plain,(
% 10.17/1.74 i5=i1|e_870=select(a_865,i1)),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4772])).
% 10.17/1.74 fof(f4867,plain,(
% 10.17/1.74 i5=i_881|e_883=select(a_872,i_881)),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4775])).
% 10.17/1.74 fof(f4873,plain,(
% 10.17/1.74 i5=i_881|e_882=select(a_851,i_881)),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4803])).
% 10.17/1.74 fof(f4880,plain,(
% 10.17/1.74 i5=i1|e_849=e_839|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4819])).
% 10.17/1.74 fof(f4881,plain,(
% 10.17/1.74 i5=i1|e_849=select(a_844,i1)),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f4820])).
% 10.17/1.74 fof(f4883,plain,(
% 10.17/1.74 select(a_840,i5)=e_837|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4625,f4826])).
% 10.17/1.74 fof(f4884,plain,(
% 10.17/1.74 e_841=e_837|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f88,f4883])).
% 10.17/1.74 fof(f4885,plain,(
% 10.17/1.74 e_847=e_843),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f135,f4835])).
% 10.17/1.74 fof(f4887,plain,(
% 10.17/1.74 e_854=e_843|i1=i5),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4885,f234])).
% 10.17/1.74 fof(f4888,plain,(
% 10.17/1.74 select(a_848,i5)=e_843),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4885,f174])).
% 10.17/1.74 fof(f4890,plain,(
% 10.17/1.74 e_879=e_875),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4795,f105])).
% 10.17/1.74 fof(f4891,plain,(
% 10.17/1.74 select(a_880,i5)=e_875),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4890,f4793])).
% 10.17/1.74 fof(f4901,plain,(
% 10.17/1.74 e_864=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4799,f98])).
% 10.17/1.74 fof(f4902,plain,(
% 10.17/1.74 select(a_865,i0)=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4901,f362])).
% 10.17/1.74 fof(f4904,plain,(
% 10.17/1.74 e_858=e_854),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4810,f96])).
% 10.17/1.74 fof(f4905,plain,(
% 10.17/1.74 select(a_859,i5)=e_854),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4904,f4801])).
% 10.17/1.74 fof(f4912,plain,(
% 10.17/1.74 e_875=e_873),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4832,f103])).
% 10.17/1.74 fof(f4920,plain,(
% 10.17/1.74 e_868=e_866),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4833,f100])).
% 10.17/1.74 fof(f4946,plain,(
% 10.17/1.74 ~e_841=e_837|i5=i_881|i1=i_881),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4901,f4850])).
% 10.17/1.74 fof(f4947,plain,(
% 10.17/1.74 i5=i_881|i1=i_881|i1=i5),
% 10.17/1.74 inference(resolution,[status(thm)],[f4946,f4884])).
% 10.17/1.74 fof(f4977,plain,(
% 10.17/1.74 ~e_882=e_837|i5=i_881|i1=i_881),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4901,f4857])).
% 10.17/1.74 fof(f5009,plain,(
% 10.17/1.74 i5=i_881|e_882=select(a_851,i1)|i5=i_881|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4947,f4873])).
% 10.17/1.74 fof(f5011,plain,(
% 10.17/1.74 i5=i_881|e_883=select(a_872,i1)|i5=i_881|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4947,f4867])).
% 10.17/1.74 fof(f5018,plain,(
% 10.17/1.74 i5=i_881|e_882=e_849|i5=i_881|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f202,f5009])).
% 10.17/1.74 fof(f5019,plain,(
% 10.17/1.74 i5=i_881|e_882=e_849|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5018])).
% 10.17/1.74 fof(f5021,plain,(
% 10.17/1.74 i5=i_881|e_883=e_870|i5=i_881|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f370,f5011])).
% 10.17/1.74 fof(f5022,plain,(
% 10.17/1.74 i5=i_881|e_883=e_870|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5021])).
% 10.17/1.74 fof(f5032,plain,(
% 10.17/1.74 ~e_882=e_870|i5=i_881|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5022,f109])).
% 10.17/1.74 fof(f5035,plain,(
% 10.17/1.74 ~e_849=e_870|i5=i_881|i1=i5|i5=i_881|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5019,f5032])).
% 10.17/1.74 fof(f5037,plain,(
% 10.17/1.74 ~e_849=e_870|i5=i_881|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5035])).
% 10.17/1.74 fof(f5039,plain,(
% 10.17/1.74 ~e_849=e_839|i5=i_881|i1=i5|i5=i1|i0=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4855,f5037])).
% 10.17/1.74 fof(f5040,plain,(
% 10.17/1.74 ~e_849=e_839|i5=i_881|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5039])).
% 10.17/1.74 fof(f5041,plain,(
% 10.17/1.74 i5=i_881|i1=i5|i0=i1),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5040,f4880])).
% 10.17/1.74 fof(f5050,plain,(
% 10.17/1.74 e_883=select(a_880,i5)|i1=i5|i0=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5041,f107])).
% 10.17/1.74 fof(f5051,plain,(
% 10.17/1.74 e_882=select(a_859,i5)|i1=i5|i0=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5041,f106])).
% 10.17/1.74 fof(f5209,plain,(
% 10.17/1.74 e_866=e_843|i0=i5|i1=i0),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4920,f4843])).
% 10.17/1.74 fof(f5210,plain,(
% 10.17/1.74 i1=i5|e_873=e_866),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4920,f4783])).
% 10.17/1.74 fof(f5212,plain,(
% 10.17/1.74 select(a_869,i5)=e_866),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4920,f4797])).
% 10.17/1.74 fof(f5214,plain,(
% 10.17/1.74 e_854=e_852),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f4834,f94])).
% 10.17/1.74 fof(f5217,plain,(
% 10.17/1.74 e_852=e_843|i1=i5),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5214,f4887])).
% 10.17/1.74 fof(f5233,plain,(
% 10.17/1.74 select(a_880,i5)=e_873),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4912,f4891])).
% 10.17/1.74 fof(f5240,plain,(
% 10.17/1.74 select(a_859,i5)=e_852),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5214,f4905])).
% 10.17/1.74 fof(f5387,plain,(
% 10.17/1.74 e_883=e_873|i1=i5|i0=i1),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5233,f5050])).
% 10.17/1.74 fof(f5392,plain,(
% 10.17/1.74 ~e_882=e_873|i1=i5|i0=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5387,f109])).
% 10.17/1.74 fof(f5398,plain,(
% 10.17/1.74 e_882=e_852|i1=i5|i0=i1),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5240,f5051])).
% 10.17/1.74 fof(f5401,plain,(
% 10.17/1.74 ~e_852=e_873|i1=i5|i0=i1|i1=i5|i0=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5398,f5392])).
% 10.17/1.74 fof(f5407,plain,(
% 10.17/1.74 ~e_852=e_873|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5401])).
% 10.17/1.74 fof(f5410,plain,(
% 10.17/1.74 ~e_852=e_866|i1=i5|i0=i1|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5210,f5407])).
% 10.17/1.74 fof(f5411,plain,(
% 10.17/1.74 ~e_852=e_843|i1=i5|i0=i1|i1=i5|i0=i5|i1=i0),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4838,f5407])).
% 10.17/1.74 fof(f5413,plain,(
% 10.17/1.74 ~e_852=e_866|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5410])).
% 10.17/1.74 fof(f5414,plain,(
% 10.17/1.74 ~e_852=e_843|i1=i5|i0=i1|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5411])).
% 10.17/1.74 fof(f5415,plain,(
% 10.17/1.74 i1=i5|i0=i1|i0=i5),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5414,f5217])).
% 10.17/1.74 fof(f5423,plain,(
% 10.17/1.74 select(a_865,i1)=e_837|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5415,f4902])).
% 10.17/1.74 fof(f5436,plain,(
% 10.17/1.74 select(a_844,i1)=e_841|i5=i0|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5415,f158])).
% 10.17/1.74 fof(f5439,plain,(
% 10.17/1.74 e_862=select(a_861,i1)|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5415,f97])).
% 10.17/1.74 fof(f5440,plain,(
% 10.17/1.74 e_843=select(a_840,i1)|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5415,f89])).
% 10.17/1.74 fof(f5450,plain,(
% 10.17/1.74 select(a_844,i1)=e_841|i5=i0|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5436])).
% 10.17/1.74 fof(f5451,plain,(
% 10.17/1.74 e_843=e_839|i1=i5|i0=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f113,f5440])).
% 10.17/1.74 fof(f5484,plain,(
% 10.17/1.74 e_870=e_837|i1=i5|i0=i5|i5=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4866,f5423])).
% 10.17/1.74 fof(f5488,plain,(
% 10.17/1.74 e_870=e_837|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5484])).
% 10.17/1.74 fof(f5493,plain,(
% 10.17/1.74 ~e_849=e_837|i5=i_881|i1=i5|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5488,f5037])).
% 10.17/1.74 fof(f5498,plain,(
% 10.17/1.74 ~e_849=e_837|i5=i_881|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5493])).
% 10.17/1.74 fof(f5500,plain,(
% 10.17/1.74 e_849=e_841|i5=i0|i1=i5|i5=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4881,f5450])).
% 10.17/1.74 fof(f5504,plain,(
% 10.17/1.74 e_849=e_841|i5=i0|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5500])).
% 10.17/1.74 fof(f5510,plain,(
% 10.17/1.74 e_849=e_837|i5=i0|i1=i5|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4884,f5504])).
% 10.17/1.74 fof(f5514,plain,(
% 10.17/1.74 e_849=e_837|i5=i0|i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5510])).
% 10.17/1.74 fof(f5531,plain,(
% 10.17/1.74 e_862=e_839|i1=i5|i0=i5|i5=i1),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4791,f5439])).
% 10.17/1.74 fof(f5537,plain,(
% 10.17/1.74 e_862=e_839|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5531])).
% 10.17/1.74 fof(f5551,plain,(
% 10.17/1.74 i5=i_881|i1=i5|i0=i5),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5498,f5514])).
% 10.17/1.74 fof(f5564,plain,(
% 10.17/1.74 e_883=select(a_880,i5)|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5551,f107])).
% 10.17/1.74 fof(f5565,plain,(
% 10.17/1.74 e_882=select(a_859,i5)|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5551,f106])).
% 10.17/1.74 fof(f5576,plain,(
% 10.17/1.74 e_883=e_873|i1=i5|i0=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5233,f5564])).
% 10.17/1.74 fof(f5577,plain,(
% 10.17/1.74 e_882=e_852|i1=i5|i0=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5240,f5565])).
% 10.17/1.74 fof(f5584,plain,(
% 10.17/1.74 ~e_882=e_873|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5576,f109])).
% 10.17/1.74 fof(f5600,plain,(
% 10.17/1.74 ~e_852=e_873|i1=i5|i0=i5|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5577,f5584])).
% 10.17/1.74 fof(f5604,plain,(
% 10.17/1.74 ~e_852=e_873|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5600])).
% 10.17/1.74 fof(f5608,plain,(
% 10.17/1.74 ~e_852=e_862|i1=i5|i0=i5|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f4762,f5604])).
% 10.17/1.74 fof(f5610,plain,(
% 10.17/1.74 ~e_852=e_862|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5608])).
% 10.17/1.74 fof(f5615,plain,(
% 10.17/1.74 ~e_852=e_839|i1=i5|i0=i5|i1=i5|i0=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5537,f5610])).
% 10.17/1.74 fof(f5617,plain,(
% 10.17/1.74 ~e_852=e_839|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5615])).
% 10.17/1.74 fof(f5619,plain,(
% 10.17/1.74 ~e_843=e_839|i1=i5|i0=i5|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5217,f5617])).
% 10.17/1.74 fof(f5620,plain,(
% 10.17/1.74 ~e_843=e_839|i1=i5|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5619])).
% 10.17/1.74 fof(f5621,plain,(
% 10.17/1.74 i1=i5|i0=i5),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5620,f5451])).
% 10.17/1.74 fof(f5624,plain,(
% 10.17/1.74 select(a_865,i5)=e_837|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5621,f4902])).
% 10.17/1.74 fof(f5641,plain,(
% 10.17/1.74 e_843=select(a_840,i5)|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5621,f89])).
% 10.17/1.74 fof(f5642,plain,(
% 10.17/1.74 e_866=e_837|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f4833,f5624])).
% 10.17/1.74 fof(f5656,plain,(
% 10.17/1.74 e_843=e_841|i1=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f88,f5641])).
% 10.17/1.74 fof(f5659,plain,(
% 10.17/1.74 ~e_852=e_837|i1=i5|i0=i1|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5642,f5413])).
% 10.17/1.74 fof(f5668,plain,(
% 10.17/1.74 ~e_852=e_837|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5659])).
% 10.17/1.74 fof(f5695,plain,(
% 10.17/1.74 ~e_843=e_837|i1=i5|i0=i1|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5217,f5668])).
% 10.17/1.74 fof(f5696,plain,(
% 10.17/1.74 ~e_843=e_837|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5695])).
% 10.17/1.74 fof(f5697,plain,(
% 10.17/1.74 ~e_841=e_837|i1=i5|i0=i1|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5656,f5696])).
% 10.17/1.74 fof(f5698,plain,(
% 10.17/1.74 ~e_841=e_837|i1=i5|i0=i1),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5697])).
% 10.17/1.74 fof(f5699,plain,(
% 10.17/1.74 i1=i5|i0=i1),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5698,f4884])).
% 10.17/1.74 fof(f5701,plain,(
% 10.17/1.74 i1=i5|i5=i1|i1=i5),
% 10.17/1.74 inference(paramodulation,[status(thm)],[f5621,f5699])).
% 10.17/1.74 fof(f5722,plain,(
% 10.17/1.74 i1=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5701])).
% 10.17/1.74 fof(f5824,plain,(
% 10.17/1.74 e_866=e_843|i0=i5|i5=i0),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f5209])).
% 10.17/1.74 fof(f5857,plain,(
% 10.17/1.74 ~e_882=e_837|i5=i_881|i5=i_881),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f4977])).
% 10.17/1.74 fof(f5858,plain,(
% 10.17/1.74 i5=i_881|e_882=e_841|i5=i_881),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f4851])).
% 10.17/1.74 fof(f5865,plain,(
% 10.17/1.74 select(a_872,i5)=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f370])).
% 10.17/1.74 fof(f5871,plain,(
% 10.17/1.74 select(a_851,i5)=e_849),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f202])).
% 10.17/1.74 fof(f5878,plain,(
% 10.17/1.74 select(a_840,i5)=e_839),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f113])).
% 10.17/1.74 fof(f5881,plain,(
% 10.17/1.74 e_870=select(a_869,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f101])).
% 10.17/1.74 fof(f5882,plain,(
% 10.17/1.74 e_849=select(a_848,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f92])).
% 10.17/1.74 fof(f5883,plain,(
% 10.17/1.74 e_837=select(a_836,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5722,f86])).
% 10.17/1.74 fof(f5889,plain,(
% 10.17/1.74 e_866=e_843|i0=i5),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5824])).
% 10.17/1.74 fof(f5909,plain,(
% 10.17/1.74 ~e_882=e_837|i5=i_881),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5857])).
% 10.17/1.74 fof(f5910,plain,(
% 10.17/1.74 i5=i_881|e_882=e_841),
% 10.17/1.74 inference(duplicate_literals_removal,[status(thm)],[f5858])).
% 10.17/1.74 fof(f5914,plain,(
% 10.17/1.74 e_873=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5865,f4832])).
% 10.17/1.74 fof(f5920,plain,(
% 10.17/1.74 select(a_880,i5)=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5914,f5233])).
% 10.17/1.74 fof(f5932,plain,(
% 10.17/1.74 e_852=e_849),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5871,f4834])).
% 10.17/1.74 fof(f5937,plain,(
% 10.17/1.74 select(a_859,i5)=e_849),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5932,f5240])).
% 10.17/1.74 fof(f5944,plain,(
% 10.17/1.74 e_841=e_839),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5878,f88])).
% 10.17/1.74 fof(f5949,plain,(
% 10.17/1.74 e_870=e_866),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5881,f5212])).
% 10.17/1.74 fof(f5955,plain,(
% 10.17/1.74 e_870=select(a_865,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5949,f4833])).
% 10.17/1.74 fof(f5964,plain,(
% 10.17/1.74 e_870=e_843|i0=i5),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5949,f5889])).
% 10.17/1.74 fof(f5985,plain,(
% 10.17/1.74 i5=i_881|e_882=e_839),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5944,f5910])).
% 10.17/1.74 fof(f6169,plain,(
% 10.17/1.74 e_849=e_843),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5882,f4888])).
% 10.17/1.74 fof(f6180,plain,(
% 10.17/1.74 e_870=e_849|i0=i5),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6169,f5964])).
% 10.17/1.74 fof(f6188,plain,(
% 10.17/1.74 e_849=select(a_840,i0)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6169,f89])).
% 10.17/1.74 fof(f6189,plain,(
% 10.17/1.74 e_839=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f5883,f4836])).
% 10.17/1.74 fof(f6191,plain,(
% 10.17/1.74 i5=i_881|e_882=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6189,f5985])).
% 10.17/1.74 fof(f6194,plain,(
% 10.17/1.74 select(a_840,i5)=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6189,f5878])).
% 10.17/1.74 fof(f6197,plain,(
% 10.17/1.74 i5=i_881),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f6191,f5909])).
% 10.17/1.74 fof(f6217,plain,(
% 10.17/1.74 e_883=select(a_880,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6197,f107])).
% 10.17/1.74 fof(f6218,plain,(
% 10.17/1.74 e_882=select(a_859,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6197,f106])).
% 10.17/1.74 fof(f6483,plain,(
% 10.17/1.74 ~e_882=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6484,f109])).
% 10.17/1.74 fof(f6484,plain,(
% 10.17/1.74 e_883=e_870),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5920,f6217])).
% 10.17/1.74 fof(f6485,plain,(
% 10.17/1.74 ~e_849=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6486,f6483])).
% 10.17/1.74 fof(f6486,plain,(
% 10.17/1.74 e_882=e_849),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f5937,f6218])).
% 10.17/1.74 fof(f6487,plain,(
% 10.17/1.74 i0=i5),
% 10.17/1.74 inference(backward_subsumption_resolution,[status(thm)],[f6180,f6485])).
% 10.17/1.74 fof(f6488,plain,(
% 10.17/1.74 e_849=select(a_840,i5)),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6487,f6188])).
% 10.17/1.74 fof(f6515,plain,(
% 10.17/1.74 select(a_865,i5)=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6487,f4902])).
% 10.17/1.74 fof(f6522,plain,(
% 10.17/1.74 e_849=e_837),
% 10.17/1.74 inference(forward_demodulation,[status(thm)],[f6194,f6488])).
% 10.17/1.74 fof(f6526,plain,(
% 10.17/1.74 ~e_837=e_870),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6522,f6485])).
% 10.17/1.74 fof(f6558,plain,(
% 10.17/1.74 e_870=e_837),
% 10.17/1.74 inference(backward_demodulation,[status(thm)],[f6515,f5955])).
% 10.17/1.74 fof(f6559,plain,(
% 10.17/1.74 $false),
% 10.17/1.74 inference(forward_subsumption_resolution,[status(thm)],[f6558,f6526])).
% 10.17/1.74 % SZS output end CNFRefutation for theBenchmark.p
% 10.17/1.74 % Elapsed time: 1.360220 seconds
% 10.17/1.74 % CPU time: 10.447939 seconds
% 10.17/1.74 % Total memory used: 212.984 MB
% 10.17/1.74 % Net memory used: 207.500 MB
%------------------------------------------------------------------------------