Drodi---4.1.1.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : SWV537-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox2/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:48:26 PM UTC 2026

% Result   : Unsatisfiable 21.25s 8.26s
% Output   : CNFRefutation 21.25s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [A,I,E] : select(store(A,I,E),I) = E,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f2,axiom,
    ! [I,J,A,E] :
      ( select(store(A,I,E),J) = select(A,J)
      | I = J ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f5,hypothesis,
    a_838 = store(a_836,i2,e_837),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f6,hypothesis,
    a_840 = store(a_838,i1,e_839),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f7,hypothesis,
    a_842 = store(a_840,i0,e_841),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f8,hypothesis,
    a_844 = store(a_842,i5,e_843),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f9,hypothesis,
    a_846 = store(a_844,i2,e_845),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f10,hypothesis,
    a_848 = store(a_846,i5,e_847),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f11,hypothesis,
    a_850 = store(a_848,i1,e_849),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f12,hypothesis,
    a_851 = store(a_850,i1,e_849),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f13,hypothesis,
    a_853 = store(a_851,i5,e_852),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f14,hypothesis,
    a_855 = store(a_853,i2,e_854),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f15,hypothesis,
    a_857 = store(a_855,i5,e_856),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f16,hypothesis,
    a_859 = store(a_857,i2,e_858),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f17,hypothesis,
    a_860 = store(a_836,i1,e_839),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f18,hypothesis,
    a_861 = store(a_860,i2,e_837),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f19,hypothesis,
    a_863 = store(a_861,i5,e_862),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f20,hypothesis,
    a_865 = store(a_863,i0,e_864),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f21,hypothesis,
    a_867 = store(a_865,i5,e_866),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f22,hypothesis,
    a_869 = store(a_867,i2,e_868),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f23,hypothesis,
    a_871 = store(a_869,i1,e_870),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f24,hypothesis,
    a_872 = store(a_871,i1,e_870),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f25,hypothesis,
    a_874 = store(a_872,i5,e_873),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f26,hypothesis,
    a_876 = store(a_874,i2,e_875),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f27,hypothesis,
    a_878 = store(a_876,i5,e_877),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f28,hypothesis,
    a_880 = store(a_878,i2,e_879),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f31,hypothesis,
    e_837 = select(a_836,i1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f32,hypothesis,
    e_839 = select(a_836,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f33,hypothesis,
    e_841 = select(a_840,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f34,hypothesis,
    e_843 = select(a_840,i0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f35,hypothesis,
    e_845 = select(a_844,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f36,hypothesis,
    e_847 = select(a_844,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f37,hypothesis,
    e_849 = select(a_848,i1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f38,hypothesis,
    e_852 = select(a_851,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f39,hypothesis,
    e_854 = select(a_851,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f40,hypothesis,
    e_856 = select(a_855,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f41,hypothesis,
    e_858 = select(a_855,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f42,hypothesis,
    e_862 = select(a_861,i0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f43,hypothesis,
    e_864 = select(a_861,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f44,hypothesis,
    e_866 = select(a_865,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f45,hypothesis,
    e_868 = select(a_865,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f46,hypothesis,
    e_870 = select(a_869,i1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f47,hypothesis,
    e_873 = select(a_872,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f48,hypothesis,
    e_875 = select(a_872,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f49,hypothesis,
    e_877 = select(a_876,i2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f50,hypothesis,
    e_879 = select(a_876,i5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f51,hypothesis,
    e_882 = select(a_859,i_881),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f52,hypothesis,
    e_883 = select(a_880,i_881),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f54,negated_conjecture,
    e_882 != e_883,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f55,plain,
    ! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
    inference(cnf_transformation,[status(thm)],[f1]) ).

fof(f56,plain,
    ! [I,J] :
      ( ! [A,E] : select(store(A,I,E),J) = select(A,J)
      | I = J ),
    inference(miniscoping,[status(thm)],[f2]) ).

fof(f57,plain,
    ! [X0,X1,X2,X3] :
      ( select(store(X2,X0,X3),X1) = select(X2,X1)
      | X0 = X1 ),
    inference(cnf_transformation,[status(thm)],[f56]) ).

fof(f60,plain,
    a_838 = store(a_836,i2,e_837),
    inference(cnf_transformation,[status(thm)],[f5]) ).

fof(f61,plain,
    a_840 = store(a_838,i1,e_839),
    inference(cnf_transformation,[status(thm)],[f6]) ).

fof(f62,plain,
    a_842 = store(a_840,i0,e_841),
    inference(cnf_transformation,[status(thm)],[f7]) ).

fof(f63,plain,
    a_844 = store(a_842,i5,e_843),
    inference(cnf_transformation,[status(thm)],[f8]) ).

fof(f64,plain,
    a_846 = store(a_844,i2,e_845),
    inference(cnf_transformation,[status(thm)],[f9]) ).

fof(f65,plain,
    a_848 = store(a_846,i5,e_847),
    inference(cnf_transformation,[status(thm)],[f10]) ).

fof(f66,plain,
    a_850 = store(a_848,i1,e_849),
    inference(cnf_transformation,[status(thm)],[f11]) ).

fof(f67,plain,
    a_851 = store(a_850,i1,e_849),
    inference(cnf_transformation,[status(thm)],[f12]) ).

fof(f68,plain,
    a_853 = store(a_851,i5,e_852),
    inference(cnf_transformation,[status(thm)],[f13]) ).

fof(f69,plain,
    a_855 = store(a_853,i2,e_854),
    inference(cnf_transformation,[status(thm)],[f14]) ).

fof(f70,plain,
    a_857 = store(a_855,i5,e_856),
    inference(cnf_transformation,[status(thm)],[f15]) ).

fof(f71,plain,
    a_859 = store(a_857,i2,e_858),
    inference(cnf_transformation,[status(thm)],[f16]) ).

fof(f72,plain,
    a_860 = store(a_836,i1,e_839),
    inference(cnf_transformation,[status(thm)],[f17]) ).

fof(f73,plain,
    a_861 = store(a_860,i2,e_837),
    inference(cnf_transformation,[status(thm)],[f18]) ).

fof(f74,plain,
    a_863 = store(a_861,i5,e_862),
    inference(cnf_transformation,[status(thm)],[f19]) ).

fof(f75,plain,
    a_865 = store(a_863,i0,e_864),
    inference(cnf_transformation,[status(thm)],[f20]) ).

fof(f76,plain,
    a_867 = store(a_865,i5,e_866),
    inference(cnf_transformation,[status(thm)],[f21]) ).

fof(f77,plain,
    a_869 = store(a_867,i2,e_868),
    inference(cnf_transformation,[status(thm)],[f22]) ).

fof(f78,plain,
    a_871 = store(a_869,i1,e_870),
    inference(cnf_transformation,[status(thm)],[f23]) ).

fof(f79,plain,
    a_872 = store(a_871,i1,e_870),
    inference(cnf_transformation,[status(thm)],[f24]) ).

fof(f80,plain,
    a_874 = store(a_872,i5,e_873),
    inference(cnf_transformation,[status(thm)],[f25]) ).

fof(f81,plain,
    a_876 = store(a_874,i2,e_875),
    inference(cnf_transformation,[status(thm)],[f26]) ).

fof(f82,plain,
    a_878 = store(a_876,i5,e_877),
    inference(cnf_transformation,[status(thm)],[f27]) ).

fof(f83,plain,
    a_880 = store(a_878,i2,e_879),
    inference(cnf_transformation,[status(thm)],[f28]) ).

fof(f86,plain,
    e_837 = select(a_836,i1),
    inference(cnf_transformation,[status(thm)],[f31]) ).

fof(f87,plain,
    e_839 = select(a_836,i2),
    inference(cnf_transformation,[status(thm)],[f32]) ).

fof(f88,plain,
    e_841 = select(a_840,i5),
    inference(cnf_transformation,[status(thm)],[f33]) ).

fof(f89,plain,
    e_843 = select(a_840,i0),
    inference(cnf_transformation,[status(thm)],[f34]) ).

fof(f90,plain,
    e_845 = select(a_844,i5),
    inference(cnf_transformation,[status(thm)],[f35]) ).

fof(f91,plain,
    e_847 = select(a_844,i2),
    inference(cnf_transformation,[status(thm)],[f36]) ).

fof(f92,plain,
    e_849 = select(a_848,i1),
    inference(cnf_transformation,[status(thm)],[f37]) ).

fof(f93,plain,
    e_852 = select(a_851,i2),
    inference(cnf_transformation,[status(thm)],[f38]) ).

fof(f94,plain,
    e_854 = select(a_851,i5),
    inference(cnf_transformation,[status(thm)],[f39]) ).

fof(f95,plain,
    e_856 = select(a_855,i2),
    inference(cnf_transformation,[status(thm)],[f40]) ).

fof(f96,plain,
    e_858 = select(a_855,i5),
    inference(cnf_transformation,[status(thm)],[f41]) ).

fof(f97,plain,
    e_862 = select(a_861,i0),
    inference(cnf_transformation,[status(thm)],[f42]) ).

fof(f98,plain,
    e_864 = select(a_861,i5),
    inference(cnf_transformation,[status(thm)],[f43]) ).

fof(f99,plain,
    e_866 = select(a_865,i2),
    inference(cnf_transformation,[status(thm)],[f44]) ).

fof(f100,plain,
    e_868 = select(a_865,i5),
    inference(cnf_transformation,[status(thm)],[f45]) ).

fof(f101,plain,
    e_870 = select(a_869,i1),
    inference(cnf_transformation,[status(thm)],[f46]) ).

fof(f102,plain,
    e_873 = select(a_872,i2),
    inference(cnf_transformation,[status(thm)],[f47]) ).

fof(f103,plain,
    e_875 = select(a_872,i5),
    inference(cnf_transformation,[status(thm)],[f48]) ).

fof(f104,plain,
    e_877 = select(a_876,i2),
    inference(cnf_transformation,[status(thm)],[f49]) ).

fof(f105,plain,
    e_879 = select(a_876,i5),
    inference(cnf_transformation,[status(thm)],[f50]) ).

fof(f106,plain,
    e_882 = select(a_859,i_881),
    inference(cnf_transformation,[status(thm)],[f51]) ).

fof(f107,plain,
    e_883 = select(a_880,i_881),
    inference(cnf_transformation,[status(thm)],[f52]) ).

fof(f109,plain,
    e_882 != e_883,
    inference(cnf_transformation,[status(thm)],[f54]) ).

fof(f116,plain,
    ! [X0] :
      ( select(a_838,X0) = select(a_836,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f60,f57]) ).

fof(f117,plain,
    select(a_838,i2) = e_837,
    inference(paramodulation,[status(thm)],[f60,f55]) ).

fof(f118,plain,
    ! [X0] :
      ( select(a_840,X0) = select(a_838,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f61,f57]) ).

fof(f119,plain,
    select(a_840,i1) = e_839,
    inference(paramodulation,[status(thm)],[f61,f55]) ).

fof(f120,plain,
    ! [X0] :
      ( select(a_842,X0) = select(a_840,X0)
      | i0 = X0 ),
    inference(paramodulation,[status(thm)],[f62,f57]) ).

fof(f121,plain,
    select(a_842,i0) = e_841,
    inference(paramodulation,[status(thm)],[f62,f55]) ).

fof(f122,plain,
    ! [X0] :
      ( select(a_844,X0) = select(a_842,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f63,f57]) ).

fof(f123,plain,
    select(a_844,i5) = e_843,
    inference(paramodulation,[status(thm)],[f63,f55]) ).

fof(f124,plain,
    e_845 = e_843,
    inference(forward_demodulation,[status(thm)],[f90,f123]) ).

fof(f125,plain,
    e_843 = select(a_844,i5),
    inference(backward_demodulation,[status(thm)],[f124,f90]) ).

fof(f126,plain,
    a_846 = store(a_844,i2,e_843),
    inference(forward_demodulation,[status(thm)],[f124,f64]) ).

fof(f127,plain,
    ! [X0] :
      ( select(a_846,X0) = select(a_844,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f126,f57]) ).

fof(f128,plain,
    select(a_846,i2) = e_843,
    inference(paramodulation,[status(thm)],[f126,f55]) ).

fof(f129,plain,
    ! [X0] :
      ( select(a_848,X0) = select(a_846,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f65,f57]) ).

fof(f130,plain,
    select(a_848,i5) = e_847,
    inference(paramodulation,[status(thm)],[f65,f55]) ).

fof(f131,plain,
    ! [X0] :
      ( select(a_850,X0) = select(a_848,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f66,f57]) ).

fof(f133,plain,
    ! [X0] :
      ( select(a_851,X0) = select(a_850,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f67,f57]) ).

fof(f134,plain,
    select(a_851,i1) = e_849,
    inference(paramodulation,[status(thm)],[f67,f55]) ).

fof(f135,plain,
    ! [X0] :
      ( select(a_853,X0) = select(a_851,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f68,f57]) ).

fof(f136,plain,
    select(a_853,i5) = e_852,
    inference(paramodulation,[status(thm)],[f68,f55]) ).

fof(f137,plain,
    ! [X0] :
      ( select(a_855,X0) = select(a_853,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f69,f57]) ).

fof(f138,plain,
    select(a_855,i2) = e_854,
    inference(paramodulation,[status(thm)],[f69,f55]) ).

fof(f139,plain,
    e_856 = e_854,
    inference(forward_demodulation,[status(thm)],[f95,f138]) ).

fof(f140,plain,
    e_854 = select(a_855,i2),
    inference(backward_demodulation,[status(thm)],[f139,f95]) ).

fof(f141,plain,
    a_857 = store(a_855,i5,e_854),
    inference(forward_demodulation,[status(thm)],[f139,f70]) ).

fof(f142,plain,
    ! [X0] :
      ( select(a_857,X0) = select(a_855,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f141,f57]) ).

fof(f143,plain,
    select(a_857,i5) = e_854,
    inference(paramodulation,[status(thm)],[f141,f55]) ).

fof(f144,plain,
    ! [X0] :
      ( select(a_859,X0) = select(a_857,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f71,f57]) ).

fof(f145,plain,
    select(a_859,i2) = e_858,
    inference(paramodulation,[status(thm)],[f71,f55]) ).

fof(f146,plain,
    ! [X0] :
      ( select(a_860,X0) = select(a_836,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f72,f57]) ).

fof(f147,plain,
    select(a_860,i1) = e_839,
    inference(paramodulation,[status(thm)],[f72,f55]) ).

fof(f148,plain,
    ! [X0] :
      ( select(a_861,X0) = select(a_860,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f73,f57]) ).

fof(f149,plain,
    select(a_861,i2) = e_837,
    inference(paramodulation,[status(thm)],[f73,f55]) ).

fof(f150,plain,
    ! [X0] :
      ( select(a_863,X0) = select(a_861,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f74,f57]) ).

fof(f151,plain,
    select(a_863,i5) = e_862,
    inference(paramodulation,[status(thm)],[f74,f55]) ).

fof(f152,plain,
    ! [X0] :
      ( select(a_865,X0) = select(a_863,X0)
      | i0 = X0 ),
    inference(paramodulation,[status(thm)],[f75,f57]) ).

fof(f153,plain,
    select(a_865,i0) = e_864,
    inference(paramodulation,[status(thm)],[f75,f55]) ).

fof(f154,plain,
    ! [X0] :
      ( select(a_867,X0) = select(a_865,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f76,f57]) ).

fof(f155,plain,
    select(a_867,i5) = e_866,
    inference(paramodulation,[status(thm)],[f76,f55]) ).

fof(f156,plain,
    ! [X0] :
      ( select(a_869,X0) = select(a_867,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f77,f57]) ).

fof(f157,plain,
    select(a_869,i2) = e_868,
    inference(paramodulation,[status(thm)],[f77,f55]) ).

fof(f158,plain,
    ! [X0] :
      ( select(a_871,X0) = select(a_869,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f78,f57]) ).

fof(f160,plain,
    ! [X0] :
      ( select(a_872,X0) = select(a_871,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f79,f57]) ).

fof(f161,plain,
    select(a_872,i1) = e_870,
    inference(paramodulation,[status(thm)],[f79,f55]) ).

fof(f162,plain,
    ! [X0] :
      ( select(a_874,X0) = select(a_872,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f80,f57]) ).

fof(f163,plain,
    select(a_874,i5) = e_873,
    inference(paramodulation,[status(thm)],[f80,f55]) ).

fof(f164,plain,
    ! [X0] :
      ( select(a_876,X0) = select(a_874,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f81,f57]) ).

fof(f165,plain,
    select(a_876,i2) = e_875,
    inference(paramodulation,[status(thm)],[f81,f55]) ).

fof(f166,plain,
    e_877 = e_875,
    inference(forward_demodulation,[status(thm)],[f104,f165]) ).

fof(f167,plain,
    e_875 = select(a_876,i2),
    inference(backward_demodulation,[status(thm)],[f166,f104]) ).

fof(f168,plain,
    a_878 = store(a_876,i5,e_875),
    inference(forward_demodulation,[status(thm)],[f166,f82]) ).

fof(f169,plain,
    ! [X0] :
      ( select(a_878,X0) = select(a_876,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f168,f57]) ).

fof(f170,plain,
    select(a_878,i5) = e_875,
    inference(paramodulation,[status(thm)],[f168,f55]) ).

fof(f171,plain,
    ! [X0] :
      ( select(a_880,X0) = select(a_878,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f83,f57]) ).

fof(f172,plain,
    select(a_880,i2) = e_879,
    inference(paramodulation,[status(thm)],[f83,f55]) ).

fof(f192,plain,
    ( e_843 = select(a_838,i0)
    | i1 = i0 ),
    inference(paramodulation,[status(thm)],[f89,f118]) ).

fof(f193,plain,
    ( e_841 = select(a_838,i5)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f88,f118]) ).

fof(f197,plain,
    ( select(a_842,i1) = e_839
    | i0 = i1 ),
    inference(paramodulation,[status(thm)],[f119,f120]) ).

fof(f200,plain,
    ! [X0] :
      ( i1 = X0
      | select(a_842,X0) = select(a_838,X0)
      | i0 = X0 ),
    inference(paramodulation,[status(thm)],[f118,f120]) ).

fof(f206,plain,
    ( e_847 = select(a_842,i2)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f91,f122]) ).

fof(f211,plain,
    ! [X0] :
      ( i5 = X0
      | select(a_846,X0) = select(a_842,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f122,f127]) ).

fof(f216,plain,
    ( e_849 = select(a_846,i1)
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f92,f129]) ).

fof(f219,plain,
    ( select(a_850,i5) = e_847
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f130,f131]) ).

fof(f221,plain,
    ! [X0] :
      ( i5 = X0
      | select(a_850,X0) = select(a_846,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f129,f131]) ).

fof(f226,plain,
    ( e_854 = select(a_850,i5)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f94,f133]) ).

fof(f227,plain,
    ( e_852 = select(a_850,i2)
    | i1 = i2 ),
    inference(paramodulation,[status(thm)],[f93,f133]) ).

fof(f231,plain,
    ( select(a_853,i1) = e_849
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f134,f135]) ).

fof(f234,plain,
    ! [X0] :
      ( i1 = X0
      | select(a_853,X0) = select(a_850,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f133,f135]) ).

fof(f240,plain,
    ( e_858 = select(a_853,i5)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f96,f137]) ).

fof(f243,plain,
    ( e_858 = e_852
    | i2 = i5 ),
    inference(forward_demodulation,[status(thm)],[f136,f240]) ).

fof(f245,plain,
    ( i2 = i5
    | a_859 = store(a_857,i2,e_852) ),
    inference(paramodulation,[status(thm)],[f243,f71]) ).

fof(f248,plain,
    ! [X0] :
      ( i2 = X0
      | select(a_857,X0) = select(a_853,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f137,f142]) ).

fof(f253,plain,
    ( e_882 = select(a_857,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f106,f144]) ).

fof(f259,plain,
    ! [X0] :
      ( i2 = X0
      | select(a_860,X0) = select(a_838,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f116,f146]) ).

fof(f267,plain,
    ( e_864 = select(a_860,i5)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f98,f148]) ).

fof(f268,plain,
    ( e_862 = select(a_860,i0)
    | i2 = i0 ),
    inference(paramodulation,[status(thm)],[f97,f148]) ).

fof(f272,plain,
    ( select(a_863,i2) = e_837
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f149,f150]) ).

fof(f275,plain,
    ! [X0] :
      ( i2 = X0
      | select(a_863,X0) = select(a_860,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f148,f150]) ).

fof(f281,plain,
    ( e_868 = select(a_863,i5)
    | i0 = i5 ),
    inference(paramodulation,[status(thm)],[f100,f152]) ).

fof(f282,plain,
    ( e_866 = select(a_863,i2)
    | i0 = i2 ),
    inference(paramodulation,[status(thm)],[f99,f152]) ).

fof(f286,plain,
    ( e_868 = e_862
    | i0 = i5 ),
    inference(forward_demodulation,[status(thm)],[f151,f281]) ).

fof(f288,plain,
    ( i0 = i5
    | a_869 = store(a_867,i2,e_862) ),
    inference(paramodulation,[status(thm)],[f286,f77]) ).

fof(f289,plain,
    ( select(a_867,i0) = e_864
    | i5 = i0 ),
    inference(paramodulation,[status(thm)],[f153,f154]) ).

fof(f292,plain,
    ! [X0] :
      ( i0 = X0
      | select(a_867,X0) = select(a_863,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f152,f154]) ).

fof(f298,plain,
    ( e_870 = select(a_867,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f101,f156]) ).

fof(f301,plain,
    ( i1 = i5
    | e_854 = e_847
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f219,f226]) ).

fof(f303,plain,
    ( e_854 = e_847
    | i1 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f301]) ).

fof(f305,plain,
    ( i1 = i5
    | a_857 = store(a_855,i5,e_847) ),
    inference(paramodulation,[status(thm)],[f303,f141]) ).

fof(f307,plain,
    ( select(a_871,i2) = e_868
    | i1 = i2 ),
    inference(paramodulation,[status(thm)],[f157,f158]) ).

fof(f309,plain,
    ! [X0] :
      ( i2 = X0
      | select(a_871,X0) = select(a_867,X0)
      | i1 = X0 ),
    inference(paramodulation,[status(thm)],[f156,f158]) ).

fof(f314,plain,
    ( e_875 = select(a_871,i5)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f103,f160]) ).

fof(f315,plain,
    ( e_873 = select(a_871,i2)
    | i1 = i2 ),
    inference(paramodulation,[status(thm)],[f102,f160]) ).

fof(f319,plain,
    ( select(a_874,i1) = e_870
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f161,f162]) ).

fof(f322,plain,
    ! [X0] :
      ( i1 = X0
      | select(a_874,X0) = select(a_871,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f160,f162]) ).

fof(f328,plain,
    ( e_879 = select(a_874,i5)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f105,f164]) ).

fof(f331,plain,
    ( e_879 = e_873
    | i2 = i5 ),
    inference(forward_demodulation,[status(thm)],[f163,f328]) ).

fof(f336,plain,
    ! [X0] :
      ( i2 = X0
      | select(a_878,X0) = select(a_874,X0)
      | i5 = X0 ),
    inference(paramodulation,[status(thm)],[f164,f169]) ).

fof(f341,plain,
    ( e_883 = select(a_878,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f107,f171]) ).

fof(f356,plain,
    ( i5 = i2
    | i1 = i2
    | e_847 = select(a_838,i2)
    | i0 = i2 ),
    inference(paramodulation,[status(thm)],[f206,f200]) ).

fof(f364,plain,
    ( i5 = i2
    | i1 = i2
    | e_847 = e_837
    | i0 = i2 ),
    inference(forward_demodulation,[status(thm)],[f117,f356]) ).

fof(f368,plain,
    ( i5 = i1
    | i5 = i1
    | e_849 = select(a_842,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f216,f211]) ).

fof(f374,plain,
    ( i5 = i1
    | e_849 = select(a_842,i1)
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f368]) ).

fof(f376,plain,
    ( i5 = i2
    | e_866 = e_837
    | i0 = i2 ),
    inference(paramodulation,[status(thm)],[f272,f282]) ).

fof(f378,plain,
    ( i1 = i2
    | i5 = i2
    | e_852 = select(a_846,i2)
    | i1 = i2 ),
    inference(paramodulation,[status(thm)],[f227,f221]) ).

fof(f386,plain,
    ( i1 = i2
    | i5 = i2
    | e_852 = e_843
    | i1 = i2 ),
    inference(forward_demodulation,[status(thm)],[f128,f378]) ).

fof(f387,plain,
    ( i5 = i2
    | e_852 = e_843
    | i1 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f386]) ).

fof(f399,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_882 = select(a_853,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f253,f248]) ).

fof(f404,plain,
    ( i2 = i_881
    | e_882 = select(a_853,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f399]) ).

fof(f406,plain,
    ( i1 = i_881
    | i5 = i_881
    | i2 = i_881
    | e_882 = select(a_850,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f234,f404]) ).

fof(f408,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_882 = select(a_850,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f406]) ).

fof(f410,plain,
    ( i1 = i2
    | e_873 = e_868
    | i1 = i2 ),
    inference(paramodulation,[status(thm)],[f307,f315]) ).

fof(f412,plain,
    ( e_873 = e_868
    | i1 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f410]) ).

fof(f414,plain,
    ( i1 = i2
    | a_874 = store(a_872,i5,e_868) ),
    inference(paramodulation,[status(thm)],[f412,f80]) ).

fof(f415,plain,
    ( i2 = i0
    | i2 = i0
    | e_862 = select(a_838,i0)
    | i1 = i0 ),
    inference(paramodulation,[status(thm)],[f268,f259]) ).

fof(f416,plain,
    ( i2 = i5
    | i2 = i5
    | e_864 = select(a_838,i5)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f267,f259]) ).

fof(f425,plain,
    ( i2 = i0
    | e_862 = select(a_838,i0)
    | i1 = i0 ),
    inference(duplicate_literals_removal,[status(thm)],[f415]) ).

fof(f426,plain,
    ( i2 = i5
    | e_864 = select(a_838,i5)
    | i1 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f416]) ).

fof(f447,plain,
    ( i5 = i_881
    | i1 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_846,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f221,f408]) ).

fof(f449,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_882 = select(a_846,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f447]) ).

fof(f451,plain,
    ( i5 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_842,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f211,f449]) ).

fof(f453,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_882 = select(a_842,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f451]) ).

fof(f455,plain,
    ( i1 = i_881
    | i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_838,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f200,f453]) ).

fof(f457,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_838,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f455]) ).

fof(f475,plain,
    ( i2 = i1
    | i0 = i1
    | e_870 = select(a_863,i1)
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f298,f292]) ).

fof(f486,plain,
    ( i5 = i2
    | i1 = i2
    | i2 = i5
    | a_859 = store(a_857,i2,e_843) ),
    inference(paramodulation,[status(thm)],[f387,f245]) ).

fof(f489,plain,
    ( i1 = i2
    | i2 = i5
    | a_859 = store(a_857,i2,e_843) ),
    inference(duplicate_literals_removal,[status(thm)],[f486]) ).

fof(f500,plain,
    ( i1 = i5
    | i2 = i5
    | e_875 = select(a_867,i5)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f314,f309]) ).

fof(f508,plain,
    ( i1 = i5
    | i2 = i5
    | e_875 = e_866
    | i1 = i5 ),
    inference(forward_demodulation,[status(thm)],[f155,f500]) ).

fof(f509,plain,
    ( i2 = i5
    | e_875 = e_866
    | i1 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f508]) ).

fof(f520,plain,
    ( i2 = i5
    | i1 = i5
    | a_878 = store(a_876,i5,e_866) ),
    inference(paramodulation,[status(thm)],[f509,f168]) ).

fof(f526,plain,
    ( i0 = i5
    | i1 = i2
    | a_874 = store(a_872,i5,e_862) ),
    inference(paramodulation,[status(thm)],[f286,f414]) ).

fof(f531,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_883 = select(a_874,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f341,f336]) ).

fof(f536,plain,
    ( i2 = i_881
    | e_883 = select(a_874,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f531]) ).

fof(f538,plain,
    ( i1 = i_881
    | i5 = i_881
    | i2 = i_881
    | e_883 = select(a_871,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f322,f536]) ).

fof(f540,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_883 = select(a_871,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f538]) ).

fof(f542,plain,
    ( i2 = i_881
    | i1 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_867,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f309,f540]) ).

fof(f544,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_883 = select(a_867,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f542]) ).

fof(f546,plain,
    ( i5 = i2
    | i0 = i2
    | i5 = i2
    | i1 = i2
    | e_847 = e_866
    | i0 = i2 ),
    inference(paramodulation,[status(thm)],[f376,f364]) ).

fof(f550,plain,
    ( i5 = i2
    | i1 = i2
    | e_847 = e_866
    | i0 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f546]) ).

fof(f556,plain,
    ( i1 = i0
    | i2 = i0
    | e_862 = e_843
    | i1 = i0 ),
    inference(paramodulation,[status(thm)],[f192,f425]) ).

fof(f560,plain,
    ( i2 = i0
    | e_862 = e_843
    | i1 = i0 ),
    inference(duplicate_literals_removal,[status(thm)],[f556]) ).

fof(f564,plain,
    ( i0 = i_881
    | i5 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_863,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f292,f544]) ).

fof(f566,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_863,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f564]) ).

fof(f568,plain,
    ( i2 = i_881
    | i5 = i_881
    | i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_860,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f275,f566]) ).

fof(f570,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_860,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f568]) ).

fof(f573,plain,
    ( i2 = i_881
    | i1 = i_881
    | i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_838,i_881)
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f259,f570]) ).

fof(f577,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_838,i_881)
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f573]) ).

fof(f586,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = e_882
    | i5 = i_881 ),
    inference(paramodulation,[status(thm)],[f457,f577]) ).

fof(f590,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = e_882
    | i5 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f586]) ).

fof(f591,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f590,f109]) ).

fof(f596,plain,
    ( i2 = i0
    | i1 = i0
    | i0 = i5
    | a_869 = store(a_867,i2,e_843) ),
    inference(paramodulation,[status(thm)],[f560,f288]) ).

fof(f598,plain,
    ( i1 = i5
    | i2 = i5
    | e_864 = e_841
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f193,f426]) ).

fof(f602,plain,
    ( i2 = i5
    | e_864 = e_841
    | i1 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f598]) ).

fof(f618,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | select(a_865,i_881) = e_864 ),
    inference(paramodulation,[status(thm)],[f591,f153]) ).

fof(f620,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | select(a_842,i_881) = e_841 ),
    inference(paramodulation,[status(thm)],[f591,f121]) ).

fof(f624,plain,
    ( i5 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | select(a_867,i_881) = e_864 ),
    inference(paramodulation,[status(thm)],[f154,f618]) ).

fof(f628,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | select(a_867,i_881) = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f624]) ).

fof(f630,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_841 ),
    inference(paramodulation,[status(thm)],[f453,f620]) ).

fof(f634,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f630]) ).

fof(f664,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_864 ),
    inference(paramodulation,[status(thm)],[f544,f628]) ).

fof(f668,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f664]) ).

fof(f672,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_882 != e_864 ),
    inference(paramodulation,[status(thm)],[f668,f109]) ).

fof(f673,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_841 != e_864 ),
    inference(paramodulation,[status(thm)],[f634,f672]) ).

fof(f674,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | e_841 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f673]) ).

fof(f683,plain,
    ( i2 = i5
    | i1 = i5
    | i1 = i_881
    | i2 = i_881
    | i5 = i_881 ),
    inference(resolution,[status(thm)],[f674,f602]) ).

fof(f695,plain,
    ( i1 = i2
    | i2 = i5
    | select(a_859,i2) = e_843 ),
    inference(paramodulation,[status(thm)],[f489,f55]) ).

fof(f696,plain,
    ( i1 = i2
    | i2 = i5
    | e_858 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f145,f695]) ).

fof(f702,plain,
    ( i5 = i2
    | i1 = i2
    | i0 = i2
    | i2 = i5
    | i1 = i5
    | a_878 = store(a_876,i5,e_847) ),
    inference(paramodulation,[status(thm)],[f550,f520]) ).

fof(f705,plain,
    ( i1 = i2
    | i0 = i2
    | i2 = i5
    | i1 = i5
    | a_878 = store(a_876,i5,e_847) ),
    inference(duplicate_literals_removal,[status(thm)],[f702]) ).

fof(f707,plain,
    ( i2 = i1
    | i5 = i1
    | i2 = i1
    | i0 = i1
    | e_870 = select(a_860,i1)
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f275,f475]) ).

fof(f709,plain,
    ( i2 = i1
    | i5 = i1
    | i2 = i1
    | i0 = i1
    | e_870 = e_839
    | i5 = i1 ),
    inference(forward_demodulation,[status(thm)],[f147,f707]) ).

fof(f710,plain,
    ( i2 = i1
    | i0 = i1
    | e_870 = e_839
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f709]) ).

fof(f751,plain,
    ( i0 = i5
    | i1 = i2
    | select(a_874,i5) = e_862 ),
    inference(paramodulation,[status(thm)],[f526,f55]) ).

fof(f752,plain,
    ( i0 = i5
    | i1 = i2
    | e_873 = e_862 ),
    inference(forward_demodulation,[status(thm)],[f163,f751]) ).

fof(f767,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | select(a_874,i_881) = e_870
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f683,f319]) ).

fof(f769,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | select(a_853,i_881) = e_849
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f683,f231]) ).

fof(f770,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = select(a_846,i_881)
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f683,f216]) ).

fof(f771,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | select(a_842,i_881) = e_839
    | i0 = i1 ),
    inference(paramodulation,[status(thm)],[f683,f197]) ).

fof(f792,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | select(a_874,i_881) = e_870
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f767]) ).

fof(f793,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | select(a_853,i_881) = e_849
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f769]) ).

fof(f794,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = select(a_846,i_881)
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f770]) ).

fof(f821,plain,
    ( i2 = i0
    | i1 = i0
    | i0 = i5
    | select(a_869,i2) = e_843 ),
    inference(paramodulation,[status(thm)],[f596,f55]) ).

fof(f822,plain,
    ( i2 = i0
    | i1 = i0
    | i0 = i5
    | e_868 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f157,f821]) ).

fof(f992,plain,
    ( i1 = i2
    | i0 = i2
    | i2 = i5
    | i1 = i5
    | select(a_878,i5) = e_847 ),
    inference(paramodulation,[status(thm)],[f705,f55]) ).

fof(f993,plain,
    ( i1 = i2
    | i0 = i2
    | i2 = i5
    | i1 = i5
    | e_875 = e_847 ),
    inference(forward_demodulation,[status(thm)],[f170,f992]) ).

fof(f1044,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_870
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f536,f792]) ).

fof(f1048,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_870
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1044]) ).

fof(f1052,plain,
    ( i2 = i1
    | i0 = i1
    | i5 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_839
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f710,f1048]) ).

fof(f1056,plain,
    ( i2 = i1
    | i0 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_839
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1052]) ).

fof(f1058,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_849
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f404,f793]) ).

fof(f1062,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_849
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1058]) ).

fof(f1089,plain,
    ( i5 = i_881
    | i2 = i_881
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = select(a_842,i_881)
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f211,f794]) ).

fof(f1093,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = select(a_842,i_881)
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1089]) ).

fof(f1581,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = e_839
    | i0 = i1 ),
    inference(paramodulation,[status(thm)],[f1093,f771]) ).

fof(f1591,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | e_849 = e_839
    | i0 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1581]) ).

fof(f1598,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_839
    | i0 = i1 ),
    inference(paramodulation,[status(thm)],[f1062,f1591]) ).

fof(f1607,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | e_882 = e_839
    | i0 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1598]) ).

fof(f1657,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881
    | i0 = i1
    | i2 = i1
    | i0 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_882
    | i5 = i1 ),
    inference(paramodulation,[status(thm)],[f1607,f1056]) ).

fof(f1671,plain,
    ( i2 = i1
    | i0 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | e_883 = e_882
    | i5 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1657]) ).

fof(f1672,plain,
    ( i2 = i1
    | i0 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1 ),
    inference(forward_subsumption_resolution,[status(thm)],[f1671,f109]) ).

fof(f1702,plain,
    ( i2 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i5 = i1
    | e_849 = select(a_842,i0)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f1672,f374]) ).

fof(f1704,plain,
    ( i2 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_870 = select(a_867,i0)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f1672,f298]) ).

fof(f1725,plain,
    ( i1 = i5
    | i0 != i5
    | i2 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881 ),
    inference(equality_factoring,[status(thm)],[f1672]) ).

fof(f1745,plain,
    ( i2 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i5 = i1
    | e_849 = e_841
    | i2 = i1 ),
    inference(forward_demodulation,[status(thm)],[f121,f1702]) ).

fof(f1746,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_849 = e_841
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1745]) ).

fof(f1748,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_870 = select(a_867,i0)
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1704]) ).

fof(f1773,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_882 = e_841
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f1062,f1746]) ).

fof(f1785,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_882 = e_841
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f1773]) ).

fof(f2063,plain,
    ( i5 = i0
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_870 = e_864
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f289,f1748]) ).

fof(f2071,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_870 = e_864
    | i2 = i1 ),
    inference(forward_subsumption_resolution,[status(thm)],[f2063,f1725]) ).

fof(f2096,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_883 = e_864
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f1048,f2071]) ).

fof(f2106,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | e_883 = e_864
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f2096]) ).

fof(f2139,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i1
    | e_882 != e_864 ),
    inference(paramodulation,[status(thm)],[f2106,f109]) ).

fof(f2164,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i1
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i1
    | e_841 != e_864 ),
    inference(paramodulation,[status(thm)],[f1785,f2139]) ).

fof(f2166,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i1
    | e_841 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f2164]) ).

fof(f2167,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i5 = i1
    | i2 = i1 ),
    inference(forward_subsumption_resolution,[status(thm)],[f2166,f602]) ).

fof(f2188,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_864 = select(a_860,i1)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f2167,f267]) ).

fof(f2216,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_841 = select(a_840,i1) ),
    inference(paramodulation,[status(thm)],[f2167,f88]) ).

fof(f2217,plain,
    ( i5 = i_881
    | i1 != i_881
    | i2 = i5
    | i2 = i_881
    | i2 = i1 ),
    inference(equality_factoring,[status(thm)],[f2167]) ).

fof(f2236,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_864 = e_839
    | i2 = i5 ),
    inference(forward_demodulation,[status(thm)],[f147,f2188]) ).

fof(f2237,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_864 = e_839
    | i2 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f2236]) ).

fof(f2244,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_841 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f119,f2216]) ).

fof(f2363,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i1
    | i2 = i5
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_841 = e_864 ),
    inference(paramodulation,[status(thm)],[f2237,f2244]) ).

fof(f2381,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1
    | e_841 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f2363]) ).

fof(f2429,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1 ),
    inference(resolution,[status(thm)],[f2381,f674]) ).

fof(f2435,plain,
    ( i1 = i_881
    | i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f2429]) ).

fof(f2436,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881
    | i2 = i1 ),
    inference(forward_subsumption_resolution,[status(thm)],[f2435,f2217]) ).

fof(f2501,plain,
    ( i2 = i_881
    | i1 != i_881
    | i2 = i5
    | i5 = i_881 ),
    inference(equality_factoring,[status(thm)],[f2436]) ).

fof(f2502,plain,
    ( i2 = i5
    | i1 != i5
    | i2 = i_881
    | i5 = i_881 ),
    inference(equality_factoring,[status(thm)],[f2436]) ).

fof(f2630,plain,
    ( i2 = i5
    | i1 = i5
    | i2 = i_881
    | i5 = i_881 ),
    inference(backward_subsumption_resolution,[status(thm)],[f683,f2501]) ).

fof(f2715,plain,
    ( i2 = i5
    | i2 = i_881
    | i5 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f2630,f2502]) ).

fof(f2725,plain,
    ( i2 = i5
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | a_878 = store(a_876,i_881,e_866) ),
    inference(paramodulation,[status(thm)],[f2715,f520]) ).

fof(f2731,plain,
    ( i2 = i5
    | i2 = i_881
    | i1 = i5
    | a_857 = store(a_855,i_881,e_847) ),
    inference(paramodulation,[status(thm)],[f2715,f305]) ).

fof(f2733,plain,
    ( i2 = i5
    | i2 = i_881
    | e_864 = select(a_860,i_881)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f2715,f267]) ).

fof(f2739,plain,
    ( i2 = i5
    | i2 = i_881
    | select(a_878,i_881) = e_875 ),
    inference(paramodulation,[status(thm)],[f2715,f170]) ).

fof(f2747,plain,
    ( i2 = i5
    | i2 = i_881
    | select(a_857,i_881) = e_854 ),
    inference(paramodulation,[status(thm)],[f2715,f143]) ).

fof(f2761,plain,
    ( i2 = i5
    | i2 = i_881
    | e_841 = select(a_840,i_881) ),
    inference(paramodulation,[status(thm)],[f2715,f88]) ).

fof(f2769,plain,
    ( i2 = i_881
    | i2 = i5
    | i1 = i5
    | a_878 = store(a_876,i_881,e_866) ),
    inference(duplicate_literals_removal,[status(thm)],[f2725]) ).

fof(f2774,plain,
    ( i2 = i_881
    | e_864 = select(a_860,i_881)
    | i2 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f2733]) ).

fof(f2778,plain,
    ( i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_864 = select(a_838,i_881)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f259,f2774]) ).

fof(f2783,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_864 = select(a_838,i_881)
    | i2 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f2778]) ).

fof(f2794,plain,
    ( i2 = i_881
    | i2 = i5
    | i2 = i_881
    | e_883 = e_875 ),
    inference(paramodulation,[status(thm)],[f341,f2739]) ).

fof(f2798,plain,
    ( i2 = i5
    | i2 = i_881
    | e_883 = e_875 ),
    inference(duplicate_literals_removal,[status(thm)],[f2794]) ).

fof(f2804,plain,
    ( i2 = i5
    | i2 = i_881
    | e_882 != e_875 ),
    inference(paramodulation,[status(thm)],[f2798,f109]) ).

fof(f2833,plain,
    ( i2 = i_881
    | i2 = i5
    | i2 = i_881
    | e_882 = e_854 ),
    inference(paramodulation,[status(thm)],[f253,f2747]) ).

fof(f2837,plain,
    ( i2 = i5
    | i2 = i_881
    | e_882 = e_854 ),
    inference(duplicate_literals_removal,[status(thm)],[f2833]) ).

fof(f2842,plain,
    ( i2 = i5
    | i2 = i_881
    | i2 = i5
    | i2 = i_881
    | e_854 != e_875 ),
    inference(paramodulation,[status(thm)],[f2837,f2804]) ).

fof(f2846,plain,
    ( i2 = i5
    | i2 = i_881
    | e_854 != e_875 ),
    inference(duplicate_literals_removal,[status(thm)],[f2842]) ).

fof(f2849,plain,
    ( i1 = i2
    | i0 = i2
    | i2 = i5
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_854 != e_847 ),
    inference(paramodulation,[status(thm)],[f993,f2846]) ).

fof(f2851,plain,
    ( i1 = i2
    | i0 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_854 != e_847 ),
    inference(duplicate_literals_removal,[status(thm)],[f2849]) ).

fof(f2852,plain,
    ( i1 = i2
    | i0 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f2851,f303]) ).

fof(f2913,plain,
    ( i1 = i_881
    | i2 = i5
    | i2 = i_881
    | e_841 = select(a_838,i_881) ),
    inference(paramodulation,[status(thm)],[f118,f2761]) ).

fof(f2993,plain,
    ( i2 = i_881
    | i2 = i5
    | i1 = i5
    | select(a_878,i_881) = e_866 ),
    inference(paramodulation,[status(thm)],[f2769,f55]) ).

fof(f3104,plain,
    ( i2 = i5
    | i2 = i_881
    | i1 = i5
    | select(a_857,i_881) = e_847 ),
    inference(paramodulation,[status(thm)],[f2731,f55]) ).

fof(f3152,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_847 = select(a_842,i0)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f2852,f206]) ).

fof(f3170,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_866 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f2852,f99]) ).

fof(f3204,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(forward_demodulation,[status(thm)],[f121,f3152]) ).

fof(f3205,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f3204]) ).

fof(f3207,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | e_866 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f3170]) ).

fof(f3298,plain,
    ( i1 = i_881
    | i2 = i_881
    | i2 = i5
    | i1 = i_881
    | i2 = i5
    | i2 = i_881
    | e_841 = e_864 ),
    inference(paramodulation,[status(thm)],[f2783,f2913]) ).

fof(f3310,plain,
    ( i1 = i_881
    | i2 = i5
    | i2 = i_881
    | e_841 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f3298]) ).

fof(f3353,plain,
    ( i2 = i_881
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_883 = e_866 ),
    inference(paramodulation,[status(thm)],[f341,f2993]) ).

fof(f3359,plain,
    ( i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_883 = e_866 ),
    inference(duplicate_literals_removal,[status(thm)],[f3353]) ).

fof(f3368,plain,
    ( i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_882 != e_866 ),
    inference(paramodulation,[status(thm)],[f3359,f109]) ).

fof(f3406,plain,
    ( i2 = i_881
    | i2 = i5
    | i2 = i_881
    | i1 = i5
    | e_882 = e_847 ),
    inference(paramodulation,[status(thm)],[f253,f3104]) ).

fof(f3412,plain,
    ( i2 = i5
    | i2 = i_881
    | i1 = i5
    | e_882 = e_847 ),
    inference(duplicate_literals_removal,[status(thm)],[f3406]) ).

fof(f3419,plain,
    ( i2 = i5
    | i2 = i_881
    | i1 = i5
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_866 ),
    inference(paramodulation,[status(thm)],[f3412,f3368]) ).

fof(f3426,plain,
    ( i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_866 ),
    inference(duplicate_literals_removal,[status(thm)],[f3419]) ).

fof(f3489,plain,
    ( i1 = i2
    | i1 = i5
    | i2 = i5
    | i2 = i_881
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_864 ),
    inference(paramodulation,[status(thm)],[f3207,f3426]) ).

fof(f3500,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f3489]) ).

fof(f3606,plain,
    ( i2 = i5
    | i1 = i5
    | i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_841 ),
    inference(paramodulation,[status(thm)],[f602,f3500]) ).

fof(f3609,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i5
    | e_847 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f3606]) ).

fof(f3610,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f3609,f3205]) ).

fof(f3630,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_864 = select(a_860,i1)
    | i2 = i5 ),
    inference(paramodulation,[status(thm)],[f3610,f267]) ).

fof(f3640,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | select(a_867,i1) = e_866 ),
    inference(paramodulation,[status(thm)],[f3610,f155]) ).

fof(f3647,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | select(a_848,i1) = e_847 ),
    inference(paramodulation,[status(thm)],[f3610,f130]) ).

fof(f3652,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_875 = select(a_872,i1) ),
    inference(paramodulation,[status(thm)],[f3610,f103]) ).

fof(f3657,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_854 = select(a_851,i1) ),
    inference(paramodulation,[status(thm)],[f3610,f94]) ).

fof(f3658,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_841 = select(a_840,i1) ),
    inference(paramodulation,[status(thm)],[f3610,f88]) ).

fof(f3677,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_864 = e_839
    | i2 = i5 ),
    inference(forward_demodulation,[status(thm)],[f147,f3630]) ).

fof(f3678,plain,
    ( i1 = i2
    | i2 = i_881
    | e_864 = e_839
    | i2 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f3677]) ).

fof(f3682,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_849 = e_847 ),
    inference(forward_demodulation,[status(thm)],[f92,f3647]) ).

fof(f3683,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_875 = e_870 ),
    inference(forward_demodulation,[status(thm)],[f161,f3652]) ).

fof(f3684,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_854 = e_849 ),
    inference(forward_demodulation,[status(thm)],[f134,f3657]) ).

fof(f3685,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_841 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f119,f3658]) ).

fof(f3821,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_854 = e_847 ),
    inference(paramodulation,[status(thm)],[f3682,f3684]) ).

fof(f3829,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_854 = e_847 ),
    inference(duplicate_literals_removal,[status(thm)],[f3821]) ).

fof(f3835,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_841 = e_864 ),
    inference(paramodulation,[status(thm)],[f3678,f3685]) ).

fof(f3847,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_841 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f3835]) ).

fof(f4098,plain,
    ( i2 = i1
    | i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_870 = e_866 ),
    inference(paramodulation,[status(thm)],[f298,f3640]) ).

fof(f4104,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_870 = e_866 ),
    inference(duplicate_literals_removal,[status(thm)],[f4098]) ).

fof(f4110,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_875 = e_866 ),
    inference(paramodulation,[status(thm)],[f3683,f4104]) ).

fof(f4122,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | e_875 = e_866 ),
    inference(duplicate_literals_removal,[status(thm)],[f4110]) ).

fof(f4158,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i2 = i5
    | i2 = i_881
    | e_854 != e_866 ),
    inference(paramodulation,[status(thm)],[f4122,f2846]) ).

fof(f4166,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_866 ),
    inference(duplicate_literals_removal,[status(thm)],[f4158]) ).

fof(f4192,plain,
    ( i5 = i2
    | i1 = i2
    | i0 = i2
    | i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_847 ),
    inference(paramodulation,[status(thm)],[f550,f4166]) ).

fof(f4193,plain,
    ( i0 = i2
    | i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_847 ),
    inference(duplicate_literals_removal,[status(thm)],[f4192]) ).

fof(f4194,plain,
    ( i0 = i2
    | i1 = i2
    | i2 = i5
    | i2 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f4193,f3829]) ).

fof(f4226,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_847 = select(a_842,i0)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f4194,f206]) ).

fof(f4244,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_866 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f4194,f99]) ).

fof(f4279,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(forward_demodulation,[status(thm)],[f121,f4226]) ).

fof(f4280,plain,
    ( i1 = i2
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f4279]) ).

fof(f4282,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_866 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f4244]) ).

fof(f4311,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_864 ),
    inference(paramodulation,[status(thm)],[f4282,f4166]) ).

fof(f4324,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f4311]) ).

fof(f4346,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_841 ),
    inference(paramodulation,[status(thm)],[f3847,f4324]) ).

fof(f4349,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_854 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f4346]) ).

fof(f4366,plain,
    ( i1 = i2
    | i2 = i_881
    | i2 = i5
    | i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_847 != e_841 ),
    inference(paramodulation,[status(thm)],[f3829,f4349]) ).

fof(f4369,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881
    | e_847 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f4366]) ).

fof(f4370,plain,
    ( i1 = i2
    | i2 = i5
    | i2 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f4369,f4280]) ).

fof(f4401,plain,
    ( i2 = i5
    | i2 = i_881
    | e_847 = select(a_842,i1)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f4370,f206]) ).

fof(f4419,plain,
    ( i2 = i5
    | i2 = i_881
    | e_866 = select(a_865,i1) ),
    inference(paramodulation,[status(thm)],[f4370,f99]) ).

fof(f4423,plain,
    ( i2 = i5
    | i2 = i_881
    | e_839 = select(a_836,i1) ),
    inference(paramodulation,[status(thm)],[f4370,f87]) ).

fof(f4424,plain,
    ( i2 = i_881
    | i1 != i_881
    | i2 = i5 ),
    inference(equality_factoring,[status(thm)],[f4370]) ).

fof(f4425,plain,
    ( i2 = i5
    | i1 != i5
    | i2 = i_881 ),
    inference(equality_factoring,[status(thm)],[f4370]) ).

fof(f4450,plain,
    ( i2 = i_881
    | e_847 = select(a_842,i1)
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f4401]) ).

fof(f4454,plain,
    ( i2 = i5
    | i2 = i_881
    | e_839 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f86,f4423]) ).

fof(f4537,plain,
    ( i2 = i5
    | i2 = i_881
    | e_841 = e_864 ),
    inference(backward_subsumption_resolution,[status(thm)],[f3310,f4424]) ).

fof(f4550,plain,
    ( i2 = i_881
    | i2 = i5
    | e_847 != e_866 ),
    inference(backward_subsumption_resolution,[status(thm)],[f3426,f4425]) ).

fof(f4838,plain,
    ( i0 = i1
    | i2 = i_881
    | e_847 = e_839
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f197,f4450]) ).

fof(f4975,plain,
    ( i2 = i5
    | i2 = i_881
    | i0 = i1
    | i2 = i_881
    | e_847 = e_837
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f4454,f4838]) ).

fof(f4987,plain,
    ( i0 = i1
    | i2 = i_881
    | e_847 = e_837
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f4975]) ).

fof(f4998,plain,
    ( i5 = i2
    | i0 = i2
    | i0 = i1
    | i2 = i_881
    | e_847 = e_866
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f376,f4987]) ).

fof(f5003,plain,
    ( i0 = i2
    | i0 = i1
    | i2 = i_881
    | e_847 = e_866
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f4998]) ).

fof(f5004,plain,
    ( i0 = i2
    | i0 = i1
    | i2 = i_881
    | i5 = i2 ),
    inference(forward_subsumption_resolution,[status(thm)],[f5003,f4550]) ).

fof(f5009,plain,
    ( i0 = i2
    | i2 = i_881
    | i5 = i2
    | i2 = i5
    | i2 = i_881
    | e_866 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f5004,f4419]) ).

fof(f5017,plain,
    ( i0 = i2
    | i2 = i_881
    | i5 = i2
    | i2 = i_881
    | e_847 = select(a_842,i0)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f5004,f4450]) ).

fof(f5060,plain,
    ( i0 = i2
    | i2 = i_881
    | i5 = i2
    | i2 = i5
    | i2 = i_881
    | e_866 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f5009]) ).

fof(f5061,plain,
    ( i0 = i2
    | i2 = i5
    | i2 = i_881
    | e_866 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f5060]) ).

fof(f5070,plain,
    ( i0 = i2
    | i2 = i_881
    | i5 = i2
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(forward_demodulation,[status(thm)],[f121,f5017]) ).

fof(f5071,plain,
    ( i0 = i2
    | i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f5070]) ).

fof(f5093,plain,
    ( i0 = i2
    | i2 = i5
    | i2 = i_881
    | i2 = i_881
    | i2 = i5
    | e_847 != e_864 ),
    inference(paramodulation,[status(thm)],[f5061,f4550]) ).

fof(f5104,plain,
    ( i0 = i2
    | i2 = i_881
    | i2 = i5
    | e_847 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f5093]) ).

fof(f5169,plain,
    ( i2 = i5
    | i2 = i_881
    | i0 = i2
    | i2 = i_881
    | i2 = i5
    | e_847 != e_841 ),
    inference(paramodulation,[status(thm)],[f4537,f5104]) ).

fof(f5171,plain,
    ( i0 = i2
    | i2 = i_881
    | i2 = i5
    | e_847 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f5169]) ).

fof(f5172,plain,
    ( i0 = i2
    | i2 = i_881
    | i2 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f5171,f5071]) ).

fof(f5206,plain,
    ( i2 = i_881
    | i2 = i5
    | e_847 = select(a_842,i0)
    | i5 = i2 ),
    inference(paramodulation,[status(thm)],[f5172,f206]) ).

fof(f5224,plain,
    ( i2 = i_881
    | i2 = i5
    | e_866 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f5172,f99]) ).

fof(f5256,plain,
    ( i2 = i_881
    | i2 = i5
    | e_847 = e_841
    | i5 = i2 ),
    inference(forward_demodulation,[status(thm)],[f121,f5206]) ).

fof(f5257,plain,
    ( i2 = i_881
    | e_847 = e_841
    | i5 = i2 ),
    inference(duplicate_literals_removal,[status(thm)],[f5256]) ).

fof(f5259,plain,
    ( i2 = i_881
    | i2 = i5
    | e_866 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f5224]) ).

fof(f5375,plain,
    ( i2 = i_881
    | i2 = i5
    | i2 = i_881
    | i2 = i5
    | e_847 != e_864 ),
    inference(paramodulation,[status(thm)],[f5259,f4550]) ).

fof(f5386,plain,
    ( i2 = i_881
    | i2 = i5
    | e_847 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f5375]) ).

fof(f5437,plain,
    ( i2 = i5
    | i2 = i_881
    | i2 = i_881
    | i2 = i5
    | e_847 != e_841 ),
    inference(paramodulation,[status(thm)],[f4537,f5386]) ).

fof(f5439,plain,
    ( i2 = i_881
    | i2 = i5
    | e_847 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f5437]) ).

fof(f5440,plain,
    ( i2 = i_881
    | i2 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f5439,f5257]) ).

fof(f5465,plain,
    ( i2 = i_881
    | e_841 = select(a_838,i2)
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f5440,f193]) ).

fof(f5467,plain,
    ( i2 = i_881
    | a_878 = store(a_876,i2,e_875) ),
    inference(paramodulation,[status(thm)],[f5440,f168]) ).

fof(f5469,plain,
    ( i2 = i_881
    | a_874 = store(a_872,i2,e_873) ),
    inference(paramodulation,[status(thm)],[f5440,f80]) ).

fof(f5471,plain,
    ( i2 = i_881
    | a_867 = store(a_865,i2,e_866) ),
    inference(paramodulation,[status(thm)],[f5440,f76]) ).

fof(f5473,plain,
    ( i2 = i_881
    | a_863 = store(a_861,i2,e_862) ),
    inference(paramodulation,[status(thm)],[f5440,f74]) ).

fof(f5476,plain,
    ( i2 = i_881
    | a_857 = store(a_855,i2,e_854) ),
    inference(paramodulation,[status(thm)],[f5440,f141]) ).

fof(f5479,plain,
    ( i2 = i_881
    | a_853 = store(a_851,i2,e_852) ),
    inference(paramodulation,[status(thm)],[f5440,f68]) ).

fof(f5481,plain,
    ( i2 = i_881
    | a_848 = store(a_846,i2,e_847) ),
    inference(paramodulation,[status(thm)],[f5440,f65]) ).

fof(f5484,plain,
    ( i2 = i_881
    | a_844 = store(a_842,i2,e_843) ),
    inference(paramodulation,[status(thm)],[f5440,f63]) ).

fof(f5485,plain,
    ( i2 = i_881
    | e_864 = select(a_861,i2) ),
    inference(paramodulation,[status(thm)],[f5440,f98]) ).

fof(f5488,plain,
    ( i2 = i_881
    | e_841 = select(a_840,i2) ),
    inference(paramodulation,[status(thm)],[f5440,f88]) ).

fof(f5494,plain,
    ( i2 = i_881
    | e_841 = e_837
    | i1 = i5 ),
    inference(forward_demodulation,[status(thm)],[f117,f5465]) ).

fof(f5499,plain,
    ( i2 = i_881
    | e_864 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f149,f5485]) ).

fof(f5555,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_841 = e_864
    | i1 = i5 ),
    inference(paramodulation,[status(thm)],[f5499,f5494]) ).

fof(f5563,plain,
    ( i2 = i_881
    | e_841 = e_864
    | i1 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f5555]) ).

fof(f5607,plain,
    ( i1 = i2
    | i2 = i_881
    | e_841 = select(a_838,i2) ),
    inference(paramodulation,[status(thm)],[f118,f5488]) ).

fof(f5612,plain,
    ( i1 = i2
    | i2 = i_881
    | e_841 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f117,f5607]) ).

fof(f5650,plain,
    ( i2 = i_881
    | i1 = i2
    | i2 = i_881
    | e_841 = e_864 ),
    inference(paramodulation,[status(thm)],[f5499,f5612]) ).

fof(f5659,plain,
    ( i1 = i2
    | i2 = i_881
    | e_841 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f5650]) ).

fof(f5663,plain,
    ( i1 = i_881
    | i2 = i_881
    | i5 = i_881
    | i1 = i2
    | i2 = i_881 ),
    inference(resolution,[status(thm)],[f5659,f674]) ).

fof(f5671,plain,
    ( i1 = i_881
    | i5 = i_881
    | i1 = i2
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f5663]) ).

fof(f5678,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_878,X0) = select(a_876,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5467,f57]) ).

fof(f5686,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_874,X0) = select(a_872,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5469,f57]) ).

fof(f5693,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_867,X0) = select(a_865,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5471,f57]) ).

fof(f5699,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_863,X0) = select(a_861,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5473,f57]) ).

fof(f5704,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_857,X0) = select(a_855,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5476,f57]) ).

fof(f5709,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_853,X0) = select(a_851,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5479,f57]) ).

fof(f5713,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_848,X0) = select(a_846,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5481,f57]) ).

fof(f5716,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_844,X0) = select(a_842,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f5484,f57]) ).

fof(f6157,plain,
    ! [X0] :
      ( i2 = X0
      | i2 = i_881
      | select(a_878,X0) = select(a_874,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f164,f5678]) ).

fof(f6163,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_878,X0) = select(a_874,X0)
      | i2 = X0 ),
    inference(duplicate_literals_removal,[status(thm)],[f6157]) ).

fof(f6166,plain,
    ( i2 = i_881
    | select(a_874,i1) = e_870
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f161,f5686]) ).

fof(f6170,plain,
    ! [X0] :
      ( i1 = X0
      | i2 = i_881
      | select(a_874,X0) = select(a_871,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f160,f5686]) ).

fof(f6180,plain,
    ( i5 = i_881
    | i1 = i2
    | i2 = i_881
    | i2 = i_881
    | select(a_874,i_881) = e_870
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f5671,f6166]) ).

fof(f6184,plain,
    ( i5 = i_881
    | i2 = i_881
    | select(a_874,i_881) = e_870
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f6180]) ).

fof(f6187,plain,
    ( i2 = i_881
    | select(a_867,i0) = e_864
    | i2 = i0 ),
    inference(paramodulation,[status(thm)],[f153,f5693]) ).

fof(f6192,plain,
    ! [X0] :
      ( i0 = X0
      | i2 = i_881
      | select(a_867,X0) = select(a_863,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f152,f5693]) ).

fof(f6221,plain,
    ! [X0] :
      ( i2 = X0
      | i2 = i_881
      | select(a_863,X0) = select(a_860,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f148,f5699]) ).

fof(f6230,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_863,X0) = select(a_860,X0)
      | i2 = X0 ),
    inference(duplicate_literals_removal,[status(thm)],[f6221]) ).

fof(f6245,plain,
    ! [X0] :
      ( i2 = X0
      | i2 = i_881
      | select(a_857,X0) = select(a_853,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f137,f5704]) ).

fof(f6251,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_857,X0) = select(a_853,X0)
      | i2 = X0 ),
    inference(duplicate_literals_removal,[status(thm)],[f6245]) ).

fof(f6254,plain,
    ( i2 = i_881
    | select(a_853,i1) = e_849
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f134,f5709]) ).

fof(f6258,plain,
    ! [X0] :
      ( i1 = X0
      | i2 = i_881
      | select(a_853,X0) = select(a_850,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f133,f5709]) ).

fof(f6268,plain,
    ( i5 = i_881
    | i1 = i2
    | i2 = i_881
    | i2 = i_881
    | select(a_853,i_881) = e_849
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f5671,f6254]) ).

fof(f6272,plain,
    ( i5 = i_881
    | i2 = i_881
    | select(a_853,i_881) = e_849
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f6268]) ).

fof(f6277,plain,
    ( i2 = i_881
    | e_849 = select(a_846,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f92,f5713]) ).

fof(f6278,plain,
    ! [X0] :
      ( i1 = X0
      | i2 = i_881
      | select(a_850,X0) = select(a_846,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f131,f5713]) ).

fof(f6298,plain,
    ! [X0] :
      ( i2 = X0
      | i2 = i_881
      | select(a_846,X0) = select(a_842,X0)
      | i2 = X0 ),
    inference(paramodulation,[status(thm)],[f127,f5716]) ).

fof(f6304,plain,
    ! [X0] :
      ( i2 = i_881
      | select(a_846,X0) = select(a_842,X0)
      | i2 = X0 ),
    inference(duplicate_literals_removal,[status(thm)],[f6298]) ).

fof(f6309,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_883 = select(a_874,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f341,f6163]) ).

fof(f6318,plain,
    ( e_883 = select(a_874,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f6309]) ).

fof(f6355,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_882 = select(a_853,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f253,f6251]) ).

fof(f6364,plain,
    ( e_882 = select(a_853,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f6355]) ).

fof(f6371,plain,
    ( i2 = i_881
    | i2 = i1
    | i2 = i_881
    | e_849 = select(a_842,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f6277,f6304]) ).

fof(f6383,plain,
    ( i2 = i_881
    | e_849 = select(a_842,i1)
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f6371]) ).

fof(f6390,plain,
    ( i0 = i1
    | i2 = i_881
    | e_849 = e_839
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f197,f6383]) ).

fof(f7553,plain,
    ( i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = select(a_871,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f6318,f6170]) ).

fof(f7573,plain,
    ( i1 = i_881
    | e_883 = select(a_871,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7553]) ).

fof(f7578,plain,
    ( i2 = i_881
    | i1 = i_881
    | i1 = i_881
    | e_883 = select(a_867,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f309,f7573]) ).

fof(f7584,plain,
    ( i1 = i_881
    | e_883 = select(a_867,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7578]) ).

fof(f7601,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i_881
    | e_883 = e_870
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f6318,f6184]) ).

fof(f7608,plain,
    ( i5 = i_881
    | i2 = i_881
    | e_883 = e_870
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7601]) ).

fof(f7622,plain,
    ( i1 = i_881
    | i2 = i_881
    | i0 = i_881
    | i2 = i_881
    | e_883 = select(a_863,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f7584,f6192]) ).

fof(f7625,plain,
    ( i2 = i1
    | i0 = i1
    | i2 = i_881
    | e_870 = select(a_863,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f298,f6192]) ).

fof(f7648,plain,
    ( i1 = i_881
    | i0 = i_881
    | e_883 = select(a_863,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7622]) ).

fof(f7651,plain,
    ( i0 = i1
    | i2 = i_881
    | e_870 = select(a_863,i1)
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7625]) ).

fof(f7659,plain,
    ( i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_850,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f6364,f6258]) ).

fof(f7683,plain,
    ( i1 = i_881
    | e_882 = select(a_850,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7659]) ).

fof(f7699,plain,
    ( i2 = i_881
    | i5 = i_881
    | i2 = i_881
    | e_882 = e_849
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f6364,f6272]) ).

fof(f7706,plain,
    ( i5 = i_881
    | i2 = i_881
    | e_882 = e_849
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7699]) ).

fof(f7713,plain,
    ( i0 = i1
    | i2 = i_881
    | i2 = i1
    | i5 = i_881
    | i2 = i_881
    | e_882 = e_839
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f6390,f7706]) ).

fof(f7720,plain,
    ( i0 = i1
    | i5 = i_881
    | i2 = i_881
    | e_882 = e_839
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7713]) ).

fof(f7724,plain,
    ( i1 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = select(a_846,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f7683,f6278]) ).

fof(f7748,plain,
    ( i1 = i_881
    | e_882 = select(a_846,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7724]) ).

fof(f7759,plain,
    ( i2 = i_881
    | i2 = i_881
    | i1 = i_881
    | e_882 = select(a_842,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f6304,f7748]) ).

fof(f7765,plain,
    ( i1 = i_881
    | e_882 = select(a_842,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7759]) ).

fof(f7772,plain,
    ( i1 = i_881
    | i0 = i_881
    | i1 = i_881
    | e_882 = select(a_838,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f200,f7765]) ).

fof(f7777,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_882 = select(a_838,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7772]) ).

fof(f7855,plain,
    ( i2 = i_881
    | i2 = i_881
    | i1 = i_881
    | i0 = i_881
    | e_883 = select(a_860,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f6230,f7648]) ).

fof(f7861,plain,
    ( i1 = i_881
    | i0 = i_881
    | e_883 = select(a_860,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7855]) ).

fof(f7867,plain,
    ( i2 = i_881
    | i2 = i1
    | i0 = i1
    | i2 = i_881
    | e_870 = select(a_860,i1)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f6230,f7651]) ).

fof(f7874,plain,
    ( i2 = i_881
    | i2 = i1
    | i0 = i1
    | i2 = i_881
    | e_870 = e_839
    | i2 = i1 ),
    inference(forward_demodulation,[status(thm)],[f147,f7867]) ).

fof(f7875,plain,
    ( i0 = i1
    | i2 = i_881
    | e_870 = e_839
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7874]) ).

fof(f7884,plain,
    ( i5 = i_881
    | i2 = i_881
    | i2 = i1
    | i0 = i1
    | i2 = i_881
    | e_883 = e_839
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f7608,f7875]) ).

fof(f7892,plain,
    ( i5 = i_881
    | i0 = i1
    | i2 = i_881
    | e_883 = e_839
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7884]) ).

fof(f7930,plain,
    ( i2 = i_881
    | i1 = i_881
    | i1 = i_881
    | i0 = i_881
    | e_883 = select(a_838,i_881)
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f259,f7861]) ).

fof(f7940,plain,
    ( i1 = i_881
    | i0 = i_881
    | e_883 = select(a_838,i_881)
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f7930]) ).

fof(f7946,plain,
    ( i0 = i1
    | i5 = i_881
    | i2 = i_881
    | i2 = i1
    | i5 = i_881
    | i0 = i1
    | i2 = i_881
    | e_883 = e_882
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f7720,f7892]) ).

fof(f7954,plain,
    ( i5 = i_881
    | i0 = i1
    | i2 = i_881
    | e_883 = e_882
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7946]) ).

fof(f7955,plain,
    ( i5 = i_881
    | i0 = i1
    | i2 = i_881
    | i2 = i1 ),
    inference(forward_subsumption_resolution,[status(thm)],[f7954,f109]) ).

fof(f7962,plain,
    ( i5 = i_881
    | i1 = i2
    | i2 = i_881
    | i5 = i_881
    | i0 = i_881
    | i2 = i_881
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f5671,f7955]) ).

fof(f7965,plain,
    ( i5 = i_881
    | i2 = i_881
    | i2 = i1
    | i2 = i_881
    | e_849 = select(a_842,i0)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f7955,f6383]) ).

fof(f8000,plain,
    ( i1 = i2
    | i0 != i2
    | i5 = i_881
    | i2 = i_881 ),
    inference(equality_factoring,[status(thm)],[f7955]) ).

fof(f8001,plain,
    ( i5 = i_881
    | i0 = i_881
    | i2 = i_881
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f7962]) ).

fof(f8004,plain,
    ( i5 = i_881
    | i2 = i_881
    | i2 = i1
    | i2 = i_881
    | e_849 = e_841
    | i2 = i1 ),
    inference(forward_demodulation,[status(thm)],[f121,f7965]) ).

fof(f8005,plain,
    ( i5 = i_881
    | i2 = i_881
    | e_849 = e_841
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f8004]) ).

fof(f8048,plain,
    ( i5 = i_881
    | i2 = i_881
    | i2 = i1
    | i5 = i_881
    | i2 = i_881
    | e_882 = e_841
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f7706,f8005]) ).

fof(f8058,plain,
    ( i5 = i_881
    | i2 = i_881
    | e_882 = e_841
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f8048]) ).

fof(f8076,plain,
    ( i2 = i_881
    | i1 = i2
    | i0 != i2
    | i2 = i_881
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f5440,f8000]) ).

fof(f8077,plain,
    ( i1 = i2
    | i0 != i2
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f8076]) ).

fof(f8082,plain,
    ( i0 = i_881
    | i1 = i_881
    | i2 = i_881
    | i1 = i_881
    | i0 = i_881
    | e_883 = e_882
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f7777,f7940]) ).

fof(f8094,plain,
    ( i1 = i_881
    | i0 = i_881
    | e_883 = e_882
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f8082]) ).

fof(f8095,plain,
    ( i1 = i_881
    | i0 = i_881
    | i2 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f8094,f109]) ).

fof(f8122,plain,
    ( i1 = i_881
    | i2 = i_881
    | select(a_865,i_881) = e_864 ),
    inference(paramodulation,[status(thm)],[f8095,f153]) ).

fof(f8124,plain,
    ( i1 = i_881
    | i2 = i_881
    | select(a_842,i_881) = e_841 ),
    inference(paramodulation,[status(thm)],[f8095,f121]) ).

fof(f8132,plain,
    ( i2 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | select(a_867,i_881) = e_864 ),
    inference(paramodulation,[status(thm)],[f5693,f8122]) ).

fof(f8140,plain,
    ( i1 = i_881
    | i2 = i_881
    | select(a_867,i_881) = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8132]) ).

fof(f8144,plain,
    ( i1 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_882 = e_841 ),
    inference(paramodulation,[status(thm)],[f7765,f8124]) ).

fof(f8154,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_882 = e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f8144]) ).

fof(f8191,plain,
    ( i1 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_883 = e_864 ),
    inference(paramodulation,[status(thm)],[f7584,f8140]) ).

fof(f8203,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_883 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8191]) ).

fof(f8210,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_882 != e_864 ),
    inference(paramodulation,[status(thm)],[f8203,f109]) ).

fof(f8211,plain,
    ( i1 = i_881
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881
    | e_841 != e_864 ),
    inference(paramodulation,[status(thm)],[f8154,f8210]) ).

fof(f8213,plain,
    ( i1 = i_881
    | i2 = i_881
    | e_841 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8211]) ).

fof(f8215,plain,
    ( i1 = i2
    | i2 = i_881
    | i1 = i_881
    | i2 = i_881 ),
    inference(resolution,[status(thm)],[f8213,f5659]) ).

fof(f8216,plain,
    ( i2 = i_881
    | i1 = i5
    | i1 = i_881
    | i2 = i_881 ),
    inference(resolution,[status(thm)],[f8213,f5563]) ).

fof(f8221,plain,
    ( i1 = i2
    | i1 = i_881
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f8215]) ).

fof(f8222,plain,
    ( i1 = i5
    | i1 = i_881
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f8216]) ).

fof(f8245,plain,
    ( i1 = i2
    | i2 = i_881
    | e_870 = select(a_867,i_881)
    | i2 = i1 ),
    inference(paramodulation,[status(thm)],[f8221,f298]) ).

fof(f8281,plain,
    ( i2 = i_881
    | e_870 = select(a_867,i_881)
    | i2 = i1 ),
    inference(duplicate_literals_removal,[status(thm)],[f8245]) ).

fof(f8321,plain,
    ( i1 = i5
    | i_881 != i5
    | i2 = i_881 ),
    inference(equality_factoring,[status(thm)],[f8222]) ).

fof(f8356,plain,
    ( i2 = i_881
    | i1 = i2
    | i_881 != i5
    | i2 = i_881 ),
    inference(paramodulation,[status(thm)],[f5440,f8321]) ).

fof(f8357,plain,
    ( i1 = i2
    | i_881 != i5
    | i2 = i_881 ),
    inference(duplicate_literals_removal,[status(thm)],[f8356]) ).

fof(f8386,plain,
    ( i2 = i_881
    | e_882 = e_841
    | i2 = i1 ),
    inference(backward_subsumption_resolution,[status(thm)],[f8058,f8357]) ).

fof(f8389,plain,
    ( i0 = i_881
    | i2 = i_881
    | i2 = i1 ),
    inference(backward_subsumption_resolution,[status(thm)],[f8001,f8357]) ).

fof(f8395,plain,
    ( i2 = i_881
    | e_883 = e_870
    | i2 = i1 ),
    inference(backward_subsumption_resolution,[status(thm)],[f7608,f8357]) ).

fof(f8442,plain,
    ( i2 = i_881
    | i2 = i1
    | i2 = i_881
    | select(a_867,i_881) = e_864
    | i2 = i0 ),
    inference(paramodulation,[status(thm)],[f8389,f6187]) ).

fof(f8461,plain,
    ( i2 = i1
    | i2 = i_881
    | select(a_867,i_881) = e_864
    | i2 = i0 ),
    inference(duplicate_literals_removal,[status(thm)],[f8442]) ).

fof(f8462,plain,
    ( i2 = i1
    | i2 = i_881
    | select(a_867,i_881) = e_864 ),
    inference(forward_subsumption_resolution,[status(thm)],[f8461,f8077]) ).

fof(f8914,plain,
    ( i2 = i_881
    | i2 = i1
    | i2 = i1
    | i2 = i_881
    | e_870 = e_864 ),
    inference(paramodulation,[status(thm)],[f8281,f8462]) ).

fof(f8928,plain,
    ( i2 = i1
    | i2 = i_881
    | e_870 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8914]) ).

fof(f8935,plain,
    ( i2 = i_881
    | i2 = i1
    | i2 = i1
    | i2 = i_881
    | e_883 = e_864 ),
    inference(paramodulation,[status(thm)],[f8395,f8928]) ).

fof(f8943,plain,
    ( i2 = i1
    | i2 = i_881
    | e_883 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8935]) ).

fof(f8951,plain,
    ( i2 = i1
    | i2 = i_881
    | e_882 != e_864 ),
    inference(paramodulation,[status(thm)],[f8943,f109]) ).

fof(f8952,plain,
    ( i2 = i_881
    | i2 = i1
    | i2 = i1
    | i2 = i_881
    | e_841 != e_864 ),
    inference(paramodulation,[status(thm)],[f8386,f8951]) ).

fof(f8954,plain,
    ( i2 = i1
    | i2 = i_881
    | e_841 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f8952]) ).

fof(f8955,plain,
    ( i2 = i1
    | i2 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f8954,f5659]) ).

fof(f9004,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_841 = select(a_840,i1) ),
    inference(paramodulation,[status(thm)],[f8955,f5488]) ).

fof(f9063,plain,
    ( i2 = i_881
    | e_839 = select(a_836,i1) ),
    inference(paramodulation,[status(thm)],[f8955,f87]) ).

fof(f9064,plain,
    ( i2 = i_881
    | i1 != i_881 ),
    inference(equality_factoring,[status(thm)],[f8955]) ).

fof(f9116,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_841 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f119,f9004]) ).

fof(f9117,plain,
    ( i2 = i_881
    | e_841 = e_839 ),
    inference(duplicate_literals_removal,[status(thm)],[f9116]) ).

fof(f9135,plain,
    ( i2 = i_881
    | e_839 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f86,f9063]) ).

fof(f9198,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_841 = e_837 ),
    inference(paramodulation,[status(thm)],[f9117,f9135]) ).

fof(f9206,plain,
    ( i2 = i_881
    | e_841 = e_837 ),
    inference(duplicate_literals_removal,[status(thm)],[f9198]) ).

fof(f9211,plain,
    ( i2 = i_881
    | e_841 != e_864 ),
    inference(backward_subsumption_resolution,[status(thm)],[f8213,f9064]) ).

fof(f9312,plain,
    ( i2 = i_881
    | i2 = i_881
    | e_841 = e_864 ),
    inference(paramodulation,[status(thm)],[f5499,f9206]) ).

fof(f9320,plain,
    ( i2 = i_881
    | e_841 = e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f9312]) ).

fof(f9574,plain,
    ( i_881 = i0
    | i1 = i0
    | i0 = i5
    | e_868 = e_843 ),
    inference(backward_demodulation,[status(thm)],[f9674,f822]) ).

fof(f9581,plain,
    ( i0 = i5
    | i1 = i_881
    | e_873 = e_862 ),
    inference(backward_demodulation,[status(thm)],[f9674,f752]) ).

fof(f9589,plain,
    ( i1 = i_881
    | i2 = i5
    | e_858 = e_843 ),
    inference(backward_demodulation,[status(thm)],[f9674,f696]) ).

fof(f9598,plain,
    ( i_881 = i5
    | e_864 = e_841
    | i1 = i5 ),
    inference(backward_demodulation,[status(thm)],[f9674,f602]) ).

fof(f9600,plain,
    ( i_881 = i0
    | e_862 = e_843
    | i1 = i0 ),
    inference(backward_demodulation,[status(thm)],[f9674,f560]) ).

fof(f9613,plain,
    ( i_881 = i5
    | a_859 = store(a_857,i2,e_852) ),
    inference(backward_demodulation,[status(thm)],[f9674,f245]) ).

fof(f9620,plain,
    ( e_873 = e_868
    | i1 = i_881 ),
    inference(backward_demodulation,[status(thm)],[f9674,f412]) ).

fof(f9629,plain,
    ( e_862 = select(a_860,i0)
    | i_881 = i0 ),
    inference(backward_demodulation,[status(thm)],[f9674,f268]) ).

fof(f9630,plain,
    ( e_864 = select(a_860,i5)
    | i_881 = i5 ),
    inference(backward_demodulation,[status(thm)],[f9674,f267]) ).

fof(f9636,plain,
    ( e_879 = e_873
    | i_881 = i5 ),
    inference(backward_demodulation,[status(thm)],[f9674,f331]) ).

fof(f9653,plain,
    select(a_880,i_881) = e_879,
    inference(backward_demodulation,[status(thm)],[f9674,f172]) ).

fof(f9655,plain,
    e_875 = select(a_876,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f167]) ).

fof(f9657,plain,
    select(a_869,i_881) = e_868,
    inference(backward_demodulation,[status(thm)],[f9674,f157]) ).

fof(f9659,plain,
    select(a_861,i_881) = e_837,
    inference(backward_demodulation,[status(thm)],[f9674,f149]) ).

fof(f9660,plain,
    select(a_859,i_881) = e_858,
    inference(backward_demodulation,[status(thm)],[f9674,f145]) ).

fof(f9661,plain,
    e_854 = select(a_855,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f140]) ).

fof(f9662,plain,
    a_861 = store(a_860,i_881,e_837),
    inference(backward_demodulation,[status(thm)],[f9674,f73]) ).

fof(f9664,plain,
    select(a_846,i_881) = e_843,
    inference(backward_demodulation,[status(thm)],[f9674,f128]) ).

fof(f9666,plain,
    select(a_838,i_881) = e_837,
    inference(backward_demodulation,[status(thm)],[f9674,f117]) ).

fof(f9668,plain,
    e_873 = select(a_872,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f102]) ).

fof(f9669,plain,
    e_866 = select(a_865,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f99]) ).

fof(f9670,plain,
    a_838 = store(a_836,i_881,e_837),
    inference(backward_demodulation,[status(thm)],[f9674,f60]) ).

fof(f9671,plain,
    e_852 = select(a_851,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f93]) ).

fof(f9672,plain,
    e_847 = select(a_844,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f91]) ).

fof(f9673,plain,
    e_839 = select(a_836,i_881),
    inference(backward_demodulation,[status(thm)],[f9674,f87]) ).

fof(f9674,plain,
    i2 = i_881,
    inference(forward_subsumption_resolution,[status(thm)],[f9320,f9211]) ).

fof(f9709,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_858 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f9674,f9589]) ).

fof(f9722,plain,
    ( i_881 = i5
    | a_859 = store(a_857,i_881,e_852) ),
    inference(forward_demodulation,[status(thm)],[f9674,f9613]) ).

fof(f9738,plain,
    e_883 = e_879,
    inference(forward_demodulation,[status(thm)],[f107,f9653]) ).

fof(f9739,plain,
    e_882 = e_858,
    inference(forward_demodulation,[status(thm)],[f106,f9660]) ).

fof(f9741,plain,
    e_882 != e_879,
    inference(backward_demodulation,[status(thm)],[f9738,f109]) ).

fof(f9746,plain,
    e_858 = select(a_859,i_881),
    inference(backward_demodulation,[status(thm)],[f9739,f106]) ).

fof(f9747,plain,
    e_858 != e_879,
    inference(forward_demodulation,[status(thm)],[f9739,f9741]) ).

fof(f9756,plain,
    ( i_881 = i5
    | e_858 != e_873 ),
    inference(paramodulation,[status(thm)],[f9636,f9747]) ).

fof(f9794,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_858 != e_868 ),
    inference(paramodulation,[status(thm)],[f9620,f9756]) ).

fof(f9937,plain,
    ( i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_862 ),
    inference(paramodulation,[status(thm)],[f9581,f9756]) ).

fof(f10155,plain,
    ( i_881 = i0
    | i1 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f9574,f9794]) ).

fof(f10159,plain,
    ( i_881 = i0
    | i1 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f10155,f9709]) ).

fof(f10302,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | select(a_860,i0) = e_839 ),
    inference(paramodulation,[status(thm)],[f10159,f147]) ).

fof(f10306,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | select(a_840,i0) = e_839 ),
    inference(paramodulation,[status(thm)],[f10159,f119]) ).

fof(f10324,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_843 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f89,f10306]) ).

fof(f10430,plain,
    ( i_881 = i0
    | i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_862 = e_839 ),
    inference(paramodulation,[status(thm)],[f9629,f10302]) ).

fof(f10436,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_862 = e_839 ),
    inference(duplicate_literals_removal,[status(thm)],[f10430]) ).

fof(f10537,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_862 = e_843 ),
    inference(paramodulation,[status(thm)],[f10324,f10436]) ).

fof(f10547,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_862 = e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f10537]) ).

fof(f10562,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f10547,f9937]) ).

fof(f10568,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f10562]) ).

fof(f10569,plain,
    ( i_881 = i0
    | i0 = i5
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f10568,f9709]) ).

fof(f10607,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_868 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f10569,f100]) ).

fof(f10609,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_864 = select(a_861,i0) ),
    inference(paramodulation,[status(thm)],[f10569,f98]) ).

fof(f10612,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_841 = select(a_840,i0) ),
    inference(paramodulation,[status(thm)],[f10569,f88]) ).

fof(f10627,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_868 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f10607]) ).

fof(f10628,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_864 = e_862 ),
    inference(forward_demodulation,[status(thm)],[f97,f10609]) ).

fof(f10629,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_841 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f89,f10612]) ).

fof(f10635,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_864 ),
    inference(paramodulation,[status(thm)],[f10627,f9794]) ).

fof(f10642,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f10635]) ).

fof(f10660,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_862 ),
    inference(paramodulation,[status(thm)],[f10628,f10642]) ).

fof(f10661,plain,
    ( i_881 = i5
    | i1 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_841 ),
    inference(paramodulation,[status(thm)],[f9598,f10642]) ).

fof(f10662,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_862 ),
    inference(duplicate_literals_removal,[status(thm)],[f10660]) ).

fof(f10663,plain,
    ( i1 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f10661]) ).

fof(f10664,plain,
    ( i_881 = i0
    | i1 = i0
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f9600,f10662]) ).

fof(f10665,plain,
    ( i1 = i0
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f10664]) ).

fof(f10666,plain,
    ( i1 = i0
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f10665,f9709]) ).

fof(f10688,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | select(a_840,i0) = e_839 ),
    inference(paramodulation,[status(thm)],[f10666,f119]) ).

fof(f10706,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_843 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f89,f10688]) ).

fof(f10801,plain,
    ( i1 = i_881
    | i_881 = i5
    | i1 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_843 != e_841 ),
    inference(paramodulation,[status(thm)],[f9709,f10663]) ).

fof(f10803,plain,
    ( i1 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_843 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f10801]) ).

fof(f10804,plain,
    ( i1 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f10803,f10629]) ).

fof(f10819,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_864 = select(a_860,i1)
    | i_881 = i5 ),
    inference(paramodulation,[status(thm)],[f10804,f9630]) ).

fof(f10863,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_864 = e_839
    | i_881 = i5 ),
    inference(forward_demodulation,[status(thm)],[f147,f10819]) ).

fof(f10864,plain,
    ( i_881 = i0
    | i1 = i_881
    | e_864 = e_839
    | i_881 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f10863]) ).

fof(f10872,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | i_881 = i0
    | i1 = i_881
    | e_864 = e_843
    | i_881 = i5 ),
    inference(paramodulation,[status(thm)],[f10706,f10864]) ).

fof(f10880,plain,
    ( i_881 = i0
    | i1 = i_881
    | e_864 = e_843
    | i_881 = i5 ),
    inference(duplicate_literals_removal,[status(thm)],[f10872]) ).

fof(f10928,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f10880,f10642]) ).

fof(f10934,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f10928]) ).

fof(f10935,plain,
    ( i_881 = i0
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f10934,f9709]) ).

fof(f10950,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_862 = select(a_861,i_881) ),
    inference(paramodulation,[status(thm)],[f10935,f97]) ).

fof(f10951,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_843 = select(a_840,i_881) ),
    inference(paramodulation,[status(thm)],[f10935,f89]) ).

fof(f10956,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_862 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f9659,f10950]) ).

fof(f10996,plain,
    ( i1 = i_881
    | i1 = i_881
    | i_881 = i5
    | e_843 = select(a_838,i_881) ),
    inference(paramodulation,[status(thm)],[f118,f10951]) ).

fof(f10999,plain,
    ( i1 = i_881
    | i1 = i_881
    | i_881 = i5
    | e_843 = e_837 ),
    inference(forward_demodulation,[status(thm)],[f9666,f10996]) ).

fof(f11000,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_843 = e_837 ),
    inference(duplicate_literals_removal,[status(thm)],[f10999]) ).

fof(f11003,plain,
    ( i1 = i_881
    | i_881 = i5
    | i1 = i_881
    | i_881 = i5
    | e_843 = e_862 ),
    inference(paramodulation,[status(thm)],[f10956,f11000]) ).

fof(f11009,plain,
    ( i1 = i_881
    | i_881 = i5
    | e_843 = e_862 ),
    inference(duplicate_literals_removal,[status(thm)],[f11003]) ).

fof(f11016,plain,
    ( i1 = i_881
    | i_881 = i5
    | i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f11009,f9937]) ).

fof(f11022,plain,
    ( i0 = i5
    | i1 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11016]) ).

fof(f11023,plain,
    ( i0 = i5
    | i1 = i_881
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f11022,f9709]) ).

fof(f11064,plain,
    ( i5 = i_881
    | i0 != i_881
    | i1 = i_881 ),
    inference(equality_factoring,[status(thm)],[f11023]) ).

fof(f11078,plain,
    ( i5 = i_881
    | i1 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f11064,f10935]) ).

fof(f11092,plain,
    ( i5 = i_881
    | select(a_872,i_881) = e_870 ),
    inference(paramodulation,[status(thm)],[f11078,f161]) ).

fof(f11097,plain,
    ( i5 = i_881
    | select(a_851,i_881) = e_849 ),
    inference(paramodulation,[status(thm)],[f11078,f134]) ).

fof(f11098,plain,
    ( i5 = i_881
    | a_860 = store(a_836,i_881,e_839) ),
    inference(paramodulation,[status(thm)],[f11078,f72]) ).

fof(f11103,plain,
    ( i5 = i_881
    | e_870 = select(a_869,i_881) ),
    inference(paramodulation,[status(thm)],[f11078,f101]) ).

fof(f11104,plain,
    ( i5 = i_881
    | a_840 = store(a_838,i_881,e_839) ),
    inference(paramodulation,[status(thm)],[f11078,f61]) ).

fof(f11105,plain,
    ( i5 = i_881
    | e_849 = select(a_848,i_881) ),
    inference(paramodulation,[status(thm)],[f11078,f92]) ).

fof(f11106,plain,
    ( i5 = i_881
    | e_837 = select(a_836,i_881) ),
    inference(paramodulation,[status(thm)],[f11078,f86]) ).

fof(f11108,plain,
    ( i5 = i_881
    | e_873 = e_870 ),
    inference(forward_demodulation,[status(thm)],[f9668,f11092]) ).

fof(f11109,plain,
    ( i5 = i_881
    | e_852 = e_849 ),
    inference(forward_demodulation,[status(thm)],[f9671,f11097]) ).

fof(f11110,plain,
    ( i5 = i_881
    | e_870 = e_868 ),
    inference(forward_demodulation,[status(thm)],[f9657,f11103]) ).

fof(f11111,plain,
    ( i5 = i_881
    | e_837 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f9673,f11106]) ).

fof(f11120,plain,
    ( i5 = i_881
    | i5 = i_881
    | e_873 = e_868 ),
    inference(paramodulation,[status(thm)],[f11108,f11110]) ).

fof(f11126,plain,
    ( i5 = i_881
    | e_873 = e_868 ),
    inference(duplicate_literals_removal,[status(thm)],[f11120]) ).

fof(f11140,plain,
    ( i5 = i_881
    | i_881 = i5
    | e_858 != e_868 ),
    inference(paramodulation,[status(thm)],[f11126,f9756]) ).

fof(f11144,plain,
    ( i_881 = i5
    | e_858 != e_868 ),
    inference(duplicate_literals_removal,[status(thm)],[f11140]) ).

fof(f11146,plain,
    ( i0 = i5
    | i_881 = i5
    | e_858 != e_862 ),
    inference(paramodulation,[status(thm)],[f286,f11144]) ).

fof(f11184,plain,
    ( i5 = i_881
    | i5 = i_881
    | e_849 = select(a_846,i_881) ),
    inference(paramodulation,[status(thm)],[f129,f11105]) ).

fof(f11187,plain,
    ( i5 = i_881
    | i5 = i_881
    | e_849 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f9664,f11184]) ).

fof(f11188,plain,
    ( i5 = i_881
    | e_849 = e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11187]) ).

fof(f11191,plain,
    ( i5 = i_881
    | i5 = i_881
    | e_852 = e_843 ),
    inference(paramodulation,[status(thm)],[f11109,f11188]) ).

fof(f11197,plain,
    ( i5 = i_881
    | e_852 = e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11191]) ).

fof(f11199,plain,
    ( i5 = i_881
    | i_881 = i5
    | a_859 = store(a_857,i_881,e_843) ),
    inference(paramodulation,[status(thm)],[f11197,f9722]) ).

fof(f11201,plain,
    ( i_881 = i5
    | a_859 = store(a_857,i_881,e_843) ),
    inference(duplicate_literals_removal,[status(thm)],[f11199]) ).

fof(f11218,plain,
    ( i5 = i_881
    | i5 = i_881
    | a_860 = store(a_836,i_881,e_837) ),
    inference(paramodulation,[status(thm)],[f11111,f11098]) ).

fof(f11221,plain,
    ( i5 = i_881
    | i5 = i_881
    | a_860 = a_838 ),
    inference(forward_demodulation,[status(thm)],[f9670,f11218]) ).

fof(f11222,plain,
    ( i5 = i_881
    | a_860 = a_838 ),
    inference(duplicate_literals_removal,[status(thm)],[f11221]) ).

fof(f11229,plain,
    ( i5 = i_881
    | a_861 = store(a_838,i_881,e_837) ),
    inference(paramodulation,[status(thm)],[f11222,f9662]) ).

fof(f11266,plain,
    ( i5 = i_881
    | i5 = i_881
    | a_840 = store(a_838,i_881,e_837) ),
    inference(paramodulation,[status(thm)],[f11111,f11104]) ).

fof(f11269,plain,
    ( i5 = i_881
    | a_840 = store(a_838,i_881,e_837) ),
    inference(duplicate_literals_removal,[status(thm)],[f11266]) ).

fof(f11362,plain,
    ( i_881 = i5
    | select(a_859,i_881) = e_843 ),
    inference(paramodulation,[status(thm)],[f11201,f55]) ).

fof(f11363,plain,
    ( i_881 = i5
    | e_858 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f9746,f11362]) ).

fof(f11460,plain,
    ( i5 = i_881
    | i5 = i_881
    | a_840 = a_861 ),
    inference(paramodulation,[status(thm)],[f11229,f11269]) ).

fof(f11465,plain,
    ( i5 = i_881
    | a_840 = a_861 ),
    inference(duplicate_literals_removal,[status(thm)],[f11460]) ).

fof(f11474,plain,
    ( i5 = i_881
    | e_862 = select(a_840,i0) ),
    inference(paramodulation,[status(thm)],[f11465,f97]) ).

fof(f11476,plain,
    ( i5 = i_881
    | e_862 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f89,f11474]) ).

fof(f11479,plain,
    ( i5 = i_881
    | i0 = i5
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f11476,f11146]) ).

fof(f11484,plain,
    ( i0 = i5
    | i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11479]) ).

fof(f11485,plain,
    ( i0 = i5
    | i_881 = i5 ),
    inference(forward_subsumption_resolution,[status(thm)],[f11484,f11363]) ).

fof(f11521,plain,
    ( i_881 = i5
    | e_868 = select(a_865,i0) ),
    inference(paramodulation,[status(thm)],[f11485,f100]) ).

fof(f11523,plain,
    ( i_881 = i5
    | e_864 = select(a_861,i0) ),
    inference(paramodulation,[status(thm)],[f11485,f98]) ).

fof(f11536,plain,
    ( i_881 = i5
    | e_868 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f153,f11521]) ).

fof(f11537,plain,
    ( i_881 = i5
    | e_864 = e_862 ),
    inference(forward_demodulation,[status(thm)],[f97,f11523]) ).

fof(f11547,plain,
    ( i_881 = i5
    | i_881 = i5
    | e_858 != e_864 ),
    inference(paramodulation,[status(thm)],[f11536,f11144]) ).

fof(f11558,plain,
    ( i_881 = i5
    | e_858 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f11547]) ).

fof(f11584,plain,
    ( i_881 = i5
    | i_881 = i5
    | e_858 != e_862 ),
    inference(paramodulation,[status(thm)],[f11537,f11558]) ).

fof(f11586,plain,
    ( i_881 = i5
    | e_858 != e_862 ),
    inference(duplicate_literals_removal,[status(thm)],[f11584]) ).

fof(f11608,plain,
    ( i5 = i_881
    | i_881 = i5
    | e_858 != e_843 ),
    inference(paramodulation,[status(thm)],[f11476,f11586]) ).

fof(f11611,plain,
    ( i_881 = i5
    | e_858 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11608]) ).

fof(f11612,plain,
    i_881 = i5,
    inference(forward_subsumption_resolution,[status(thm)],[f11611,f11363]) ).

fof(f11689,plain,
    ( i_881 = i0
    | i1 = i0
    | i0 = i_881
    | e_868 = e_843 ),
    inference(backward_demodulation,[status(thm)],[f11612,f9574]) ).

fof(f11733,plain,
    ( e_854 = e_847
    | i1 = i_881 ),
    inference(backward_demodulation,[status(thm)],[f11612,f303]) ).

fof(f11737,plain,
    ( e_868 = e_862
    | i0 = i_881 ),
    inference(backward_demodulation,[status(thm)],[f11612,f286]) ).

fof(f11743,plain,
    ( e_841 = select(a_838,i_881)
    | i1 = i5 ),
    inference(backward_demodulation,[status(thm)],[f11612,f193]) ).

fof(f11757,plain,
    select(a_848,i_881) = e_847,
    inference(backward_demodulation,[status(thm)],[f11612,f130]) ).

fof(f11758,plain,
    e_843 = select(a_844,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f125]) ).

fof(f11760,plain,
    e_879 = select(a_876,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f105]) ).

fof(f11762,plain,
    e_875 = select(a_872,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f103]) ).

fof(f11763,plain,
    e_868 = select(a_865,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f100]) ).

fof(f11765,plain,
    e_864 = select(a_861,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f98]) ).

fof(f11766,plain,
    e_858 = select(a_855,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f96]) ).

fof(f11767,plain,
    e_854 = select(a_851,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f94]) ).

fof(f11768,plain,
    e_841 = select(a_840,i_881),
    inference(backward_demodulation,[status(thm)],[f11612,f88]) ).

fof(f11778,plain,
    ( i1 = i0
    | i0 = i_881
    | e_868 = e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f11689]) ).

fof(f11792,plain,
    ( e_841 = select(a_838,i_881)
    | i1 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f11612,f11743]) ).

fof(f11793,plain,
    ( e_841 = e_837
    | i1 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f9666,f11792]) ).

fof(f11794,plain,
    e_843 = e_847,
    inference(forward_demodulation,[status(thm)],[f9672,f11758]) ).

fof(f11795,plain,
    e_879 = e_875,
    inference(forward_demodulation,[status(thm)],[f9655,f11760]) ).

fof(f11796,plain,
    e_875 = e_873,
    inference(forward_demodulation,[status(thm)],[f9668,f11762]) ).

fof(f11797,plain,
    e_868 = e_866,
    inference(forward_demodulation,[status(thm)],[f9669,f11763]) ).

fof(f11798,plain,
    e_864 = e_837,
    inference(forward_demodulation,[status(thm)],[f9659,f11765]) ).

fof(f11799,plain,
    e_858 = e_854,
    inference(forward_demodulation,[status(thm)],[f9661,f11766]) ).

fof(f11800,plain,
    e_854 = e_852,
    inference(forward_demodulation,[status(thm)],[f9671,f11767]) ).

fof(f11808,plain,
    e_858 != e_875,
    inference(backward_demodulation,[status(thm)],[f11795,f9747]) ).

fof(f11817,plain,
    select(a_869,i_881) = e_866,
    inference(backward_demodulation,[status(thm)],[f11797,f9657]) ).

fof(f11818,plain,
    ( e_873 = e_866
    | i1 = i_881 ),
    inference(backward_demodulation,[status(thm)],[f11797,f9620]) ).

fof(f11821,plain,
    a_838 = store(a_836,i_881,e_864),
    inference(backward_demodulation,[status(thm)],[f11798,f9670]) ).

fof(f11824,plain,
    a_861 = store(a_860,i_881,e_864),
    inference(backward_demodulation,[status(thm)],[f11798,f9662]) ).

fof(f11826,plain,
    e_864 = select(a_836,i1),
    inference(backward_demodulation,[status(thm)],[f11798,f86]) ).

fof(f11838,plain,
    e_858 = e_852,
    inference(backward_demodulation,[status(thm)],[f11800,f11799]) ).

fof(f11842,plain,
    e_858 != e_873,
    inference(forward_demodulation,[status(thm)],[f11796,f11808]) ).

fof(f11852,plain,
    e_852 != e_873,
    inference(backward_demodulation,[status(thm)],[f11838,f11842]) ).

fof(f11855,plain,
    ( e_852 = e_847
    | i1 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f11800,f11733]) ).

fof(f11856,plain,
    ( e_852 = e_843
    | i1 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f11794,f11855]) ).

fof(f11867,plain,
    ( e_866 = e_862
    | i0 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f11797,f11737]) ).

fof(f11869,plain,
    ( e_841 = e_864
    | i1 = i_881 ),
    inference(forward_demodulation,[status(thm)],[f11798,f11793]) ).

fof(f11881,plain,
    select(a_848,i_881) = e_843,
    inference(forward_demodulation,[status(thm)],[f11794,f11757]) ).

fof(f11903,plain,
    ( i1 = i_881
    | e_852 != e_866 ),
    inference(paramodulation,[status(thm)],[f11818,f11852]) ).

fof(f11949,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_852 != e_862 ),
    inference(paramodulation,[status(thm)],[f11867,f11903]) ).

fof(f11993,plain,
    ( i1 = i0
    | i0 = i_881
    | e_866 = e_843 ),
    inference(forward_demodulation,[status(thm)],[f11797,f11778]) ).

fof(f11995,plain,
    ( i1 = i0
    | i0 = i_881
    | i1 = i_881
    | e_852 != e_843 ),
    inference(paramodulation,[status(thm)],[f11993,f11903]) ).

fof(f12000,plain,
    ( i1 = i0
    | i0 = i_881
    | i1 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f11995,f11856]) ).

fof(f12098,plain,
    ( i0 = i_881
    | i1 = i_881
    | select(a_860,i0) = e_839 ),
    inference(paramodulation,[status(thm)],[f12000,f147]) ).

fof(f12102,plain,
    ( i0 = i_881
    | i1 = i_881
    | select(a_840,i0) = e_839 ),
    inference(paramodulation,[status(thm)],[f12000,f119]) ).

fof(f12117,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_843 = e_839 ),
    inference(forward_demodulation,[status(thm)],[f89,f12102]) ).

fof(f12334,plain,
    ( i_881 = i0
    | i0 = i_881
    | i1 = i_881
    | e_862 = e_839 ),
    inference(paramodulation,[status(thm)],[f9629,f12098]) ).

fof(f12340,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_862 = e_839 ),
    inference(duplicate_literals_removal,[status(thm)],[f12334]) ).

fof(f12344,plain,
    ( i0 = i_881
    | i1 = i_881
    | i0 = i_881
    | i1 = i_881
    | e_862 = e_843 ),
    inference(paramodulation,[status(thm)],[f12117,f12340]) ).

fof(f12352,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_862 = e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f12344]) ).

fof(f12365,plain,
    ( i0 = i_881
    | i1 = i_881
    | i0 = i_881
    | i1 = i_881
    | e_852 != e_843 ),
    inference(paramodulation,[status(thm)],[f12352,f11949]) ).

fof(f12374,plain,
    ( i0 = i_881
    | i1 = i_881
    | e_852 != e_843 ),
    inference(duplicate_literals_removal,[status(thm)],[f12365]) ).

fof(f12375,plain,
    ( i0 = i_881
    | i1 = i_881 ),
    inference(forward_subsumption_resolution,[status(thm)],[f12374,f11856]) ).

fof(f12384,plain,
    ( i1 = i_881
    | select(a_865,i_881) = e_864 ),
    inference(paramodulation,[status(thm)],[f12375,f153]) ).

fof(f12389,plain,
    ( i1 = i_881
    | e_843 = select(a_840,i_881) ),
    inference(paramodulation,[status(thm)],[f12375,f89]) ).

fof(f12394,plain,
    ( i1 = i_881
    | e_866 = e_864 ),
    inference(forward_demodulation,[status(thm)],[f9669,f12384]) ).

fof(f12396,plain,
    ( i1 = i_881
    | e_843 = e_841 ),
    inference(forward_demodulation,[status(thm)],[f11768,f12389]) ).

fof(f12404,plain,
    ( i1 = i_881
    | i1 = i_881
    | e_852 != e_864 ),
    inference(paramodulation,[status(thm)],[f12394,f11903]) ).

fof(f12412,plain,
    ( i1 = i_881
    | e_852 != e_864 ),
    inference(duplicate_literals_removal,[status(thm)],[f12404]) ).

fof(f12435,plain,
    ( i1 = i_881
    | i1 = i_881
    | e_852 != e_841 ),
    inference(paramodulation,[status(thm)],[f11869,f12412]) ).

fof(f12437,plain,
    ( i1 = i_881
    | e_852 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f12435]) ).

fof(f12446,plain,
    ( i1 = i_881
    | i1 = i_881
    | e_843 != e_841 ),
    inference(paramodulation,[status(thm)],[f11856,f12437]) ).

fof(f12447,plain,
    ( i1 = i_881
    | e_843 != e_841 ),
    inference(duplicate_literals_removal,[status(thm)],[f12446]) ).

fof(f12448,plain,
    i1 = i_881,
    inference(forward_subsumption_resolution,[status(thm)],[f12447,f12396]) ).

fof(f12491,plain,
    e_864 = select(a_836,i_881),
    inference(backward_demodulation,[status(thm)],[f12448,f11826]) ).

fof(f12516,plain,
    select(a_872,i_881) = e_870,
    inference(backward_demodulation,[status(thm)],[f12448,f161]) ).

fof(f12521,plain,
    select(a_851,i_881) = e_849,
    inference(backward_demodulation,[status(thm)],[f12448,f134]) ).

fof(f12522,plain,
    a_860 = store(a_836,i_881,e_839),
    inference(backward_demodulation,[status(thm)],[f12448,f72]) ).

fof(f12524,plain,
    select(a_840,i_881) = e_839,
    inference(backward_demodulation,[status(thm)],[f12448,f119]) ).

fof(f12527,plain,
    e_870 = select(a_869,i_881),
    inference(backward_demodulation,[status(thm)],[f12448,f101]) ).

fof(f12528,plain,
    a_840 = store(a_838,i_881,e_839),
    inference(backward_demodulation,[status(thm)],[f12448,f61]) ).

fof(f12529,plain,
    e_849 = select(a_848,i_881),
    inference(backward_demodulation,[status(thm)],[f12448,f92]) ).

fof(f12542,plain,
    e_864 = e_839,
    inference(forward_demodulation,[status(thm)],[f9673,f12491]) ).

fof(f12550,plain,
    e_873 = e_870,
    inference(forward_demodulation,[status(thm)],[f9668,f12516]) ).

fof(f12551,plain,
    e_852 = e_849,
    inference(forward_demodulation,[status(thm)],[f9671,f12521]) ).

fof(f12552,plain,
    e_841 = e_839,
    inference(forward_demodulation,[status(thm)],[f11768,f12524]) ).

fof(f12553,plain,
    e_870 = e_866,
    inference(forward_demodulation,[status(thm)],[f11817,f12527]) ).

fof(f12554,plain,
    e_849 = e_843,
    inference(forward_demodulation,[status(thm)],[f11881,f12529]) ).

fof(f12563,plain,
    a_860 = store(a_836,i_881,e_864),
    inference(forward_demodulation,[status(thm)],[f12542,f12522]) ).

fof(f12565,plain,
    a_861 = store(a_838,i_881,e_864),
    inference(backward_demodulation,[status(thm)],[f12568,f11824]) ).

fof(f12568,plain,
    a_860 = a_838,
    inference(forward_demodulation,[status(thm)],[f11821,f12563]) ).

fof(f12569,plain,
    e_841 = e_839,
    inference(backward_demodulation,[status(thm)],[f12577,f12542]) ).

fof(f12575,plain,
    select(a_865,i0) = e_841,
    inference(backward_demodulation,[status(thm)],[f12577,f153]) ).

fof(f12577,plain,
    e_841 = e_864,
    inference(forward_demodulation,[status(thm)],[f12542,f12552]) ).

fof(f12588,plain,
    e_852 != e_866,
    inference(backward_demodulation,[status(thm)],[f12595,f11852]) ).

fof(f12595,plain,
    e_873 = e_866,
    inference(forward_demodulation,[status(thm)],[f12550,f12553]) ).

fof(f12614,plain,
    e_852 = e_843,
    inference(forward_demodulation,[status(thm)],[f12551,f12554]) ).

fof(f12617,plain,
    a_840 = store(a_838,i_881,e_841),
    inference(forward_demodulation,[status(thm)],[f12569,f12528]) ).

fof(f12620,plain,
    e_843 != e_866,
    inference(forward_demodulation,[status(thm)],[f12614,f12588]) ).

fof(f12628,plain,
    a_861 = store(a_838,i_881,e_841),
    inference(forward_demodulation,[status(thm)],[f12577,f12565]) ).

fof(f12631,plain,
    e_862 = select(a_840,i0),
    inference(backward_demodulation,[status(thm)],[f12632,f97]) ).

fof(f12632,plain,
    a_861 = a_840,
    inference(forward_demodulation,[status(thm)],[f12617,f12628]) ).

fof(f12633,plain,
    e_862 = e_843,
    inference(forward_demodulation,[status(thm)],[f89,f12631]) ).

fof(f12642,plain,
    ( e_866 = e_843
    | i0 = i_881 ),
    inference(backward_demodulation,[status(thm)],[f12633,f11867]) ).

fof(f12643,plain,
    i0 = i_881,
    inference(forward_subsumption_resolution,[status(thm)],[f12642,f12620]) ).

fof(f12651,plain,
    e_843 = select(a_840,i_881),
    inference(backward_demodulation,[status(thm)],[f12643,f89]) ).

fof(f12653,plain,
    e_843 = e_841,
    inference(forward_demodulation,[status(thm)],[f11768,f12651]) ).

fof(f12664,plain,
    e_841 != e_866,
    inference(backward_demodulation,[status(thm)],[f12653,f12620]) ).

fof(f12711,plain,
    select(a_865,i_881) = e_841,
    inference(forward_demodulation,[status(thm)],[f12643,f12575]) ).

fof(f12712,plain,
    e_866 = e_841,
    inference(forward_demodulation,[status(thm)],[f9669,f12711]) ).

fof(f12713,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[f12712,f12664]) ).

%------------------------------------------------------------------------------
%----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 -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38  % Computer : n007.cluster.edu
% 0.11/5.38  % Model    : x86_64 x86_64
% 0.11/5.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38  % Memory   : 8046.5625MB
% 0.11/5.38  % OS       : Linux 6.8.0-71-generic
% 0.11/5.38  % CPULimit : 300
% 0.11/5.38  % WCLimit  : 300
% 0.11/5.38  % DateTime : Mon Sep 21 09:01:57 UTC 2026
% 0.11/5.39  % CPUTime  : 
% 0.15/5.40  % Drodi V4.1.1
% 21.25/8.26  % Refutation found
% 21.25/8.26  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.25/8.26  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.86/8.32  % Elapsed time: 2.911857 seconds
% 0.86/8.32  % CPU time: 22.843611 seconds
% 0.86/8.32  % Total memory used: 319.978 MB
% 0.86/8.32  % Net memory used: 307.644 MB
%------------------------------------------------------------------------------