Vampire---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWV512-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 01:16:36 PM UTC 2026

% Result   : Unsatisfiable 15.02s 4.90s
% Output   : Refutation 30.67s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  246
%            Number of leaves      :  247
% Syntax   : Number of formulae    :  678 ( 677 unt;   0 def)
%            Number of atoms       :  679 ( 678 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :  432 ( 431   ~;   1   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    7 (   2 avg)
%            Maximal term depth    :   31 (   4 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :  122 ( 122 usr; 121 con; 0-3 aty)
%            Number of variables   :  560 ( 560   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f5,axiom,
    ! [X2,X3,X0,X1,X4] :
      ( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
      | X0 = X1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).

fof(f6,axiom,
    a_1018 = store(a1,i1,e1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).

fof(f7,axiom,
    a_1019 = store(a_1018,i2,e2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).

fof(f8,axiom,
    a_1020 = store(a_1019,i3,e3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).

fof(f9,axiom,
    a_1021 = store(a_1020,i4,e4),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).

fof(f10,axiom,
    a_1022 = store(a_1021,i5,e5),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).

fof(f11,axiom,
    a_1023 = store(a_1022,i6,e6),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).

fof(f12,axiom,
    a_1024 = store(a_1023,i7,e7),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).

fof(f13,axiom,
    a_1025 = store(a_1024,i8,e8),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).

fof(f14,axiom,
    a_1026 = store(a_1025,i9,e9),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).

fof(f15,axiom,
    a_1027 = store(a_1026,i10,e10),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).

fof(f16,axiom,
    a_1028 = store(a_1027,i11,e11),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).

fof(f17,axiom,
    a_1029 = store(a_1028,i12,e12),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).

fof(f18,axiom,
    a_1030 = store(a_1029,i13,e13),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).

fof(f19,axiom,
    a_1031 = store(a_1030,i14,e14),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).

fof(f20,axiom,
    a_1032 = store(a_1031,i15,e15),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).

fof(f21,axiom,
    a_1033 = store(a_1032,i16,e16),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).

fof(f22,axiom,
    a_1034 = store(a_1033,i17,e17),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).

fof(f23,axiom,
    a_1035 = store(a_1034,i18,e18),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).

fof(f24,axiom,
    a_1036 = store(a_1035,i19,e19),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).

fof(f25,axiom,
    a_1037 = store(a_1036,i20,e20),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).

fof(f26,axiom,
    a_1038 = store(a_1037,i21,e21),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).

fof(f27,axiom,
    a_1039 = store(a_1038,i22,e22),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).

fof(f28,axiom,
    a_1040 = store(a_1039,i23,e23),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).

fof(f29,axiom,
    a_1041 = store(a_1040,i24,e24),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).

fof(f30,axiom,
    a_1042 = store(a_1041,i25,e25),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).

fof(f31,axiom,
    a_1043 = store(a_1042,i26,e26),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).

fof(f32,axiom,
    a_1044 = store(a_1043,i27,e27),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).

fof(f33,axiom,
    a_1045 = store(a_1044,i28,e28),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).

fof(f34,axiom,
    a_1046 = store(a_1045,i29,e29),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).

fof(f35,axiom,
    a_1047 = store(a_1046,i30,e30),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).

fof(f36,axiom,
    a_1048 = store(a1,i13,e13),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).

fof(f37,axiom,
    a_1049 = store(a_1048,i1,e1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).

fof(f38,axiom,
    a_1050 = store(a_1049,i19,e19),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).

fof(f39,axiom,
    a_1051 = store(a_1050,i4,e4),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).

fof(f40,axiom,
    a_1052 = store(a_1051,i9,e9),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).

fof(f41,axiom,
    a_1053 = store(a_1052,i30,e30),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).

fof(f42,axiom,
    a_1054 = store(a_1053,i2,e2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).

fof(f43,axiom,
    a_1055 = store(a_1054,i15,e15),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).

fof(f44,axiom,
    a_1056 = store(a_1055,i25,e25),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).

fof(f45,axiom,
    a_1057 = store(a_1056,i18,e18),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).

fof(f46,axiom,
    a_1058 = store(a_1057,i20,e20),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).

fof(f47,axiom,
    a_1059 = store(a_1058,i8,e8),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).

fof(f48,axiom,
    a_1060 = store(a_1059,i21,e21),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).

fof(f49,axiom,
    a_1061 = store(a_1060,i6,e6),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).

fof(f50,axiom,
    a_1062 = store(a_1061,i11,e11),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).

fof(f51,axiom,
    a_1063 = store(a_1062,i14,e14),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).

fof(f52,axiom,
    a_1064 = store(a_1063,i29,e29),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).

fof(f53,axiom,
    a_1065 = store(a_1064,i5,e5),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).

fof(f54,axiom,
    a_1066 = store(a_1065,i26,e26),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).

fof(f55,axiom,
    a_1067 = store(a_1066,i22,e22),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).

fof(f56,axiom,
    a_1068 = store(a_1067,i27,e27),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).

fof(f57,axiom,
    a_1069 = store(a_1068,i3,e3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).

fof(f58,axiom,
    a_1070 = store(a_1069,i12,e12),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).

fof(f59,axiom,
    a_1071 = store(a_1070,i16,e16),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).

fof(f60,axiom,
    a_1072 = store(a_1071,i28,e28),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).

fof(f61,axiom,
    a_1073 = store(a_1072,i17,e17),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp55) ).

fof(f62,axiom,
    a_1074 = store(a_1073,i23,e23),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).

fof(f63,axiom,
    a_1075 = store(a_1074,i24,e24),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).

fof(f64,axiom,
    a_1076 = store(a_1075,i7,e7),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).

fof(f65,axiom,
    a_1077 = store(a_1076,i10,e10),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).

fof(f66,axiom,
    i29 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).

fof(f67,axiom,
    i28 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).

fof(f68,axiom,
    i28 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).

fof(f69,axiom,
    i27 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).

fof(f70,axiom,
    i27 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).

fof(f72,axiom,
    i26 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).

fof(f73,axiom,
    i26 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).

fof(f76,axiom,
    i25 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).

fof(f81,axiom,
    i24 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).

fof(f82,axiom,
    i24 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp76) ).

fof(f83,axiom,
    i24 != i28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp77) ).

fof(f84,axiom,
    i24 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp78) ).

fof(f85,axiom,
    i24 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp79) ).

fof(f86,axiom,
    i24 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp80) ).

fof(f87,axiom,
    i23 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp81) ).

fof(f88,axiom,
    i23 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp82) ).

fof(f89,axiom,
    i23 != i28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp83) ).

fof(f90,axiom,
    i23 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp84) ).

fof(f91,axiom,
    i23 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp85) ).

fof(f92,axiom,
    i23 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp86) ).

fof(f94,axiom,
    i22 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp88) ).

fof(f95,axiom,
    i22 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp89) ).

fof(f98,axiom,
    i22 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp92) ).

fof(f99,axiom,
    i22 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp93) ).

fof(f102,axiom,
    i21 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp96) ).

fof(f107,axiom,
    i21 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp101) ).

fof(f111,axiom,
    i20 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp105) ).

fof(f116,axiom,
    i20 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp110) ).

fof(f132,axiom,
    i18 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp126) ).

fof(f137,axiom,
    i18 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp131) ).

fof(f143,axiom,
    i18 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp137) ).

fof(f144,axiom,
    i17 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp138) ).

fof(f145,axiom,
    i17 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp139) ).

fof(f146,axiom,
    i17 != i28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp140) ).

fof(f147,axiom,
    i17 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp141) ).

fof(f148,axiom,
    i17 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp142) ).

fof(f149,axiom,
    i17 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp143) ).

fof(f152,axiom,
    i17 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp146) ).

fof(f153,axiom,
    i17 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp147) ).

fof(f154,axiom,
    i17 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp148) ).

fof(f155,axiom,
    i17 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp149) ).

fof(f156,axiom,
    i17 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp150) ).

fof(f157,axiom,
    i16 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp151) ).

fof(f158,axiom,
    i16 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp152) ).

fof(f160,axiom,
    i16 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp154) ).

fof(f161,axiom,
    i16 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp155) ).

fof(f162,axiom,
    i16 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp156) ).

fof(f165,axiom,
    i16 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp159) ).

fof(f166,axiom,
    i16 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp160) ).

fof(f167,axiom,
    i16 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp161) ).

fof(f168,axiom,
    i16 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp162) ).

fof(f169,axiom,
    i16 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp163) ).

fof(f171,axiom,
    i15 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp165) ).

fof(f182,axiom,
    i15 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp176) ).

fof(f186,axiom,
    i14 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp180) ).

fof(f191,axiom,
    i14 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp185) ).

fof(f195,axiom,
    i14 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp189) ).

fof(f196,axiom,
    i14 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp190) ).

fof(f197,axiom,
    i14 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp191) ).

fof(f198,axiom,
    i14 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp192) ).

fof(f201,axiom,
    i14 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp195) ).

fof(f219,axiom,
    i12 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp213) ).

fof(f220,axiom,
    i12 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp214) ).

fof(f222,axiom,
    i12 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp216) ).

fof(f223,axiom,
    i12 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp217) ).

fof(f224,axiom,
    i12 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp218) ).

fof(f227,axiom,
    i12 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp221) ).

fof(f228,axiom,
    i12 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp222) ).

fof(f229,axiom,
    i12 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp223) ).

fof(f230,axiom,
    i12 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp224) ).

fof(f231,axiom,
    i12 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp225) ).

fof(f234,axiom,
    i12 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp228) ).

fof(f235,axiom,
    i12 != i14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp229) ).

fof(f236,axiom,
    i12 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp230) ).

fof(f237,axiom,
    i11 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp231) ).

fof(f242,axiom,
    i11 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp236) ).

fof(f246,axiom,
    i11 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp240) ).

fof(f247,axiom,
    i11 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp241) ).

fof(f248,axiom,
    i11 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp242) ).

fof(f249,axiom,
    i11 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp243) ).

fof(f252,axiom,
    i11 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp246) ).

fof(f254,axiom,
    i11 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp248) ).

fof(f256,axiom,
    i10 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp250) ).

fof(f257,axiom,
    i10 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp251) ).

fof(f258,axiom,
    i10 != i28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp252) ).

fof(f259,axiom,
    i10 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp253) ).

fof(f260,axiom,
    i10 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp254) ).

fof(f261,axiom,
    i10 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp255) ).

fof(f262,axiom,
    i10 != i24,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp256) ).

fof(f263,axiom,
    i10 != i23,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp257) ).

fof(f264,axiom,
    i10 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp258) ).

fof(f265,axiom,
    i10 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp259) ).

fof(f266,axiom,
    i10 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp260) ).

fof(f267,axiom,
    i10 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp261) ).

fof(f268,axiom,
    i10 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp262) ).

fof(f269,axiom,
    i10 != i17,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp263) ).

fof(f270,axiom,
    i10 != i16,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp264) ).

fof(f271,axiom,
    i10 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp265) ).

fof(f272,axiom,
    i10 != i14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp266) ).

fof(f273,axiom,
    i10 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp267) ).

fof(f274,axiom,
    i10 != i12,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp268) ).

fof(f275,axiom,
    i10 != i11,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp269) ).

fof(f287,axiom,
    i9 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp281) ).

fof(f293,axiom,
    i9 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp287) ).

fof(f297,axiom,
    i8 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp291) ).

fof(f302,axiom,
    i8 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp296) ).

fof(f307,axiom,
    i8 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp301) ).

fof(f308,axiom,
    i8 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp302) ).

fof(f309,axiom,
    i8 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp303) ).

fof(f312,axiom,
    i8 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp306) ).

fof(f314,axiom,
    i8 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp308) ).

fof(f318,axiom,
    i8 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp312) ).

fof(f319,axiom,
    i7 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp313) ).

fof(f320,axiom,
    i7 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp314) ).

fof(f321,axiom,
    i7 != i28,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp315) ).

fof(f322,axiom,
    i7 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp316) ).

fof(f323,axiom,
    i7 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp317) ).

fof(f324,axiom,
    i7 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp318) ).

fof(f325,axiom,
    i7 != i24,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp319) ).

fof(f326,axiom,
    i7 != i23,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp320) ).

fof(f327,axiom,
    i7 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp321) ).

fof(f328,axiom,
    i7 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp322) ).

fof(f329,axiom,
    i7 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp323) ).

fof(f330,axiom,
    i7 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp324) ).

fof(f331,axiom,
    i7 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp325) ).

fof(f332,axiom,
    i7 != i17,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp326) ).

fof(f333,axiom,
    i7 != i16,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp327) ).

fof(f334,axiom,
    i7 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp328) ).

fof(f335,axiom,
    i7 != i14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp329) ).

fof(f336,axiom,
    i7 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp330) ).

fof(f337,axiom,
    i7 != i12,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp331) ).

fof(f338,axiom,
    i7 != i11,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp332) ).

fof(f340,axiom,
    i7 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp334) ).

fof(f341,axiom,
    i7 != i8,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp335) ).

fof(f342,axiom,
    i6 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp336) ).

fof(f347,axiom,
    i6 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp341) ).

fof(f351,axiom,
    i6 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp345) ).

fof(f352,axiom,
    i6 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp346) ).

fof(f353,axiom,
    i6 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp347) ).

fof(f354,axiom,
    i6 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp348) ).

fof(f357,axiom,
    i6 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp351) ).

fof(f359,axiom,
    i6 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp353) ).

fof(f363,axiom,
    i6 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp357) ).

fof(f364,axiom,
    i6 != i8,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp358) ).

fof(f366,axiom,
    i5 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp360) ).

fof(f367,axiom,
    i5 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp361) ).

fof(f371,axiom,
    i5 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp365) ).

fof(f375,axiom,
    i5 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp369) ).

fof(f376,axiom,
    i5 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp370) ).

fof(f377,axiom,
    i5 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp371) ).

fof(f378,axiom,
    i5 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp372) ).

fof(f381,axiom,
    i5 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp375) ).

fof(f382,axiom,
    i5 != i14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp376) ).

fof(f383,axiom,
    i5 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp377) ).

fof(f385,axiom,
    i5 != i11,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp379) ).

fof(f387,axiom,
    i5 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp381) ).

fof(f388,axiom,
    i5 != i8,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp382) ).

fof(f390,axiom,
    i5 != i6,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp384) ).

fof(f402,axiom,
    i4 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp396) ).

fof(f408,axiom,
    i4 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp402) ).

fof(f417,axiom,
    i3 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp411) ).

fof(f418,axiom,
    i3 != i29,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp412) ).

fof(f420,axiom,
    i3 != i27,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp414) ).

fof(f421,axiom,
    i3 != i26,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp415) ).

fof(f422,axiom,
    i3 != i25,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp416) ).

fof(f425,axiom,
    i3 != i22,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp419) ).

fof(f426,axiom,
    i3 != i21,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp420) ).

fof(f427,axiom,
    i3 != i20,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp421) ).

fof(f428,axiom,
    i3 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp422) ).

fof(f429,axiom,
    i3 != i18,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp423) ).

fof(f432,axiom,
    i3 != i15,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp426) ).

fof(f433,axiom,
    i3 != i14,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp427) ).

fof(f434,axiom,
    i3 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp428) ).

fof(f436,axiom,
    i3 != i11,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp430) ).

fof(f438,axiom,
    i3 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp432) ).

fof(f439,axiom,
    i3 != i8,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp433) ).

fof(f441,axiom,
    i3 != i6,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp435) ).

fof(f442,axiom,
    i3 != i5,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp436) ).

fof(f443,axiom,
    i3 != i4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp437) ).

fof(f444,axiom,
    i2 != i30,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp438) ).

fof(f455,axiom,
    i2 != i19,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp449) ).

fof(f461,axiom,
    i2 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp455) ).

fof(f465,axiom,
    i2 != i9,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp459) ).

fof(f470,axiom,
    i2 != i4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp464) ).

fof(f489,axiom,
    i1 != i13,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp483) ).

fof(f501,negated_conjecture,
    a_1047 != a_1077,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).

fof(f564,plain,
    ! [X2,X0,X1] : store(store(X0,i29,X1),i30,X2) = store(store(X0,i30,X2),i29,X1),
    inference(unit_resulting_resolution,[],[f5,f66]) ).

fof(f566,plain,
    ! [X2,X0,X1] : store(store(X0,i28,X1),i30,X2) = store(store(X0,i30,X2),i28,X1),
    inference(unit_resulting_resolution,[],[f5,f67]) ).

fof(f568,plain,
    ! [X2,X0,X1] : store(store(X0,i28,X1),i29,X2) = store(store(X0,i29,X2),i28,X1),
    inference(unit_resulting_resolution,[],[f5,f68]) ).

fof(f570,plain,
    ! [X2,X0,X1] : store(store(X0,i27,X1),i30,X2) = store(store(X0,i30,X2),i27,X1),
    inference(unit_resulting_resolution,[],[f5,f69]) ).

fof(f572,plain,
    ! [X2,X0,X1] : store(store(X0,i27,X1),i29,X2) = store(store(X0,i29,X2),i27,X1),
    inference(unit_resulting_resolution,[],[f5,f70]) ).

fof(f576,plain,
    ! [X2,X0,X1] : store(store(X0,i26,X1),i30,X2) = store(store(X0,i30,X2),i26,X1),
    inference(unit_resulting_resolution,[],[f5,f72]) ).

fof(f578,plain,
    ! [X2,X0,X1] : store(store(X0,i26,X1),i29,X2) = store(store(X0,i29,X2),i26,X1),
    inference(unit_resulting_resolution,[],[f5,f73]) ).

fof(f584,plain,
    ! [X2,X0,X1] : store(store(X0,i25,X1),i30,X2) = store(store(X0,i30,X2),i25,X1),
    inference(unit_resulting_resolution,[],[f5,f76]) ).

fof(f594,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i30,X2) = store(store(X0,i30,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f81]) ).

fof(f596,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i29,X2) = store(store(X0,i29,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f82]) ).

fof(f598,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i28,X2) = store(store(X0,i28,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f83]) ).

fof(f600,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i27,X2) = store(store(X0,i27,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f84]) ).

fof(f602,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i26,X2) = store(store(X0,i26,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f85]) ).

fof(f604,plain,
    ! [X2,X0,X1] : store(store(X0,i24,X1),i25,X2) = store(store(X0,i25,X2),i24,X1),
    inference(unit_resulting_resolution,[],[f5,f86]) ).

fof(f606,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i30,X2) = store(store(X0,i30,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f87]) ).

fof(f608,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i29,X2) = store(store(X0,i29,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f88]) ).

fof(f610,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i28,X2) = store(store(X0,i28,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f89]) ).

fof(f612,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i27,X2) = store(store(X0,i27,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f90]) ).

fof(f614,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i26,X2) = store(store(X0,i26,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f91]) ).

fof(f616,plain,
    ! [X2,X0,X1] : store(store(X0,i23,X1),i25,X2) = store(store(X0,i25,X2),i23,X1),
    inference(unit_resulting_resolution,[],[f5,f92]) ).

fof(f620,plain,
    ! [X2,X0,X1] : store(store(X0,i22,X1),i30,X2) = store(store(X0,i30,X2),i22,X1),
    inference(unit_resulting_resolution,[],[f5,f94]) ).

fof(f622,plain,
    ! [X2,X0,X1] : store(store(X0,i22,X1),i29,X2) = store(store(X0,i29,X2),i22,X1),
    inference(unit_resulting_resolution,[],[f5,f95]) ).

fof(f628,plain,
    ! [X2,X0,X1] : store(store(X0,i22,X1),i26,X2) = store(store(X0,i26,X2),i22,X1),
    inference(unit_resulting_resolution,[],[f5,f98]) ).

fof(f630,plain,
    ! [X2,X0,X1] : store(store(X0,i22,X1),i25,X2) = store(store(X0,i25,X2),i22,X1),
    inference(unit_resulting_resolution,[],[f5,f99]) ).

fof(f636,plain,
    ! [X2,X0,X1] : store(store(X0,i21,X1),i30,X2) = store(store(X0,i30,X2),i21,X1),
    inference(unit_resulting_resolution,[],[f5,f102]) ).

fof(f646,plain,
    ! [X2,X0,X1] : store(store(X0,i21,X1),i25,X2) = store(store(X0,i25,X2),i21,X1),
    inference(unit_resulting_resolution,[],[f5,f107]) ).

fof(f654,plain,
    ! [X2,X0,X1] : store(store(X0,i20,X1),i30,X2) = store(store(X0,i30,X2),i20,X1),
    inference(unit_resulting_resolution,[],[f5,f111]) ).

fof(f664,plain,
    ! [X2,X0,X1] : store(store(X0,i20,X1),i25,X2) = store(store(X0,i25,X2),i20,X1),
    inference(unit_resulting_resolution,[],[f5,f116]) ).

fof(f696,plain,
    ! [X2,X0,X1] : store(store(X0,i18,X1),i30,X2) = store(store(X0,i30,X2),i18,X1),
    inference(unit_resulting_resolution,[],[f5,f132]) ).

fof(f706,plain,
    ! [X2,X0,X1] : store(store(X0,i18,X1),i25,X2) = store(store(X0,i25,X2),i18,X1),
    inference(unit_resulting_resolution,[],[f5,f137]) ).

fof(f718,plain,
    ! [X2,X0,X1] : store(store(X0,i18,X1),i19,X2) = store(store(X0,i19,X2),i18,X1),
    inference(unit_resulting_resolution,[],[f5,f143]) ).

fof(f720,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i30,X2) = store(store(X0,i30,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f144]) ).

fof(f722,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i29,X2) = store(store(X0,i29,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f145]) ).

fof(f724,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i28,X2) = store(store(X0,i28,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f146]) ).

fof(f726,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i27,X2) = store(store(X0,i27,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f147]) ).

fof(f728,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i26,X2) = store(store(X0,i26,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f148]) ).

fof(f730,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i25,X2) = store(store(X0,i25,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f149]) ).

fof(f736,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i22,X2) = store(store(X0,i22,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f152]) ).

fof(f738,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i21,X2) = store(store(X0,i21,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f153]) ).

fof(f740,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i20,X2) = store(store(X0,i20,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f154]) ).

fof(f742,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i19,X2) = store(store(X0,i19,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f155]) ).

fof(f744,plain,
    ! [X2,X0,X1] : store(store(X0,i17,X1),i18,X2) = store(store(X0,i18,X2),i17,X1),
    inference(unit_resulting_resolution,[],[f5,f156]) ).

fof(f746,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i30,X2) = store(store(X0,i30,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f157]) ).

fof(f748,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i29,X2) = store(store(X0,i29,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f158]) ).

fof(f752,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i27,X2) = store(store(X0,i27,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f160]) ).

fof(f754,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i26,X2) = store(store(X0,i26,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f161]) ).

fof(f756,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i25,X2) = store(store(X0,i25,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f162]) ).

fof(f762,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i22,X2) = store(store(X0,i22,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f165]) ).

fof(f764,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i21,X2) = store(store(X0,i21,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f166]) ).

fof(f766,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i20,X2) = store(store(X0,i20,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f167]) ).

fof(f768,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i19,X2) = store(store(X0,i19,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f168]) ).

fof(f770,plain,
    ! [X2,X0,X1] : store(store(X0,i16,X1),i18,X2) = store(store(X0,i18,X2),i16,X1),
    inference(unit_resulting_resolution,[],[f5,f169]) ).

fof(f774,plain,
    ! [X2,X0,X1] : store(store(X0,i15,X1),i30,X2) = store(store(X0,i30,X2),i15,X1),
    inference(unit_resulting_resolution,[],[f5,f171]) ).

fof(f796,plain,
    ! [X2,X0,X1] : store(store(X0,i15,X1),i19,X2) = store(store(X0,i19,X2),i15,X1),
    inference(unit_resulting_resolution,[],[f5,f182]) ).

fof(f804,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i30,X2) = store(store(X0,i30,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f186]) ).

fof(f814,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i25,X2) = store(store(X0,i25,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f191]) ).

fof(f822,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i21,X2) = store(store(X0,i21,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f195]) ).

fof(f824,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i20,X2) = store(store(X0,i20,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f196]) ).

fof(f826,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i19,X2) = store(store(X0,i19,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f197]) ).

fof(f828,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i18,X2) = store(store(X0,i18,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f198]) ).

fof(f834,plain,
    ! [X2,X0,X1] : store(store(X0,i14,X1),i15,X2) = store(store(X0,i15,X2),i14,X1),
    inference(unit_resulting_resolution,[],[f5,f201]) ).

fof(f870,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i30,X2) = store(store(X0,i30,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f219]) ).

fof(f872,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i29,X2) = store(store(X0,i29,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f220]) ).

fof(f876,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i27,X2) = store(store(X0,i27,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f222]) ).

fof(f878,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i26,X2) = store(store(X0,i26,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f223]) ).

fof(f880,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i25,X2) = store(store(X0,i25,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f224]) ).

fof(f886,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i22,X2) = store(store(X0,i22,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f227]) ).

fof(f888,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i21,X2) = store(store(X0,i21,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f228]) ).

fof(f890,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i20,X2) = store(store(X0,i20,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f229]) ).

fof(f892,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i19,X2) = store(store(X0,i19,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f230]) ).

fof(f894,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i18,X2) = store(store(X0,i18,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f231]) ).

fof(f900,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i15,X2) = store(store(X0,i15,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f234]) ).

fof(f902,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i14,X2) = store(store(X0,i14,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f235]) ).

fof(f904,plain,
    ! [X2,X0,X1] : store(store(X0,i12,X1),i13,X2) = store(store(X0,i13,X2),i12,X1),
    inference(unit_resulting_resolution,[],[f5,f236]) ).

fof(f906,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i30,X2) = store(store(X0,i30,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f237]) ).

fof(f916,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i25,X2) = store(store(X0,i25,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f242]) ).

fof(f924,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i21,X2) = store(store(X0,i21,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f246]) ).

fof(f926,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i20,X2) = store(store(X0,i20,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f247]) ).

fof(f928,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i19,X2) = store(store(X0,i19,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f248]) ).

fof(f930,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i18,X2) = store(store(X0,i18,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f249]) ).

fof(f936,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i15,X2) = store(store(X0,i15,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f252]) ).

fof(f940,plain,
    ! [X2,X0,X1] : store(store(X0,i11,X1),i13,X2) = store(store(X0,i13,X2),i11,X1),
    inference(unit_resulting_resolution,[],[f5,f254]) ).

fof(f944,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i30,X2) = store(store(X0,i30,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f256]) ).

fof(f946,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i29,X2) = store(store(X0,i29,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f257]) ).

fof(f948,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i28,X2) = store(store(X0,i28,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f258]) ).

fof(f950,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i27,X2) = store(store(X0,i27,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f259]) ).

fof(f952,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i26,X2) = store(store(X0,i26,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f260]) ).

fof(f954,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i25,X2) = store(store(X0,i25,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f261]) ).

fof(f956,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i24,X2) = store(store(X0,i24,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f262]) ).

fof(f958,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i23,X2) = store(store(X0,i23,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f263]) ).

fof(f960,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i22,X2) = store(store(X0,i22,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f264]) ).

fof(f962,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i21,X2) = store(store(X0,i21,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f265]) ).

fof(f964,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i20,X2) = store(store(X0,i20,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f266]) ).

fof(f966,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i19,X2) = store(store(X0,i19,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f267]) ).

fof(f968,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i18,X2) = store(store(X0,i18,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f268]) ).

fof(f970,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i17,X2) = store(store(X0,i17,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f269]) ).

fof(f972,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i16,X2) = store(store(X0,i16,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f270]) ).

fof(f974,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i15,X2) = store(store(X0,i15,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f271]) ).

fof(f976,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i14,X2) = store(store(X0,i14,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f272]) ).

fof(f978,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i13,X2) = store(store(X0,i13,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f273]) ).

fof(f980,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i12,X2) = store(store(X0,i12,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f274]) ).

fof(f982,plain,
    ! [X2,X0,X1] : store(store(X0,i10,X1),i11,X2) = store(store(X0,i11,X2),i10,X1),
    inference(unit_resulting_resolution,[],[f5,f275]) ).

fof(f1006,plain,
    ! [X2,X0,X1] : store(store(X0,i9,X1),i19,X2) = store(store(X0,i19,X2),i9,X1),
    inference(unit_resulting_resolution,[],[f5,f287]) ).

fof(f1018,plain,
    ! [X2,X0,X1] : store(store(X0,i9,X1),i13,X2) = store(store(X0,i13,X2),i9,X1),
    inference(unit_resulting_resolution,[],[f5,f293]) ).

fof(f1026,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i30,X2) = store(store(X0,i30,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f297]) ).

fof(f1036,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i25,X2) = store(store(X0,i25,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f302]) ).

fof(f1046,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i20,X2) = store(store(X0,i20,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f307]) ).

fof(f1048,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i19,X2) = store(store(X0,i19,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f308]) ).

fof(f1050,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i18,X2) = store(store(X0,i18,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f309]) ).

fof(f1056,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i15,X2) = store(store(X0,i15,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f312]) ).

fof(f1060,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i13,X2) = store(store(X0,i13,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f314]) ).

fof(f1068,plain,
    ! [X2,X0,X1] : store(store(X0,i8,X1),i9,X2) = store(store(X0,i9,X2),i8,X1),
    inference(unit_resulting_resolution,[],[f5,f318]) ).

fof(f1070,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i30,X2) = store(store(X0,i30,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f319]) ).

fof(f1072,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i29,X2) = store(store(X0,i29,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f320]) ).

fof(f1074,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i28,X2) = store(store(X0,i28,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f321]) ).

fof(f1076,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i27,X2) = store(store(X0,i27,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f322]) ).

fof(f1078,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i26,X2) = store(store(X0,i26,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f323]) ).

fof(f1080,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i25,X2) = store(store(X0,i25,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f324]) ).

fof(f1082,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i24,X2) = store(store(X0,i24,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f325]) ).

fof(f1084,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i23,X2) = store(store(X0,i23,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f326]) ).

fof(f1086,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i22,X2) = store(store(X0,i22,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f327]) ).

fof(f1088,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i21,X2) = store(store(X0,i21,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f328]) ).

fof(f1090,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i20,X2) = store(store(X0,i20,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f329]) ).

fof(f1092,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i19,X2) = store(store(X0,i19,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f330]) ).

fof(f1094,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i18,X2) = store(store(X0,i18,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f331]) ).

fof(f1096,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i17,X2) = store(store(X0,i17,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f332]) ).

fof(f1098,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i16,X2) = store(store(X0,i16,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f333]) ).

fof(f1100,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i15,X2) = store(store(X0,i15,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f334]) ).

fof(f1102,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i14,X2) = store(store(X0,i14,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f335]) ).

fof(f1104,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i13,X2) = store(store(X0,i13,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f336]) ).

fof(f1106,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i12,X2) = store(store(X0,i12,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f337]) ).

fof(f1108,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i11,X2) = store(store(X0,i11,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f338]) ).

fof(f1112,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i9,X2) = store(store(X0,i9,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f340]) ).

fof(f1114,plain,
    ! [X2,X0,X1] : store(store(X0,i7,X1),i8,X2) = store(store(X0,i8,X2),i7,X1),
    inference(unit_resulting_resolution,[],[f5,f341]) ).

fof(f1116,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i30,X2) = store(store(X0,i30,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f342]) ).

fof(f1126,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i25,X2) = store(store(X0,i25,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f347]) ).

fof(f1134,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i21,X2) = store(store(X0,i21,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f351]) ).

fof(f1136,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i20,X2) = store(store(X0,i20,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f352]) ).

fof(f1138,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i19,X2) = store(store(X0,i19,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f353]) ).

fof(f1140,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i18,X2) = store(store(X0,i18,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f354]) ).

fof(f1146,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i15,X2) = store(store(X0,i15,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f357]) ).

fof(f1150,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i13,X2) = store(store(X0,i13,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f359]) ).

fof(f1158,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i9,X2) = store(store(X0,i9,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f363]) ).

fof(f1160,plain,
    ! [X2,X0,X1] : store(store(X0,i6,X1),i8,X2) = store(store(X0,i8,X2),i6,X1),
    inference(unit_resulting_resolution,[],[f5,f364]) ).

fof(f1164,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i30,X2) = store(store(X0,i30,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f366]) ).

fof(f1166,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i29,X2) = store(store(X0,i29,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f367]) ).

fof(f1174,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i25,X2) = store(store(X0,i25,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f371]) ).

fof(f1182,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i21,X2) = store(store(X0,i21,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f375]) ).

fof(f1184,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i20,X2) = store(store(X0,i20,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f376]) ).

fof(f1186,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i19,X2) = store(store(X0,i19,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f377]) ).

fof(f1188,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i18,X2) = store(store(X0,i18,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f378]) ).

fof(f1194,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i15,X2) = store(store(X0,i15,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f381]) ).

fof(f1196,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i14,X2) = store(store(X0,i14,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f382]) ).

fof(f1198,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i13,X2) = store(store(X0,i13,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f383]) ).

fof(f1202,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i11,X2) = store(store(X0,i11,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f385]) ).

fof(f1206,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i9,X2) = store(store(X0,i9,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f387]) ).

fof(f1208,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i8,X2) = store(store(X0,i8,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f388]) ).

fof(f1212,plain,
    ! [X2,X0,X1] : store(store(X0,i5,X1),i6,X2) = store(store(X0,i6,X2),i5,X1),
    inference(unit_resulting_resolution,[],[f5,f390]) ).

fof(f1236,plain,
    ! [X2,X0,X1] : store(store(X0,i4,X1),i19,X2) = store(store(X0,i19,X2),i4,X1),
    inference(unit_resulting_resolution,[],[f5,f402]) ).

fof(f1248,plain,
    ! [X2,X0,X1] : store(store(X0,i4,X1),i13,X2) = store(store(X0,i13,X2),i4,X1),
    inference(unit_resulting_resolution,[],[f5,f408]) ).

fof(f1266,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i30,X2) = store(store(X0,i30,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f417]) ).

fof(f1268,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i29,X2) = store(store(X0,i29,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f418]) ).

fof(f1272,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i27,X2) = store(store(X0,i27,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f420]) ).

fof(f1274,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i26,X2) = store(store(X0,i26,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f421]) ).

fof(f1276,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i25,X2) = store(store(X0,i25,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f422]) ).

fof(f1282,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i22,X2) = store(store(X0,i22,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f425]) ).

fof(f1284,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i21,X2) = store(store(X0,i21,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f426]) ).

fof(f1286,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i20,X2) = store(store(X0,i20,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f427]) ).

fof(f1288,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i19,X2) = store(store(X0,i19,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f428]) ).

fof(f1290,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i18,X2) = store(store(X0,i18,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f429]) ).

fof(f1296,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i15,X2) = store(store(X0,i15,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f432]) ).

fof(f1298,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i14,X2) = store(store(X0,i14,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f433]) ).

fof(f1300,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i13,X2) = store(store(X0,i13,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f434]) ).

fof(f1304,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i11,X2) = store(store(X0,i11,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f436]) ).

fof(f1308,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i9,X2) = store(store(X0,i9,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f438]) ).

fof(f1310,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i8,X2) = store(store(X0,i8,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f439]) ).

fof(f1314,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i6,X2) = store(store(X0,i6,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f441]) ).

fof(f1316,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i5,X2) = store(store(X0,i5,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f442]) ).

fof(f1318,plain,
    ! [X2,X0,X1] : store(store(X0,i3,X1),i4,X2) = store(store(X0,i4,X2),i3,X1),
    inference(unit_resulting_resolution,[],[f5,f443]) ).

fof(f1320,plain,
    ! [X2,X0,X1] : store(store(X0,i2,X1),i30,X2) = store(store(X0,i30,X2),i2,X1),
    inference(unit_resulting_resolution,[],[f5,f444]) ).

fof(f1342,plain,
    ! [X2,X0,X1] : store(store(X0,i2,X1),i19,X2) = store(store(X0,i19,X2),i2,X1),
    inference(unit_resulting_resolution,[],[f5,f455]) ).

fof(f1354,plain,
    ! [X2,X0,X1] : store(store(X0,i2,X1),i13,X2) = store(store(X0,i13,X2),i2,X1),
    inference(unit_resulting_resolution,[],[f5,f461]) ).

fof(f1362,plain,
    ! [X2,X0,X1] : store(store(X0,i2,X1),i9,X2) = store(store(X0,i9,X2),i2,X1),
    inference(unit_resulting_resolution,[],[f5,f465]) ).

fof(f1372,plain,
    ! [X2,X0,X1] : store(store(X0,i2,X1),i4,X2) = store(store(X0,i4,X2),i2,X1),
    inference(unit_resulting_resolution,[],[f5,f470]) ).

fof(f1410,plain,
    ! [X2,X0,X1] : store(store(X0,i1,X1),i13,X2) = store(store(X0,i13,X2),i1,X1),
    inference(unit_resulting_resolution,[],[f5,f489]) ).

fof(f1524,plain,
    a_1047 != store(a_1076,i10,e10),
    inference(superposition,[],[f501,f65]) ).

fof(f1525,plain,
    a_1047 != store(store(a_1075,i7,e7),i10,e10),
    inference(forward_demodulation,[],[f1524,f64]) ).

fof(f1526,plain,
    a_1047 != store(store(store(a_1074,i24,e24),i7,e7),i10,e10),
    inference(forward_demodulation,[],[f1525,f63]) ).

fof(f1527,plain,
    a_1047 != store(store(store(a_1074,i7,e7),i24,e24),i10,e10),
    inference(forward_demodulation,[],[f1526,f1082]) ).

fof(f1528,plain,
    a_1047 != store(store(store(a_1074,i7,e7),i10,e10),i24,e24),
    inference(forward_demodulation,[],[f1527,f956]) ).

fof(f1529,plain,
    a_1047 != store(store(store(store(a_1073,i23,e23),i7,e7),i10,e10),i24,e24),
    inference(forward_demodulation,[],[f1528,f62]) ).

fof(f1530,plain,
    a_1047 != store(store(store(store(a_1073,i7,e7),i23,e23),i10,e10),i24,e24),
    inference(forward_demodulation,[],[f1529,f1084]) ).

fof(f1531,plain,
    a_1047 != store(store(store(store(a_1073,i7,e7),i10,e10),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1530,f958]) ).

fof(f1532,plain,
    a_1047 != store(store(store(store(store(a_1072,i17,e17),i7,e7),i10,e10),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1531,f61]) ).

fof(f1533,plain,
    a_1047 != store(store(store(store(store(a_1072,i7,e7),i17,e17),i10,e10),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1532,f1096]) ).

fof(f1534,plain,
    a_1047 != store(store(store(store(store(a_1072,i7,e7),i10,e10),i17,e17),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1533,f970]) ).

fof(f1535,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i28,e28),i7,e7),i10,e10),i17,e17),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1534,f60]) ).

fof(f1536,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i7,e7),i28,e28),i10,e10),i17,e17),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1535,f1074]) ).

fof(f1537,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i7,e7),i10,e10),i28,e28),i17,e17),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1536,f948]) ).

fof(f1538,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i7,e7),i10,e10),i17,e17),i28,e28),i23,e23),i24,e24),
    inference(forward_demodulation,[],[f1537,f724]) ).

fof(f1539,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i7,e7),i10,e10),i17,e17),i23,e23),i28,e28),i24,e24),
    inference(forward_demodulation,[],[f1538,f610]) ).

fof(f1540,plain,
    a_1047 != store(store(store(store(store(store(a_1071,i7,e7),i10,e10),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1539,f598]) ).

fof(f1541,plain,
    a_1047 != store(store(store(store(store(store(store(a_1070,i16,e16),i7,e7),i10,e10),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1540,f59]) ).

fof(f1542,plain,
    a_1047 != store(store(store(store(store(store(store(a_1070,i7,e7),i16,e16),i10,e10),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1541,f1098]) ).

fof(f1543,plain,
    a_1047 != store(store(store(store(store(store(store(a_1070,i7,e7),i10,e10),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1542,f972]) ).

fof(f1544,plain,
    a_1047 != store(store(store(store(store(store(store(store(a_1069,i12,e12),i7,e7),i10,e10),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1543,f58]) ).

fof(f1545,plain,
    a_1047 != store(store(store(store(store(store(store(store(a_1069,i7,e7),i12,e12),i10,e10),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1544,f1106]) ).

fof(f1546,plain,
    a_1047 != store(store(store(store(store(store(store(store(a_1069,i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1545,f980]) ).

fof(f1547,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(a_1068,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1546,f57]) ).

fof(f1548,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i27,e27),i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1547,f56]) ).

fof(f1549,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i27,e27),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1548,f1272]) ).

fof(f1550,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i27,e27),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1549,f1076]) ).

fof(f1551,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i27,e27),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1550,f950]) ).

fof(f1552,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i12,e12),i27,e27),i16,e16),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1551,f876]) ).

fof(f1553,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i27,e27),i17,e17),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1552,f752]) ).

fof(f1554,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i27,e27),i23,e23),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1553,f726]) ).

fof(f1555,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i27,e27),i24,e24),i28,e28),
    inference(forward_demodulation,[],[f1554,f612]) ).

fof(f1556,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1067,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1555,f600]) ).

fof(f1557,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i22,e22),i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1556,f55]) ).

fof(f1558,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i22,e22),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1557,f1282]) ).

fof(f1559,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i7,e7),i22,e22),i10,e10),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1558,f1086]) ).

fof(f1560,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i7,e7),i10,e10),i22,e22),i12,e12),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1559,f960]) ).

fof(f1561,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i7,e7),i10,e10),i12,e12),i22,e22),i16,e16),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1560,f886]) ).

fof(f1562,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i22,e22),i17,e17),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1561,f762]) ).

fof(f1563,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1066,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1562,f736]) ).

fof(f1564,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i26,e26),i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1563,f54]) ).

fof(f1565,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i26,e26),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1564,f1274]) ).

fof(f1566,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i26,e26),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1565,f1078]) ).

fof(f1567,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i26,e26),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1566,f952]) ).

fof(f1568,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i26,e26),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1567,f878]) ).

fof(f1569,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i26,e26),i17,e17),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1568,f754]) ).

fof(f1570,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i26,e26),i22,e22),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1569,f728]) ).

fof(f1571,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i26,e26),i23,e23),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1570,f628]) ).

fof(f1572,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i26,e26),i24,e24),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1571,f614]) ).

fof(f1573,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1065,i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1572,f602]) ).

fof(f1574,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(a_1064,i5,e5),i3,e3),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1573,f53]) ).

fof(f1575,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(a_1064,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1574,f1316]) ).

fof(f1576,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i29,e29),i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1575,f52]) ).

fof(f1577,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i29,e29),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1576,f1268]) ).

fof(f1578,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i29,e29),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1577,f1166]) ).

fof(f1579,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i29,e29),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1578,f1072]) ).

fof(f1580,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i29,e29),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1579,f946]) ).

fof(f1581,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i29,e29),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1580,f872]) ).

fof(f1582,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i29,e29),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1581,f748]) ).

fof(f1583,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i29,e29),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1582,f722]) ).

fof(f1584,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i29,e29),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1583,f622]) ).

fof(f1585,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i29,e29),i24,e24),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1584,f608]) ).

fof(f1586,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i29,e29),i26,e26),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1585,f596]) ).

fof(f1587,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i29,e29),i27,e27),i28,e28),
    inference(forward_demodulation,[],[f1586,f578]) ).

fof(f1588,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i29,e29),i28,e28),
    inference(forward_demodulation,[],[f1587,f572]) ).

fof(f1589,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1063,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1588,f568]) ).

fof(f1590,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i14,e14),i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1589,f51]) ).

fof(f1591,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i3,e3),i14,e14),i5,e5),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1590,f1298]) ).

fof(f1592,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i3,e3),i5,e5),i14,e14),i7,e7),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1591,f1196]) ).

fof(f1593,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i3,e3),i5,e5),i7,e7),i14,e14),i10,e10),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1592,f1102]) ).

fof(f1594,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i3,e3),i5,e5),i7,e7),i10,e10),i14,e14),i12,e12),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1593,f976]) ).

fof(f1595,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1062,i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1594,f902]) ).

fof(f1596,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1061,i11,e11),i3,e3),i5,e5),i7,e7),i10,e10),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1595,f50]) ).

fof(f1597,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1061,i3,e3),i11,e11),i5,e5),i7,e7),i10,e10),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1596,f1304]) ).

fof(f1598,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1061,i3,e3),i5,e5),i11,e11),i7,e7),i10,e10),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1597,f1202]) ).

fof(f1599,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1061,i3,e3),i5,e5),i7,e7),i11,e11),i10,e10),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1598,f1108]) ).

fof(f1600,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1061,i3,e3),i5,e5),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1599,f982]) ).

fof(f1601,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1060,i6,e6),i3,e3),i5,e5),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1600,f49]) ).

fof(f1602,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1060,i3,e3),i6,e6),i5,e5),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1601,f1314]) ).

fof(f1603,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1060,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1602,f1212]) ).

fof(f1604,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i21,e21),i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1603,f48]) ).

fof(f1605,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i21,e21),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1604,f1284]) ).

fof(f1606,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i21,e21),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1605,f1182]) ).

fof(f1607,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i21,e21),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1606,f1134]) ).

fof(f1608,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i21,e21),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1607,f1088]) ).

fof(f1609,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i21,e21),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1608,f962]) ).

fof(f1610,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i21,e21),i12,e12),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1609,f924]) ).

fof(f1611,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i21,e21),i14,e14),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1610,f888]) ).

fof(f1612,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i21,e21),i16,e16),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1611,f822]) ).

fof(f1613,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i21,e21),i17,e17),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1612,f764]) ).

fof(f1614,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1059,i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1613,f738]) ).

fof(f1615,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1058,i8,e8),i3,e3),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1614,f47]) ).

fof(f1616,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1058,i3,e3),i8,e8),i5,e5),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1615,f1310]) ).

fof(f1617,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1058,i3,e3),i5,e5),i8,e8),i6,e6),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1616,f1208]) ).

fof(f1618,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1058,i3,e3),i5,e5),i6,e6),i8,e8),i7,e7),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1617,f1160]) ).

fof(f1619,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1058,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1618,f1114]) ).

fof(f1620,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i20,e20),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1619,f46]) ).

fof(f1621,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i20,e20),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1620,f1286]) ).

fof(f1622,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i20,e20),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1621,f1184]) ).

fof(f1623,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i20,e20),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1622,f1136]) ).

fof(f1624,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i20,e20),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1623,f1090]) ).

fof(f1625,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i20,e20),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1624,f1046]) ).

fof(f1626,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i20,e20),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1625,f964]) ).

fof(f1627,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i20,e20),i12,e12),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1626,f926]) ).

fof(f1628,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i20,e20),i14,e14),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1627,f890]) ).

fof(f1629,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i20,e20),i16,e16),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1628,f824]) ).

fof(f1630,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i20,e20),i17,e17),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1629,f766]) ).

fof(f1631,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1057,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1630,f740]) ).

fof(f1632,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i18,e18),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1631,f45]) ).

fof(f1633,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i18,e18),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1632,f1290]) ).

fof(f1634,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i18,e18),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1633,f1188]) ).

fof(f1635,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i18,e18),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1634,f1140]) ).

fof(f1636,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i18,e18),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1635,f1094]) ).

fof(f1637,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i18,e18),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1636,f1050]) ).

fof(f1638,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i18,e18),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1637,f968]) ).

fof(f1639,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i18,e18),i12,e12),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1638,f930]) ).

fof(f1640,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i18,e18),i14,e14),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1639,f894]) ).

fof(f1641,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i18,e18),i16,e16),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1640,f828]) ).

fof(f1642,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i18,e18),i17,e17),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1641,f770]) ).

fof(f1643,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1056,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1642,f744]) ).

fof(f1644,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i25,e25),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1643,f44]) ).

fof(f1645,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i25,e25),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1644,f1276]) ).

fof(f1646,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i25,e25),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1645,f1174]) ).

fof(f1647,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i25,e25),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1646,f1126]) ).

fof(f1648,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i25,e25),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1647,f1080]) ).

fof(f1649,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i25,e25),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1648,f1036]) ).

fof(f1650,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i25,e25),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1649,f954]) ).

fof(f1651,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i25,e25),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1650,f916]) ).

fof(f1652,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i25,e25),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1651,f880]) ).

fof(f1653,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i25,e25),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1652,f814]) ).

fof(f1654,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i25,e25),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1653,f756]) ).

fof(f1655,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i25,e25),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1654,f730]) ).

fof(f1656,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i25,e25),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1655,f706]) ).

fof(f1657,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i25,e25),i21,e21),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1656,f664]) ).

fof(f1658,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i25,e25),i22,e22),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1657,f646]) ).

fof(f1659,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i25,e25),i23,e23),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1658,f630]) ).

fof(f1660,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i25,e25),i24,e24),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1659,f616]) ).

fof(f1661,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1055,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1660,f604]) ).

fof(f1662,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i15,e15),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1661,f43]) ).

fof(f1663,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i15,e15),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1662,f1296]) ).

fof(f1664,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i15,e15),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1663,f1194]) ).

fof(f1665,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i15,e15),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1664,f1146]) ).

fof(f1666,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i15,e15),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1665,f1100]) ).

fof(f1667,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i15,e15),i10,e10),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1666,f1056]) ).

fof(f1668,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i15,e15),i11,e11),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1667,f974]) ).

fof(f1669,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i15,e15),i12,e12),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1668,f936]) ).

fof(f1670,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i15,e15),i14,e14),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1669,f900]) ).

fof(f1671,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1054,i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1670,f834]) ).

fof(f1672,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1671,f42]) ).

fof(f1673,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i30,e30),i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1672,f41]) ).

fof(f1674,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i30,e30),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1673,f1320]) ).

fof(f1675,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i30,e30),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1674,f1266]) ).

fof(f1676,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i30,e30),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1675,f1164]) ).

fof(f1677,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i30,e30),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1676,f1116]) ).

fof(f1678,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i30,e30),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1677,f1070]) ).

fof(f1679,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i30,e30),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1678,f1026]) ).

fof(f1680,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i30,e30),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1679,f944]) ).

fof(f1681,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i30,e30),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1680,f906]) ).

fof(f1682,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i30,e30),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1681,f870]) ).

fof(f1683,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i30,e30),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1682,f804]) ).

fof(f1684,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i30,e30),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1683,f774]) ).

fof(f1685,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i30,e30),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1684,f746]) ).

fof(f1686,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i30,e30),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1685,f720]) ).

fof(f1687,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i30,e30),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1686,f696]) ).

fof(f1688,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i30,e30),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1687,f654]) ).

fof(f1689,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i30,e30),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1688,f636]) ).

fof(f1690,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i30,e30),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1689,f620]) ).

fof(f1691,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i30,e30),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1690,f606]) ).

fof(f1692,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i30,e30),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1691,f594]) ).

fof(f1693,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i30,e30),i26,e26),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1692,f584]) ).

fof(f1694,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i30,e30),i27,e27),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1693,f576]) ).

fof(f1695,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i30,e30),i28,e28),i29,e29),
    inference(forward_demodulation,[],[f1694,f570]) ).

fof(f1696,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i30,e30),i29,e29),
    inference(forward_demodulation,[],[f1695,f566]) ).

fof(f1697,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1052,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1696,f564]) ).

fof(f1698,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i9,e9),i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1697,f40]) ).

fof(f1699,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i9,e9),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1698,f1362]) ).

fof(f1700,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i3,e3),i9,e9),i5,e5),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1699,f1308]) ).

fof(f1701,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i3,e3),i5,e5),i9,e9),i6,e6),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1700,f1206]) ).

fof(f1702,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i3,e3),i5,e5),i6,e6),i9,e9),i7,e7),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1701,f1158]) ).

fof(f1703,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i9,e9),i8,e8),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1702,f1112]) ).

fof(f1704,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1051,i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1703,f1068]) ).

fof(f1705,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1050,i4,e4),i2,e2),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1704,f39]) ).

fof(f1706,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1050,i2,e2),i4,e4),i3,e3),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1705,f1372]) ).

fof(f1707,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1050,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1706,f1318]) ).

fof(f1708,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i19,e19),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1707,f38]) ).

fof(f1709,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i19,e19),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1708,f1342]) ).

fof(f1710,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i19,e19),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1709,f1288]) ).

fof(f1711,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i19,e19),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1710,f1236]) ).

fof(f1712,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i19,e19),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1711,f1186]) ).

fof(f1713,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i19,e19),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1712,f1138]) ).

fof(f1714,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i19,e19),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1713,f1092]) ).

fof(f1715,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i19,e19),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1714,f1048]) ).

fof(f1716,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i19,e19),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1715,f1006]) ).

fof(f1717,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i19,e19),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1716,f966]) ).

fof(f1718,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i19,e19),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1717,f928]) ).

fof(f1719,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i19,e19),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1718,f892]) ).

fof(f1720,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i19,e19),i15,e15),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1719,f826]) ).

fof(f1721,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i19,e19),i16,e16),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1720,f796]) ).

fof(f1722,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i19,e19),i17,e17),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1721,f768]) ).

fof(f1723,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i19,e19),i18,e18),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1722,f742]) ).

fof(f1724,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1049,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1723,f718]) ).

fof(f1725,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1048,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1724,f37]) ).

fof(f1726,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i13,e13),i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1725,f36]) ).

fof(f1727,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i13,e13),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1726,f1410]) ).

fof(f1728,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i13,e13),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1727,f1354]) ).

fof(f1729,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i13,e13),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1728,f1300]) ).

fof(f1730,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i13,e13),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1729,f1248]) ).

fof(f1731,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i13,e13),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1730,f1198]) ).

fof(f1732,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i13,e13),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1731,f1150]) ).

fof(f1733,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i13,e13),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1732,f1104]) ).

fof(f1734,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i13,e13),i9,e9),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1733,f1060]) ).

fof(f1735,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i13,e13),i10,e10),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1734,f1018]) ).

fof(f1736,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i13,e13),i11,e11),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1735,f978]) ).

fof(f1737,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i13,e13),i12,e12),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1736,f940]) ).

fof(f1738,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1737,f904]) ).

fof(f1739,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1018,i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1738,f6]) ).

fof(f1740,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1019,i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1739,f7]) ).

fof(f1741,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1020,i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1740,f8]) ).

fof(f1742,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1021,i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1741,f9]) ).

fof(f1743,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1022,i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1742,f10]) ).

fof(f1744,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1023,i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1743,f11]) ).

fof(f1745,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1024,i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1744,f12]) ).

fof(f1746,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1025,i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1745,f13]) ).

fof(f1747,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1026,i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1746,f14]) ).

fof(f1748,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1027,i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1747,f15]) ).

fof(f1749,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1028,i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1748,f16]) ).

fof(f1750,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1029,i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1749,f17]) ).

fof(f1751,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1030,i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1750,f18]) ).

fof(f1752,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1031,i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1751,f19]) ).

fof(f1753,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1032,i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1752,f20]) ).

fof(f1754,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1033,i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1753,f21]) ).

fof(f1755,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(store(a_1034,i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1754,f22]) ).

fof(f1756,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(store(a_1035,i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1755,f23]) ).

fof(f1757,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(store(a_1036,i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1756,f24]) ).

fof(f1758,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(store(a_1037,i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1757,f25]) ).

fof(f1759,plain,
    a_1047 != store(store(store(store(store(store(store(store(store(a_1038,i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1758,f26]) ).

fof(f1760,plain,
    a_1047 != store(store(store(store(store(store(store(store(a_1039,i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1759,f27]) ).

fof(f1761,plain,
    a_1047 != store(store(store(store(store(store(store(a_1040,i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1760,f28]) ).

fof(f1762,plain,
    a_1047 != store(store(store(store(store(store(a_1041,i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1761,f29]) ).

fof(f1763,plain,
    a_1047 != store(store(store(store(store(a_1042,i26,e26),i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1762,f30]) ).

fof(f1764,plain,
    a_1047 != store(store(store(store(a_1043,i27,e27),i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1763,f31]) ).

fof(f1765,plain,
    a_1047 != store(store(store(a_1044,i28,e28),i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1764,f32]) ).

fof(f1766,plain,
    a_1047 != store(store(a_1045,i29,e29),i30,e30),
    inference(forward_demodulation,[],[f1765,f33]) ).

fof(f1767,plain,
    a_1047 != store(a_1046,i30,e30),
    inference(forward_demodulation,[],[f1766,f34]) ).

fof(f1768,plain,
    a_1047 != a_1047,
    inference(forward_demodulation,[],[f1767,f35]) ).

fof(f1769,plain,
    $false,
    inference(trivial_inequality_removal,[],[f1768]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWV512-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.18  % Computer : n013.cluster.edu
% 0.10/0.18  % Model    : x86_64 x86_64
% 0.10/0.18  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18  % Memory   : 8046.5625MB
% 0.10/0.18  % OS       : Linux 6.8.0-71-generic
% 0.10/0.18  % CPULimit : 300
% 0.10/0.18  % WCLimit  : 300
% 0.10/0.18  % DateTime : Mon Sep 28 11:23:06 UTC 2026
% 0.10/0.19  % CPUTime  : 
% 0.10/0.19  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21  Running first-order theorem proving
% 0.10/0.21  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.30/1.82  % (1112224)Input is clausal, will run a generic CNF schedule.
% 7.30/1.82  % (1112233)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4213094374:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.30/1.82  % (1112233)Instruction limit reached! 
% 7.30/1.82  % (1112233)------------------------------
% 7.30/1.82  % (1112233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.30/1.82  % (1112233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.82  % (1112233)CaDiCaL version: 2.1.3
% 7.30/1.82  % (1112233)Termination reason: Instruction limit
% 7.30/1.82  % (1112233)Termination phase: Saturation
% 7.30/1.82  % (1112233)Time elapsed: 0.034 s
% 7.30/1.82  % (1112233)Peak memory usage: 88 MB
% 7.30/1.82  % (1112233)Instructions burned: 117 (million)
% 7.30/1.82  % (1112231)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=909157009:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.30/1.82  % (1112230)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1513185750:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.30/1.82  % (1112232)lrs+10_1_sil=8000:sp=occurrence:random_seed=3047228451:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.30/1.82  % (1112229)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2529360888:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.30/1.82  % (1112234)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=179183766:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.30/1.82  % (1112235)dis-21_1_sil=8000:lcm=predicate:random_seed=3369055633:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.30/1.82  % (1112235)Refutation not found, incomplete strategy
% 7.30/1.82  % (1112235)------------------------------
% 7.30/1.82  % (1112235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.30/1.82  % (1112235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.82  % (1112235)CaDiCaL version: 2.1.3
% 7.30/1.82  % (1112235)Termination reason: Refutation not found, incomplete strategy
% 7.30/1.82  % (1112235)Time elapsed: 0.012 s
% 7.30/1.82  % (1112235)Peak memory usage: 88 MB
% 7.30/1.82  % (1112235)Instructions burned: 24 (million)
% 7.30/1.82  % (1112232)Instruction limit reached! 
% 7.30/1.82  % (1112232)------------------------------
% 7.30/1.82  % (1112232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.30/1.82  % (1112232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.82  % (1112232)CaDiCaL version: 2.1.3
% 7.30/1.82  % (1112232)Termination reason: Instruction limit
% 7.30/1.82  % (1112232)Termination phase: Saturation
% 7.30/1.82  % (1112232)Time elapsed: 0.060 s
% 7.30/1.82  % (1112232)Peak memory usage: 88 MB
% 7.30/1.82  % (1112232)Instructions burned: 107 (million)
% 7.30/1.82  % (1112241)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=4287565719:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.30/1.82  % (1112234)Instruction limit reached! 
% 7.30/1.82  % (1112234)------------------------------
% 7.30/1.82  % (1112234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.30/1.82  % (1112234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.82  % (1112234)CaDiCaL version: 2.1.3
% 7.30/1.82  % (1112234)Termination reason: Instruction limit
% 7.30/1.82  % (1112234)Termination phase: Saturation
% 7.30/1.82  % (1112234)Time elapsed: 0.102 s
% 7.30/1.82  % (1112234)Peak memory usage: 89 MB
% 7.30/1.82  % (1112234)Instructions burned: 182 (million)
% 7.30/1.82  % (1112241)Instruction limit reached! 
% 7.30/1.82  % (1112241)------------------------------
% 7.30/1.82  % (1112241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.30/1.82  % (1112241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.82  % (1112241)CaDiCaL version: 2.1.3
% 7.30/1.82  % (1112241)Termination reason: Instruction limit
% 7.30/1.82  % (1112241)Termination phase: Saturation
% 7.30/1.82  % (1112241)Time elapsed: 0.045 s
% 7.30/1.82  % (1112241)Peak memory usage: 89 MB
% 7.30/1.82  % (1112241)Instructions burned: 145 (million)
% 7.30/1.82  % (1112244)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2236456126:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 16.02/3.01  % (1112246)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2463165274:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.02/3.01  % (1112247)lrs+10_64_to=lpo:sil=8000:random_seed=1828490047:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 16.02/3.01  % (1112235)------------------------------
% 16.02/3.01  % (1112235)------------------------------
% 16.02/3.01  % (1112247)Instruction limit reached! 
% 16.02/3.01  % (1112247)------------------------------
% 16.02/3.01  % (1112247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.01  % (1112247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.01  % (1112247)CaDiCaL version: 2.1.3
% 16.02/3.01  % (1112247)Termination reason: Instruction limit
% 16.02/3.01  % (1112247)Termination phase: Saturation
% 16.02/3.01  % (1112247)Time elapsed: 0.029 s
% 16.02/3.01  % (1112247)Peak memory usage: 88 MB
% 16.02/3.01  % (1112247)Instructions burned: 126 (million)
% 16.02/3.01  % (1112244)Instruction limit reached! 
% 16.02/3.01  % (1112244)------------------------------
% 16.02/3.01  % (1112244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.01  % (1112244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.01  % (1112244)CaDiCaL version: 2.1.3
% 16.02/3.01  % (1112244)Termination reason: Instruction limit
% 16.02/3.01  % (1112244)Termination phase: Saturation
% 16.02/3.01  % (1112244)Time elapsed: 0.093 s
% 16.02/3.01  % (1112244)Peak memory usage: 89 MB
% 16.02/3.01  % (1112244)Instructions burned: 191 (million)
% 16.02/3.01  % (1112246)Instruction limit reached! 
% 16.02/3.01  % (1112246)------------------------------
% 16.02/3.01  % (1112246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.01  % (1112246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.01  % (1112246)CaDiCaL version: 2.1.3
% 16.02/3.01  % (1112246)Termination reason: Instruction limit
% 16.02/3.01  % (1112246)Termination phase: Saturation
% 16.02/3.01  % (1112246)Time elapsed: 0.108 s
% 16.02/3.01  % (1112246)Peak memory usage: 89 MB
% 16.02/3.01  % (1112246)Instructions burned: 220 (million)
% 16.02/3.01  % (1112251)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1048944344:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.02/3.01  % (1112252)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=18057947:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 16.02/3.01  % (1112251)Instruction limit reached! 
% 16.02/3.01  % (1112251)------------------------------
% 16.02/3.01  % (1112251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.01  % (1112251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.01  % (1112251)CaDiCaL version: 2.1.3
% 16.02/3.01  % (1112251)Termination reason: Instruction limit
% 16.02/3.01  % (1112251)Termination phase: Saturation
% 16.02/3.01  % (1112251)Time elapsed: 0.062 s
% 16.02/3.01  % (1112251)Peak memory usage: 90 MB
% 16.02/3.01  % (1112251)Instructions burned: 196 (million)
% 16.02/3.01  % (1112253)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4233001778:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 16.02/3.01  % (1112254)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1711474340:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 16.02/3.01  % (1112252)Instruction limit reached! 
% 16.02/3.01  % (1112252)------------------------------
% 16.02/3.01  % (1112252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.01  % (1112252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.01  % (1112252)CaDiCaL version: 2.1.3
% 16.02/3.01  % (1112252)Termination reason: Instruction limit
% 16.02/3.01  % (1112252)Termination phase: Saturation
% 16.02/3.01  % (1112252)Time elapsed: 0.094 s
% 16.02/3.01  % (1112252)Peak memory usage: 91 MB
% 16.02/3.01  % (1112252)Instructions burned: 157 (million)
% 16.02/3.01  % (1112257)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=797988782:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 16.02/3.01  % (1112254)Instruction limit reached! 
% 16.02/3.01  % (1112254)------------------------------
% 15.02/4.90  % (1112254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112254)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112254)Termination reason: Instruction limit
% 15.02/4.90  % (1112254)Termination phase: Saturation
% 15.02/4.90  % (1112254)Time elapsed: 0.052 s
% 15.02/4.90  % (1112254)Peak memory usage: 90 MB
% 15.02/4.90  % (1112254)Instructions burned: 108 (million)
% 15.02/4.90  % (1112257)Instruction limit reached! 
% 15.02/4.90  % (1112257)------------------------------
% 15.02/4.90  % (1112257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112257)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112257)Termination reason: Instruction limit
% 15.02/4.90  % (1112257)Termination phase: Saturation
% 15.02/4.90  % (1112257)Time elapsed: 0.035 s
% 15.02/4.90  % (1112257)Peak memory usage: 88 MB
% 15.02/4.90  % (1112257)Instructions burned: 111 (million)
% 15.02/4.90  % (1112260)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3392239840:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 15.02/4.90  % (1112263)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=932773516:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 15.02/4.90  % (1112262)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4070374760:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 15.02/4.90  % (1112263)Instruction limit reached! 
% 15.02/4.90  % (1112263)------------------------------
% 15.02/4.90  % (1112263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112263)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112263)Termination reason: Instruction limit
% 15.02/4.90  % (1112263)Termination phase: Saturation
% 15.02/4.90  % (1112263)Time elapsed: 0.041 s
% 15.02/4.90  % (1112263)Peak memory usage: 89 MB
% 15.02/4.90  % (1112263)Instructions burned: 135 (million)
% 15.02/4.90  % (1112260)Instruction limit reached! 
% 15.02/4.90  % (1112260)------------------------------
% 15.02/4.90  % (1112260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112260)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112260)Termination reason: Instruction limit
% 15.02/4.90  % (1112260)Termination phase: Saturation
% 15.02/4.90  % (1112260)Time elapsed: 0.130 s
% 15.02/4.90  % (1112260)Peak memory usage: 91 MB
% 15.02/4.90  % (1112260)Instructions burned: 243 (million)
% 15.02/4.90  % (1112267)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4072156803:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 15.02/4.90  % (1112267)Instruction limit reached! 
% 15.02/4.90  % (1112267)------------------------------
% 15.02/4.90  % (1112267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112267)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112267)Termination reason: Instruction limit
% 15.02/4.90  % (1112267)Termination phase: Saturation
% 15.02/4.90  % (1112267)Time elapsed: 0.117 s
% 15.02/4.90  % (1112267)Peak memory usage: 92 MB
% 15.02/4.90  % (1112267)Instructions burned: 500 (million)
% 15.02/4.90  % (1112268)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1568501581:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 15.02/4.90  % (1112268)Instruction limit reached! 
% 15.02/4.90  % (1112268)------------------------------
% 15.02/4.90  % (1112268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112268)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112268)Termination reason: Instruction limit
% 15.02/4.90  % (1112268)Termination phase: Saturation
% 15.02/4.90  % (1112268)Time elapsed: 0.093 s
% 15.02/4.90  % (1112268)Peak memory usage: 90 MB
% 15.02/4.90  % (1112268)Instructions burned: 191 (million)
% 15.02/4.90  % (1112271)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1715838847:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 15.02/4.90  % (1112272)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1138332267:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 15.02/4.90  % (1112271)Instruction limit reached! 
% 15.02/4.90  % (1112271)------------------------------
% 15.02/4.90  % (1112271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112271)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112271)Termination reason: Instruction limit
% 15.02/4.90  % (1112271)Termination phase: Saturation
% 15.02/4.90  % (1112271)Time elapsed: 0.131 s
% 15.02/4.90  % (1112271)Peak memory usage: 92 MB
% 15.02/4.90  % (1112271)Instructions burned: 264 (million)
% 15.02/4.90  % (1112272)Instruction limit reached! 
% 15.02/4.90  % (1112272)------------------------------
% 15.02/4.90  % (1112272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112272)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112272)Termination reason: Instruction limit
% 15.02/4.90  % (1112272)Termination phase: Saturation
% 15.02/4.90  % (1112272)Time elapsed: 0.083 s
% 15.02/4.90  % (1112272)Peak memory usage: 89 MB
% 15.02/4.90  % (1112272)Instructions burned: 156 (million)
% 15.02/4.90  % (1112275)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3709817992:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 15.02/4.90  % (1112276)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3380702453:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 15.02/4.90  % (1112276)Instruction limit reached! 
% 15.02/4.90  % (1112276)------------------------------
% 15.02/4.90  % (1112276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112276)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112276)Termination reason: Instruction limit
% 15.02/4.90  % (1112276)Termination phase: Saturation
% 15.02/4.90  % (1112276)Time elapsed: 0.280 s
% 15.02/4.90  % (1112276)Peak memory usage: 94 MB
% 15.02/4.90  % (1112276)Instructions burned: 538 (million)
% 15.02/4.90  % (1112279)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1214789949:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 15.02/4.90  % (1112279)Instruction limit reached! 
% 15.02/4.90  % (1112279)------------------------------
% 15.02/4.90  % (1112279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112279)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112279)Termination reason: Instruction limit
% 15.02/4.90  % (1112279)Termination phase: Saturation
% 15.02/4.90  % (1112279)Time elapsed: 0.079 s
% 15.02/4.90  % (1112279)Peak memory usage: 89 MB
% 15.02/4.90  % (1112279)Instructions burned: 182 (million)
% 15.02/4.90  % (1112281)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=232177597:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 15.02/4.90  % (1112253)Instruction limit reached! 
% 15.02/4.90  % (1112253)------------------------------
% 15.02/4.90  % (1112253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112253)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112253)Termination reason: Instruction limit
% 15.02/4.90  % (1112253)Termination phase: Saturation
% 15.02/4.90  % (1112253)Time elapsed: 1.589 s
% 15.02/4.90  % (1112253)Peak memory usage: 148 MB
% 15.02/4.90  % (1112253)Instructions burned: 3395 (million)
% 15.02/4.90  % (1112283)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=490146843:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 15.02/4.90  % (1112283)Instruction limit reached! 
% 15.02/4.90  % (1112283)------------------------------
% 15.02/4.90  % (1112283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112283)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112283)Termination reason: Instruction limit
% 15.02/4.90  % (1112283)Termination phase: Saturation
% 15.02/4.90  % (1112283)Time elapsed: 0.094 s
% 15.02/4.90  % (1112283)Peak memory usage: 92 MB
% 15.02/4.90  % (1112283)Instructions burned: 414 (million)
% 15.02/4.90  % (1112285)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1711084620:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi)
% 15.02/4.90  % (1112262)Instruction limit reached! 
% 15.02/4.90  % (1112262)------------------------------
% 15.02/4.90  % (1112262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112262)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112262)Termination reason: Instruction limit
% 15.02/4.90  % (1112262)Termination phase: Saturation
% 15.02/4.90  % (1112262)Time elapsed: 2.472 s
% 15.02/4.90  % (1112262)Peak memory usage: 145 MB
% 15.02/4.90  % (1112262)Instructions burned: 5209 (million)
% 15.02/4.90  % (1112287)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2908088980:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2966 on theBenchmark for (2966ds/303Mi)
% 15.02/4.90  % (1112287)Refutation not found, incomplete strategy
% 15.02/4.90  % (1112287)------------------------------
% 15.02/4.90  % (1112287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112287)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112287)Termination reason: Refutation not found, incomplete strategy
% 15.02/4.90  % (1112287)Time elapsed: 0.122 s
% 15.02/4.90  % (1112287)Peak memory usage: 92 MB
% 15.02/4.90  % (1112287)Instructions burned: 293 (million)
% 15.02/4.90  % (1112287)------------------------------
% 15.02/4.90  % (1112287)------------------------------
% 15.02/4.90  % (1112275)Instruction limit reached! 
% 15.02/4.90  % (1112275)------------------------------
% 15.02/4.90  % (1112275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.90  % (1112275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.90  % (1112275)CaDiCaL version: 2.1.3
% 15.02/4.90  % (1112275)Termination reason: Instruction limit
% 15.02/4.90  % (1112275)Termination phase: Saturation
% 15.02/4.90  % (1112275)Time elapsed: 2.385 s
% 15.02/4.90  % (1112275)Peak memory usage: 148 MB
% 15.02/4.90  % (1112275)Instructions burned: 3256 (million)
% 15.02/4.90  % (1112289)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2442839527:st=4:i=720:sd=3:fsr=off:ss=axioms_2962 on theBenchmark for (2962ds/720Mi)
% 15.02/4.90  % (1112290)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3105261384:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi)
% 15.02/4.90  % (1112289)First to succeed.
% 15.02/4.90  % (1112289)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1112224"
% 15.02/4.90  % (1112289)Refutation found. Thanks to Tanya!
% 15.02/4.90  % SZS status Unsatisfiable for theBenchmark
% 15.02/4.90  % SZS output start Proof for theBenchmark
% See solution above
% 30.67/5.10  % (1112289)------------------------------
% 30.67/5.10  % (1112289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.67/5.10  % (1112289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.67/5.10  % (1112289)CaDiCaL version: 2.1.3
% 30.67/5.10  % (1112289)Termination reason: Refutation
% 30.67/5.10  % (1112289)Time elapsed: 0.088 s
% 30.67/5.10  % (1112289)Peak memory usage: 90 MB
% 30.67/5.10  % (1112289)Instructions burned: 179 (million)
% 30.67/5.10  % (1112289)------------------------------
% 30.67/5.10  % (1112289)------------------------------
% 30.67/5.10  % (1112224)Success in time 4.255 s
% 30.67/5.10  % Vampire exiting
%------------------------------------------------------------------------------