%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:49:07 PM UTC 2026
% Result : Unsatisfiable 54.84s 7.36s
% Output : CNFRefutation 43.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 329
% Syntax : Number of formulae : 1862 (1472 unt; 0 def)
% Number of atoms : 2347 (2346 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 910 ( 425 ~; 485 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 27 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 346 ( 346 usr; 343 con; 0-3 aty)
% Number of variables : 246 ( 246 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(X)))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X] : s(s(s(s(s(s(s(s(s(X))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X] : s(s(s(s(s(s(s(s(X)))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [X] : s(s(s(s(s(s(s(X))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] : s(s(s(s(s(s(X)))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] : s(s(s(s(s(X))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X] : s(s(s(s(X)))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [X] : s(s(s(X))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [X] : s(s(X)) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X] : s(X) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,hypothesis,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,hypothesis,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
earray_170 = select(q30,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,hypothesis,
earray_172 = store(earray_170,index_171,e30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,hypothesis,
earray_176 = select(q31,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,hypothesis,
earray_178 = store(earray_176,index_177,e31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
earray_182 = select(q32,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
earray_184 = store(earray_182,index_183,e32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
earray_191 = select(q33,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,hypothesis,
earray_193 = store(earray_191,index_192,e33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,hypothesis,
earray_197 = select(q34,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
earray_199 = store(earray_197,index_198,e34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
earray_203 = select(q35,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
earray_205 = store(earray_203,index_204,e35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
earray_212 = select(q36,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
earray_214 = store(earray_212,index_213,e36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
earray_218 = select(q37,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
earray_220 = store(earray_218,index_219,e37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
earray_224 = select(q38,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
earray_226 = store(earray_224,index_225,e38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
earray_239 = select(q39,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
earray_241 = store(earray_239,index_240,e39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
earray_281 = select(q40,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,hypothesis,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
elem_283 = select(earray_281,index_282),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_105 = select(q22,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_111 = select(q23,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_117 = s(index_116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_120 = select(q24,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_123 = s(index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_126 = select(q25,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_129 = s(index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_132 = select(q26,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_135 = s(index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_138 = s(index_137),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_141 = select(q27,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_147 = select(q28,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_153 = select(q2,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_159 = s(index_158),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_162 = select(q29,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_165 = s(index_162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_168 = s(index_167),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_171 = select(q30,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_177 = select(q31,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_183 = select(q32,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_189 = s(index_188),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_192 = select(q33,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_195 = s(index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_198 = select(q34,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_201 = s(index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_204 = select(q35,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_207 = s(index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_21 = select(q11,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_210 = s(index_209),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
index_213 = select(q36,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
index_219 = select(q37,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
index_225 = select(q38,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
index_230 = select(queue_229,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
index_231 = s(index_230),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
index_234 = select(q3,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
index_237 = s(index_234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
index_240 = select(q39,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
index_246 = select(q4,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
index_249 = s(index_246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
index_252 = select(q5,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
index_255 = s(index_252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
index_257 = select(queue_256,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
index_258 = s(index_257),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
index_261 = select(q6,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
index_267 = select(q7,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
index_27 = s(index_26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
index_270 = s(index_267),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
index_273 = select(q8,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
index_278 = select(queue_277,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
index_279 = s(index_278),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
index_282 = select(q40,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
index_30 = select(q12,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
index_33 = s(index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
index_36 = select(q13,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
index_39 = s(index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
index_42 = select(q14,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
index_45 = s(index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
index_48 = s(index_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
index_51 = select(q15,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
index_57 = select(q16,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
index_63 = select(q17,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
index_69 = s(index_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
index_72 = select(q18,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
index_75 = s(index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
index_78 = select(q1,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
index_81 = s(index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
index_84 = select(q19,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
index_87 = s(index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
index_90 = select(q20,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
index_93 = s(index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
index_96 = s(index_95),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
index_99 = select(q21,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
queue_173 = store(q30,seq,earray_172),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
queue_179 = store(q31,seq,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
queue_185 = store(q32,seq,earray_184),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
queue_194 = store(q33,seq,earray_193),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
queue_200 = store(q34,seq,earray_199),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
queue_206 = store(q35,seq,earray_205),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
queue_215 = store(q36,seq,earray_214),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
queue_221 = store(q37,seq,earray_220),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
queue_227 = store(q38,seq,earray_226),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
queue_232 = store(queue_229,head,index_231),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
queue_236 = store(q3,seq,earray_235),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
queue_238 = store(queue_236,tail,index_237),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
queue_242 = store(q39,seq,earray_241),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
queue_244 = store(queue_242,tail,index_243),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
queue_248 = store(q4,seq,earray_247),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
queue_250 = store(queue_248,tail,index_249),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
queue_254 = store(q5,seq,earray_253),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
queue_256 = store(queue_254,tail,index_255),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
queue_259 = store(queue_256,head,index_258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
queue_263 = store(q6,seq,earray_262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
queue_269 = store(q7,seq,earray_268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f327,hypothesis,
queue_275 = store(q8,seq,earray_274),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f328,hypothesis,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f329,hypothesis,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f330,hypothesis,
queue_280 = store(queue_277,head,index_279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,hypothesis,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f332,hypothesis,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f333,hypothesis,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f334,hypothesis,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f335,hypothesis,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f336,hypothesis,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f337,hypothesis,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f338,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f339,hypothesis,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f340,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f341,hypothesis,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f342,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,hypothesis,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f344,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f345,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f346,hypothesis,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f347,hypothesis,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f348,hypothesis,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f349,hypothesis,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f350,hypothesis,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f351,hypothesis,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f352,hypothesis,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f353,hypothesis,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,hypothesis,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f355,hypothesis,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f357,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f358,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f359,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,hypothesis,
q12 = queue_28,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f361,hypothesis,
q13 = queue_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f362,hypothesis,
q14 = queue_40,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f363,hypothesis,
q15 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f364,hypothesis,
q16 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f365,hypothesis,
q17 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,hypothesis,
q18 = queue_70,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f367,hypothesis,
q19 = queue_76,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f368,hypothesis,
q2 = queue_82,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f369,hypothesis,
q20 = queue_88,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f370,hypothesis,
q21 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f371,hypothesis,
q22 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f372,hypothesis,
q23 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f373,hypothesis,
q24 = queue_118,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f374,hypothesis,
q25 = queue_124,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f375,hypothesis,
q26 = queue_130,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f376,hypothesis,
q27 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f377,hypothesis,
q28 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f378,hypothesis,
q29 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f379,hypothesis,
q3 = queue_160,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,hypothesis,
q30 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f381,hypothesis,
q31 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,hypothesis,
q32 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f383,hypothesis,
q33 = queue_190,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,hypothesis,
q34 = queue_196,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f385,hypothesis,
q35 = queue_202,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f386,hypothesis,
q36 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f387,hypothesis,
q37 = queue_217,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f388,hypothesis,
q38 = queue_223,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f389,hypothesis,
q39 = queue_232,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f390,hypothesis,
q4 = queue_238,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f391,hypothesis,
q40 = queue_244,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f392,hypothesis,
q5 = queue_250,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f393,hypothesis,
q6 = queue_259,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f394,hypothesis,
q7 = queue_265,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f395,hypothesis,
q8 = queue_271,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f396,hypothesis,
q9 = queue_280,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f397,negated_conjecture,
elem_283 != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f398,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f399,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f400,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f401,plain,
head != tail,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f402,plain,
head != seq,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f403,plain,
tail != seq,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f444,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f445,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f446,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f447,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f448,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f449,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f450,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f451,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f452,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f453,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f454,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f455,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f456,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f457,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f458,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f459,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f460,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f461,plain,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f462,plain,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f463,plain,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f464,plain,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f465,plain,
! [X0] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f466,plain,
! [X0] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f467,plain,
! [X0] : s(s(s(X0))) != X0,
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f468,plain,
! [X0] : s(s(X0)) != X0,
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f469,plain,
! [X0] : s(X0) != X0,
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f471,plain,
earray_100 = store(earray_98,index_99,e21),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f472,plain,
earray_104 = select(q22,seq),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f473,plain,
earray_106 = store(earray_104,index_105,e22),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f474,plain,
earray_110 = select(q23,seq),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f475,plain,
earray_112 = store(earray_110,index_111,e23),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f476,plain,
earray_119 = select(q24,seq),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f477,plain,
earray_121 = store(earray_119,index_120,e24),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f478,plain,
earray_125 = select(q25,seq),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f479,plain,
earray_127 = store(earray_125,index_126,e25),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f480,plain,
earray_131 = select(q26,seq),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f481,plain,
earray_133 = store(earray_131,index_132,e26),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f483,plain,
earray_140 = select(q27,seq),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f484,plain,
earray_142 = store(earray_140,index_141,e27),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f485,plain,
earray_146 = select(q28,seq),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f486,plain,
earray_148 = store(earray_146,index_147,e28),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f490,plain,
earray_161 = select(q29,seq),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f491,plain,
earray_163 = store(earray_161,index_162,e29),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f492,plain,
earray_170 = select(q30,seq),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f493,plain,
earray_172 = store(earray_170,index_171,e30),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f494,plain,
earray_176 = select(q31,seq),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f495,plain,
earray_178 = store(earray_176,index_177,e31),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f496,plain,
earray_182 = select(q32,seq),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f497,plain,
earray_184 = store(earray_182,index_183,e32),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f498,plain,
earray_191 = select(q33,seq),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f499,plain,
earray_193 = store(earray_191,index_192,e33),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f500,plain,
earray_197 = select(q34,seq),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f501,plain,
earray_199 = store(earray_197,index_198,e34),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f504,plain,
earray_203 = select(q35,seq),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f505,plain,
earray_205 = store(earray_203,index_204,e35),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f506,plain,
earray_212 = select(q36,seq),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f507,plain,
earray_214 = store(earray_212,index_213,e36),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f508,plain,
earray_218 = select(q37,seq),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f510,plain,
earray_220 = store(earray_218,index_219,e37),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f511,plain,
earray_224 = select(q38,seq),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f512,plain,
earray_226 = store(earray_224,index_225,e38),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f515,plain,
earray_239 = select(q39,seq),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f516,plain,
earray_241 = store(earray_239,index_240,e39),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f527,plain,
earray_281 = select(q40,seq),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f531,plain,
earray_37 = store(earray_35,index_36,e13),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f533,plain,
earray_41 = select(q14,seq),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f534,plain,
earray_43 = store(earray_41,index_42,e14),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f535,plain,
earray_50 = select(q15,seq),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f536,plain,
earray_52 = store(earray_50,index_51,e15),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f537,plain,
earray_56 = select(q16,seq),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f538,plain,
earray_58 = store(earray_56,index_57,e16),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f539,plain,
earray_62 = select(q17,seq),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f540,plain,
earray_64 = store(earray_62,index_63,e17),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f541,plain,
earray_71 = select(q18,seq),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f542,plain,
earray_73 = store(earray_71,index_72,e18),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f546,plain,
earray_83 = select(q19,seq),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f547,plain,
earray_85 = store(earray_83,index_84,e19),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f548,plain,
earray_89 = select(q20,seq),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f549,plain,
earray_91 = store(earray_89,index_90,e20),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f550,plain,
earray_98 = select(q21,seq),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f551,plain,
elem_283 = select(earray_281,index_282),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f552,plain,
index_0 = select(q,tail),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f553,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f554,plain,
index_105 = select(q22,tail),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f555,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f556,plain,
index_111 = select(q23,tail),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f557,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f558,plain,
index_116 = select(queue_115,head),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f559,plain,
index_117 = s(index_116),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f560,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f561,plain,
index_120 = select(q24,tail),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f562,plain,
index_123 = s(index_120),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f563,plain,
index_126 = select(q25,tail),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f564,plain,
index_129 = s(index_126),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f565,plain,
index_132 = select(q26,tail),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f566,plain,
index_135 = s(index_132),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f567,plain,
index_137 = select(queue_136,head),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f568,plain,
index_138 = s(index_137),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f569,plain,
index_141 = select(q27,tail),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f570,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f571,plain,
index_147 = select(q28,tail),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f572,plain,
index_15 = select(q10,tail),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f573,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f574,plain,
index_153 = select(q2,tail),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f575,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f576,plain,
index_158 = select(queue_157,head),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f577,plain,
index_159 = s(index_158),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f578,plain,
index_162 = select(q29,tail),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f579,plain,
index_165 = s(index_162),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f580,plain,
index_167 = select(queue_166,head),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f581,plain,
index_168 = s(index_167),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f582,plain,
index_171 = select(q30,tail),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f583,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f584,plain,
index_177 = select(q31,tail),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f585,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f586,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f587,plain,
index_183 = select(q32,tail),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f588,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f589,plain,
index_188 = select(queue_187,head),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f590,plain,
index_189 = s(index_188),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f591,plain,
index_192 = select(q33,tail),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f592,plain,
index_195 = s(index_192),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f593,plain,
index_198 = select(q34,tail),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f594,plain,
index_201 = s(index_198),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f595,plain,
index_204 = select(q35,tail),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f596,plain,
index_207 = s(index_204),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f597,plain,
index_209 = select(queue_208,head),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f598,plain,
index_21 = select(q11,tail),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f599,plain,
index_210 = s(index_209),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f600,plain,
index_213 = select(q36,tail),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f601,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f602,plain,
index_219 = select(q37,tail),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f603,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f604,plain,
index_225 = select(q38,tail),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f605,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f606,plain,
index_230 = select(queue_229,head),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f607,plain,
index_231 = s(index_230),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f608,plain,
index_234 = select(q3,tail),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f609,plain,
index_237 = s(index_234),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f610,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f611,plain,
index_240 = select(q39,tail),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f613,plain,
index_246 = select(q4,tail),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f614,plain,
index_249 = s(index_246),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f615,plain,
index_252 = select(q5,tail),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f616,plain,
index_255 = s(index_252),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f617,plain,
index_257 = select(queue_256,head),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f618,plain,
index_258 = s(index_257),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f619,plain,
index_26 = select(queue_25,head),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f620,plain,
index_261 = select(q6,tail),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f621,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f622,plain,
index_267 = select(q7,tail),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f623,plain,
index_27 = s(index_26),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f624,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f625,plain,
index_273 = select(q8,tail),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f626,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f627,plain,
index_278 = select(queue_277,head),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f628,plain,
index_279 = s(index_278),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f629,plain,
index_282 = select(q40,head),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f630,plain,
index_3 = select(q0,tail),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f631,plain,
index_30 = select(q12,tail),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f632,plain,
index_33 = s(index_30),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f633,plain,
index_36 = select(q13,tail),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f634,plain,
index_39 = s(index_36),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f635,plain,
index_42 = select(q14,tail),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f636,plain,
index_45 = s(index_42),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f637,plain,
index_47 = select(queue_46,head),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f638,plain,
index_48 = s(index_47),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f639,plain,
index_51 = select(q15,tail),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f640,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f641,plain,
index_57 = select(q16,tail),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f642,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f643,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f644,plain,
index_63 = select(q17,tail),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f645,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f646,plain,
index_68 = select(queue_67,head),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f647,plain,
index_69 = s(index_68),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f648,plain,
index_72 = select(q18,tail),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f649,plain,
index_75 = s(index_72),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f650,plain,
index_78 = select(q1,tail),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f651,plain,
index_81 = s(index_78),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f652,plain,
index_84 = select(q19,tail),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f653,plain,
index_87 = s(index_84),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f654,plain,
index_9 = select(q9,tail),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f655,plain,
index_90 = select(q20,tail),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f656,plain,
index_93 = s(index_90),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f657,plain,
index_95 = select(queue_94,head),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f658,plain,
index_96 = s(index_95),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f659,plain,
index_99 = select(q21,tail),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f660,plain,
queue_1 = store(q,head,index_0),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f661,plain,
queue_101 = store(q21,seq,earray_100),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f662,plain,
queue_103 = store(queue_101,tail,index_102),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f663,plain,
queue_107 = store(q22,seq,earray_106),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f664,plain,
queue_109 = store(queue_107,tail,index_108),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f665,plain,
queue_11 = store(q9,seq,earray_10),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f666,plain,
queue_113 = store(q23,seq,earray_112),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f667,plain,
queue_115 = store(queue_113,tail,index_114),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f668,plain,
queue_118 = store(queue_115,head,index_117),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f669,plain,
queue_122 = store(q24,seq,earray_121),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f670,plain,
queue_124 = store(queue_122,tail,index_123),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f671,plain,
queue_128 = store(q25,seq,earray_127),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f672,plain,
queue_13 = store(queue_11,tail,index_12),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f673,plain,
queue_130 = store(queue_128,tail,index_129),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f674,plain,
queue_134 = store(q26,seq,earray_133),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f675,plain,
queue_136 = store(queue_134,tail,index_135),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f676,plain,
queue_139 = store(queue_136,head,index_138),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f677,plain,
queue_143 = store(q27,seq,earray_142),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f678,plain,
queue_145 = store(queue_143,tail,index_144),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f679,plain,
queue_149 = store(q28,seq,earray_148),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f680,plain,
queue_151 = store(queue_149,tail,index_150),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f681,plain,
queue_155 = store(q2,seq,earray_154),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f682,plain,
queue_157 = store(queue_155,tail,index_156),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f683,plain,
queue_160 = store(queue_157,head,index_159),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f684,plain,
queue_164 = store(q29,seq,earray_163),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f685,plain,
queue_166 = store(queue_164,tail,index_165),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f686,plain,
queue_169 = store(queue_166,head,index_168),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f687,plain,
queue_17 = store(q10,seq,earray_16),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f688,plain,
queue_173 = store(q30,seq,earray_172),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f689,plain,
queue_175 = store(queue_173,tail,index_174),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f690,plain,
queue_179 = store(q31,seq,earray_178),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f691,plain,
queue_181 = store(queue_179,tail,index_180),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f692,plain,
queue_185 = store(q32,seq,earray_184),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f693,plain,
queue_187 = store(queue_185,tail,index_186),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f694,plain,
queue_19 = store(queue_17,tail,index_18),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f695,plain,
queue_190 = store(queue_187,head,index_189),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f696,plain,
queue_194 = store(q33,seq,earray_193),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f697,plain,
queue_196 = store(queue_194,tail,index_195),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f698,plain,
queue_200 = store(q34,seq,earray_199),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f699,plain,
queue_202 = store(queue_200,tail,index_201),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f700,plain,
queue_206 = store(q35,seq,earray_205),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f701,plain,
queue_208 = store(queue_206,tail,index_207),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f702,plain,
queue_211 = store(queue_208,head,index_210),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f703,plain,
queue_215 = store(q36,seq,earray_214),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f704,plain,
queue_217 = store(queue_215,tail,index_216),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f705,plain,
queue_221 = store(q37,seq,earray_220),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f706,plain,
queue_223 = store(queue_221,tail,index_222),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f707,plain,
queue_227 = store(q38,seq,earray_226),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f708,plain,
queue_229 = store(queue_227,tail,index_228),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f709,plain,
queue_23 = store(q11,seq,earray_22),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f710,plain,
queue_232 = store(queue_229,head,index_231),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f711,plain,
queue_236 = store(q3,seq,earray_235),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f712,plain,
queue_238 = store(queue_236,tail,index_237),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f713,plain,
queue_242 = store(q39,seq,earray_241),
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f714,plain,
queue_244 = store(queue_242,tail,index_243),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f715,plain,
queue_248 = store(q4,seq,earray_247),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f716,plain,
queue_25 = store(queue_23,tail,index_24),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f717,plain,
queue_250 = store(queue_248,tail,index_249),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f718,plain,
queue_254 = store(q5,seq,earray_253),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f719,plain,
queue_256 = store(queue_254,tail,index_255),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f720,plain,
queue_259 = store(queue_256,head,index_258),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f721,plain,
queue_263 = store(q6,seq,earray_262),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f722,plain,
queue_265 = store(queue_263,tail,index_264),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f723,plain,
queue_269 = store(q7,seq,earray_268),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f724,plain,
queue_271 = store(queue_269,tail,index_270),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f725,plain,
queue_275 = store(q8,seq,earray_274),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f726,plain,
queue_277 = store(queue_275,tail,index_276),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f727,plain,
queue_28 = store(queue_25,head,index_27),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f728,plain,
queue_280 = store(queue_277,head,index_279),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f729,plain,
queue_32 = store(q12,seq,earray_31),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f730,plain,
queue_34 = store(queue_32,tail,index_33),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f731,plain,
queue_38 = store(q13,seq,earray_37),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f732,plain,
queue_40 = store(queue_38,tail,index_39),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f733,plain,
queue_44 = store(q14,seq,earray_43),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f734,plain,
queue_46 = store(queue_44,tail,index_45),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f735,plain,
queue_49 = store(queue_46,head,index_48),
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f736,plain,
queue_5 = store(q0,seq,earray_4),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f737,plain,
queue_53 = store(q15,seq,earray_52),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f738,plain,
queue_55 = store(queue_53,tail,index_54),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f739,plain,
queue_59 = store(q16,seq,earray_58),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f740,plain,
queue_61 = store(queue_59,tail,index_60),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f741,plain,
queue_65 = store(q17,seq,earray_64),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f742,plain,
queue_67 = store(queue_65,tail,index_66),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f743,plain,
queue_7 = store(queue_5,tail,index_6),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f744,plain,
queue_70 = store(queue_67,head,index_69),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f745,plain,
queue_74 = store(q18,seq,earray_73),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f746,plain,
queue_76 = store(queue_74,tail,index_75),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f747,plain,
queue_80 = store(q1,seq,earray_79),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f748,plain,
queue_82 = store(queue_80,tail,index_81),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f749,plain,
queue_86 = store(q19,seq,earray_85),
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f750,plain,
queue_88 = store(queue_86,tail,index_87),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f751,plain,
queue_92 = store(q20,seq,earray_91),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f752,plain,
queue_94 = store(queue_92,tail,index_93),
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f753,plain,
queue_97 = store(queue_94,head,index_96),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f754,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f755,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f756,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f757,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f758,plain,
q12 = queue_28,
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f759,plain,
q13 = queue_34,
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f760,plain,
q14 = queue_40,
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f761,plain,
q15 = queue_49,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f762,plain,
q16 = queue_55,
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f763,plain,
q17 = queue_61,
inference(cnf_transformation,[status(thm)],[f365]) ).
fof(f764,plain,
q18 = queue_70,
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f765,plain,
q19 = queue_76,
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f766,plain,
q2 = queue_82,
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f767,plain,
q20 = queue_88,
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f768,plain,
q21 = queue_97,
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f769,plain,
q22 = queue_103,
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f770,plain,
q23 = queue_109,
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f771,plain,
q24 = queue_118,
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f772,plain,
q25 = queue_124,
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f773,plain,
q26 = queue_130,
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f774,plain,
q27 = queue_139,
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f775,plain,
q28 = queue_145,
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f776,plain,
q29 = queue_151,
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f777,plain,
q3 = queue_160,
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f778,plain,
q30 = queue_169,
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f779,plain,
q31 = queue_175,
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f780,plain,
q32 = queue_181,
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f781,plain,
q33 = queue_190,
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f782,plain,
q34 = queue_196,
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f783,plain,
q35 = queue_202,
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f784,plain,
q36 = queue_211,
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f785,plain,
q37 = queue_217,
inference(cnf_transformation,[status(thm)],[f387]) ).
fof(f786,plain,
q38 = queue_223,
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f787,plain,
q39 = queue_232,
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f788,plain,
q4 = queue_238,
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f789,plain,
q40 = queue_244,
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f790,plain,
q5 = queue_250,
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f791,plain,
q6 = queue_259,
inference(cnf_transformation,[status(thm)],[f393]) ).
fof(f792,plain,
q7 = queue_265,
inference(cnf_transformation,[status(thm)],[f394]) ).
fof(f793,plain,
q8 = queue_271,
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f794,plain,
q9 = queue_280,
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f795,plain,
elem_283 != e13,
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f796,plain,
select(earray_37,index_36) = e13,
inference(paramodulation,[status(thm)],[f531,f398]) ).
fof(f3281,plain,
s(index_39) != index_36,
inference(paramodulation,[status(thm)],[f634,f468]) ).
fof(f3302,plain,
index_39 != index_36,
inference(paramodulation,[status(thm)],[f634,f469]) ).
fof(f3365,plain,
s(s(s(s(s(s(index_39)))))) != index_36,
inference(paramodulation,[status(thm)],[f634,f463]) ).
fof(f3407,plain,
s(s(s(s(s(index_39))))) != index_36,
inference(paramodulation,[status(thm)],[f634,f464]) ).
fof(f3449,plain,
s(s(s(s(index_39)))) != index_36,
inference(paramodulation,[status(thm)],[f634,f465]) ).
fof(f3556,plain,
s(s(s(index_39))) != index_36,
inference(paramodulation,[status(thm)],[f634,f466]) ).
fof(f3731,plain,
s(s(index_39)) != index_36,
inference(paramodulation,[status(thm)],[f634,f467]) ).
fof(f3972,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_99 = X0 ),
inference(paramodulation,[status(thm)],[f471,f400]) ).
fof(f3974,plain,
earray_104 = select(queue_103,seq),
inference(forward_demodulation,[status(thm)],[f769,f472]) ).
fof(f4043,plain,
earray_110 = select(queue_109,seq),
inference(forward_demodulation,[status(thm)],[f770,f474]) ).
fof(f4178,plain,
earray_119 = select(queue_118,seq),
inference(forward_demodulation,[status(thm)],[f771,f476]) ).
fof(f4311,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_120 = X0 ),
inference(paramodulation,[status(thm)],[f477,f400]) ).
fof(f4313,plain,
earray_125 = select(queue_124,seq),
inference(forward_demodulation,[status(thm)],[f772,f478]) ).
fof(f4316,plain,
earray_131 = select(queue_130,seq),
inference(forward_demodulation,[status(thm)],[f773,f480]) ).
fof(f4320,plain,
earray_140 = select(queue_139,seq),
inference(forward_demodulation,[status(thm)],[f774,f483]) ).
fof(f4321,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_141 = X0 ),
inference(paramodulation,[status(thm)],[f484,f400]) ).
fof(f4323,plain,
earray_146 = select(queue_145,seq),
inference(forward_demodulation,[status(thm)],[f775,f485]) ).
fof(f4331,plain,
earray_161 = select(queue_151,seq),
inference(forward_demodulation,[status(thm)],[f776,f490]) ).
fof(f4334,plain,
earray_170 = select(queue_169,seq),
inference(forward_demodulation,[status(thm)],[f778,f492]) ).
fof(f4335,plain,
! [X0] :
( select(earray_172,X0) = select(earray_170,X0)
| index_171 = X0 ),
inference(paramodulation,[status(thm)],[f493,f400]) ).
fof(f4337,plain,
earray_176 = select(queue_175,seq),
inference(forward_demodulation,[status(thm)],[f779,f494]) ).
fof(f4340,plain,
earray_182 = select(queue_181,seq),
inference(forward_demodulation,[status(thm)],[f780,f496]) ).
fof(f4343,plain,
earray_191 = select(queue_190,seq),
inference(forward_demodulation,[status(thm)],[f781,f498]) ).
fof(f4344,plain,
! [X0] :
( select(earray_193,X0) = select(earray_191,X0)
| index_192 = X0 ),
inference(paramodulation,[status(thm)],[f499,f400]) ).
fof(f4346,plain,
earray_197 = select(queue_196,seq),
inference(forward_demodulation,[status(thm)],[f782,f500]) ).
fof(f4351,plain,
earray_203 = select(queue_202,seq),
inference(forward_demodulation,[status(thm)],[f783,f504]) ).
fof(f4352,plain,
earray_212 = select(queue_211,seq),
inference(forward_demodulation,[status(thm)],[f784,f506]) ).
fof(f4353,plain,
earray_218 = select(queue_217,seq),
inference(forward_demodulation,[status(thm)],[f785,f508]) ).
fof(f4356,plain,
! [X0] :
( select(earray_214,X0) = select(earray_212,X0)
| index_213 = X0 ),
inference(paramodulation,[status(thm)],[f507,f400]) ).
fof(f4358,plain,
earray_224 = select(queue_223,seq),
inference(forward_demodulation,[status(thm)],[f786,f511]) ).
fof(f4360,plain,
earray_239 = select(queue_232,seq),
inference(forward_demodulation,[status(thm)],[f787,f515]) ).
fof(f4374,plain,
earray_281 = select(queue_244,seq),
inference(forward_demodulation,[status(thm)],[f789,f527]) ).
fof(f4377,plain,
earray_41 = select(queue_40,seq),
inference(forward_demodulation,[status(thm)],[f760,f533]) ).
fof(f4378,plain,
! [X0] :
( select(earray_241,X0) = select(earray_239,X0)
| index_240 = X0 ),
inference(paramodulation,[status(thm)],[f516,f400]) ).
fof(f4382,plain,
earray_50 = select(queue_49,seq),
inference(forward_demodulation,[status(thm)],[f761,f535]) ).
fof(f4383,plain,
earray_56 = select(queue_55,seq),
inference(forward_demodulation,[status(thm)],[f762,f537]) ).
fof(f4384,plain,
earray_62 = select(queue_61,seq),
inference(forward_demodulation,[status(thm)],[f763,f539]) ).
fof(f4385,plain,
earray_71 = select(queue_70,seq),
inference(forward_demodulation,[status(thm)],[f764,f541]) ).
fof(f4394,plain,
earray_83 = select(queue_76,seq),
inference(forward_demodulation,[status(thm)],[f765,f546]) ).
fof(f4395,plain,
earray_89 = select(queue_88,seq),
inference(forward_demodulation,[status(thm)],[f767,f548]) ).
fof(f4398,plain,
earray_98 = select(queue_97,seq),
inference(forward_demodulation,[status(thm)],[f768,f550]) ).
fof(f4399,plain,
index_105 = select(queue_103,tail),
inference(forward_demodulation,[status(thm)],[f769,f554]) ).
fof(f4400,plain,
index_111 = select(queue_109,tail),
inference(forward_demodulation,[status(thm)],[f770,f556]) ).
fof(f4405,plain,
index_120 = select(queue_118,tail),
inference(forward_demodulation,[status(thm)],[f771,f561]) ).
fof(f4406,plain,
index_126 = select(queue_124,tail),
inference(forward_demodulation,[status(thm)],[f772,f563]) ).
fof(f4407,plain,
index_132 = select(queue_130,tail),
inference(forward_demodulation,[status(thm)],[f773,f565]) ).
fof(f4408,plain,
index_141 = select(queue_139,tail),
inference(forward_demodulation,[status(thm)],[f774,f569]) ).
fof(f4411,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_51 = X0 ),
inference(paramodulation,[status(thm)],[f536,f400]) ).
fof(f4415,plain,
index_147 = select(queue_145,tail),
inference(forward_demodulation,[status(thm)],[f775,f571]) ).
fof(f4416,plain,
index_15 = select(queue_13,tail),
inference(forward_demodulation,[status(thm)],[f756,f572]) ).
fof(f4419,plain,
index_153 = select(queue_82,tail),
inference(forward_demodulation,[status(thm)],[f766,f574]) ).
fof(f4420,plain,
index_162 = select(queue_151,tail),
inference(forward_demodulation,[status(thm)],[f776,f578]) ).
fof(f4421,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_72 = X0 ),
inference(paramodulation,[status(thm)],[f542,f400]) ).
fof(f4425,plain,
index_171 = select(queue_169,tail),
inference(forward_demodulation,[status(thm)],[f778,f582]) ).
fof(f4426,plain,
index_177 = select(queue_175,tail),
inference(forward_demodulation,[status(thm)],[f779,f584]) ).
fof(f4427,plain,
index_183 = select(queue_181,tail),
inference(forward_demodulation,[status(thm)],[f780,f587]) ).
fof(f4428,plain,
index_192 = select(queue_190,tail),
inference(forward_demodulation,[status(thm)],[f781,f591]) ).
fof(f4429,plain,
index_198 = select(queue_196,tail),
inference(forward_demodulation,[status(thm)],[f782,f593]) ).
fof(f4434,plain,
index_204 = select(queue_202,tail),
inference(forward_demodulation,[status(thm)],[f783,f595]) ).
fof(f4435,plain,
index_21 = select(queue_19,tail),
inference(forward_demodulation,[status(thm)],[f757,f598]) ).
fof(f4436,plain,
index_213 = select(queue_211,tail),
inference(forward_demodulation,[status(thm)],[f784,f600]) ).
fof(f4437,plain,
index_219 = select(queue_217,tail),
inference(forward_demodulation,[status(thm)],[f785,f602]) ).
fof(f4438,plain,
index_225 = select(queue_223,tail),
inference(forward_demodulation,[status(thm)],[f786,f604]) ).
fof(f4439,plain,
index_234 = select(queue_160,tail),
inference(forward_demodulation,[status(thm)],[f777,f608]) ).
fof(f4440,plain,
index_240 = select(queue_232,tail),
inference(forward_demodulation,[status(thm)],[f787,f611]) ).
fof(f4441,plain,
index_246 = select(queue_238,tail),
inference(forward_demodulation,[status(thm)],[f788,f613]) ).
fof(f4442,plain,
index_252 = select(queue_250,tail),
inference(forward_demodulation,[status(thm)],[f790,f615]) ).
fof(f4443,plain,
index_261 = select(queue_259,tail),
inference(forward_demodulation,[status(thm)],[f791,f620]) ).
fof(f4444,plain,
index_267 = select(queue_265,tail),
inference(forward_demodulation,[status(thm)],[f792,f622]) ).
fof(f4445,plain,
index_273 = select(queue_271,tail),
inference(forward_demodulation,[status(thm)],[f793,f625]) ).
fof(f4446,plain,
index_282 = select(queue_244,head),
inference(forward_demodulation,[status(thm)],[f789,f629]) ).
fof(f4447,plain,
index_3 = select(queue_1,tail),
inference(forward_demodulation,[status(thm)],[f754,f630]) ).
fof(f4448,plain,
index_30 = select(queue_28,tail),
inference(forward_demodulation,[status(thm)],[f758,f631]) ).
fof(f4449,plain,
index_36 = select(queue_34,tail),
inference(forward_demodulation,[status(thm)],[f759,f633]) ).
fof(f4450,plain,
index_42 = select(queue_40,tail),
inference(forward_demodulation,[status(thm)],[f760,f635]) ).
fof(f4451,plain,
index_51 = select(queue_49,tail),
inference(forward_demodulation,[status(thm)],[f761,f639]) ).
fof(f4452,plain,
index_57 = select(queue_55,tail),
inference(forward_demodulation,[status(thm)],[f762,f641]) ).
fof(f4453,plain,
index_63 = select(queue_61,tail),
inference(forward_demodulation,[status(thm)],[f763,f644]) ).
fof(f4454,plain,
index_72 = select(queue_70,tail),
inference(forward_demodulation,[status(thm)],[f764,f648]) ).
fof(f4455,plain,
index_78 = select(queue_7,tail),
inference(forward_demodulation,[status(thm)],[f755,f650]) ).
fof(f4456,plain,
index_84 = select(queue_76,tail),
inference(forward_demodulation,[status(thm)],[f765,f652]) ).
fof(f4457,plain,
index_9 = select(queue_280,tail),
inference(forward_demodulation,[status(thm)],[f794,f654]) ).
fof(f4458,plain,
index_90 = select(queue_88,tail),
inference(forward_demodulation,[status(thm)],[f767,f655]) ).
fof(f4459,plain,
index_99 = select(queue_97,tail),
inference(forward_demodulation,[status(thm)],[f768,f659]) ).
fof(f4460,plain,
! [X0] :
( select(queue_1,X0) = select(q,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f660,f400]) ).
fof(f4461,plain,
select(queue_1,head) = index_0,
inference(paramodulation,[status(thm)],[f660,f398]) ).
fof(f4462,plain,
queue_101 = store(queue_97,seq,earray_100),
inference(forward_demodulation,[status(thm)],[f768,f661]) ).
fof(f4463,plain,
! [X0] :
( select(queue_101,X0) = select(queue_97,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4462,f400]) ).
fof(f4464,plain,
select(queue_101,seq) = earray_100,
inference(paramodulation,[status(thm)],[f4462,f398]) ).
fof(f4465,plain,
! [X0] :
( select(queue_103,X0) = select(queue_101,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f662,f400]) ).
fof(f4466,plain,
select(queue_103,tail) = index_102,
inference(paramodulation,[status(thm)],[f662,f398]) ).
fof(f4467,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f4399,f4466]) ).
fof(f4470,plain,
earray_106 = store(earray_104,index_102,e22),
inference(backward_demodulation,[status(thm)],[f4467,f473]) ).
fof(f4472,plain,
index_108 = s(index_102),
inference(backward_demodulation,[status(thm)],[f4467,f555]) ).
fof(f4473,plain,
queue_107 = store(queue_103,seq,earray_106),
inference(forward_demodulation,[status(thm)],[f769,f663]) ).
fof(f4474,plain,
! [X0] :
( select(queue_107,X0) = select(queue_103,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4473,f400]) ).
fof(f4475,plain,
select(queue_107,seq) = earray_106,
inference(paramodulation,[status(thm)],[f4473,f398]) ).
fof(f4543,plain,
! [X0] :
( select(queue_109,X0) = select(queue_107,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f664,f400]) ).
fof(f4544,plain,
select(queue_109,tail) = index_108,
inference(paramodulation,[status(thm)],[f664,f398]) ).
fof(f4545,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f4400,f4544]) ).
fof(f4546,plain,
queue_11 = store(queue_280,seq,earray_10),
inference(forward_demodulation,[status(thm)],[f794,f665]) ).
fof(f4547,plain,
! [X0] :
( select(queue_11,X0) = select(queue_280,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4546,f400]) ).
fof(f4551,plain,
earray_112 = store(earray_110,index_108,e23),
inference(backward_demodulation,[status(thm)],[f4545,f475]) ).
fof(f4553,plain,
index_114 = s(index_108),
inference(backward_demodulation,[status(thm)],[f4545,f557]) ).
fof(f4621,plain,
queue_113 = store(queue_109,seq,earray_112),
inference(forward_demodulation,[status(thm)],[f770,f666]) ).
fof(f4622,plain,
! [X0] :
( select(queue_113,X0) = select(queue_109,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4621,f400]) ).
fof(f4623,plain,
select(queue_113,seq) = earray_112,
inference(paramodulation,[status(thm)],[f4621,f398]) ).
fof(f4624,plain,
! [X0] :
( select(queue_115,X0) = select(queue_113,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f667,f400]) ).
fof(f4625,plain,
select(queue_115,tail) = index_114,
inference(paramodulation,[status(thm)],[f667,f398]) ).
fof(f4626,plain,
! [X0] :
( select(queue_118,X0) = select(queue_115,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f668,f400]) ).
fof(f4627,plain,
select(queue_118,head) = index_117,
inference(paramodulation,[status(thm)],[f668,f398]) ).
fof(f4628,plain,
queue_122 = store(queue_118,seq,earray_121),
inference(forward_demodulation,[status(thm)],[f771,f669]) ).
fof(f4629,plain,
! [X0] :
( select(queue_122,X0) = select(queue_118,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4628,f400]) ).
fof(f4630,plain,
select(queue_122,seq) = earray_121,
inference(paramodulation,[status(thm)],[f4628,f398]) ).
fof(f4631,plain,
! [X0] :
( select(queue_124,X0) = select(queue_122,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f670,f400]) ).
fof(f4632,plain,
select(queue_124,tail) = index_123,
inference(paramodulation,[status(thm)],[f670,f398]) ).
fof(f4633,plain,
index_126 = index_123,
inference(forward_demodulation,[status(thm)],[f4406,f4632]) ).
fof(f4634,plain,
queue_128 = store(queue_124,seq,earray_127),
inference(forward_demodulation,[status(thm)],[f772,f671]) ).
fof(f4635,plain,
! [X0] :
( select(queue_128,X0) = select(queue_124,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4634,f400]) ).
fof(f4636,plain,
select(queue_128,seq) = earray_127,
inference(paramodulation,[status(thm)],[f4634,f398]) ).
fof(f4639,plain,
earray_127 = store(earray_125,index_123,e25),
inference(backward_demodulation,[status(thm)],[f4633,f479]) ).
fof(f4641,plain,
index_129 = s(index_123),
inference(backward_demodulation,[status(thm)],[f4633,f564]) ).
fof(f4709,plain,
! [X0] :
( select(queue_13,X0) = select(queue_11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f672,f400]) ).
fof(f4710,plain,
select(queue_13,tail) = index_12,
inference(paramodulation,[status(thm)],[f672,f398]) ).
fof(f4711,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f4416,f4710]) ).
fof(f4712,plain,
! [X0] :
( select(queue_130,X0) = select(queue_128,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f673,f400]) ).
fof(f4713,plain,
select(queue_130,tail) = index_129,
inference(paramodulation,[status(thm)],[f673,f398]) ).
fof(f4714,plain,
index_132 = index_129,
inference(forward_demodulation,[status(thm)],[f4407,f4713]) ).
fof(f4715,plain,
queue_134 = store(queue_130,seq,earray_133),
inference(forward_demodulation,[status(thm)],[f773,f674]) ).
fof(f4716,plain,
! [X0] :
( select(queue_134,X0) = select(queue_130,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4715,f400]) ).
fof(f4717,plain,
select(queue_134,seq) = earray_133,
inference(paramodulation,[status(thm)],[f4715,f398]) ).
fof(f4722,plain,
index_18 = s(index_12),
inference(backward_demodulation,[status(thm)],[f4711,f585]) ).
fof(f4725,plain,
earray_133 = store(earray_131,index_129,e26),
inference(backward_demodulation,[status(thm)],[f4714,f481]) ).
fof(f4727,plain,
index_135 = s(index_129),
inference(backward_demodulation,[status(thm)],[f4714,f566]) ).
fof(f4728,plain,
! [X0] :
( select(queue_136,X0) = select(queue_134,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f675,f400]) ).
fof(f4729,plain,
select(queue_136,tail) = index_135,
inference(paramodulation,[status(thm)],[f675,f398]) ).
fof(f4797,plain,
! [X0] :
( select(queue_139,X0) = select(queue_136,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f676,f400]) ).
fof(f4798,plain,
select(queue_139,head) = index_138,
inference(paramodulation,[status(thm)],[f676,f398]) ).
fof(f4799,plain,
queue_143 = store(queue_139,seq,earray_142),
inference(forward_demodulation,[status(thm)],[f774,f677]) ).
fof(f4800,plain,
! [X0] :
( select(queue_143,X0) = select(queue_139,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4799,f400]) ).
fof(f4801,plain,
select(queue_143,seq) = earray_142,
inference(paramodulation,[status(thm)],[f4799,f398]) ).
fof(f4869,plain,
! [X0] :
( select(queue_145,X0) = select(queue_143,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f678,f400]) ).
fof(f4870,plain,
select(queue_145,tail) = index_144,
inference(paramodulation,[status(thm)],[f678,f398]) ).
fof(f4871,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f4415,f4870]) ).
fof(f4872,plain,
queue_149 = store(queue_145,seq,earray_148),
inference(forward_demodulation,[status(thm)],[f775,f679]) ).
fof(f4873,plain,
! [X0] :
( select(queue_149,X0) = select(queue_145,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4872,f400]) ).
fof(f4874,plain,
select(queue_149,seq) = earray_148,
inference(paramodulation,[status(thm)],[f4872,f398]) ).
fof(f4875,plain,
! [X0] :
( select(queue_151,X0) = select(queue_149,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f680,f400]) ).
fof(f4876,plain,
select(queue_151,tail) = index_150,
inference(paramodulation,[status(thm)],[f680,f398]) ).
fof(f4877,plain,
index_162 = index_150,
inference(forward_demodulation,[status(thm)],[f4420,f4876]) ).
fof(f4879,plain,
earray_148 = store(earray_146,index_144,e28),
inference(backward_demodulation,[status(thm)],[f4871,f486]) ).
fof(f4882,plain,
index_150 = s(index_144),
inference(backward_demodulation,[status(thm)],[f4871,f573]) ).
fof(f4884,plain,
earray_163 = store(earray_161,index_150,e29),
inference(backward_demodulation,[status(thm)],[f4877,f491]) ).
fof(f4887,plain,
index_165 = s(index_150),
inference(backward_demodulation,[status(thm)],[f4877,f579]) ).
fof(f4888,plain,
queue_155 = store(queue_82,seq,earray_154),
inference(forward_demodulation,[status(thm)],[f766,f681]) ).
fof(f4889,plain,
! [X0] :
( select(queue_155,X0) = select(queue_82,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f4888,f400]) ).
fof(f4958,plain,
! [X0] :
( select(queue_157,X0) = select(queue_155,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f682,f400]) ).
fof(f4959,plain,
select(queue_157,tail) = index_156,
inference(paramodulation,[status(thm)],[f682,f398]) ).
fof(f4960,plain,
! [X0] :
( select(queue_160,X0) = select(queue_157,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f683,f400]) ).
fof(f4961,plain,
select(queue_160,head) = index_159,
inference(paramodulation,[status(thm)],[f683,f398]) ).
fof(f5029,plain,
queue_164 = store(queue_151,seq,earray_163),
inference(forward_demodulation,[status(thm)],[f776,f684]) ).
fof(f5030,plain,
! [X0] :
( select(queue_164,X0) = select(queue_151,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5029,f400]) ).
fof(f5031,plain,
select(queue_164,seq) = earray_163,
inference(paramodulation,[status(thm)],[f5029,f398]) ).
fof(f5032,plain,
! [X0] :
( select(queue_166,X0) = select(queue_164,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f685,f400]) ).
fof(f5033,plain,
select(queue_166,tail) = index_165,
inference(paramodulation,[status(thm)],[f685,f398]) ).
fof(f5034,plain,
! [X0] :
( select(queue_169,X0) = select(queue_166,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f686,f400]) ).
fof(f5035,plain,
select(queue_169,head) = index_168,
inference(paramodulation,[status(thm)],[f686,f398]) ).
fof(f5036,plain,
queue_17 = store(queue_13,seq,earray_16),
inference(forward_demodulation,[status(thm)],[f756,f687]) ).
fof(f5037,plain,
! [X0] :
( select(queue_17,X0) = select(queue_13,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5036,f400]) ).
fof(f5039,plain,
queue_173 = store(queue_169,seq,earray_172),
inference(forward_demodulation,[status(thm)],[f778,f688]) ).
fof(f5040,plain,
! [X0] :
( select(queue_173,X0) = select(queue_169,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5039,f400]) ).
fof(f5041,plain,
select(queue_173,seq) = earray_172,
inference(paramodulation,[status(thm)],[f5039,f398]) ).
fof(f5042,plain,
! [X0] :
( select(queue_175,X0) = select(queue_173,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f689,f400]) ).
fof(f5043,plain,
select(queue_175,tail) = index_174,
inference(paramodulation,[status(thm)],[f689,f398]) ).
fof(f5044,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f4426,f5043]) ).
fof(f5046,plain,
earray_178 = store(earray_176,index_174,e31),
inference(backward_demodulation,[status(thm)],[f5044,f495]) ).
fof(f5049,plain,
index_180 = s(index_174),
inference(backward_demodulation,[status(thm)],[f5044,f586]) ).
fof(f5117,plain,
queue_179 = store(queue_175,seq,earray_178),
inference(forward_demodulation,[status(thm)],[f779,f690]) ).
fof(f5118,plain,
! [X0] :
( select(queue_179,X0) = select(queue_175,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5117,f400]) ).
fof(f5119,plain,
select(queue_179,seq) = earray_178,
inference(paramodulation,[status(thm)],[f5117,f398]) ).
fof(f5120,plain,
! [X0] :
( select(queue_181,X0) = select(queue_179,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f691,f400]) ).
fof(f5121,plain,
select(queue_181,tail) = index_180,
inference(paramodulation,[status(thm)],[f691,f398]) ).
fof(f5122,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f4427,f5121]) ).
fof(f5123,plain,
queue_185 = store(queue_181,seq,earray_184),
inference(forward_demodulation,[status(thm)],[f780,f692]) ).
fof(f5124,plain,
! [X0] :
( select(queue_185,X0) = select(queue_181,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5123,f400]) ).
fof(f5125,plain,
select(queue_185,seq) = earray_184,
inference(paramodulation,[status(thm)],[f5123,f398]) ).
fof(f5127,plain,
earray_184 = store(earray_182,index_180,e32),
inference(backward_demodulation,[status(thm)],[f5122,f497]) ).
fof(f5130,plain,
index_186 = s(index_180),
inference(backward_demodulation,[status(thm)],[f5122,f588]) ).
fof(f5131,plain,
! [X0] :
( select(queue_187,X0) = select(queue_185,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f693,f400]) ).
fof(f5132,plain,
select(queue_187,tail) = index_186,
inference(paramodulation,[status(thm)],[f693,f398]) ).
fof(f5200,plain,
! [X0] :
( select(queue_19,X0) = select(queue_17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f694,f400]) ).
fof(f5201,plain,
select(queue_19,tail) = index_18,
inference(paramodulation,[status(thm)],[f694,f398]) ).
fof(f5202,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f4435,f5201]) ).
fof(f5203,plain,
! [X0] :
( select(queue_190,X0) = select(queue_187,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f695,f400]) ).
fof(f5204,plain,
select(queue_190,head) = index_189,
inference(paramodulation,[status(thm)],[f695,f398]) ).
fof(f5210,plain,
index_24 = s(index_18),
inference(backward_demodulation,[status(thm)],[f5202,f610]) ).
fof(f5278,plain,
queue_194 = store(queue_190,seq,earray_193),
inference(forward_demodulation,[status(thm)],[f781,f696]) ).
fof(f5279,plain,
! [X0] :
( select(queue_194,X0) = select(queue_190,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5278,f400]) ).
fof(f5280,plain,
select(queue_194,seq) = earray_193,
inference(paramodulation,[status(thm)],[f5278,f398]) ).
fof(f5281,plain,
! [X0] :
( select(queue_196,X0) = select(queue_194,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f697,f400]) ).
fof(f5282,plain,
select(queue_196,tail) = index_195,
inference(paramodulation,[status(thm)],[f697,f398]) ).
fof(f5283,plain,
index_198 = index_195,
inference(forward_demodulation,[status(thm)],[f4429,f5282]) ).
fof(f5284,plain,
queue_200 = store(queue_196,seq,earray_199),
inference(forward_demodulation,[status(thm)],[f782,f698]) ).
fof(f5285,plain,
! [X0] :
( select(queue_200,X0) = select(queue_196,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5284,f400]) ).
fof(f5286,plain,
select(queue_200,seq) = earray_199,
inference(paramodulation,[status(thm)],[f5284,f398]) ).
fof(f5288,plain,
earray_199 = store(earray_197,index_195,e34),
inference(backward_demodulation,[status(thm)],[f5283,f501]) ).
fof(f5291,plain,
index_201 = s(index_195),
inference(backward_demodulation,[status(thm)],[f5283,f594]) ).
fof(f5292,plain,
! [X0] :
( select(queue_202,X0) = select(queue_200,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f699,f400]) ).
fof(f5293,plain,
select(queue_202,tail) = index_201,
inference(paramodulation,[status(thm)],[f699,f398]) ).
fof(f5294,plain,
index_204 = index_201,
inference(forward_demodulation,[status(thm)],[f4434,f5293]) ).
fof(f5296,plain,
earray_205 = store(earray_203,index_201,e35),
inference(backward_demodulation,[status(thm)],[f5294,f505]) ).
fof(f5299,plain,
index_207 = s(index_201),
inference(backward_demodulation,[status(thm)],[f5294,f596]) ).
fof(f5367,plain,
queue_206 = store(queue_202,seq,earray_205),
inference(forward_demodulation,[status(thm)],[f783,f700]) ).
fof(f5368,plain,
! [X0] :
( select(queue_206,X0) = select(queue_202,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5367,f400]) ).
fof(f5369,plain,
select(queue_206,seq) = earray_205,
inference(paramodulation,[status(thm)],[f5367,f398]) ).
fof(f5370,plain,
! [X0] :
( select(queue_208,X0) = select(queue_206,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f701,f400]) ).
fof(f5371,plain,
select(queue_208,tail) = index_207,
inference(paramodulation,[status(thm)],[f701,f398]) ).
fof(f5442,plain,
! [X0] :
( select(queue_211,X0) = select(queue_208,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f702,f400]) ).
fof(f5443,plain,
select(queue_211,head) = index_210,
inference(paramodulation,[status(thm)],[f702,f398]) ).
fof(f5444,plain,
queue_215 = store(queue_211,seq,earray_214),
inference(forward_demodulation,[status(thm)],[f784,f703]) ).
fof(f5445,plain,
! [X0] :
( select(queue_215,X0) = select(queue_211,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5444,f400]) ).
fof(f5446,plain,
select(queue_215,seq) = earray_214,
inference(paramodulation,[status(thm)],[f5444,f398]) ).
fof(f5447,plain,
! [X0] :
( select(queue_217,X0) = select(queue_215,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f704,f400]) ).
fof(f5448,plain,
select(queue_217,tail) = index_216,
inference(paramodulation,[status(thm)],[f704,f398]) ).
fof(f5449,plain,
index_219 = index_216,
inference(forward_demodulation,[status(thm)],[f4437,f5448]) ).
fof(f5452,plain,
earray_220 = store(earray_218,index_216,e37),
inference(backward_demodulation,[status(thm)],[f5449,f510]) ).
fof(f5455,plain,
index_222 = s(index_216),
inference(backward_demodulation,[status(thm)],[f5449,f603]) ).
fof(f5456,plain,
queue_221 = store(queue_217,seq,earray_220),
inference(forward_demodulation,[status(thm)],[f785,f705]) ).
fof(f5457,plain,
! [X0] :
( select(queue_221,X0) = select(queue_217,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5456,f400]) ).
fof(f5458,plain,
select(queue_221,seq) = earray_220,
inference(paramodulation,[status(thm)],[f5456,f398]) ).
fof(f5527,plain,
! [X0] :
( select(queue_223,X0) = select(queue_221,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f706,f400]) ).
fof(f5528,plain,
select(queue_223,tail) = index_222,
inference(paramodulation,[status(thm)],[f706,f398]) ).
fof(f5529,plain,
index_225 = index_222,
inference(forward_demodulation,[status(thm)],[f4438,f5528]) ).
fof(f5530,plain,
queue_227 = store(queue_223,seq,earray_226),
inference(forward_demodulation,[status(thm)],[f786,f707]) ).
fof(f5531,plain,
! [X0] :
( select(queue_227,X0) = select(queue_223,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5530,f400]) ).
fof(f5532,plain,
select(queue_227,seq) = earray_226,
inference(paramodulation,[status(thm)],[f5530,f398]) ).
fof(f5535,plain,
earray_226 = store(earray_224,index_222,e38),
inference(backward_demodulation,[status(thm)],[f5529,f512]) ).
fof(f5538,plain,
index_228 = s(index_222),
inference(backward_demodulation,[status(thm)],[f5529,f605]) ).
fof(f5607,plain,
! [X0] :
( select(queue_229,X0) = select(queue_227,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f708,f400]) ).
fof(f5608,plain,
select(queue_229,tail) = index_228,
inference(paramodulation,[status(thm)],[f708,f398]) ).
fof(f5609,plain,
queue_23 = store(queue_19,seq,earray_22),
inference(forward_demodulation,[status(thm)],[f757,f709]) ).
fof(f5610,plain,
! [X0] :
( select(queue_23,X0) = select(queue_19,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5609,f400]) ).
fof(f5612,plain,
! [X0] :
( select(queue_232,X0) = select(queue_229,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f710,f400]) ).
fof(f5613,plain,
select(queue_232,head) = index_231,
inference(paramodulation,[status(thm)],[f710,f398]) ).
fof(f5616,plain,
queue_236 = store(queue_160,seq,earray_235),
inference(forward_demodulation,[status(thm)],[f777,f711]) ).
fof(f5617,plain,
! [X0] :
( select(queue_236,X0) = select(queue_160,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5616,f400]) ).
fof(f5626,plain,
! [X0] :
( select(queue_238,X0) = select(queue_236,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f712,f400]) ).
fof(f5627,plain,
select(queue_238,tail) = index_237,
inference(paramodulation,[status(thm)],[f712,f398]) ).
fof(f5628,plain,
index_246 = index_237,
inference(forward_demodulation,[status(thm)],[f4441,f5627]) ).
fof(f5629,plain,
queue_242 = store(queue_232,seq,earray_241),
inference(forward_demodulation,[status(thm)],[f787,f713]) ).
fof(f5630,plain,
! [X0] :
( select(queue_242,X0) = select(queue_232,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5629,f400]) ).
fof(f5631,plain,
select(queue_242,seq) = earray_241,
inference(paramodulation,[status(thm)],[f5629,f398]) ).
fof(f5637,plain,
index_249 = s(index_237),
inference(backward_demodulation,[status(thm)],[f5628,f614]) ).
fof(f5706,plain,
! [X0] :
( select(queue_244,X0) = select(queue_242,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f714,f400]) ).
fof(f5708,plain,
queue_248 = store(queue_238,seq,earray_247),
inference(forward_demodulation,[status(thm)],[f788,f715]) ).
fof(f5709,plain,
! [X0] :
( select(queue_248,X0) = select(queue_238,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5708,f400]) ).
fof(f5711,plain,
! [X0] :
( select(queue_25,X0) = select(queue_23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f716,f400]) ).
fof(f5712,plain,
select(queue_25,tail) = index_24,
inference(paramodulation,[status(thm)],[f716,f398]) ).
fof(f5714,plain,
! [X0] :
( select(queue_250,X0) = select(queue_248,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f717,f400]) ).
fof(f5715,plain,
select(queue_250,tail) = index_249,
inference(paramodulation,[status(thm)],[f717,f398]) ).
fof(f5716,plain,
index_252 = index_249,
inference(forward_demodulation,[status(thm)],[f4442,f5715]) ).
fof(f5722,plain,
index_255 = s(index_249),
inference(backward_demodulation,[status(thm)],[f5716,f616]) ).
fof(f5791,plain,
queue_254 = store(queue_250,seq,earray_253),
inference(forward_demodulation,[status(thm)],[f790,f718]) ).
fof(f5792,plain,
! [X0] :
( select(queue_254,X0) = select(queue_250,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5791,f400]) ).
fof(f5794,plain,
! [X0] :
( select(queue_256,X0) = select(queue_254,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f719,f400]) ).
fof(f5795,plain,
select(queue_256,tail) = index_255,
inference(paramodulation,[status(thm)],[f719,f398]) ).
fof(f5800,plain,
! [X0] :
( select(queue_259,X0) = select(queue_256,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f720,f400]) ).
fof(f5801,plain,
select(queue_259,head) = index_258,
inference(paramodulation,[status(thm)],[f720,f398]) ).
fof(f5802,plain,
queue_263 = store(queue_259,seq,earray_262),
inference(forward_demodulation,[status(thm)],[f791,f721]) ).
fof(f5803,plain,
! [X0] :
( select(queue_263,X0) = select(queue_259,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5802,f400]) ).
fof(f5805,plain,
! [X0] :
( select(queue_265,X0) = select(queue_263,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f722,f400]) ).
fof(f5806,plain,
select(queue_265,tail) = index_264,
inference(paramodulation,[status(thm)],[f722,f398]) ).
fof(f5807,plain,
index_267 = index_264,
inference(forward_demodulation,[status(thm)],[f4444,f5806]) ).
fof(f5813,plain,
index_270 = s(index_264),
inference(backward_demodulation,[status(thm)],[f5807,f624]) ).
fof(f5814,plain,
queue_269 = store(queue_265,seq,earray_268),
inference(forward_demodulation,[status(thm)],[f792,f723]) ).
fof(f5815,plain,
! [X0] :
( select(queue_269,X0) = select(queue_265,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5814,f400]) ).
fof(f5885,plain,
! [X0] :
( select(queue_271,X0) = select(queue_269,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f724,f400]) ).
fof(f5886,plain,
select(queue_271,tail) = index_270,
inference(paramodulation,[status(thm)],[f724,f398]) ).
fof(f5887,plain,
index_273 = index_270,
inference(forward_demodulation,[status(thm)],[f4445,f5886]) ).
fof(f5888,plain,
queue_275 = store(queue_271,seq,earray_274),
inference(forward_demodulation,[status(thm)],[f793,f725]) ).
fof(f5889,plain,
! [X0] :
( select(queue_275,X0) = select(queue_271,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5888,f400]) ).
fof(f5896,plain,
index_276 = s(index_270),
inference(backward_demodulation,[status(thm)],[f5887,f626]) ).
fof(f5965,plain,
! [X0] :
( select(queue_277,X0) = select(queue_275,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f726,f400]) ).
fof(f5966,plain,
select(queue_277,tail) = index_276,
inference(paramodulation,[status(thm)],[f726,f398]) ).
fof(f5967,plain,
! [X0] :
( select(queue_28,X0) = select(queue_25,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f727,f400]) ).
fof(f5968,plain,
select(queue_28,head) = index_27,
inference(paramodulation,[status(thm)],[f727,f398]) ).
fof(f5969,plain,
! [X0] :
( select(queue_280,X0) = select(queue_277,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f728,f400]) ).
fof(f5970,plain,
select(queue_280,head) = index_279,
inference(paramodulation,[status(thm)],[f728,f398]) ).
fof(f5972,plain,
queue_32 = store(queue_28,seq,earray_31),
inference(forward_demodulation,[status(thm)],[f758,f729]) ).
fof(f5973,plain,
! [X0] :
( select(queue_32,X0) = select(queue_28,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5972,f400]) ).
fof(f5981,plain,
! [X0] :
( select(queue_34,X0) = select(queue_32,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f730,f400]) ).
fof(f5982,plain,
select(queue_34,tail) = index_33,
inference(paramodulation,[status(thm)],[f730,f398]) ).
fof(f5983,plain,
index_36 = index_33,
inference(forward_demodulation,[status(thm)],[f4449,f5982]) ).
fof(f5984,plain,
queue_38 = store(queue_34,seq,earray_37),
inference(forward_demodulation,[status(thm)],[f759,f731]) ).
fof(f5985,plain,
! [X0] :
( select(queue_38,X0) = select(queue_34,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f5984,f400]) ).
fof(f5986,plain,
select(queue_38,seq) = earray_37,
inference(paramodulation,[status(thm)],[f5984,f398]) ).
fof(f5987,plain,
s(s(index_39)) != index_33,
inference(backward_demodulation,[status(thm)],[f5983,f3731]) ).
fof(f5989,plain,
s(index_39) != index_33,
inference(backward_demodulation,[status(thm)],[f5983,f3281]) ).
fof(f5990,plain,
index_39 != index_33,
inference(backward_demodulation,[status(thm)],[f5983,f3302]) ).
fof(f5991,plain,
index_39 = s(index_33),
inference(backward_demodulation,[status(thm)],[f5983,f634]) ).
fof(f5993,plain,
select(earray_37,index_33) = e13,
inference(backward_demodulation,[status(thm)],[f5983,f796]) ).
fof(f6063,plain,
! [X0] :
( select(queue_40,X0) = select(queue_38,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f732,f400]) ).
fof(f6064,plain,
select(queue_40,tail) = index_39,
inference(paramodulation,[status(thm)],[f732,f398]) ).
fof(f6065,plain,
index_42 = index_39,
inference(forward_demodulation,[status(thm)],[f4450,f6064]) ).
fof(f6066,plain,
queue_44 = store(queue_40,seq,earray_43),
inference(forward_demodulation,[status(thm)],[f760,f733]) ).
fof(f6067,plain,
! [X0] :
( select(queue_44,X0) = select(queue_40,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6066,f400]) ).
fof(f6068,plain,
select(queue_44,seq) = earray_43,
inference(paramodulation,[status(thm)],[f6066,f398]) ).
fof(f6069,plain,
! [X0] :
( select(queue_46,X0) = select(queue_44,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f734,f400]) ).
fof(f6070,plain,
select(queue_46,tail) = index_45,
inference(paramodulation,[status(thm)],[f734,f398]) ).
fof(f6077,plain,
earray_43 = store(earray_41,index_39,e14),
inference(backward_demodulation,[status(thm)],[f6065,f534]) ).
fof(f6080,plain,
index_45 = s(index_39),
inference(backward_demodulation,[status(thm)],[f6065,f636]) ).
fof(f6081,plain,
! [X0] :
( select(queue_49,X0) = select(queue_46,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f735,f400]) ).
fof(f6082,plain,
select(queue_49,head) = index_48,
inference(paramodulation,[status(thm)],[f735,f398]) ).
fof(f6083,plain,
queue_5 = store(queue_1,seq,earray_4),
inference(forward_demodulation,[status(thm)],[f754,f736]) ).
fof(f6084,plain,
! [X0] :
( select(queue_5,X0) = select(queue_1,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6083,f400]) ).
fof(f6087,plain,
index_45 != index_33,
inference(backward_demodulation,[status(thm)],[f6080,f5989]) ).
fof(f6159,plain,
queue_53 = store(queue_49,seq,earray_52),
inference(forward_demodulation,[status(thm)],[f761,f737]) ).
fof(f6160,plain,
! [X0] :
( select(queue_53,X0) = select(queue_49,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6159,f400]) ).
fof(f6161,plain,
select(queue_53,seq) = earray_52,
inference(paramodulation,[status(thm)],[f6159,f398]) ).
fof(f6162,plain,
! [X0] :
( select(queue_55,X0) = select(queue_53,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f738,f400]) ).
fof(f6163,plain,
select(queue_55,tail) = index_54,
inference(paramodulation,[status(thm)],[f738,f398]) ).
fof(f6164,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f4452,f6163]) ).
fof(f6165,plain,
queue_59 = store(queue_55,seq,earray_58),
inference(forward_demodulation,[status(thm)],[f762,f739]) ).
fof(f6166,plain,
! [X0] :
( select(queue_59,X0) = select(queue_55,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6165,f400]) ).
fof(f6167,plain,
select(queue_59,seq) = earray_58,
inference(paramodulation,[status(thm)],[f6165,f398]) ).
fof(f6169,plain,
earray_58 = store(earray_56,index_54,e16),
inference(backward_demodulation,[status(thm)],[f6164,f538]) ).
fof(f6172,plain,
index_60 = s(index_54),
inference(backward_demodulation,[status(thm)],[f6164,f643]) ).
fof(f6173,plain,
! [X0] :
( select(queue_61,X0) = select(queue_59,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f740,f400]) ).
fof(f6174,plain,
select(queue_61,tail) = index_60,
inference(paramodulation,[status(thm)],[f740,f398]) ).
fof(f6175,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f4453,f6174]) ).
fof(f6177,plain,
earray_64 = store(earray_62,index_60,e17),
inference(backward_demodulation,[status(thm)],[f6175,f540]) ).
fof(f6180,plain,
index_66 = s(index_60),
inference(backward_demodulation,[status(thm)],[f6175,f645]) ).
fof(f6249,plain,
queue_65 = store(queue_61,seq,earray_64),
inference(forward_demodulation,[status(thm)],[f763,f741]) ).
fof(f6250,plain,
! [X0] :
( select(queue_65,X0) = select(queue_61,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6249,f400]) ).
fof(f6251,plain,
select(queue_65,seq) = earray_64,
inference(paramodulation,[status(thm)],[f6249,f398]) ).
fof(f6252,plain,
! [X0] :
( select(queue_67,X0) = select(queue_65,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f742,f400]) ).
fof(f6253,plain,
select(queue_67,tail) = index_66,
inference(paramodulation,[status(thm)],[f742,f398]) ).
fof(f6322,plain,
! [X0] :
( select(queue_7,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f743,f400]) ).
fof(f6323,plain,
select(queue_7,tail) = index_6,
inference(paramodulation,[status(thm)],[f743,f398]) ).
fof(f6324,plain,
index_78 = index_6,
inference(forward_demodulation,[status(thm)],[f4455,f6323]) ).
fof(f6325,plain,
! [X0] :
( select(queue_70,X0) = select(queue_67,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f744,f400]) ).
fof(f6326,plain,
select(queue_70,head) = index_69,
inference(paramodulation,[status(thm)],[f744,f398]) ).
fof(f6327,plain,
queue_74 = store(queue_70,seq,earray_73),
inference(forward_demodulation,[status(thm)],[f764,f745]) ).
fof(f6328,plain,
! [X0] :
( select(queue_74,X0) = select(queue_70,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6327,f400]) ).
fof(f6329,plain,
select(queue_74,seq) = earray_73,
inference(paramodulation,[status(thm)],[f6327,f398]) ).
fof(f6334,plain,
index_81 = s(index_6),
inference(backward_demodulation,[status(thm)],[f6324,f651]) ).
fof(f6335,plain,
! [X0] :
( select(queue_76,X0) = select(queue_74,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f746,f400]) ).
fof(f6336,plain,
select(queue_76,tail) = index_75,
inference(paramodulation,[status(thm)],[f746,f398]) ).
fof(f6337,plain,
index_84 = index_75,
inference(forward_demodulation,[status(thm)],[f4456,f6336]) ).
fof(f6339,plain,
earray_85 = store(earray_83,index_75,e19),
inference(backward_demodulation,[status(thm)],[f6337,f547]) ).
fof(f6342,plain,
index_87 = s(index_75),
inference(backward_demodulation,[status(thm)],[f6337,f653]) ).
fof(f6411,plain,
queue_80 = store(queue_7,seq,earray_79),
inference(forward_demodulation,[status(thm)],[f755,f747]) ).
fof(f6412,plain,
! [X0] :
( select(queue_80,X0) = select(queue_7,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6411,f400]) ).
fof(f6414,plain,
! [X0] :
( select(queue_82,X0) = select(queue_80,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f748,f400]) ).
fof(f6415,plain,
select(queue_82,tail) = index_81,
inference(paramodulation,[status(thm)],[f748,f398]) ).
fof(f6416,plain,
index_153 = index_81,
inference(forward_demodulation,[status(thm)],[f4419,f6415]) ).
fof(f6422,plain,
index_156 = s(index_81),
inference(backward_demodulation,[status(thm)],[f6416,f575]) ).
fof(f6490,plain,
queue_86 = store(queue_76,seq,earray_85),
inference(forward_demodulation,[status(thm)],[f765,f749]) ).
fof(f6491,plain,
! [X0] :
( select(queue_86,X0) = select(queue_76,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6490,f400]) ).
fof(f6492,plain,
select(queue_86,seq) = earray_85,
inference(paramodulation,[status(thm)],[f6490,f398]) ).
fof(f6493,plain,
! [X0] :
( select(queue_88,X0) = select(queue_86,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f750,f400]) ).
fof(f6494,plain,
select(queue_88,tail) = index_87,
inference(paramodulation,[status(thm)],[f750,f398]) ).
fof(f6495,plain,
index_90 = index_87,
inference(forward_demodulation,[status(thm)],[f4458,f6494]) ).
fof(f6496,plain,
queue_92 = store(queue_88,seq,earray_91),
inference(forward_demodulation,[status(thm)],[f767,f751]) ).
fof(f6497,plain,
! [X0] :
( select(queue_92,X0) = select(queue_88,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f6496,f400]) ).
fof(f6498,plain,
select(queue_92,seq) = earray_91,
inference(paramodulation,[status(thm)],[f6496,f398]) ).
fof(f6500,plain,
earray_91 = store(earray_89,index_87,e20),
inference(backward_demodulation,[status(thm)],[f6495,f549]) ).
fof(f6503,plain,
index_93 = s(index_87),
inference(backward_demodulation,[status(thm)],[f6495,f656]) ).
fof(f6504,plain,
! [X0] :
( select(queue_94,X0) = select(queue_92,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f752,f400]) ).
fof(f6505,plain,
select(queue_94,tail) = index_93,
inference(paramodulation,[status(thm)],[f752,f398]) ).
fof(f6574,plain,
! [X0] :
( select(queue_97,X0) = select(queue_94,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f753,f400]) ).
fof(f6575,plain,
select(queue_97,head) = index_96,
inference(paramodulation,[status(thm)],[f753,f398]) ).
fof(f6646,plain,
! [X0] :
( select(earray_106,X0) = select(earray_104,X0)
| index_102 = X0 ),
inference(paramodulation,[status(thm)],[f4470,f400]) ).
fof(f6648,plain,
! [X0] :
( select(earray_112,X0) = select(earray_110,X0)
| index_108 = X0 ),
inference(paramodulation,[status(thm)],[f4551,f400]) ).
fof(f6657,plain,
! [X0] :
( select(earray_127,X0) = select(earray_125,X0)
| index_123 = X0 ),
inference(paramodulation,[status(thm)],[f4639,f400]) ).
fof(f6665,plain,
! [X0] :
( select(earray_133,X0) = select(earray_131,X0)
| index_129 = X0 ),
inference(paramodulation,[status(thm)],[f4725,f400]) ).
fof(f6671,plain,
! [X0] :
( select(earray_148,X0) = select(earray_146,X0)
| index_144 = X0 ),
inference(paramodulation,[status(thm)],[f4879,f400]) ).
fof(f6677,plain,
! [X0] :
( select(earray_163,X0) = select(earray_161,X0)
| index_150 = X0 ),
inference(paramodulation,[status(thm)],[f4884,f400]) ).
fof(f6679,plain,
! [X0] :
( select(earray_178,X0) = select(earray_176,X0)
| index_174 = X0 ),
inference(paramodulation,[status(thm)],[f5046,f400]) ).
fof(f6685,plain,
! [X0] :
( select(earray_184,X0) = select(earray_182,X0)
| index_180 = X0 ),
inference(paramodulation,[status(thm)],[f5127,f400]) ).
fof(f6692,plain,
! [X0] :
( select(earray_199,X0) = select(earray_197,X0)
| index_195 = X0 ),
inference(paramodulation,[status(thm)],[f5288,f400]) ).
fof(f6698,plain,
! [X0] :
( select(earray_205,X0) = select(earray_203,X0)
| index_201 = X0 ),
inference(paramodulation,[status(thm)],[f5296,f400]) ).
fof(f6703,plain,
! [X0] :
( select(earray_220,X0) = select(earray_218,X0)
| index_216 = X0 ),
inference(paramodulation,[status(thm)],[f5452,f400]) ).
fof(f6705,plain,
! [X0] :
( select(earray_226,X0) = select(earray_224,X0)
| index_222 = X0 ),
inference(paramodulation,[status(thm)],[f5535,f400]) ).
fof(f6718,plain,
! [X0] :
( select(earray_43,X0) = select(earray_41,X0)
| index_39 = X0 ),
inference(paramodulation,[status(thm)],[f6077,f400]) ).
fof(f6721,plain,
! [X0] :
( select(earray_58,X0) = select(earray_56,X0)
| index_54 = X0 ),
inference(paramodulation,[status(thm)],[f6169,f400]) ).
fof(f6723,plain,
! [X0] :
( select(earray_64,X0) = select(earray_62,X0)
| index_60 = X0 ),
inference(paramodulation,[status(thm)],[f6177,f400]) ).
fof(f6728,plain,
! [X0] :
( select(earray_85,X0) = select(earray_83,X0)
| index_75 = X0 ),
inference(paramodulation,[status(thm)],[f6339,f400]) ).
fof(f6734,plain,
! [X0] :
( select(earray_91,X0) = select(earray_89,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f6500,f400]) ).
fof(f6768,plain,
s(index_45) != index_33,
inference(forward_demodulation,[status(thm)],[f6080,f5987]) ).
fof(f6802,plain,
s(s(index_45)) != index_36,
inference(forward_demodulation,[status(thm)],[f6080,f3556]) ).
fof(f6803,plain,
s(s(index_45)) != index_33,
inference(forward_demodulation,[status(thm)],[f5983,f6802]) ).
fof(f6937,plain,
s(s(s(index_45))) != index_36,
inference(forward_demodulation,[status(thm)],[f6080,f3449]) ).
fof(f6938,plain,
s(s(s(index_45))) != index_33,
inference(forward_demodulation,[status(thm)],[f5983,f6937]) ).
fof(f7186,plain,
( index_3 = select(q,tail)
| head = tail ),
inference(paramodulation,[status(thm)],[f4447,f4460]) ).
fof(f7191,plain,
( index_3 = index_0
| head = tail ),
inference(forward_demodulation,[status(thm)],[f552,f7186]) ).
fof(f7192,plain,
index_3 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[f7191,f401]) ).
fof(f7208,plain,
index_6 = s(index_0),
inference(backward_demodulation,[status(thm)],[f7192,f642]) ).
fof(f7416,plain,
( select(queue_101,head) = index_96
| seq = head ),
inference(paramodulation,[status(thm)],[f6575,f4463]) ).
fof(f7422,plain,
select(queue_101,head) = index_96,
inference(forward_subsumption_resolution,[status(thm)],[f7416,f402]) ).
fof(f7431,plain,
( earray_104 = select(queue_101,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f3974,f4465]) ).
fof(f7434,plain,
( earray_104 = earray_100
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4464,f7431]) ).
fof(f7435,plain,
earray_104 = earray_100,
inference(forward_subsumption_resolution,[status(thm)],[f7434,f403]) ).
fof(f7452,plain,
( earray_110 = select(queue_107,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4043,f4543]) ).
fof(f7455,plain,
( earray_110 = earray_106
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4475,f7452]) ).
fof(f7456,plain,
earray_110 = earray_106,
inference(forward_subsumption_resolution,[status(thm)],[f7455,f403]) ).
fof(f7468,plain,
( select(queue_11,head) = index_279
| seq = head ),
inference(paramodulation,[status(thm)],[f5970,f4547]) ).
fof(f7474,plain,
select(queue_11,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[f7468,f402]) ).
fof(f7487,plain,
( index_116 = select(queue_113,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f558,f4624]) ).
fof(f7490,plain,
index_116 = select(queue_113,head),
inference(forward_subsumption_resolution,[status(thm)],[f7487,f401]) ).
fof(f7492,plain,
( seq = head
| index_116 = select(queue_109,head) ),
inference(paramodulation,[status(thm)],[f4622,f7490]) ).
fof(f7494,plain,
index_116 = select(queue_109,head),
inference(forward_subsumption_resolution,[status(thm)],[f7492,f402]) ).
fof(f7496,plain,
( tail = head
| index_116 = select(queue_107,head) ),
inference(paramodulation,[status(thm)],[f4543,f7494]) ).
fof(f7498,plain,
index_116 = select(queue_107,head),
inference(forward_subsumption_resolution,[status(thm)],[f7496,f401]) ).
fof(f7500,plain,
( seq = head
| index_116 = select(queue_103,head) ),
inference(paramodulation,[status(thm)],[f4474,f7498]) ).
fof(f7502,plain,
index_116 = select(queue_103,head),
inference(forward_subsumption_resolution,[status(thm)],[f7500,f402]) ).
fof(f7507,plain,
( tail = head
| index_116 = select(queue_101,head) ),
inference(paramodulation,[status(thm)],[f4465,f7502]) ).
fof(f7509,plain,
( tail = head
| index_116 = index_96 ),
inference(forward_demodulation,[status(thm)],[f7422,f7507]) ).
fof(f7510,plain,
index_116 = index_96,
inference(forward_subsumption_resolution,[status(thm)],[f7509,f401]) ).
fof(f7521,plain,
index_116 = s(index_95),
inference(backward_demodulation,[status(thm)],[f7510,f658]) ).
fof(f7667,plain,
( select(queue_118,tail) = index_114
| head = tail ),
inference(paramodulation,[status(thm)],[f4625,f4626]) ).
fof(f7669,plain,
! [X0] :
( tail = X0
| select(queue_118,X0) = select(queue_113,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4624,f4626]) ).
fof(f7673,plain,
( index_120 = index_114
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4405,f7667]) ).
fof(f7674,plain,
index_120 = index_114,
inference(forward_subsumption_resolution,[status(thm)],[f7673,f401]) ).
fof(f7707,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_114 = X0 ),
inference(backward_demodulation,[status(thm)],[f7674,f4311]) ).
fof(f7716,plain,
index_123 = s(index_114),
inference(backward_demodulation,[status(thm)],[f7674,f562]) ).
fof(f8179,plain,
( earray_125 = select(queue_122,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4313,f4631]) ).
fof(f8182,plain,
( earray_125 = earray_121
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4630,f8179]) ).
fof(f8183,plain,
earray_125 = earray_121,
inference(forward_subsumption_resolution,[status(thm)],[f8182,f403]) ).
fof(f8217,plain,
( earray_131 = select(queue_128,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4316,f4712]) ).
fof(f8220,plain,
( earray_131 = earray_127
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4636,f8217]) ).
fof(f8221,plain,
earray_131 = earray_127,
inference(forward_subsumption_resolution,[status(thm)],[f8220,f403]) ).
fof(f8240,plain,
( index_137 = select(queue_134,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f567,f4728]) ).
fof(f8243,plain,
index_137 = select(queue_134,head),
inference(forward_subsumption_resolution,[status(thm)],[f8240,f401]) ).
fof(f8245,plain,
( seq = head
| index_137 = select(queue_130,head) ),
inference(paramodulation,[status(thm)],[f4716,f8243]) ).
fof(f8247,plain,
index_137 = select(queue_130,head),
inference(forward_subsumption_resolution,[status(thm)],[f8245,f402]) ).
fof(f8251,plain,
( tail = head
| index_137 = select(queue_128,head) ),
inference(paramodulation,[status(thm)],[f4712,f8247]) ).
fof(f8253,plain,
index_137 = select(queue_128,head),
inference(forward_subsumption_resolution,[status(thm)],[f8251,f401]) ).
fof(f8255,plain,
( seq = head
| index_137 = select(queue_124,head) ),
inference(paramodulation,[status(thm)],[f4635,f8253]) ).
fof(f8257,plain,
index_137 = select(queue_124,head),
inference(forward_subsumption_resolution,[status(thm)],[f8255,f402]) ).
fof(f8263,plain,
( tail = head
| index_137 = select(queue_122,head) ),
inference(paramodulation,[status(thm)],[f4631,f8257]) ).
fof(f8265,plain,
index_137 = select(queue_122,head),
inference(forward_subsumption_resolution,[status(thm)],[f8263,f401]) ).
fof(f8267,plain,
( seq = head
| index_137 = select(queue_118,head) ),
inference(paramodulation,[status(thm)],[f4629,f8265]) ).
fof(f8269,plain,
( seq = head
| index_137 = index_117 ),
inference(forward_demodulation,[status(thm)],[f4627,f8267]) ).
fof(f8270,plain,
index_137 = index_117,
inference(forward_subsumption_resolution,[status(thm)],[f8269,f402]) ).
fof(f8284,plain,
index_138 = s(index_117),
inference(backward_demodulation,[status(thm)],[f8270,f568]) ).
fof(f8429,plain,
( select(queue_139,tail) = index_135
| head = tail ),
inference(paramodulation,[status(thm)],[f4729,f4797]) ).
fof(f8430,plain,
! [X0] :
( tail = X0
| select(queue_139,X0) = select(queue_134,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4728,f4797]) ).
fof(f8434,plain,
( index_141 = index_135
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4408,f8429]) ).
fof(f8435,plain,
index_141 = index_135,
inference(forward_subsumption_resolution,[status(thm)],[f8434,f401]) ).
fof(f8438,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_135 = X0 ),
inference(backward_demodulation,[status(thm)],[f8435,f4321]) ).
fof(f8447,plain,
index_144 = s(index_135),
inference(backward_demodulation,[status(thm)],[f8435,f570]) ).
fof(f8806,plain,
( earray_146 = select(queue_143,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4323,f4869]) ).
fof(f8809,plain,
( earray_146 = earray_142
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4801,f8806]) ).
fof(f8810,plain,
earray_146 = earray_142,
inference(forward_subsumption_resolution,[status(thm)],[f8809,f403]) ).
fof(f8831,plain,
( earray_161 = select(queue_149,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4331,f4875]) ).
fof(f8834,plain,
( earray_161 = earray_148
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f4874,f8831]) ).
fof(f8835,plain,
earray_161 = earray_148,
inference(forward_subsumption_resolution,[status(thm)],[f8834,f403]) ).
fof(f8872,plain,
( index_158 = select(queue_155,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f576,f4958]) ).
fof(f8875,plain,
index_158 = select(queue_155,head),
inference(forward_subsumption_resolution,[status(thm)],[f8872,f401]) ).
fof(f8877,plain,
( select(queue_160,tail) = index_156
| head = tail ),
inference(paramodulation,[status(thm)],[f4959,f4960]) ).
fof(f8883,plain,
( index_234 = index_156
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4439,f8877]) ).
fof(f8884,plain,
index_234 = index_156,
inference(forward_subsumption_resolution,[status(thm)],[f8883,f401]) ).
fof(f8896,plain,
index_237 = s(index_156),
inference(backward_demodulation,[status(thm)],[f8884,f609]) ).
fof(f9173,plain,
( index_167 = select(queue_164,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f580,f5032]) ).
fof(f9176,plain,
index_167 = select(queue_164,head),
inference(forward_subsumption_resolution,[status(thm)],[f9173,f401]) ).
fof(f9178,plain,
( seq = head
| index_167 = select(queue_151,head) ),
inference(paramodulation,[status(thm)],[f5030,f9176]) ).
fof(f9180,plain,
index_167 = select(queue_151,head),
inference(forward_subsumption_resolution,[status(thm)],[f9178,f402]) ).
fof(f9182,plain,
( tail = head
| index_167 = select(queue_149,head) ),
inference(paramodulation,[status(thm)],[f4875,f9180]) ).
fof(f9184,plain,
index_167 = select(queue_149,head),
inference(forward_subsumption_resolution,[status(thm)],[f9182,f401]) ).
fof(f9194,plain,
( seq = head
| index_167 = select(queue_145,head) ),
inference(paramodulation,[status(thm)],[f4873,f9184]) ).
fof(f9196,plain,
index_167 = select(queue_145,head),
inference(forward_subsumption_resolution,[status(thm)],[f9194,f402]) ).
fof(f9198,plain,
( tail = head
| index_167 = select(queue_143,head) ),
inference(paramodulation,[status(thm)],[f4869,f9196]) ).
fof(f9200,plain,
index_167 = select(queue_143,head),
inference(forward_subsumption_resolution,[status(thm)],[f9198,f401]) ).
fof(f9202,plain,
( seq = head
| index_167 = select(queue_139,head) ),
inference(paramodulation,[status(thm)],[f4800,f9200]) ).
fof(f9204,plain,
( seq = head
| index_167 = index_138 ),
inference(forward_demodulation,[status(thm)],[f4798,f9202]) ).
fof(f9205,plain,
index_167 = index_138,
inference(forward_subsumption_resolution,[status(thm)],[f9204,f402]) ).
fof(f9231,plain,
index_168 = s(index_138),
inference(backward_demodulation,[status(thm)],[f9205,f581]) ).
fof(f9353,plain,
( select(queue_169,tail) = index_165
| head = tail ),
inference(paramodulation,[status(thm)],[f5033,f5034]) ).
fof(f9354,plain,
! [X0] :
( tail = X0
| select(queue_169,X0) = select(queue_164,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f5032,f5034]) ).
fof(f9358,plain,
( index_171 = index_165
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4425,f9353]) ).
fof(f9359,plain,
index_171 = index_165,
inference(forward_subsumption_resolution,[status(thm)],[f9358,f401]) ).
fof(f9366,plain,
! [X0] :
( select(earray_172,X0) = select(earray_170,X0)
| index_165 = X0 ),
inference(backward_demodulation,[status(thm)],[f9359,f4335]) ).
fof(f9375,plain,
index_174 = s(index_165),
inference(backward_demodulation,[status(thm)],[f9359,f583]) ).
fof(f9727,plain,
( earray_176 = select(queue_173,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4337,f5042]) ).
fof(f9730,plain,
( earray_176 = earray_172
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5041,f9727]) ).
fof(f9731,plain,
earray_176 = earray_172,
inference(forward_subsumption_resolution,[status(thm)],[f9730,f403]) ).
fof(f9746,plain,
( earray_182 = select(queue_179,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4340,f5120]) ).
fof(f9749,plain,
( earray_182 = earray_178
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5119,f9746]) ).
fof(f9750,plain,
earray_182 = earray_178,
inference(forward_subsumption_resolution,[status(thm)],[f9749,f403]) ).
fof(f9769,plain,
( index_188 = select(queue_185,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f589,f5131]) ).
fof(f9772,plain,
index_188 = select(queue_185,head),
inference(forward_subsumption_resolution,[status(thm)],[f9769,f401]) ).
fof(f9774,plain,
( seq = head
| index_188 = select(queue_181,head) ),
inference(paramodulation,[status(thm)],[f5124,f9772]) ).
fof(f9776,plain,
index_188 = select(queue_181,head),
inference(forward_subsumption_resolution,[status(thm)],[f9774,f402]) ).
fof(f9778,plain,
( tail = head
| index_188 = select(queue_179,head) ),
inference(paramodulation,[status(thm)],[f5120,f9776]) ).
fof(f9780,plain,
index_188 = select(queue_179,head),
inference(forward_subsumption_resolution,[status(thm)],[f9778,f401]) ).
fof(f9788,plain,
( seq = head
| index_188 = select(queue_175,head) ),
inference(paramodulation,[status(thm)],[f5118,f9780]) ).
fof(f9790,plain,
index_188 = select(queue_175,head),
inference(forward_subsumption_resolution,[status(thm)],[f9788,f402]) ).
fof(f9799,plain,
( tail = head
| index_188 = select(queue_173,head) ),
inference(paramodulation,[status(thm)],[f5042,f9790]) ).
fof(f9801,plain,
index_188 = select(queue_173,head),
inference(forward_subsumption_resolution,[status(thm)],[f9799,f401]) ).
fof(f9803,plain,
( seq = head
| index_188 = select(queue_169,head) ),
inference(paramodulation,[status(thm)],[f5040,f9801]) ).
fof(f9805,plain,
( seq = head
| index_188 = index_168 ),
inference(forward_demodulation,[status(thm)],[f5035,f9803]) ).
fof(f9806,plain,
index_188 = index_168,
inference(forward_subsumption_resolution,[status(thm)],[f9805,f402]) ).
fof(f9820,plain,
index_189 = s(index_168),
inference(backward_demodulation,[status(thm)],[f9806,f590]) ).
fof(f10064,plain,
( select(queue_190,tail) = index_186
| head = tail ),
inference(paramodulation,[status(thm)],[f5132,f5203]) ).
fof(f10065,plain,
! [X0] :
( tail = X0
| select(queue_190,X0) = select(queue_185,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f5131,f5203]) ).
fof(f10069,plain,
( index_192 = index_186
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4428,f10064]) ).
fof(f10070,plain,
index_192 = index_186,
inference(forward_subsumption_resolution,[status(thm)],[f10069,f401]) ).
fof(f10073,plain,
! [X0] :
( select(earray_193,X0) = select(earray_191,X0)
| index_186 = X0 ),
inference(backward_demodulation,[status(thm)],[f10070,f4344]) ).
fof(f10082,plain,
index_195 = s(index_186),
inference(backward_demodulation,[status(thm)],[f10070,f592]) ).
fof(f10455,plain,
( earray_197 = select(queue_194,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4346,f5281]) ).
fof(f10458,plain,
( earray_197 = earray_193
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5280,f10455]) ).
fof(f10459,plain,
earray_197 = earray_193,
inference(forward_subsumption_resolution,[status(thm)],[f10458,f403]) ).
fof(f10490,plain,
( earray_203 = select(queue_200,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4351,f5292]) ).
fof(f10493,plain,
( earray_203 = earray_199
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5286,f10490]) ).
fof(f10494,plain,
earray_203 = earray_199,
inference(forward_subsumption_resolution,[status(thm)],[f10493,f403]) ).
fof(f10534,plain,
( index_209 = select(queue_206,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f597,f5370]) ).
fof(f10537,plain,
index_209 = select(queue_206,head),
inference(forward_subsumption_resolution,[status(thm)],[f10534,f401]) ).
fof(f10539,plain,
( seq = head
| index_209 = select(queue_202,head) ),
inference(paramodulation,[status(thm)],[f5368,f10537]) ).
fof(f10541,plain,
index_209 = select(queue_202,head),
inference(forward_subsumption_resolution,[status(thm)],[f10539,f402]) ).
fof(f10543,plain,
( tail = head
| index_209 = select(queue_200,head) ),
inference(paramodulation,[status(thm)],[f5292,f10541]) ).
fof(f10545,plain,
index_209 = select(queue_200,head),
inference(forward_subsumption_resolution,[status(thm)],[f10543,f401]) ).
fof(f10574,plain,
( seq = head
| index_209 = select(queue_196,head) ),
inference(paramodulation,[status(thm)],[f5285,f10545]) ).
fof(f10576,plain,
index_209 = select(queue_196,head),
inference(forward_subsumption_resolution,[status(thm)],[f10574,f402]) ).
fof(f10587,plain,
( tail = head
| index_209 = select(queue_194,head) ),
inference(paramodulation,[status(thm)],[f5281,f10576]) ).
fof(f10589,plain,
index_209 = select(queue_194,head),
inference(forward_subsumption_resolution,[status(thm)],[f10587,f401]) ).
fof(f10591,plain,
( seq = head
| index_209 = select(queue_190,head) ),
inference(paramodulation,[status(thm)],[f5279,f10589]) ).
fof(f10593,plain,
( seq = head
| index_209 = index_189 ),
inference(forward_demodulation,[status(thm)],[f5204,f10591]) ).
fof(f10594,plain,
index_209 = index_189,
inference(forward_subsumption_resolution,[status(thm)],[f10593,f402]) ).
fof(f10608,plain,
index_210 = s(index_189),
inference(backward_demodulation,[status(thm)],[f10594,f599]) ).
fof(f10834,plain,
( select(queue_211,tail) = index_207
| head = tail ),
inference(paramodulation,[status(thm)],[f5371,f5442]) ).
fof(f10835,plain,
! [X0] :
( tail = X0
| select(queue_211,X0) = select(queue_206,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f5370,f5442]) ).
fof(f10839,plain,
( index_213 = index_207
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4436,f10834]) ).
fof(f10840,plain,
index_213 = index_207,
inference(forward_subsumption_resolution,[status(thm)],[f10839,f401]) ).
fof(f10843,plain,
! [X0] :
( select(earray_214,X0) = select(earray_212,X0)
| index_207 = X0 ),
inference(backward_demodulation,[status(thm)],[f10840,f4356]) ).
fof(f10852,plain,
index_216 = s(index_207),
inference(backward_demodulation,[status(thm)],[f10840,f601]) ).
fof(f11297,plain,
( earray_218 = select(queue_215,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4353,f5447]) ).
fof(f11300,plain,
( earray_218 = earray_214
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5446,f11297]) ).
fof(f11301,plain,
earray_218 = earray_214,
inference(forward_subsumption_resolution,[status(thm)],[f11300,f403]) ).
fof(f11314,plain,
( earray_224 = select(queue_221,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4358,f5527]) ).
fof(f11317,plain,
( earray_224 = earray_220
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5458,f11314]) ).
fof(f11318,plain,
earray_224 = earray_220,
inference(forward_subsumption_resolution,[status(thm)],[f11317,f403]) ).
fof(f11353,plain,
( index_230 = select(queue_227,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f606,f5607]) ).
fof(f11356,plain,
index_230 = select(queue_227,head),
inference(forward_subsumption_resolution,[status(thm)],[f11353,f401]) ).
fof(f11369,plain,
( seq = head
| index_230 = select(queue_223,head) ),
inference(paramodulation,[status(thm)],[f5531,f11356]) ).
fof(f11371,plain,
index_230 = select(queue_223,head),
inference(forward_subsumption_resolution,[status(thm)],[f11369,f402]) ).
fof(f11373,plain,
( tail = head
| index_230 = select(queue_221,head) ),
inference(paramodulation,[status(thm)],[f5527,f11371]) ).
fof(f11375,plain,
index_230 = select(queue_221,head),
inference(forward_subsumption_resolution,[status(thm)],[f11373,f401]) ).
fof(f11399,plain,
( seq = head
| index_230 = select(queue_217,head) ),
inference(paramodulation,[status(thm)],[f5457,f11375]) ).
fof(f11401,plain,
index_230 = select(queue_217,head),
inference(forward_subsumption_resolution,[status(thm)],[f11399,f402]) ).
fof(f11403,plain,
( tail = head
| index_230 = select(queue_215,head) ),
inference(paramodulation,[status(thm)],[f5447,f11401]) ).
fof(f11405,plain,
index_230 = select(queue_215,head),
inference(forward_subsumption_resolution,[status(thm)],[f11403,f401]) ).
fof(f11407,plain,
( seq = head
| index_230 = select(queue_211,head) ),
inference(paramodulation,[status(thm)],[f5445,f11405]) ).
fof(f11409,plain,
( seq = head
| index_230 = index_210 ),
inference(forward_demodulation,[status(thm)],[f5443,f11407]) ).
fof(f11410,plain,
index_230 = index_210,
inference(forward_subsumption_resolution,[status(thm)],[f11409,f402]) ).
fof(f11424,plain,
index_231 = s(index_210),
inference(backward_demodulation,[status(thm)],[f11410,f607]) ).
fof(f11639,plain,
( select(queue_232,tail) = index_228
| head = tail ),
inference(paramodulation,[status(thm)],[f5608,f5612]) ).
fof(f11640,plain,
! [X0] :
( tail = X0
| select(queue_232,X0) = select(queue_227,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f5607,f5612]) ).
fof(f11644,plain,
( index_240 = index_228
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4440,f11639]) ).
fof(f11645,plain,
index_240 = index_228,
inference(forward_subsumption_resolution,[status(thm)],[f11644,f401]) ).
fof(f11648,plain,
! [X0] :
( select(earray_241,X0) = select(earray_239,X0)
| index_228 = X0 ),
inference(backward_demodulation,[status(thm)],[f11645,f4378]) ).
fof(f11830,plain,
( index_282 = select(queue_242,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f4446,f5706]) ).
fof(f11831,plain,
( earray_281 = select(queue_242,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4374,f5706]) ).
fof(f11835,plain,
index_282 = select(queue_242,head),
inference(forward_subsumption_resolution,[status(thm)],[f11830,f401]) ).
fof(f11836,plain,
( earray_281 = earray_241
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5631,f11831]) ).
fof(f11837,plain,
earray_281 = earray_241,
inference(forward_subsumption_resolution,[status(thm)],[f11836,f403]) ).
fof(f11842,plain,
elem_283 = select(earray_241,index_282),
inference(backward_demodulation,[status(thm)],[f11837,f551]) ).
fof(f11849,plain,
( seq = head
| index_282 = select(queue_232,head) ),
inference(paramodulation,[status(thm)],[f5630,f11835]) ).
fof(f11851,plain,
( seq = head
| index_282 = index_231 ),
inference(forward_demodulation,[status(thm)],[f5613,f11849]) ).
fof(f11852,plain,
index_282 = index_231,
inference(forward_subsumption_resolution,[status(thm)],[f11851,f402]) ).
fof(f11870,plain,
index_282 = s(index_210),
inference(backward_demodulation,[status(thm)],[f11852,f11424]) ).
fof(f11992,plain,
( index_26 = select(queue_23,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f619,f5711]) ).
fof(f11995,plain,
index_26 = select(queue_23,head),
inference(forward_subsumption_resolution,[status(thm)],[f11992,f401]) ).
fof(f11997,plain,
( seq = head
| index_26 = select(queue_19,head) ),
inference(paramodulation,[status(thm)],[f5610,f11995]) ).
fof(f11999,plain,
index_26 = select(queue_19,head),
inference(forward_subsumption_resolution,[status(thm)],[f11997,f402]) ).
fof(f12033,plain,
( tail = head
| index_26 = select(queue_17,head) ),
inference(paramodulation,[status(thm)],[f5200,f11999]) ).
fof(f12035,plain,
index_26 = select(queue_17,head),
inference(forward_subsumption_resolution,[status(thm)],[f12033,f401]) ).
fof(f12052,plain,
( seq = head
| index_26 = select(queue_13,head) ),
inference(paramodulation,[status(thm)],[f5037,f12035]) ).
fof(f12054,plain,
index_26 = select(queue_13,head),
inference(forward_subsumption_resolution,[status(thm)],[f12052,f402]) ).
fof(f12056,plain,
( tail = head
| index_26 = select(queue_11,head) ),
inference(paramodulation,[status(thm)],[f4709,f12054]) ).
fof(f12058,plain,
( tail = head
| index_26 = index_279 ),
inference(forward_demodulation,[status(thm)],[f7474,f12056]) ).
fof(f12059,plain,
index_26 = index_279,
inference(forward_subsumption_resolution,[status(thm)],[f12058,f401]) ).
fof(f12070,plain,
index_26 = s(index_278),
inference(backward_demodulation,[status(thm)],[f12059,f628]) ).
fof(f12320,plain,
( index_257 = select(queue_254,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f617,f5794]) ).
fof(f12323,plain,
index_257 = select(queue_254,head),
inference(forward_subsumption_resolution,[status(thm)],[f12320,f401]) ).
fof(f12325,plain,
( seq = head
| index_257 = select(queue_250,head) ),
inference(paramodulation,[status(thm)],[f5792,f12323]) ).
fof(f12327,plain,
index_257 = select(queue_250,head),
inference(forward_subsumption_resolution,[status(thm)],[f12325,f402]) ).
fof(f12329,plain,
( tail = head
| index_257 = select(queue_248,head) ),
inference(paramodulation,[status(thm)],[f5714,f12327]) ).
fof(f12331,plain,
index_257 = select(queue_248,head),
inference(forward_subsumption_resolution,[status(thm)],[f12329,f401]) ).
fof(f12351,plain,
( seq = head
| index_257 = select(queue_238,head) ),
inference(paramodulation,[status(thm)],[f5709,f12331]) ).
fof(f12353,plain,
index_257 = select(queue_238,head),
inference(forward_subsumption_resolution,[status(thm)],[f12351,f402]) ).
fof(f12355,plain,
( tail = head
| index_257 = select(queue_236,head) ),
inference(paramodulation,[status(thm)],[f5626,f12353]) ).
fof(f12357,plain,
index_257 = select(queue_236,head),
inference(forward_subsumption_resolution,[status(thm)],[f12355,f401]) ).
fof(f12359,plain,
( seq = head
| index_257 = select(queue_160,head) ),
inference(paramodulation,[status(thm)],[f5617,f12357]) ).
fof(f12361,plain,
( seq = head
| index_257 = index_159 ),
inference(forward_demodulation,[status(thm)],[f4961,f12359]) ).
fof(f12362,plain,
index_257 = index_159,
inference(forward_subsumption_resolution,[status(thm)],[f12361,f402]) ).
fof(f12421,plain,
index_258 = s(index_159),
inference(backward_demodulation,[status(thm)],[f12362,f618]) ).
fof(f12597,plain,
( select(queue_259,tail) = index_255
| head = tail ),
inference(paramodulation,[status(thm)],[f5795,f5800]) ).
fof(f12602,plain,
( index_261 = index_255
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4443,f12597]) ).
fof(f12603,plain,
index_261 = index_255,
inference(forward_subsumption_resolution,[status(thm)],[f12602,f401]) ).
fof(f12649,plain,
index_264 = s(index_255),
inference(backward_demodulation,[status(thm)],[f12603,f621]) ).
fof(f13090,plain,
( index_278 = select(queue_275,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f627,f5965]) ).
fof(f13093,plain,
index_278 = select(queue_275,head),
inference(forward_subsumption_resolution,[status(thm)],[f13090,f401]) ).
fof(f13096,plain,
( seq = head
| index_278 = select(queue_271,head) ),
inference(paramodulation,[status(thm)],[f5889,f13093]) ).
fof(f13098,plain,
index_278 = select(queue_271,head),
inference(forward_subsumption_resolution,[status(thm)],[f13096,f402]) ).
fof(f13100,plain,
( tail = head
| index_278 = select(queue_269,head) ),
inference(paramodulation,[status(thm)],[f5885,f13098]) ).
fof(f13102,plain,
index_278 = select(queue_269,head),
inference(forward_subsumption_resolution,[status(thm)],[f13100,f401]) ).
fof(f13106,plain,
( seq = head
| index_278 = select(queue_265,head) ),
inference(paramodulation,[status(thm)],[f5815,f13102]) ).
fof(f13108,plain,
index_278 = select(queue_265,head),
inference(forward_subsumption_resolution,[status(thm)],[f13106,f402]) ).
fof(f13110,plain,
( tail = head
| index_278 = select(queue_263,head) ),
inference(paramodulation,[status(thm)],[f5805,f13108]) ).
fof(f13112,plain,
index_278 = select(queue_263,head),
inference(forward_subsumption_resolution,[status(thm)],[f13110,f401]) ).
fof(f13114,plain,
( seq = head
| index_278 = select(queue_259,head) ),
inference(paramodulation,[status(thm)],[f5803,f13112]) ).
fof(f13116,plain,
( seq = head
| index_278 = index_258 ),
inference(forward_demodulation,[status(thm)],[f5801,f13114]) ).
fof(f13117,plain,
index_278 = index_258,
inference(forward_subsumption_resolution,[status(thm)],[f13116,f402]) ).
fof(f13131,plain,
index_26 = s(index_258),
inference(backward_demodulation,[status(thm)],[f13117,f12070]) ).
fof(f13355,plain,
( select(queue_28,tail) = index_24
| head = tail ),
inference(paramodulation,[status(thm)],[f5712,f5967]) ).
fof(f13361,plain,
( index_30 = index_24
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4448,f13355]) ).
fof(f13362,plain,
index_30 = index_24,
inference(forward_subsumption_resolution,[status(thm)],[f13361,f401]) ).
fof(f13374,plain,
index_33 = s(index_24),
inference(backward_demodulation,[status(thm)],[f13362,f632]) ).
fof(f13730,plain,
( select(queue_280,tail) = index_276
| head = tail ),
inference(paramodulation,[status(thm)],[f5966,f5969]) ).
fof(f13735,plain,
( index_9 = index_276
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4457,f13730]) ).
fof(f13736,plain,
index_9 = index_276,
inference(forward_subsumption_resolution,[status(thm)],[f13735,f401]) ).
fof(f13749,plain,
index_12 = s(index_276),
inference(backward_demodulation,[status(thm)],[f13736,f560]) ).
fof(f14397,plain,
( earray_41 = select(queue_38,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4377,f6063]) ).
fof(f14400,plain,
( earray_41 = earray_37
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f5986,f14397]) ).
fof(f14401,plain,
earray_41 = earray_37,
inference(forward_subsumption_resolution,[status(thm)],[f14400,f403]) ).
fof(f14447,plain,
( index_47 = select(queue_44,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f637,f6069]) ).
fof(f14450,plain,
index_47 = select(queue_44,head),
inference(forward_subsumption_resolution,[status(thm)],[f14447,f401]) ).
fof(f14463,plain,
( seq = head
| index_47 = select(queue_40,head) ),
inference(paramodulation,[status(thm)],[f6067,f14450]) ).
fof(f14465,plain,
index_47 = select(queue_40,head),
inference(forward_subsumption_resolution,[status(thm)],[f14463,f402]) ).
fof(f14467,plain,
( tail = head
| index_47 = select(queue_38,head) ),
inference(paramodulation,[status(thm)],[f6063,f14465]) ).
fof(f14469,plain,
index_47 = select(queue_38,head),
inference(forward_subsumption_resolution,[status(thm)],[f14467,f401]) ).
fof(f14493,plain,
( seq = head
| index_47 = select(queue_34,head) ),
inference(paramodulation,[status(thm)],[f5985,f14469]) ).
fof(f14495,plain,
index_47 = select(queue_34,head),
inference(forward_subsumption_resolution,[status(thm)],[f14493,f402]) ).
fof(f14497,plain,
( tail = head
| index_47 = select(queue_32,head) ),
inference(paramodulation,[status(thm)],[f5981,f14495]) ).
fof(f14499,plain,
index_47 = select(queue_32,head),
inference(forward_subsumption_resolution,[status(thm)],[f14497,f401]) ).
fof(f14501,plain,
( seq = head
| index_47 = select(queue_28,head) ),
inference(paramodulation,[status(thm)],[f5973,f14499]) ).
fof(f14503,plain,
( seq = head
| index_47 = index_27 ),
inference(forward_demodulation,[status(thm)],[f5968,f14501]) ).
fof(f14504,plain,
index_47 = index_27,
inference(forward_subsumption_resolution,[status(thm)],[f14503,f402]) ).
fof(f14518,plain,
index_48 = s(index_27),
inference(backward_demodulation,[status(thm)],[f14504,f638]) ).
fof(f14810,plain,
( select(queue_49,tail) = index_45
| head = tail ),
inference(paramodulation,[status(thm)],[f6070,f6081]) ).
fof(f14811,plain,
! [X0] :
( tail = X0
| select(queue_49,X0) = select(queue_44,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f6069,f6081]) ).
fof(f14815,plain,
( index_51 = index_45
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4451,f14810]) ).
fof(f14816,plain,
index_51 = index_45,
inference(forward_subsumption_resolution,[status(thm)],[f14815,f401]) ).
fof(f14819,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_45 = X0 ),
inference(backward_demodulation,[status(thm)],[f14816,f4411]) ).
fof(f14828,plain,
index_54 = s(index_45),
inference(backward_demodulation,[status(thm)],[f14816,f640]) ).
fof(f14841,plain,
s(s(index_54)) != index_33,
inference(backward_demodulation,[status(thm)],[f14828,f6938]) ).
fof(f14843,plain,
s(index_54) != index_33,
inference(backward_demodulation,[status(thm)],[f14828,f6803]) ).
fof(f14846,plain,
index_54 != index_33,
inference(backward_demodulation,[status(thm)],[f14828,f6768]) ).
fof(f14926,plain,
s(index_60) != index_33,
inference(forward_demodulation,[status(thm)],[f6172,f14841]) ).
fof(f14927,plain,
index_66 != index_33,
inference(forward_demodulation,[status(thm)],[f6180,f14926]) ).
fof(f14930,plain,
index_60 != index_33,
inference(forward_demodulation,[status(thm)],[f6172,f14843]) ).
fof(f15148,plain,
( earray_56 = select(queue_53,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4383,f6162]) ).
fof(f15151,plain,
( earray_56 = earray_52
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f6161,f15148]) ).
fof(f15152,plain,
earray_56 = earray_52,
inference(forward_subsumption_resolution,[status(thm)],[f15151,f403]) ).
fof(f15169,plain,
( earray_62 = select(queue_59,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4384,f6173]) ).
fof(f15172,plain,
( earray_62 = earray_58
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f6167,f15169]) ).
fof(f15173,plain,
earray_62 = earray_58,
inference(forward_subsumption_resolution,[status(thm)],[f15172,f403]) ).
fof(f15198,plain,
( index_68 = select(queue_65,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f646,f6252]) ).
fof(f15201,plain,
index_68 = select(queue_65,head),
inference(forward_subsumption_resolution,[status(thm)],[f15198,f401]) ).
fof(f15207,plain,
( seq = head
| index_68 = select(queue_61,head) ),
inference(paramodulation,[status(thm)],[f6250,f15201]) ).
fof(f15209,plain,
index_68 = select(queue_61,head),
inference(forward_subsumption_resolution,[status(thm)],[f15207,f402]) ).
fof(f15211,plain,
( tail = head
| index_68 = select(queue_59,head) ),
inference(paramodulation,[status(thm)],[f6173,f15209]) ).
fof(f15213,plain,
index_68 = select(queue_59,head),
inference(forward_subsumption_resolution,[status(thm)],[f15211,f401]) ).
fof(f15223,plain,
( seq = head
| index_68 = select(queue_55,head) ),
inference(paramodulation,[status(thm)],[f6166,f15213]) ).
fof(f15225,plain,
index_68 = select(queue_55,head),
inference(forward_subsumption_resolution,[status(thm)],[f15223,f402]) ).
fof(f15227,plain,
( tail = head
| index_68 = select(queue_53,head) ),
inference(paramodulation,[status(thm)],[f6162,f15225]) ).
fof(f15229,plain,
index_68 = select(queue_53,head),
inference(forward_subsumption_resolution,[status(thm)],[f15227,f401]) ).
fof(f15231,plain,
( seq = head
| index_68 = select(queue_49,head) ),
inference(paramodulation,[status(thm)],[f6160,f15229]) ).
fof(f15233,plain,
( seq = head
| index_68 = index_48 ),
inference(forward_demodulation,[status(thm)],[f6082,f15231]) ).
fof(f15234,plain,
index_68 = index_48,
inference(forward_subsumption_resolution,[status(thm)],[f15233,f402]) ).
fof(f15248,plain,
index_69 = s(index_48),
inference(backward_demodulation,[status(thm)],[f15234,f647]) ).
fof(f15421,plain,
( select(queue_70,tail) = index_66
| head = tail ),
inference(paramodulation,[status(thm)],[f6253,f6325]) ).
fof(f15422,plain,
! [X0] :
( tail = X0
| select(queue_70,X0) = select(queue_65,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f6252,f6325]) ).
fof(f15426,plain,
( index_72 = index_66
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4454,f15421]) ).
fof(f15427,plain,
index_72 = index_66,
inference(forward_subsumption_resolution,[status(thm)],[f15426,f401]) ).
fof(f15449,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_66 = X0 ),
inference(backward_demodulation,[status(thm)],[f15427,f4421]) ).
fof(f15458,plain,
index_75 = s(index_66),
inference(backward_demodulation,[status(thm)],[f15427,f649]) ).
fof(f15802,plain,
( earray_83 = select(queue_74,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4394,f6335]) ).
fof(f15805,plain,
( earray_83 = earray_73
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f6329,f15802]) ).
fof(f15806,plain,
earray_83 = earray_73,
inference(forward_subsumption_resolution,[status(thm)],[f15805,f403]) ).
fof(f15820,plain,
! [X0] :
( seq = X0
| select(queue_155,X0) = select(queue_80,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4889,f6414]) ).
fof(f15858,plain,
( earray_89 = select(queue_86,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f4395,f6493]) ).
fof(f15861,plain,
( earray_89 = earray_85
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f6492,f15858]) ).
fof(f15862,plain,
earray_89 = earray_85,
inference(forward_subsumption_resolution,[status(thm)],[f15861,f403]) ).
fof(f15915,plain,
( index_95 = select(queue_92,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f657,f6504]) ).
fof(f15918,plain,
index_95 = select(queue_92,head),
inference(forward_subsumption_resolution,[status(thm)],[f15915,f401]) ).
fof(f15920,plain,
( seq = head
| index_95 = select(queue_88,head) ),
inference(paramodulation,[status(thm)],[f6497,f15918]) ).
fof(f15922,plain,
index_95 = select(queue_88,head),
inference(forward_subsumption_resolution,[status(thm)],[f15920,f402]) ).
fof(f15924,plain,
( tail = head
| index_95 = select(queue_86,head) ),
inference(paramodulation,[status(thm)],[f6493,f15922]) ).
fof(f15926,plain,
index_95 = select(queue_86,head),
inference(forward_subsumption_resolution,[status(thm)],[f15924,f401]) ).
fof(f15963,plain,
( seq = head
| index_95 = select(queue_76,head) ),
inference(paramodulation,[status(thm)],[f6491,f15926]) ).
fof(f15965,plain,
index_95 = select(queue_76,head),
inference(forward_subsumption_resolution,[status(thm)],[f15963,f402]) ).
fof(f15979,plain,
( tail = head
| index_95 = select(queue_74,head) ),
inference(paramodulation,[status(thm)],[f6335,f15965]) ).
fof(f15981,plain,
index_95 = select(queue_74,head),
inference(forward_subsumption_resolution,[status(thm)],[f15979,f401]) ).
fof(f15983,plain,
( seq = head
| index_95 = select(queue_70,head) ),
inference(paramodulation,[status(thm)],[f6328,f15981]) ).
fof(f15985,plain,
( seq = head
| index_95 = index_69 ),
inference(forward_demodulation,[status(thm)],[f6326,f15983]) ).
fof(f15986,plain,
index_95 = index_69,
inference(forward_subsumption_resolution,[status(thm)],[f15985,f402]) ).
fof(f15998,plain,
index_116 = s(index_69),
inference(backward_demodulation,[status(thm)],[f15986,f7521]) ).
fof(f16708,plain,
( select(queue_97,tail) = index_93
| head = tail ),
inference(paramodulation,[status(thm)],[f6505,f6574]) ).
fof(f16709,plain,
! [X0] :
( tail = X0
| select(queue_97,X0) = select(queue_92,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f6504,f6574]) ).
fof(f16713,plain,
( index_99 = index_93
| head = tail ),
inference(forward_demodulation,[status(thm)],[f4459,f16708]) ).
fof(f16714,plain,
index_99 = index_93,
inference(forward_subsumption_resolution,[status(thm)],[f16713,f401]) ).
fof(f16726,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_93 = X0 ),
inference(backward_demodulation,[status(thm)],[f16714,f3972]) ).
fof(f16733,plain,
index_102 = s(index_93),
inference(backward_demodulation,[status(thm)],[f16714,f553]) ).
fof(f18126,plain,
! [X0] :
( select(earray_106,X0) = select(earray_100,X0)
| index_102 = X0 ),
inference(forward_demodulation,[status(thm)],[f7435,f6646]) ).
fof(f18129,plain,
! [X0] :
( select(earray_112,X0) = select(earray_106,X0)
| index_108 = X0 ),
inference(forward_demodulation,[status(thm)],[f7456,f6648]) ).
fof(f18162,plain,
! [X0] :
( select(earray_127,X0) = select(earray_121,X0)
| index_123 = X0 ),
inference(forward_demodulation,[status(thm)],[f8183,f6657]) ).
fof(f18178,plain,
! [X0] :
( select(earray_133,X0) = select(earray_127,X0)
| index_129 = X0 ),
inference(forward_demodulation,[status(thm)],[f8221,f6665]) ).
fof(f18181,plain,
! [X0] :
( select(earray_148,X0) = select(earray_142,X0)
| index_144 = X0 ),
inference(forward_demodulation,[status(thm)],[f8810,f6671]) ).
fof(f18184,plain,
! [X0] :
( select(earray_163,X0) = select(earray_148,X0)
| index_150 = X0 ),
inference(forward_demodulation,[status(thm)],[f8835,f6677]) ).
fof(f18187,plain,
! [X0] :
( select(earray_178,X0) = select(earray_172,X0)
| index_174 = X0 ),
inference(forward_demodulation,[status(thm)],[f9731,f6679]) ).
fof(f18210,plain,
! [X0] :
( select(earray_184,X0) = select(earray_178,X0)
| index_180 = X0 ),
inference(forward_demodulation,[status(thm)],[f9750,f6685]) ).
fof(f18216,plain,
! [X0] :
( select(earray_199,X0) = select(earray_193,X0)
| index_195 = X0 ),
inference(forward_demodulation,[status(thm)],[f10459,f6692]) ).
fof(f18219,plain,
! [X0] :
( select(earray_205,X0) = select(earray_199,X0)
| index_201 = X0 ),
inference(forward_demodulation,[status(thm)],[f10494,f6698]) ).
fof(f18222,plain,
! [X0] :
( select(earray_220,X0) = select(earray_214,X0)
| index_216 = X0 ),
inference(forward_demodulation,[status(thm)],[f11301,f6703]) ).
fof(f18225,plain,
! [X0] :
( select(earray_226,X0) = select(earray_220,X0)
| index_222 = X0 ),
inference(forward_demodulation,[status(thm)],[f11318,f6705]) ).
fof(f18360,plain,
! [X0] :
( select(earray_43,X0) = select(earray_37,X0)
| index_39 = X0 ),
inference(forward_demodulation,[status(thm)],[f14401,f6718]) ).
fof(f18363,plain,
! [X0] :
( select(earray_58,X0) = select(earray_52,X0)
| index_54 = X0 ),
inference(forward_demodulation,[status(thm)],[f15152,f6721]) ).
fof(f18426,plain,
! [X0] :
( select(earray_64,X0) = select(earray_58,X0)
| index_60 = X0 ),
inference(forward_demodulation,[status(thm)],[f15173,f6723]) ).
fof(f18435,plain,
! [X0] :
( select(earray_85,X0) = select(earray_73,X0)
| index_75 = X0 ),
inference(forward_demodulation,[status(thm)],[f15806,f6728]) ).
fof(f18528,plain,
! [X0] :
( select(earray_91,X0) = select(earray_85,X0)
| index_87 = X0 ),
inference(forward_demodulation,[status(thm)],[f15862,f6734]) ).
fof(f19177,plain,
( elem_283 = select(earray_239,index_282)
| index_228 = index_282 ),
inference(paramodulation,[status(thm)],[f11842,f11648]) ).
fof(f19464,plain,
s(s(s(s(index_45)))) != index_36,
inference(forward_demodulation,[status(thm)],[f6080,f3407]) ).
fof(f19465,plain,
s(s(s(index_54))) != index_36,
inference(forward_demodulation,[status(thm)],[f14828,f19464]) ).
fof(f19466,plain,
s(s(index_60)) != index_36,
inference(forward_demodulation,[status(thm)],[f6172,f19465]) ).
fof(f19467,plain,
s(index_66) != index_36,
inference(forward_demodulation,[status(thm)],[f6180,f19466]) ).
fof(f19468,plain,
index_75 != index_36,
inference(forward_demodulation,[status(thm)],[f15458,f19467]) ).
fof(f19469,plain,
index_75 != index_33,
inference(forward_demodulation,[status(thm)],[f5983,f19468]) ).
fof(f20654,plain,
s(s(s(s(s(index_45))))) != index_36,
inference(forward_demodulation,[status(thm)],[f6080,f3365]) ).
fof(f20655,plain,
s(s(s(s(index_54)))) != index_36,
inference(forward_demodulation,[status(thm)],[f14828,f20654]) ).
fof(f20656,plain,
s(s(s(index_60))) != index_36,
inference(forward_demodulation,[status(thm)],[f6172,f20655]) ).
fof(f20657,plain,
s(s(index_66)) != index_36,
inference(forward_demodulation,[status(thm)],[f6180,f20656]) ).
fof(f20658,plain,
s(index_75) != index_36,
inference(forward_demodulation,[status(thm)],[f15458,f20657]) ).
fof(f20659,plain,
index_87 != index_36,
inference(forward_demodulation,[status(thm)],[f6342,f20658]) ).
fof(f20660,plain,
index_87 != index_33,
inference(forward_demodulation,[status(thm)],[f5983,f20659]) ).
fof(f21604,plain,
( tail = seq
| earray_119 = select(queue_113,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4178,f7669]) ).
fof(f21608,plain,
( tail = seq
| earray_119 = earray_112
| head = seq ),
inference(forward_demodulation,[status(thm)],[f4623,f21604]) ).
fof(f21609,plain,
( tail = seq
| earray_119 = earray_112 ),
inference(forward_subsumption_resolution,[status(thm)],[f21608,f402]) ).
fof(f21628,plain,
! [X0] :
( select(earray_121,X0) = select(earray_112,X0)
| index_114 = X0 ),
inference(backward_demodulation,[status(thm)],[f21631,f7707]) ).
fof(f21631,plain,
earray_119 = earray_112,
inference(forward_subsumption_resolution,[status(thm)],[f21609,f403]) ).
fof(f21682,plain,
( tail = seq
| earray_140 = select(queue_134,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4320,f8430]) ).
fof(f21686,plain,
( tail = seq
| earray_140 = earray_133
| head = seq ),
inference(forward_demodulation,[status(thm)],[f4717,f21682]) ).
fof(f21687,plain,
( tail = seq
| earray_140 = earray_133 ),
inference(forward_subsumption_resolution,[status(thm)],[f21686,f402]) ).
fof(f21690,plain,
! [X0] :
( select(earray_142,X0) = select(earray_133,X0)
| index_135 = X0 ),
inference(backward_demodulation,[status(thm)],[f21693,f8438]) ).
fof(f21693,plain,
earray_140 = earray_133,
inference(forward_subsumption_resolution,[status(thm)],[f21687,f403]) ).
fof(f21769,plain,
( tail = seq
| earray_170 = select(queue_164,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4334,f9354]) ).
fof(f21773,plain,
( tail = seq
| earray_170 = earray_163
| head = seq ),
inference(forward_demodulation,[status(thm)],[f5031,f21769]) ).
fof(f21774,plain,
( tail = seq
| earray_170 = earray_163 ),
inference(forward_subsumption_resolution,[status(thm)],[f21773,f402]) ).
fof(f21777,plain,
! [X0] :
( select(earray_172,X0) = select(earray_163,X0)
| index_165 = X0 ),
inference(backward_demodulation,[status(thm)],[f21780,f9366]) ).
fof(f21780,plain,
earray_170 = earray_163,
inference(forward_subsumption_resolution,[status(thm)],[f21774,f403]) ).
fof(f21829,plain,
( tail = seq
| earray_191 = select(queue_185,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4343,f10065]) ).
fof(f21833,plain,
( tail = seq
| earray_191 = earray_184
| head = seq ),
inference(forward_demodulation,[status(thm)],[f5125,f21829]) ).
fof(f21834,plain,
( tail = seq
| earray_191 = earray_184 ),
inference(forward_subsumption_resolution,[status(thm)],[f21833,f402]) ).
fof(f21837,plain,
! [X0] :
( select(earray_193,X0) = select(earray_184,X0)
| index_186 = X0 ),
inference(backward_demodulation,[status(thm)],[f21840,f10073]) ).
fof(f21840,plain,
earray_191 = earray_184,
inference(forward_subsumption_resolution,[status(thm)],[f21834,f403]) ).
fof(f21878,plain,
( tail = seq
| earray_212 = select(queue_206,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4352,f10835]) ).
fof(f21882,plain,
( tail = seq
| earray_212 = earray_205
| head = seq ),
inference(forward_demodulation,[status(thm)],[f5369,f21878]) ).
fof(f21883,plain,
( tail = seq
| earray_212 = earray_205 ),
inference(forward_subsumption_resolution,[status(thm)],[f21882,f402]) ).
fof(f21886,plain,
! [X0] :
( select(earray_214,X0) = select(earray_205,X0)
| index_207 = X0 ),
inference(backward_demodulation,[status(thm)],[f21889,f10843]) ).
fof(f21889,plain,
earray_212 = earray_205,
inference(forward_subsumption_resolution,[status(thm)],[f21883,f403]) ).
fof(f21916,plain,
( tail = seq
| earray_239 = select(queue_227,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4360,f11640]) ).
fof(f21920,plain,
( tail = seq
| earray_239 = earray_226
| head = seq ),
inference(forward_demodulation,[status(thm)],[f5532,f21916]) ).
fof(f21921,plain,
( tail = seq
| earray_239 = earray_226 ),
inference(forward_subsumption_resolution,[status(thm)],[f21920,f402]) ).
fof(f21924,plain,
( elem_283 = select(earray_226,index_282)
| index_228 = index_282 ),
inference(backward_demodulation,[status(thm)],[f21928,f19177]) ).
fof(f21928,plain,
earray_239 = earray_226,
inference(forward_subsumption_resolution,[status(thm)],[f21921,f403]) ).
fof(f22377,plain,
( tail = seq
| earray_50 = select(queue_44,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4382,f14811]) ).
fof(f22381,plain,
( tail = seq
| earray_50 = earray_43
| head = seq ),
inference(forward_demodulation,[status(thm)],[f6068,f22377]) ).
fof(f22382,plain,
( tail = seq
| earray_50 = earray_43 ),
inference(forward_subsumption_resolution,[status(thm)],[f22381,f402]) ).
fof(f22385,plain,
! [X0] :
( select(earray_52,X0) = select(earray_43,X0)
| index_45 = X0 ),
inference(backward_demodulation,[status(thm)],[f22388,f14819]) ).
fof(f22388,plain,
earray_50 = earray_43,
inference(forward_subsumption_resolution,[status(thm)],[f22382,f403]) ).
fof(f22421,plain,
( tail = seq
| earray_71 = select(queue_65,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4385,f15422]) ).
fof(f22425,plain,
( tail = seq
| earray_71 = earray_64
| head = seq ),
inference(forward_demodulation,[status(thm)],[f6251,f22421]) ).
fof(f22426,plain,
( tail = seq
| earray_71 = earray_64 ),
inference(forward_subsumption_resolution,[status(thm)],[f22425,f402]) ).
fof(f22435,plain,
! [X0] :
( select(earray_73,X0) = select(earray_64,X0)
| index_66 = X0 ),
inference(backward_demodulation,[status(thm)],[f22438,f15449]) ).
fof(f22438,plain,
earray_71 = earray_64,
inference(forward_subsumption_resolution,[status(thm)],[f22426,f403]) ).
fof(f22464,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_155,X0) = select(queue_7,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f6412,f15820]) ).
fof(f22467,plain,
! [X0] :
( seq = X0
| select(queue_155,X0) = select(queue_7,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f22464]) ).
fof(f22471,plain,
( tail = seq
| earray_98 = select(queue_92,seq)
| head = seq ),
inference(paramodulation,[status(thm)],[f4398,f16709]) ).
fof(f22477,plain,
( tail = seq
| earray_98 = earray_91
| head = seq ),
inference(forward_demodulation,[status(thm)],[f6498,f22471]) ).
fof(f22478,plain,
( tail = seq
| earray_98 = earray_91 ),
inference(forward_subsumption_resolution,[status(thm)],[f22477,f402]) ).
fof(f22487,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_87 = X0 ),
inference(backward_demodulation,[status(thm)],[f22492,f18528]) ).
fof(f22492,plain,
earray_98 = earray_91,
inference(forward_subsumption_resolution,[status(thm)],[f22478,f403]) ).
fof(f22507,plain,
! [X0] :
( index_75 = X0
| select(earray_98,X0) = select(earray_73,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f18435,f22487]) ).
fof(f22550,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_155,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f6322,f22467]) ).
fof(f22554,plain,
! [X0] :
( seq = X0
| select(queue_155,X0) = select(queue_5,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f22550]) ).
fof(f22563,plain,
! [X0] :
( index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_64,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f22435,f22507]) ).
fof(f22583,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_155,X0) = select(queue_1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f6084,f22554]) ).
fof(f22586,plain,
! [X0] :
( seq = X0
| select(queue_155,X0) = select(queue_1,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f22583]) ).
fof(f22591,plain,
( seq = head
| index_158 = select(queue_1,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f8875,f22586]) ).
fof(f22597,plain,
( seq = head
| index_158 = index_0
| tail = head ),
inference(forward_demodulation,[status(thm)],[f4461,f22591]) ).
fof(f22598,plain,
( seq = head
| index_158 = index_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f22597,f401]) ).
fof(f22614,plain,
index_159 = s(index_0),
inference(backward_demodulation,[status(thm)],[f22615,f577]) ).
fof(f22615,plain,
index_158 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[f22598,f402]) ).
fof(f22616,plain,
index_159 = index_6,
inference(forward_demodulation,[status(thm)],[f7208,f22614]) ).
fof(f22636,plain,
index_81 = s(index_159),
inference(backward_demodulation,[status(thm)],[f22616,f6334]) ).
fof(f22640,plain,
index_81 = index_258,
inference(forward_demodulation,[status(thm)],[f12421,f22636]) ).
fof(f23445,plain,
index_156 = s(index_258),
inference(backward_demodulation,[status(thm)],[f22640,f6422]) ).
fof(f23449,plain,
index_156 = index_26,
inference(forward_demodulation,[status(thm)],[f13131,f23445]) ).
fof(f23481,plain,
index_27 = s(index_156),
inference(backward_demodulation,[status(thm)],[f23449,f623]) ).
fof(f23482,plain,
index_27 = index_237,
inference(forward_demodulation,[status(thm)],[f8896,f23481]) ).
fof(f25311,plain,
index_48 = s(index_237),
inference(backward_demodulation,[status(thm)],[f23482,f14518]) ).
fof(f25318,plain,
index_48 = index_249,
inference(forward_demodulation,[status(thm)],[f5637,f25311]) ).
fof(f25332,plain,
index_69 = s(index_249),
inference(backward_demodulation,[status(thm)],[f25318,f15248]) ).
fof(f25339,plain,
index_69 = index_255,
inference(forward_demodulation,[status(thm)],[f5722,f25332]) ).
fof(f25368,plain,
index_116 = s(index_255),
inference(backward_demodulation,[status(thm)],[f25339,f15998]) ).
fof(f25374,plain,
index_116 = index_264,
inference(forward_demodulation,[status(thm)],[f12649,f25368]) ).
fof(f25412,plain,
index_270 = s(index_116),
inference(backward_demodulation,[status(thm)],[f25374,f5813]) ).
fof(f25416,plain,
index_270 = index_117,
inference(forward_demodulation,[status(thm)],[f559,f25412]) ).
fof(f25884,plain,
index_276 = s(index_117),
inference(backward_demodulation,[status(thm)],[f25416,f5896]) ).
fof(f25888,plain,
index_276 = index_138,
inference(forward_demodulation,[status(thm)],[f8284,f25884]) ).
fof(f25913,plain,
index_12 = s(index_138),
inference(backward_demodulation,[status(thm)],[f25888,f13749]) ).
fof(f25928,plain,
index_12 = index_168,
inference(forward_demodulation,[status(thm)],[f9231,f25913]) ).
fof(f25973,plain,
index_189 = s(index_12),
inference(backward_demodulation,[status(thm)],[f25928,f9820]) ).
fof(f25982,plain,
index_189 = index_18,
inference(forward_demodulation,[status(thm)],[f4722,f25973]) ).
fof(f26006,plain,
index_210 = s(index_18),
inference(backward_demodulation,[status(thm)],[f25982,f10608]) ).
fof(f26014,plain,
index_210 = index_24,
inference(forward_demodulation,[status(thm)],[f5210,f26006]) ).
fof(f27617,plain,
index_33 = s(index_210),
inference(backward_demodulation,[status(thm)],[f26014,f13374]) ).
fof(f27628,plain,
index_33 = index_282,
inference(forward_demodulation,[status(thm)],[f11870,f27617]) ).
fof(f27644,plain,
index_87 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f20660]) ).
fof(f27645,plain,
index_75 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f19469]) ).
fof(f27646,plain,
index_54 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f14846]) ).
fof(f27647,plain,
index_60 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f14930]) ).
fof(f27648,plain,
index_66 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f14927]) ).
fof(f27655,plain,
index_45 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f6087]) ).
fof(f27656,plain,
select(earray_37,index_282) = e13,
inference(backward_demodulation,[status(thm)],[f27628,f5993]) ).
fof(f27657,plain,
index_39 = s(index_282),
inference(backward_demodulation,[status(thm)],[f27628,f5991]) ).
fof(f27658,plain,
index_39 != index_282,
inference(backward_demodulation,[status(thm)],[f27628,f5990]) ).
fof(f27881,plain,
s(s(s(s(s(s(s(index_39))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f462]) ).
fof(f27882,plain,
s(s(s(s(s(s(s(s(index_39)))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f461]) ).
fof(f27883,plain,
s(s(s(s(s(s(s(s(s(index_39))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f460]) ).
fof(f27884,plain,
s(s(s(s(s(s(s(s(s(s(index_39)))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f459]) ).
fof(f27885,plain,
s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f458]) ).
fof(f27886,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f457]) ).
fof(f27887,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f456]) ).
fof(f27888,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f455]) ).
fof(f27889,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f454]) ).
fof(f27890,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f453]) ).
fof(f27891,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f452]) ).
fof(f27892,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f451]) ).
fof(f27893,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f450]) ).
fof(f27894,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f449]) ).
fof(f27895,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f448]) ).
fof(f27896,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f447]) ).
fof(f27897,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f446]) ).
fof(f27898,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f445]) ).
fof(f27899,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f27657,f444]) ).
fof(f29484,plain,
s(s(s(s(s(s(index_45)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27881]) ).
fof(f29485,plain,
s(s(s(s(s(index_54))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29484]) ).
fof(f29486,plain,
s(s(s(s(index_60)))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29485]) ).
fof(f29487,plain,
s(s(s(index_66))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29486]) ).
fof(f29488,plain,
s(s(index_75)) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29487]) ).
fof(f29489,plain,
s(index_87) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29488]) ).
fof(f29490,plain,
index_93 != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29489]) ).
fof(f29491,plain,
s(s(s(s(s(s(s(index_45))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27882]) ).
fof(f29492,plain,
s(s(s(s(s(s(index_54)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29491]) ).
fof(f29493,plain,
s(s(s(s(s(index_60))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29492]) ).
fof(f29494,plain,
s(s(s(s(index_66)))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29493]) ).
fof(f29495,plain,
s(s(s(index_75))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29494]) ).
fof(f29496,plain,
s(s(index_87)) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29495]) ).
fof(f29497,plain,
s(index_93) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29496]) ).
fof(f29498,plain,
index_102 != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29497]) ).
fof(f29499,plain,
s(s(s(s(s(s(s(s(index_45)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27883]) ).
fof(f29500,plain,
s(s(s(s(s(s(s(index_54))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29499]) ).
fof(f29501,plain,
s(s(s(s(s(s(index_60)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29500]) ).
fof(f29502,plain,
s(s(s(s(s(index_66))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29501]) ).
fof(f29503,plain,
s(s(s(s(index_75)))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29502]) ).
fof(f29504,plain,
s(s(s(index_87))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29503]) ).
fof(f29505,plain,
s(s(index_93)) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29504]) ).
fof(f29506,plain,
s(index_102) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29505]) ).
fof(f29507,plain,
index_108 != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29506]) ).
fof(f29508,plain,
s(s(s(s(s(s(s(s(s(index_45))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27884]) ).
fof(f29509,plain,
s(s(s(s(s(s(s(s(index_54)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29508]) ).
fof(f29510,plain,
s(s(s(s(s(s(s(index_60))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29509]) ).
fof(f29511,plain,
s(s(s(s(s(s(index_66)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29510]) ).
fof(f29512,plain,
s(s(s(s(s(index_75))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29511]) ).
fof(f29513,plain,
s(s(s(s(index_87)))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29512]) ).
fof(f29514,plain,
s(s(s(index_93))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29513]) ).
fof(f29515,plain,
s(s(index_102)) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29514]) ).
fof(f29516,plain,
s(index_108) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29515]) ).
fof(f29517,plain,
index_114 != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29516]) ).
fof(f29518,plain,
s(s(s(s(s(s(s(s(s(s(index_45)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27885]) ).
fof(f29519,plain,
s(s(s(s(s(s(s(s(s(index_54))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29518]) ).
fof(f29520,plain,
s(s(s(s(s(s(s(s(index_60)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29519]) ).
fof(f29521,plain,
s(s(s(s(s(s(s(index_66))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29520]) ).
fof(f29522,plain,
s(s(s(s(s(s(index_75)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29521]) ).
fof(f29523,plain,
s(s(s(s(s(index_87))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29522]) ).
fof(f29524,plain,
s(s(s(s(index_93)))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29523]) ).
fof(f29525,plain,
s(s(s(index_102))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29524]) ).
fof(f29526,plain,
s(s(index_108)) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29525]) ).
fof(f29527,plain,
s(index_114) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29526]) ).
fof(f29528,plain,
index_123 != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29527]) ).
fof(f29529,plain,
s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27886]) ).
fof(f29530,plain,
s(s(s(s(s(s(s(s(s(s(index_54)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29529]) ).
fof(f29531,plain,
s(s(s(s(s(s(s(s(s(index_60))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29530]) ).
fof(f29532,plain,
s(s(s(s(s(s(s(s(index_66)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29531]) ).
fof(f29533,plain,
s(s(s(s(s(s(s(index_75))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29532]) ).
fof(f29534,plain,
s(s(s(s(s(s(index_87)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29533]) ).
fof(f29535,plain,
s(s(s(s(s(index_93))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29534]) ).
fof(f29536,plain,
s(s(s(s(index_102)))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29535]) ).
fof(f29537,plain,
s(s(s(index_108))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29536]) ).
fof(f29538,plain,
s(s(index_114)) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29537]) ).
fof(f29539,plain,
s(index_123) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29538]) ).
fof(f29540,plain,
index_129 != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29539]) ).
fof(f29541,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27887]) ).
fof(f29542,plain,
s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29541]) ).
fof(f29543,plain,
s(s(s(s(s(s(s(s(s(s(index_60)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29542]) ).
fof(f29544,plain,
s(s(s(s(s(s(s(s(s(index_66))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29543]) ).
fof(f29545,plain,
s(s(s(s(s(s(s(s(index_75)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29544]) ).
fof(f29546,plain,
s(s(s(s(s(s(s(index_87))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29545]) ).
fof(f29547,plain,
s(s(s(s(s(s(index_93)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29546]) ).
fof(f29548,plain,
s(s(s(s(s(index_102))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29547]) ).
fof(f29549,plain,
s(s(s(s(index_108)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29548]) ).
fof(f29550,plain,
s(s(s(index_114))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29549]) ).
fof(f29551,plain,
s(s(index_123)) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29550]) ).
fof(f29552,plain,
s(index_129) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29551]) ).
fof(f29553,plain,
index_135 != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29552]) ).
fof(f29554,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27888]) ).
fof(f29555,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29554]) ).
fof(f29556,plain,
s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29555]) ).
fof(f29557,plain,
s(s(s(s(s(s(s(s(s(s(index_66)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29556]) ).
fof(f29558,plain,
s(s(s(s(s(s(s(s(s(index_75))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29557]) ).
fof(f29559,plain,
s(s(s(s(s(s(s(s(index_87)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29558]) ).
fof(f29560,plain,
s(s(s(s(s(s(s(index_93))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29559]) ).
fof(f29561,plain,
s(s(s(s(s(s(index_102)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29560]) ).
fof(f29562,plain,
s(s(s(s(s(index_108))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29561]) ).
fof(f29563,plain,
s(s(s(s(index_114)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29562]) ).
fof(f29564,plain,
s(s(s(index_123))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29563]) ).
fof(f29565,plain,
s(s(index_129)) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29564]) ).
fof(f29566,plain,
s(index_135) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29565]) ).
fof(f29567,plain,
index_144 != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29566]) ).
fof(f29568,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27889]) ).
fof(f29569,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29568]) ).
fof(f29570,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29569]) ).
fof(f29571,plain,
s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29570]) ).
fof(f29572,plain,
s(s(s(s(s(s(s(s(s(s(index_75)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29571]) ).
fof(f29573,plain,
s(s(s(s(s(s(s(s(s(index_87))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29572]) ).
fof(f29574,plain,
s(s(s(s(s(s(s(s(index_93)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29573]) ).
fof(f29575,plain,
s(s(s(s(s(s(s(index_102))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29574]) ).
fof(f29576,plain,
s(s(s(s(s(s(index_108)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29575]) ).
fof(f29577,plain,
s(s(s(s(s(index_114))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29576]) ).
fof(f29578,plain,
s(s(s(s(index_123)))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29577]) ).
fof(f29579,plain,
s(s(s(index_129))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29578]) ).
fof(f29580,plain,
s(s(index_135)) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29579]) ).
fof(f29581,plain,
s(index_144) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29580]) ).
fof(f29582,plain,
index_150 != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29581]) ).
fof(f29583,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27890]) ).
fof(f29584,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29583]) ).
fof(f29585,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29584]) ).
fof(f29586,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29585]) ).
fof(f29587,plain,
s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29586]) ).
fof(f29588,plain,
s(s(s(s(s(s(s(s(s(s(index_87)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29587]) ).
fof(f29589,plain,
s(s(s(s(s(s(s(s(s(index_93))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29588]) ).
fof(f29590,plain,
s(s(s(s(s(s(s(s(index_102)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29589]) ).
fof(f29591,plain,
s(s(s(s(s(s(s(index_108))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29590]) ).
fof(f29592,plain,
s(s(s(s(s(s(index_114)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29591]) ).
fof(f29593,plain,
s(s(s(s(s(index_123))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29592]) ).
fof(f29594,plain,
s(s(s(s(index_129)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29593]) ).
fof(f29595,plain,
s(s(s(index_135))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29594]) ).
fof(f29596,plain,
s(s(index_144)) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29595]) ).
fof(f29597,plain,
s(index_150) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29596]) ).
fof(f29598,plain,
index_165 != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29597]) ).
fof(f29599,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27891]) ).
fof(f29600,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29599]) ).
fof(f29601,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29600]) ).
fof(f29602,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29601]) ).
fof(f29603,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29602]) ).
fof(f29604,plain,
s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29603]) ).
fof(f29605,plain,
s(s(s(s(s(s(s(s(s(s(index_93)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29604]) ).
fof(f29606,plain,
s(s(s(s(s(s(s(s(s(index_102))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29605]) ).
fof(f29607,plain,
s(s(s(s(s(s(s(s(index_108)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29606]) ).
fof(f29608,plain,
s(s(s(s(s(s(s(index_114))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29607]) ).
fof(f29609,plain,
s(s(s(s(s(s(index_123)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29608]) ).
fof(f29610,plain,
s(s(s(s(s(index_129))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29609]) ).
fof(f29611,plain,
s(s(s(s(index_135)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29610]) ).
fof(f29612,plain,
s(s(s(index_144))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29611]) ).
fof(f29613,plain,
s(s(index_150)) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29612]) ).
fof(f29614,plain,
s(index_165) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29613]) ).
fof(f29615,plain,
index_174 != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29614]) ).
fof(f29616,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27892]) ).
fof(f29617,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29616]) ).
fof(f29618,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29617]) ).
fof(f29619,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29618]) ).
fof(f29620,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29619]) ).
fof(f29621,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29620]) ).
fof(f29622,plain,
s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29621]) ).
fof(f29623,plain,
s(s(s(s(s(s(s(s(s(s(index_102)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29622]) ).
fof(f29624,plain,
s(s(s(s(s(s(s(s(s(index_108))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29623]) ).
fof(f29625,plain,
s(s(s(s(s(s(s(s(index_114)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29624]) ).
fof(f29626,plain,
s(s(s(s(s(s(s(index_123))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29625]) ).
fof(f29627,plain,
s(s(s(s(s(s(index_129)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29626]) ).
fof(f29628,plain,
s(s(s(s(s(index_135))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29627]) ).
fof(f29629,plain,
s(s(s(s(index_144)))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29628]) ).
fof(f29630,plain,
s(s(s(index_150))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29629]) ).
fof(f29631,plain,
s(s(index_165)) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29630]) ).
fof(f29632,plain,
s(index_174) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29631]) ).
fof(f29633,plain,
index_180 != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29632]) ).
fof(f29634,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27893]) ).
fof(f29635,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29634]) ).
fof(f29636,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29635]) ).
fof(f29637,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29636]) ).
fof(f29638,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29637]) ).
fof(f29639,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29638]) ).
fof(f29640,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29639]) ).
fof(f29641,plain,
s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29640]) ).
fof(f29642,plain,
s(s(s(s(s(s(s(s(s(s(index_108)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29641]) ).
fof(f29643,plain,
s(s(s(s(s(s(s(s(s(index_114))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29642]) ).
fof(f29644,plain,
s(s(s(s(s(s(s(s(index_123)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29643]) ).
fof(f29645,plain,
s(s(s(s(s(s(s(index_129))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29644]) ).
fof(f29646,plain,
s(s(s(s(s(s(index_135)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29645]) ).
fof(f29647,plain,
s(s(s(s(s(index_144))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29646]) ).
fof(f29648,plain,
s(s(s(s(index_150)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29647]) ).
fof(f29649,plain,
s(s(s(index_165))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29648]) ).
fof(f29650,plain,
s(s(index_174)) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29649]) ).
fof(f29651,plain,
s(index_180) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29650]) ).
fof(f29652,plain,
index_186 != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29651]) ).
fof(f29653,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27894]) ).
fof(f29654,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29653]) ).
fof(f29655,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29654]) ).
fof(f29656,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29655]) ).
fof(f29657,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29656]) ).
fof(f29658,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29657]) ).
fof(f29659,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29658]) ).
fof(f29660,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29659]) ).
fof(f29661,plain,
s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29660]) ).
fof(f29662,plain,
s(s(s(s(s(s(s(s(s(s(index_114)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29661]) ).
fof(f29663,plain,
s(s(s(s(s(s(s(s(s(index_123))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29662]) ).
fof(f29664,plain,
s(s(s(s(s(s(s(s(index_129)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29663]) ).
fof(f29665,plain,
s(s(s(s(s(s(s(index_135))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29664]) ).
fof(f29666,plain,
s(s(s(s(s(s(index_144)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29665]) ).
fof(f29667,plain,
s(s(s(s(s(index_150))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29666]) ).
fof(f29668,plain,
s(s(s(s(index_165)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29667]) ).
fof(f29669,plain,
s(s(s(index_174))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29668]) ).
fof(f29670,plain,
s(s(index_180)) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29669]) ).
fof(f29671,plain,
s(index_186) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29670]) ).
fof(f29672,plain,
index_195 != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29671]) ).
fof(f29673,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27895]) ).
fof(f29674,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29673]) ).
fof(f29675,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29674]) ).
fof(f29676,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29675]) ).
fof(f29677,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29676]) ).
fof(f29678,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29677]) ).
fof(f29679,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29678]) ).
fof(f29680,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29679]) ).
fof(f29681,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29680]) ).
fof(f29682,plain,
s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29681]) ).
fof(f29683,plain,
s(s(s(s(s(s(s(s(s(s(index_123)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29682]) ).
fof(f29684,plain,
s(s(s(s(s(s(s(s(s(index_129))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29683]) ).
fof(f29685,plain,
s(s(s(s(s(s(s(s(index_135)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29684]) ).
fof(f29686,plain,
s(s(s(s(s(s(s(index_144))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29685]) ).
fof(f29687,plain,
s(s(s(s(s(s(index_150)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29686]) ).
fof(f29688,plain,
s(s(s(s(s(index_165))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29687]) ).
fof(f29689,plain,
s(s(s(s(index_174)))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29688]) ).
fof(f29690,plain,
s(s(s(index_180))) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29689]) ).
fof(f29691,plain,
s(s(index_186)) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29690]) ).
fof(f29692,plain,
s(index_195) != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29691]) ).
fof(f29693,plain,
index_201 != index_282,
inference(forward_demodulation,[status(thm)],[f5291,f29692]) ).
fof(f29694,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27896]) ).
fof(f29695,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29694]) ).
fof(f29696,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29695]) ).
fof(f29697,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29696]) ).
fof(f29698,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29697]) ).
fof(f29699,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29698]) ).
fof(f29700,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29699]) ).
fof(f29701,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29700]) ).
fof(f29702,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29701]) ).
fof(f29703,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29702]) ).
fof(f29704,plain,
s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29703]) ).
fof(f29705,plain,
s(s(s(s(s(s(s(s(s(s(index_129)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29704]) ).
fof(f29706,plain,
s(s(s(s(s(s(s(s(s(index_135))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29705]) ).
fof(f29707,plain,
s(s(s(s(s(s(s(s(index_144)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29706]) ).
fof(f29708,plain,
s(s(s(s(s(s(s(index_150))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29707]) ).
fof(f29709,plain,
s(s(s(s(s(s(index_165)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29708]) ).
fof(f29710,plain,
s(s(s(s(s(index_174))))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29709]) ).
fof(f29711,plain,
s(s(s(s(index_180)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29710]) ).
fof(f29712,plain,
s(s(s(index_186))) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29711]) ).
fof(f29713,plain,
s(s(index_195)) != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29712]) ).
fof(f29714,plain,
s(index_201) != index_282,
inference(forward_demodulation,[status(thm)],[f5291,f29713]) ).
fof(f29715,plain,
index_207 != index_282,
inference(forward_demodulation,[status(thm)],[f5299,f29714]) ).
fof(f29716,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27897]) ).
fof(f29717,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29716]) ).
fof(f29718,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29717]) ).
fof(f29719,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29718]) ).
fof(f29720,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29719]) ).
fof(f29721,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29720]) ).
fof(f29722,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29721]) ).
fof(f29723,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29722]) ).
fof(f29724,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29723]) ).
fof(f29725,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29724]) ).
fof(f29726,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_123)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29725]) ).
fof(f29727,plain,
s(s(s(s(s(s(s(s(s(s(s(index_129))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29726]) ).
fof(f29728,plain,
s(s(s(s(s(s(s(s(s(s(index_135)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29727]) ).
fof(f29729,plain,
s(s(s(s(s(s(s(s(s(index_144))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29728]) ).
fof(f29730,plain,
s(s(s(s(s(s(s(s(index_150)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29729]) ).
fof(f29731,plain,
s(s(s(s(s(s(s(index_165))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29730]) ).
fof(f29732,plain,
s(s(s(s(s(s(index_174)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29731]) ).
fof(f29733,plain,
s(s(s(s(s(index_180))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29732]) ).
fof(f29734,plain,
s(s(s(s(index_186)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29733]) ).
fof(f29735,plain,
s(s(s(index_195))) != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29734]) ).
fof(f29736,plain,
s(s(index_201)) != index_282,
inference(forward_demodulation,[status(thm)],[f5291,f29735]) ).
fof(f29737,plain,
s(index_207) != index_282,
inference(forward_demodulation,[status(thm)],[f5299,f29736]) ).
fof(f29738,plain,
index_216 != index_282,
inference(forward_demodulation,[status(thm)],[f10852,f29737]) ).
fof(f29739,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27898]) ).
fof(f29740,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29739]) ).
fof(f29741,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29740]) ).
fof(f29742,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29741]) ).
fof(f29743,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29742]) ).
fof(f29744,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29743]) ).
fof(f29745,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29744]) ).
fof(f29746,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29745]) ).
fof(f29747,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29746]) ).
fof(f29748,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29747]) ).
fof(f29749,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29748]) ).
fof(f29750,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_129)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29749]) ).
fof(f29751,plain,
s(s(s(s(s(s(s(s(s(s(s(index_135))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29750]) ).
fof(f29752,plain,
s(s(s(s(s(s(s(s(s(s(index_144)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29751]) ).
fof(f29753,plain,
s(s(s(s(s(s(s(s(s(index_150))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29752]) ).
fof(f29754,plain,
s(s(s(s(s(s(s(s(index_165)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29753]) ).
fof(f29755,plain,
s(s(s(s(s(s(s(index_174))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29754]) ).
fof(f29756,plain,
s(s(s(s(s(s(index_180)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29755]) ).
fof(f29757,plain,
s(s(s(s(s(index_186))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29756]) ).
fof(f29758,plain,
s(s(s(s(index_195)))) != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29757]) ).
fof(f29759,plain,
s(s(s(index_201))) != index_282,
inference(forward_demodulation,[status(thm)],[f5291,f29758]) ).
fof(f29760,plain,
s(s(index_207)) != index_282,
inference(forward_demodulation,[status(thm)],[f5299,f29759]) ).
fof(f29761,plain,
s(index_216) != index_282,
inference(forward_demodulation,[status(thm)],[f10852,f29760]) ).
fof(f29762,plain,
index_222 != index_282,
inference(forward_demodulation,[status(thm)],[f5455,f29761]) ).
fof(f29763,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6080,f27899]) ).
fof(f29764,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f14828,f29763]) ).
fof(f29765,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6172,f29764]) ).
fof(f29766,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6180,f29765]) ).
fof(f29767,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f15458,f29766]) ).
fof(f29768,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6342,f29767]) ).
fof(f29769,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f6503,f29768]) ).
fof(f29770,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f16733,f29769]) ).
fof(f29771,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4472,f29770]) ).
fof(f29772,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4553,f29771]) ).
fof(f29773,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_123)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7716,f29772]) ).
fof(f29774,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_129))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4641,f29773]) ).
fof(f29775,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_135)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4727,f29774]) ).
fof(f29776,plain,
s(s(s(s(s(s(s(s(s(s(s(index_144))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8447,f29775]) ).
fof(f29777,plain,
s(s(s(s(s(s(s(s(s(s(index_150)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4882,f29776]) ).
fof(f29778,plain,
s(s(s(s(s(s(s(s(s(index_165))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4887,f29777]) ).
fof(f29779,plain,
s(s(s(s(s(s(s(s(index_174)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f9375,f29778]) ).
fof(f29780,plain,
s(s(s(s(s(s(s(index_180))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5049,f29779]) ).
fof(f29781,plain,
s(s(s(s(s(s(index_186)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5130,f29780]) ).
fof(f29782,plain,
s(s(s(s(s(index_195))))) != index_282,
inference(forward_demodulation,[status(thm)],[f10082,f29781]) ).
fof(f29783,plain,
s(s(s(s(index_201)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5291,f29782]) ).
fof(f29784,plain,
s(s(s(index_207))) != index_282,
inference(forward_demodulation,[status(thm)],[f5299,f29783]) ).
fof(f29785,plain,
s(s(index_216)) != index_282,
inference(forward_demodulation,[status(thm)],[f10852,f29784]) ).
fof(f29786,plain,
s(index_222) != index_282,
inference(forward_demodulation,[status(thm)],[f5455,f29785]) ).
fof(f29787,plain,
index_228 != index_282,
inference(forward_demodulation,[status(thm)],[f5538,f29786]) ).
fof(f32306,plain,
elem_283 = select(earray_226,index_282),
inference(backward_subsumption_resolution,[status(thm)],[f21924,f29787]) ).
fof(f32338,plain,
( index_222 = index_282
| elem_283 = select(earray_220,index_282) ),
inference(paramodulation,[status(thm)],[f18225,f32306]) ).
fof(f32340,plain,
elem_283 = select(earray_220,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32338,f29762]) ).
fof(f32342,plain,
( index_216 = index_282
| elem_283 = select(earray_214,index_282) ),
inference(paramodulation,[status(thm)],[f18222,f32340]) ).
fof(f32344,plain,
elem_283 = select(earray_214,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32342,f29738]) ).
fof(f32346,plain,
( index_207 = index_282
| elem_283 = select(earray_205,index_282) ),
inference(paramodulation,[status(thm)],[f21886,f32344]) ).
fof(f32348,plain,
elem_283 = select(earray_205,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32346,f29715]) ).
fof(f32350,plain,
( index_201 = index_282
| elem_283 = select(earray_199,index_282) ),
inference(paramodulation,[status(thm)],[f18219,f32348]) ).
fof(f32352,plain,
elem_283 = select(earray_199,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32350,f29693]) ).
fof(f32376,plain,
( index_195 = index_282
| elem_283 = select(earray_193,index_282) ),
inference(paramodulation,[status(thm)],[f18216,f32352]) ).
fof(f32378,plain,
elem_283 = select(earray_193,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32376,f29672]) ).
fof(f32380,plain,
( index_186 = index_282
| elem_283 = select(earray_184,index_282) ),
inference(paramodulation,[status(thm)],[f21837,f32378]) ).
fof(f32382,plain,
elem_283 = select(earray_184,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32380,f29652]) ).
fof(f32384,plain,
( index_180 = index_282
| elem_283 = select(earray_178,index_282) ),
inference(paramodulation,[status(thm)],[f18210,f32382]) ).
fof(f32386,plain,
elem_283 = select(earray_178,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32384,f29633]) ).
fof(f32408,plain,
( index_174 = index_282
| elem_283 = select(earray_172,index_282) ),
inference(paramodulation,[status(thm)],[f18187,f32386]) ).
fof(f32410,plain,
elem_283 = select(earray_172,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32408,f29615]) ).
fof(f32412,plain,
( index_165 = index_282
| elem_283 = select(earray_163,index_282) ),
inference(paramodulation,[status(thm)],[f21777,f32410]) ).
fof(f32414,plain,
elem_283 = select(earray_163,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32412,f29598]) ).
fof(f32416,plain,
( index_150 = index_282
| elem_283 = select(earray_148,index_282) ),
inference(paramodulation,[status(thm)],[f18184,f32414]) ).
fof(f32418,plain,
elem_283 = select(earray_148,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32416,f29582]) ).
fof(f32440,plain,
( index_144 = index_282
| elem_283 = select(earray_142,index_282) ),
inference(paramodulation,[status(thm)],[f18181,f32418]) ).
fof(f32442,plain,
elem_283 = select(earray_142,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32440,f29567]) ).
fof(f32444,plain,
( index_135 = index_282
| elem_283 = select(earray_133,index_282) ),
inference(paramodulation,[status(thm)],[f21690,f32442]) ).
fof(f32446,plain,
elem_283 = select(earray_133,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32444,f29553]) ).
fof(f32448,plain,
( index_129 = index_282
| elem_283 = select(earray_127,index_282) ),
inference(paramodulation,[status(thm)],[f18178,f32446]) ).
fof(f32450,plain,
elem_283 = select(earray_127,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32448,f29540]) ).
fof(f32474,plain,
( index_123 = index_282
| elem_283 = select(earray_121,index_282) ),
inference(paramodulation,[status(thm)],[f18162,f32450]) ).
fof(f32476,plain,
elem_283 = select(earray_121,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32474,f29528]) ).
fof(f32478,plain,
( index_114 = index_282
| elem_283 = select(earray_112,index_282) ),
inference(paramodulation,[status(thm)],[f21628,f32476]) ).
fof(f32480,plain,
elem_283 = select(earray_112,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32478,f29517]) ).
fof(f32482,plain,
( index_108 = index_282
| elem_283 = select(earray_106,index_282) ),
inference(paramodulation,[status(thm)],[f18129,f32480]) ).
fof(f32484,plain,
elem_283 = select(earray_106,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32482,f29507]) ).
fof(f32516,plain,
( index_102 = index_282
| elem_283 = select(earray_100,index_282) ),
inference(paramodulation,[status(thm)],[f18126,f32484]) ).
fof(f32518,plain,
elem_283 = select(earray_100,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f32516,f29498]) ).
fof(f35964,plain,
! [X0] :
( index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_58,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f18426,f22563]) ).
fof(f39247,plain,
! [X0] :
( index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_52,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f18363,f35964]) ).
fof(f40864,plain,
! [X0] :
( index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_43,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f22385,f39247]) ).
fof(f46571,plain,
! [X0] :
( index_39 = X0
| index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_37,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f18360,f40864]) ).
fof(f49431,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| index_75 = index_282
| select(earray_98,index_282) = e13
| index_87 = index_282 ),
inference(paramodulation,[status(thm)],[f27656,f46571]) ).
fof(f49435,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| index_75 = index_282
| select(earray_98,index_282) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f49431,f27644]) ).
fof(f49437,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| select(earray_98,index_282) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f49435,f27645]) ).
fof(f49438,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| select(earray_100,index_282) = e13 ),
inference(paramodulation,[status(thm)],[f16726,f49437]) ).
fof(f49440,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| elem_283 = e13 ),
inference(forward_demodulation,[status(thm)],[f32518,f49438]) ).
fof(f49441,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f49440,f795]) ).
fof(f49450,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f49441,f27648]) ).
fof(f49451,plain,
( index_93 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282 ),
inference(resolution,[status(thm)],[f49450,f27658]) ).
fof(f49480,plain,
( index_93 = index_282
| index_45 = index_282
| index_54 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f49451,f27647]) ).
fof(f49493,plain,
( index_93 = index_282
| index_45 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f49480,f27646]) ).
fof(f49494,plain,
index_93 = index_282,
inference(resolution,[status(thm)],[f49493,f27655]) ).
fof(f49527,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f49494,f29490]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n005.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 09:10:49 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 54.84/7.36 % Refutation found
% 54.84/7.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 54.84/7.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 37.99/8.66 % Elapsed time: 8.082476 seconds
% 37.99/8.66 % CPU time: 50.672410 seconds
% 37.99/8.66 % Total memory used: 558.833 MB
% 37.99/8.66 % Net memory used: 554.361 MB
%------------------------------------------------------------------------------