%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:09 PM UTC 2026
% Result : Unsatisfiable 0.16s 5.68s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 100
% Number of leaves : 249
% Syntax : Number of formulae : 1204 ( 967 unt; 0 def)
% Number of atoms : 1577 (1576 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 382 ( 9 ~; 373 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 295 ( 295 usr; 291 con; 0-3 aty)
% Number of variables : 207 ( 207 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : p(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : s(p(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] : s(s(s(X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
earray_244 = store(earray_242,index_243,e45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
earray_278 = select(q46,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
elem_280 = select(earray_278,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
elem_283 = select(earray_278,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
index_105 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
index_111 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
index_117 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
index_123 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
index_126 = s(index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
index_129 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
index_135 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,hypothesis,
index_141 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
index_147 = select(q30,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,hypothesis,
index_153 = select(q31,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,hypothesis,
index_159 = select(q32,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
index_162 = s(index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_165 = select(q33,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,hypothesis,
index_168 = s(index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,hypothesis,
index_171 = select(q34,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,hypothesis,
index_177 = select(q35,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
index_183 = select(q36,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
index_189 = select(q37,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
index_192 = s(index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
index_195 = select(q38,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
index_198 = s(index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
index_201 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
index_207 = select(q39,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
index_210 = s(index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
index_213 = select(q40,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
index_219 = select(q41,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_225 = select(q42,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_231 = select(q43,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_234 = s(index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_237 = select(q44,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_243 = select(q45,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_249 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_255 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_261 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_267 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_27 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_273 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_279 = select(q46,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_281 = select(q46,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
s(index_282) = index_281,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_33 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_39 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_45 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_51 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_57 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_63 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_69 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_75 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_81 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_87 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_93 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_99 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
queue_101 = store(q23,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
queue_107 = store(q24,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
queue_113 = store(q25,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
queue_119 = store(q26,seq,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
queue_121 = store(queue_119,tail,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
queue_125 = store(q27,seq,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
queue_127 = store(queue_125,tail,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_131 = store(q28,seq,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_133 = store(queue_131,tail,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_137 = store(q2,seq,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_139 = store(queue_137,tail,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_143 = store(q29,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_149 = store(q30,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_155 = store(q31,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_161 = store(q32,seq,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_163 = store(queue_161,tail,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_167 = store(q33,seq,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_169 = store(queue_167,tail,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_173 = store(q34,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_179 = store(q35,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_185 = store(q36,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_191 = store(q37,seq,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_193 = store(queue_191,tail,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_197 = store(q38,seq,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_199 = store(queue_197,tail,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_203 = store(q3,seq,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_205 = store(queue_203,tail,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_209 = store(q39,seq,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_211 = store(queue_209,tail,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_215 = store(q40,seq,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_221 = store(q41,seq,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_227 = store(q42,seq,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_233 = store(q43,seq,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_235 = store(queue_233,tail,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_239 = store(q44,seq,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_241 = store(queue_239,tail,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_245 = store(q45,seq,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_247 = store(queue_245,tail,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_251 = store(q4,seq,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_253 = store(queue_251,tail,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_257 = store(q5,seq,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_259 = store(queue_257,tail,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_263 = store(q6,seq,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_269 = store(q7,seq,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_275 = store(q8,seq,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_29 = store(q12,seq,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_31 = store(queue_29,tail,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_35 = store(q13,seq,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_37 = store(queue_35,tail,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_41 = store(q14,seq,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_43 = store(queue_41,tail,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_47 = store(q15,seq,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_49 = store(queue_47,tail,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_53 = store(q16,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_59 = store(q17,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_65 = store(q18,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
queue_71 = store(q1,seq,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
queue_73 = store(queue_71,tail,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
queue_77 = store(q19,seq,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
queue_79 = store(queue_77,tail,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
queue_83 = store(q20,seq,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
queue_85 = store(queue_83,tail,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
queue_89 = store(q21,seq,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
queue_91 = store(queue_89,tail,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
queue_95 = store(q22,seq,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
queue_97 = store(queue_95,tail,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f327,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f328,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f329,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f330,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f331,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f332,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f333,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f334,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f335,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f336,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f337,hypothesis,
q5 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f338,hypothesis,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f339,hypothesis,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f340,hypothesis,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,hypothesis,
q9 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f342,negated_conjecture,
elem_280 != elem_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f344,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f345,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f346,plain,
head != tail,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f347,plain,
head != seq,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f348,plain,
tail != seq,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f349,plain,
! [X0] : p(s(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f350,plain,
! [X0] : s(p(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f353,plain,
! [X0] : s(s(s(X0))) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f408,plain,
earray_244 = store(earray_242,index_243,e45),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f420,plain,
earray_278 = select(q46,seq),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f447,plain,
elem_280 = select(earray_278,index_279),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f448,plain,
elem_283 = select(earray_278,index_282),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f449,plain,
index_0 = select(q,tail),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f450,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f451,plain,
index_105 = select(q24,tail),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f452,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f453,plain,
index_111 = select(q25,tail),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f454,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f455,plain,
index_117 = select(q26,tail),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f456,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f457,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f458,plain,
index_123 = select(q27,tail),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f459,plain,
index_126 = s(index_123),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f460,plain,
index_129 = select(q28,tail),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f461,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f462,plain,
index_135 = select(q2,tail),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f463,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f464,plain,
index_141 = select(q29,tail),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f465,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f466,plain,
index_147 = select(q30,tail),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f467,plain,
index_15 = select(q10,tail),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f468,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f469,plain,
index_153 = select(q31,tail),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f470,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f471,plain,
index_159 = select(q32,tail),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f472,plain,
index_162 = s(index_159),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f473,plain,
index_165 = select(q33,tail),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f474,plain,
index_168 = s(index_165),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f475,plain,
index_171 = select(q34,tail),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f476,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f477,plain,
index_177 = select(q35,tail),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f478,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f479,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f480,plain,
index_183 = select(q36,tail),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f481,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f482,plain,
index_189 = select(q37,tail),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f483,plain,
index_192 = s(index_189),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f484,plain,
index_195 = select(q38,tail),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f485,plain,
index_198 = s(index_195),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f486,plain,
index_201 = select(q3,tail),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f487,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f488,plain,
index_207 = select(q39,tail),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f489,plain,
index_21 = select(q11,tail),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f490,plain,
index_210 = s(index_207),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f491,plain,
index_213 = select(q40,tail),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f492,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f493,plain,
index_219 = select(q41,tail),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f494,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f495,plain,
index_225 = select(q42,tail),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f496,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f497,plain,
index_231 = select(q43,tail),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f498,plain,
index_234 = s(index_231),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f499,plain,
index_237 = select(q44,tail),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f500,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f501,plain,
index_240 = s(index_237),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f502,plain,
index_243 = select(q45,tail),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f503,plain,
index_246 = s(index_243),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f504,plain,
index_249 = select(q4,tail),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f505,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f506,plain,
index_255 = select(q5,tail),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f507,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f508,plain,
index_261 = select(q6,tail),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f509,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f510,plain,
index_267 = select(q7,tail),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f511,plain,
index_27 = select(q12,tail),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f512,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f513,plain,
index_273 = select(q8,tail),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f514,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f515,plain,
index_279 = select(q46,head),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f516,plain,
index_281 = select(q46,tail),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f517,plain,
s(index_282) = index_281,
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f518,plain,
index_3 = select(q0,tail),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f519,plain,
index_30 = s(index_27),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f520,plain,
index_33 = select(q13,tail),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f521,plain,
index_36 = s(index_33),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f522,plain,
index_39 = select(q14,tail),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f523,plain,
index_42 = s(index_39),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f524,plain,
index_45 = select(q15,tail),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f525,plain,
index_48 = s(index_45),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f526,plain,
index_51 = select(q16,tail),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f527,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f528,plain,
index_57 = select(q17,tail),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f529,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f530,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f531,plain,
index_63 = select(q18,tail),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f532,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f533,plain,
index_69 = select(q1,tail),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f534,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f535,plain,
index_75 = select(q19,tail),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f536,plain,
index_78 = s(index_75),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f537,plain,
index_81 = select(q20,tail),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f538,plain,
index_84 = s(index_81),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f539,plain,
index_87 = select(q21,tail),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f540,plain,
index_9 = select(q9,tail),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f541,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f542,plain,
index_93 = select(q22,tail),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f543,plain,
index_96 = s(index_93),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f544,plain,
index_99 = select(q23,tail),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f545,plain,
queue_1 = store(q,head,index_0),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f546,plain,
queue_101 = store(q23,seq,earray_100),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f547,plain,
queue_103 = store(queue_101,tail,index_102),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f548,plain,
queue_107 = store(q24,seq,earray_106),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f549,plain,
queue_109 = store(queue_107,tail,index_108),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f550,plain,
queue_11 = store(q9,seq,earray_10),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f551,plain,
queue_113 = store(q25,seq,earray_112),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f552,plain,
queue_115 = store(queue_113,tail,index_114),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f553,plain,
queue_119 = store(q26,seq,earray_118),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f554,plain,
queue_121 = store(queue_119,tail,index_120),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f555,plain,
queue_125 = store(q27,seq,earray_124),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f556,plain,
queue_127 = store(queue_125,tail,index_126),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f557,plain,
queue_13 = store(queue_11,tail,index_12),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f558,plain,
queue_131 = store(q28,seq,earray_130),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f559,plain,
queue_133 = store(queue_131,tail,index_132),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f560,plain,
queue_137 = store(q2,seq,earray_136),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f561,plain,
queue_139 = store(queue_137,tail,index_138),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f562,plain,
queue_143 = store(q29,seq,earray_142),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f563,plain,
queue_145 = store(queue_143,tail,index_144),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f564,plain,
queue_149 = store(q30,seq,earray_148),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f565,plain,
queue_151 = store(queue_149,tail,index_150),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f566,plain,
queue_155 = store(q31,seq,earray_154),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f567,plain,
queue_157 = store(queue_155,tail,index_156),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f568,plain,
queue_161 = store(q32,seq,earray_160),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f569,plain,
queue_163 = store(queue_161,tail,index_162),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f570,plain,
queue_167 = store(q33,seq,earray_166),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f571,plain,
queue_169 = store(queue_167,tail,index_168),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f572,plain,
queue_17 = store(q10,seq,earray_16),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f573,plain,
queue_173 = store(q34,seq,earray_172),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f574,plain,
queue_175 = store(queue_173,tail,index_174),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f575,plain,
queue_179 = store(q35,seq,earray_178),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f576,plain,
queue_181 = store(queue_179,tail,index_180),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f577,plain,
queue_185 = store(q36,seq,earray_184),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f578,plain,
queue_187 = store(queue_185,tail,index_186),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f579,plain,
queue_19 = store(queue_17,tail,index_18),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f580,plain,
queue_191 = store(q37,seq,earray_190),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f581,plain,
queue_193 = store(queue_191,tail,index_192),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f582,plain,
queue_197 = store(q38,seq,earray_196),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f583,plain,
queue_199 = store(queue_197,tail,index_198),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f584,plain,
queue_203 = store(q3,seq,earray_202),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f585,plain,
queue_205 = store(queue_203,tail,index_204),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f586,plain,
queue_209 = store(q39,seq,earray_208),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f587,plain,
queue_211 = store(queue_209,tail,index_210),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f588,plain,
queue_215 = store(q40,seq,earray_214),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f589,plain,
queue_217 = store(queue_215,tail,index_216),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f590,plain,
queue_221 = store(q41,seq,earray_220),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f591,plain,
queue_223 = store(queue_221,tail,index_222),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f592,plain,
queue_227 = store(q42,seq,earray_226),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f593,plain,
queue_229 = store(queue_227,tail,index_228),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f594,plain,
queue_23 = store(q11,seq,earray_22),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f595,plain,
queue_233 = store(q43,seq,earray_232),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f596,plain,
queue_235 = store(queue_233,tail,index_234),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f597,plain,
queue_239 = store(q44,seq,earray_238),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f598,plain,
queue_241 = store(queue_239,tail,index_240),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f599,plain,
queue_245 = store(q45,seq,earray_244),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f600,plain,
queue_247 = store(queue_245,tail,index_246),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f601,plain,
queue_25 = store(queue_23,tail,index_24),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f602,plain,
queue_251 = store(q4,seq,earray_250),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f603,plain,
queue_253 = store(queue_251,tail,index_252),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f604,plain,
queue_257 = store(q5,seq,earray_256),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f605,plain,
queue_259 = store(queue_257,tail,index_258),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f606,plain,
queue_263 = store(q6,seq,earray_262),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f607,plain,
queue_265 = store(queue_263,tail,index_264),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f608,plain,
queue_269 = store(q7,seq,earray_268),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f609,plain,
queue_271 = store(queue_269,tail,index_270),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f610,plain,
queue_275 = store(q8,seq,earray_274),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f611,plain,
queue_277 = store(queue_275,tail,index_276),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f612,plain,
queue_29 = store(q12,seq,earray_28),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f613,plain,
queue_31 = store(queue_29,tail,index_30),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f614,plain,
queue_35 = store(q13,seq,earray_34),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f615,plain,
queue_37 = store(queue_35,tail,index_36),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f616,plain,
queue_41 = store(q14,seq,earray_40),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f617,plain,
queue_43 = store(queue_41,tail,index_42),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f618,plain,
queue_47 = store(q15,seq,earray_46),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f619,plain,
queue_49 = store(queue_47,tail,index_48),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f620,plain,
queue_5 = store(q0,seq,earray_4),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f621,plain,
queue_53 = store(q16,seq,earray_52),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f622,plain,
queue_55 = store(queue_53,tail,index_54),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f623,plain,
queue_59 = store(q17,seq,earray_58),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f624,plain,
queue_61 = store(queue_59,tail,index_60),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f625,plain,
queue_65 = store(q18,seq,earray_64),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f626,plain,
queue_67 = store(queue_65,tail,index_66),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f627,plain,
queue_7 = store(queue_5,tail,index_6),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f628,plain,
queue_71 = store(q1,seq,earray_70),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f629,plain,
queue_73 = store(queue_71,tail,index_72),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f630,plain,
queue_77 = store(q19,seq,earray_76),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f631,plain,
queue_79 = store(queue_77,tail,index_78),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f632,plain,
queue_83 = store(q20,seq,earray_82),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f633,plain,
queue_85 = store(queue_83,tail,index_84),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f634,plain,
queue_89 = store(q21,seq,earray_88),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f635,plain,
queue_91 = store(queue_89,tail,index_90),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f636,plain,
queue_95 = store(q22,seq,earray_94),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f637,plain,
queue_97 = store(queue_95,tail,index_96),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f638,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f639,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f640,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f641,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f642,plain,
q12 = queue_25,
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f643,plain,
q13 = queue_31,
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f644,plain,
q14 = queue_37,
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f645,plain,
q15 = queue_43,
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f646,plain,
q16 = queue_49,
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f647,plain,
q17 = queue_55,
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f648,plain,
q18 = queue_61,
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f649,plain,
q19 = queue_67,
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f650,plain,
q2 = queue_73,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f651,plain,
q20 = queue_79,
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f652,plain,
q21 = queue_85,
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f653,plain,
q22 = queue_91,
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f654,plain,
q23 = queue_97,
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f655,plain,
q24 = queue_103,
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f656,plain,
q25 = queue_109,
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f657,plain,
q26 = queue_115,
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f658,plain,
q27 = queue_121,
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f659,plain,
q28 = queue_127,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f660,plain,
q29 = queue_133,
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f661,plain,
q3 = queue_139,
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f662,plain,
q30 = queue_145,
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f663,plain,
q31 = queue_151,
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f664,plain,
q32 = queue_157,
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f665,plain,
q33 = queue_163,
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f666,plain,
q34 = queue_169,
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f667,plain,
q35 = queue_175,
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f668,plain,
q36 = queue_181,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f669,plain,
q37 = queue_187,
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f670,plain,
q38 = queue_193,
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f671,plain,
q39 = queue_199,
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f672,plain,
q4 = queue_205,
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f673,plain,
q40 = queue_211,
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f674,plain,
q41 = queue_217,
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f675,plain,
q42 = queue_223,
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f676,plain,
q43 = queue_229,
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f677,plain,
q44 = queue_235,
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f678,plain,
q45 = queue_241,
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f679,plain,
q46 = queue_247,
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f680,plain,
q5 = queue_253,
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f681,plain,
q6 = queue_259,
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f682,plain,
q7 = queue_265,
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f683,plain,
q8 = queue_271,
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f684,plain,
q9 = queue_277,
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f685,plain,
elem_280 != elem_283,
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f694,plain,
! [X0] : s(s(X0)) = p(X0),
inference(paramodulation,[status(thm)],[f350,f353]) ).
fof(f732,plain,
p(index_102) = index_99,
inference(paramodulation,[status(thm)],[f450,f349]) ).
fof(f736,plain,
p(index_108) = index_105,
inference(paramodulation,[status(thm)],[f452,f349]) ).
fof(f749,plain,
p(index_12) = index_9,
inference(paramodulation,[status(thm)],[f456,f349]) ).
fof(f755,plain,
p(index_120) = index_117,
inference(paramodulation,[status(thm)],[f457,f349]) ).
fof(f759,plain,
p(index_126) = index_123,
inference(paramodulation,[status(thm)],[f459,f349]) ).
fof(f766,plain,
p(index_132) = index_129,
inference(paramodulation,[status(thm)],[f461,f349]) ).
fof(f770,plain,
p(index_138) = index_135,
inference(paramodulation,[status(thm)],[f463,f349]) ).
fof(f774,plain,
p(index_144) = index_141,
inference(paramodulation,[status(thm)],[f465,f349]) ).
fof(f782,plain,
p(index_150) = index_147,
inference(paramodulation,[status(thm)],[f468,f349]) ).
fof(f788,plain,
p(index_156) = index_153,
inference(paramodulation,[status(thm)],[f470,f349]) ).
fof(f792,plain,
p(index_162) = index_159,
inference(paramodulation,[status(thm)],[f472,f349]) ).
fof(f799,plain,
p(index_168) = index_165,
inference(paramodulation,[status(thm)],[f474,f349]) ).
fof(f803,plain,
p(index_174) = index_171,
inference(paramodulation,[status(thm)],[f476,f349]) ).
fof(f807,plain,
p(index_18) = index_15,
inference(paramodulation,[status(thm)],[f478,f349]) ).
fof(f815,plain,
p(index_180) = index_177,
inference(paramodulation,[status(thm)],[f479,f349]) ).
fof(f821,plain,
p(index_186) = index_183,
inference(paramodulation,[status(thm)],[f481,f349]) ).
fof(f825,plain,
p(index_192) = index_189,
inference(paramodulation,[status(thm)],[f483,f349]) ).
fof(f831,plain,
p(index_198) = index_195,
inference(paramodulation,[status(thm)],[f485,f349]) ).
fof(f835,plain,
p(index_204) = index_201,
inference(paramodulation,[status(thm)],[f487,f349]) ).
fof(f839,plain,
p(index_210) = index_207,
inference(paramodulation,[status(thm)],[f490,f349]) ).
fof(f847,plain,
p(index_216) = index_213,
inference(paramodulation,[status(thm)],[f492,f349]) ).
fof(f853,plain,
p(index_222) = index_219,
inference(paramodulation,[status(thm)],[f494,f349]) ).
fof(f857,plain,
p(index_228) = index_225,
inference(paramodulation,[status(thm)],[f496,f349]) ).
fof(f864,plain,
p(index_234) = index_231,
inference(paramodulation,[status(thm)],[f498,f349]) ).
fof(f868,plain,
p(index_24) = index_21,
inference(paramodulation,[status(thm)],[f500,f349]) ).
fof(f872,plain,
p(index_240) = index_237,
inference(paramodulation,[status(thm)],[f501,f349]) ).
fof(f881,plain,
p(index_246) = index_243,
inference(paramodulation,[status(thm)],[f503,f349]) ).
fof(f886,plain,
p(index_252) = index_249,
inference(paramodulation,[status(thm)],[f505,f349]) ).
fof(f897,plain,
p(index_264) = index_261,
inference(paramodulation,[status(thm)],[f509,f349]) ).
fof(f901,plain,
p(index_270) = index_267,
inference(paramodulation,[status(thm)],[f512,f349]) ).
fof(f905,plain,
p(index_276) = index_273,
inference(paramodulation,[status(thm)],[f514,f349]) ).
fof(f914,plain,
p(index_281) = index_282,
inference(paramodulation,[status(thm)],[f517,f349]) ).
fof(f923,plain,
p(index_36) = index_33,
inference(paramodulation,[status(thm)],[f521,f349]) ).
fof(f926,plain,
select(earray_244,index_243) = e45,
inference(paramodulation,[status(thm)],[f408,f343]) ).
fof(f947,plain,
p(index_6) = index_3,
inference(paramodulation,[status(thm)],[f529,f349]) ).
fof(f956,plain,
p(index_66) = index_63,
inference(paramodulation,[status(thm)],[f532,f349]) ).
fof(f963,plain,
p(index_72) = index_69,
inference(paramodulation,[status(thm)],[f534,f349]) ).
fof(f1037,plain,
earray_278 = select(queue_247,seq),
inference(forward_demodulation,[status(thm)],[f679,f420]) ).
fof(f1131,plain,
index_105 = select(queue_103,tail),
inference(forward_demodulation,[status(thm)],[f655,f451]) ).
fof(f1134,plain,
index_111 = select(queue_109,tail),
inference(forward_demodulation,[status(thm)],[f656,f453]) ).
fof(f1139,plain,
index_117 = select(queue_115,tail),
inference(forward_demodulation,[status(thm)],[f657,f455]) ).
fof(f1140,plain,
index_123 = select(queue_121,tail),
inference(forward_demodulation,[status(thm)],[f658,f458]) ).
fof(f1147,plain,
index_129 = select(queue_127,tail),
inference(forward_demodulation,[status(thm)],[f659,f460]) ).
fof(f1148,plain,
index_135 = select(queue_73,tail),
inference(forward_demodulation,[status(thm)],[f650,f462]) ).
fof(f1149,plain,
index_141 = select(queue_133,tail),
inference(forward_demodulation,[status(thm)],[f660,f464]) ).
fof(f1152,plain,
index_147 = select(queue_145,tail),
inference(forward_demodulation,[status(thm)],[f662,f466]) ).
fof(f1157,plain,
index_15 = select(queue_13,tail),
inference(forward_demodulation,[status(thm)],[f640,f467]) ).
fof(f1158,plain,
index_153 = select(queue_151,tail),
inference(forward_demodulation,[status(thm)],[f663,f469]) ).
fof(f1165,plain,
index_159 = select(queue_157,tail),
inference(forward_demodulation,[status(thm)],[f664,f471]) ).
fof(f1166,plain,
index_165 = select(queue_163,tail),
inference(forward_demodulation,[status(thm)],[f665,f473]) ).
fof(f1167,plain,
index_171 = select(queue_169,tail),
inference(forward_demodulation,[status(thm)],[f666,f475]) ).
fof(f1170,plain,
index_177 = select(queue_175,tail),
inference(forward_demodulation,[status(thm)],[f667,f477]) ).
fof(f1175,plain,
index_183 = select(queue_181,tail),
inference(forward_demodulation,[status(thm)],[f668,f480]) ).
fof(f1176,plain,
index_189 = select(queue_187,tail),
inference(forward_demodulation,[status(thm)],[f669,f482]) ).
fof(f1183,plain,
index_195 = select(queue_193,tail),
inference(forward_demodulation,[status(thm)],[f670,f484]) ).
fof(f1184,plain,
index_201 = select(queue_139,tail),
inference(forward_demodulation,[status(thm)],[f661,f486]) ).
fof(f1185,plain,
index_207 = select(queue_199,tail),
inference(forward_demodulation,[status(thm)],[f671,f488]) ).
fof(f1188,plain,
index_21 = select(queue_19,tail),
inference(forward_demodulation,[status(thm)],[f641,f489]) ).
fof(f1191,plain,
index_213 = select(queue_211,tail),
inference(forward_demodulation,[status(thm)],[f673,f491]) ).
fof(f1192,plain,
index_219 = select(queue_217,tail),
inference(forward_demodulation,[status(thm)],[f674,f493]) ).
fof(f1193,plain,
index_225 = select(queue_223,tail),
inference(forward_demodulation,[status(thm)],[f675,f495]) ).
fof(f1194,plain,
index_231 = select(queue_229,tail),
inference(forward_demodulation,[status(thm)],[f676,f497]) ).
fof(f1195,plain,
index_237 = select(queue_235,tail),
inference(forward_demodulation,[status(thm)],[f677,f499]) ).
fof(f1196,plain,
index_243 = select(queue_241,tail),
inference(forward_demodulation,[status(thm)],[f678,f502]) ).
fof(f1197,plain,
index_249 = select(queue_205,tail),
inference(forward_demodulation,[status(thm)],[f672,f504]) ).
fof(f1198,plain,
index_255 = select(queue_253,tail),
inference(forward_demodulation,[status(thm)],[f680,f506]) ).
fof(f1199,plain,
index_261 = select(queue_259,tail),
inference(forward_demodulation,[status(thm)],[f681,f508]) ).
fof(f1200,plain,
index_267 = select(queue_265,tail),
inference(forward_demodulation,[status(thm)],[f682,f510]) ).
fof(f1201,plain,
index_27 = select(queue_25,tail),
inference(forward_demodulation,[status(thm)],[f642,f511]) ).
fof(f1202,plain,
index_273 = select(queue_271,tail),
inference(forward_demodulation,[status(thm)],[f683,f513]) ).
fof(f1203,plain,
index_279 = select(queue_247,head),
inference(forward_demodulation,[status(thm)],[f679,f515]) ).
fof(f1204,plain,
index_281 = select(queue_247,tail),
inference(forward_demodulation,[status(thm)],[f679,f516]) ).
fof(f1205,plain,
index_3 = select(queue_1,tail),
inference(forward_demodulation,[status(thm)],[f638,f518]) ).
fof(f1206,plain,
index_33 = select(queue_31,tail),
inference(forward_demodulation,[status(thm)],[f643,f520]) ).
fof(f1207,plain,
index_39 = select(queue_37,tail),
inference(forward_demodulation,[status(thm)],[f644,f522]) ).
fof(f1208,plain,
index_45 = select(queue_43,tail),
inference(forward_demodulation,[status(thm)],[f645,f524]) ).
fof(f1209,plain,
index_51 = select(queue_49,tail),
inference(forward_demodulation,[status(thm)],[f646,f526]) ).
fof(f1210,plain,
index_57 = select(queue_55,tail),
inference(forward_demodulation,[status(thm)],[f647,f528]) ).
fof(f1211,plain,
index_63 = select(queue_61,tail),
inference(forward_demodulation,[status(thm)],[f648,f531]) ).
fof(f1212,plain,
index_69 = select(queue_7,tail),
inference(forward_demodulation,[status(thm)],[f639,f533]) ).
fof(f1213,plain,
index_75 = select(queue_67,tail),
inference(forward_demodulation,[status(thm)],[f649,f535]) ).
fof(f1214,plain,
index_81 = select(queue_79,tail),
inference(forward_demodulation,[status(thm)],[f651,f537]) ).
fof(f1263,plain,
index_87 = select(queue_85,tail),
inference(forward_demodulation,[status(thm)],[f652,f539]) ).
fof(f1264,plain,
index_9 = select(queue_277,tail),
inference(forward_demodulation,[status(thm)],[f684,f540]) ).
fof(f1265,plain,
index_93 = select(queue_91,tail),
inference(forward_demodulation,[status(thm)],[f653,f542]) ).
fof(f1266,plain,
index_99 = select(queue_97,tail),
inference(forward_demodulation,[status(thm)],[f654,f544]) ).
fof(f1267,plain,
! [X0] :
( select(queue_1,X0) = select(q,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f545,f345]) ).
fof(f1268,plain,
select(queue_1,head) = index_0,
inference(paramodulation,[status(thm)],[f545,f343]) ).
fof(f1325,plain,
queue_101 = store(queue_97,seq,earray_100),
inference(forward_demodulation,[status(thm)],[f654,f546]) ).
fof(f1326,plain,
! [X0] :
( select(queue_101,X0) = select(queue_97,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1325,f345]) ).
fof(f1328,plain,
! [X0] :
( select(queue_103,X0) = select(queue_101,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f547,f345]) ).
fof(f1329,plain,
select(queue_103,tail) = index_102,
inference(paramodulation,[status(thm)],[f547,f343]) ).
fof(f1330,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f1131,f1329]) ).
fof(f1331,plain,
queue_107 = store(queue_103,seq,earray_106),
inference(forward_demodulation,[status(thm)],[f655,f548]) ).
fof(f1332,plain,
! [X0] :
( select(queue_107,X0) = select(queue_103,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1331,f345]) ).
fof(f1337,plain,
p(index_108) = index_102,
inference(backward_demodulation,[status(thm)],[f1330,f736]) ).
fof(f1340,plain,
index_108 = s(index_102),
inference(backward_demodulation,[status(thm)],[f1330,f452]) ).
fof(f1343,plain,
! [X0] :
( select(queue_109,X0) = select(queue_107,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f549,f345]) ).
fof(f1344,plain,
select(queue_109,tail) = index_108,
inference(paramodulation,[status(thm)],[f549,f343]) ).
fof(f1345,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f1134,f1344]) ).
fof(f1351,plain,
index_114 = s(index_108),
inference(backward_demodulation,[status(thm)],[f1345,f454]) ).
fof(f1357,plain,
queue_11 = store(queue_277,seq,earray_10),
inference(forward_demodulation,[status(thm)],[f684,f550]) ).
fof(f1358,plain,
! [X0] :
( select(queue_11,X0) = select(queue_277,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1357,f345]) ).
fof(f1360,plain,
queue_113 = store(queue_109,seq,earray_112),
inference(forward_demodulation,[status(thm)],[f656,f551]) ).
fof(f1361,plain,
! [X0] :
( select(queue_113,X0) = select(queue_109,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1360,f345]) ).
fof(f1364,plain,
s(index_108) = p(index_102),
inference(paramodulation,[status(thm)],[f1340,f694]) ).
fof(f1368,plain,
s(index_108) = index_99,
inference(forward_demodulation,[status(thm)],[f732,f1364]) ).
fof(f1376,plain,
s(index_114) = p(index_108),
inference(paramodulation,[status(thm)],[f1351,f694]) ).
fof(f1380,plain,
s(index_114) = index_102,
inference(forward_demodulation,[status(thm)],[f1337,f1376]) ).
fof(f1382,plain,
! [X0] :
( select(queue_115,X0) = select(queue_113,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f552,f345]) ).
fof(f1383,plain,
select(queue_115,tail) = index_114,
inference(paramodulation,[status(thm)],[f552,f343]) ).
fof(f1384,plain,
index_117 = index_114,
inference(forward_demodulation,[status(thm)],[f1139,f1383]) ).
fof(f1385,plain,
queue_119 = store(queue_115,seq,earray_118),
inference(forward_demodulation,[status(thm)],[f657,f553]) ).
fof(f1386,plain,
! [X0] :
( select(queue_119,X0) = select(queue_115,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1385,f345]) ).
fof(f1388,plain,
! [X0] :
( select(queue_121,X0) = select(queue_119,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f554,f345]) ).
fof(f1389,plain,
select(queue_121,tail) = index_120,
inference(paramodulation,[status(thm)],[f554,f343]) ).
fof(f1390,plain,
index_123 = index_120,
inference(forward_demodulation,[status(thm)],[f1140,f1389]) ).
fof(f1393,plain,
p(index_120) = index_114,
inference(backward_demodulation,[status(thm)],[f1384,f755]) ).
fof(f1401,plain,
p(index_126) = index_120,
inference(backward_demodulation,[status(thm)],[f1390,f759]) ).
fof(f1406,plain,
queue_125 = store(queue_121,seq,earray_124),
inference(forward_demodulation,[status(thm)],[f658,f555]) ).
fof(f1407,plain,
! [X0] :
( select(queue_125,X0) = select(queue_121,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1406,f345]) ).
fof(f1409,plain,
! [X0] :
( select(queue_127,X0) = select(queue_125,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f556,f345]) ).
fof(f1410,plain,
select(queue_127,tail) = index_126,
inference(paramodulation,[status(thm)],[f556,f343]) ).
fof(f1411,plain,
index_129 = index_126,
inference(forward_demodulation,[status(thm)],[f1147,f1410]) ).
fof(f1412,plain,
! [X0] :
( select(queue_13,X0) = select(queue_11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f557,f345]) ).
fof(f1413,plain,
select(queue_13,tail) = index_12,
inference(paramodulation,[status(thm)],[f557,f343]) ).
fof(f1414,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f1157,f1413]) ).
fof(f1417,plain,
p(index_132) = index_126,
inference(backward_demodulation,[status(thm)],[f1411,f766]) ).
fof(f1424,plain,
p(index_18) = index_12,
inference(backward_demodulation,[status(thm)],[f1414,f807]) ).
fof(f1427,plain,
index_18 = s(index_12),
inference(backward_demodulation,[status(thm)],[f1414,f478]) ).
fof(f1432,plain,
index_114 = select(queue_97,tail),
inference(backward_demodulation,[status(thm)],[f1438,f1266]) ).
fof(f1438,plain,
index_114 = index_99,
inference(forward_demodulation,[status(thm)],[f1351,f1368]) ).
fof(f1440,plain,
queue_131 = store(queue_127,seq,earray_130),
inference(forward_demodulation,[status(thm)],[f659,f558]) ).
fof(f1441,plain,
! [X0] :
( select(queue_131,X0) = select(queue_127,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1440,f345]) ).
fof(f1443,plain,
! [X0] :
( select(queue_133,X0) = select(queue_131,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f559,f345]) ).
fof(f1444,plain,
select(queue_133,tail) = index_132,
inference(paramodulation,[status(thm)],[f559,f343]) ).
fof(f1445,plain,
index_141 = index_132,
inference(forward_demodulation,[status(thm)],[f1149,f1444]) ).
fof(f1446,plain,
queue_137 = store(queue_73,seq,earray_136),
inference(forward_demodulation,[status(thm)],[f650,f560]) ).
fof(f1447,plain,
! [X0] :
( select(queue_137,X0) = select(queue_73,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1446,f345]) ).
fof(f1451,plain,
p(index_144) = index_132,
inference(backward_demodulation,[status(thm)],[f1445,f774]) ).
fof(f1456,plain,
! [X0] :
( select(queue_139,X0) = select(queue_137,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f561,f345]) ).
fof(f1457,plain,
select(queue_139,tail) = index_138,
inference(paramodulation,[status(thm)],[f561,f343]) ).
fof(f1458,plain,
index_201 = index_138,
inference(forward_demodulation,[status(thm)],[f1184,f1457]) ).
fof(f1461,plain,
p(index_204) = index_138,
inference(backward_demodulation,[status(thm)],[f1458,f835]) ).
fof(f1465,plain,
index_204 = s(index_138),
inference(backward_demodulation,[status(thm)],[f1458,f487]) ).
fof(f1467,plain,
queue_143 = store(queue_133,seq,earray_142),
inference(forward_demodulation,[status(thm)],[f660,f562]) ).
fof(f1468,plain,
! [X0] :
( select(queue_143,X0) = select(queue_133,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1467,f345]) ).
fof(f1470,plain,
! [X0] :
( select(queue_145,X0) = select(queue_143,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f563,f345]) ).
fof(f1471,plain,
select(queue_145,tail) = index_144,
inference(paramodulation,[status(thm)],[f563,f343]) ).
fof(f1472,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f1152,f1471]) ).
fof(f1475,plain,
p(index_150) = index_144,
inference(backward_demodulation,[status(thm)],[f1472,f782]) ).
fof(f1489,plain,
s(index_114) = index_120,
inference(paramodulation,[status(thm)],[f1393,f350]) ).
fof(f1491,plain,
index_102 = index_120,
inference(forward_demodulation,[status(thm)],[f1380,f1489]) ).
fof(f1498,plain,
queue_149 = store(queue_145,seq,earray_148),
inference(forward_demodulation,[status(thm)],[f662,f564]) ).
fof(f1499,plain,
! [X0] :
( select(queue_149,X0) = select(queue_145,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1498,f345]) ).
fof(f1501,plain,
! [X0] :
( select(queue_151,X0) = select(queue_149,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f565,f345]) ).
fof(f1502,plain,
select(queue_151,tail) = index_150,
inference(paramodulation,[status(thm)],[f565,f343]) ).
fof(f1503,plain,
index_153 = index_150,
inference(forward_demodulation,[status(thm)],[f1158,f1502]) ).
fof(f1504,plain,
queue_155 = store(queue_151,seq,earray_154),
inference(forward_demodulation,[status(thm)],[f663,f566]) ).
fof(f1505,plain,
! [X0] :
( select(queue_155,X0) = select(queue_151,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1504,f345]) ).
fof(f1509,plain,
p(index_156) = index_150,
inference(backward_demodulation,[status(thm)],[f1503,f788]) ).
fof(f1514,plain,
! [X0] :
( select(queue_157,X0) = select(queue_155,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f567,f345]) ).
fof(f1515,plain,
select(queue_157,tail) = index_156,
inference(paramodulation,[status(thm)],[f567,f343]) ).
fof(f1516,plain,
index_159 = index_156,
inference(forward_demodulation,[status(thm)],[f1165,f1515]) ).
fof(f1519,plain,
p(index_162) = index_156,
inference(backward_demodulation,[status(thm)],[f1516,f792]) ).
fof(f1526,plain,
queue_161 = store(queue_157,seq,earray_160),
inference(forward_demodulation,[status(thm)],[f664,f568]) ).
fof(f1527,plain,
! [X0] :
( select(queue_161,X0) = select(queue_157,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1526,f345]) ).
fof(f1529,plain,
! [X0] :
( select(queue_163,X0) = select(queue_161,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f569,f345]) ).
fof(f1530,plain,
select(queue_163,tail) = index_162,
inference(paramodulation,[status(thm)],[f569,f343]) ).
fof(f1531,plain,
index_165 = index_162,
inference(forward_demodulation,[status(thm)],[f1166,f1530]) ).
fof(f1534,plain,
p(index_168) = index_162,
inference(backward_demodulation,[status(thm)],[f1531,f799]) ).
fof(f1541,plain,
p(index_126) = index_102,
inference(forward_demodulation,[status(thm)],[f1491,f1401]) ).
fof(f1544,plain,
s(index_102) = index_126,
inference(paramodulation,[status(thm)],[f1541,f350]) ).
fof(f1545,plain,
index_108 = index_126,
inference(forward_demodulation,[status(thm)],[f1340,f1544]) ).
fof(f1552,plain,
queue_167 = store(queue_163,seq,earray_166),
inference(forward_demodulation,[status(thm)],[f665,f570]) ).
fof(f1553,plain,
! [X0] :
( select(queue_167,X0) = select(queue_163,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1552,f345]) ).
fof(f1555,plain,
! [X0] :
( select(queue_169,X0) = select(queue_167,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f571,f345]) ).
fof(f1556,plain,
select(queue_169,tail) = index_168,
inference(paramodulation,[status(thm)],[f571,f343]) ).
fof(f1557,plain,
index_171 = index_168,
inference(forward_demodulation,[status(thm)],[f1167,f1556]) ).
fof(f1558,plain,
queue_17 = store(queue_13,seq,earray_16),
inference(forward_demodulation,[status(thm)],[f640,f572]) ).
fof(f1559,plain,
! [X0] :
( select(queue_17,X0) = select(queue_13,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1558,f345]) ).
fof(f1561,plain,
queue_173 = store(queue_169,seq,earray_172),
inference(forward_demodulation,[status(thm)],[f666,f573]) ).
fof(f1562,plain,
! [X0] :
( select(queue_173,X0) = select(queue_169,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1561,f345]) ).
fof(f1566,plain,
p(index_174) = index_168,
inference(backward_demodulation,[status(thm)],[f1557,f803]) ).
fof(f1576,plain,
! [X0] :
( select(queue_175,X0) = select(queue_173,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f574,f345]) ).
fof(f1577,plain,
select(queue_175,tail) = index_174,
inference(paramodulation,[status(thm)],[f574,f343]) ).
fof(f1578,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f1170,f1577]) ).
fof(f1579,plain,
queue_179 = store(queue_175,seq,earray_178),
inference(forward_demodulation,[status(thm)],[f667,f575]) ).
fof(f1580,plain,
! [X0] :
( select(queue_179,X0) = select(queue_175,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1579,f345]) ).
fof(f1584,plain,
p(index_180) = index_174,
inference(backward_demodulation,[status(thm)],[f1578,f815]) ).
fof(f1591,plain,
p(index_132) = index_108,
inference(forward_demodulation,[status(thm)],[f1545,f1417]) ).
fof(f1594,plain,
s(index_108) = index_132,
inference(paramodulation,[status(thm)],[f1591,f350]) ).
fof(f1596,plain,
index_114 = index_132,
inference(forward_demodulation,[status(thm)],[f1351,f1594]) ).
fof(f1603,plain,
! [X0] :
( select(queue_181,X0) = select(queue_179,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f576,f345]) ).
fof(f1604,plain,
select(queue_181,tail) = index_180,
inference(paramodulation,[status(thm)],[f576,f343]) ).
fof(f1605,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f1175,f1604]) ).
fof(f1606,plain,
queue_185 = store(queue_181,seq,earray_184),
inference(forward_demodulation,[status(thm)],[f668,f577]) ).
fof(f1607,plain,
! [X0] :
( select(queue_185,X0) = select(queue_181,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1606,f345]) ).
fof(f1609,plain,
! [X0] :
( select(queue_187,X0) = select(queue_185,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f578,f345]) ).
fof(f1610,plain,
select(queue_187,tail) = index_186,
inference(paramodulation,[status(thm)],[f578,f343]) ).
fof(f1611,plain,
index_189 = index_186,
inference(forward_demodulation,[status(thm)],[f1176,f1610]) ).
fof(f1614,plain,
p(index_186) = index_180,
inference(backward_demodulation,[status(thm)],[f1605,f821]) ).
fof(f1619,plain,
! [X0] :
( select(queue_19,X0) = select(queue_17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f579,f345]) ).
fof(f1620,plain,
select(queue_19,tail) = index_18,
inference(paramodulation,[status(thm)],[f579,f343]) ).
fof(f1621,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f1188,f1620]) ).
fof(f1624,plain,
p(index_192) = index_186,
inference(backward_demodulation,[status(thm)],[f1611,f825]) ).
fof(f1631,plain,
p(index_24) = index_18,
inference(backward_demodulation,[status(thm)],[f1621,f868]) ).
fof(f1635,plain,
index_24 = s(index_18),
inference(backward_demodulation,[status(thm)],[f1621,f500]) ).
fof(f1636,plain,
queue_191 = store(queue_187,seq,earray_190),
inference(forward_demodulation,[status(thm)],[f669,f580]) ).
fof(f1637,plain,
! [X0] :
( select(queue_191,X0) = select(queue_187,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1636,f345]) ).
fof(f1639,plain,
! [X0] :
( select(queue_193,X0) = select(queue_191,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f581,f345]) ).
fof(f1640,plain,
select(queue_193,tail) = index_192,
inference(paramodulation,[status(thm)],[f581,f343]) ).
fof(f1641,plain,
index_195 = index_192,
inference(forward_demodulation,[status(thm)],[f1183,f1640]) ).
fof(f1644,plain,
p(index_198) = index_192,
inference(backward_demodulation,[status(thm)],[f1641,f831]) ).
fof(f1658,plain,
queue_197 = store(queue_193,seq,earray_196),
inference(forward_demodulation,[status(thm)],[f670,f582]) ).
fof(f1659,plain,
! [X0] :
( select(queue_197,X0) = select(queue_193,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1658,f345]) ).
fof(f1661,plain,
! [X0] :
( select(queue_199,X0) = select(queue_197,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f583,f345]) ).
fof(f1662,plain,
select(queue_199,tail) = index_198,
inference(paramodulation,[status(thm)],[f583,f343]) ).
fof(f1663,plain,
index_207 = index_198,
inference(forward_demodulation,[status(thm)],[f1185,f1662]) ).
fof(f1664,plain,
queue_203 = store(queue_139,seq,earray_202),
inference(forward_demodulation,[status(thm)],[f661,f584]) ).
fof(f1665,plain,
! [X0] :
( select(queue_203,X0) = select(queue_139,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1664,f345]) ).
fof(f1669,plain,
p(index_210) = index_198,
inference(backward_demodulation,[status(thm)],[f1663,f839]) ).
fof(f1674,plain,
! [X0] :
( select(queue_205,X0) = select(queue_203,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f585,f345]) ).
fof(f1675,plain,
select(queue_205,tail) = index_204,
inference(paramodulation,[status(thm)],[f585,f343]) ).
fof(f1676,plain,
index_249 = index_204,
inference(forward_demodulation,[status(thm)],[f1197,f1675]) ).
fof(f1679,plain,
p(index_252) = index_204,
inference(backward_demodulation,[status(thm)],[f1676,f886]) ).
fof(f1683,plain,
index_252 = s(index_204),
inference(backward_demodulation,[status(thm)],[f1676,f505]) ).
fof(f1685,plain,
s(index_18) = p(index_12),
inference(paramodulation,[status(thm)],[f1427,f694]) ).
fof(f1689,plain,
s(index_18) = index_9,
inference(forward_demodulation,[status(thm)],[f749,f1685]) ).
fof(f1691,plain,
queue_209 = store(queue_199,seq,earray_208),
inference(forward_demodulation,[status(thm)],[f671,f586]) ).
fof(f1692,plain,
! [X0] :
( select(queue_209,X0) = select(queue_199,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1691,f345]) ).
fof(f1694,plain,
! [X0] :
( select(queue_211,X0) = select(queue_209,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f587,f345]) ).
fof(f1695,plain,
select(queue_211,tail) = index_210,
inference(paramodulation,[status(thm)],[f587,f343]) ).
fof(f1696,plain,
index_213 = index_210,
inference(forward_demodulation,[status(thm)],[f1191,f1695]) ).
fof(f1699,plain,
p(index_216) = index_210,
inference(backward_demodulation,[status(thm)],[f1696,f847]) ).
fof(f1710,plain,
p(index_144) = index_114,
inference(forward_demodulation,[status(thm)],[f1596,f1451]) ).
fof(f1713,plain,
s(index_114) = index_144,
inference(paramodulation,[status(thm)],[f1710,f350]) ).
fof(f1715,plain,
index_102 = index_144,
inference(forward_demodulation,[status(thm)],[f1380,f1713]) ).
fof(f1716,plain,
queue_215 = store(queue_211,seq,earray_214),
inference(forward_demodulation,[status(thm)],[f673,f588]) ).
fof(f1717,plain,
! [X0] :
( select(queue_215,X0) = select(queue_211,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1716,f345]) ).
fof(f1719,plain,
! [X0] :
( select(queue_217,X0) = select(queue_215,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f589,f345]) ).
fof(f1720,plain,
select(queue_217,tail) = index_216,
inference(paramodulation,[status(thm)],[f589,f343]) ).
fof(f1721,plain,
index_219 = index_216,
inference(forward_demodulation,[status(thm)],[f1192,f1720]) ).
fof(f1722,plain,
queue_221 = store(queue_217,seq,earray_220),
inference(forward_demodulation,[status(thm)],[f674,f590]) ).
fof(f1723,plain,
! [X0] :
( select(queue_221,X0) = select(queue_217,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1722,f345]) ).
fof(f1733,plain,
p(index_222) = index_216,
inference(backward_demodulation,[status(thm)],[f1721,f853]) ).
fof(f1738,plain,
! [X0] :
( select(queue_223,X0) = select(queue_221,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f591,f345]) ).
fof(f1739,plain,
select(queue_223,tail) = index_222,
inference(paramodulation,[status(thm)],[f591,f343]) ).
fof(f1740,plain,
index_225 = index_222,
inference(forward_demodulation,[status(thm)],[f1193,f1739]) ).
fof(f1743,plain,
p(index_228) = index_222,
inference(backward_demodulation,[status(thm)],[f1740,f857]) ).
fof(f1748,plain,
queue_227 = store(queue_223,seq,earray_226),
inference(forward_demodulation,[status(thm)],[f675,f592]) ).
fof(f1749,plain,
! [X0] :
( select(queue_227,X0) = select(queue_223,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1748,f345]) ).
fof(f1751,plain,
! [X0] :
( select(queue_229,X0) = select(queue_227,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f593,f345]) ).
fof(f1752,plain,
select(queue_229,tail) = index_228,
inference(paramodulation,[status(thm)],[f593,f343]) ).
fof(f1753,plain,
index_231 = index_228,
inference(forward_demodulation,[status(thm)],[f1194,f1752]) ).
fof(f1756,plain,
p(index_234) = index_228,
inference(backward_demodulation,[status(thm)],[f1753,f864]) ).
fof(f1770,plain,
queue_23 = store(queue_19,seq,earray_22),
inference(forward_demodulation,[status(thm)],[f641,f594]) ).
fof(f1771,plain,
! [X0] :
( select(queue_23,X0) = select(queue_19,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1770,f345]) ).
fof(f1773,plain,
queue_233 = store(queue_229,seq,earray_232),
inference(forward_demodulation,[status(thm)],[f676,f595]) ).
fof(f1774,plain,
! [X0] :
( select(queue_233,X0) = select(queue_229,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1773,f345]) ).
fof(f1776,plain,
! [X0] :
( select(queue_235,X0) = select(queue_233,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f596,f345]) ).
fof(f1777,plain,
select(queue_235,tail) = index_234,
inference(paramodulation,[status(thm)],[f596,f343]) ).
fof(f1778,plain,
index_237 = index_234,
inference(forward_demodulation,[status(thm)],[f1195,f1777]) ).
fof(f1781,plain,
p(index_240) = index_234,
inference(backward_demodulation,[status(thm)],[f1778,f872]) ).
fof(f1786,plain,
queue_239 = store(queue_235,seq,earray_238),
inference(forward_demodulation,[status(thm)],[f677,f597]) ).
fof(f1787,plain,
! [X0] :
( select(queue_239,X0) = select(queue_235,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1786,f345]) ).
fof(f1790,plain,
s(index_204) = p(index_138),
inference(paramodulation,[status(thm)],[f1465,f694]) ).
fof(f1794,plain,
s(index_204) = index_135,
inference(forward_demodulation,[status(thm)],[f770,f1790]) ).
fof(f1798,plain,
p(index_150) = index_102,
inference(forward_demodulation,[status(thm)],[f1715,f1475]) ).
fof(f1801,plain,
s(index_102) = index_150,
inference(paramodulation,[status(thm)],[f1798,f350]) ).
fof(f1803,plain,
index_108 = index_150,
inference(forward_demodulation,[status(thm)],[f1340,f1801]) ).
fof(f1804,plain,
! [X0] :
( select(queue_241,X0) = select(queue_239,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f598,f345]) ).
fof(f1805,plain,
select(queue_241,tail) = index_240,
inference(paramodulation,[status(thm)],[f598,f343]) ).
fof(f1806,plain,
index_243 = index_240,
inference(forward_demodulation,[status(thm)],[f1196,f1805]) ).
fof(f1807,plain,
queue_245 = store(queue_241,seq,earray_244),
inference(forward_demodulation,[status(thm)],[f678,f599]) ).
fof(f1808,plain,
! [X0] :
( select(queue_245,X0) = select(queue_241,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1807,f345]) ).
fof(f1809,plain,
select(queue_245,seq) = earray_244,
inference(paramodulation,[status(thm)],[f1807,f343]) ).
fof(f1818,plain,
p(index_246) = index_240,
inference(backward_demodulation,[status(thm)],[f1806,f881]) ).
fof(f1826,plain,
! [X0] :
( select(queue_247,X0) = select(queue_245,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f600,f345]) ).
fof(f1827,plain,
select(queue_247,tail) = index_246,
inference(paramodulation,[status(thm)],[f600,f343]) ).
fof(f1828,plain,
index_281 = index_246,
inference(forward_demodulation,[status(thm)],[f1204,f1827]) ).
fof(f1829,plain,
! [X0] :
( select(queue_25,X0) = select(queue_23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f601,f345]) ).
fof(f1830,plain,
select(queue_25,tail) = index_24,
inference(paramodulation,[status(thm)],[f601,f343]) ).
fof(f1831,plain,
index_27 = index_24,
inference(forward_demodulation,[status(thm)],[f1201,f1830]) ).
fof(f1832,plain,
queue_251 = store(queue_205,seq,earray_250),
inference(forward_demodulation,[status(thm)],[f672,f602]) ).
fof(f1833,plain,
! [X0] :
( select(queue_251,X0) = select(queue_205,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1832,f345]) ).
fof(f1837,plain,
p(index_246) = index_282,
inference(backward_demodulation,[status(thm)],[f1828,f914]) ).
fof(f1847,plain,
index_30 = s(index_24),
inference(backward_demodulation,[status(thm)],[f1831,f519]) ).
fof(f1848,plain,
! [X0] :
( select(queue_253,X0) = select(queue_251,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f603,f345]) ).
fof(f1849,plain,
select(queue_253,tail) = index_252,
inference(paramodulation,[status(thm)],[f603,f343]) ).
fof(f1850,plain,
index_255 = index_252,
inference(forward_demodulation,[status(thm)],[f1198,f1849]) ).
fof(f1857,plain,
index_258 = s(index_252),
inference(backward_demodulation,[status(thm)],[f1850,f507]) ).
fof(f1858,plain,
queue_257 = store(queue_253,seq,earray_256),
inference(forward_demodulation,[status(thm)],[f680,f604]) ).
fof(f1859,plain,
! [X0] :
( select(queue_257,X0) = select(queue_253,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1858,f345]) ).
fof(f1861,plain,
! [X0] :
( select(queue_259,X0) = select(queue_257,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f605,f345]) ).
fof(f1862,plain,
select(queue_259,tail) = index_258,
inference(paramodulation,[status(thm)],[f605,f343]) ).
fof(f1863,plain,
index_261 = index_258,
inference(forward_demodulation,[status(thm)],[f1199,f1862]) ).
fof(f1866,plain,
p(index_264) = index_258,
inference(backward_demodulation,[status(thm)],[f1863,f897]) ).
fof(f1870,plain,
index_264 = s(index_258),
inference(backward_demodulation,[status(thm)],[f1863,f509]) ).
fof(f1875,plain,
queue_263 = store(queue_259,seq,earray_262),
inference(forward_demodulation,[status(thm)],[f681,f606]) ).
fof(f1876,plain,
! [X0] :
( select(queue_263,X0) = select(queue_259,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1875,f345]) ).
fof(f1878,plain,
! [X0] :
( select(queue_265,X0) = select(queue_263,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f607,f345]) ).
fof(f1879,plain,
select(queue_265,tail) = index_264,
inference(paramodulation,[status(thm)],[f607,f343]) ).
fof(f1880,plain,
index_267 = index_264,
inference(forward_demodulation,[status(thm)],[f1200,f1879]) ).
fof(f1881,plain,
queue_269 = store(queue_265,seq,earray_268),
inference(forward_demodulation,[status(thm)],[f682,f608]) ).
fof(f1882,plain,
! [X0] :
( select(queue_269,X0) = select(queue_265,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1881,f345]) ).
fof(f1886,plain,
p(index_270) = index_264,
inference(backward_demodulation,[status(thm)],[f1880,f901]) ).
fof(f1890,plain,
index_270 = s(index_264),
inference(backward_demodulation,[status(thm)],[f1880,f512]) ).
fof(f1891,plain,
! [X0] :
( select(queue_271,X0) = select(queue_269,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f609,f345]) ).
fof(f1892,plain,
select(queue_271,tail) = index_270,
inference(paramodulation,[status(thm)],[f609,f343]) ).
fof(f1893,plain,
index_273 = index_270,
inference(forward_demodulation,[status(thm)],[f1202,f1892]) ).
fof(f1896,plain,
p(index_276) = index_270,
inference(backward_demodulation,[status(thm)],[f1893,f905]) ).
fof(f1901,plain,
p(index_156) = index_108,
inference(forward_demodulation,[status(thm)],[f1803,f1509]) ).
fof(f1904,plain,
s(index_108) = index_156,
inference(paramodulation,[status(thm)],[f1901,f350]) ).
fof(f1906,plain,
index_114 = index_156,
inference(forward_demodulation,[status(thm)],[f1351,f1904]) ).
fof(f1913,plain,
queue_275 = store(queue_271,seq,earray_274),
inference(forward_demodulation,[status(thm)],[f683,f610]) ).
fof(f1914,plain,
! [X0] :
( select(queue_275,X0) = select(queue_271,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1913,f345]) ).
fof(f1916,plain,
! [X0] :
( select(queue_277,X0) = select(queue_275,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f611,f345]) ).
fof(f1917,plain,
select(queue_277,tail) = index_276,
inference(paramodulation,[status(thm)],[f611,f343]) ).
fof(f1918,plain,
index_9 = index_276,
inference(forward_demodulation,[status(thm)],[f1264,f1917]) ).
fof(f1923,plain,
p(index_12) = index_276,
inference(backward_demodulation,[status(thm)],[f1918,f749]) ).
fof(f1925,plain,
index_12 = s(index_276),
inference(backward_demodulation,[status(thm)],[f1918,f456]) ).
fof(f1930,plain,
queue_29 = store(queue_25,seq,earray_28),
inference(forward_demodulation,[status(thm)],[f642,f612]) ).
fof(f1931,plain,
! [X0] :
( select(queue_29,X0) = select(queue_25,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1930,f345]) ).
fof(f1933,plain,
! [X0] :
( select(queue_31,X0) = select(queue_29,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f613,f345]) ).
fof(f1934,plain,
select(queue_31,tail) = index_30,
inference(paramodulation,[status(thm)],[f613,f343]) ).
fof(f1935,plain,
index_33 = index_30,
inference(forward_demodulation,[status(thm)],[f1206,f1934]) ).
fof(f1936,plain,
queue_35 = store(queue_31,seq,earray_34),
inference(forward_demodulation,[status(thm)],[f643,f614]) ).
fof(f1937,plain,
! [X0] :
( select(queue_35,X0) = select(queue_31,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1936,f345]) ).
fof(f1941,plain,
p(index_36) = index_30,
inference(backward_demodulation,[status(thm)],[f1935,f923]) ).
fof(f1946,plain,
! [X0] :
( select(queue_37,X0) = select(queue_35,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f615,f345]) ).
fof(f1947,plain,
select(queue_37,tail) = index_36,
inference(paramodulation,[status(thm)],[f615,f343]) ).
fof(f1948,plain,
index_39 = index_36,
inference(forward_demodulation,[status(thm)],[f1207,f1947]) ).
fof(f1955,plain,
index_42 = s(index_36),
inference(backward_demodulation,[status(thm)],[f1948,f523]) ).
fof(f1960,plain,
queue_41 = store(queue_37,seq,earray_40),
inference(forward_demodulation,[status(thm)],[f644,f616]) ).
fof(f1961,plain,
! [X0] :
( select(queue_41,X0) = select(queue_37,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1960,f345]) ).
fof(f1963,plain,
! [X0] :
( select(queue_43,X0) = select(queue_41,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f617,f345]) ).
fof(f1964,plain,
select(queue_43,tail) = index_42,
inference(paramodulation,[status(thm)],[f617,f343]) ).
fof(f1965,plain,
index_45 = index_42,
inference(forward_demodulation,[status(thm)],[f1208,f1964]) ).
fof(f1972,plain,
index_48 = s(index_42),
inference(backward_demodulation,[status(thm)],[f1965,f525]) ).
fof(f1973,plain,
p(index_162) = index_114,
inference(forward_demodulation,[status(thm)],[f1906,f1519]) ).
fof(f1976,plain,
s(index_114) = index_162,
inference(paramodulation,[status(thm)],[f1973,f350]) ).
fof(f1978,plain,
index_102 = index_162,
inference(forward_demodulation,[status(thm)],[f1380,f1976]) ).
fof(f1985,plain,
queue_47 = store(queue_43,seq,earray_46),
inference(forward_demodulation,[status(thm)],[f645,f618]) ).
fof(f1986,plain,
! [X0] :
( select(queue_47,X0) = select(queue_43,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1985,f345]) ).
fof(f1988,plain,
! [X0] :
( select(queue_49,X0) = select(queue_47,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f619,f345]) ).
fof(f1989,plain,
select(queue_49,tail) = index_48,
inference(paramodulation,[status(thm)],[f619,f343]) ).
fof(f1990,plain,
index_51 = index_48,
inference(forward_demodulation,[status(thm)],[f1209,f1989]) ).
fof(f1991,plain,
queue_5 = store(queue_1,seq,earray_4),
inference(forward_demodulation,[status(thm)],[f638,f620]) ).
fof(f1992,plain,
! [X0] :
( select(queue_5,X0) = select(queue_1,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f1991,f345]) ).
fof(f2000,plain,
index_54 = s(index_48),
inference(backward_demodulation,[status(thm)],[f1990,f527]) ).
fof(f2001,plain,
queue_53 = store(queue_49,seq,earray_52),
inference(forward_demodulation,[status(thm)],[f646,f621]) ).
fof(f2002,plain,
! [X0] :
( select(queue_53,X0) = select(queue_49,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2001,f345]) ).
fof(f2011,plain,
p(index_168) = index_102,
inference(forward_demodulation,[status(thm)],[f1978,f1534]) ).
fof(f2014,plain,
s(index_102) = index_168,
inference(paramodulation,[status(thm)],[f2011,f350]) ).
fof(f2016,plain,
index_108 = index_168,
inference(forward_demodulation,[status(thm)],[f1340,f2014]) ).
fof(f2017,plain,
! [X0] :
( select(queue_55,X0) = select(queue_53,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f622,f345]) ).
fof(f2018,plain,
select(queue_55,tail) = index_54,
inference(paramodulation,[status(thm)],[f622,f343]) ).
fof(f2019,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f1210,f2018]) ).
fof(f2020,plain,
queue_59 = store(queue_55,seq,earray_58),
inference(forward_demodulation,[status(thm)],[f647,f623]) ).
fof(f2021,plain,
! [X0] :
( select(queue_59,X0) = select(queue_55,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2020,f345]) ).
fof(f2035,plain,
index_60 = s(index_54),
inference(backward_demodulation,[status(thm)],[f2019,f530]) ).
fof(f2039,plain,
! [X0] :
( select(queue_61,X0) = select(queue_59,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f624,f345]) ).
fof(f2040,plain,
select(queue_61,tail) = index_60,
inference(paramodulation,[status(thm)],[f624,f343]) ).
fof(f2041,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f1211,f2040]) ).
fof(f2042,plain,
queue_65 = store(queue_61,seq,earray_64),
inference(forward_demodulation,[status(thm)],[f648,f625]) ).
fof(f2043,plain,
! [X0] :
( select(queue_65,X0) = select(queue_61,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2042,f345]) ).
fof(f2045,plain,
! [X0] :
( select(queue_67,X0) = select(queue_65,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f626,f345]) ).
fof(f2046,plain,
select(queue_67,tail) = index_66,
inference(paramodulation,[status(thm)],[f626,f343]) ).
fof(f2047,plain,
index_75 = index_66,
inference(forward_demodulation,[status(thm)],[f1213,f2046]) ).
fof(f2050,plain,
p(index_66) = index_60,
inference(backward_demodulation,[status(thm)],[f2041,f956]) ).
fof(f2061,plain,
index_78 = s(index_66),
inference(backward_demodulation,[status(thm)],[f2047,f536]) ).
fof(f2062,plain,
! [X0] :
( select(queue_7,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f627,f345]) ).
fof(f2063,plain,
select(queue_7,tail) = index_6,
inference(paramodulation,[status(thm)],[f627,f343]) ).
fof(f2064,plain,
index_69 = index_6,
inference(forward_demodulation,[status(thm)],[f1212,f2063]) ).
fof(f2067,plain,
p(index_72) = index_6,
inference(backward_demodulation,[status(thm)],[f2064,f963]) ).
fof(f2073,plain,
queue_71 = store(queue_7,seq,earray_70),
inference(forward_demodulation,[status(thm)],[f639,f628]) ).
fof(f2074,plain,
! [X0] :
( select(queue_71,X0) = select(queue_7,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2073,f345]) ).
fof(f2076,plain,
! [X0] :
( select(queue_73,X0) = select(queue_71,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f629,f345]) ).
fof(f2077,plain,
select(queue_73,tail) = index_72,
inference(paramodulation,[status(thm)],[f629,f343]) ).
fof(f2078,plain,
index_135 = index_72,
inference(forward_demodulation,[status(thm)],[f1148,f2077]) ).
fof(f2082,plain,
p(index_138) = index_72,
inference(backward_demodulation,[status(thm)],[f2078,f770]) ).
fof(f2089,plain,
queue_77 = store(queue_67,seq,earray_76),
inference(forward_demodulation,[status(thm)],[f649,f630]) ).
fof(f2090,plain,
! [X0] :
( select(queue_77,X0) = select(queue_67,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2089,f345]) ).
fof(f2092,plain,
! [X0] :
( select(queue_79,X0) = select(queue_77,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f631,f345]) ).
fof(f2093,plain,
select(queue_79,tail) = index_78,
inference(paramodulation,[status(thm)],[f631,f343]) ).
fof(f2094,plain,
index_81 = index_78,
inference(forward_demodulation,[status(thm)],[f1214,f2093]) ).
fof(f2095,plain,
queue_83 = store(queue_79,seq,earray_82),
inference(forward_demodulation,[status(thm)],[f651,f632]) ).
fof(f2096,plain,
! [X0] :
( select(queue_83,X0) = select(queue_79,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2095,f345]) ).
fof(f2104,plain,
index_84 = s(index_78),
inference(backward_demodulation,[status(thm)],[f2094,f538]) ).
fof(f2105,plain,
! [X0] :
( select(queue_85,X0) = select(queue_83,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f633,f345]) ).
fof(f2106,plain,
select(queue_85,tail) = index_84,
inference(paramodulation,[status(thm)],[f633,f343]) ).
fof(f2107,plain,
index_87 = index_84,
inference(forward_demodulation,[status(thm)],[f1263,f2106]) ).
fof(f2114,plain,
index_90 = s(index_84),
inference(backward_demodulation,[status(thm)],[f2107,f541]) ).
fof(f2117,plain,
p(index_174) = index_108,
inference(forward_demodulation,[status(thm)],[f2016,f1566]) ).
fof(f2120,plain,
s(index_108) = index_174,
inference(paramodulation,[status(thm)],[f2117,f350]) ).
fof(f2122,plain,
index_114 = index_174,
inference(forward_demodulation,[status(thm)],[f1351,f2120]) ).
fof(f2123,plain,
queue_89 = store(queue_85,seq,earray_88),
inference(forward_demodulation,[status(thm)],[f652,f634]) ).
fof(f2124,plain,
! [X0] :
( select(queue_89,X0) = select(queue_85,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2123,f345]) ).
fof(f2126,plain,
! [X0] :
( select(queue_91,X0) = select(queue_89,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f635,f345]) ).
fof(f2127,plain,
select(queue_91,tail) = index_90,
inference(paramodulation,[status(thm)],[f635,f343]) ).
fof(f2128,plain,
index_93 = index_90,
inference(forward_demodulation,[status(thm)],[f1265,f2127]) ).
fof(f2141,plain,
index_96 = s(index_90),
inference(backward_demodulation,[status(thm)],[f2128,f543]) ).
fof(f2145,plain,
queue_95 = store(queue_91,seq,earray_94),
inference(forward_demodulation,[status(thm)],[f653,f636]) ).
fof(f2146,plain,
! [X0] :
( select(queue_95,X0) = select(queue_91,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f2145,f345]) ).
fof(f2148,plain,
! [X0] :
( select(queue_97,X0) = select(queue_95,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f637,f345]) ).
fof(f2156,plain,
p(index_180) = index_114,
inference(forward_demodulation,[status(thm)],[f2122,f1584]) ).
fof(f2159,plain,
s(index_114) = index_180,
inference(paramodulation,[status(thm)],[f2156,f350]) ).
fof(f2161,plain,
index_102 = index_180,
inference(forward_demodulation,[status(thm)],[f1380,f2159]) ).
fof(f2177,plain,
p(index_186) = index_102,
inference(forward_demodulation,[status(thm)],[f2161,f1614]) ).
fof(f2180,plain,
s(index_102) = index_186,
inference(paramodulation,[status(thm)],[f2177,f350]) ).
fof(f2182,plain,
index_108 = index_186,
inference(forward_demodulation,[status(thm)],[f1340,f2180]) ).
fof(f2202,plain,
p(index_192) = index_108,
inference(forward_demodulation,[status(thm)],[f2182,f1624]) ).
fof(f2205,plain,
s(index_108) = index_192,
inference(paramodulation,[status(thm)],[f2202,f350]) ).
fof(f2207,plain,
index_114 = index_192,
inference(forward_demodulation,[status(thm)],[f1351,f2205]) ).
fof(f2231,plain,
s(index_24) = p(index_18),
inference(paramodulation,[status(thm)],[f1635,f694]) ).
fof(f2235,plain,
s(index_24) = index_12,
inference(forward_demodulation,[status(thm)],[f1424,f2231]) ).
fof(f2241,plain,
p(index_198) = index_114,
inference(forward_demodulation,[status(thm)],[f2207,f1644]) ).
fof(f2244,plain,
s(index_114) = index_198,
inference(paramodulation,[status(thm)],[f2241,f350]) ).
fof(f2246,plain,
index_102 = index_198,
inference(forward_demodulation,[status(thm)],[f1380,f2244]) ).
fof(f2264,plain,
p(index_210) = index_102,
inference(forward_demodulation,[status(thm)],[f2246,f1669]) ).
fof(f2267,plain,
s(index_102) = index_210,
inference(paramodulation,[status(thm)],[f2264,f350]) ).
fof(f2269,plain,
index_108 = index_210,
inference(forward_demodulation,[status(thm)],[f1340,f2267]) ).
fof(f2302,plain,
index_24 = index_9,
inference(forward_demodulation,[status(thm)],[f1635,f1689]) ).
fof(f2308,plain,
index_24 = index_276,
inference(forward_demodulation,[status(thm)],[f1918,f2302]) ).
fof(f2318,plain,
p(index_216) = index_108,
inference(forward_demodulation,[status(thm)],[f2269,f1699]) ).
fof(f2321,plain,
s(index_108) = index_216,
inference(paramodulation,[status(thm)],[f2318,f350]) ).
fof(f2323,plain,
index_114 = index_216,
inference(forward_demodulation,[status(thm)],[f1351,f2321]) ).
fof(f2343,plain,
p(index_222) = index_114,
inference(forward_demodulation,[status(thm)],[f2323,f1733]) ).
fof(f2346,plain,
s(index_114) = index_222,
inference(paramodulation,[status(thm)],[f2343,f350]) ).
fof(f2348,plain,
index_102 = index_222,
inference(forward_demodulation,[status(thm)],[f1380,f2346]) ).
fof(f2370,plain,
p(index_228) = index_102,
inference(forward_demodulation,[status(thm)],[f2348,f1743]) ).
fof(f2373,plain,
s(index_102) = index_228,
inference(paramodulation,[status(thm)],[f2370,f350]) ).
fof(f2375,plain,
index_108 = index_228,
inference(forward_demodulation,[status(thm)],[f1340,f2373]) ).
fof(f2392,plain,
p(index_234) = index_108,
inference(forward_demodulation,[status(thm)],[f2375,f1756]) ).
fof(f2395,plain,
s(index_108) = index_234,
inference(paramodulation,[status(thm)],[f2392,f350]) ).
fof(f2397,plain,
index_114 = index_234,
inference(forward_demodulation,[status(thm)],[f1351,f2395]) ).
fof(f2421,plain,
p(index_240) = index_114,
inference(forward_demodulation,[status(thm)],[f2397,f1781]) ).
fof(f2424,plain,
s(index_114) = index_240,
inference(paramodulation,[status(thm)],[f2421,f350]) ).
fof(f2426,plain,
index_102 = index_240,
inference(forward_demodulation,[status(thm)],[f1380,f2424]) ).
fof(f2431,plain,
index_243 = index_102,
inference(backward_demodulation,[status(thm)],[f2426,f1806]) ).
fof(f2445,plain,
index_252 = index_135,
inference(forward_demodulation,[status(thm)],[f1683,f1794]) ).
fof(f2452,plain,
index_252 = index_72,
inference(forward_demodulation,[status(thm)],[f2078,f2445]) ).
fof(f2455,plain,
p(index_246) = index_102,
inference(forward_demodulation,[status(thm)],[f2426,f1818]) ).
fof(f2458,plain,
s(index_102) = index_246,
inference(paramodulation,[status(thm)],[f2455,f350]) ).
fof(f2460,plain,
index_108 = index_246,
inference(forward_demodulation,[status(thm)],[f1340,f2458]) ).
fof(f2482,plain,
p(index_108) = index_282,
inference(forward_demodulation,[status(thm)],[f2460,f1837]) ).
fof(f2486,plain,
index_243 = index_282,
inference(backward_demodulation,[status(thm)],[f2519,f2431]) ).
fof(f2512,plain,
s(index_114) = index_282,
inference(backward_demodulation,[status(thm)],[f2519,f1380]) ).
fof(f2519,plain,
index_102 = index_282,
inference(forward_demodulation,[status(thm)],[f1337,f2482]) ).
fof(f2579,plain,
s(index_258) = index_264,
inference(paramodulation,[status(thm)],[f1866,f350]) ).
fof(f2596,plain,
s(index_270) = p(index_264),
inference(paramodulation,[status(thm)],[f1890,f694]) ).
fof(f2600,plain,
s(index_270) = index_258,
inference(forward_demodulation,[status(thm)],[f1866,f2596]) ).
fof(f2606,plain,
p(index_24) = index_270,
inference(forward_demodulation,[status(thm)],[f2308,f1896]) ).
fof(f2609,plain,
p(index_18) = index_264,
inference(backward_demodulation,[status(thm)],[f2615,f1886]) ).
fof(f2615,plain,
index_18 = index_270,
inference(forward_demodulation,[status(thm)],[f1631,f2606]) ).
fof(f2617,plain,
index_12 = index_264,
inference(forward_demodulation,[status(thm)],[f1424,f2609]) ).
fof(f2620,plain,
index_12 = s(index_258),
inference(backward_demodulation,[status(thm)],[f2617,f1870]) ).
fof(f2641,plain,
p(index_12) = index_24,
inference(forward_demodulation,[status(thm)],[f2308,f1923]) ).
fof(f2650,plain,
index_12 = s(index_24),
inference(forward_demodulation,[status(thm)],[f2308,f1925]) ).
fof(f2659,plain,
index_12 = index_30,
inference(forward_demodulation,[status(thm)],[f1847,f2650]) ).
fof(f2666,plain,
p(index_36) = index_12,
inference(forward_demodulation,[status(thm)],[f2659,f1941]) ).
fof(f2669,plain,
s(index_12) = index_36,
inference(paramodulation,[status(thm)],[f2666,f350]) ).
fof(f2671,plain,
index_18 = index_36,
inference(forward_demodulation,[status(thm)],[f1427,f2669]) ).
fof(f2699,plain,
index_42 = s(index_18),
inference(forward_demodulation,[status(thm)],[f2671,f1955]) ).
fof(f2706,plain,
index_42 = index_24,
inference(forward_demodulation,[status(thm)],[f1635,f2699]) ).
fof(f2721,plain,
index_48 = s(index_24),
inference(forward_demodulation,[status(thm)],[f2706,f1972]) ).
fof(f2763,plain,
s(index_60) = index_66,
inference(paramodulation,[status(thm)],[f2050,f350]) ).
fof(f2786,plain,
p(index_252) = index_6,
inference(forward_demodulation,[status(thm)],[f2452,f2067]) ).
fof(f2791,plain,
p(index_204) = index_3,
inference(backward_demodulation,[status(thm)],[f2795,f947]) ).
fof(f2795,plain,
index_204 = index_6,
inference(forward_demodulation,[status(thm)],[f1679,f2786]) ).
fof(f2796,plain,
index_138 = index_3,
inference(forward_demodulation,[status(thm)],[f1461,f2791]) ).
fof(f2801,plain,
index_138 = select(queue_1,tail),
inference(backward_demodulation,[status(thm)],[f2796,f1205]) ).
fof(f2817,plain,
p(index_138) = index_252,
inference(forward_demodulation,[status(thm)],[f2452,f2082]) ).
fof(f2820,plain,
s(index_252) = index_138,
inference(paramodulation,[status(thm)],[f2817,f350]) ).
fof(f2822,plain,
index_258 = index_138,
inference(forward_demodulation,[status(thm)],[f1857,f2820]) ).
fof(f2891,plain,
index_54 = s(index_12),
inference(backward_demodulation,[status(thm)],[f2900,f2000]) ).
fof(f2900,plain,
index_48 = index_12,
inference(forward_demodulation,[status(thm)],[f2721,f2235]) ).
fof(f2901,plain,
index_54 = index_18,
inference(forward_demodulation,[status(thm)],[f1427,f2891]) ).
fof(f2908,plain,
index_60 = s(index_18),
inference(backward_demodulation,[status(thm)],[f2901,f2035]) ).
fof(f2914,plain,
index_60 = index_24,
inference(forward_demodulation,[status(thm)],[f1635,f2908]) ).
fof(f2976,plain,
s(index_138) = index_264,
inference(forward_demodulation,[status(thm)],[f2822,f2579]) ).
fof(f2977,plain,
index_204 = index_264,
inference(forward_demodulation,[status(thm)],[f1465,f2976]) ).
fof(f2987,plain,
p(index_12) = index_138,
inference(backward_demodulation,[status(thm)],[f2992,f1461]) ).
fof(f2992,plain,
index_204 = index_12,
inference(forward_demodulation,[status(thm)],[f2617,f2977]) ).
fof(f2994,plain,
index_24 = index_138,
inference(forward_demodulation,[status(thm)],[f2641,f2987]) ).
fof(f3016,plain,
index_60 = index_138,
inference(backward_demodulation,[status(thm)],[f2994,f2914]) ).
fof(f3048,plain,
s(index_18) = index_258,
inference(forward_demodulation,[status(thm)],[f2615,f2600]) ).
fof(f3049,plain,
s(index_18) = index_138,
inference(forward_demodulation,[status(thm)],[f2822,f3048]) ).
fof(f3061,plain,
index_12 = s(index_138),
inference(forward_demodulation,[status(thm)],[f2822,f2620]) ).
fof(f3085,plain,
s(index_138) = index_66,
inference(forward_demodulation,[status(thm)],[f3016,f2763]) ).
fof(f3091,plain,
index_78 = s(index_12),
inference(backward_demodulation,[status(thm)],[f3096,f2061]) ).
fof(f3096,plain,
index_12 = index_66,
inference(forward_demodulation,[status(thm)],[f3061,f3085]) ).
fof(f3097,plain,
index_78 = index_18,
inference(forward_demodulation,[status(thm)],[f1427,f3091]) ).
fof(f3100,plain,
index_84 = s(index_18),
inference(backward_demodulation,[status(thm)],[f3097,f2104]) ).
fof(f3107,plain,
index_84 = index_138,
inference(forward_demodulation,[status(thm)],[f3049,f3100]) ).
fof(f3117,plain,
index_90 = s(index_138),
inference(backward_demodulation,[status(thm)],[f3107,f2114]) ).
fof(f3124,plain,
index_90 = index_12,
inference(forward_demodulation,[status(thm)],[f3061,f3117]) ).
fof(f3133,plain,
index_96 = s(index_12),
inference(backward_demodulation,[status(thm)],[f3124,f2141]) ).
fof(f3139,plain,
index_96 = index_18,
inference(forward_demodulation,[status(thm)],[f1427,f3133]) ).
fof(f3142,plain,
queue_97 = store(queue_95,tail,index_18),
inference(backward_demodulation,[status(thm)],[f3139,f637]) ).
fof(f3382,plain,
select(queue_97,tail) = index_18,
inference(paramodulation,[status(thm)],[f3142,f343]) ).
fof(f3383,plain,
index_114 = index_18,
inference(forward_demodulation,[status(thm)],[f1432,f3382]) ).
fof(f3407,plain,
s(index_114) = index_138,
inference(backward_demodulation,[status(thm)],[f3383,f3049]) ).
fof(f3430,plain,
index_282 = index_138,
inference(forward_demodulation,[status(thm)],[f2512,f3407]) ).
fof(f3454,plain,
index_282 = select(queue_1,tail),
inference(backward_demodulation,[status(thm)],[f3430,f2801]) ).
fof(f3553,plain,
select(earray_244,index_282) = e45,
inference(forward_demodulation,[status(thm)],[f2486,f926]) ).
fof(f3978,plain,
( index_282 = select(q,tail)
| head = tail ),
inference(paramodulation,[status(thm)],[f3454,f1267]) ).
fof(f3984,plain,
( index_282 = index_0
| head = tail ),
inference(forward_demodulation,[status(thm)],[f449,f3978]) ).
fof(f3985,plain,
index_282 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[f3984,f346]) ).
fof(f3990,plain,
select(queue_1,head) = index_282,
inference(backward_demodulation,[status(thm)],[f3985,f1268]) ).
fof(f4475,plain,
( index_279 = select(queue_245,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f1203,f1826]) ).
fof(f4476,plain,
( earray_278 = select(queue_245,seq)
| tail = seq ),
inference(paramodulation,[status(thm)],[f1037,f1826]) ).
fof(f4480,plain,
index_279 = select(queue_245,head),
inference(forward_subsumption_resolution,[status(thm)],[f4475,f346]) ).
fof(f4481,plain,
( earray_278 = earray_244
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f1809,f4476]) ).
fof(f4482,plain,
earray_278 = earray_244,
inference(forward_subsumption_resolution,[status(thm)],[f4481,f348]) ).
fof(f4495,plain,
elem_283 = select(earray_244,index_282),
inference(backward_demodulation,[status(thm)],[f4482,f448]) ).
fof(f4496,plain,
elem_280 = select(earray_244,index_279),
inference(backward_demodulation,[status(thm)],[f4482,f447]) ).
fof(f4497,plain,
elem_283 = e45,
inference(forward_demodulation,[status(thm)],[f3553,f4495]) ).
fof(f4498,plain,
elem_280 != e45,
inference(backward_demodulation,[status(thm)],[f4497,f685]) ).
fof(f4506,plain,
( seq = head
| index_279 = select(queue_241,head) ),
inference(paramodulation,[status(thm)],[f1808,f4480]) ).
fof(f4508,plain,
index_279 = select(queue_241,head),
inference(forward_subsumption_resolution,[status(thm)],[f4506,f347]) ).
fof(f4529,plain,
( tail = head
| index_279 = select(queue_239,head) ),
inference(paramodulation,[status(thm)],[f1804,f4508]) ).
fof(f4531,plain,
index_279 = select(queue_239,head),
inference(forward_subsumption_resolution,[status(thm)],[f4529,f346]) ).
fof(f4535,plain,
( seq = head
| index_279 = select(queue_235,head) ),
inference(paramodulation,[status(thm)],[f1787,f4531]) ).
fof(f4537,plain,
index_279 = select(queue_235,head),
inference(forward_subsumption_resolution,[status(thm)],[f4535,f347]) ).
fof(f4552,plain,
( tail = head
| index_279 = select(queue_233,head) ),
inference(paramodulation,[status(thm)],[f1776,f4537]) ).
fof(f4554,plain,
index_279 = select(queue_233,head),
inference(forward_subsumption_resolution,[status(thm)],[f4552,f346]) ).
fof(f4575,plain,
( seq = head
| index_279 = select(queue_229,head) ),
inference(paramodulation,[status(thm)],[f1774,f4554]) ).
fof(f4577,plain,
index_279 = select(queue_229,head),
inference(forward_subsumption_resolution,[status(thm)],[f4575,f347]) ).
fof(f4581,plain,
( tail = head
| index_279 = select(queue_227,head) ),
inference(paramodulation,[status(thm)],[f1751,f4577]) ).
fof(f4583,plain,
index_279 = select(queue_227,head),
inference(forward_subsumption_resolution,[status(thm)],[f4581,f346]) ).
fof(f4598,plain,
( seq = head
| index_279 = select(queue_223,head) ),
inference(paramodulation,[status(thm)],[f1749,f4583]) ).
fof(f4600,plain,
index_279 = select(queue_223,head),
inference(forward_subsumption_resolution,[status(thm)],[f4598,f347]) ).
fof(f4608,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_275,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1358,f1916]) ).
fof(f4624,plain,
( tail = head
| index_279 = select(queue_221,head) ),
inference(paramodulation,[status(thm)],[f1738,f4600]) ).
fof(f4626,plain,
index_279 = select(queue_221,head),
inference(forward_subsumption_resolution,[status(thm)],[f4624,f346]) ).
fof(f4643,plain,
( seq = head
| index_279 = select(queue_217,head) ),
inference(paramodulation,[status(thm)],[f1723,f4626]) ).
fof(f4645,plain,
index_279 = select(queue_217,head),
inference(forward_subsumption_resolution,[status(thm)],[f4643,f347]) ).
fof(f4666,plain,
( tail = head
| index_279 = select(queue_215,head) ),
inference(paramodulation,[status(thm)],[f1719,f4645]) ).
fof(f4668,plain,
index_279 = select(queue_215,head),
inference(forward_subsumption_resolution,[status(thm)],[f4666,f346]) ).
fof(f4672,plain,
( seq = head
| index_279 = select(queue_211,head) ),
inference(paramodulation,[status(thm)],[f1717,f4668]) ).
fof(f4674,plain,
index_279 = select(queue_211,head),
inference(forward_subsumption_resolution,[status(thm)],[f4672,f347]) ).
fof(f4689,plain,
( tail = head
| index_279 = select(queue_209,head) ),
inference(paramodulation,[status(thm)],[f1694,f4674]) ).
fof(f4691,plain,
index_279 = select(queue_209,head),
inference(forward_subsumption_resolution,[status(thm)],[f4689,f346]) ).
fof(f4712,plain,
( seq = head
| index_279 = select(queue_199,head) ),
inference(paramodulation,[status(thm)],[f1692,f4691]) ).
fof(f4714,plain,
index_279 = select(queue_199,head),
inference(forward_subsumption_resolution,[status(thm)],[f4712,f347]) ).
fof(f4718,plain,
( tail = head
| index_279 = select(queue_197,head) ),
inference(paramodulation,[status(thm)],[f1661,f4714]) ).
fof(f4720,plain,
index_279 = select(queue_197,head),
inference(forward_subsumption_resolution,[status(thm)],[f4718,f346]) ).
fof(f4726,plain,
( seq = head
| index_279 = select(queue_193,head) ),
inference(paramodulation,[status(thm)],[f1659,f4720]) ).
fof(f4728,plain,
index_279 = select(queue_193,head),
inference(forward_subsumption_resolution,[status(thm)],[f4726,f347]) ).
fof(f4730,plain,
( tail = head
| index_279 = select(queue_191,head) ),
inference(paramodulation,[status(thm)],[f1639,f4728]) ).
fof(f4732,plain,
index_279 = select(queue_191,head),
inference(forward_subsumption_resolution,[status(thm)],[f4730,f346]) ).
fof(f4734,plain,
( seq = head
| index_279 = select(queue_187,head) ),
inference(paramodulation,[status(thm)],[f1637,f4732]) ).
fof(f4736,plain,
index_279 = select(queue_187,head),
inference(forward_subsumption_resolution,[status(thm)],[f4734,f347]) ).
fof(f4764,plain,
( tail = head
| index_279 = select(queue_185,head) ),
inference(paramodulation,[status(thm)],[f1609,f4736]) ).
fof(f4766,plain,
index_279 = select(queue_185,head),
inference(forward_subsumption_resolution,[status(thm)],[f4764,f346]) ).
fof(f4774,plain,
( seq = head
| index_279 = select(queue_181,head) ),
inference(paramodulation,[status(thm)],[f1607,f4766]) ).
fof(f4776,plain,
index_279 = select(queue_181,head),
inference(forward_subsumption_resolution,[status(thm)],[f4774,f347]) ).
fof(f4778,plain,
( tail = head
| index_279 = select(queue_179,head) ),
inference(paramodulation,[status(thm)],[f1603,f4776]) ).
fof(f4780,plain,
index_279 = select(queue_179,head),
inference(forward_subsumption_resolution,[status(thm)],[f4778,f346]) ).
fof(f4808,plain,
( seq = head
| index_279 = select(queue_175,head) ),
inference(paramodulation,[status(thm)],[f1580,f4780]) ).
fof(f4810,plain,
index_279 = select(queue_175,head),
inference(forward_subsumption_resolution,[status(thm)],[f4808,f347]) ).
fof(f4818,plain,
( tail = head
| index_279 = select(queue_173,head) ),
inference(paramodulation,[status(thm)],[f1576,f4810]) ).
fof(f4820,plain,
index_279 = select(queue_173,head),
inference(forward_subsumption_resolution,[status(thm)],[f4818,f346]) ).
fof(f4822,plain,
( seq = head
| index_279 = select(queue_169,head) ),
inference(paramodulation,[status(thm)],[f1562,f4820]) ).
fof(f4824,plain,
index_279 = select(queue_169,head),
inference(forward_subsumption_resolution,[status(thm)],[f4822,f347]) ).
fof(f4826,plain,
( tail = head
| index_279 = select(queue_167,head) ),
inference(paramodulation,[status(thm)],[f1555,f4824]) ).
fof(f4828,plain,
index_279 = select(queue_167,head),
inference(forward_subsumption_resolution,[status(thm)],[f4826,f346]) ).
fof(f4834,plain,
! [X0] :
( seq = X0
| select(queue_137,X0) = select(queue_71,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1447,f2076]) ).
fof(f4850,plain,
( seq = head
| index_279 = select(queue_163,head) ),
inference(paramodulation,[status(thm)],[f1553,f4828]) ).
fof(f4852,plain,
index_279 = select(queue_163,head),
inference(forward_subsumption_resolution,[status(thm)],[f4850,f347]) ).
fof(f4869,plain,
( tail = head
| index_279 = select(queue_161,head) ),
inference(paramodulation,[status(thm)],[f1529,f4852]) ).
fof(f4871,plain,
index_279 = select(queue_161,head),
inference(forward_subsumption_resolution,[status(thm)],[f4869,f346]) ).
fof(f4879,plain,
( seq = head
| index_279 = select(queue_157,head) ),
inference(paramodulation,[status(thm)],[f1527,f4871]) ).
fof(f4881,plain,
index_279 = select(queue_157,head),
inference(forward_subsumption_resolution,[status(thm)],[f4879,f347]) ).
fof(f4894,plain,
( tail = head
| index_279 = select(queue_155,head) ),
inference(paramodulation,[status(thm)],[f1514,f4881]) ).
fof(f4896,plain,
index_279 = select(queue_155,head),
inference(forward_subsumption_resolution,[status(thm)],[f4894,f346]) ).
fof(f4902,plain,
( seq = head
| index_279 = select(queue_151,head) ),
inference(paramodulation,[status(thm)],[f1505,f4896]) ).
fof(f4904,plain,
index_279 = select(queue_151,head),
inference(forward_subsumption_resolution,[status(thm)],[f4902,f347]) ).
fof(f4906,plain,
( tail = head
| index_279 = select(queue_149,head) ),
inference(paramodulation,[status(thm)],[f1501,f4904]) ).
fof(f4908,plain,
index_279 = select(queue_149,head),
inference(forward_subsumption_resolution,[status(thm)],[f4906,f346]) ).
fof(f4910,plain,
( seq = head
| index_279 = select(queue_145,head) ),
inference(paramodulation,[status(thm)],[f1499,f4908]) ).
fof(f4912,plain,
index_279 = select(queue_145,head),
inference(forward_subsumption_resolution,[status(thm)],[f4910,f347]) ).
fof(f4931,plain,
( tail = head
| index_279 = select(queue_143,head) ),
inference(paramodulation,[status(thm)],[f1470,f4912]) ).
fof(f4933,plain,
index_279 = select(queue_143,head),
inference(forward_subsumption_resolution,[status(thm)],[f4931,f346]) ).
fof(f4937,plain,
( seq = head
| index_279 = select(queue_133,head) ),
inference(paramodulation,[status(thm)],[f1468,f4933]) ).
fof(f4939,plain,
index_279 = select(queue_133,head),
inference(forward_subsumption_resolution,[status(thm)],[f4937,f347]) ).
fof(f4943,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_95,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1326,f2148]) ).
fof(f4959,plain,
( tail = head
| index_279 = select(queue_131,head) ),
inference(paramodulation,[status(thm)],[f1443,f4939]) ).
fof(f4961,plain,
index_279 = select(queue_131,head),
inference(forward_subsumption_resolution,[status(thm)],[f4959,f346]) ).
fof(f4976,plain,
( seq = head
| index_279 = select(queue_127,head) ),
inference(paramodulation,[status(thm)],[f1441,f4961]) ).
fof(f4978,plain,
index_279 = select(queue_127,head),
inference(forward_subsumption_resolution,[status(thm)],[f4976,f347]) ).
fof(f4990,plain,
( tail = head
| index_279 = select(queue_125,head) ),
inference(paramodulation,[status(thm)],[f1409,f4978]) ).
fof(f4992,plain,
index_279 = select(queue_125,head),
inference(forward_subsumption_resolution,[status(thm)],[f4990,f346]) ).
fof(f4994,plain,
( seq = head
| index_279 = select(queue_121,head) ),
inference(paramodulation,[status(thm)],[f1407,f4992]) ).
fof(f4996,plain,
index_279 = select(queue_121,head),
inference(forward_subsumption_resolution,[status(thm)],[f4994,f347]) ).
fof(f4998,plain,
( tail = head
| index_279 = select(queue_119,head) ),
inference(paramodulation,[status(thm)],[f1388,f4996]) ).
fof(f5000,plain,
index_279 = select(queue_119,head),
inference(forward_subsumption_resolution,[status(thm)],[f4998,f346]) ).
fof(f5009,plain,
( seq = head
| index_279 = select(queue_115,head) ),
inference(paramodulation,[status(thm)],[f1386,f5000]) ).
fof(f5011,plain,
index_279 = select(queue_115,head),
inference(forward_subsumption_resolution,[status(thm)],[f5009,f347]) ).
fof(f5017,plain,
( tail = head
| index_279 = select(queue_113,head) ),
inference(paramodulation,[status(thm)],[f1382,f5011]) ).
fof(f5019,plain,
index_279 = select(queue_113,head),
inference(forward_subsumption_resolution,[status(thm)],[f5017,f346]) ).
fof(f5021,plain,
( seq = head
| index_279 = select(queue_109,head) ),
inference(paramodulation,[status(thm)],[f1361,f5019]) ).
fof(f5023,plain,
index_279 = select(queue_109,head),
inference(forward_subsumption_resolution,[status(thm)],[f5021,f347]) ).
fof(f5029,plain,
( tail = head
| index_279 = select(queue_107,head) ),
inference(paramodulation,[status(thm)],[f1343,f5023]) ).
fof(f5031,plain,
index_279 = select(queue_107,head),
inference(forward_subsumption_resolution,[status(thm)],[f5029,f346]) ).
fof(f5033,plain,
( seq = head
| index_279 = select(queue_103,head) ),
inference(paramodulation,[status(thm)],[f1332,f5031]) ).
fof(f5035,plain,
index_279 = select(queue_103,head),
inference(forward_subsumption_resolution,[status(thm)],[f5033,f347]) ).
fof(f5037,plain,
( tail = head
| index_279 = select(queue_101,head) ),
inference(paramodulation,[status(thm)],[f1328,f5035]) ).
fof(f5039,plain,
index_279 = select(queue_101,head),
inference(forward_subsumption_resolution,[status(thm)],[f5037,f346]) ).
fof(f5339,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_271,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1914,f4608]) ).
fof(f5342,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_271,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5339]) ).
fof(f5345,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_137,X0) = select(queue_7,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2074,f4834]) ).
fof(f5348,plain,
! [X0] :
( seq = X0
| select(queue_137,X0) = select(queue_7,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5345]) ).
fof(f5351,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_91,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2146,f4943]) ).
fof(f5354,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_91,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5351]) ).
fof(f5373,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_269,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1891,f5342]) ).
fof(f5377,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_269,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5373]) ).
fof(f5384,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_137,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2062,f5348]) ).
fof(f5388,plain,
! [X0] :
( seq = X0
| select(queue_137,X0) = select(queue_5,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5384]) ).
fof(f5392,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_89,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2126,f5354]) ).
fof(f5396,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_89,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5392]) ).
fof(f5399,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_265,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1882,f5377]) ).
fof(f5402,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_265,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5399]) ).
fof(f5411,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_137,X0) = select(queue_1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1992,f5388]) ).
fof(f5414,plain,
! [X0] :
( seq = X0
| select(queue_137,X0) = select(queue_1,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5411]) ).
fof(f5417,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_85,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2124,f5396]) ).
fof(f5420,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_85,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5417]) ).
fof(f5424,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_263,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1878,f5402]) ).
fof(f5428,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_263,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5424]) ).
fof(f5448,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_83,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2105,f5420]) ).
fof(f5452,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_83,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5448]) ).
fof(f5455,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_259,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1876,f5428]) ).
fof(f5458,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_259,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5455]) ).
fof(f5467,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_79,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2096,f5452]) ).
fof(f5470,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_79,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5467]) ).
fof(f5474,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_257,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1861,f5458]) ).
fof(f5478,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_257,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5474]) ).
fof(f5482,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_77,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2092,f5470]) ).
fof(f5486,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_77,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5482]) ).
fof(f5501,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_253,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1859,f5478]) ).
fof(f5504,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_253,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5501]) ).
fof(f5507,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_67,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2090,f5486]) ).
fof(f5510,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_67,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5507]) ).
fof(f5514,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_251,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1848,f5504]) ).
fof(f5518,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_251,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5514]) ).
fof(f5528,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_65,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2045,f5510]) ).
fof(f5532,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_65,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5528]) ).
fof(f5535,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_205,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1833,f5518]) ).
fof(f5538,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_205,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5535]) ).
fof(f5541,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_61,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2043,f5532]) ).
fof(f5544,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_61,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5541]) ).
fof(f5558,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_203,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1674,f5538]) ).
fof(f5562,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_203,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5558]) ).
fof(f5566,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_59,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2039,f5544]) ).
fof(f5570,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_59,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5566]) ).
fof(f5573,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_11,X0) = select(queue_139,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1665,f5562]) ).
fof(f5576,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_139,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5573]) ).
fof(f5585,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_55,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2021,f5570]) ).
fof(f5588,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_55,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5585]) ).
fof(f5592,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_137,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1456,f5576]) ).
fof(f5596,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_137,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5592]) ).
fof(f5600,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_53,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2017,f5588]) ).
fof(f5604,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_53,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5600]) ).
fof(f5620,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(queue_11,X0) = select(queue_1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f5414,f5596]) ).
fof(f5624,plain,
! [X0] :
( seq = X0
| select(queue_11,X0) = select(queue_1,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5620]) ).
fof(f5627,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_49,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2002,f5604]) ).
fof(f5630,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_49,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5627]) ).
fof(f5644,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_47,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1988,f5630]) ).
fof(f5648,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_47,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5644]) ).
fof(f5651,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_43,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1986,f5648]) ).
fof(f5654,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_43,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5651]) ).
fof(f5658,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_41,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1963,f5654]) ).
fof(f5662,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_41,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5658]) ).
fof(f5677,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_37,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1961,f5662]) ).
fof(f5680,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_37,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5677]) ).
fof(f5684,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_35,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1946,f5680]) ).
fof(f5688,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_35,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5684]) ).
fof(f5691,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_31,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1937,f5688]) ).
fof(f5694,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_31,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5691]) ).
fof(f5708,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_29,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1933,f5694]) ).
fof(f5712,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_29,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5708]) ).
fof(f5715,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_25,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1931,f5712]) ).
fof(f5718,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_25,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5715]) ).
fof(f5722,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1829,f5718]) ).
fof(f5726,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_23,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5722]) ).
fof(f5739,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_19,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1771,f5726]) ).
fof(f5742,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_19,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5739]) ).
fof(f5746,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1619,f5742]) ).
fof(f5750,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_17,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5746]) ).
fof(f5753,plain,
! [X0] :
( seq = X0
| seq = X0
| select(queue_101,X0) = select(queue_13,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1559,f5750]) ).
fof(f5756,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_13,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5753]) ).
fof(f5760,plain,
! [X0] :
( tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1412,f5756]) ).
fof(f5764,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_11,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5760]) ).
fof(f5768,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(queue_101,X0) = select(queue_1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f5624,f5764]) ).
fof(f5772,plain,
! [X0] :
( seq = X0
| select(queue_101,X0) = select(queue_1,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5768]) ).
fof(f5774,plain,
( seq = head
| index_279 = select(queue_1,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f5039,f5772]) ).
fof(f5780,plain,
( seq = head
| index_279 = index_282
| tail = head ),
inference(forward_demodulation,[status(thm)],[f3990,f5774]) ).
fof(f5781,plain,
( seq = head
| index_279 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f5780,f346]) ).
fof(f5889,plain,
select(earray_244,index_279) = e45,
inference(backward_demodulation,[status(thm)],[f5951,f3553]) ).
fof(f5951,plain,
index_279 = index_282,
inference(forward_subsumption_resolution,[status(thm)],[f5781,f347]) ).
fof(f5952,plain,
elem_280 = e45,
inference(forward_demodulation,[status(thm)],[f4496,f5889]) ).
fof(f5953,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5952,f4498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n006.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Mon Sep 21 09:11:21 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.16/5.40 % Drodi V4.1.1
% 0.16/5.68 % Refutation found
% 0.16/5.68 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/5.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/5.70 % Elapsed time: 0.300742 seconds
% 0.16/5.70 % CPU time: 2.088985 seconds
% 0.16/5.70 % Total memory used: 146.156 MB
% 0.16/5.70 % Net memory used: 145.008 MB
%------------------------------------------------------------------------------