%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 03:23:49 PM UTC 2026
% Result : Unsatisfiable 6.09s 1.78s
% Output : CNFRefutation 8.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 159
% Number of leaves : 245
% Syntax : Number of formulae : 1012 ( 822 unt; 0 def)
% Number of atoms : 1295 (1294 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 290 ( 7 ~; 283 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 293 ( 293 usr; 289 con; 0-3 aty)
% Number of variables : 181 ( 0 sgn 181 !; 0 ?; 172 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_tail) ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_seq) ).
fof(f6,axiom,
! [X0] : p(s(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ps) ).
fof(f10,axiom,
! [X0] : s(s(s(X0))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circular) ).
fof(f104,axiom,
elem_280 = select(earray_278,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f105,axiom,
elem_283 = select(earray_278,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f106,axiom,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f107,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f108,axiom,
index_105 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f109,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f110,axiom,
index_111 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f111,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f112,axiom,
index_117 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f113,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f114,axiom,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f115,axiom,
index_123 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f116,axiom,
index_126 = s(index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f117,axiom,
index_129 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f118,axiom,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f119,axiom,
index_135 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f120,axiom,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f121,axiom,
index_141 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f122,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f123,axiom,
index_147 = select(q30,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f124,axiom,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f125,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f126,axiom,
index_153 = select(q31,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f127,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f128,axiom,
index_159 = select(q32,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f129,axiom,
index_162 = s(index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f130,axiom,
index_165 = select(q33,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f131,axiom,
index_168 = s(index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f132,axiom,
index_171 = select(q34,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f133,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f134,axiom,
index_177 = select(q35,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f135,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f136,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f137,axiom,
index_183 = select(q36,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f138,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f139,axiom,
index_189 = select(q37,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f140,axiom,
index_192 = s(index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f141,axiom,
index_195 = select(q38,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f142,axiom,
index_198 = s(index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f143,axiom,
index_201 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f144,axiom,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f145,axiom,
index_207 = select(q39,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f146,axiom,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f147,axiom,
index_210 = s(index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f148,axiom,
index_213 = select(q40,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f149,axiom,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f150,axiom,
index_219 = select(q41,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f151,axiom,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f152,axiom,
index_225 = select(q42,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f153,axiom,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f154,axiom,
index_231 = select(q43,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f155,axiom,
index_234 = s(index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f156,axiom,
index_237 = select(q44,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f157,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f158,axiom,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f159,axiom,
index_243 = select(q45,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f160,axiom,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f161,axiom,
index_249 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f162,axiom,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f163,axiom,
index_255 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f164,axiom,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f165,axiom,
index_261 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f166,axiom,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f167,axiom,
index_267 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f168,axiom,
index_27 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f169,axiom,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f170,axiom,
index_273 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f171,axiom,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f172,axiom,
index_279 = select(q46,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f173,axiom,
index_281 = select(q46,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f174,axiom,
s(index_282) = index_281,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f175,plain,
index_281 = s(index_282),
inference(reorient_equations,[],[f174]) ).
fof(f176,axiom,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f177,axiom,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f178,axiom,
index_33 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f179,axiom,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f180,axiom,
index_39 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f181,axiom,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f182,axiom,
index_45 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f183,axiom,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f184,axiom,
index_51 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f185,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f186,axiom,
index_57 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f187,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f188,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f189,axiom,
index_63 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f190,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f191,axiom,
index_69 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f192,axiom,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f193,axiom,
index_75 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f194,axiom,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f195,axiom,
index_81 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f196,axiom,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f197,axiom,
index_87 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f198,axiom,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f199,axiom,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f200,axiom,
index_93 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f201,axiom,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f202,axiom,
index_99 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f203,axiom,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f204,axiom,
queue_101 = store(q23,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f205,axiom,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f206,axiom,
queue_107 = store(q24,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f207,axiom,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f208,axiom,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f209,axiom,
queue_113 = store(q25,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f210,axiom,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f211,axiom,
queue_119 = store(q26,seq,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f212,axiom,
queue_121 = store(queue_119,tail,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f213,axiom,
queue_125 = store(q27,seq,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f214,axiom,
queue_127 = store(queue_125,tail,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f215,axiom,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f216,axiom,
queue_131 = store(q28,seq,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f217,axiom,
queue_133 = store(queue_131,tail,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f218,axiom,
queue_137 = store(q2,seq,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f219,axiom,
queue_139 = store(queue_137,tail,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f220,axiom,
queue_143 = store(q29,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f221,axiom,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f222,axiom,
queue_149 = store(q30,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f223,axiom,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f224,axiom,
queue_155 = store(q31,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f225,axiom,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f226,axiom,
queue_161 = store(q32,seq,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f227,axiom,
queue_163 = store(queue_161,tail,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f228,axiom,
queue_167 = store(q33,seq,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f229,axiom,
queue_169 = store(queue_167,tail,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f230,axiom,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f231,axiom,
queue_173 = store(q34,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f232,axiom,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f233,axiom,
queue_179 = store(q35,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f234,axiom,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f235,axiom,
queue_185 = store(q36,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f236,axiom,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f237,axiom,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f238,axiom,
queue_191 = store(q37,seq,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f239,axiom,
queue_193 = store(queue_191,tail,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f240,axiom,
queue_197 = store(q38,seq,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f241,axiom,
queue_199 = store(queue_197,tail,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f242,axiom,
queue_203 = store(q3,seq,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f243,axiom,
queue_205 = store(queue_203,tail,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f244,axiom,
queue_209 = store(q39,seq,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f245,axiom,
queue_211 = store(queue_209,tail,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f246,axiom,
queue_215 = store(q40,seq,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f247,axiom,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f248,axiom,
queue_221 = store(q41,seq,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f249,axiom,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f250,axiom,
queue_227 = store(q42,seq,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f251,axiom,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f252,axiom,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f253,axiom,
queue_233 = store(q43,seq,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f254,axiom,
queue_235 = store(queue_233,tail,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f255,axiom,
queue_239 = store(q44,seq,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f256,axiom,
queue_241 = store(queue_239,tail,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f257,axiom,
queue_245 = store(q45,seq,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f258,axiom,
queue_247 = store(queue_245,tail,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f259,axiom,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f260,axiom,
queue_251 = store(q4,seq,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f261,axiom,
queue_253 = store(queue_251,tail,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f262,axiom,
queue_257 = store(q5,seq,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f263,axiom,
queue_259 = store(queue_257,tail,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f264,axiom,
queue_263 = store(q6,seq,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f265,axiom,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f266,axiom,
queue_269 = store(q7,seq,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f267,axiom,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f268,axiom,
queue_275 = store(q8,seq,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f269,axiom,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f270,axiom,
queue_29 = store(q12,seq,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f271,axiom,
queue_31 = store(queue_29,tail,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f272,axiom,
queue_35 = store(q13,seq,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f273,axiom,
queue_37 = store(queue_35,tail,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f274,axiom,
queue_41 = store(q14,seq,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f275,axiom,
queue_43 = store(queue_41,tail,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f276,axiom,
queue_47 = store(q15,seq,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f277,axiom,
queue_49 = store(queue_47,tail,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f278,axiom,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp266) ).
fof(f279,axiom,
queue_53 = store(q16,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f280,axiom,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f281,axiom,
queue_59 = store(q17,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f282,axiom,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f283,axiom,
queue_65 = store(q18,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f284,axiom,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f285,axiom,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f286,axiom,
queue_71 = store(q1,seq,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f287,axiom,
queue_73 = store(queue_71,tail,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f288,axiom,
queue_77 = store(q19,seq,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f289,axiom,
queue_79 = store(queue_77,tail,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f290,axiom,
queue_83 = store(q20,seq,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f291,axiom,
queue_85 = store(queue_83,tail,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f292,axiom,
queue_89 = store(q21,seq,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f293,axiom,
queue_91 = store(queue_89,tail,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f294,axiom,
queue_95 = store(q22,seq,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f295,axiom,
queue_97 = store(queue_95,tail,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f296,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f297,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f298,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f299,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f300,axiom,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f301,axiom,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f302,axiom,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f303,axiom,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f304,axiom,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f305,axiom,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f306,axiom,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f307,axiom,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f308,axiom,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f309,axiom,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f310,axiom,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f311,axiom,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f312,axiom,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f313,axiom,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f314,axiom,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f315,axiom,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f316,axiom,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f317,axiom,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f318,axiom,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f319,axiom,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f320,axiom,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f321,axiom,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f322,axiom,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f323,axiom,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f324,axiom,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f325,axiom,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f326,axiom,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f327,axiom,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f328,axiom,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f329,axiom,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f330,axiom,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f331,axiom,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f332,axiom,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f333,axiom,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f334,axiom,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f335,axiom,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f336,axiom,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f337,axiom,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp325) ).
fof(f338,axiom,
q5 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp326) ).
fof(f339,axiom,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp327) ).
fof(f340,axiom,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp328) ).
fof(f341,axiom,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp329) ).
fof(f342,axiom,
q9 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp330) ).
fof(f343,negated_conjecture,
elem_280 != elem_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f391,plain,
index_105 = select(queue_103,tail),
inference(definition_unfolding,[],[f108,f313]) ).
fof(f392,plain,
index_111 = select(queue_109,tail),
inference(definition_unfolding,[],[f110,f314]) ).
fof(f393,plain,
index_117 = select(queue_115,tail),
inference(definition_unfolding,[],[f112,f315]) ).
fof(f394,plain,
index_123 = select(queue_121,tail),
inference(definition_unfolding,[],[f115,f316]) ).
fof(f395,plain,
index_129 = select(queue_127,tail),
inference(definition_unfolding,[],[f117,f317]) ).
fof(f396,plain,
index_135 = select(queue_73,tail),
inference(definition_unfolding,[],[f119,f308]) ).
fof(f397,plain,
index_141 = select(queue_133,tail),
inference(definition_unfolding,[],[f121,f318]) ).
fof(f398,plain,
index_147 = select(queue_145,tail),
inference(definition_unfolding,[],[f123,f320]) ).
fof(f399,plain,
index_15 = select(queue_13,tail),
inference(definition_unfolding,[],[f124,f298]) ).
fof(f400,plain,
index_153 = select(queue_151,tail),
inference(definition_unfolding,[],[f126,f321]) ).
fof(f401,plain,
index_159 = select(queue_157,tail),
inference(definition_unfolding,[],[f128,f322]) ).
fof(f402,plain,
index_165 = select(queue_163,tail),
inference(definition_unfolding,[],[f130,f323]) ).
fof(f403,plain,
index_171 = select(queue_169,tail),
inference(definition_unfolding,[],[f132,f324]) ).
fof(f404,plain,
index_177 = select(queue_175,tail),
inference(definition_unfolding,[],[f134,f325]) ).
fof(f405,plain,
index_183 = select(queue_181,tail),
inference(definition_unfolding,[],[f137,f326]) ).
fof(f406,plain,
index_189 = select(queue_187,tail),
inference(definition_unfolding,[],[f139,f327]) ).
fof(f407,plain,
index_195 = select(queue_193,tail),
inference(definition_unfolding,[],[f141,f328]) ).
fof(f408,plain,
index_201 = select(queue_139,tail),
inference(definition_unfolding,[],[f143,f319]) ).
fof(f409,plain,
index_207 = select(queue_199,tail),
inference(definition_unfolding,[],[f145,f329]) ).
fof(f410,plain,
index_21 = select(queue_19,tail),
inference(definition_unfolding,[],[f146,f299]) ).
fof(f411,plain,
index_213 = select(queue_211,tail),
inference(definition_unfolding,[],[f148,f331]) ).
fof(f412,plain,
index_219 = select(queue_217,tail),
inference(definition_unfolding,[],[f150,f332]) ).
fof(f413,plain,
index_225 = select(queue_223,tail),
inference(definition_unfolding,[],[f152,f333]) ).
fof(f414,plain,
index_231 = select(queue_229,tail),
inference(definition_unfolding,[],[f154,f334]) ).
fof(f415,plain,
index_237 = select(queue_235,tail),
inference(definition_unfolding,[],[f156,f335]) ).
fof(f416,plain,
index_243 = select(queue_241,tail),
inference(definition_unfolding,[],[f159,f336]) ).
fof(f417,plain,
index_249 = select(queue_205,tail),
inference(definition_unfolding,[],[f161,f330]) ).
fof(f418,plain,
index_255 = select(queue_253,tail),
inference(definition_unfolding,[],[f163,f338]) ).
fof(f419,plain,
index_261 = select(queue_259,tail),
inference(definition_unfolding,[],[f165,f339]) ).
fof(f420,plain,
index_267 = select(queue_265,tail),
inference(definition_unfolding,[],[f167,f340]) ).
fof(f421,plain,
index_27 = select(queue_25,tail),
inference(definition_unfolding,[],[f168,f300]) ).
fof(f422,plain,
index_273 = select(queue_271,tail),
inference(definition_unfolding,[],[f170,f341]) ).
fof(f423,plain,
index_279 = select(queue_247,head),
inference(definition_unfolding,[],[f172,f337]) ).
fof(f424,plain,
index_281 = select(queue_247,tail),
inference(definition_unfolding,[],[f173,f337]) ).
fof(f425,plain,
index_3 = select(queue_1,tail),
inference(definition_unfolding,[],[f176,f296]) ).
fof(f426,plain,
index_33 = select(queue_31,tail),
inference(definition_unfolding,[],[f178,f301]) ).
fof(f427,plain,
index_39 = select(queue_37,tail),
inference(definition_unfolding,[],[f180,f302]) ).
fof(f428,plain,
index_45 = select(queue_43,tail),
inference(definition_unfolding,[],[f182,f303]) ).
fof(f429,plain,
index_51 = select(queue_49,tail),
inference(definition_unfolding,[],[f184,f304]) ).
fof(f430,plain,
index_57 = select(queue_55,tail),
inference(definition_unfolding,[],[f186,f305]) ).
fof(f431,plain,
index_63 = select(queue_61,tail),
inference(definition_unfolding,[],[f189,f306]) ).
fof(f432,plain,
index_69 = select(queue_7,tail),
inference(definition_unfolding,[],[f191,f297]) ).
fof(f433,plain,
index_75 = select(queue_67,tail),
inference(definition_unfolding,[],[f193,f307]) ).
fof(f434,plain,
index_81 = select(queue_79,tail),
inference(definition_unfolding,[],[f195,f309]) ).
fof(f435,plain,
index_87 = select(queue_85,tail),
inference(definition_unfolding,[],[f197,f310]) ).
fof(f436,plain,
index_9 = select(queue_277,tail),
inference(definition_unfolding,[],[f198,f342]) ).
fof(f437,plain,
index_93 = select(queue_91,tail),
inference(definition_unfolding,[],[f200,f311]) ).
fof(f438,plain,
index_99 = select(queue_97,tail),
inference(definition_unfolding,[],[f202,f312]) ).
fof(f439,plain,
queue_101 = store(queue_97,seq,earray_100),
inference(definition_unfolding,[],[f204,f312]) ).
fof(f440,plain,
queue_107 = store(queue_103,seq,earray_106),
inference(definition_unfolding,[],[f206,f313]) ).
fof(f441,plain,
queue_11 = store(queue_277,seq,earray_10),
inference(definition_unfolding,[],[f208,f342]) ).
fof(f442,plain,
queue_113 = store(queue_109,seq,earray_112),
inference(definition_unfolding,[],[f209,f314]) ).
fof(f443,plain,
queue_119 = store(queue_115,seq,earray_118),
inference(definition_unfolding,[],[f211,f315]) ).
fof(f444,plain,
queue_125 = store(queue_121,seq,earray_124),
inference(definition_unfolding,[],[f213,f316]) ).
fof(f445,plain,
queue_131 = store(queue_127,seq,earray_130),
inference(definition_unfolding,[],[f216,f317]) ).
fof(f446,plain,
queue_137 = store(queue_73,seq,earray_136),
inference(definition_unfolding,[],[f218,f308]) ).
fof(f447,plain,
queue_143 = store(queue_133,seq,earray_142),
inference(definition_unfolding,[],[f220,f318]) ).
fof(f448,plain,
queue_149 = store(queue_145,seq,earray_148),
inference(definition_unfolding,[],[f222,f320]) ).
fof(f449,plain,
queue_155 = store(queue_151,seq,earray_154),
inference(definition_unfolding,[],[f224,f321]) ).
fof(f450,plain,
queue_161 = store(queue_157,seq,earray_160),
inference(definition_unfolding,[],[f226,f322]) ).
fof(f451,plain,
queue_167 = store(queue_163,seq,earray_166),
inference(definition_unfolding,[],[f228,f323]) ).
fof(f452,plain,
queue_17 = store(queue_13,seq,earray_16),
inference(definition_unfolding,[],[f230,f298]) ).
fof(f453,plain,
queue_173 = store(queue_169,seq,earray_172),
inference(definition_unfolding,[],[f231,f324]) ).
fof(f454,plain,
queue_179 = store(queue_175,seq,earray_178),
inference(definition_unfolding,[],[f233,f325]) ).
fof(f455,plain,
queue_185 = store(queue_181,seq,earray_184),
inference(definition_unfolding,[],[f235,f326]) ).
fof(f456,plain,
queue_191 = store(queue_187,seq,earray_190),
inference(definition_unfolding,[],[f238,f327]) ).
fof(f457,plain,
queue_197 = store(queue_193,seq,earray_196),
inference(definition_unfolding,[],[f240,f328]) ).
fof(f458,plain,
queue_203 = store(queue_139,seq,earray_202),
inference(definition_unfolding,[],[f242,f319]) ).
fof(f459,plain,
queue_209 = store(queue_199,seq,earray_208),
inference(definition_unfolding,[],[f244,f329]) ).
fof(f460,plain,
queue_215 = store(queue_211,seq,earray_214),
inference(definition_unfolding,[],[f246,f331]) ).
fof(f461,plain,
queue_221 = store(queue_217,seq,earray_220),
inference(definition_unfolding,[],[f248,f332]) ).
fof(f462,plain,
queue_227 = store(queue_223,seq,earray_226),
inference(definition_unfolding,[],[f250,f333]) ).
fof(f463,plain,
queue_23 = store(queue_19,seq,earray_22),
inference(definition_unfolding,[],[f252,f299]) ).
fof(f464,plain,
queue_233 = store(queue_229,seq,earray_232),
inference(definition_unfolding,[],[f253,f334]) ).
fof(f465,plain,
queue_239 = store(queue_235,seq,earray_238),
inference(definition_unfolding,[],[f255,f335]) ).
fof(f466,plain,
queue_245 = store(queue_241,seq,earray_244),
inference(definition_unfolding,[],[f257,f336]) ).
fof(f467,plain,
queue_251 = store(queue_205,seq,earray_250),
inference(definition_unfolding,[],[f260,f330]) ).
fof(f468,plain,
queue_257 = store(queue_253,seq,earray_256),
inference(definition_unfolding,[],[f262,f338]) ).
fof(f469,plain,
queue_263 = store(queue_259,seq,earray_262),
inference(definition_unfolding,[],[f264,f339]) ).
fof(f470,plain,
queue_269 = store(queue_265,seq,earray_268),
inference(definition_unfolding,[],[f266,f340]) ).
fof(f471,plain,
queue_275 = store(queue_271,seq,earray_274),
inference(definition_unfolding,[],[f268,f341]) ).
fof(f472,plain,
queue_29 = store(queue_25,seq,earray_28),
inference(definition_unfolding,[],[f270,f300]) ).
fof(f473,plain,
queue_35 = store(queue_31,seq,earray_34),
inference(definition_unfolding,[],[f272,f301]) ).
fof(f474,plain,
queue_41 = store(queue_37,seq,earray_40),
inference(definition_unfolding,[],[f274,f302]) ).
fof(f475,plain,
queue_47 = store(queue_43,seq,earray_46),
inference(definition_unfolding,[],[f276,f303]) ).
fof(f476,plain,
queue_5 = store(queue_1,seq,earray_4),
inference(definition_unfolding,[],[f278,f296]) ).
fof(f477,plain,
queue_53 = store(queue_49,seq,earray_52),
inference(definition_unfolding,[],[f279,f304]) ).
fof(f478,plain,
queue_59 = store(queue_55,seq,earray_58),
inference(definition_unfolding,[],[f281,f305]) ).
fof(f479,plain,
queue_65 = store(queue_61,seq,earray_64),
inference(definition_unfolding,[],[f283,f306]) ).
fof(f480,plain,
queue_71 = store(queue_7,seq,earray_70),
inference(definition_unfolding,[],[f286,f297]) ).
fof(f481,plain,
queue_77 = store(queue_67,seq,earray_76),
inference(definition_unfolding,[],[f288,f307]) ).
fof(f482,plain,
queue_83 = store(queue_79,seq,earray_82),
inference(definition_unfolding,[],[f290,f309]) ).
fof(f483,plain,
queue_89 = store(queue_85,seq,earray_88),
inference(definition_unfolding,[],[f292,f310]) ).
fof(f484,plain,
queue_95 = store(queue_91,seq,earray_94),
inference(definition_unfolding,[],[f294,f311]) ).
tcf(c_391,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_392,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_393,plain,
head != tail,
inference(cnf_transformation,[],[f3]) ).
tcf(c_394,plain,
head != seq,
inference(cnf_transformation,[],[f4]) ).
tcf(c_396,plain,
! [X0: $i] : p(s(X0)) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_400,plain,
! [X0: $i] : s(s(s(X0))) = X0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_494,plain,
select(earray_278,index_279) = elem_280,
inference(cnf_transformation,[],[f104]) ).
tcf(c_495,plain,
select(earray_278,index_282) = elem_283,
inference(cnf_transformation,[],[f105]) ).
tcf(c_496,plain,
select(q,tail) = index_0,
inference(cnf_transformation,[],[f106]) ).
tcf(c_497,plain,
s(index_99) = index_102,
inference(cnf_transformation,[],[f107]) ).
tcf(c_498,plain,
select(queue_103,tail) = index_105,
inference(cnf_transformation,[],[f391]) ).
tcf(c_499,plain,
s(index_105) = index_108,
inference(cnf_transformation,[],[f109]) ).
tcf(c_500,plain,
select(queue_109,tail) = index_111,
inference(cnf_transformation,[],[f392]) ).
tcf(c_501,plain,
s(index_111) = index_114,
inference(cnf_transformation,[],[f111]) ).
tcf(c_502,plain,
select(queue_115,tail) = index_117,
inference(cnf_transformation,[],[f393]) ).
tcf(c_503,plain,
s(index_9) = index_12,
inference(cnf_transformation,[],[f113]) ).
tcf(c_504,plain,
s(index_117) = index_120,
inference(cnf_transformation,[],[f114]) ).
tcf(c_505,plain,
select(queue_121,tail) = index_123,
inference(cnf_transformation,[],[f394]) ).
tcf(c_506,plain,
s(index_123) = index_126,
inference(cnf_transformation,[],[f116]) ).
tcf(c_507,plain,
select(queue_127,tail) = index_129,
inference(cnf_transformation,[],[f395]) ).
tcf(c_508,plain,
s(index_129) = index_132,
inference(cnf_transformation,[],[f118]) ).
tcf(c_509,plain,
select(queue_73,tail) = index_135,
inference(cnf_transformation,[],[f396]) ).
tcf(c_510,plain,
s(index_135) = index_138,
inference(cnf_transformation,[],[f120]) ).
tcf(c_511,plain,
select(queue_133,tail) = index_141,
inference(cnf_transformation,[],[f397]) ).
tcf(c_512,plain,
s(index_141) = index_144,
inference(cnf_transformation,[],[f122]) ).
tcf(c_513,plain,
select(queue_145,tail) = index_147,
inference(cnf_transformation,[],[f398]) ).
tcf(c_514,plain,
select(queue_13,tail) = index_15,
inference(cnf_transformation,[],[f399]) ).
tcf(c_515,plain,
s(index_147) = index_150,
inference(cnf_transformation,[],[f125]) ).
tcf(c_516,plain,
select(queue_151,tail) = index_153,
inference(cnf_transformation,[],[f400]) ).
tcf(c_517,plain,
s(index_153) = index_156,
inference(cnf_transformation,[],[f127]) ).
tcf(c_518,plain,
select(queue_157,tail) = index_159,
inference(cnf_transformation,[],[f401]) ).
tcf(c_519,plain,
s(index_159) = index_162,
inference(cnf_transformation,[],[f129]) ).
tcf(c_520,plain,
select(queue_163,tail) = index_165,
inference(cnf_transformation,[],[f402]) ).
tcf(c_521,plain,
s(index_165) = index_168,
inference(cnf_transformation,[],[f131]) ).
tcf(c_522,plain,
select(queue_169,tail) = index_171,
inference(cnf_transformation,[],[f403]) ).
tcf(c_523,plain,
s(index_171) = index_174,
inference(cnf_transformation,[],[f133]) ).
tcf(c_524,plain,
select(queue_175,tail) = index_177,
inference(cnf_transformation,[],[f404]) ).
tcf(c_525,plain,
s(index_15) = index_18,
inference(cnf_transformation,[],[f135]) ).
tcf(c_526,plain,
s(index_177) = index_180,
inference(cnf_transformation,[],[f136]) ).
tcf(c_527,plain,
select(queue_181,tail) = index_183,
inference(cnf_transformation,[],[f405]) ).
tcf(c_528,plain,
s(index_183) = index_186,
inference(cnf_transformation,[],[f138]) ).
tcf(c_529,plain,
select(queue_187,tail) = index_189,
inference(cnf_transformation,[],[f406]) ).
tcf(c_530,plain,
s(index_189) = index_192,
inference(cnf_transformation,[],[f140]) ).
tcf(c_531,plain,
select(queue_193,tail) = index_195,
inference(cnf_transformation,[],[f407]) ).
tcf(c_532,plain,
s(index_195) = index_198,
inference(cnf_transformation,[],[f142]) ).
tcf(c_533,plain,
select(queue_139,tail) = index_201,
inference(cnf_transformation,[],[f408]) ).
tcf(c_534,plain,
s(index_201) = index_204,
inference(cnf_transformation,[],[f144]) ).
tcf(c_535,plain,
select(queue_199,tail) = index_207,
inference(cnf_transformation,[],[f409]) ).
tcf(c_536,plain,
select(queue_19,tail) = index_21,
inference(cnf_transformation,[],[f410]) ).
tcf(c_537,plain,
s(index_207) = index_210,
inference(cnf_transformation,[],[f147]) ).
tcf(c_538,plain,
select(queue_211,tail) = index_213,
inference(cnf_transformation,[],[f411]) ).
tcf(c_539,plain,
s(index_213) = index_216,
inference(cnf_transformation,[],[f149]) ).
tcf(c_540,plain,
select(queue_217,tail) = index_219,
inference(cnf_transformation,[],[f412]) ).
tcf(c_541,plain,
s(index_219) = index_222,
inference(cnf_transformation,[],[f151]) ).
tcf(c_542,plain,
select(queue_223,tail) = index_225,
inference(cnf_transformation,[],[f413]) ).
tcf(c_543,plain,
s(index_225) = index_228,
inference(cnf_transformation,[],[f153]) ).
tcf(c_544,plain,
select(queue_229,tail) = index_231,
inference(cnf_transformation,[],[f414]) ).
tcf(c_545,plain,
s(index_231) = index_234,
inference(cnf_transformation,[],[f155]) ).
tcf(c_546,plain,
select(queue_235,tail) = index_237,
inference(cnf_transformation,[],[f415]) ).
tcf(c_547,plain,
s(index_21) = index_24,
inference(cnf_transformation,[],[f157]) ).
tcf(c_548,plain,
s(index_237) = index_240,
inference(cnf_transformation,[],[f158]) ).
tcf(c_549,plain,
select(queue_241,tail) = index_243,
inference(cnf_transformation,[],[f416]) ).
tcf(c_550,plain,
s(index_243) = index_246,
inference(cnf_transformation,[],[f160]) ).
tcf(c_551,plain,
select(queue_205,tail) = index_249,
inference(cnf_transformation,[],[f417]) ).
tcf(c_552,plain,
s(index_249) = index_252,
inference(cnf_transformation,[],[f162]) ).
tcf(c_553,plain,
select(queue_253,tail) = index_255,
inference(cnf_transformation,[],[f418]) ).
tcf(c_554,plain,
s(index_255) = index_258,
inference(cnf_transformation,[],[f164]) ).
tcf(c_555,plain,
select(queue_259,tail) = index_261,
inference(cnf_transformation,[],[f419]) ).
tcf(c_556,plain,
s(index_261) = index_264,
inference(cnf_transformation,[],[f166]) ).
tcf(c_557,plain,
select(queue_265,tail) = index_267,
inference(cnf_transformation,[],[f420]) ).
tcf(c_558,plain,
select(queue_25,tail) = index_27,
inference(cnf_transformation,[],[f421]) ).
tcf(c_559,plain,
s(index_267) = index_270,
inference(cnf_transformation,[],[f169]) ).
tcf(c_560,plain,
select(queue_271,tail) = index_273,
inference(cnf_transformation,[],[f422]) ).
tcf(c_561,plain,
s(index_273) = index_276,
inference(cnf_transformation,[],[f171]) ).
tcf(c_562,plain,
select(queue_247,head) = index_279,
inference(cnf_transformation,[],[f423]) ).
tcf(c_563,plain,
select(queue_247,tail) = index_281,
inference(cnf_transformation,[],[f424]) ).
tcf(c_564,plain,
s(index_282) = index_281,
inference(cnf_transformation,[],[f175]) ).
tcf(c_565,plain,
select(queue_1,tail) = index_3,
inference(cnf_transformation,[],[f425]) ).
tcf(c_566,plain,
s(index_27) = index_30,
inference(cnf_transformation,[],[f177]) ).
tcf(c_567,plain,
select(queue_31,tail) = index_33,
inference(cnf_transformation,[],[f426]) ).
tcf(c_568,plain,
s(index_33) = index_36,
inference(cnf_transformation,[],[f179]) ).
tcf(c_569,plain,
select(queue_37,tail) = index_39,
inference(cnf_transformation,[],[f427]) ).
tcf(c_570,plain,
s(index_39) = index_42,
inference(cnf_transformation,[],[f181]) ).
tcf(c_571,plain,
select(queue_43,tail) = index_45,
inference(cnf_transformation,[],[f428]) ).
tcf(c_572,plain,
s(index_45) = index_48,
inference(cnf_transformation,[],[f183]) ).
tcf(c_573,plain,
select(queue_49,tail) = index_51,
inference(cnf_transformation,[],[f429]) ).
tcf(c_574,plain,
s(index_51) = index_54,
inference(cnf_transformation,[],[f185]) ).
tcf(c_575,plain,
select(queue_55,tail) = index_57,
inference(cnf_transformation,[],[f430]) ).
tcf(c_576,plain,
s(index_3) = index_6,
inference(cnf_transformation,[],[f187]) ).
tcf(c_577,plain,
s(index_57) = index_60,
inference(cnf_transformation,[],[f188]) ).
tcf(c_578,plain,
select(queue_61,tail) = index_63,
inference(cnf_transformation,[],[f431]) ).
tcf(c_579,plain,
s(index_63) = index_66,
inference(cnf_transformation,[],[f190]) ).
tcf(c_580,plain,
select(queue_7,tail) = index_69,
inference(cnf_transformation,[],[f432]) ).
tcf(c_581,plain,
s(index_69) = index_72,
inference(cnf_transformation,[],[f192]) ).
tcf(c_582,plain,
select(queue_67,tail) = index_75,
inference(cnf_transformation,[],[f433]) ).
tcf(c_583,plain,
s(index_75) = index_78,
inference(cnf_transformation,[],[f194]) ).
tcf(c_584,plain,
select(queue_79,tail) = index_81,
inference(cnf_transformation,[],[f434]) ).
tcf(c_585,plain,
s(index_81) = index_84,
inference(cnf_transformation,[],[f196]) ).
tcf(c_586,plain,
select(queue_85,tail) = index_87,
inference(cnf_transformation,[],[f435]) ).
tcf(c_587,plain,
select(queue_277,tail) = index_9,
inference(cnf_transformation,[],[f436]) ).
tcf(c_588,plain,
s(index_87) = index_90,
inference(cnf_transformation,[],[f199]) ).
tcf(c_589,plain,
select(queue_91,tail) = index_93,
inference(cnf_transformation,[],[f437]) ).
tcf(c_590,plain,
s(index_93) = index_96,
inference(cnf_transformation,[],[f201]) ).
tcf(c_591,plain,
select(queue_97,tail) = index_99,
inference(cnf_transformation,[],[f438]) ).
tcf(c_592,plain,
store(q,head,index_0) = queue_1,
inference(cnf_transformation,[],[f203]) ).
tcf(c_593,plain,
store(queue_97,seq,earray_100) = queue_101,
inference(cnf_transformation,[],[f439]) ).
tcf(c_594,plain,
store(queue_101,tail,index_102) = queue_103,
inference(cnf_transformation,[],[f205]) ).
tcf(c_595,plain,
store(queue_103,seq,earray_106) = queue_107,
inference(cnf_transformation,[],[f440]) ).
tcf(c_596,plain,
store(queue_107,tail,index_108) = queue_109,
inference(cnf_transformation,[],[f207]) ).
tcf(c_597,plain,
store(queue_277,seq,earray_10) = queue_11,
inference(cnf_transformation,[],[f441]) ).
tcf(c_598,plain,
store(queue_109,seq,earray_112) = queue_113,
inference(cnf_transformation,[],[f442]) ).
tcf(c_599,plain,
store(queue_113,tail,index_114) = queue_115,
inference(cnf_transformation,[],[f210]) ).
tcf(c_600,plain,
store(queue_115,seq,earray_118) = queue_119,
inference(cnf_transformation,[],[f443]) ).
tcf(c_601,plain,
store(queue_119,tail,index_120) = queue_121,
inference(cnf_transformation,[],[f212]) ).
tcf(c_602,plain,
store(queue_121,seq,earray_124) = queue_125,
inference(cnf_transformation,[],[f444]) ).
tcf(c_603,plain,
store(queue_125,tail,index_126) = queue_127,
inference(cnf_transformation,[],[f214]) ).
tcf(c_604,plain,
store(queue_11,tail,index_12) = queue_13,
inference(cnf_transformation,[],[f215]) ).
tcf(c_605,plain,
store(queue_127,seq,earray_130) = queue_131,
inference(cnf_transformation,[],[f445]) ).
tcf(c_606,plain,
store(queue_131,tail,index_132) = queue_133,
inference(cnf_transformation,[],[f217]) ).
tcf(c_607,plain,
store(queue_73,seq,earray_136) = queue_137,
inference(cnf_transformation,[],[f446]) ).
tcf(c_608,plain,
store(queue_137,tail,index_138) = queue_139,
inference(cnf_transformation,[],[f219]) ).
tcf(c_609,plain,
store(queue_133,seq,earray_142) = queue_143,
inference(cnf_transformation,[],[f447]) ).
tcf(c_610,plain,
store(queue_143,tail,index_144) = queue_145,
inference(cnf_transformation,[],[f221]) ).
tcf(c_611,plain,
store(queue_145,seq,earray_148) = queue_149,
inference(cnf_transformation,[],[f448]) ).
tcf(c_612,plain,
store(queue_149,tail,index_150) = queue_151,
inference(cnf_transformation,[],[f223]) ).
tcf(c_613,plain,
store(queue_151,seq,earray_154) = queue_155,
inference(cnf_transformation,[],[f449]) ).
tcf(c_614,plain,
store(queue_155,tail,index_156) = queue_157,
inference(cnf_transformation,[],[f225]) ).
tcf(c_615,plain,
store(queue_157,seq,earray_160) = queue_161,
inference(cnf_transformation,[],[f450]) ).
tcf(c_616,plain,
store(queue_161,tail,index_162) = queue_163,
inference(cnf_transformation,[],[f227]) ).
tcf(c_617,plain,
store(queue_163,seq,earray_166) = queue_167,
inference(cnf_transformation,[],[f451]) ).
tcf(c_618,plain,
store(queue_167,tail,index_168) = queue_169,
inference(cnf_transformation,[],[f229]) ).
tcf(c_619,plain,
store(queue_13,seq,earray_16) = queue_17,
inference(cnf_transformation,[],[f452]) ).
tcf(c_620,plain,
store(queue_169,seq,earray_172) = queue_173,
inference(cnf_transformation,[],[f453]) ).
tcf(c_621,plain,
store(queue_173,tail,index_174) = queue_175,
inference(cnf_transformation,[],[f232]) ).
tcf(c_622,plain,
store(queue_175,seq,earray_178) = queue_179,
inference(cnf_transformation,[],[f454]) ).
tcf(c_623,plain,
store(queue_179,tail,index_180) = queue_181,
inference(cnf_transformation,[],[f234]) ).
tcf(c_624,plain,
store(queue_181,seq,earray_184) = queue_185,
inference(cnf_transformation,[],[f455]) ).
tcf(c_625,plain,
store(queue_185,tail,index_186) = queue_187,
inference(cnf_transformation,[],[f236]) ).
tcf(c_626,plain,
store(queue_17,tail,index_18) = queue_19,
inference(cnf_transformation,[],[f237]) ).
tcf(c_627,plain,
store(queue_187,seq,earray_190) = queue_191,
inference(cnf_transformation,[],[f456]) ).
tcf(c_628,plain,
store(queue_191,tail,index_192) = queue_193,
inference(cnf_transformation,[],[f239]) ).
tcf(c_629,plain,
store(queue_193,seq,earray_196) = queue_197,
inference(cnf_transformation,[],[f457]) ).
tcf(c_630,plain,
store(queue_197,tail,index_198) = queue_199,
inference(cnf_transformation,[],[f241]) ).
tcf(c_631,plain,
store(queue_139,seq,earray_202) = queue_203,
inference(cnf_transformation,[],[f458]) ).
tcf(c_632,plain,
store(queue_203,tail,index_204) = queue_205,
inference(cnf_transformation,[],[f243]) ).
tcf(c_633,plain,
store(queue_199,seq,earray_208) = queue_209,
inference(cnf_transformation,[],[f459]) ).
tcf(c_634,plain,
store(queue_209,tail,index_210) = queue_211,
inference(cnf_transformation,[],[f245]) ).
tcf(c_635,plain,
store(queue_211,seq,earray_214) = queue_215,
inference(cnf_transformation,[],[f460]) ).
tcf(c_636,plain,
store(queue_215,tail,index_216) = queue_217,
inference(cnf_transformation,[],[f247]) ).
tcf(c_637,plain,
store(queue_217,seq,earray_220) = queue_221,
inference(cnf_transformation,[],[f461]) ).
tcf(c_638,plain,
store(queue_221,tail,index_222) = queue_223,
inference(cnf_transformation,[],[f249]) ).
tcf(c_639,plain,
store(queue_223,seq,earray_226) = queue_227,
inference(cnf_transformation,[],[f462]) ).
tcf(c_640,plain,
store(queue_227,tail,index_228) = queue_229,
inference(cnf_transformation,[],[f251]) ).
tcf(c_641,plain,
store(queue_19,seq,earray_22) = queue_23,
inference(cnf_transformation,[],[f463]) ).
tcf(c_642,plain,
store(queue_229,seq,earray_232) = queue_233,
inference(cnf_transformation,[],[f464]) ).
tcf(c_643,plain,
store(queue_233,tail,index_234) = queue_235,
inference(cnf_transformation,[],[f254]) ).
tcf(c_644,plain,
store(queue_235,seq,earray_238) = queue_239,
inference(cnf_transformation,[],[f465]) ).
tcf(c_645,plain,
store(queue_239,tail,index_240) = queue_241,
inference(cnf_transformation,[],[f256]) ).
tcf(c_646,plain,
store(queue_241,seq,earray_244) = queue_245,
inference(cnf_transformation,[],[f466]) ).
tcf(c_647,plain,
store(queue_245,tail,index_246) = queue_247,
inference(cnf_transformation,[],[f258]) ).
tcf(c_648,plain,
store(queue_23,tail,index_24) = queue_25,
inference(cnf_transformation,[],[f259]) ).
tcf(c_649,plain,
store(queue_205,seq,earray_250) = queue_251,
inference(cnf_transformation,[],[f467]) ).
tcf(c_650,plain,
store(queue_251,tail,index_252) = queue_253,
inference(cnf_transformation,[],[f261]) ).
tcf(c_651,plain,
store(queue_253,seq,earray_256) = queue_257,
inference(cnf_transformation,[],[f468]) ).
tcf(c_652,plain,
store(queue_257,tail,index_258) = queue_259,
inference(cnf_transformation,[],[f263]) ).
tcf(c_653,plain,
store(queue_259,seq,earray_262) = queue_263,
inference(cnf_transformation,[],[f469]) ).
tcf(c_654,plain,
store(queue_263,tail,index_264) = queue_265,
inference(cnf_transformation,[],[f265]) ).
tcf(c_655,plain,
store(queue_265,seq,earray_268) = queue_269,
inference(cnf_transformation,[],[f470]) ).
tcf(c_656,plain,
store(queue_269,tail,index_270) = queue_271,
inference(cnf_transformation,[],[f267]) ).
tcf(c_657,plain,
store(queue_271,seq,earray_274) = queue_275,
inference(cnf_transformation,[],[f471]) ).
tcf(c_658,plain,
store(queue_275,tail,index_276) = queue_277,
inference(cnf_transformation,[],[f269]) ).
tcf(c_659,plain,
store(queue_25,seq,earray_28) = queue_29,
inference(cnf_transformation,[],[f472]) ).
tcf(c_660,plain,
store(queue_29,tail,index_30) = queue_31,
inference(cnf_transformation,[],[f271]) ).
tcf(c_661,plain,
store(queue_31,seq,earray_34) = queue_35,
inference(cnf_transformation,[],[f473]) ).
tcf(c_662,plain,
store(queue_35,tail,index_36) = queue_37,
inference(cnf_transformation,[],[f273]) ).
tcf(c_663,plain,
store(queue_37,seq,earray_40) = queue_41,
inference(cnf_transformation,[],[f474]) ).
tcf(c_664,plain,
store(queue_41,tail,index_42) = queue_43,
inference(cnf_transformation,[],[f275]) ).
tcf(c_665,plain,
store(queue_43,seq,earray_46) = queue_47,
inference(cnf_transformation,[],[f475]) ).
tcf(c_666,plain,
store(queue_47,tail,index_48) = queue_49,
inference(cnf_transformation,[],[f277]) ).
tcf(c_667,plain,
store(queue_1,seq,earray_4) = queue_5,
inference(cnf_transformation,[],[f476]) ).
tcf(c_668,plain,
store(queue_49,seq,earray_52) = queue_53,
inference(cnf_transformation,[],[f477]) ).
tcf(c_669,plain,
store(queue_53,tail,index_54) = queue_55,
inference(cnf_transformation,[],[f280]) ).
tcf(c_670,plain,
store(queue_55,seq,earray_58) = queue_59,
inference(cnf_transformation,[],[f478]) ).
tcf(c_671,plain,
store(queue_59,tail,index_60) = queue_61,
inference(cnf_transformation,[],[f282]) ).
tcf(c_672,plain,
store(queue_61,seq,earray_64) = queue_65,
inference(cnf_transformation,[],[f479]) ).
tcf(c_673,plain,
store(queue_65,tail,index_66) = queue_67,
inference(cnf_transformation,[],[f284]) ).
tcf(c_674,plain,
store(queue_5,tail,index_6) = queue_7,
inference(cnf_transformation,[],[f285]) ).
tcf(c_675,plain,
store(queue_7,seq,earray_70) = queue_71,
inference(cnf_transformation,[],[f480]) ).
tcf(c_676,plain,
store(queue_71,tail,index_72) = queue_73,
inference(cnf_transformation,[],[f287]) ).
tcf(c_677,plain,
store(queue_67,seq,earray_76) = queue_77,
inference(cnf_transformation,[],[f481]) ).
tcf(c_678,plain,
store(queue_77,tail,index_78) = queue_79,
inference(cnf_transformation,[],[f289]) ).
tcf(c_679,plain,
store(queue_79,seq,earray_82) = queue_83,
inference(cnf_transformation,[],[f482]) ).
tcf(c_680,plain,
store(queue_83,tail,index_84) = queue_85,
inference(cnf_transformation,[],[f291]) ).
tcf(c_681,plain,
store(queue_85,seq,earray_88) = queue_89,
inference(cnf_transformation,[],[f483]) ).
tcf(c_682,plain,
store(queue_89,tail,index_90) = queue_91,
inference(cnf_transformation,[],[f293]) ).
tcf(c_683,plain,
store(queue_91,seq,earray_94) = queue_95,
inference(cnf_transformation,[],[f484]) ).
tcf(c_684,plain,
store(queue_95,tail,index_96) = queue_97,
inference(cnf_transformation,[],[f295]) ).
tcf(c_685,negated_conjecture,
elem_280 != elem_283,
inference(cnf_transformation,[],[f343]) ).
tcf(c_1293,negated_conjecture,
elem_280 != elem_283,
inference(demodulation,[status(thm)],[c_685]) ).
tcf(c_1927,plain,
p(index_102) = index_99,
inference(superposition,[status(thm)],[c_497,c_396]) ).
tcf(c_1928,plain,
p(index_108) = index_105,
inference(superposition,[status(thm)],[c_499,c_396]) ).
tcf(c_1929,plain,
p(index_114) = index_111,
inference(superposition,[status(thm)],[c_501,c_396]) ).
tcf(c_1930,plain,
p(index_12) = index_9,
inference(superposition,[status(thm)],[c_503,c_396]) ).
tcf(c_1934,plain,
p(index_138) = index_135,
inference(superposition,[status(thm)],[c_510,c_396]) ).
tcf(c_1941,plain,
p(index_18) = index_15,
inference(superposition,[status(thm)],[c_525,c_396]) ).
tcf(c_1952,plain,
p(index_24) = index_21,
inference(superposition,[status(thm)],[c_547,c_396]) ).
tcf(c_1955,plain,
p(index_252) = index_249,
inference(superposition,[status(thm)],[c_552,c_396]) ).
tcf(c_1960,plain,
p(index_281) = index_282,
inference(superposition,[status(thm)],[c_564,c_396]) ).
tcf(c_1966,plain,
p(index_6) = index_3,
inference(superposition,[status(thm)],[c_576,c_396]) ).
tcf(c_1969,plain,
p(index_72) = index_69,
inference(superposition,[status(thm)],[c_581,c_396]) ).
tcf(c_2269,plain,
! [X0: $i] : s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c_400,c_396]) ).
tcf(c_2412,plain,
s(index_108) = p(index_105),
inference(superposition,[status(thm)],[c_499,c_2269]) ).
tcf(c_2425,plain,
s(index_18) = p(index_15),
inference(superposition,[status(thm)],[c_525,c_2269]) ).
tcf(c_2430,plain,
s(index_204) = p(index_201),
inference(superposition,[status(thm)],[c_534,c_2269]) ).
tcf(c_2803,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(q,X0) = select(queue_1,X0) ) ),
inference(superposition,[status(thm)],[c_592,c_392]) ).
tcf(c_2804,plain,
select(queue_1,head) = index_0,
inference(superposition,[status(thm)],[c_592,c_391]) ).
tcf(c_2862,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_101,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_593,c_392]) ).
tcf(c_2867,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_101,X0) = select(queue_103,X0) ) ),
inference(superposition,[status(thm)],[c_594,c_392]) ).
tcf(c_2868,plain,
select(queue_103,tail) = index_102,
inference(superposition,[status(thm)],[c_594,c_391]) ).
tcf(c_2869,plain,
index_105 = index_102,
inference(light_normalisation,[status(thm)],[c_2868,c_498]) ).
tcf(c_2876,plain,
p(index_105) = index_99,
inference(demodulation,[status(thm)],[c_1927,c_2869]) ).
tcf(c_2877,plain,
s(index_99) = index_105,
inference(demodulation,[status(thm)],[c_497,c_2869]) ).
tcf(c_2878,plain,
s(index_108) = index_99,
inference(demodulation,[status(thm)],[c_2412,c_2876]) ).
tcf(c_2882,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_103,X0) = select(queue_107,X0) ) ),
inference(superposition,[status(thm)],[c_595,c_392]) ).
tcf(c_2887,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_107,X0) = select(queue_109,X0) ) ),
inference(superposition,[status(thm)],[c_596,c_392]) ).
tcf(c_2888,plain,
select(queue_109,tail) = index_108,
inference(superposition,[status(thm)],[c_596,c_391]) ).
tcf(c_2889,plain,
index_111 = index_108,
inference(light_normalisation,[status(thm)],[c_2888,c_500]) ).
tcf(c_2894,plain,
p(index_111) = index_105,
inference(demodulation,[status(thm)],[c_1928,c_2889]) ).
tcf(c_2895,plain,
s(index_105) = index_111,
inference(demodulation,[status(thm)],[c_499,c_2889]) ).
tcf(c_2904,plain,
index_99 = index_114,
inference(light_normalisation,[status(thm)],[c_2878,c_501,c_2889]) ).
tcf(c_2906,plain,
p(index_99) = index_111,
inference(demodulation,[status(thm)],[c_1929,c_2904]) ).
tcf(c_2907,plain,
s(index_111) = index_99,
inference(demodulation,[status(thm)],[c_501,c_2904]) ).
tcf(c_2925,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_11,X0) = select(queue_277,X0) ) ),
inference(superposition,[status(thm)],[c_597,c_392]) ).
tcf(c_2930,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_109,X0) = select(queue_113,X0) ) ),
inference(superposition,[status(thm)],[c_598,c_392]) ).
tcf(c_2935,plain,
store(queue_113,tail,index_99) = queue_115,
inference(light_normalisation,[status(thm)],[c_599,c_2904]) ).
tcf(c_2936,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_113,X0) = select(queue_115,X0) ) ),
inference(superposition,[status(thm)],[c_2935,c_392]) ).
tcf(c_2937,plain,
select(queue_115,tail) = index_99,
inference(superposition,[status(thm)],[c_2935,c_391]) ).
tcf(c_2940,plain,
index_99 = index_117,
inference(demodulation,[status(thm)],[c_502,c_2937]) ).
tcf(c_2948,plain,
s(index_99) = index_120,
inference(demodulation,[status(thm)],[c_504,c_2940]) ).
tcf(c_2949,plain,
index_105 = index_120,
inference(light_normalisation,[status(thm)],[c_2948,c_2877]) ).
tcf(c_2954,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_115,X0) = select(queue_119,X0) ) ),
inference(superposition,[status(thm)],[c_600,c_392]) ).
tcf(c_2992,plain,
store(queue_119,tail,index_105) = queue_121,
inference(light_normalisation,[status(thm)],[c_601,c_2949]) ).
tcf(c_2993,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_119,X0) = select(queue_121,X0) ) ),
inference(superposition,[status(thm)],[c_2992,c_392]) ).
tcf(c_2994,plain,
select(queue_121,tail) = index_105,
inference(superposition,[status(thm)],[c_2992,c_391]) ).
tcf(c_2997,plain,
index_105 = index_123,
inference(demodulation,[status(thm)],[c_505,c_2994]) ).
tcf(c_3005,plain,
s(index_105) = index_126,
inference(demodulation,[status(thm)],[c_506,c_2997]) ).
tcf(c_3006,plain,
index_111 = index_126,
inference(light_normalisation,[status(thm)],[c_3005,c_2895]) ).
tcf(c_3011,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_121,X0) = select(queue_125,X0) ) ),
inference(superposition,[status(thm)],[c_602,c_392]) ).
tcf(c_3016,plain,
store(queue_125,tail,index_111) = queue_127,
inference(light_normalisation,[status(thm)],[c_603,c_3006]) ).
tcf(c_3017,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_125,X0) = select(queue_127,X0) ) ),
inference(superposition,[status(thm)],[c_3016,c_392]) ).
tcf(c_3018,plain,
select(queue_127,tail) = index_111,
inference(superposition,[status(thm)],[c_3016,c_391]) ).
tcf(c_3021,plain,
index_111 = index_129,
inference(demodulation,[status(thm)],[c_507,c_3018]) ).
tcf(c_3029,plain,
s(index_111) = index_132,
inference(demodulation,[status(thm)],[c_508,c_3021]) ).
tcf(c_3030,plain,
index_99 = index_132,
inference(light_normalisation,[status(thm)],[c_3029,c_2907]) ).
tcf(c_3035,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_11,X0) = select(queue_13,X0) ) ),
inference(superposition,[status(thm)],[c_604,c_392]) ).
tcf(c_3036,plain,
select(queue_13,tail) = index_12,
inference(superposition,[status(thm)],[c_604,c_391]) ).
tcf(c_3037,plain,
index_15 = index_12,
inference(light_normalisation,[status(thm)],[c_3036,c_514]) ).
tcf(c_3044,plain,
p(index_15) = index_9,
inference(demodulation,[status(thm)],[c_1930,c_3037]) ).
tcf(c_3045,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[c_503,c_3037]) ).
tcf(c_3046,plain,
s(index_18) = index_9,
inference(demodulation,[status(thm)],[c_2425,c_3044]) ).
tcf(c_3065,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_127,X0) = select(queue_131,X0) ) ),
inference(superposition,[status(thm)],[c_605,c_392]) ).
tcf(c_3070,plain,
store(queue_131,tail,index_99) = queue_133,
inference(light_normalisation,[status(thm)],[c_606,c_3030]) ).
tcf(c_3071,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_131,X0) = select(queue_133,X0) ) ),
inference(superposition,[status(thm)],[c_3070,c_392]) ).
tcf(c_3072,plain,
select(queue_133,tail) = index_99,
inference(superposition,[status(thm)],[c_3070,c_391]) ).
tcf(c_3075,plain,
index_99 = index_141,
inference(demodulation,[status(thm)],[c_511,c_3072]) ).
tcf(c_3082,plain,
s(index_99) = index_144,
inference(demodulation,[status(thm)],[c_512,c_3075]) ).
tcf(c_3083,plain,
index_105 = index_144,
inference(light_normalisation,[status(thm)],[c_3082,c_2877]) ).
tcf(c_3085,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_137,X0) = select(queue_73,X0) ) ),
inference(superposition,[status(thm)],[c_607,c_392]) ).
tcf(c_3090,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_137,X0) = select(queue_139,X0) ) ),
inference(superposition,[status(thm)],[c_608,c_392]) ).
tcf(c_3091,plain,
select(queue_139,tail) = index_138,
inference(superposition,[status(thm)],[c_608,c_391]) ).
tcf(c_3092,plain,
index_201 = index_138,
inference(light_normalisation,[status(thm)],[c_3091,c_533]) ).
tcf(c_3099,plain,
p(index_201) = index_135,
inference(demodulation,[status(thm)],[c_1934,c_3092]) ).
tcf(c_3100,plain,
s(index_135) = index_201,
inference(demodulation,[status(thm)],[c_510,c_3092]) ).
tcf(c_3101,plain,
s(index_204) = index_135,
inference(demodulation,[status(thm)],[c_2430,c_3099]) ).
tcf(c_3129,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_133,X0) = select(queue_143,X0) ) ),
inference(superposition,[status(thm)],[c_609,c_392]) ).
tcf(c_3134,plain,
store(queue_143,tail,index_105) = queue_145,
inference(light_normalisation,[status(thm)],[c_610,c_3083]) ).
tcf(c_3135,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_143,X0) = select(queue_145,X0) ) ),
inference(superposition,[status(thm)],[c_3134,c_392]) ).
tcf(c_3136,plain,
select(queue_145,tail) = index_105,
inference(superposition,[status(thm)],[c_3134,c_391]) ).
tcf(c_3139,plain,
index_105 = index_147,
inference(demodulation,[status(thm)],[c_513,c_3136]) ).
tcf(c_3146,plain,
s(index_105) = index_150,
inference(demodulation,[status(thm)],[c_515,c_3139]) ).
tcf(c_3147,plain,
index_111 = index_150,
inference(light_normalisation,[status(thm)],[c_3146,c_2895]) ).
tcf(c_3149,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_145,X0) = select(queue_149,X0) ) ),
inference(superposition,[status(thm)],[c_611,c_392]) ).
tcf(c_3154,plain,
store(queue_149,tail,index_111) = queue_151,
inference(light_normalisation,[status(thm)],[c_612,c_3147]) ).
tcf(c_3155,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_149,X0) = select(queue_151,X0) ) ),
inference(superposition,[status(thm)],[c_3154,c_392]) ).
tcf(c_3156,plain,
select(queue_151,tail) = index_111,
inference(superposition,[status(thm)],[c_3154,c_391]) ).
tcf(c_3159,plain,
index_111 = index_153,
inference(demodulation,[status(thm)],[c_516,c_3156]) ).
tcf(c_3166,plain,
s(index_111) = index_156,
inference(demodulation,[status(thm)],[c_517,c_3159]) ).
tcf(c_3167,plain,
index_99 = index_156,
inference(light_normalisation,[status(thm)],[c_3166,c_2907]) ).
tcf(c_3190,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_151,X0) = select(queue_155,X0) ) ),
inference(superposition,[status(thm)],[c_613,c_392]) ).
tcf(c_3195,plain,
store(queue_155,tail,index_99) = queue_157,
inference(light_normalisation,[status(thm)],[c_614,c_3167]) ).
tcf(c_3196,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_155,X0) = select(queue_157,X0) ) ),
inference(superposition,[status(thm)],[c_3195,c_392]) ).
tcf(c_3197,plain,
select(queue_157,tail) = index_99,
inference(superposition,[status(thm)],[c_3195,c_391]) ).
tcf(c_3200,plain,
index_99 = index_159,
inference(demodulation,[status(thm)],[c_518,c_3197]) ).
tcf(c_3207,plain,
s(index_99) = index_162,
inference(demodulation,[status(thm)],[c_519,c_3200]) ).
tcf(c_3208,plain,
index_105 = index_162,
inference(light_normalisation,[status(thm)],[c_3207,c_2877]) ).
tcf(c_3210,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_157,X0) = select(queue_161,X0) ) ),
inference(superposition,[status(thm)],[c_615,c_392]) ).
tcf(c_3215,plain,
store(queue_161,tail,index_105) = queue_163,
inference(light_normalisation,[status(thm)],[c_616,c_3208]) ).
tcf(c_3216,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_161,X0) = select(queue_163,X0) ) ),
inference(superposition,[status(thm)],[c_3215,c_392]) ).
tcf(c_3217,plain,
select(queue_163,tail) = index_105,
inference(superposition,[status(thm)],[c_3215,c_391]) ).
tcf(c_3220,plain,
index_105 = index_165,
inference(demodulation,[status(thm)],[c_520,c_3217]) ).
tcf(c_3227,plain,
s(index_105) = index_168,
inference(demodulation,[status(thm)],[c_521,c_3220]) ).
tcf(c_3228,plain,
index_111 = index_168,
inference(light_normalisation,[status(thm)],[c_3227,c_2895]) ).
tcf(c_3245,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_163,X0) = select(queue_167,X0) ) ),
inference(superposition,[status(thm)],[c_617,c_392]) ).
tcf(c_3250,plain,
store(queue_167,tail,index_111) = queue_169,
inference(light_normalisation,[status(thm)],[c_618,c_3228]) ).
tcf(c_3251,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_167,X0) = select(queue_169,X0) ) ),
inference(superposition,[status(thm)],[c_3250,c_392]) ).
tcf(c_3252,plain,
select(queue_169,tail) = index_111,
inference(superposition,[status(thm)],[c_3250,c_391]) ).
tcf(c_3255,plain,
index_111 = index_171,
inference(demodulation,[status(thm)],[c_522,c_3252]) ).
tcf(c_3262,plain,
s(index_111) = index_174,
inference(demodulation,[status(thm)],[c_523,c_3255]) ).
tcf(c_3263,plain,
index_99 = index_174,
inference(light_normalisation,[status(thm)],[c_3262,c_2907]) ).
tcf(c_3265,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_13,X0) = select(queue_17,X0) ) ),
inference(superposition,[status(thm)],[c_619,c_392]) ).
tcf(c_3270,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_169,X0) = select(queue_173,X0) ) ),
inference(superposition,[status(thm)],[c_620,c_392]) ).
tcf(c_3289,plain,
store(queue_173,tail,index_99) = queue_175,
inference(light_normalisation,[status(thm)],[c_621,c_3263]) ).
tcf(c_3290,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_173,X0) = select(queue_175,X0) ) ),
inference(superposition,[status(thm)],[c_3289,c_392]) ).
tcf(c_3291,plain,
select(queue_175,tail) = index_99,
inference(superposition,[status(thm)],[c_3289,c_391]) ).
tcf(c_3294,plain,
index_99 = index_177,
inference(demodulation,[status(thm)],[c_524,c_3291]) ).
tcf(c_3301,plain,
s(index_99) = index_180,
inference(demodulation,[status(thm)],[c_526,c_3294]) ).
tcf(c_3302,plain,
index_105 = index_180,
inference(light_normalisation,[status(thm)],[c_3301,c_2877]) ).
tcf(c_3304,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_175,X0) = select(queue_179,X0) ) ),
inference(superposition,[status(thm)],[c_622,c_392]) ).
tcf(c_3309,plain,
store(queue_179,tail,index_105) = queue_181,
inference(light_normalisation,[status(thm)],[c_623,c_3302]) ).
tcf(c_3310,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_179,X0) = select(queue_181,X0) ) ),
inference(superposition,[status(thm)],[c_3309,c_392]) ).
tcf(c_3311,plain,
select(queue_181,tail) = index_105,
inference(superposition,[status(thm)],[c_3309,c_391]) ).
tcf(c_3314,plain,
index_105 = index_183,
inference(demodulation,[status(thm)],[c_527,c_3311]) ).
tcf(c_3321,plain,
s(index_105) = index_186,
inference(demodulation,[status(thm)],[c_528,c_3314]) ).
tcf(c_3322,plain,
index_111 = index_186,
inference(light_normalisation,[status(thm)],[c_3321,c_2895]) ).
tcf(c_3324,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_181,X0) = select(queue_185,X0) ) ),
inference(superposition,[status(thm)],[c_624,c_392]) ).
tcf(c_3342,plain,
store(queue_185,tail,index_111) = queue_187,
inference(light_normalisation,[status(thm)],[c_625,c_3322]) ).
tcf(c_3343,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_185,X0) = select(queue_187,X0) ) ),
inference(superposition,[status(thm)],[c_3342,c_392]) ).
tcf(c_3344,plain,
select(queue_187,tail) = index_111,
inference(superposition,[status(thm)],[c_3342,c_391]) ).
tcf(c_3347,plain,
index_111 = index_189,
inference(demodulation,[status(thm)],[c_529,c_3344]) ).
tcf(c_3354,plain,
s(index_111) = index_192,
inference(demodulation,[status(thm)],[c_530,c_3347]) ).
tcf(c_3355,plain,
index_99 = index_192,
inference(light_normalisation,[status(thm)],[c_3354,c_2907]) ).
tcf(c_3357,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_17,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_626,c_392]) ).
tcf(c_3358,plain,
select(queue_19,tail) = index_18,
inference(superposition,[status(thm)],[c_626,c_391]) ).
tcf(c_3359,plain,
index_21 = index_18,
inference(light_normalisation,[status(thm)],[c_3358,c_536]) ).
tcf(c_3365,plain,
s(index_21) = index_9,
inference(demodulation,[status(thm)],[c_3046,c_3359]) ).
tcf(c_3367,plain,
p(index_21) = index_15,
inference(demodulation,[status(thm)],[c_1941,c_3359]) ).
tcf(c_3371,plain,
index_9 = index_24,
inference(demodulation,[status(thm)],[c_547,c_3365]) ).
tcf(c_3373,plain,
p(index_9) = index_21,
inference(demodulation,[status(thm)],[c_1952,c_3371]) ).
tcf(c_3374,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_187,X0) = select(queue_191,X0) ) ),
inference(superposition,[status(thm)],[c_627,c_392]) ).
tcf(c_3379,plain,
store(queue_191,tail,index_99) = queue_193,
inference(light_normalisation,[status(thm)],[c_628,c_3355]) ).
tcf(c_3380,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_191,X0) = select(queue_193,X0) ) ),
inference(superposition,[status(thm)],[c_3379,c_392]) ).
tcf(c_3381,plain,
select(queue_193,tail) = index_99,
inference(superposition,[status(thm)],[c_3379,c_391]) ).
tcf(c_3384,plain,
index_99 = index_195,
inference(demodulation,[status(thm)],[c_531,c_3381]) ).
tcf(c_3391,plain,
s(index_99) = index_198,
inference(demodulation,[status(thm)],[c_532,c_3384]) ).
tcf(c_3392,plain,
index_105 = index_198,
inference(light_normalisation,[status(thm)],[c_3391,c_2877]) ).
tcf(c_3416,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_193,X0) = select(queue_197,X0) ) ),
inference(superposition,[status(thm)],[c_629,c_392]) ).
tcf(c_3421,plain,
store(queue_197,tail,index_105) = queue_199,
inference(light_normalisation,[status(thm)],[c_630,c_3392]) ).
tcf(c_3422,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_197,X0) = select(queue_199,X0) ) ),
inference(superposition,[status(thm)],[c_3421,c_392]) ).
tcf(c_3423,plain,
select(queue_199,tail) = index_105,
inference(superposition,[status(thm)],[c_3421,c_391]) ).
tcf(c_3426,plain,
index_105 = index_207,
inference(demodulation,[status(thm)],[c_535,c_3423]) ).
tcf(c_3433,plain,
s(index_105) = index_210,
inference(demodulation,[status(thm)],[c_537,c_3426]) ).
tcf(c_3434,plain,
index_111 = index_210,
inference(light_normalisation,[status(thm)],[c_3433,c_2895]) ).
tcf(c_3436,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_139,X0) = select(queue_203,X0) ) ),
inference(superposition,[status(thm)],[c_631,c_392]) ).
tcf(c_3441,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_203,X0) = select(queue_205,X0) ) ),
inference(superposition,[status(thm)],[c_632,c_392]) ).
tcf(c_3442,plain,
select(queue_205,tail) = index_204,
inference(superposition,[status(thm)],[c_632,c_391]) ).
tcf(c_3443,plain,
index_249 = index_204,
inference(light_normalisation,[status(thm)],[c_3442,c_551]) ).
tcf(c_3449,plain,
s(index_249) = index_135,
inference(demodulation,[status(thm)],[c_3101,c_3443]) ).
tcf(c_3452,plain,
s(index_201) = index_249,
inference(demodulation,[status(thm)],[c_534,c_3443]) ).
tcf(c_3455,plain,
index_135 = index_252,
inference(demodulation,[status(thm)],[c_552,c_3449]) ).
tcf(c_3457,plain,
p(index_135) = index_249,
inference(demodulation,[status(thm)],[c_1955,c_3455]) ).
tcf(c_3474,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_199,X0) = select(queue_209,X0) ) ),
inference(superposition,[status(thm)],[c_633,c_392]) ).
tcf(c_3479,plain,
store(queue_209,tail,index_111) = queue_211,
inference(light_normalisation,[status(thm)],[c_634,c_3434]) ).
tcf(c_3480,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_209,X0) = select(queue_211,X0) ) ),
inference(superposition,[status(thm)],[c_3479,c_392]) ).
tcf(c_3481,plain,
select(queue_211,tail) = index_111,
inference(superposition,[status(thm)],[c_3479,c_391]) ).
tcf(c_3484,plain,
index_111 = index_213,
inference(demodulation,[status(thm)],[c_538,c_3481]) ).
tcf(c_3491,plain,
s(index_111) = index_216,
inference(demodulation,[status(thm)],[c_539,c_3484]) ).
tcf(c_3492,plain,
index_99 = index_216,
inference(light_normalisation,[status(thm)],[c_3491,c_2907]) ).
tcf(c_3494,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_211,X0) = select(queue_215,X0) ) ),
inference(superposition,[status(thm)],[c_635,c_392]) ).
tcf(c_3499,plain,
store(queue_215,tail,index_99) = queue_217,
inference(light_normalisation,[status(thm)],[c_636,c_3492]) ).
tcf(c_3500,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_215,X0) = select(queue_217,X0) ) ),
inference(superposition,[status(thm)],[c_3499,c_392]) ).
tcf(c_3501,plain,
select(queue_217,tail) = index_99,
inference(superposition,[status(thm)],[c_3499,c_391]) ).
tcf(c_3504,plain,
index_99 = index_219,
inference(demodulation,[status(thm)],[c_540,c_3501]) ).
tcf(c_3511,plain,
s(index_99) = index_222,
inference(demodulation,[status(thm)],[c_541,c_3504]) ).
tcf(c_3512,plain,
index_105 = index_222,
inference(light_normalisation,[status(thm)],[c_3511,c_2877]) ).
tcf(c_3536,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_217,X0) = select(queue_221,X0) ) ),
inference(superposition,[status(thm)],[c_637,c_392]) ).
tcf(c_3541,plain,
store(queue_221,tail,index_105) = queue_223,
inference(light_normalisation,[status(thm)],[c_638,c_3512]) ).
tcf(c_3542,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_221,X0) = select(queue_223,X0) ) ),
inference(superposition,[status(thm)],[c_3541,c_392]) ).
tcf(c_3543,plain,
select(queue_223,tail) = index_105,
inference(superposition,[status(thm)],[c_3541,c_391]) ).
tcf(c_3546,plain,
index_105 = index_225,
inference(demodulation,[status(thm)],[c_542,c_3543]) ).
tcf(c_3553,plain,
s(index_105) = index_228,
inference(demodulation,[status(thm)],[c_543,c_3546]) ).
tcf(c_3554,plain,
index_111 = index_228,
inference(light_normalisation,[status(thm)],[c_3553,c_2895]) ).
tcf(c_3556,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_223,X0) = select(queue_227,X0) ) ),
inference(superposition,[status(thm)],[c_639,c_392]) ).
tcf(c_3561,plain,
store(queue_227,tail,index_111) = queue_229,
inference(light_normalisation,[status(thm)],[c_640,c_3554]) ).
tcf(c_3562,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_227,X0) = select(queue_229,X0) ) ),
inference(superposition,[status(thm)],[c_3561,c_392]) ).
tcf(c_3563,plain,
select(queue_229,tail) = index_111,
inference(superposition,[status(thm)],[c_3561,c_391]) ).
tcf(c_3566,plain,
index_111 = index_231,
inference(demodulation,[status(thm)],[c_544,c_3563]) ).
tcf(c_3573,plain,
s(index_111) = index_234,
inference(demodulation,[status(thm)],[c_545,c_3566]) ).
tcf(c_3574,plain,
index_99 = index_234,
inference(light_normalisation,[status(thm)],[c_3573,c_2907]) ).
tcf(c_3594,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_19,X0) = select(queue_23,X0) ) ),
inference(superposition,[status(thm)],[c_641,c_392]) ).
tcf(c_3599,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_229,X0) = select(queue_233,X0) ) ),
inference(superposition,[status(thm)],[c_642,c_392]) ).
tcf(c_3604,plain,
store(queue_233,tail,index_99) = queue_235,
inference(light_normalisation,[status(thm)],[c_643,c_3574]) ).
tcf(c_3605,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_233,X0) = select(queue_235,X0) ) ),
inference(superposition,[status(thm)],[c_3604,c_392]) ).
tcf(c_3606,plain,
select(queue_235,tail) = index_99,
inference(superposition,[status(thm)],[c_3604,c_391]) ).
tcf(c_3609,plain,
index_99 = index_237,
inference(demodulation,[status(thm)],[c_546,c_3606]) ).
tcf(c_3616,plain,
s(index_99) = index_240,
inference(demodulation,[status(thm)],[c_548,c_3609]) ).
tcf(c_3617,plain,
index_105 = index_240,
inference(light_normalisation,[status(thm)],[c_3616,c_2877]) ).
tcf(c_3619,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_235,X0) = select(queue_239,X0) ) ),
inference(superposition,[status(thm)],[c_644,c_392]) ).
tcf(c_3639,plain,
store(queue_239,tail,index_105) = queue_241,
inference(light_normalisation,[status(thm)],[c_645,c_3617]) ).
tcf(c_3640,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_239,X0) = select(queue_241,X0) ) ),
inference(superposition,[status(thm)],[c_3639,c_392]) ).
tcf(c_3641,plain,
select(queue_241,tail) = index_105,
inference(superposition,[status(thm)],[c_3639,c_391]) ).
tcf(c_3644,plain,
index_105 = index_243,
inference(demodulation,[status(thm)],[c_549,c_3641]) ).
tcf(c_3651,plain,
s(index_105) = index_246,
inference(demodulation,[status(thm)],[c_550,c_3644]) ).
tcf(c_3652,plain,
index_111 = index_246,
inference(light_normalisation,[status(thm)],[c_3651,c_2895]) ).
tcf(c_3654,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_241,X0) = select(queue_245,X0) ) ),
inference(superposition,[status(thm)],[c_646,c_392]) ).
tcf(c_3659,plain,
store(queue_245,tail,index_111) = queue_247,
inference(light_normalisation,[status(thm)],[c_647,c_3652]) ).
tcf(c_3660,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_245,X0) = select(queue_247,X0) ) ),
inference(superposition,[status(thm)],[c_3659,c_392]) ).
tcf(c_3661,plain,
select(queue_247,tail) = index_111,
inference(superposition,[status(thm)],[c_3659,c_391]) ).
tcf(c_3664,plain,
index_111 = index_281,
inference(demodulation,[status(thm)],[c_563,c_3661]) ).
tcf(c_3668,plain,
p(index_111) = index_282,
inference(demodulation,[status(thm)],[c_1960,c_3664]) ).
tcf(c_3670,plain,
index_105 = index_282,
inference(light_normalisation,[status(thm)],[c_3668,c_2894]) ).
tcf(c_3671,plain,
select(earray_278,index_105) = elem_283,
inference(demodulation,[status(thm)],[c_495,c_3670]) ).
tcf(c_3674,plain,
store(queue_23,tail,index_9) = queue_25,
inference(light_normalisation,[status(thm)],[c_648,c_3371]) ).
tcf(c_3675,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_23,X0) = select(queue_25,X0) ) ),
inference(superposition,[status(thm)],[c_3674,c_392]) ).
tcf(c_3676,plain,
select(queue_25,tail) = index_9,
inference(superposition,[status(thm)],[c_3674,c_391]) ).
tcf(c_3679,plain,
index_9 = index_27,
inference(demodulation,[status(thm)],[c_558,c_3676]) ).
tcf(c_3686,plain,
s(index_9) = index_30,
inference(demodulation,[status(thm)],[c_566,c_3679]) ).
tcf(c_3687,plain,
index_15 = index_30,
inference(light_normalisation,[status(thm)],[c_3686,c_3045]) ).
tcf(c_3695,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_205,X0) = select(queue_251,X0) ) ),
inference(superposition,[status(thm)],[c_649,c_392]) ).
tcf(c_3700,plain,
store(queue_251,tail,index_135) = queue_253,
inference(light_normalisation,[status(thm)],[c_650,c_3455]) ).
tcf(c_3701,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_251,X0) = select(queue_253,X0) ) ),
inference(superposition,[status(thm)],[c_3700,c_392]) ).
tcf(c_3702,plain,
select(queue_253,tail) = index_135,
inference(superposition,[status(thm)],[c_3700,c_391]) ).
tcf(c_3705,plain,
index_135 = index_255,
inference(demodulation,[status(thm)],[c_553,c_3702]) ).
tcf(c_3712,plain,
s(index_135) = index_258,
inference(demodulation,[status(thm)],[c_554,c_3705]) ).
tcf(c_3713,plain,
index_201 = index_258,
inference(light_normalisation,[status(thm)],[c_3712,c_3100]) ).
tcf(c_3715,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_253,X0) = select(queue_257,X0) ) ),
inference(superposition,[status(thm)],[c_651,c_392]) ).
tcf(c_3720,plain,
store(queue_257,tail,index_201) = queue_259,
inference(light_normalisation,[status(thm)],[c_652,c_3713]) ).
tcf(c_3721,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_257,X0) = select(queue_259,X0) ) ),
inference(superposition,[status(thm)],[c_3720,c_392]) ).
tcf(c_3722,plain,
select(queue_259,tail) = index_201,
inference(superposition,[status(thm)],[c_3720,c_391]) ).
tcf(c_3725,plain,
index_201 = index_261,
inference(demodulation,[status(thm)],[c_555,c_3722]) ).
tcf(c_3732,plain,
s(index_201) = index_264,
inference(demodulation,[status(thm)],[c_556,c_3725]) ).
tcf(c_3733,plain,
index_249 = index_264,
inference(light_normalisation,[status(thm)],[c_3732,c_3452]) ).
tcf(c_3750,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_259,X0) = select(queue_263,X0) ) ),
inference(superposition,[status(thm)],[c_653,c_392]) ).
tcf(c_3755,plain,
store(queue_263,tail,index_249) = queue_265,
inference(light_normalisation,[status(thm)],[c_654,c_3733]) ).
tcf(c_3756,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_263,X0) = select(queue_265,X0) ) ),
inference(superposition,[status(thm)],[c_3755,c_392]) ).
tcf(c_3757,plain,
select(queue_265,tail) = index_249,
inference(superposition,[status(thm)],[c_3755,c_391]) ).
tcf(c_3760,plain,
index_249 = index_267,
inference(demodulation,[status(thm)],[c_557,c_3757]) ).
tcf(c_3767,plain,
s(index_249) = index_270,
inference(demodulation,[status(thm)],[c_559,c_3760]) ).
tcf(c_3768,plain,
index_135 = index_270,
inference(light_normalisation,[status(thm)],[c_3767,c_3449]) ).
tcf(c_3770,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_265,X0) = select(queue_269,X0) ) ),
inference(superposition,[status(thm)],[c_655,c_392]) ).
tcf(c_3775,plain,
store(queue_269,tail,index_135) = queue_271,
inference(light_normalisation,[status(thm)],[c_656,c_3768]) ).
tcf(c_3776,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_269,X0) = select(queue_271,X0) ) ),
inference(superposition,[status(thm)],[c_3775,c_392]) ).
tcf(c_3777,plain,
select(queue_271,tail) = index_135,
inference(superposition,[status(thm)],[c_3775,c_391]) ).
tcf(c_3780,plain,
index_135 = index_273,
inference(demodulation,[status(thm)],[c_560,c_3777]) ).
tcf(c_3787,plain,
s(index_135) = index_276,
inference(demodulation,[status(thm)],[c_561,c_3780]) ).
tcf(c_3788,plain,
index_201 = index_276,
inference(light_normalisation,[status(thm)],[c_3787,c_3100]) ).
tcf(c_3804,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_271,X0) = select(queue_275,X0) ) ),
inference(superposition,[status(thm)],[c_657,c_392]) ).
tcf(c_3809,plain,
store(queue_275,tail,index_201) = queue_277,
inference(light_normalisation,[status(thm)],[c_658,c_3788]) ).
tcf(c_3810,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_275,X0) = select(queue_277,X0) ) ),
inference(superposition,[status(thm)],[c_3809,c_392]) ).
tcf(c_3811,plain,
select(queue_277,tail) = index_201,
inference(superposition,[status(thm)],[c_3809,c_391]) ).
tcf(c_3812,plain,
index_9 = index_201,
inference(light_normalisation,[status(thm)],[c_3811,c_587]) ).
tcf(c_3826,plain,
p(index_9) = index_135,
inference(demodulation,[status(thm)],[c_3099,c_3812]) ).
tcf(c_3831,plain,
index_135 = index_21,
inference(demodulation,[status(thm)],[c_3373,c_3826]) ).
tcf(c_3835,plain,
p(index_135) = index_15,
inference(demodulation,[status(thm)],[c_3367,c_3831]) ).
tcf(c_3836,plain,
s(index_135) = index_9,
inference(demodulation,[status(thm)],[c_3365,c_3831]) ).
tcf(c_3841,plain,
index_15 = index_249,
inference(demodulation,[status(thm)],[c_3457,c_3835]) ).
tcf(c_3846,plain,
s(index_15) = index_135,
inference(demodulation,[status(thm)],[c_3449,c_3841]) ).
tcf(c_3855,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_25,X0) = select(queue_29,X0) ) ),
inference(superposition,[status(thm)],[c_659,c_392]) ).
tcf(c_3860,plain,
store(queue_29,tail,index_15) = queue_31,
inference(light_normalisation,[status(thm)],[c_660,c_3687]) ).
tcf(c_3861,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_29,X0) = select(queue_31,X0) ) ),
inference(superposition,[status(thm)],[c_3860,c_392]) ).
tcf(c_3862,plain,
select(queue_31,tail) = index_15,
inference(superposition,[status(thm)],[c_3860,c_391]) ).
tcf(c_3865,plain,
index_15 = index_33,
inference(demodulation,[status(thm)],[c_567,c_3862]) ).
tcf(c_3872,plain,
s(index_15) = index_36,
inference(demodulation,[status(thm)],[c_568,c_3865]) ).
tcf(c_3873,plain,
index_135 = index_36,
inference(light_normalisation,[status(thm)],[c_3872,c_3846]) ).
tcf(c_3882,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_31,X0) = select(queue_35,X0) ) ),
inference(superposition,[status(thm)],[c_661,c_392]) ).
tcf(c_3887,plain,
store(queue_35,tail,index_135) = queue_37,
inference(light_normalisation,[status(thm)],[c_662,c_3873]) ).
tcf(c_3888,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_35,X0) = select(queue_37,X0) ) ),
inference(superposition,[status(thm)],[c_3887,c_392]) ).
tcf(c_3889,plain,
select(queue_37,tail) = index_135,
inference(superposition,[status(thm)],[c_3887,c_391]) ).
tcf(c_3892,plain,
index_135 = index_39,
inference(demodulation,[status(thm)],[c_569,c_3889]) ).
tcf(c_3898,plain,
s(index_135) = index_42,
inference(demodulation,[status(thm)],[c_570,c_3892]) ).
tcf(c_3899,plain,
index_9 = index_42,
inference(light_normalisation,[status(thm)],[c_3898,c_3836]) ).
tcf(c_3901,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_37,X0) = select(queue_41,X0) ) ),
inference(superposition,[status(thm)],[c_663,c_392]) ).
tcf(c_3906,plain,
store(queue_41,tail,index_9) = queue_43,
inference(light_normalisation,[status(thm)],[c_664,c_3899]) ).
tcf(c_3907,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_41,X0) = select(queue_43,X0) ) ),
inference(superposition,[status(thm)],[c_3906,c_392]) ).
tcf(c_3908,plain,
select(queue_43,tail) = index_9,
inference(superposition,[status(thm)],[c_3906,c_391]) ).
tcf(c_3911,plain,
index_9 = index_45,
inference(demodulation,[status(thm)],[c_571,c_3908]) ).
tcf(c_3917,plain,
s(index_9) = index_48,
inference(demodulation,[status(thm)],[c_572,c_3911]) ).
tcf(c_3918,plain,
index_15 = index_48,
inference(light_normalisation,[status(thm)],[c_3917,c_3045]) ).
tcf(c_3941,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_43,X0) = select(queue_47,X0) ) ),
inference(superposition,[status(thm)],[c_665,c_392]) ).
tcf(c_3946,plain,
store(queue_47,tail,index_15) = queue_49,
inference(light_normalisation,[status(thm)],[c_666,c_3918]) ).
tcf(c_3947,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_47,X0) = select(queue_49,X0) ) ),
inference(superposition,[status(thm)],[c_3946,c_392]) ).
tcf(c_3948,plain,
select(queue_49,tail) = index_15,
inference(superposition,[status(thm)],[c_3946,c_391]) ).
tcf(c_3951,plain,
index_15 = index_51,
inference(demodulation,[status(thm)],[c_573,c_3948]) ).
tcf(c_3957,plain,
s(index_15) = index_54,
inference(demodulation,[status(thm)],[c_574,c_3951]) ).
tcf(c_3958,plain,
index_135 = index_54,
inference(light_normalisation,[status(thm)],[c_3957,c_3846]) ).
tcf(c_3960,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_1,X0) = select(queue_5,X0) ) ),
inference(superposition,[status(thm)],[c_667,c_392]) ).
tcf(c_3965,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_49,X0) = select(queue_53,X0) ) ),
inference(superposition,[status(thm)],[c_668,c_392]) ).
tcf(c_3990,plain,
store(queue_53,tail,index_135) = queue_55,
inference(light_normalisation,[status(thm)],[c_669,c_3958]) ).
tcf(c_3991,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_53,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_3990,c_392]) ).
tcf(c_3992,plain,
select(queue_55,tail) = index_135,
inference(superposition,[status(thm)],[c_3990,c_391]) ).
tcf(c_3995,plain,
index_135 = index_57,
inference(demodulation,[status(thm)],[c_575,c_3992]) ).
tcf(c_4001,plain,
s(index_135) = index_60,
inference(demodulation,[status(thm)],[c_577,c_3995]) ).
tcf(c_4002,plain,
index_9 = index_60,
inference(light_normalisation,[status(thm)],[c_4001,c_3836]) ).
tcf(c_4004,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_55,X0) = select(queue_59,X0) ) ),
inference(superposition,[status(thm)],[c_670,c_392]) ).
tcf(c_4009,plain,
store(queue_59,tail,index_9) = queue_61,
inference(light_normalisation,[status(thm)],[c_671,c_4002]) ).
tcf(c_4010,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_59,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_4009,c_392]) ).
tcf(c_4011,plain,
select(queue_61,tail) = index_9,
inference(superposition,[status(thm)],[c_4009,c_391]) ).
tcf(c_4014,plain,
index_9 = index_63,
inference(demodulation,[status(thm)],[c_578,c_4011]) ).
tcf(c_4020,plain,
s(index_9) = index_66,
inference(demodulation,[status(thm)],[c_579,c_4014]) ).
tcf(c_4021,plain,
index_15 = index_66,
inference(light_normalisation,[status(thm)],[c_4020,c_3045]) ).
tcf(c_4023,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_61,X0) = select(queue_65,X0) ) ),
inference(superposition,[status(thm)],[c_672,c_392]) ).
tcf(c_4043,plain,
store(queue_65,tail,index_15) = queue_67,
inference(light_normalisation,[status(thm)],[c_673,c_4021]) ).
tcf(c_4044,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_65,X0) = select(queue_67,X0) ) ),
inference(superposition,[status(thm)],[c_4043,c_392]) ).
tcf(c_4045,plain,
select(queue_67,tail) = index_15,
inference(superposition,[status(thm)],[c_4043,c_391]) ).
tcf(c_4048,plain,
index_15 = index_75,
inference(demodulation,[status(thm)],[c_582,c_4045]) ).
tcf(c_4054,plain,
s(index_15) = index_78,
inference(demodulation,[status(thm)],[c_583,c_4048]) ).
tcf(c_4055,plain,
index_135 = index_78,
inference(light_normalisation,[status(thm)],[c_4054,c_3846]) ).
tcf(c_4057,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_5,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_674,c_392]) ).
tcf(c_4058,plain,
select(queue_7,tail) = index_6,
inference(superposition,[status(thm)],[c_674,c_391]) ).
tcf(c_4059,plain,
index_69 = index_6,
inference(light_normalisation,[status(thm)],[c_4058,c_580]) ).
tcf(c_4066,plain,
p(index_69) = index_3,
inference(demodulation,[status(thm)],[c_1966,c_4059]) ).
tcf(c_4072,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_7,X0) = select(queue_71,X0) ) ),
inference(superposition,[status(thm)],[c_675,c_392]) ).
tcf(c_4077,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_71,X0) = select(queue_73,X0) ) ),
inference(superposition,[status(thm)],[c_676,c_392]) ).
tcf(c_4078,plain,
select(queue_73,tail) = index_72,
inference(superposition,[status(thm)],[c_676,c_391]) ).
tcf(c_4079,plain,
index_135 = index_72,
inference(light_normalisation,[status(thm)],[c_4078,c_509]) ).
tcf(c_4084,plain,
p(index_135) = index_69,
inference(demodulation,[status(thm)],[c_1969,c_4079]) ).
tcf(c_4086,plain,
index_15 = index_69,
inference(light_normalisation,[status(thm)],[c_4084,c_3835]) ).
tcf(c_4094,plain,
index_9 = index_3,
inference(light_normalisation,[status(thm)],[c_4066,c_3044,c_4086]) ).
tcf(c_4097,plain,
select(queue_1,tail) = index_9,
inference(demodulation,[status(thm)],[c_565,c_4094]) ).
tcf(c_4107,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_67,X0) = select(queue_77,X0) ) ),
inference(superposition,[status(thm)],[c_677,c_392]) ).
tcf(c_4112,plain,
store(queue_77,tail,index_135) = queue_79,
inference(light_normalisation,[status(thm)],[c_678,c_4055]) ).
tcf(c_4113,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_77,X0) = select(queue_79,X0) ) ),
inference(superposition,[status(thm)],[c_4112,c_392]) ).
tcf(c_4114,plain,
select(queue_79,tail) = index_135,
inference(superposition,[status(thm)],[c_4112,c_391]) ).
tcf(c_4117,plain,
index_135 = index_81,
inference(demodulation,[status(thm)],[c_584,c_4114]) ).
tcf(c_4123,plain,
s(index_135) = index_84,
inference(demodulation,[status(thm)],[c_585,c_4117]) ).
tcf(c_4124,plain,
index_9 = index_84,
inference(light_normalisation,[status(thm)],[c_4123,c_3836]) ).
tcf(c_4126,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_79,X0) = select(queue_83,X0) ) ),
inference(superposition,[status(thm)],[c_679,c_392]) ).
tcf(c_4131,plain,
store(queue_83,tail,index_9) = queue_85,
inference(light_normalisation,[status(thm)],[c_680,c_4124]) ).
tcf(c_4132,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_83,X0) = select(queue_85,X0) ) ),
inference(superposition,[status(thm)],[c_4131,c_392]) ).
tcf(c_4133,plain,
select(queue_85,tail) = index_9,
inference(superposition,[status(thm)],[c_4131,c_391]) ).
tcf(c_4136,plain,
index_9 = index_87,
inference(demodulation,[status(thm)],[c_586,c_4133]) ).
tcf(c_4142,plain,
s(index_9) = index_90,
inference(demodulation,[status(thm)],[c_588,c_4136]) ).
tcf(c_4143,plain,
index_15 = index_90,
inference(light_normalisation,[status(thm)],[c_4142,c_3045]) ).
tcf(c_4160,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_85,X0) = select(queue_89,X0) ) ),
inference(superposition,[status(thm)],[c_681,c_392]) ).
tcf(c_4165,plain,
store(queue_89,tail,index_15) = queue_91,
inference(light_normalisation,[status(thm)],[c_682,c_4143]) ).
tcf(c_4166,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_89,X0) = select(queue_91,X0) ) ),
inference(superposition,[status(thm)],[c_4165,c_392]) ).
tcf(c_4167,plain,
select(queue_91,tail) = index_15,
inference(superposition,[status(thm)],[c_4165,c_391]) ).
tcf(c_4170,plain,
index_15 = index_93,
inference(demodulation,[status(thm)],[c_589,c_4167]) ).
tcf(c_4176,plain,
s(index_15) = index_96,
inference(demodulation,[status(thm)],[c_590,c_4170]) ).
tcf(c_4177,plain,
index_135 = index_96,
inference(light_normalisation,[status(thm)],[c_4176,c_3846]) ).
tcf(c_4179,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_91,X0) = select(queue_95,X0) ) ),
inference(superposition,[status(thm)],[c_683,c_392]) ).
tcf(c_4184,plain,
store(queue_95,tail,index_135) = queue_97,
inference(light_normalisation,[status(thm)],[c_684,c_4177]) ).
tcf(c_4185,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_95,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_4184,c_392]) ).
tcf(c_4186,plain,
select(queue_97,tail) = index_135,
inference(superposition,[status(thm)],[c_4184,c_391]) ).
tcf(c_4187,plain,
index_99 = index_135,
inference(light_normalisation,[status(thm)],[c_4186,c_591]) ).
tcf(c_4202,plain,
p(index_99) = index_15,
inference(demodulation,[status(thm)],[c_3835,c_4187]) ).
tcf(c_4222,plain,
index_111 = index_15,
inference(light_normalisation,[status(thm)],[c_4202,c_2906]) ).
tcf(c_4243,plain,
p(index_111) = index_9,
inference(demodulation,[status(thm)],[c_3044,c_4222]) ).
tcf(c_4248,plain,
index_9 = index_105,
inference(demodulation,[status(thm)],[c_2894,c_4243]) ).
tcf(c_4251,plain,
select(earray_278,index_9) = elem_283,
inference(demodulation,[status(thm)],[c_3671,c_4248]) ).
tcf(c_4801,plain,
( ( head = tail )
| ( select(queue_1,tail) = index_0 ) ),
inference(superposition,[status(thm)],[c_496,c_2803]) ).
tcf(c_4803,plain,
( ( index_9 = index_0 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_4801,c_4097]) ).
tcf(c_4804,plain,
index_9 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[c_4803,c_393]) ).
tcf(c_4805,plain,
select(queue_1,head) = index_9,
inference(demodulation,[status(thm)],[c_2804,c_4804]) ).
tcf(c_4824,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_2867,c_2862]) ).
tcf(c_4850,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_109,X0) ) ),
inference(superposition,[status(thm)],[c_2887,c_2882]) ).
tcf(c_4881,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_109,X0) = select(queue_115,X0) ) ),
inference(superposition,[status(thm)],[c_2936,c_2930]) ).
tcf(c_4915,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_115,X0) = select(queue_121,X0) ) ),
inference(superposition,[status(thm)],[c_2993,c_2954]) ).
tcf(c_4946,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_121,X0) = select(queue_127,X0) ) ),
inference(superposition,[status(thm)],[c_3017,c_3011]) ).
tcf(c_4970,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_277,X0) ) ),
inference(superposition,[status(thm)],[c_3035,c_2925]) ).
tcf(c_4998,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_127,X0) = select(queue_133,X0) ) ),
inference(superposition,[status(thm)],[c_3071,c_3065]) ).
tcf(c_5025,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_139,X0) = select(queue_73,X0) ) ),
inference(superposition,[status(thm)],[c_3090,c_3085]) ).
tcf(c_5046,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_133,X0) = select(queue_145,X0) ) ),
inference(superposition,[status(thm)],[c_3135,c_3129]) ).
tcf(c_5067,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_145,X0) = select(queue_151,X0) ) ),
inference(superposition,[status(thm)],[c_3155,c_3149]) ).
tcf(c_5104,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_151,X0) = select(queue_157,X0) ) ),
inference(superposition,[status(thm)],[c_3196,c_3190]) ).
tcf(c_5129,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_157,X0) = select(queue_163,X0) ) ),
inference(superposition,[status(thm)],[c_3216,c_3210]) ).
tcf(c_5150,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_163,X0) = select(queue_169,X0) ) ),
inference(superposition,[status(thm)],[c_3251,c_3245]) ).
tcf(c_5190,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_169,X0) = select(queue_175,X0) ) ),
inference(superposition,[status(thm)],[c_3290,c_3270]) ).
tcf(c_5217,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_175,X0) = select(queue_181,X0) ) ),
inference(superposition,[status(thm)],[c_3310,c_3304]) ).
tcf(c_5238,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_181,X0) = select(queue_187,X0) ) ),
inference(superposition,[status(thm)],[c_3343,c_3324]) ).
tcf(c_5257,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_3357,c_3265]) ).
tcf(c_5290,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_187,X0) = select(queue_193,X0) ) ),
inference(superposition,[status(thm)],[c_3380,c_3374]) ).
tcf(c_5315,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_193,X0) = select(queue_199,X0) ) ),
inference(superposition,[status(thm)],[c_3422,c_3416]) ).
tcf(c_5336,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_139,X0) = select(queue_205,X0) ) ),
inference(superposition,[status(thm)],[c_3441,c_3436]) ).
tcf(c_5370,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_199,X0) = select(queue_211,X0) ) ),
inference(superposition,[status(thm)],[c_3480,c_3474]) ).
tcf(c_5397,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_211,X0) = select(queue_217,X0) ) ),
inference(superposition,[status(thm)],[c_3500,c_3494]) ).
tcf(c_5422,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_217,X0) = select(queue_223,X0) ) ),
inference(superposition,[status(thm)],[c_3542,c_3536]) ).
tcf(c_5450,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_223,X0) = select(queue_229,X0) ) ),
inference(superposition,[status(thm)],[c_3562,c_3556]) ).
tcf(c_5483,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_229,X0) = select(queue_235,X0) ) ),
inference(superposition,[status(thm)],[c_3605,c_3599]) ).
tcf(c_5508,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_235,X0) = select(queue_241,X0) ) ),
inference(superposition,[status(thm)],[c_3640,c_3619]) ).
tcf(c_5533,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_241,X0) = select(queue_247,X0) ) ),
inference(superposition,[status(thm)],[c_3660,c_3654]) ).
tcf(c_5568,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_19,X0) = select(queue_25,X0) ) ),
inference(superposition,[status(thm)],[c_3675,c_3594]) ).
tcf(c_5597,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_205,X0) = select(queue_253,X0) ) ),
inference(superposition,[status(thm)],[c_3701,c_3695]) ).
tcf(c_5623,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_253,X0) = select(queue_259,X0) ) ),
inference(superposition,[status(thm)],[c_3721,c_3715]) ).
tcf(c_5658,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_259,X0) = select(queue_265,X0) ) ),
inference(superposition,[status(thm)],[c_3756,c_3750]) ).
tcf(c_5687,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_265,X0) = select(queue_271,X0) ) ),
inference(superposition,[status(thm)],[c_3776,c_3770]) ).
tcf(c_5716,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_271,X0) = select(queue_277,X0) ) ),
inference(superposition,[status(thm)],[c_3810,c_3804]) ).
tcf(c_5762,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_25,X0) = select(queue_31,X0) ) ),
inference(superposition,[status(thm)],[c_3861,c_3855]) ).
tcf(c_5795,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_31,X0) = select(queue_37,X0) ) ),
inference(superposition,[status(thm)],[c_3888,c_3882]) ).
tcf(c_5820,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_37,X0) = select(queue_43,X0) ) ),
inference(superposition,[status(thm)],[c_3907,c_3901]) ).
tcf(c_5855,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_43,X0) = select(queue_49,X0) ) ),
inference(superposition,[status(thm)],[c_3947,c_3941]) ).
tcf(c_5892,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_49,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_3991,c_3965]) ).
tcf(c_5917,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_55,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_4010,c_4004]) ).
tcf(c_5950,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_61,X0) = select(queue_67,X0) ) ),
inference(superposition,[status(thm)],[c_4044,c_4023]) ).
tcf(c_5974,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_1,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_4057,c_3960]) ).
tcf(c_5999,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_7,X0) = select(queue_73,X0) ) ),
inference(superposition,[status(thm)],[c_4077,c_4072]) ).
tcf(c_6021,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_67,X0) = select(queue_79,X0) ) ),
inference(superposition,[status(thm)],[c_4113,c_4107]) ).
tcf(c_6063,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_79,X0) = select(queue_85,X0) ) ),
inference(superposition,[status(thm)],[c_4132,c_4126]) ).
tcf(c_6088,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_85,X0) = select(queue_91,X0) ) ),
inference(superposition,[status(thm)],[c_4166,c_4160]) ).
tcf(c_6113,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_91,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_4185,c_4179]) ).
tcf(c_6773,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_241,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5533,c_562]) ).
tcf(c_6775,plain,
select(queue_241,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6773,c_394,c_393]) ).
tcf(c_6776,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_235,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5508,c_6775]) ).
tcf(c_6778,plain,
select(queue_235,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6776,c_394,c_393]) ).
tcf(c_6779,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_229,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5483,c_6778]) ).
tcf(c_6781,plain,
select(queue_229,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6779,c_394,c_393]) ).
tcf(c_6802,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_223,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5450,c_6781]) ).
tcf(c_6804,plain,
select(queue_223,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6802,c_394,c_393]) ).
tcf(c_6805,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_217,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5422,c_6804]) ).
tcf(c_6807,plain,
select(queue_217,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6805,c_394,c_393]) ).
tcf(c_6808,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_211,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5397,c_6807]) ).
tcf(c_6810,plain,
select(queue_211,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6808,c_394,c_393]) ).
tcf(c_6811,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_199,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5370,c_6810]) ).
tcf(c_6813,plain,
select(queue_199,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6811,c_394,c_393]) ).
tcf(c_6814,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_193,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5315,c_6813]) ).
tcf(c_6816,plain,
select(queue_193,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6814,c_394,c_393]) ).
tcf(c_6817,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_187,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5290,c_6816]) ).
tcf(c_6819,plain,
select(queue_187,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6817,c_394,c_393]) ).
tcf(c_6820,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_181,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5238,c_6819]) ).
tcf(c_6822,plain,
select(queue_181,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6820,c_394,c_393]) ).
tcf(c_6827,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_175,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5217,c_6822]) ).
tcf(c_6829,plain,
select(queue_175,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6827,c_394,c_393]) ).
tcf(c_6830,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_169,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5190,c_6829]) ).
tcf(c_6832,plain,
select(queue_169,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6830,c_394,c_393]) ).
tcf(c_6833,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_163,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5150,c_6832]) ).
tcf(c_6835,plain,
select(queue_163,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6833,c_394,c_393]) ).
tcf(c_6840,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_157,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5129,c_6835]) ).
tcf(c_6842,plain,
select(queue_157,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6840,c_394,c_393]) ).
tcf(c_6843,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_151,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5104,c_6842]) ).
tcf(c_6845,plain,
select(queue_151,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6843,c_394,c_393]) ).
tcf(c_6891,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_271,X0) ) ),
inference(superposition,[status(thm)],[c_5716,c_4970]) ).
tcf(c_6905,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_145,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5067,c_6845]) ).
tcf(c_6907,plain,
select(queue_145,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6905,c_394,c_393]) ).
tcf(c_6908,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_133,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_5046,c_6907]) ).
tcf(c_6910,plain,
select(queue_133,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6908,c_394,c_393]) ).
tcf(c_6911,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_127,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_4998,c_6910]) ).
tcf(c_6913,plain,
select(queue_127,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6911,c_394,c_393]) ).
tcf(c_6918,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_121,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_4946,c_6913]) ).
tcf(c_6920,plain,
select(queue_121,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6918,c_394,c_393]) ).
tcf(c_6921,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_115,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_4915,c_6920]) ).
tcf(c_6923,plain,
select(queue_115,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6921,c_394,c_393]) ).
tcf(c_6924,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_109,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_4881,c_6923]) ).
tcf(c_6926,plain,
select(queue_109,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6924,c_394,c_393]) ).
tcf(c_6931,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_103,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_4850,c_6926]) ).
tcf(c_6933,plain,
select(queue_103,head) = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_6931,c_394,c_393]) ).
tcf(c_7015,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_139,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_5999,c_5025]) ).
tcf(c_7064,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_91,X0) ) ),
inference(superposition,[status(thm)],[c_6113,c_4824]) ).
tcf(c_7145,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_265,X0) ) ),
inference(superposition,[status(thm)],[c_6891,c_5687]) ).
tcf(c_7160,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_1,X0) = select(queue_139,X0) ) ),
inference(superposition,[status(thm)],[c_7015,c_5974]) ).
tcf(c_7175,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_85,X0) ) ),
inference(superposition,[status(thm)],[c_7064,c_6088]) ).
tcf(c_7228,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_259,X0) ) ),
inference(superposition,[status(thm)],[c_7145,c_5658]) ).
tcf(c_7257,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_79,X0) ) ),
inference(superposition,[status(thm)],[c_7175,c_6063]) ).
tcf(c_7272,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_253,X0) ) ),
inference(superposition,[status(thm)],[c_7228,c_5623]) ).
tcf(c_7287,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_67,X0) ) ),
inference(superposition,[status(thm)],[c_7257,c_6021]) ).
tcf(c_7306,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_205,X0) ) ),
inference(superposition,[status(thm)],[c_7272,c_5597]) ).
tcf(c_7321,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_7287,c_5950]) ).
tcf(c_7336,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_139,X0) ) ),
inference(superposition,[status(thm)],[c_7306,c_5336]) ).
tcf(c_7355,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_7321,c_5917]) ).
tcf(c_7370,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_1,X0) = select(queue_13,X0) ) ),
inference(superposition,[status(thm)],[c_7336,c_7160]) ).
tcf(c_7385,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_49,X0) ) ),
inference(superposition,[status(thm)],[c_7355,c_5892]) ).
tcf(c_7414,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_43,X0) ) ),
inference(superposition,[status(thm)],[c_7385,c_5855]) ).
tcf(c_7429,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_37,X0) ) ),
inference(superposition,[status(thm)],[c_7414,c_5820]) ).
tcf(c_7482,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_31,X0) ) ),
inference(superposition,[status(thm)],[c_7429,c_5795]) ).
tcf(c_7497,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_25,X0) ) ),
inference(superposition,[status(thm)],[c_7482,c_5762]) ).
tcf(c_7569,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_7497,c_5568]) ).
tcf(c_7584,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_13,X0) ) ),
inference(superposition,[status(thm)],[c_7569,c_5257]) ).
tcf(c_7599,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_1,X0) = select(queue_103,X0) ) ),
inference(superposition,[status(thm)],[c_7584,c_7370]) ).
tcf(c_7614,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_1,head) = index_279 ) ),
inference(superposition,[status(thm)],[c_7599,c_6933]) ).
tcf(c_7615,plain,
( ( index_9 = index_279 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_7614,c_4805]) ).
tcf(c_7616,plain,
index_9 = index_279,
inference(forward_subsumption_resolution,[status(thm)],[c_7615,c_394,c_393]) ).
tcf(c_7640,plain,
select(earray_278,index_9) = elem_280,
inference(demodulation,[status(thm)],[c_494,c_7616]) ).
tcf(c_7641,plain,
elem_280 = elem_283,
inference(demodulation,[status(thm)],[c_4251,c_7640]) ).
tcf(c_7642,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_7641,c_1293]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 20:38:21 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 6.09/1.78 % SZS status Started for theBenchmark.p
% 6.09/1.78 % SZS status Unsatisfiable for theBenchmark.p
% 6.09/1.78
% 6.09/1.78 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.09/1.78
% 6.09/1.78 % ------ iProver source info
% 6.09/1.78
% 6.09/1.78 % git: date: 2026-07-19 20:42:38 +0200
% 6.09/1.78 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.09/1.78 % git: non_committed_changes: false
% 6.09/1.78
% 6.09/1.78 % ------ Parsing...% successful
% 6.09/1.78
% 6.09/1.78
% 6.09/1.78 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.09/1.78
% 6.09/1.78 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.09/1.78
% 6.09/1.78 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.09/1.78
% 6.09/1.78 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.09/1.78 % ------ Proving...
% 6.09/1.78 % ------ Problem Properties
% 6.09/1.78
% 6.09/1.78 %
% 6.09/1.78 % clauses 295
% 6.09/1.78 % conjectures 1
% 6.09/1.78 % EPR 4
% 6.09/1.78 % Horn 294
% 6.09/1.78 % unary 294
% 6.09/1.78 % binary 1
% 6.09/1.78 % lits 296
% 6.09/1.78 % lits eq 296
% 6.09/1.78 % fd_pure 0
% 6.09/1.78 % fd_pseudo 0
% 6.09/1.78 % fd_cond 0
% 6.09/1.78 % fd_pseudo_cond 1
% 6.09/1.78 % AC symbols 0
% 6.09/1.78
% 6.09/1.78 % ------ Schedule dynamic 5 is on
% 6.09/1.78
% 6.09/1.78 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.09/1.78
% 6.09/1.78
% 6.09/1.78 % ------
% 6.09/1.78 % Current options:
% 6.09/1.78 % ------
% 6.09/1.78
% 6.09/1.78
% 6.09/1.78 %
% 6.09/1.78
% 6.09/1.78 % ------ Proving...
% 6.09/1.78 %
% 6.09/1.78
% 6.09/1.78 % SZS status Unsatisfiable for theBenchmark.p
% 6.09/1.78
% 6.09/1.78 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.22/1.81
% 8.22/1.81
%------------------------------------------------------------------------------