%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 09:08:45 AM UTC 2026
% Result : Unsatisfiable 29.65s 9.74s
% Output : CNFRefutation 29.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 264
% Number of leaves : 263
% Syntax : Number of formulae : 1689 (1290 unt; 0 def)
% Number of atoms : 2088 (2087 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 411 ( 12 ~; 399 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 313 ( 313 usr; 309 con; 0-3 aty)
% Number of variables : 171 ( 4 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : select(store(VAR_0,VAR_1,VAR_2),VAR_1) = VAR_2,
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
select(store(A,B,C),B) = C,
inference(clausify,[status(thm)],[a1]) ).
fof(a2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( select(store(VAR_2,VAR_0,VAR_3),VAR_1) = select(VAR_2,VAR_1)
| VAR_0 = VAR_1 ),
file('theBenchmark.p',a2) ).
cnf(c_2,plain,
( select(store(C,A,D),B) = select(C,B)
| A = B ),
inference(clausify,[status(thm)],[a2]) ).
fof(head_distinct_from_tail,axiom,
head != tail,
file('theBenchmark.p',head_distinct_from_tail) ).
cnf(c_3,plain,
head != tail,
inference(clausify,[status(thm)],[head_distinct_from_tail]) ).
fof(head_distinct_from_seq,axiom,
head != seq,
file('theBenchmark.p',head_distinct_from_seq) ).
cnf(c_4,plain,
head != seq,
inference(clausify,[status(thm)],[head_distinct_from_seq]) ).
fof(tail_distinct_from_seq,axiom,
tail != seq,
file('theBenchmark.p',tail_distinct_from_seq) ).
cnf(c_5,plain,
tail != seq,
inference(clausify,[status(thm)],[tail_distinct_from_seq]) ).
cnf(c_6,plain,
seq != tail,
inference(copy,[status(thm)],[c_5]) ).
fof(ps,axiom,
! [VAR_0] : p(s(VAR_0)) = VAR_0,
file('theBenchmark.p',ps) ).
cnf(c_7,plain,
p(s(A)) = A,
inference(clausify,[status(thm)],[ps]) ).
fof(circular,axiom,
! [VAR_0] : s(s(s(VAR_0))) = VAR_0,
file('theBenchmark.p',circular) ).
cnf(c_11,plain,
s(s(s(A))) = A,
inference(clausify,[status(thm)],[circular]) ).
fof(hyp61,axiom,
earray_262 = store(earray_260,index_261,e48),
file('theBenchmark.p',hyp61) ).
cnf(c_134,plain,
earray_262 = store(earray_260,index_261,e48),
inference(clausify,[status(thm)],[hyp61]) ).
cnf(c_135,plain,
store(earray_260,index_261,e48) = earray_262,
inference(copy,[status(thm)],[c_134]) ).
fof(hyp73,axiom,
earray_296 = select(q49,seq),
file('theBenchmark.p',hyp73) ).
cnf(c_158,plain,
earray_296 = select(q49,seq),
inference(clausify,[status(thm)],[hyp73]) ).
cnf(c_159,plain,
select(q49,seq) = earray_296,
inference(copy,[status(thm)],[c_158]) ).
fof(hyp99,axiom,
elem_298 = select(earray_296,index_297),
file('theBenchmark.p',hyp99) ).
cnf(c_210,plain,
elem_298 = select(earray_296,index_297),
inference(clausify,[status(thm)],[hyp99]) ).
cnf(c_211,plain,
select(earray_296,index_297) = elem_298,
inference(copy,[status(thm)],[c_210]) ).
fof(hyp100,axiom,
elem_301 = select(earray_296,index_300),
file('theBenchmark.p',hyp100) ).
cnf(c_212,plain,
elem_301 = select(earray_296,index_300),
inference(clausify,[status(thm)],[hyp100]) ).
cnf(c_213,plain,
select(earray_296,index_300) = elem_301,
inference(copy,[status(thm)],[c_212]) ).
fof(hyp101,axiom,
index_0 = select(q,tail),
file('theBenchmark.p',hyp101) ).
cnf(c_214,plain,
index_0 = select(q,tail),
inference(clausify,[status(thm)],[hyp101]) ).
cnf(c_215,plain,
select(q,tail) = index_0,
inference(copy,[status(thm)],[c_214]) ).
fof(hyp102,axiom,
index_102 = s(index_99),
file('theBenchmark.p',hyp102) ).
cnf(c_216,plain,
index_102 = s(index_99),
inference(clausify,[status(thm)],[hyp102]) ).
cnf(c_217,plain,
s(index_99) = index_102,
inference(copy,[status(thm)],[c_216]) ).
fof(hyp103,axiom,
index_105 = select(q24,tail),
file('theBenchmark.p',hyp103) ).
cnf(c_218,plain,
index_105 = select(q24,tail),
inference(clausify,[status(thm)],[hyp103]) ).
cnf(c_219,plain,
select(q24,tail) = index_105,
inference(copy,[status(thm)],[c_218]) ).
fof(hyp104,axiom,
index_108 = s(index_105),
file('theBenchmark.p',hyp104) ).
cnf(c_220,plain,
index_108 = s(index_105),
inference(clausify,[status(thm)],[hyp104]) ).
cnf(c_221,plain,
s(index_105) = index_108,
inference(copy,[status(thm)],[c_220]) ).
fof(hyp105,axiom,
index_111 = select(q25,tail),
file('theBenchmark.p',hyp105) ).
cnf(c_222,plain,
index_111 = select(q25,tail),
inference(clausify,[status(thm)],[hyp105]) ).
cnf(c_223,plain,
select(q25,tail) = index_111,
inference(copy,[status(thm)],[c_222]) ).
fof(hyp106,axiom,
index_114 = s(index_111),
file('theBenchmark.p',hyp106) ).
cnf(c_224,plain,
index_114 = s(index_111),
inference(clausify,[status(thm)],[hyp106]) ).
cnf(c_225,plain,
s(index_111) = index_114,
inference(copy,[status(thm)],[c_224]) ).
fof(hyp107,axiom,
index_117 = select(q26,tail),
file('theBenchmark.p',hyp107) ).
cnf(c_226,plain,
index_117 = select(q26,tail),
inference(clausify,[status(thm)],[hyp107]) ).
cnf(c_227,plain,
select(q26,tail) = index_117,
inference(copy,[status(thm)],[c_226]) ).
fof(hyp108,axiom,
index_12 = s(index_9),
file('theBenchmark.p',hyp108) ).
cnf(c_228,plain,
index_12 = s(index_9),
inference(clausify,[status(thm)],[hyp108]) ).
cnf(c_229,plain,
s(index_9) = index_12,
inference(copy,[status(thm)],[c_228]) ).
fof(hyp109,axiom,
index_120 = s(index_117),
file('theBenchmark.p',hyp109) ).
cnf(c_230,plain,
index_120 = s(index_117),
inference(clausify,[status(thm)],[hyp109]) ).
cnf(c_231,plain,
s(index_117) = index_120,
inference(copy,[status(thm)],[c_230]) ).
fof(hyp110,axiom,
index_123 = select(q27,tail),
file('theBenchmark.p',hyp110) ).
cnf(c_232,plain,
index_123 = select(q27,tail),
inference(clausify,[status(thm)],[hyp110]) ).
cnf(c_233,plain,
select(q27,tail) = index_123,
inference(copy,[status(thm)],[c_232]) ).
fof(hyp111,axiom,
index_126 = s(index_123),
file('theBenchmark.p',hyp111) ).
cnf(c_234,plain,
index_126 = s(index_123),
inference(clausify,[status(thm)],[hyp111]) ).
cnf(c_235,plain,
s(index_123) = index_126,
inference(copy,[status(thm)],[c_234]) ).
fof(hyp112,axiom,
index_129 = select(q28,tail),
file('theBenchmark.p',hyp112) ).
cnf(c_236,plain,
index_129 = select(q28,tail),
inference(clausify,[status(thm)],[hyp112]) ).
cnf(c_237,plain,
select(q28,tail) = index_129,
inference(copy,[status(thm)],[c_236]) ).
fof(hyp113,axiom,
index_132 = s(index_129),
file('theBenchmark.p',hyp113) ).
cnf(c_238,plain,
index_132 = s(index_129),
inference(clausify,[status(thm)],[hyp113]) ).
cnf(c_239,plain,
s(index_129) = index_132,
inference(copy,[status(thm)],[c_238]) ).
fof(hyp114,axiom,
index_135 = select(q2,tail),
file('theBenchmark.p',hyp114) ).
cnf(c_240,plain,
index_135 = select(q2,tail),
inference(clausify,[status(thm)],[hyp114]) ).
cnf(c_241,plain,
select(q2,tail) = index_135,
inference(copy,[status(thm)],[c_240]) ).
fof(hyp115,axiom,
index_138 = s(index_135),
file('theBenchmark.p',hyp115) ).
cnf(c_242,plain,
index_138 = s(index_135),
inference(clausify,[status(thm)],[hyp115]) ).
cnf(c_243,plain,
s(index_135) = index_138,
inference(copy,[status(thm)],[c_242]) ).
fof(hyp116,axiom,
index_141 = select(q29,tail),
file('theBenchmark.p',hyp116) ).
cnf(c_244,plain,
index_141 = select(q29,tail),
inference(clausify,[status(thm)],[hyp116]) ).
cnf(c_245,plain,
select(q29,tail) = index_141,
inference(copy,[status(thm)],[c_244]) ).
fof(hyp117,axiom,
index_144 = s(index_141),
file('theBenchmark.p',hyp117) ).
cnf(c_246,plain,
index_144 = s(index_141),
inference(clausify,[status(thm)],[hyp117]) ).
cnf(c_247,plain,
s(index_141) = index_144,
inference(copy,[status(thm)],[c_246]) ).
fof(hyp118,axiom,
index_147 = select(q30,tail),
file('theBenchmark.p',hyp118) ).
cnf(c_248,plain,
index_147 = select(q30,tail),
inference(clausify,[status(thm)],[hyp118]) ).
cnf(c_249,plain,
select(q30,tail) = index_147,
inference(copy,[status(thm)],[c_248]) ).
fof(hyp119,axiom,
index_15 = select(q10,tail),
file('theBenchmark.p',hyp119) ).
cnf(c_250,plain,
index_15 = select(q10,tail),
inference(clausify,[status(thm)],[hyp119]) ).
cnf(c_251,plain,
select(q10,tail) = index_15,
inference(copy,[status(thm)],[c_250]) ).
fof(hyp120,axiom,
index_150 = s(index_147),
file('theBenchmark.p',hyp120) ).
cnf(c_252,plain,
index_150 = s(index_147),
inference(clausify,[status(thm)],[hyp120]) ).
cnf(c_253,plain,
s(index_147) = index_150,
inference(copy,[status(thm)],[c_252]) ).
fof(hyp121,axiom,
index_153 = select(q31,tail),
file('theBenchmark.p',hyp121) ).
cnf(c_254,plain,
index_153 = select(q31,tail),
inference(clausify,[status(thm)],[hyp121]) ).
cnf(c_255,plain,
select(q31,tail) = index_153,
inference(copy,[status(thm)],[c_254]) ).
fof(hyp122,axiom,
index_156 = s(index_153),
file('theBenchmark.p',hyp122) ).
cnf(c_256,plain,
index_156 = s(index_153),
inference(clausify,[status(thm)],[hyp122]) ).
cnf(c_257,plain,
s(index_153) = index_156,
inference(copy,[status(thm)],[c_256]) ).
fof(hyp123,axiom,
index_159 = select(q32,tail),
file('theBenchmark.p',hyp123) ).
cnf(c_258,plain,
index_159 = select(q32,tail),
inference(clausify,[status(thm)],[hyp123]) ).
cnf(c_259,plain,
select(q32,tail) = index_159,
inference(copy,[status(thm)],[c_258]) ).
fof(hyp124,axiom,
index_162 = s(index_159),
file('theBenchmark.p',hyp124) ).
cnf(c_260,plain,
index_162 = s(index_159),
inference(clausify,[status(thm)],[hyp124]) ).
cnf(c_261,plain,
s(index_159) = index_162,
inference(copy,[status(thm)],[c_260]) ).
fof(hyp125,axiom,
index_165 = select(q33,tail),
file('theBenchmark.p',hyp125) ).
cnf(c_262,plain,
index_165 = select(q33,tail),
inference(clausify,[status(thm)],[hyp125]) ).
cnf(c_263,plain,
select(q33,tail) = index_165,
inference(copy,[status(thm)],[c_262]) ).
fof(hyp126,axiom,
index_168 = s(index_165),
file('theBenchmark.p',hyp126) ).
cnf(c_264,plain,
index_168 = s(index_165),
inference(clausify,[status(thm)],[hyp126]) ).
cnf(c_265,plain,
s(index_165) = index_168,
inference(copy,[status(thm)],[c_264]) ).
fof(hyp127,axiom,
index_171 = select(q34,tail),
file('theBenchmark.p',hyp127) ).
cnf(c_266,plain,
index_171 = select(q34,tail),
inference(clausify,[status(thm)],[hyp127]) ).
cnf(c_267,plain,
select(q34,tail) = index_171,
inference(copy,[status(thm)],[c_266]) ).
fof(hyp128,axiom,
index_174 = s(index_171),
file('theBenchmark.p',hyp128) ).
cnf(c_268,plain,
index_174 = s(index_171),
inference(clausify,[status(thm)],[hyp128]) ).
cnf(c_269,plain,
s(index_171) = index_174,
inference(copy,[status(thm)],[c_268]) ).
fof(hyp129,axiom,
index_177 = select(q35,tail),
file('theBenchmark.p',hyp129) ).
cnf(c_270,plain,
index_177 = select(q35,tail),
inference(clausify,[status(thm)],[hyp129]) ).
cnf(c_271,plain,
select(q35,tail) = index_177,
inference(copy,[status(thm)],[c_270]) ).
fof(hyp130,axiom,
index_18 = s(index_15),
file('theBenchmark.p',hyp130) ).
cnf(c_272,plain,
index_18 = s(index_15),
inference(clausify,[status(thm)],[hyp130]) ).
cnf(c_273,plain,
s(index_15) = index_18,
inference(copy,[status(thm)],[c_272]) ).
fof(hyp131,axiom,
index_180 = s(index_177),
file('theBenchmark.p',hyp131) ).
cnf(c_274,plain,
index_180 = s(index_177),
inference(clausify,[status(thm)],[hyp131]) ).
cnf(c_275,plain,
s(index_177) = index_180,
inference(copy,[status(thm)],[c_274]) ).
fof(hyp132,axiom,
index_183 = select(q36,tail),
file('theBenchmark.p',hyp132) ).
cnf(c_276,plain,
index_183 = select(q36,tail),
inference(clausify,[status(thm)],[hyp132]) ).
cnf(c_277,plain,
select(q36,tail) = index_183,
inference(copy,[status(thm)],[c_276]) ).
fof(hyp133,axiom,
index_186 = s(index_183),
file('theBenchmark.p',hyp133) ).
cnf(c_278,plain,
index_186 = s(index_183),
inference(clausify,[status(thm)],[hyp133]) ).
cnf(c_279,plain,
s(index_183) = index_186,
inference(copy,[status(thm)],[c_278]) ).
fof(hyp134,axiom,
index_189 = select(q37,tail),
file('theBenchmark.p',hyp134) ).
cnf(c_280,plain,
index_189 = select(q37,tail),
inference(clausify,[status(thm)],[hyp134]) ).
cnf(c_281,plain,
select(q37,tail) = index_189,
inference(copy,[status(thm)],[c_280]) ).
fof(hyp135,axiom,
index_192 = s(index_189),
file('theBenchmark.p',hyp135) ).
cnf(c_282,plain,
index_192 = s(index_189),
inference(clausify,[status(thm)],[hyp135]) ).
cnf(c_283,plain,
s(index_189) = index_192,
inference(copy,[status(thm)],[c_282]) ).
fof(hyp136,axiom,
index_195 = select(q38,tail),
file('theBenchmark.p',hyp136) ).
cnf(c_284,plain,
index_195 = select(q38,tail),
inference(clausify,[status(thm)],[hyp136]) ).
cnf(c_285,plain,
select(q38,tail) = index_195,
inference(copy,[status(thm)],[c_284]) ).
fof(hyp137,axiom,
index_198 = s(index_195),
file('theBenchmark.p',hyp137) ).
cnf(c_286,plain,
index_198 = s(index_195),
inference(clausify,[status(thm)],[hyp137]) ).
cnf(c_287,plain,
s(index_195) = index_198,
inference(copy,[status(thm)],[c_286]) ).
fof(hyp138,axiom,
index_201 = select(q3,tail),
file('theBenchmark.p',hyp138) ).
cnf(c_288,plain,
index_201 = select(q3,tail),
inference(clausify,[status(thm)],[hyp138]) ).
cnf(c_289,plain,
select(q3,tail) = index_201,
inference(copy,[status(thm)],[c_288]) ).
fof(hyp139,axiom,
index_204 = s(index_201),
file('theBenchmark.p',hyp139) ).
cnf(c_290,plain,
index_204 = s(index_201),
inference(clausify,[status(thm)],[hyp139]) ).
cnf(c_291,plain,
s(index_201) = index_204,
inference(copy,[status(thm)],[c_290]) ).
fof(hyp140,axiom,
index_207 = select(q39,tail),
file('theBenchmark.p',hyp140) ).
cnf(c_292,plain,
index_207 = select(q39,tail),
inference(clausify,[status(thm)],[hyp140]) ).
cnf(c_293,plain,
select(q39,tail) = index_207,
inference(copy,[status(thm)],[c_292]) ).
fof(hyp141,axiom,
index_21 = select(q11,tail),
file('theBenchmark.p',hyp141) ).
cnf(c_294,plain,
index_21 = select(q11,tail),
inference(clausify,[status(thm)],[hyp141]) ).
cnf(c_295,plain,
select(q11,tail) = index_21,
inference(copy,[status(thm)],[c_294]) ).
fof(hyp142,axiom,
index_210 = s(index_207),
file('theBenchmark.p',hyp142) ).
cnf(c_296,plain,
index_210 = s(index_207),
inference(clausify,[status(thm)],[hyp142]) ).
cnf(c_297,plain,
s(index_207) = index_210,
inference(copy,[status(thm)],[c_296]) ).
fof(hyp143,axiom,
index_213 = select(q40,tail),
file('theBenchmark.p',hyp143) ).
cnf(c_298,plain,
index_213 = select(q40,tail),
inference(clausify,[status(thm)],[hyp143]) ).
cnf(c_299,plain,
select(q40,tail) = index_213,
inference(copy,[status(thm)],[c_298]) ).
fof(hyp144,axiom,
index_216 = s(index_213),
file('theBenchmark.p',hyp144) ).
cnf(c_300,plain,
index_216 = s(index_213),
inference(clausify,[status(thm)],[hyp144]) ).
cnf(c_301,plain,
s(index_213) = index_216,
inference(copy,[status(thm)],[c_300]) ).
fof(hyp145,axiom,
index_219 = select(q41,tail),
file('theBenchmark.p',hyp145) ).
cnf(c_302,plain,
index_219 = select(q41,tail),
inference(clausify,[status(thm)],[hyp145]) ).
cnf(c_303,plain,
select(q41,tail) = index_219,
inference(copy,[status(thm)],[c_302]) ).
fof(hyp146,axiom,
index_222 = s(index_219),
file('theBenchmark.p',hyp146) ).
cnf(c_304,plain,
index_222 = s(index_219),
inference(clausify,[status(thm)],[hyp146]) ).
cnf(c_305,plain,
s(index_219) = index_222,
inference(copy,[status(thm)],[c_304]) ).
fof(hyp147,axiom,
index_225 = select(q42,tail),
file('theBenchmark.p',hyp147) ).
cnf(c_306,plain,
index_225 = select(q42,tail),
inference(clausify,[status(thm)],[hyp147]) ).
cnf(c_307,plain,
select(q42,tail) = index_225,
inference(copy,[status(thm)],[c_306]) ).
fof(hyp148,axiom,
index_228 = s(index_225),
file('theBenchmark.p',hyp148) ).
cnf(c_308,plain,
index_228 = s(index_225),
inference(clausify,[status(thm)],[hyp148]) ).
cnf(c_309,plain,
s(index_225) = index_228,
inference(copy,[status(thm)],[c_308]) ).
fof(hyp149,axiom,
index_231 = select(q43,tail),
file('theBenchmark.p',hyp149) ).
cnf(c_310,plain,
index_231 = select(q43,tail),
inference(clausify,[status(thm)],[hyp149]) ).
cnf(c_311,plain,
select(q43,tail) = index_231,
inference(copy,[status(thm)],[c_310]) ).
fof(hyp150,axiom,
index_234 = s(index_231),
file('theBenchmark.p',hyp150) ).
cnf(c_312,plain,
index_234 = s(index_231),
inference(clausify,[status(thm)],[hyp150]) ).
cnf(c_313,plain,
s(index_231) = index_234,
inference(copy,[status(thm)],[c_312]) ).
fof(hyp151,axiom,
index_237 = select(q44,tail),
file('theBenchmark.p',hyp151) ).
cnf(c_314,plain,
index_237 = select(q44,tail),
inference(clausify,[status(thm)],[hyp151]) ).
cnf(c_315,plain,
select(q44,tail) = index_237,
inference(copy,[status(thm)],[c_314]) ).
fof(hyp152,axiom,
index_24 = s(index_21),
file('theBenchmark.p',hyp152) ).
cnf(c_316,plain,
index_24 = s(index_21),
inference(clausify,[status(thm)],[hyp152]) ).
cnf(c_317,plain,
s(index_21) = index_24,
inference(copy,[status(thm)],[c_316]) ).
fof(hyp153,axiom,
index_240 = s(index_237),
file('theBenchmark.p',hyp153) ).
cnf(c_318,plain,
index_240 = s(index_237),
inference(clausify,[status(thm)],[hyp153]) ).
cnf(c_319,plain,
s(index_237) = index_240,
inference(copy,[status(thm)],[c_318]) ).
fof(hyp154,axiom,
index_243 = select(q45,tail),
file('theBenchmark.p',hyp154) ).
cnf(c_320,plain,
index_243 = select(q45,tail),
inference(clausify,[status(thm)],[hyp154]) ).
cnf(c_321,plain,
select(q45,tail) = index_243,
inference(copy,[status(thm)],[c_320]) ).
fof(hyp155,axiom,
index_246 = s(index_243),
file('theBenchmark.p',hyp155) ).
cnf(c_322,plain,
index_246 = s(index_243),
inference(clausify,[status(thm)],[hyp155]) ).
cnf(c_323,plain,
s(index_243) = index_246,
inference(copy,[status(thm)],[c_322]) ).
fof(hyp156,axiom,
index_249 = select(q46,tail),
file('theBenchmark.p',hyp156) ).
cnf(c_324,plain,
index_249 = select(q46,tail),
inference(clausify,[status(thm)],[hyp156]) ).
cnf(c_325,plain,
select(q46,tail) = index_249,
inference(copy,[status(thm)],[c_324]) ).
fof(hyp157,axiom,
index_252 = s(index_249),
file('theBenchmark.p',hyp157) ).
cnf(c_326,plain,
index_252 = s(index_249),
inference(clausify,[status(thm)],[hyp157]) ).
cnf(c_327,plain,
s(index_249) = index_252,
inference(copy,[status(thm)],[c_326]) ).
fof(hyp158,axiom,
index_255 = select(q47,tail),
file('theBenchmark.p',hyp158) ).
cnf(c_328,plain,
index_255 = select(q47,tail),
inference(clausify,[status(thm)],[hyp158]) ).
cnf(c_329,plain,
select(q47,tail) = index_255,
inference(copy,[status(thm)],[c_328]) ).
fof(hyp159,axiom,
index_258 = s(index_255),
file('theBenchmark.p',hyp159) ).
cnf(c_330,plain,
index_258 = s(index_255),
inference(clausify,[status(thm)],[hyp159]) ).
cnf(c_331,plain,
s(index_255) = index_258,
inference(copy,[status(thm)],[c_330]) ).
fof(hyp160,axiom,
index_261 = select(q48,tail),
file('theBenchmark.p',hyp160) ).
cnf(c_332,plain,
index_261 = select(q48,tail),
inference(clausify,[status(thm)],[hyp160]) ).
cnf(c_333,plain,
select(q48,tail) = index_261,
inference(copy,[status(thm)],[c_332]) ).
fof(hyp161,axiom,
index_264 = s(index_261),
file('theBenchmark.p',hyp161) ).
cnf(c_334,plain,
index_264 = s(index_261),
inference(clausify,[status(thm)],[hyp161]) ).
cnf(c_335,plain,
s(index_261) = index_264,
inference(copy,[status(thm)],[c_334]) ).
fof(hyp162,axiom,
index_267 = select(q4,tail),
file('theBenchmark.p',hyp162) ).
cnf(c_336,plain,
index_267 = select(q4,tail),
inference(clausify,[status(thm)],[hyp162]) ).
cnf(c_337,plain,
select(q4,tail) = index_267,
inference(copy,[status(thm)],[c_336]) ).
fof(hyp163,axiom,
index_27 = select(q12,tail),
file('theBenchmark.p',hyp163) ).
cnf(c_338,plain,
index_27 = select(q12,tail),
inference(clausify,[status(thm)],[hyp163]) ).
cnf(c_339,plain,
select(q12,tail) = index_27,
inference(copy,[status(thm)],[c_338]) ).
fof(hyp164,axiom,
index_270 = s(index_267),
file('theBenchmark.p',hyp164) ).
cnf(c_340,plain,
index_270 = s(index_267),
inference(clausify,[status(thm)],[hyp164]) ).
cnf(c_341,plain,
s(index_267) = index_270,
inference(copy,[status(thm)],[c_340]) ).
fof(hyp165,axiom,
index_273 = select(q5,tail),
file('theBenchmark.p',hyp165) ).
cnf(c_342,plain,
index_273 = select(q5,tail),
inference(clausify,[status(thm)],[hyp165]) ).
cnf(c_343,plain,
select(q5,tail) = index_273,
inference(copy,[status(thm)],[c_342]) ).
fof(hyp166,axiom,
index_276 = s(index_273),
file('theBenchmark.p',hyp166) ).
cnf(c_344,plain,
index_276 = s(index_273),
inference(clausify,[status(thm)],[hyp166]) ).
cnf(c_345,plain,
s(index_273) = index_276,
inference(copy,[status(thm)],[c_344]) ).
fof(hyp167,axiom,
index_279 = select(q6,tail),
file('theBenchmark.p',hyp167) ).
cnf(c_346,plain,
index_279 = select(q6,tail),
inference(clausify,[status(thm)],[hyp167]) ).
cnf(c_347,plain,
select(q6,tail) = index_279,
inference(copy,[status(thm)],[c_346]) ).
fof(hyp168,axiom,
index_282 = s(index_279),
file('theBenchmark.p',hyp168) ).
cnf(c_348,plain,
index_282 = s(index_279),
inference(clausify,[status(thm)],[hyp168]) ).
cnf(c_349,plain,
s(index_279) = index_282,
inference(copy,[status(thm)],[c_348]) ).
fof(hyp169,axiom,
index_285 = select(q7,tail),
file('theBenchmark.p',hyp169) ).
cnf(c_350,plain,
index_285 = select(q7,tail),
inference(clausify,[status(thm)],[hyp169]) ).
cnf(c_351,plain,
select(q7,tail) = index_285,
inference(copy,[status(thm)],[c_350]) ).
fof(hyp170,axiom,
index_288 = s(index_285),
file('theBenchmark.p',hyp170) ).
cnf(c_352,plain,
index_288 = s(index_285),
inference(clausify,[status(thm)],[hyp170]) ).
cnf(c_353,plain,
s(index_285) = index_288,
inference(copy,[status(thm)],[c_352]) ).
fof(hyp171,axiom,
index_291 = select(q8,tail),
file('theBenchmark.p',hyp171) ).
cnf(c_354,plain,
index_291 = select(q8,tail),
inference(clausify,[status(thm)],[hyp171]) ).
cnf(c_355,plain,
select(q8,tail) = index_291,
inference(copy,[status(thm)],[c_354]) ).
fof(hyp172,axiom,
index_294 = s(index_291),
file('theBenchmark.p',hyp172) ).
cnf(c_356,plain,
index_294 = s(index_291),
inference(clausify,[status(thm)],[hyp172]) ).
cnf(c_357,plain,
s(index_291) = index_294,
inference(copy,[status(thm)],[c_356]) ).
fof(hyp173,axiom,
index_297 = select(q49,head),
file('theBenchmark.p',hyp173) ).
cnf(c_358,plain,
index_297 = select(q49,head),
inference(clausify,[status(thm)],[hyp173]) ).
cnf(c_359,plain,
select(q49,head) = index_297,
inference(copy,[status(thm)],[c_358]) ).
fof(hyp174,axiom,
index_299 = select(q49,tail),
file('theBenchmark.p',hyp174) ).
cnf(c_360,plain,
index_299 = select(q49,tail),
inference(clausify,[status(thm)],[hyp174]) ).
cnf(c_361,plain,
select(q49,tail) = index_299,
inference(copy,[status(thm)],[c_360]) ).
fof(hyp175,axiom,
index_3 = select(q0,tail),
file('theBenchmark.p',hyp175) ).
cnf(c_362,plain,
index_3 = select(q0,tail),
inference(clausify,[status(thm)],[hyp175]) ).
cnf(c_363,plain,
select(q0,tail) = index_3,
inference(copy,[status(thm)],[c_362]) ).
fof(hyp176,axiom,
index_30 = s(index_27),
file('theBenchmark.p',hyp176) ).
cnf(c_364,plain,
index_30 = s(index_27),
inference(clausify,[status(thm)],[hyp176]) ).
cnf(c_365,plain,
s(index_27) = index_30,
inference(copy,[status(thm)],[c_364]) ).
fof(hyp177,axiom,
s(index_300) = index_299,
file('theBenchmark.p',hyp177) ).
cnf(c_366,plain,
s(index_300) = index_299,
inference(clausify,[status(thm)],[hyp177]) ).
fof(hyp178,axiom,
index_33 = select(q13,tail),
file('theBenchmark.p',hyp178) ).
cnf(c_367,plain,
index_33 = select(q13,tail),
inference(clausify,[status(thm)],[hyp178]) ).
cnf(c_368,plain,
select(q13,tail) = index_33,
inference(copy,[status(thm)],[c_367]) ).
fof(hyp179,axiom,
index_36 = s(index_33),
file('theBenchmark.p',hyp179) ).
cnf(c_369,plain,
index_36 = s(index_33),
inference(clausify,[status(thm)],[hyp179]) ).
cnf(c_370,plain,
s(index_33) = index_36,
inference(copy,[status(thm)],[c_369]) ).
fof(hyp180,axiom,
index_39 = select(q14,tail),
file('theBenchmark.p',hyp180) ).
cnf(c_371,plain,
index_39 = select(q14,tail),
inference(clausify,[status(thm)],[hyp180]) ).
cnf(c_372,plain,
select(q14,tail) = index_39,
inference(copy,[status(thm)],[c_371]) ).
fof(hyp181,axiom,
index_42 = s(index_39),
file('theBenchmark.p',hyp181) ).
cnf(c_373,plain,
index_42 = s(index_39),
inference(clausify,[status(thm)],[hyp181]) ).
cnf(c_374,plain,
s(index_39) = index_42,
inference(copy,[status(thm)],[c_373]) ).
fof(hyp182,axiom,
index_45 = select(q15,tail),
file('theBenchmark.p',hyp182) ).
cnf(c_375,plain,
index_45 = select(q15,tail),
inference(clausify,[status(thm)],[hyp182]) ).
cnf(c_376,plain,
select(q15,tail) = index_45,
inference(copy,[status(thm)],[c_375]) ).
fof(hyp183,axiom,
index_48 = s(index_45),
file('theBenchmark.p',hyp183) ).
cnf(c_377,plain,
index_48 = s(index_45),
inference(clausify,[status(thm)],[hyp183]) ).
cnf(c_378,plain,
s(index_45) = index_48,
inference(copy,[status(thm)],[c_377]) ).
fof(hyp184,axiom,
index_51 = select(q16,tail),
file('theBenchmark.p',hyp184) ).
cnf(c_379,plain,
index_51 = select(q16,tail),
inference(clausify,[status(thm)],[hyp184]) ).
cnf(c_380,plain,
select(q16,tail) = index_51,
inference(copy,[status(thm)],[c_379]) ).
fof(hyp185,axiom,
index_54 = s(index_51),
file('theBenchmark.p',hyp185) ).
cnf(c_381,plain,
index_54 = s(index_51),
inference(clausify,[status(thm)],[hyp185]) ).
cnf(c_382,plain,
s(index_51) = index_54,
inference(copy,[status(thm)],[c_381]) ).
fof(hyp186,axiom,
index_57 = select(q17,tail),
file('theBenchmark.p',hyp186) ).
cnf(c_383,plain,
index_57 = select(q17,tail),
inference(clausify,[status(thm)],[hyp186]) ).
cnf(c_384,plain,
select(q17,tail) = index_57,
inference(copy,[status(thm)],[c_383]) ).
fof(hyp187,axiom,
index_6 = s(index_3),
file('theBenchmark.p',hyp187) ).
cnf(c_385,plain,
index_6 = s(index_3),
inference(clausify,[status(thm)],[hyp187]) ).
cnf(c_386,plain,
s(index_3) = index_6,
inference(copy,[status(thm)],[c_385]) ).
fof(hyp188,axiom,
index_60 = s(index_57),
file('theBenchmark.p',hyp188) ).
cnf(c_387,plain,
index_60 = s(index_57),
inference(clausify,[status(thm)],[hyp188]) ).
cnf(c_388,plain,
s(index_57) = index_60,
inference(copy,[status(thm)],[c_387]) ).
fof(hyp189,axiom,
index_63 = select(q18,tail),
file('theBenchmark.p',hyp189) ).
cnf(c_389,plain,
index_63 = select(q18,tail),
inference(clausify,[status(thm)],[hyp189]) ).
cnf(c_390,plain,
select(q18,tail) = index_63,
inference(copy,[status(thm)],[c_389]) ).
fof(hyp190,axiom,
index_66 = s(index_63),
file('theBenchmark.p',hyp190) ).
cnf(c_391,plain,
index_66 = s(index_63),
inference(clausify,[status(thm)],[hyp190]) ).
cnf(c_392,plain,
s(index_63) = index_66,
inference(copy,[status(thm)],[c_391]) ).
fof(hyp191,axiom,
index_69 = select(q1,tail),
file('theBenchmark.p',hyp191) ).
cnf(c_393,plain,
index_69 = select(q1,tail),
inference(clausify,[status(thm)],[hyp191]) ).
cnf(c_394,plain,
select(q1,tail) = index_69,
inference(copy,[status(thm)],[c_393]) ).
fof(hyp192,axiom,
index_72 = s(index_69),
file('theBenchmark.p',hyp192) ).
cnf(c_395,plain,
index_72 = s(index_69),
inference(clausify,[status(thm)],[hyp192]) ).
cnf(c_396,plain,
s(index_69) = index_72,
inference(copy,[status(thm)],[c_395]) ).
fof(hyp193,axiom,
index_75 = select(q19,tail),
file('theBenchmark.p',hyp193) ).
cnf(c_397,plain,
index_75 = select(q19,tail),
inference(clausify,[status(thm)],[hyp193]) ).
cnf(c_398,plain,
select(q19,tail) = index_75,
inference(copy,[status(thm)],[c_397]) ).
fof(hyp194,axiom,
index_78 = s(index_75),
file('theBenchmark.p',hyp194) ).
cnf(c_399,plain,
index_78 = s(index_75),
inference(clausify,[status(thm)],[hyp194]) ).
cnf(c_400,plain,
s(index_75) = index_78,
inference(copy,[status(thm)],[c_399]) ).
fof(hyp195,axiom,
index_81 = select(q20,tail),
file('theBenchmark.p',hyp195) ).
cnf(c_401,plain,
index_81 = select(q20,tail),
inference(clausify,[status(thm)],[hyp195]) ).
cnf(c_402,plain,
select(q20,tail) = index_81,
inference(copy,[status(thm)],[c_401]) ).
fof(hyp196,axiom,
index_84 = s(index_81),
file('theBenchmark.p',hyp196) ).
cnf(c_403,plain,
index_84 = s(index_81),
inference(clausify,[status(thm)],[hyp196]) ).
cnf(c_404,plain,
s(index_81) = index_84,
inference(copy,[status(thm)],[c_403]) ).
fof(hyp197,axiom,
index_87 = select(q21,tail),
file('theBenchmark.p',hyp197) ).
cnf(c_405,plain,
index_87 = select(q21,tail),
inference(clausify,[status(thm)],[hyp197]) ).
cnf(c_406,plain,
select(q21,tail) = index_87,
inference(copy,[status(thm)],[c_405]) ).
fof(hyp198,axiom,
index_9 = select(q9,tail),
file('theBenchmark.p',hyp198) ).
cnf(c_407,plain,
index_9 = select(q9,tail),
inference(clausify,[status(thm)],[hyp198]) ).
cnf(c_408,plain,
select(q9,tail) = index_9,
inference(copy,[status(thm)],[c_407]) ).
fof(hyp199,axiom,
index_90 = s(index_87),
file('theBenchmark.p',hyp199) ).
cnf(c_409,plain,
index_90 = s(index_87),
inference(clausify,[status(thm)],[hyp199]) ).
cnf(c_410,plain,
s(index_87) = index_90,
inference(copy,[status(thm)],[c_409]) ).
fof(hyp200,axiom,
index_93 = select(q22,tail),
file('theBenchmark.p',hyp200) ).
cnf(c_411,plain,
index_93 = select(q22,tail),
inference(clausify,[status(thm)],[hyp200]) ).
cnf(c_412,plain,
select(q22,tail) = index_93,
inference(copy,[status(thm)],[c_411]) ).
fof(hyp201,axiom,
index_96 = s(index_93),
file('theBenchmark.p',hyp201) ).
cnf(c_413,plain,
index_96 = s(index_93),
inference(clausify,[status(thm)],[hyp201]) ).
cnf(c_414,plain,
s(index_93) = index_96,
inference(copy,[status(thm)],[c_413]) ).
fof(hyp202,axiom,
index_99 = select(q23,tail),
file('theBenchmark.p',hyp202) ).
cnf(c_415,plain,
index_99 = select(q23,tail),
inference(clausify,[status(thm)],[hyp202]) ).
cnf(c_416,plain,
select(q23,tail) = index_99,
inference(copy,[status(thm)],[c_415]) ).
fof(hyp203,axiom,
queue_1 = store(q,head,index_0),
file('theBenchmark.p',hyp203) ).
cnf(c_417,plain,
queue_1 = store(q,head,index_0),
inference(clausify,[status(thm)],[hyp203]) ).
cnf(c_418,plain,
store(q,head,index_0) = queue_1,
inference(copy,[status(thm)],[c_417]) ).
fof(hyp204,axiom,
queue_101 = store(q23,seq,earray_100),
file('theBenchmark.p',hyp204) ).
cnf(c_419,plain,
queue_101 = store(q23,seq,earray_100),
inference(clausify,[status(thm)],[hyp204]) ).
cnf(c_420,plain,
store(q23,seq,earray_100) = queue_101,
inference(copy,[status(thm)],[c_419]) ).
fof(hyp205,axiom,
queue_103 = store(queue_101,tail,index_102),
file('theBenchmark.p',hyp205) ).
cnf(c_421,plain,
queue_103 = store(queue_101,tail,index_102),
inference(clausify,[status(thm)],[hyp205]) ).
cnf(c_422,plain,
store(queue_101,tail,index_102) = queue_103,
inference(copy,[status(thm)],[c_421]) ).
fof(hyp206,axiom,
queue_107 = store(q24,seq,earray_106),
file('theBenchmark.p',hyp206) ).
cnf(c_423,plain,
queue_107 = store(q24,seq,earray_106),
inference(clausify,[status(thm)],[hyp206]) ).
cnf(c_424,plain,
store(q24,seq,earray_106) = queue_107,
inference(copy,[status(thm)],[c_423]) ).
fof(hyp207,axiom,
queue_109 = store(queue_107,tail,index_108),
file('theBenchmark.p',hyp207) ).
cnf(c_425,plain,
queue_109 = store(queue_107,tail,index_108),
inference(clausify,[status(thm)],[hyp207]) ).
cnf(c_426,plain,
store(queue_107,tail,index_108) = queue_109,
inference(copy,[status(thm)],[c_425]) ).
fof(hyp208,axiom,
queue_11 = store(q9,seq,earray_10),
file('theBenchmark.p',hyp208) ).
cnf(c_427,plain,
queue_11 = store(q9,seq,earray_10),
inference(clausify,[status(thm)],[hyp208]) ).
cnf(c_428,plain,
store(q9,seq,earray_10) = queue_11,
inference(copy,[status(thm)],[c_427]) ).
fof(hyp209,axiom,
queue_113 = store(q25,seq,earray_112),
file('theBenchmark.p',hyp209) ).
cnf(c_429,plain,
queue_113 = store(q25,seq,earray_112),
inference(clausify,[status(thm)],[hyp209]) ).
cnf(c_430,plain,
store(q25,seq,earray_112) = queue_113,
inference(copy,[status(thm)],[c_429]) ).
fof(hyp210,axiom,
queue_115 = store(queue_113,tail,index_114),
file('theBenchmark.p',hyp210) ).
cnf(c_431,plain,
queue_115 = store(queue_113,tail,index_114),
inference(clausify,[status(thm)],[hyp210]) ).
cnf(c_432,plain,
store(queue_113,tail,index_114) = queue_115,
inference(copy,[status(thm)],[c_431]) ).
fof(hyp211,axiom,
queue_119 = store(q26,seq,earray_118),
file('theBenchmark.p',hyp211) ).
cnf(c_433,plain,
queue_119 = store(q26,seq,earray_118),
inference(clausify,[status(thm)],[hyp211]) ).
cnf(c_434,plain,
store(q26,seq,earray_118) = queue_119,
inference(copy,[status(thm)],[c_433]) ).
fof(hyp212,axiom,
queue_121 = store(queue_119,tail,index_120),
file('theBenchmark.p',hyp212) ).
cnf(c_435,plain,
queue_121 = store(queue_119,tail,index_120),
inference(clausify,[status(thm)],[hyp212]) ).
cnf(c_436,plain,
store(queue_119,tail,index_120) = queue_121,
inference(copy,[status(thm)],[c_435]) ).
fof(hyp213,axiom,
queue_125 = store(q27,seq,earray_124),
file('theBenchmark.p',hyp213) ).
cnf(c_437,plain,
queue_125 = store(q27,seq,earray_124),
inference(clausify,[status(thm)],[hyp213]) ).
cnf(c_438,plain,
store(q27,seq,earray_124) = queue_125,
inference(copy,[status(thm)],[c_437]) ).
fof(hyp214,axiom,
queue_127 = store(queue_125,tail,index_126),
file('theBenchmark.p',hyp214) ).
cnf(c_439,plain,
queue_127 = store(queue_125,tail,index_126),
inference(clausify,[status(thm)],[hyp214]) ).
cnf(c_440,plain,
store(queue_125,tail,index_126) = queue_127,
inference(copy,[status(thm)],[c_439]) ).
fof(hyp215,axiom,
queue_13 = store(queue_11,tail,index_12),
file('theBenchmark.p',hyp215) ).
cnf(c_441,plain,
queue_13 = store(queue_11,tail,index_12),
inference(clausify,[status(thm)],[hyp215]) ).
cnf(c_442,plain,
store(queue_11,tail,index_12) = queue_13,
inference(copy,[status(thm)],[c_441]) ).
fof(hyp216,axiom,
queue_131 = store(q28,seq,earray_130),
file('theBenchmark.p',hyp216) ).
cnf(c_443,plain,
queue_131 = store(q28,seq,earray_130),
inference(clausify,[status(thm)],[hyp216]) ).
cnf(c_444,plain,
store(q28,seq,earray_130) = queue_131,
inference(copy,[status(thm)],[c_443]) ).
fof(hyp217,axiom,
queue_133 = store(queue_131,tail,index_132),
file('theBenchmark.p',hyp217) ).
cnf(c_445,plain,
queue_133 = store(queue_131,tail,index_132),
inference(clausify,[status(thm)],[hyp217]) ).
cnf(c_446,plain,
store(queue_131,tail,index_132) = queue_133,
inference(copy,[status(thm)],[c_445]) ).
fof(hyp218,axiom,
queue_137 = store(q2,seq,earray_136),
file('theBenchmark.p',hyp218) ).
cnf(c_447,plain,
queue_137 = store(q2,seq,earray_136),
inference(clausify,[status(thm)],[hyp218]) ).
cnf(c_448,plain,
store(q2,seq,earray_136) = queue_137,
inference(copy,[status(thm)],[c_447]) ).
fof(hyp219,axiom,
queue_139 = store(queue_137,tail,index_138),
file('theBenchmark.p',hyp219) ).
cnf(c_449,plain,
queue_139 = store(queue_137,tail,index_138),
inference(clausify,[status(thm)],[hyp219]) ).
cnf(c_450,plain,
store(queue_137,tail,index_138) = queue_139,
inference(copy,[status(thm)],[c_449]) ).
fof(hyp220,axiom,
queue_143 = store(q29,seq,earray_142),
file('theBenchmark.p',hyp220) ).
cnf(c_451,plain,
queue_143 = store(q29,seq,earray_142),
inference(clausify,[status(thm)],[hyp220]) ).
cnf(c_452,plain,
store(q29,seq,earray_142) = queue_143,
inference(copy,[status(thm)],[c_451]) ).
fof(hyp221,axiom,
queue_145 = store(queue_143,tail,index_144),
file('theBenchmark.p',hyp221) ).
cnf(c_453,plain,
queue_145 = store(queue_143,tail,index_144),
inference(clausify,[status(thm)],[hyp221]) ).
cnf(c_454,plain,
store(queue_143,tail,index_144) = queue_145,
inference(copy,[status(thm)],[c_453]) ).
fof(hyp222,axiom,
queue_149 = store(q30,seq,earray_148),
file('theBenchmark.p',hyp222) ).
cnf(c_455,plain,
queue_149 = store(q30,seq,earray_148),
inference(clausify,[status(thm)],[hyp222]) ).
cnf(c_456,plain,
store(q30,seq,earray_148) = queue_149,
inference(copy,[status(thm)],[c_455]) ).
fof(hyp223,axiom,
queue_151 = store(queue_149,tail,index_150),
file('theBenchmark.p',hyp223) ).
cnf(c_457,plain,
queue_151 = store(queue_149,tail,index_150),
inference(clausify,[status(thm)],[hyp223]) ).
cnf(c_458,plain,
store(queue_149,tail,index_150) = queue_151,
inference(copy,[status(thm)],[c_457]) ).
fof(hyp224,axiom,
queue_155 = store(q31,seq,earray_154),
file('theBenchmark.p',hyp224) ).
cnf(c_459,plain,
queue_155 = store(q31,seq,earray_154),
inference(clausify,[status(thm)],[hyp224]) ).
cnf(c_460,plain,
store(q31,seq,earray_154) = queue_155,
inference(copy,[status(thm)],[c_459]) ).
fof(hyp225,axiom,
queue_157 = store(queue_155,tail,index_156),
file('theBenchmark.p',hyp225) ).
cnf(c_461,plain,
queue_157 = store(queue_155,tail,index_156),
inference(clausify,[status(thm)],[hyp225]) ).
cnf(c_462,plain,
store(queue_155,tail,index_156) = queue_157,
inference(copy,[status(thm)],[c_461]) ).
fof(hyp226,axiom,
queue_161 = store(q32,seq,earray_160),
file('theBenchmark.p',hyp226) ).
cnf(c_463,plain,
queue_161 = store(q32,seq,earray_160),
inference(clausify,[status(thm)],[hyp226]) ).
cnf(c_464,plain,
store(q32,seq,earray_160) = queue_161,
inference(copy,[status(thm)],[c_463]) ).
fof(hyp227,axiom,
queue_163 = store(queue_161,tail,index_162),
file('theBenchmark.p',hyp227) ).
cnf(c_465,plain,
queue_163 = store(queue_161,tail,index_162),
inference(clausify,[status(thm)],[hyp227]) ).
cnf(c_466,plain,
store(queue_161,tail,index_162) = queue_163,
inference(copy,[status(thm)],[c_465]) ).
fof(hyp228,axiom,
queue_167 = store(q33,seq,earray_166),
file('theBenchmark.p',hyp228) ).
cnf(c_467,plain,
queue_167 = store(q33,seq,earray_166),
inference(clausify,[status(thm)],[hyp228]) ).
cnf(c_468,plain,
store(q33,seq,earray_166) = queue_167,
inference(copy,[status(thm)],[c_467]) ).
fof(hyp229,axiom,
queue_169 = store(queue_167,tail,index_168),
file('theBenchmark.p',hyp229) ).
cnf(c_469,plain,
queue_169 = store(queue_167,tail,index_168),
inference(clausify,[status(thm)],[hyp229]) ).
cnf(c_470,plain,
store(queue_167,tail,index_168) = queue_169,
inference(copy,[status(thm)],[c_469]) ).
fof(hyp230,axiom,
queue_17 = store(q10,seq,earray_16),
file('theBenchmark.p',hyp230) ).
cnf(c_471,plain,
queue_17 = store(q10,seq,earray_16),
inference(clausify,[status(thm)],[hyp230]) ).
cnf(c_472,plain,
store(q10,seq,earray_16) = queue_17,
inference(copy,[status(thm)],[c_471]) ).
fof(hyp231,axiom,
queue_173 = store(q34,seq,earray_172),
file('theBenchmark.p',hyp231) ).
cnf(c_473,plain,
queue_173 = store(q34,seq,earray_172),
inference(clausify,[status(thm)],[hyp231]) ).
cnf(c_474,plain,
store(q34,seq,earray_172) = queue_173,
inference(copy,[status(thm)],[c_473]) ).
fof(hyp232,axiom,
queue_175 = store(queue_173,tail,index_174),
file('theBenchmark.p',hyp232) ).
cnf(c_475,plain,
queue_175 = store(queue_173,tail,index_174),
inference(clausify,[status(thm)],[hyp232]) ).
cnf(c_476,plain,
store(queue_173,tail,index_174) = queue_175,
inference(copy,[status(thm)],[c_475]) ).
fof(hyp233,axiom,
queue_179 = store(q35,seq,earray_178),
file('theBenchmark.p',hyp233) ).
cnf(c_477,plain,
queue_179 = store(q35,seq,earray_178),
inference(clausify,[status(thm)],[hyp233]) ).
cnf(c_478,plain,
store(q35,seq,earray_178) = queue_179,
inference(copy,[status(thm)],[c_477]) ).
fof(hyp234,axiom,
queue_181 = store(queue_179,tail,index_180),
file('theBenchmark.p',hyp234) ).
cnf(c_479,plain,
queue_181 = store(queue_179,tail,index_180),
inference(clausify,[status(thm)],[hyp234]) ).
cnf(c_480,plain,
store(queue_179,tail,index_180) = queue_181,
inference(copy,[status(thm)],[c_479]) ).
fof(hyp235,axiom,
queue_185 = store(q36,seq,earray_184),
file('theBenchmark.p',hyp235) ).
cnf(c_481,plain,
queue_185 = store(q36,seq,earray_184),
inference(clausify,[status(thm)],[hyp235]) ).
cnf(c_482,plain,
store(q36,seq,earray_184) = queue_185,
inference(copy,[status(thm)],[c_481]) ).
fof(hyp236,axiom,
queue_187 = store(queue_185,tail,index_186),
file('theBenchmark.p',hyp236) ).
cnf(c_483,plain,
queue_187 = store(queue_185,tail,index_186),
inference(clausify,[status(thm)],[hyp236]) ).
cnf(c_484,plain,
store(queue_185,tail,index_186) = queue_187,
inference(copy,[status(thm)],[c_483]) ).
fof(hyp237,axiom,
queue_19 = store(queue_17,tail,index_18),
file('theBenchmark.p',hyp237) ).
cnf(c_485,plain,
queue_19 = store(queue_17,tail,index_18),
inference(clausify,[status(thm)],[hyp237]) ).
cnf(c_486,plain,
store(queue_17,tail,index_18) = queue_19,
inference(copy,[status(thm)],[c_485]) ).
fof(hyp238,axiom,
queue_191 = store(q37,seq,earray_190),
file('theBenchmark.p',hyp238) ).
cnf(c_487,plain,
queue_191 = store(q37,seq,earray_190),
inference(clausify,[status(thm)],[hyp238]) ).
cnf(c_488,plain,
store(q37,seq,earray_190) = queue_191,
inference(copy,[status(thm)],[c_487]) ).
fof(hyp239,axiom,
queue_193 = store(queue_191,tail,index_192),
file('theBenchmark.p',hyp239) ).
cnf(c_489,plain,
queue_193 = store(queue_191,tail,index_192),
inference(clausify,[status(thm)],[hyp239]) ).
cnf(c_490,plain,
store(queue_191,tail,index_192) = queue_193,
inference(copy,[status(thm)],[c_489]) ).
fof(hyp240,axiom,
queue_197 = store(q38,seq,earray_196),
file('theBenchmark.p',hyp240) ).
cnf(c_491,plain,
queue_197 = store(q38,seq,earray_196),
inference(clausify,[status(thm)],[hyp240]) ).
cnf(c_492,plain,
store(q38,seq,earray_196) = queue_197,
inference(copy,[status(thm)],[c_491]) ).
fof(hyp241,axiom,
queue_199 = store(queue_197,tail,index_198),
file('theBenchmark.p',hyp241) ).
cnf(c_493,plain,
queue_199 = store(queue_197,tail,index_198),
inference(clausify,[status(thm)],[hyp241]) ).
cnf(c_494,plain,
store(queue_197,tail,index_198) = queue_199,
inference(copy,[status(thm)],[c_493]) ).
fof(hyp242,axiom,
queue_203 = store(q3,seq,earray_202),
file('theBenchmark.p',hyp242) ).
cnf(c_495,plain,
queue_203 = store(q3,seq,earray_202),
inference(clausify,[status(thm)],[hyp242]) ).
cnf(c_496,plain,
store(q3,seq,earray_202) = queue_203,
inference(copy,[status(thm)],[c_495]) ).
fof(hyp243,axiom,
queue_205 = store(queue_203,tail,index_204),
file('theBenchmark.p',hyp243) ).
cnf(c_497,plain,
queue_205 = store(queue_203,tail,index_204),
inference(clausify,[status(thm)],[hyp243]) ).
cnf(c_498,plain,
store(queue_203,tail,index_204) = queue_205,
inference(copy,[status(thm)],[c_497]) ).
fof(hyp244,axiom,
queue_209 = store(q39,seq,earray_208),
file('theBenchmark.p',hyp244) ).
cnf(c_499,plain,
queue_209 = store(q39,seq,earray_208),
inference(clausify,[status(thm)],[hyp244]) ).
cnf(c_500,plain,
store(q39,seq,earray_208) = queue_209,
inference(copy,[status(thm)],[c_499]) ).
fof(hyp245,axiom,
queue_211 = store(queue_209,tail,index_210),
file('theBenchmark.p',hyp245) ).
cnf(c_501,plain,
queue_211 = store(queue_209,tail,index_210),
inference(clausify,[status(thm)],[hyp245]) ).
cnf(c_502,plain,
store(queue_209,tail,index_210) = queue_211,
inference(copy,[status(thm)],[c_501]) ).
fof(hyp246,axiom,
queue_215 = store(q40,seq,earray_214),
file('theBenchmark.p',hyp246) ).
cnf(c_503,plain,
queue_215 = store(q40,seq,earray_214),
inference(clausify,[status(thm)],[hyp246]) ).
cnf(c_504,plain,
store(q40,seq,earray_214) = queue_215,
inference(copy,[status(thm)],[c_503]) ).
fof(hyp247,axiom,
queue_217 = store(queue_215,tail,index_216),
file('theBenchmark.p',hyp247) ).
cnf(c_505,plain,
queue_217 = store(queue_215,tail,index_216),
inference(clausify,[status(thm)],[hyp247]) ).
cnf(c_506,plain,
store(queue_215,tail,index_216) = queue_217,
inference(copy,[status(thm)],[c_505]) ).
fof(hyp248,axiom,
queue_221 = store(q41,seq,earray_220),
file('theBenchmark.p',hyp248) ).
cnf(c_507,plain,
queue_221 = store(q41,seq,earray_220),
inference(clausify,[status(thm)],[hyp248]) ).
cnf(c_508,plain,
store(q41,seq,earray_220) = queue_221,
inference(copy,[status(thm)],[c_507]) ).
fof(hyp249,axiom,
queue_223 = store(queue_221,tail,index_222),
file('theBenchmark.p',hyp249) ).
cnf(c_509,plain,
queue_223 = store(queue_221,tail,index_222),
inference(clausify,[status(thm)],[hyp249]) ).
cnf(c_510,plain,
store(queue_221,tail,index_222) = queue_223,
inference(copy,[status(thm)],[c_509]) ).
fof(hyp250,axiom,
queue_227 = store(q42,seq,earray_226),
file('theBenchmark.p',hyp250) ).
cnf(c_511,plain,
queue_227 = store(q42,seq,earray_226),
inference(clausify,[status(thm)],[hyp250]) ).
cnf(c_512,plain,
store(q42,seq,earray_226) = queue_227,
inference(copy,[status(thm)],[c_511]) ).
fof(hyp251,axiom,
queue_229 = store(queue_227,tail,index_228),
file('theBenchmark.p',hyp251) ).
cnf(c_513,plain,
queue_229 = store(queue_227,tail,index_228),
inference(clausify,[status(thm)],[hyp251]) ).
cnf(c_514,plain,
store(queue_227,tail,index_228) = queue_229,
inference(copy,[status(thm)],[c_513]) ).
fof(hyp252,axiom,
queue_23 = store(q11,seq,earray_22),
file('theBenchmark.p',hyp252) ).
cnf(c_515,plain,
queue_23 = store(q11,seq,earray_22),
inference(clausify,[status(thm)],[hyp252]) ).
cnf(c_516,plain,
store(q11,seq,earray_22) = queue_23,
inference(copy,[status(thm)],[c_515]) ).
fof(hyp253,axiom,
queue_233 = store(q43,seq,earray_232),
file('theBenchmark.p',hyp253) ).
cnf(c_517,plain,
queue_233 = store(q43,seq,earray_232),
inference(clausify,[status(thm)],[hyp253]) ).
cnf(c_518,plain,
store(q43,seq,earray_232) = queue_233,
inference(copy,[status(thm)],[c_517]) ).
fof(hyp254,axiom,
queue_235 = store(queue_233,tail,index_234),
file('theBenchmark.p',hyp254) ).
cnf(c_519,plain,
queue_235 = store(queue_233,tail,index_234),
inference(clausify,[status(thm)],[hyp254]) ).
cnf(c_520,plain,
store(queue_233,tail,index_234) = queue_235,
inference(copy,[status(thm)],[c_519]) ).
fof(hyp255,axiom,
queue_239 = store(q44,seq,earray_238),
file('theBenchmark.p',hyp255) ).
cnf(c_521,plain,
queue_239 = store(q44,seq,earray_238),
inference(clausify,[status(thm)],[hyp255]) ).
cnf(c_522,plain,
store(q44,seq,earray_238) = queue_239,
inference(copy,[status(thm)],[c_521]) ).
fof(hyp256,axiom,
queue_241 = store(queue_239,tail,index_240),
file('theBenchmark.p',hyp256) ).
cnf(c_523,plain,
queue_241 = store(queue_239,tail,index_240),
inference(clausify,[status(thm)],[hyp256]) ).
cnf(c_524,plain,
store(queue_239,tail,index_240) = queue_241,
inference(copy,[status(thm)],[c_523]) ).
fof(hyp257,axiom,
queue_245 = store(q45,seq,earray_244),
file('theBenchmark.p',hyp257) ).
cnf(c_525,plain,
queue_245 = store(q45,seq,earray_244),
inference(clausify,[status(thm)],[hyp257]) ).
cnf(c_526,plain,
store(q45,seq,earray_244) = queue_245,
inference(copy,[status(thm)],[c_525]) ).
fof(hyp258,axiom,
queue_247 = store(queue_245,tail,index_246),
file('theBenchmark.p',hyp258) ).
cnf(c_527,plain,
queue_247 = store(queue_245,tail,index_246),
inference(clausify,[status(thm)],[hyp258]) ).
cnf(c_528,plain,
store(queue_245,tail,index_246) = queue_247,
inference(copy,[status(thm)],[c_527]) ).
fof(hyp259,axiom,
queue_25 = store(queue_23,tail,index_24),
file('theBenchmark.p',hyp259) ).
cnf(c_529,plain,
queue_25 = store(queue_23,tail,index_24),
inference(clausify,[status(thm)],[hyp259]) ).
cnf(c_530,plain,
store(queue_23,tail,index_24) = queue_25,
inference(copy,[status(thm)],[c_529]) ).
fof(hyp260,axiom,
queue_251 = store(q46,seq,earray_250),
file('theBenchmark.p',hyp260) ).
cnf(c_531,plain,
queue_251 = store(q46,seq,earray_250),
inference(clausify,[status(thm)],[hyp260]) ).
cnf(c_532,plain,
store(q46,seq,earray_250) = queue_251,
inference(copy,[status(thm)],[c_531]) ).
fof(hyp261,axiom,
queue_253 = store(queue_251,tail,index_252),
file('theBenchmark.p',hyp261) ).
cnf(c_533,plain,
queue_253 = store(queue_251,tail,index_252),
inference(clausify,[status(thm)],[hyp261]) ).
cnf(c_534,plain,
store(queue_251,tail,index_252) = queue_253,
inference(copy,[status(thm)],[c_533]) ).
fof(hyp262,axiom,
queue_257 = store(q47,seq,earray_256),
file('theBenchmark.p',hyp262) ).
cnf(c_535,plain,
queue_257 = store(q47,seq,earray_256),
inference(clausify,[status(thm)],[hyp262]) ).
cnf(c_536,plain,
store(q47,seq,earray_256) = queue_257,
inference(copy,[status(thm)],[c_535]) ).
fof(hyp263,axiom,
queue_259 = store(queue_257,tail,index_258),
file('theBenchmark.p',hyp263) ).
cnf(c_537,plain,
queue_259 = store(queue_257,tail,index_258),
inference(clausify,[status(thm)],[hyp263]) ).
cnf(c_538,plain,
store(queue_257,tail,index_258) = queue_259,
inference(copy,[status(thm)],[c_537]) ).
fof(hyp264,axiom,
queue_263 = store(q48,seq,earray_262),
file('theBenchmark.p',hyp264) ).
cnf(c_539,plain,
queue_263 = store(q48,seq,earray_262),
inference(clausify,[status(thm)],[hyp264]) ).
cnf(c_540,plain,
store(q48,seq,earray_262) = queue_263,
inference(copy,[status(thm)],[c_539]) ).
fof(hyp265,axiom,
queue_265 = store(queue_263,tail,index_264),
file('theBenchmark.p',hyp265) ).
cnf(c_541,plain,
queue_265 = store(queue_263,tail,index_264),
inference(clausify,[status(thm)],[hyp265]) ).
cnf(c_542,plain,
store(queue_263,tail,index_264) = queue_265,
inference(copy,[status(thm)],[c_541]) ).
fof(hyp266,axiom,
queue_269 = store(q4,seq,earray_268),
file('theBenchmark.p',hyp266) ).
cnf(c_543,plain,
queue_269 = store(q4,seq,earray_268),
inference(clausify,[status(thm)],[hyp266]) ).
cnf(c_544,plain,
store(q4,seq,earray_268) = queue_269,
inference(copy,[status(thm)],[c_543]) ).
fof(hyp267,axiom,
queue_271 = store(queue_269,tail,index_270),
file('theBenchmark.p',hyp267) ).
cnf(c_545,plain,
queue_271 = store(queue_269,tail,index_270),
inference(clausify,[status(thm)],[hyp267]) ).
cnf(c_546,plain,
store(queue_269,tail,index_270) = queue_271,
inference(copy,[status(thm)],[c_545]) ).
fof(hyp268,axiom,
queue_275 = store(q5,seq,earray_274),
file('theBenchmark.p',hyp268) ).
cnf(c_547,plain,
queue_275 = store(q5,seq,earray_274),
inference(clausify,[status(thm)],[hyp268]) ).
cnf(c_548,plain,
store(q5,seq,earray_274) = queue_275,
inference(copy,[status(thm)],[c_547]) ).
fof(hyp269,axiom,
queue_277 = store(queue_275,tail,index_276),
file('theBenchmark.p',hyp269) ).
cnf(c_549,plain,
queue_277 = store(queue_275,tail,index_276),
inference(clausify,[status(thm)],[hyp269]) ).
cnf(c_550,plain,
store(queue_275,tail,index_276) = queue_277,
inference(copy,[status(thm)],[c_549]) ).
fof(hyp270,axiom,
queue_281 = store(q6,seq,earray_280),
file('theBenchmark.p',hyp270) ).
cnf(c_551,plain,
queue_281 = store(q6,seq,earray_280),
inference(clausify,[status(thm)],[hyp270]) ).
cnf(c_552,plain,
store(q6,seq,earray_280) = queue_281,
inference(copy,[status(thm)],[c_551]) ).
fof(hyp271,axiom,
queue_283 = store(queue_281,tail,index_282),
file('theBenchmark.p',hyp271) ).
cnf(c_553,plain,
queue_283 = store(queue_281,tail,index_282),
inference(clausify,[status(thm)],[hyp271]) ).
cnf(c_554,plain,
store(queue_281,tail,index_282) = queue_283,
inference(copy,[status(thm)],[c_553]) ).
fof(hyp272,axiom,
queue_287 = store(q7,seq,earray_286),
file('theBenchmark.p',hyp272) ).
cnf(c_555,plain,
queue_287 = store(q7,seq,earray_286),
inference(clausify,[status(thm)],[hyp272]) ).
cnf(c_556,plain,
store(q7,seq,earray_286) = queue_287,
inference(copy,[status(thm)],[c_555]) ).
fof(hyp273,axiom,
queue_289 = store(queue_287,tail,index_288),
file('theBenchmark.p',hyp273) ).
cnf(c_557,plain,
queue_289 = store(queue_287,tail,index_288),
inference(clausify,[status(thm)],[hyp273]) ).
cnf(c_558,plain,
store(queue_287,tail,index_288) = queue_289,
inference(copy,[status(thm)],[c_557]) ).
fof(hyp274,axiom,
queue_29 = store(q12,seq,earray_28),
file('theBenchmark.p',hyp274) ).
cnf(c_559,plain,
queue_29 = store(q12,seq,earray_28),
inference(clausify,[status(thm)],[hyp274]) ).
cnf(c_560,plain,
store(q12,seq,earray_28) = queue_29,
inference(copy,[status(thm)],[c_559]) ).
fof(hyp275,axiom,
queue_293 = store(q8,seq,earray_292),
file('theBenchmark.p',hyp275) ).
cnf(c_561,plain,
queue_293 = store(q8,seq,earray_292),
inference(clausify,[status(thm)],[hyp275]) ).
cnf(c_562,plain,
store(q8,seq,earray_292) = queue_293,
inference(copy,[status(thm)],[c_561]) ).
fof(hyp276,axiom,
queue_295 = store(queue_293,tail,index_294),
file('theBenchmark.p',hyp276) ).
cnf(c_563,plain,
queue_295 = store(queue_293,tail,index_294),
inference(clausify,[status(thm)],[hyp276]) ).
cnf(c_564,plain,
store(queue_293,tail,index_294) = queue_295,
inference(copy,[status(thm)],[c_563]) ).
fof(hyp277,axiom,
queue_31 = store(queue_29,tail,index_30),
file('theBenchmark.p',hyp277) ).
cnf(c_565,plain,
queue_31 = store(queue_29,tail,index_30),
inference(clausify,[status(thm)],[hyp277]) ).
cnf(c_566,plain,
store(queue_29,tail,index_30) = queue_31,
inference(copy,[status(thm)],[c_565]) ).
fof(hyp278,axiom,
queue_35 = store(q13,seq,earray_34),
file('theBenchmark.p',hyp278) ).
cnf(c_567,plain,
queue_35 = store(q13,seq,earray_34),
inference(clausify,[status(thm)],[hyp278]) ).
cnf(c_568,plain,
store(q13,seq,earray_34) = queue_35,
inference(copy,[status(thm)],[c_567]) ).
fof(hyp279,axiom,
queue_37 = store(queue_35,tail,index_36),
file('theBenchmark.p',hyp279) ).
cnf(c_569,plain,
queue_37 = store(queue_35,tail,index_36),
inference(clausify,[status(thm)],[hyp279]) ).
cnf(c_570,plain,
store(queue_35,tail,index_36) = queue_37,
inference(copy,[status(thm)],[c_569]) ).
fof(hyp280,axiom,
queue_41 = store(q14,seq,earray_40),
file('theBenchmark.p',hyp280) ).
cnf(c_571,plain,
queue_41 = store(q14,seq,earray_40),
inference(clausify,[status(thm)],[hyp280]) ).
cnf(c_572,plain,
store(q14,seq,earray_40) = queue_41,
inference(copy,[status(thm)],[c_571]) ).
fof(hyp281,axiom,
queue_43 = store(queue_41,tail,index_42),
file('theBenchmark.p',hyp281) ).
cnf(c_573,plain,
queue_43 = store(queue_41,tail,index_42),
inference(clausify,[status(thm)],[hyp281]) ).
cnf(c_574,plain,
store(queue_41,tail,index_42) = queue_43,
inference(copy,[status(thm)],[c_573]) ).
fof(hyp282,axiom,
queue_47 = store(q15,seq,earray_46),
file('theBenchmark.p',hyp282) ).
cnf(c_575,plain,
queue_47 = store(q15,seq,earray_46),
inference(clausify,[status(thm)],[hyp282]) ).
cnf(c_576,plain,
store(q15,seq,earray_46) = queue_47,
inference(copy,[status(thm)],[c_575]) ).
fof(hyp283,axiom,
queue_49 = store(queue_47,tail,index_48),
file('theBenchmark.p',hyp283) ).
cnf(c_577,plain,
queue_49 = store(queue_47,tail,index_48),
inference(clausify,[status(thm)],[hyp283]) ).
cnf(c_578,plain,
store(queue_47,tail,index_48) = queue_49,
inference(copy,[status(thm)],[c_577]) ).
fof(hyp284,axiom,
queue_5 = store(q0,seq,earray_4),
file('theBenchmark.p',hyp284) ).
cnf(c_579,plain,
queue_5 = store(q0,seq,earray_4),
inference(clausify,[status(thm)],[hyp284]) ).
cnf(c_580,plain,
store(q0,seq,earray_4) = queue_5,
inference(copy,[status(thm)],[c_579]) ).
fof(hyp285,axiom,
queue_53 = store(q16,seq,earray_52),
file('theBenchmark.p',hyp285) ).
cnf(c_581,plain,
queue_53 = store(q16,seq,earray_52),
inference(clausify,[status(thm)],[hyp285]) ).
cnf(c_582,plain,
store(q16,seq,earray_52) = queue_53,
inference(copy,[status(thm)],[c_581]) ).
fof(hyp286,axiom,
queue_55 = store(queue_53,tail,index_54),
file('theBenchmark.p',hyp286) ).
cnf(c_583,plain,
queue_55 = store(queue_53,tail,index_54),
inference(clausify,[status(thm)],[hyp286]) ).
cnf(c_584,plain,
store(queue_53,tail,index_54) = queue_55,
inference(copy,[status(thm)],[c_583]) ).
fof(hyp287,axiom,
queue_59 = store(q17,seq,earray_58),
file('theBenchmark.p',hyp287) ).
cnf(c_585,plain,
queue_59 = store(q17,seq,earray_58),
inference(clausify,[status(thm)],[hyp287]) ).
cnf(c_586,plain,
store(q17,seq,earray_58) = queue_59,
inference(copy,[status(thm)],[c_585]) ).
fof(hyp288,axiom,
queue_61 = store(queue_59,tail,index_60),
file('theBenchmark.p',hyp288) ).
cnf(c_587,plain,
queue_61 = store(queue_59,tail,index_60),
inference(clausify,[status(thm)],[hyp288]) ).
cnf(c_588,plain,
store(queue_59,tail,index_60) = queue_61,
inference(copy,[status(thm)],[c_587]) ).
fof(hyp289,axiom,
queue_65 = store(q18,seq,earray_64),
file('theBenchmark.p',hyp289) ).
cnf(c_589,plain,
queue_65 = store(q18,seq,earray_64),
inference(clausify,[status(thm)],[hyp289]) ).
cnf(c_590,plain,
store(q18,seq,earray_64) = queue_65,
inference(copy,[status(thm)],[c_589]) ).
fof(hyp290,axiom,
queue_67 = store(queue_65,tail,index_66),
file('theBenchmark.p',hyp290) ).
cnf(c_591,plain,
queue_67 = store(queue_65,tail,index_66),
inference(clausify,[status(thm)],[hyp290]) ).
cnf(c_592,plain,
store(queue_65,tail,index_66) = queue_67,
inference(copy,[status(thm)],[c_591]) ).
fof(hyp291,axiom,
queue_7 = store(queue_5,tail,index_6),
file('theBenchmark.p',hyp291) ).
cnf(c_593,plain,
queue_7 = store(queue_5,tail,index_6),
inference(clausify,[status(thm)],[hyp291]) ).
cnf(c_594,plain,
store(queue_5,tail,index_6) = queue_7,
inference(copy,[status(thm)],[c_593]) ).
fof(hyp292,axiom,
queue_71 = store(q1,seq,earray_70),
file('theBenchmark.p',hyp292) ).
cnf(c_595,plain,
queue_71 = store(q1,seq,earray_70),
inference(clausify,[status(thm)],[hyp292]) ).
cnf(c_596,plain,
store(q1,seq,earray_70) = queue_71,
inference(copy,[status(thm)],[c_595]) ).
fof(hyp293,axiom,
queue_73 = store(queue_71,tail,index_72),
file('theBenchmark.p',hyp293) ).
cnf(c_597,plain,
queue_73 = store(queue_71,tail,index_72),
inference(clausify,[status(thm)],[hyp293]) ).
cnf(c_598,plain,
store(queue_71,tail,index_72) = queue_73,
inference(copy,[status(thm)],[c_597]) ).
fof(hyp294,axiom,
queue_77 = store(q19,seq,earray_76),
file('theBenchmark.p',hyp294) ).
cnf(c_599,plain,
queue_77 = store(q19,seq,earray_76),
inference(clausify,[status(thm)],[hyp294]) ).
cnf(c_600,plain,
store(q19,seq,earray_76) = queue_77,
inference(copy,[status(thm)],[c_599]) ).
fof(hyp295,axiom,
queue_79 = store(queue_77,tail,index_78),
file('theBenchmark.p',hyp295) ).
cnf(c_601,plain,
queue_79 = store(queue_77,tail,index_78),
inference(clausify,[status(thm)],[hyp295]) ).
cnf(c_602,plain,
store(queue_77,tail,index_78) = queue_79,
inference(copy,[status(thm)],[c_601]) ).
fof(hyp296,axiom,
queue_83 = store(q20,seq,earray_82),
file('theBenchmark.p',hyp296) ).
cnf(c_603,plain,
queue_83 = store(q20,seq,earray_82),
inference(clausify,[status(thm)],[hyp296]) ).
cnf(c_604,plain,
store(q20,seq,earray_82) = queue_83,
inference(copy,[status(thm)],[c_603]) ).
fof(hyp297,axiom,
queue_85 = store(queue_83,tail,index_84),
file('theBenchmark.p',hyp297) ).
cnf(c_605,plain,
queue_85 = store(queue_83,tail,index_84),
inference(clausify,[status(thm)],[hyp297]) ).
cnf(c_606,plain,
store(queue_83,tail,index_84) = queue_85,
inference(copy,[status(thm)],[c_605]) ).
fof(hyp298,axiom,
queue_89 = store(q21,seq,earray_88),
file('theBenchmark.p',hyp298) ).
cnf(c_607,plain,
queue_89 = store(q21,seq,earray_88),
inference(clausify,[status(thm)],[hyp298]) ).
cnf(c_608,plain,
store(q21,seq,earray_88) = queue_89,
inference(copy,[status(thm)],[c_607]) ).
fof(hyp299,axiom,
queue_91 = store(queue_89,tail,index_90),
file('theBenchmark.p',hyp299) ).
cnf(c_609,plain,
queue_91 = store(queue_89,tail,index_90),
inference(clausify,[status(thm)],[hyp299]) ).
cnf(c_610,plain,
store(queue_89,tail,index_90) = queue_91,
inference(copy,[status(thm)],[c_609]) ).
fof(hyp300,axiom,
queue_95 = store(q22,seq,earray_94),
file('theBenchmark.p',hyp300) ).
cnf(c_611,plain,
queue_95 = store(q22,seq,earray_94),
inference(clausify,[status(thm)],[hyp300]) ).
cnf(c_612,plain,
store(q22,seq,earray_94) = queue_95,
inference(copy,[status(thm)],[c_611]) ).
fof(hyp301,axiom,
queue_97 = store(queue_95,tail,index_96),
file('theBenchmark.p',hyp301) ).
cnf(c_613,plain,
queue_97 = store(queue_95,tail,index_96),
inference(clausify,[status(thm)],[hyp301]) ).
cnf(c_614,plain,
store(queue_95,tail,index_96) = queue_97,
inference(copy,[status(thm)],[c_613]) ).
fof(hyp302,axiom,
q0 = queue_1,
file('theBenchmark.p',hyp302) ).
cnf(c_615,plain,
q0 = queue_1,
inference(clausify,[status(thm)],[hyp302]) ).
cnf(c_616,plain,
queue_1 = q0,
inference(copy,[status(thm)],[c_615]) ).
fof(hyp303,axiom,
q1 = queue_7,
file('theBenchmark.p',hyp303) ).
cnf(c_617,plain,
q1 = queue_7,
inference(clausify,[status(thm)],[hyp303]) ).
cnf(c_618,plain,
queue_7 = q1,
inference(copy,[status(thm)],[c_617]) ).
fof(hyp304,axiom,
q10 = queue_13,
file('theBenchmark.p',hyp304) ).
cnf(c_619,plain,
q10 = queue_13,
inference(clausify,[status(thm)],[hyp304]) ).
cnf(c_620,plain,
queue_13 = q10,
inference(copy,[status(thm)],[c_619]) ).
fof(hyp305,axiom,
q11 = queue_19,
file('theBenchmark.p',hyp305) ).
cnf(c_621,plain,
q11 = queue_19,
inference(clausify,[status(thm)],[hyp305]) ).
cnf(c_622,plain,
queue_19 = q11,
inference(copy,[status(thm)],[c_621]) ).
fof(hyp306,axiom,
q12 = queue_25,
file('theBenchmark.p',hyp306) ).
cnf(c_623,plain,
q12 = queue_25,
inference(clausify,[status(thm)],[hyp306]) ).
cnf(c_624,plain,
queue_25 = q12,
inference(copy,[status(thm)],[c_623]) ).
fof(hyp307,axiom,
q13 = queue_31,
file('theBenchmark.p',hyp307) ).
cnf(c_625,plain,
q13 = queue_31,
inference(clausify,[status(thm)],[hyp307]) ).
cnf(c_626,plain,
queue_31 = q13,
inference(copy,[status(thm)],[c_625]) ).
fof(hyp308,axiom,
q14 = queue_37,
file('theBenchmark.p',hyp308) ).
cnf(c_627,plain,
q14 = queue_37,
inference(clausify,[status(thm)],[hyp308]) ).
cnf(c_628,plain,
queue_37 = q14,
inference(copy,[status(thm)],[c_627]) ).
fof(hyp309,axiom,
q15 = queue_43,
file('theBenchmark.p',hyp309) ).
cnf(c_629,plain,
q15 = queue_43,
inference(clausify,[status(thm)],[hyp309]) ).
cnf(c_630,plain,
queue_43 = q15,
inference(copy,[status(thm)],[c_629]) ).
fof(hyp310,axiom,
q16 = queue_49,
file('theBenchmark.p',hyp310) ).
cnf(c_631,plain,
q16 = queue_49,
inference(clausify,[status(thm)],[hyp310]) ).
cnf(c_632,plain,
queue_49 = q16,
inference(copy,[status(thm)],[c_631]) ).
fof(hyp311,axiom,
q17 = queue_55,
file('theBenchmark.p',hyp311) ).
cnf(c_633,plain,
q17 = queue_55,
inference(clausify,[status(thm)],[hyp311]) ).
cnf(c_634,plain,
queue_55 = q17,
inference(copy,[status(thm)],[c_633]) ).
fof(hyp312,axiom,
q18 = queue_61,
file('theBenchmark.p',hyp312) ).
cnf(c_635,plain,
q18 = queue_61,
inference(clausify,[status(thm)],[hyp312]) ).
cnf(c_636,plain,
queue_61 = q18,
inference(copy,[status(thm)],[c_635]) ).
fof(hyp313,axiom,
q19 = queue_67,
file('theBenchmark.p',hyp313) ).
cnf(c_637,plain,
q19 = queue_67,
inference(clausify,[status(thm)],[hyp313]) ).
cnf(c_638,plain,
queue_67 = q19,
inference(copy,[status(thm)],[c_637]) ).
fof(hyp314,axiom,
q2 = queue_73,
file('theBenchmark.p',hyp314) ).
cnf(c_639,plain,
q2 = queue_73,
inference(clausify,[status(thm)],[hyp314]) ).
cnf(c_640,plain,
queue_73 = q2,
inference(copy,[status(thm)],[c_639]) ).
fof(hyp315,axiom,
q20 = queue_79,
file('theBenchmark.p',hyp315) ).
cnf(c_641,plain,
q20 = queue_79,
inference(clausify,[status(thm)],[hyp315]) ).
cnf(c_642,plain,
queue_79 = q20,
inference(copy,[status(thm)],[c_641]) ).
fof(hyp316,axiom,
q21 = queue_85,
file('theBenchmark.p',hyp316) ).
cnf(c_643,plain,
q21 = queue_85,
inference(clausify,[status(thm)],[hyp316]) ).
cnf(c_644,plain,
queue_85 = q21,
inference(copy,[status(thm)],[c_643]) ).
fof(hyp317,axiom,
q22 = queue_91,
file('theBenchmark.p',hyp317) ).
cnf(c_645,plain,
q22 = queue_91,
inference(clausify,[status(thm)],[hyp317]) ).
cnf(c_646,plain,
queue_91 = q22,
inference(copy,[status(thm)],[c_645]) ).
fof(hyp318,axiom,
q23 = queue_97,
file('theBenchmark.p',hyp318) ).
cnf(c_647,plain,
q23 = queue_97,
inference(clausify,[status(thm)],[hyp318]) ).
cnf(c_648,plain,
queue_97 = q23,
inference(copy,[status(thm)],[c_647]) ).
fof(hyp319,axiom,
q24 = queue_103,
file('theBenchmark.p',hyp319) ).
cnf(c_649,plain,
q24 = queue_103,
inference(clausify,[status(thm)],[hyp319]) ).
cnf(c_650,plain,
queue_103 = q24,
inference(copy,[status(thm)],[c_649]) ).
fof(hyp320,axiom,
q25 = queue_109,
file('theBenchmark.p',hyp320) ).
cnf(c_651,plain,
q25 = queue_109,
inference(clausify,[status(thm)],[hyp320]) ).
cnf(c_652,plain,
queue_109 = q25,
inference(copy,[status(thm)],[c_651]) ).
fof(hyp321,axiom,
q26 = queue_115,
file('theBenchmark.p',hyp321) ).
cnf(c_653,plain,
q26 = queue_115,
inference(clausify,[status(thm)],[hyp321]) ).
cnf(c_654,plain,
queue_115 = q26,
inference(copy,[status(thm)],[c_653]) ).
fof(hyp322,axiom,
q27 = queue_121,
file('theBenchmark.p',hyp322) ).
cnf(c_655,plain,
q27 = queue_121,
inference(clausify,[status(thm)],[hyp322]) ).
cnf(c_656,plain,
queue_121 = q27,
inference(copy,[status(thm)],[c_655]) ).
fof(hyp323,axiom,
q28 = queue_127,
file('theBenchmark.p',hyp323) ).
cnf(c_657,plain,
q28 = queue_127,
inference(clausify,[status(thm)],[hyp323]) ).
cnf(c_658,plain,
queue_127 = q28,
inference(copy,[status(thm)],[c_657]) ).
fof(hyp324,axiom,
q29 = queue_133,
file('theBenchmark.p',hyp324) ).
cnf(c_659,plain,
q29 = queue_133,
inference(clausify,[status(thm)],[hyp324]) ).
cnf(c_660,plain,
queue_133 = q29,
inference(copy,[status(thm)],[c_659]) ).
fof(hyp325,axiom,
q3 = queue_139,
file('theBenchmark.p',hyp325) ).
cnf(c_661,plain,
q3 = queue_139,
inference(clausify,[status(thm)],[hyp325]) ).
cnf(c_662,plain,
queue_139 = q3,
inference(copy,[status(thm)],[c_661]) ).
fof(hyp326,axiom,
q30 = queue_145,
file('theBenchmark.p',hyp326) ).
cnf(c_663,plain,
q30 = queue_145,
inference(clausify,[status(thm)],[hyp326]) ).
cnf(c_664,plain,
queue_145 = q30,
inference(copy,[status(thm)],[c_663]) ).
fof(hyp327,axiom,
q31 = queue_151,
file('theBenchmark.p',hyp327) ).
cnf(c_665,plain,
q31 = queue_151,
inference(clausify,[status(thm)],[hyp327]) ).
cnf(c_666,plain,
queue_151 = q31,
inference(copy,[status(thm)],[c_665]) ).
fof(hyp328,axiom,
q32 = queue_157,
file('theBenchmark.p',hyp328) ).
cnf(c_667,plain,
q32 = queue_157,
inference(clausify,[status(thm)],[hyp328]) ).
cnf(c_668,plain,
queue_157 = q32,
inference(copy,[status(thm)],[c_667]) ).
fof(hyp329,axiom,
q33 = queue_163,
file('theBenchmark.p',hyp329) ).
cnf(c_669,plain,
q33 = queue_163,
inference(clausify,[status(thm)],[hyp329]) ).
cnf(c_670,plain,
queue_163 = q33,
inference(copy,[status(thm)],[c_669]) ).
fof(hyp330,axiom,
q34 = queue_169,
file('theBenchmark.p',hyp330) ).
cnf(c_671,plain,
q34 = queue_169,
inference(clausify,[status(thm)],[hyp330]) ).
cnf(c_672,plain,
queue_169 = q34,
inference(copy,[status(thm)],[c_671]) ).
fof(hyp331,axiom,
q35 = queue_175,
file('theBenchmark.p',hyp331) ).
cnf(c_673,plain,
q35 = queue_175,
inference(clausify,[status(thm)],[hyp331]) ).
cnf(c_674,plain,
queue_175 = q35,
inference(copy,[status(thm)],[c_673]) ).
fof(hyp332,axiom,
q36 = queue_181,
file('theBenchmark.p',hyp332) ).
cnf(c_675,plain,
q36 = queue_181,
inference(clausify,[status(thm)],[hyp332]) ).
cnf(c_676,plain,
queue_181 = q36,
inference(copy,[status(thm)],[c_675]) ).
fof(hyp333,axiom,
q37 = queue_187,
file('theBenchmark.p',hyp333) ).
cnf(c_677,plain,
q37 = queue_187,
inference(clausify,[status(thm)],[hyp333]) ).
cnf(c_678,plain,
queue_187 = q37,
inference(copy,[status(thm)],[c_677]) ).
fof(hyp334,axiom,
q38 = queue_193,
file('theBenchmark.p',hyp334) ).
cnf(c_679,plain,
q38 = queue_193,
inference(clausify,[status(thm)],[hyp334]) ).
cnf(c_680,plain,
queue_193 = q38,
inference(copy,[status(thm)],[c_679]) ).
fof(hyp335,axiom,
q39 = queue_199,
file('theBenchmark.p',hyp335) ).
cnf(c_681,plain,
q39 = queue_199,
inference(clausify,[status(thm)],[hyp335]) ).
cnf(c_682,plain,
queue_199 = q39,
inference(copy,[status(thm)],[c_681]) ).
fof(hyp336,axiom,
q4 = queue_205,
file('theBenchmark.p',hyp336) ).
cnf(c_683,plain,
q4 = queue_205,
inference(clausify,[status(thm)],[hyp336]) ).
cnf(c_684,plain,
queue_205 = q4,
inference(copy,[status(thm)],[c_683]) ).
fof(hyp337,axiom,
q40 = queue_211,
file('theBenchmark.p',hyp337) ).
cnf(c_685,plain,
q40 = queue_211,
inference(clausify,[status(thm)],[hyp337]) ).
cnf(c_686,plain,
queue_211 = q40,
inference(copy,[status(thm)],[c_685]) ).
fof(hyp338,axiom,
q41 = queue_217,
file('theBenchmark.p',hyp338) ).
cnf(c_687,plain,
q41 = queue_217,
inference(clausify,[status(thm)],[hyp338]) ).
cnf(c_688,plain,
queue_217 = q41,
inference(copy,[status(thm)],[c_687]) ).
fof(hyp339,axiom,
q42 = queue_223,
file('theBenchmark.p',hyp339) ).
cnf(c_689,plain,
q42 = queue_223,
inference(clausify,[status(thm)],[hyp339]) ).
cnf(c_690,plain,
queue_223 = q42,
inference(copy,[status(thm)],[c_689]) ).
fof(hyp340,axiom,
q43 = queue_229,
file('theBenchmark.p',hyp340) ).
cnf(c_691,plain,
q43 = queue_229,
inference(clausify,[status(thm)],[hyp340]) ).
cnf(c_692,plain,
queue_229 = q43,
inference(copy,[status(thm)],[c_691]) ).
fof(hyp341,axiom,
q44 = queue_235,
file('theBenchmark.p',hyp341) ).
cnf(c_693,plain,
q44 = queue_235,
inference(clausify,[status(thm)],[hyp341]) ).
cnf(c_694,plain,
queue_235 = q44,
inference(copy,[status(thm)],[c_693]) ).
fof(hyp342,axiom,
q45 = queue_241,
file('theBenchmark.p',hyp342) ).
cnf(c_695,plain,
q45 = queue_241,
inference(clausify,[status(thm)],[hyp342]) ).
cnf(c_696,plain,
queue_241 = q45,
inference(copy,[status(thm)],[c_695]) ).
fof(hyp343,axiom,
q46 = queue_247,
file('theBenchmark.p',hyp343) ).
cnf(c_697,plain,
q46 = queue_247,
inference(clausify,[status(thm)],[hyp343]) ).
cnf(c_698,plain,
queue_247 = q46,
inference(copy,[status(thm)],[c_697]) ).
fof(hyp344,axiom,
q47 = queue_253,
file('theBenchmark.p',hyp344) ).
cnf(c_699,plain,
q47 = queue_253,
inference(clausify,[status(thm)],[hyp344]) ).
cnf(c_700,plain,
queue_253 = q47,
inference(copy,[status(thm)],[c_699]) ).
fof(hyp345,axiom,
q48 = queue_259,
file('theBenchmark.p',hyp345) ).
cnf(c_701,plain,
q48 = queue_259,
inference(clausify,[status(thm)],[hyp345]) ).
cnf(c_702,plain,
queue_259 = q48,
inference(copy,[status(thm)],[c_701]) ).
fof(hyp346,axiom,
q49 = queue_265,
file('theBenchmark.p',hyp346) ).
cnf(c_703,plain,
q49 = queue_265,
inference(clausify,[status(thm)],[hyp346]) ).
cnf(c_704,plain,
queue_265 = q49,
inference(copy,[status(thm)],[c_703]) ).
fof(hyp347,axiom,
q5 = queue_271,
file('theBenchmark.p',hyp347) ).
cnf(c_705,plain,
q5 = queue_271,
inference(clausify,[status(thm)],[hyp347]) ).
cnf(c_706,plain,
queue_271 = q5,
inference(copy,[status(thm)],[c_705]) ).
fof(hyp348,axiom,
q6 = queue_277,
file('theBenchmark.p',hyp348) ).
cnf(c_707,plain,
q6 = queue_277,
inference(clausify,[status(thm)],[hyp348]) ).
cnf(c_708,plain,
queue_277 = q6,
inference(copy,[status(thm)],[c_707]) ).
fof(hyp349,axiom,
q7 = queue_283,
file('theBenchmark.p',hyp349) ).
cnf(c_709,plain,
q7 = queue_283,
inference(clausify,[status(thm)],[hyp349]) ).
cnf(c_710,plain,
queue_283 = q7,
inference(copy,[status(thm)],[c_709]) ).
fof(hyp350,axiom,
q8 = queue_289,
file('theBenchmark.p',hyp350) ).
cnf(c_711,plain,
q8 = queue_289,
inference(clausify,[status(thm)],[hyp350]) ).
cnf(c_712,plain,
queue_289 = q8,
inference(copy,[status(thm)],[c_711]) ).
fof(hyp351,axiom,
q9 = queue_295,
file('theBenchmark.p',hyp351) ).
cnf(c_713,plain,
q9 = queue_295,
inference(clausify,[status(thm)],[hyp351]) ).
cnf(c_714,plain,
queue_295 = q9,
inference(copy,[status(thm)],[c_713]) ).
fof(goal,axiom,
elem_298 != elem_301,
file('theBenchmark.p',goal) ).
cnf(c_715,plain,
elem_298 != elem_301,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_716,plain,
elem_301 != elem_298,
inference(copy,[status(thm)],[c_715]) ).
cnf(c_717,plain,
store(q,head,index_0) = q0,
inference(paramod,[status(thm)],[c_616,c_418]) ).
cnf(c_718,plain,
store(queue_5,tail,index_6) = q1,
inference(paramod,[status(thm)],[c_618,c_594]) ).
cnf(c_719,plain,
store(queue_11,tail,index_12) = q10,
inference(paramod,[status(thm)],[c_620,c_442]) ).
cnf(c_720,plain,
store(queue_17,tail,index_18) = q11,
inference(paramod,[status(thm)],[c_622,c_486]) ).
cnf(c_721,plain,
store(queue_23,tail,index_24) = q12,
inference(paramod,[status(thm)],[c_624,c_530]) ).
cnf(c_722,plain,
store(queue_29,tail,index_30) = q13,
inference(paramod,[status(thm)],[c_626,c_566]) ).
cnf(c_723,plain,
store(queue_35,tail,index_36) = q14,
inference(paramod,[status(thm)],[c_628,c_570]) ).
cnf(c_724,plain,
store(queue_41,tail,index_42) = q15,
inference(paramod,[status(thm)],[c_630,c_574]) ).
cnf(c_725,plain,
store(queue_47,tail,index_48) = q16,
inference(paramod,[status(thm)],[c_632,c_578]) ).
cnf(c_726,plain,
store(queue_53,tail,index_54) = q17,
inference(paramod,[status(thm)],[c_634,c_584]) ).
cnf(c_727,plain,
store(queue_59,tail,index_60) = q18,
inference(paramod,[status(thm)],[c_636,c_588]) ).
cnf(c_728,plain,
store(queue_65,tail,index_66) = q19,
inference(paramod,[status(thm)],[c_638,c_592]) ).
cnf(c_729,plain,
store(queue_71,tail,index_72) = q2,
inference(paramod,[status(thm)],[c_640,c_598]) ).
cnf(c_730,plain,
store(queue_77,tail,index_78) = q20,
inference(paramod,[status(thm)],[c_642,c_602]) ).
cnf(c_731,plain,
store(queue_83,tail,index_84) = q21,
inference(paramod,[status(thm)],[c_644,c_606]) ).
cnf(c_732,plain,
store(queue_89,tail,index_90) = q22,
inference(paramod,[status(thm)],[c_646,c_610]) ).
cnf(c_733,plain,
store(queue_95,tail,index_96) = q23,
inference(paramod,[status(thm)],[c_648,c_614]) ).
cnf(c_734,plain,
store(queue_101,tail,index_102) = q24,
inference(paramod,[status(thm)],[c_650,c_422]) ).
cnf(c_735,plain,
store(queue_107,tail,index_108) = q25,
inference(paramod,[status(thm)],[c_652,c_426]) ).
cnf(c_736,plain,
store(queue_113,tail,index_114) = q26,
inference(paramod,[status(thm)],[c_654,c_432]) ).
cnf(c_737,plain,
store(queue_119,tail,index_120) = q27,
inference(paramod,[status(thm)],[c_656,c_436]) ).
cnf(c_738,plain,
store(queue_125,tail,index_126) = q28,
inference(paramod,[status(thm)],[c_658,c_440]) ).
cnf(c_739,plain,
store(queue_131,tail,index_132) = q29,
inference(paramod,[status(thm)],[c_660,c_446]) ).
cnf(c_740,plain,
store(queue_137,tail,index_138) = q3,
inference(paramod,[status(thm)],[c_662,c_450]) ).
cnf(c_741,plain,
store(queue_143,tail,index_144) = q30,
inference(paramod,[status(thm)],[c_664,c_454]) ).
cnf(c_742,plain,
store(queue_149,tail,index_150) = q31,
inference(paramod,[status(thm)],[c_666,c_458]) ).
cnf(c_743,plain,
store(queue_155,tail,index_156) = q32,
inference(paramod,[status(thm)],[c_668,c_462]) ).
cnf(c_744,plain,
store(queue_161,tail,index_162) = q33,
inference(paramod,[status(thm)],[c_670,c_466]) ).
cnf(c_745,plain,
store(queue_167,tail,index_168) = q34,
inference(paramod,[status(thm)],[c_672,c_470]) ).
cnf(c_746,plain,
store(queue_173,tail,index_174) = q35,
inference(paramod,[status(thm)],[c_674,c_476]) ).
cnf(c_747,plain,
store(queue_179,tail,index_180) = q36,
inference(paramod,[status(thm)],[c_676,c_480]) ).
cnf(c_748,plain,
store(queue_185,tail,index_186) = q37,
inference(paramod,[status(thm)],[c_678,c_484]) ).
cnf(c_749,plain,
store(queue_191,tail,index_192) = q38,
inference(paramod,[status(thm)],[c_680,c_490]) ).
cnf(c_750,plain,
store(queue_197,tail,index_198) = q39,
inference(paramod,[status(thm)],[c_682,c_494]) ).
cnf(c_751,plain,
store(queue_203,tail,index_204) = q4,
inference(paramod,[status(thm)],[c_684,c_498]) ).
cnf(c_752,plain,
store(queue_209,tail,index_210) = q40,
inference(paramod,[status(thm)],[c_686,c_502]) ).
cnf(c_753,plain,
store(queue_215,tail,index_216) = q41,
inference(paramod,[status(thm)],[c_688,c_506]) ).
cnf(c_754,plain,
store(queue_221,tail,index_222) = q42,
inference(paramod,[status(thm)],[c_690,c_510]) ).
cnf(c_755,plain,
store(queue_227,tail,index_228) = q43,
inference(paramod,[status(thm)],[c_692,c_514]) ).
cnf(c_756,plain,
store(queue_233,tail,index_234) = q44,
inference(paramod,[status(thm)],[c_694,c_520]) ).
cnf(c_757,plain,
store(queue_239,tail,index_240) = q45,
inference(paramod,[status(thm)],[c_696,c_524]) ).
cnf(c_758,plain,
store(queue_245,tail,index_246) = q46,
inference(paramod,[status(thm)],[c_698,c_528]) ).
cnf(c_759,plain,
store(queue_251,tail,index_252) = q47,
inference(paramod,[status(thm)],[c_700,c_534]) ).
cnf(c_760,plain,
store(queue_257,tail,index_258) = q48,
inference(paramod,[status(thm)],[c_702,c_538]) ).
cnf(c_761,plain,
store(queue_263,tail,index_264) = q49,
inference(paramod,[status(thm)],[c_704,c_542]) ).
cnf(c_762,plain,
store(queue_269,tail,index_270) = q5,
inference(paramod,[status(thm)],[c_706,c_546]) ).
cnf(c_763,plain,
store(queue_275,tail,index_276) = q6,
inference(paramod,[status(thm)],[c_708,c_550]) ).
cnf(c_764,plain,
store(queue_281,tail,index_282) = q7,
inference(paramod,[status(thm)],[c_710,c_554]) ).
cnf(c_765,plain,
store(queue_287,tail,index_288) = q8,
inference(paramod,[status(thm)],[c_712,c_558]) ).
cnf(c_766,plain,
store(queue_293,tail,index_294) = q9,
inference(paramod,[status(thm)],[c_714,c_564]) ).
cnf(c_5802,plain,
p(A) = s(s(A)),
inference(paramod,[status(thm)],[c_11,c_7]) ).
cnf(c_772,plain,
s(s(A)) = p(A),
inference(copy,[status(thm)],[c_5802]) ).
cnf(c_864,plain,
select(earray_262,index_261) = e48,
inference(paramod,[status(thm)],[c_135,c_1]) ).
cnf(c_5803,plain,
( select(store(q,A,B),tail) = index_0
| A = tail ),
inference(paramod,[status(thm)],[c_215,c_2]) ).
cnf(c_923,plain,
( select(store(q,A,B),tail) = index_0
| tail = A ),
inference(copy,[status(thm)],[c_5803]) ).
cnf(c_1013,plain,
p(index_264) = index_261,
inference(paramod,[status(thm)],[c_335,c_7]) ).
cnf(c_1036,plain,
p(index_299) = index_300,
inference(paramod,[status(thm)],[c_366,c_7]) ).
cnf(c_1051,plain,
p(index_6) = index_3,
inference(paramod,[status(thm)],[c_386,c_7]) ).
cnf(c_1076,plain,
( select(queue_101,A) = select(q23,A)
| seq = A ),
inference(paramod,[status(thm)],[c_420,c_2]) ).
cnf(c_1078,plain,
( select(queue_107,A) = select(q24,A)
| seq = A ),
inference(paramod,[status(thm)],[c_424,c_2]) ).
cnf(c_1080,plain,
( select(queue_11,A) = select(q9,A)
| seq = A ),
inference(paramod,[status(thm)],[c_428,c_2]) ).
cnf(c_1082,plain,
( select(queue_113,A) = select(q25,A)
| seq = A ),
inference(paramod,[status(thm)],[c_430,c_2]) ).
cnf(c_1084,plain,
( select(queue_119,A) = select(q26,A)
| seq = A ),
inference(paramod,[status(thm)],[c_434,c_2]) ).
cnf(c_1086,plain,
( select(queue_125,A) = select(q27,A)
| seq = A ),
inference(paramod,[status(thm)],[c_438,c_2]) ).
cnf(c_1088,plain,
( select(queue_131,A) = select(q28,A)
| seq = A ),
inference(paramod,[status(thm)],[c_444,c_2]) ).
cnf(c_1090,plain,
( select(queue_137,A) = select(q2,A)
| seq = A ),
inference(paramod,[status(thm)],[c_448,c_2]) ).
cnf(c_1092,plain,
( select(queue_143,A) = select(q29,A)
| seq = A ),
inference(paramod,[status(thm)],[c_452,c_2]) ).
cnf(c_1094,plain,
( select(queue_149,A) = select(q30,A)
| seq = A ),
inference(paramod,[status(thm)],[c_456,c_2]) ).
cnf(c_1096,plain,
( select(queue_155,A) = select(q31,A)
| seq = A ),
inference(paramod,[status(thm)],[c_460,c_2]) ).
cnf(c_1098,plain,
( select(queue_161,A) = select(q32,A)
| seq = A ),
inference(paramod,[status(thm)],[c_464,c_2]) ).
cnf(c_1100,plain,
( select(queue_167,A) = select(q33,A)
| seq = A ),
inference(paramod,[status(thm)],[c_468,c_2]) ).
cnf(c_1102,plain,
( select(queue_17,A) = select(q10,A)
| seq = A ),
inference(paramod,[status(thm)],[c_472,c_2]) ).
cnf(c_1104,plain,
( select(queue_173,A) = select(q34,A)
| seq = A ),
inference(paramod,[status(thm)],[c_474,c_2]) ).
cnf(c_1106,plain,
( select(queue_179,A) = select(q35,A)
| seq = A ),
inference(paramod,[status(thm)],[c_478,c_2]) ).
cnf(c_1108,plain,
( select(queue_185,A) = select(q36,A)
| seq = A ),
inference(paramod,[status(thm)],[c_482,c_2]) ).
cnf(c_1110,plain,
( select(queue_191,A) = select(q37,A)
| seq = A ),
inference(paramod,[status(thm)],[c_488,c_2]) ).
cnf(c_1112,plain,
( select(queue_197,A) = select(q38,A)
| seq = A ),
inference(paramod,[status(thm)],[c_492,c_2]) ).
cnf(c_1114,plain,
( select(queue_203,A) = select(q3,A)
| seq = A ),
inference(paramod,[status(thm)],[c_496,c_2]) ).
cnf(c_1116,plain,
( select(queue_209,A) = select(q39,A)
| seq = A ),
inference(paramod,[status(thm)],[c_500,c_2]) ).
cnf(c_1118,plain,
( select(queue_215,A) = select(q40,A)
| seq = A ),
inference(paramod,[status(thm)],[c_504,c_2]) ).
cnf(c_1120,plain,
( select(queue_221,A) = select(q41,A)
| seq = A ),
inference(paramod,[status(thm)],[c_508,c_2]) ).
cnf(c_1122,plain,
( select(queue_227,A) = select(q42,A)
| seq = A ),
inference(paramod,[status(thm)],[c_512,c_2]) ).
cnf(c_1124,plain,
( select(queue_23,A) = select(q11,A)
| seq = A ),
inference(paramod,[status(thm)],[c_516,c_2]) ).
cnf(c_1126,plain,
( select(queue_233,A) = select(q43,A)
| seq = A ),
inference(paramod,[status(thm)],[c_518,c_2]) ).
cnf(c_1128,plain,
( select(queue_239,A) = select(q44,A)
| seq = A ),
inference(paramod,[status(thm)],[c_522,c_2]) ).
cnf(c_1130,plain,
( select(queue_245,A) = select(q45,A)
| seq = A ),
inference(paramod,[status(thm)],[c_526,c_2]) ).
cnf(c_1132,plain,
( select(queue_251,A) = select(q46,A)
| seq = A ),
inference(paramod,[status(thm)],[c_532,c_2]) ).
cnf(c_1134,plain,
( select(queue_257,A) = select(q47,A)
| seq = A ),
inference(paramod,[status(thm)],[c_536,c_2]) ).
cnf(c_1135,plain,
select(queue_263,seq) = earray_262,
inference(paramod,[status(thm)],[c_540,c_1]) ).
cnf(c_1136,plain,
( select(queue_263,A) = select(q48,A)
| seq = A ),
inference(paramod,[status(thm)],[c_540,c_2]) ).
cnf(c_1138,plain,
( select(queue_269,A) = select(q4,A)
| seq = A ),
inference(paramod,[status(thm)],[c_544,c_2]) ).
cnf(c_1140,plain,
( select(queue_275,A) = select(q5,A)
| seq = A ),
inference(paramod,[status(thm)],[c_548,c_2]) ).
cnf(c_1142,plain,
( select(queue_281,A) = select(q6,A)
| seq = A ),
inference(paramod,[status(thm)],[c_552,c_2]) ).
cnf(c_1144,plain,
( select(queue_287,A) = select(q7,A)
| seq = A ),
inference(paramod,[status(thm)],[c_556,c_2]) ).
cnf(c_1146,plain,
( select(queue_29,A) = select(q12,A)
| seq = A ),
inference(paramod,[status(thm)],[c_560,c_2]) ).
cnf(c_1148,plain,
( select(queue_293,A) = select(q8,A)
| seq = A ),
inference(paramod,[status(thm)],[c_562,c_2]) ).
cnf(c_1150,plain,
( select(queue_35,A) = select(q13,A)
| seq = A ),
inference(paramod,[status(thm)],[c_568,c_2]) ).
cnf(c_1152,plain,
( select(queue_41,A) = select(q14,A)
| seq = A ),
inference(paramod,[status(thm)],[c_572,c_2]) ).
cnf(c_1154,plain,
( select(queue_47,A) = select(q15,A)
| seq = A ),
inference(paramod,[status(thm)],[c_576,c_2]) ).
cnf(c_1156,plain,
( select(queue_5,A) = select(q0,A)
| seq = A ),
inference(paramod,[status(thm)],[c_580,c_2]) ).
cnf(c_1158,plain,
( select(queue_53,A) = select(q16,A)
| seq = A ),
inference(paramod,[status(thm)],[c_582,c_2]) ).
cnf(c_1160,plain,
( select(queue_59,A) = select(q17,A)
| seq = A ),
inference(paramod,[status(thm)],[c_586,c_2]) ).
cnf(c_1162,plain,
( select(queue_65,A) = select(q18,A)
| seq = A ),
inference(paramod,[status(thm)],[c_590,c_2]) ).
cnf(c_1164,plain,
( select(queue_71,A) = select(q1,A)
| seq = A ),
inference(paramod,[status(thm)],[c_596,c_2]) ).
cnf(c_1166,plain,
( select(queue_77,A) = select(q19,A)
| seq = A ),
inference(paramod,[status(thm)],[c_600,c_2]) ).
cnf(c_1168,plain,
( select(queue_83,A) = select(q20,A)
| seq = A ),
inference(paramod,[status(thm)],[c_604,c_2]) ).
cnf(c_1170,plain,
( select(queue_89,A) = select(q21,A)
| seq = A ),
inference(paramod,[status(thm)],[c_608,c_2]) ).
cnf(c_1172,plain,
( select(queue_95,A) = select(q22,A)
| seq = A ),
inference(paramod,[status(thm)],[c_612,c_2]) ).
cnf(c_1173,plain,
select(q0,head) = index_0,
inference(paramod,[status(thm)],[c_717,c_1]) ).
cnf(c_5804,plain,
select(q1,tail) = index_6,
inference(paramod,[status(thm)],[c_718,c_1]) ).
cnf(c_5805,plain,
index_69 = index_6,
inference(paramod,[status(thm)],[c_394,c_5804]) ).
cnf(c_1175,plain,
index_6 = index_69,
inference(copy,[status(thm)],[c_5805]) ).
cnf(c_5806,plain,
( select(q1,A) = select(queue_5,A)
| tail = A ),
inference(paramod,[status(thm)],[c_718,c_2]) ).
cnf(c_1176,plain,
( select(queue_5,A) = select(q1,A)
| tail = A ),
inference(copy,[status(thm)],[c_5806]) ).
cnf(c_1178,plain,
p(index_69) = index_3,
inference(paramod,[status(thm)],[c_1175,c_1051]) ).
cnf(c_1180,plain,
s(index_3) = index_69,
inference(paramod,[status(thm)],[c_1175,c_386]) ).
cnf(c_5807,plain,
select(q10,tail) = index_12,
inference(paramod,[status(thm)],[c_719,c_1]) ).
cnf(c_5808,plain,
index_15 = index_12,
inference(paramod,[status(thm)],[c_251,c_5807]) ).
cnf(c_1181,plain,
index_12 = index_15,
inference(copy,[status(thm)],[c_5808]) ).
cnf(c_5809,plain,
( select(q10,A) = select(queue_11,A)
| tail = A ),
inference(paramod,[status(thm)],[c_719,c_2]) ).
cnf(c_1182,plain,
( select(queue_11,A) = select(q10,A)
| tail = A ),
inference(copy,[status(thm)],[c_5809]) ).
cnf(c_1186,plain,
s(index_9) = index_15,
inference(paramod,[status(thm)],[c_1181,c_229]) ).
cnf(c_5810,plain,
select(q11,tail) = index_18,
inference(paramod,[status(thm)],[c_720,c_1]) ).
cnf(c_5811,plain,
index_21 = index_18,
inference(paramod,[status(thm)],[c_295,c_5810]) ).
cnf(c_1187,plain,
index_18 = index_21,
inference(copy,[status(thm)],[c_5811]) ).
cnf(c_5812,plain,
( select(q11,A) = select(queue_17,A)
| tail = A ),
inference(paramod,[status(thm)],[c_720,c_2]) ).
cnf(c_1188,plain,
( select(queue_17,A) = select(q11,A)
| tail = A ),
inference(copy,[status(thm)],[c_5812]) ).
cnf(c_1192,plain,
s(index_15) = index_21,
inference(paramod,[status(thm)],[c_1187,c_273]) ).
cnf(c_5813,plain,
select(q12,tail) = index_24,
inference(paramod,[status(thm)],[c_721,c_1]) ).
cnf(c_5814,plain,
index_27 = index_24,
inference(paramod,[status(thm)],[c_339,c_5813]) ).
cnf(c_1193,plain,
index_24 = index_27,
inference(copy,[status(thm)],[c_5814]) ).
cnf(c_5815,plain,
( select(q12,A) = select(queue_23,A)
| tail = A ),
inference(paramod,[status(thm)],[c_721,c_2]) ).
cnf(c_1194,plain,
( select(queue_23,A) = select(q12,A)
| tail = A ),
inference(copy,[status(thm)],[c_5815]) ).
cnf(c_1198,plain,
s(index_21) = index_27,
inference(paramod,[status(thm)],[c_1193,c_317]) ).
cnf(c_5816,plain,
select(q13,tail) = index_30,
inference(paramod,[status(thm)],[c_722,c_1]) ).
cnf(c_5817,plain,
index_33 = index_30,
inference(paramod,[status(thm)],[c_368,c_5816]) ).
cnf(c_1199,plain,
index_30 = index_33,
inference(copy,[status(thm)],[c_5817]) ).
cnf(c_5818,plain,
( select(q13,A) = select(queue_29,A)
| tail = A ),
inference(paramod,[status(thm)],[c_722,c_2]) ).
cnf(c_1200,plain,
( select(queue_29,A) = select(q13,A)
| tail = A ),
inference(copy,[status(thm)],[c_5818]) ).
cnf(c_1204,plain,
s(index_27) = index_33,
inference(paramod,[status(thm)],[c_1199,c_365]) ).
cnf(c_5819,plain,
select(q14,tail) = index_36,
inference(paramod,[status(thm)],[c_723,c_1]) ).
cnf(c_5820,plain,
index_39 = index_36,
inference(paramod,[status(thm)],[c_372,c_5819]) ).
cnf(c_1205,plain,
index_36 = index_39,
inference(copy,[status(thm)],[c_5820]) ).
cnf(c_5821,plain,
( select(q14,A) = select(queue_35,A)
| tail = A ),
inference(paramod,[status(thm)],[c_723,c_2]) ).
cnf(c_1206,plain,
( select(queue_35,A) = select(q14,A)
| tail = A ),
inference(copy,[status(thm)],[c_5821]) ).
cnf(c_1210,plain,
s(index_33) = index_39,
inference(paramod,[status(thm)],[c_1205,c_370]) ).
cnf(c_5822,plain,
select(q15,tail) = index_42,
inference(paramod,[status(thm)],[c_724,c_1]) ).
cnf(c_5823,plain,
index_45 = index_42,
inference(paramod,[status(thm)],[c_376,c_5822]) ).
cnf(c_1211,plain,
index_42 = index_45,
inference(copy,[status(thm)],[c_5823]) ).
cnf(c_5824,plain,
( select(q15,A) = select(queue_41,A)
| tail = A ),
inference(paramod,[status(thm)],[c_724,c_2]) ).
cnf(c_1212,plain,
( select(queue_41,A) = select(q15,A)
| tail = A ),
inference(copy,[status(thm)],[c_5824]) ).
cnf(c_1216,plain,
s(index_39) = index_45,
inference(paramod,[status(thm)],[c_1211,c_374]) ).
cnf(c_5825,plain,
select(q16,tail) = index_48,
inference(paramod,[status(thm)],[c_725,c_1]) ).
cnf(c_5826,plain,
index_51 = index_48,
inference(paramod,[status(thm)],[c_380,c_5825]) ).
cnf(c_1217,plain,
index_48 = index_51,
inference(copy,[status(thm)],[c_5826]) ).
cnf(c_5827,plain,
( select(q16,A) = select(queue_47,A)
| tail = A ),
inference(paramod,[status(thm)],[c_725,c_2]) ).
cnf(c_1218,plain,
( select(queue_47,A) = select(q16,A)
| tail = A ),
inference(copy,[status(thm)],[c_5827]) ).
cnf(c_1222,plain,
s(index_45) = index_51,
inference(paramod,[status(thm)],[c_1217,c_378]) ).
cnf(c_5828,plain,
select(q17,tail) = index_54,
inference(paramod,[status(thm)],[c_726,c_1]) ).
cnf(c_5829,plain,
index_57 = index_54,
inference(paramod,[status(thm)],[c_384,c_5828]) ).
cnf(c_1223,plain,
index_54 = index_57,
inference(copy,[status(thm)],[c_5829]) ).
cnf(c_5830,plain,
( select(q17,A) = select(queue_53,A)
| tail = A ),
inference(paramod,[status(thm)],[c_726,c_2]) ).
cnf(c_1224,plain,
( select(queue_53,A) = select(q17,A)
| tail = A ),
inference(copy,[status(thm)],[c_5830]) ).
cnf(c_1228,plain,
s(index_51) = index_57,
inference(paramod,[status(thm)],[c_1223,c_382]) ).
cnf(c_5831,plain,
select(q18,tail) = index_60,
inference(paramod,[status(thm)],[c_727,c_1]) ).
cnf(c_5832,plain,
index_63 = index_60,
inference(paramod,[status(thm)],[c_390,c_5831]) ).
cnf(c_1229,plain,
index_60 = index_63,
inference(copy,[status(thm)],[c_5832]) ).
cnf(c_5833,plain,
( select(q18,A) = select(queue_59,A)
| tail = A ),
inference(paramod,[status(thm)],[c_727,c_2]) ).
cnf(c_1230,plain,
( select(queue_59,A) = select(q18,A)
| tail = A ),
inference(copy,[status(thm)],[c_5833]) ).
cnf(c_1234,plain,
s(index_57) = index_63,
inference(paramod,[status(thm)],[c_1229,c_388]) ).
cnf(c_5834,plain,
select(q19,tail) = index_66,
inference(paramod,[status(thm)],[c_728,c_1]) ).
cnf(c_5835,plain,
index_75 = index_66,
inference(paramod,[status(thm)],[c_398,c_5834]) ).
cnf(c_1235,plain,
index_66 = index_75,
inference(copy,[status(thm)],[c_5835]) ).
cnf(c_5836,plain,
( select(q19,A) = select(queue_65,A)
| tail = A ),
inference(paramod,[status(thm)],[c_728,c_2]) ).
cnf(c_1236,plain,
( select(queue_65,A) = select(q19,A)
| tail = A ),
inference(copy,[status(thm)],[c_5836]) ).
cnf(c_1240,plain,
s(index_63) = index_75,
inference(paramod,[status(thm)],[c_1235,c_392]) ).
cnf(c_5837,plain,
select(q2,tail) = index_72,
inference(paramod,[status(thm)],[c_729,c_1]) ).
cnf(c_5838,plain,
index_135 = index_72,
inference(paramod,[status(thm)],[c_241,c_5837]) ).
cnf(c_1241,plain,
index_72 = index_135,
inference(copy,[status(thm)],[c_5838]) ).
cnf(c_5839,plain,
( select(q2,A) = select(queue_71,A)
| tail = A ),
inference(paramod,[status(thm)],[c_729,c_2]) ).
cnf(c_1242,plain,
( select(queue_71,A) = select(q2,A)
| tail = A ),
inference(copy,[status(thm)],[c_5839]) ).
cnf(c_1246,plain,
s(index_69) = index_135,
inference(paramod,[status(thm)],[c_1241,c_396]) ).
cnf(c_5840,plain,
select(q20,tail) = index_78,
inference(paramod,[status(thm)],[c_730,c_1]) ).
cnf(c_5841,plain,
index_81 = index_78,
inference(paramod,[status(thm)],[c_402,c_5840]) ).
cnf(c_1247,plain,
index_78 = index_81,
inference(copy,[status(thm)],[c_5841]) ).
cnf(c_5842,plain,
( select(q20,A) = select(queue_77,A)
| tail = A ),
inference(paramod,[status(thm)],[c_730,c_2]) ).
cnf(c_1248,plain,
( select(queue_77,A) = select(q20,A)
| tail = A ),
inference(copy,[status(thm)],[c_5842]) ).
cnf(c_1252,plain,
s(index_75) = index_81,
inference(paramod,[status(thm)],[c_1247,c_400]) ).
cnf(c_5843,plain,
select(q21,tail) = index_84,
inference(paramod,[status(thm)],[c_731,c_1]) ).
cnf(c_5844,plain,
index_87 = index_84,
inference(paramod,[status(thm)],[c_406,c_5843]) ).
cnf(c_1253,plain,
index_84 = index_87,
inference(copy,[status(thm)],[c_5844]) ).
cnf(c_5845,plain,
( select(q21,A) = select(queue_83,A)
| tail = A ),
inference(paramod,[status(thm)],[c_731,c_2]) ).
cnf(c_1254,plain,
( select(queue_83,A) = select(q21,A)
| tail = A ),
inference(copy,[status(thm)],[c_5845]) ).
cnf(c_1258,plain,
s(index_81) = index_87,
inference(paramod,[status(thm)],[c_1253,c_404]) ).
cnf(c_5846,plain,
select(q22,tail) = index_90,
inference(paramod,[status(thm)],[c_732,c_1]) ).
cnf(c_5847,plain,
index_93 = index_90,
inference(paramod,[status(thm)],[c_412,c_5846]) ).
cnf(c_1259,plain,
index_90 = index_93,
inference(copy,[status(thm)],[c_5847]) ).
cnf(c_5848,plain,
( select(q22,A) = select(queue_89,A)
| tail = A ),
inference(paramod,[status(thm)],[c_732,c_2]) ).
cnf(c_1260,plain,
( select(queue_89,A) = select(q22,A)
| tail = A ),
inference(copy,[status(thm)],[c_5848]) ).
cnf(c_1264,plain,
s(index_87) = index_93,
inference(paramod,[status(thm)],[c_1259,c_410]) ).
cnf(c_5849,plain,
select(q23,tail) = index_96,
inference(paramod,[status(thm)],[c_733,c_1]) ).
cnf(c_5850,plain,
index_99 = index_96,
inference(paramod,[status(thm)],[c_416,c_5849]) ).
cnf(c_1265,plain,
index_96 = index_99,
inference(copy,[status(thm)],[c_5850]) ).
cnf(c_5851,plain,
( select(q23,A) = select(queue_95,A)
| tail = A ),
inference(paramod,[status(thm)],[c_733,c_2]) ).
cnf(c_1266,plain,
( select(queue_95,A) = select(q23,A)
| tail = A ),
inference(copy,[status(thm)],[c_5851]) ).
cnf(c_1270,plain,
s(index_93) = index_99,
inference(paramod,[status(thm)],[c_1265,c_414]) ).
cnf(c_5852,plain,
select(q24,tail) = index_102,
inference(paramod,[status(thm)],[c_734,c_1]) ).
cnf(c_5853,plain,
index_105 = index_102,
inference(paramod,[status(thm)],[c_219,c_5852]) ).
cnf(c_1271,plain,
index_102 = index_105,
inference(copy,[status(thm)],[c_5853]) ).
cnf(c_5854,plain,
( select(q24,A) = select(queue_101,A)
| tail = A ),
inference(paramod,[status(thm)],[c_734,c_2]) ).
cnf(c_1272,plain,
( select(queue_101,A) = select(q24,A)
| tail = A ),
inference(copy,[status(thm)],[c_5854]) ).
cnf(c_1276,plain,
s(index_99) = index_105,
inference(paramod,[status(thm)],[c_1271,c_217]) ).
cnf(c_5855,plain,
select(q25,tail) = index_108,
inference(paramod,[status(thm)],[c_735,c_1]) ).
cnf(c_5856,plain,
index_111 = index_108,
inference(paramod,[status(thm)],[c_223,c_5855]) ).
cnf(c_1277,plain,
index_108 = index_111,
inference(copy,[status(thm)],[c_5856]) ).
cnf(c_5857,plain,
( select(q25,A) = select(queue_107,A)
| tail = A ),
inference(paramod,[status(thm)],[c_735,c_2]) ).
cnf(c_1278,plain,
( select(queue_107,A) = select(q25,A)
| tail = A ),
inference(copy,[status(thm)],[c_5857]) ).
cnf(c_1282,plain,
s(index_105) = index_111,
inference(paramod,[status(thm)],[c_1277,c_221]) ).
cnf(c_5858,plain,
select(q26,tail) = index_114,
inference(paramod,[status(thm)],[c_736,c_1]) ).
cnf(c_5859,plain,
index_117 = index_114,
inference(paramod,[status(thm)],[c_227,c_5858]) ).
cnf(c_1283,plain,
index_114 = index_117,
inference(copy,[status(thm)],[c_5859]) ).
cnf(c_5860,plain,
( select(q26,A) = select(queue_113,A)
| tail = A ),
inference(paramod,[status(thm)],[c_736,c_2]) ).
cnf(c_1284,plain,
( select(queue_113,A) = select(q26,A)
| tail = A ),
inference(copy,[status(thm)],[c_5860]) ).
cnf(c_1288,plain,
s(index_111) = index_117,
inference(paramod,[status(thm)],[c_1283,c_225]) ).
cnf(c_5861,plain,
select(q27,tail) = index_120,
inference(paramod,[status(thm)],[c_737,c_1]) ).
cnf(c_5862,plain,
index_123 = index_120,
inference(paramod,[status(thm)],[c_233,c_5861]) ).
cnf(c_1289,plain,
index_120 = index_123,
inference(copy,[status(thm)],[c_5862]) ).
cnf(c_5863,plain,
( select(q27,A) = select(queue_119,A)
| tail = A ),
inference(paramod,[status(thm)],[c_737,c_2]) ).
cnf(c_1290,plain,
( select(queue_119,A) = select(q27,A)
| tail = A ),
inference(copy,[status(thm)],[c_5863]) ).
cnf(c_1294,plain,
s(index_117) = index_123,
inference(paramod,[status(thm)],[c_1289,c_231]) ).
cnf(c_5864,plain,
select(q28,tail) = index_126,
inference(paramod,[status(thm)],[c_738,c_1]) ).
cnf(c_5865,plain,
index_129 = index_126,
inference(paramod,[status(thm)],[c_237,c_5864]) ).
cnf(c_1295,plain,
index_126 = index_129,
inference(copy,[status(thm)],[c_5865]) ).
cnf(c_5866,plain,
( select(q28,A) = select(queue_125,A)
| tail = A ),
inference(paramod,[status(thm)],[c_738,c_2]) ).
cnf(c_1296,plain,
( select(queue_125,A) = select(q28,A)
| tail = A ),
inference(copy,[status(thm)],[c_5866]) ).
cnf(c_1300,plain,
s(index_123) = index_129,
inference(paramod,[status(thm)],[c_1295,c_235]) ).
cnf(c_5867,plain,
select(q29,tail) = index_132,
inference(paramod,[status(thm)],[c_739,c_1]) ).
cnf(c_5868,plain,
index_141 = index_132,
inference(paramod,[status(thm)],[c_245,c_5867]) ).
cnf(c_1301,plain,
index_132 = index_141,
inference(copy,[status(thm)],[c_5868]) ).
cnf(c_5869,plain,
( select(q29,A) = select(queue_131,A)
| tail = A ),
inference(paramod,[status(thm)],[c_739,c_2]) ).
cnf(c_1302,plain,
( select(queue_131,A) = select(q29,A)
| tail = A ),
inference(copy,[status(thm)],[c_5869]) ).
cnf(c_1306,plain,
s(index_129) = index_141,
inference(paramod,[status(thm)],[c_1301,c_239]) ).
cnf(c_5870,plain,
select(q3,tail) = index_138,
inference(paramod,[status(thm)],[c_740,c_1]) ).
cnf(c_5871,plain,
index_201 = index_138,
inference(paramod,[status(thm)],[c_289,c_5870]) ).
cnf(c_1307,plain,
index_138 = index_201,
inference(copy,[status(thm)],[c_5871]) ).
cnf(c_5872,plain,
( select(q3,A) = select(queue_137,A)
| tail = A ),
inference(paramod,[status(thm)],[c_740,c_2]) ).
cnf(c_1308,plain,
( select(queue_137,A) = select(q3,A)
| tail = A ),
inference(copy,[status(thm)],[c_5872]) ).
cnf(c_1312,plain,
s(index_135) = index_201,
inference(paramod,[status(thm)],[c_1307,c_243]) ).
cnf(c_5873,plain,
select(q30,tail) = index_144,
inference(paramod,[status(thm)],[c_741,c_1]) ).
cnf(c_5874,plain,
index_147 = index_144,
inference(paramod,[status(thm)],[c_249,c_5873]) ).
cnf(c_1313,plain,
index_144 = index_147,
inference(copy,[status(thm)],[c_5874]) ).
cnf(c_5875,plain,
( select(q30,A) = select(queue_143,A)
| tail = A ),
inference(paramod,[status(thm)],[c_741,c_2]) ).
cnf(c_1314,plain,
( select(queue_143,A) = select(q30,A)
| tail = A ),
inference(copy,[status(thm)],[c_5875]) ).
cnf(c_1318,plain,
s(index_141) = index_147,
inference(paramod,[status(thm)],[c_1313,c_247]) ).
cnf(c_5876,plain,
select(q31,tail) = index_150,
inference(paramod,[status(thm)],[c_742,c_1]) ).
cnf(c_5877,plain,
index_153 = index_150,
inference(paramod,[status(thm)],[c_255,c_5876]) ).
cnf(c_1319,plain,
index_150 = index_153,
inference(copy,[status(thm)],[c_5877]) ).
cnf(c_5878,plain,
( select(q31,A) = select(queue_149,A)
| tail = A ),
inference(paramod,[status(thm)],[c_742,c_2]) ).
cnf(c_1320,plain,
( select(queue_149,A) = select(q31,A)
| tail = A ),
inference(copy,[status(thm)],[c_5878]) ).
cnf(c_1324,plain,
s(index_147) = index_153,
inference(paramod,[status(thm)],[c_1319,c_253]) ).
cnf(c_5879,plain,
select(q32,tail) = index_156,
inference(paramod,[status(thm)],[c_743,c_1]) ).
cnf(c_5880,plain,
index_159 = index_156,
inference(paramod,[status(thm)],[c_259,c_5879]) ).
cnf(c_1325,plain,
index_156 = index_159,
inference(copy,[status(thm)],[c_5880]) ).
cnf(c_5881,plain,
( select(q32,A) = select(queue_155,A)
| tail = A ),
inference(paramod,[status(thm)],[c_743,c_2]) ).
cnf(c_1326,plain,
( select(queue_155,A) = select(q32,A)
| tail = A ),
inference(copy,[status(thm)],[c_5881]) ).
cnf(c_1330,plain,
s(index_153) = index_159,
inference(paramod,[status(thm)],[c_1325,c_257]) ).
cnf(c_5882,plain,
select(q33,tail) = index_162,
inference(paramod,[status(thm)],[c_744,c_1]) ).
cnf(c_5883,plain,
index_165 = index_162,
inference(paramod,[status(thm)],[c_263,c_5882]) ).
cnf(c_1331,plain,
index_162 = index_165,
inference(copy,[status(thm)],[c_5883]) ).
cnf(c_5884,plain,
( select(q33,A) = select(queue_161,A)
| tail = A ),
inference(paramod,[status(thm)],[c_744,c_2]) ).
cnf(c_1332,plain,
( select(queue_161,A) = select(q33,A)
| tail = A ),
inference(copy,[status(thm)],[c_5884]) ).
cnf(c_1336,plain,
s(index_159) = index_165,
inference(paramod,[status(thm)],[c_1331,c_261]) ).
cnf(c_5885,plain,
select(q34,tail) = index_168,
inference(paramod,[status(thm)],[c_745,c_1]) ).
cnf(c_5886,plain,
index_171 = index_168,
inference(paramod,[status(thm)],[c_267,c_5885]) ).
cnf(c_1337,plain,
index_168 = index_171,
inference(copy,[status(thm)],[c_5886]) ).
cnf(c_5887,plain,
( select(q34,A) = select(queue_167,A)
| tail = A ),
inference(paramod,[status(thm)],[c_745,c_2]) ).
cnf(c_1338,plain,
( select(queue_167,A) = select(q34,A)
| tail = A ),
inference(copy,[status(thm)],[c_5887]) ).
cnf(c_1342,plain,
s(index_165) = index_171,
inference(paramod,[status(thm)],[c_1337,c_265]) ).
cnf(c_5888,plain,
select(q35,tail) = index_174,
inference(paramod,[status(thm)],[c_746,c_1]) ).
cnf(c_5889,plain,
index_177 = index_174,
inference(paramod,[status(thm)],[c_271,c_5888]) ).
cnf(c_1343,plain,
index_174 = index_177,
inference(copy,[status(thm)],[c_5889]) ).
cnf(c_5890,plain,
( select(q35,A) = select(queue_173,A)
| tail = A ),
inference(paramod,[status(thm)],[c_746,c_2]) ).
cnf(c_1344,plain,
( select(queue_173,A) = select(q35,A)
| tail = A ),
inference(copy,[status(thm)],[c_5890]) ).
cnf(c_1348,plain,
s(index_171) = index_177,
inference(paramod,[status(thm)],[c_1343,c_269]) ).
cnf(c_5891,plain,
select(q36,tail) = index_180,
inference(paramod,[status(thm)],[c_747,c_1]) ).
cnf(c_5892,plain,
index_183 = index_180,
inference(paramod,[status(thm)],[c_277,c_5891]) ).
cnf(c_1349,plain,
index_180 = index_183,
inference(copy,[status(thm)],[c_5892]) ).
cnf(c_5893,plain,
( select(q36,A) = select(queue_179,A)
| tail = A ),
inference(paramod,[status(thm)],[c_747,c_2]) ).
cnf(c_1350,plain,
( select(queue_179,A) = select(q36,A)
| tail = A ),
inference(copy,[status(thm)],[c_5893]) ).
cnf(c_1354,plain,
s(index_177) = index_183,
inference(paramod,[status(thm)],[c_1349,c_275]) ).
cnf(c_5894,plain,
select(q37,tail) = index_186,
inference(paramod,[status(thm)],[c_748,c_1]) ).
cnf(c_5895,plain,
index_189 = index_186,
inference(paramod,[status(thm)],[c_281,c_5894]) ).
cnf(c_1355,plain,
index_186 = index_189,
inference(copy,[status(thm)],[c_5895]) ).
cnf(c_5896,plain,
( select(q37,A) = select(queue_185,A)
| tail = A ),
inference(paramod,[status(thm)],[c_748,c_2]) ).
cnf(c_1356,plain,
( select(queue_185,A) = select(q37,A)
| tail = A ),
inference(copy,[status(thm)],[c_5896]) ).
cnf(c_1360,plain,
s(index_183) = index_189,
inference(paramod,[status(thm)],[c_1355,c_279]) ).
cnf(c_5897,plain,
select(q38,tail) = index_192,
inference(paramod,[status(thm)],[c_749,c_1]) ).
cnf(c_5898,plain,
index_195 = index_192,
inference(paramod,[status(thm)],[c_285,c_5897]) ).
cnf(c_1361,plain,
index_192 = index_195,
inference(copy,[status(thm)],[c_5898]) ).
cnf(c_5899,plain,
( select(q38,A) = select(queue_191,A)
| tail = A ),
inference(paramod,[status(thm)],[c_749,c_2]) ).
cnf(c_1362,plain,
( select(queue_191,A) = select(q38,A)
| tail = A ),
inference(copy,[status(thm)],[c_5899]) ).
cnf(c_1366,plain,
s(index_189) = index_195,
inference(paramod,[status(thm)],[c_1361,c_283]) ).
cnf(c_5900,plain,
select(q39,tail) = index_198,
inference(paramod,[status(thm)],[c_750,c_1]) ).
cnf(c_5901,plain,
index_207 = index_198,
inference(paramod,[status(thm)],[c_293,c_5900]) ).
cnf(c_1367,plain,
index_198 = index_207,
inference(copy,[status(thm)],[c_5901]) ).
cnf(c_5902,plain,
( select(q39,A) = select(queue_197,A)
| tail = A ),
inference(paramod,[status(thm)],[c_750,c_2]) ).
cnf(c_1368,plain,
( select(queue_197,A) = select(q39,A)
| tail = A ),
inference(copy,[status(thm)],[c_5902]) ).
cnf(c_1372,plain,
s(index_195) = index_207,
inference(paramod,[status(thm)],[c_1367,c_287]) ).
cnf(c_5903,plain,
select(q4,tail) = index_204,
inference(paramod,[status(thm)],[c_751,c_1]) ).
cnf(c_5904,plain,
index_267 = index_204,
inference(paramod,[status(thm)],[c_337,c_5903]) ).
cnf(c_1373,plain,
index_204 = index_267,
inference(copy,[status(thm)],[c_5904]) ).
cnf(c_5905,plain,
( select(q4,A) = select(queue_203,A)
| tail = A ),
inference(paramod,[status(thm)],[c_751,c_2]) ).
cnf(c_1374,plain,
( select(queue_203,A) = select(q4,A)
| tail = A ),
inference(copy,[status(thm)],[c_5905]) ).
cnf(c_1378,plain,
s(index_201) = index_267,
inference(paramod,[status(thm)],[c_1373,c_291]) ).
cnf(c_5906,plain,
select(q40,tail) = index_210,
inference(paramod,[status(thm)],[c_752,c_1]) ).
cnf(c_5907,plain,
index_213 = index_210,
inference(paramod,[status(thm)],[c_299,c_5906]) ).
cnf(c_1379,plain,
index_210 = index_213,
inference(copy,[status(thm)],[c_5907]) ).
cnf(c_5908,plain,
( select(q40,A) = select(queue_209,A)
| tail = A ),
inference(paramod,[status(thm)],[c_752,c_2]) ).
cnf(c_1380,plain,
( select(queue_209,A) = select(q40,A)
| tail = A ),
inference(copy,[status(thm)],[c_5908]) ).
cnf(c_1384,plain,
s(index_207) = index_213,
inference(paramod,[status(thm)],[c_1379,c_297]) ).
cnf(c_5909,plain,
select(q41,tail) = index_216,
inference(paramod,[status(thm)],[c_753,c_1]) ).
cnf(c_5910,plain,
index_219 = index_216,
inference(paramod,[status(thm)],[c_303,c_5909]) ).
cnf(c_1385,plain,
index_216 = index_219,
inference(copy,[status(thm)],[c_5910]) ).
cnf(c_5911,plain,
( select(q41,A) = select(queue_215,A)
| tail = A ),
inference(paramod,[status(thm)],[c_753,c_2]) ).
cnf(c_1386,plain,
( select(queue_215,A) = select(q41,A)
| tail = A ),
inference(copy,[status(thm)],[c_5911]) ).
cnf(c_1390,plain,
s(index_213) = index_219,
inference(paramod,[status(thm)],[c_1385,c_301]) ).
cnf(c_5912,plain,
select(q42,tail) = index_222,
inference(paramod,[status(thm)],[c_754,c_1]) ).
cnf(c_5913,plain,
index_225 = index_222,
inference(paramod,[status(thm)],[c_307,c_5912]) ).
cnf(c_1391,plain,
index_222 = index_225,
inference(copy,[status(thm)],[c_5913]) ).
cnf(c_5914,plain,
( select(q42,A) = select(queue_221,A)
| tail = A ),
inference(paramod,[status(thm)],[c_754,c_2]) ).
cnf(c_1392,plain,
( select(queue_221,A) = select(q42,A)
| tail = A ),
inference(copy,[status(thm)],[c_5914]) ).
cnf(c_1396,plain,
s(index_219) = index_225,
inference(paramod,[status(thm)],[c_1391,c_305]) ).
cnf(c_5915,plain,
select(q43,tail) = index_228,
inference(paramod,[status(thm)],[c_755,c_1]) ).
cnf(c_5916,plain,
index_231 = index_228,
inference(paramod,[status(thm)],[c_311,c_5915]) ).
cnf(c_1397,plain,
index_228 = index_231,
inference(copy,[status(thm)],[c_5916]) ).
cnf(c_5917,plain,
( select(q43,A) = select(queue_227,A)
| tail = A ),
inference(paramod,[status(thm)],[c_755,c_2]) ).
cnf(c_1398,plain,
( select(queue_227,A) = select(q43,A)
| tail = A ),
inference(copy,[status(thm)],[c_5917]) ).
cnf(c_1402,plain,
s(index_225) = index_231,
inference(paramod,[status(thm)],[c_1397,c_309]) ).
cnf(c_5918,plain,
select(q44,tail) = index_234,
inference(paramod,[status(thm)],[c_756,c_1]) ).
cnf(c_5919,plain,
index_237 = index_234,
inference(paramod,[status(thm)],[c_315,c_5918]) ).
cnf(c_1403,plain,
index_234 = index_237,
inference(copy,[status(thm)],[c_5919]) ).
cnf(c_5920,plain,
( select(q44,A) = select(queue_233,A)
| tail = A ),
inference(paramod,[status(thm)],[c_756,c_2]) ).
cnf(c_1404,plain,
( select(queue_233,A) = select(q44,A)
| tail = A ),
inference(copy,[status(thm)],[c_5920]) ).
cnf(c_1408,plain,
s(index_231) = index_237,
inference(paramod,[status(thm)],[c_1403,c_313]) ).
cnf(c_5921,plain,
select(q45,tail) = index_240,
inference(paramod,[status(thm)],[c_757,c_1]) ).
cnf(c_5922,plain,
index_243 = index_240,
inference(paramod,[status(thm)],[c_321,c_5921]) ).
cnf(c_1409,plain,
index_240 = index_243,
inference(copy,[status(thm)],[c_5922]) ).
cnf(c_5923,plain,
( select(q45,A) = select(queue_239,A)
| tail = A ),
inference(paramod,[status(thm)],[c_757,c_2]) ).
cnf(c_1410,plain,
( select(queue_239,A) = select(q45,A)
| tail = A ),
inference(copy,[status(thm)],[c_5923]) ).
cnf(c_1414,plain,
s(index_237) = index_243,
inference(paramod,[status(thm)],[c_1409,c_319]) ).
cnf(c_5924,plain,
select(q46,tail) = index_246,
inference(paramod,[status(thm)],[c_758,c_1]) ).
cnf(c_5925,plain,
index_249 = index_246,
inference(paramod,[status(thm)],[c_325,c_5924]) ).
cnf(c_1415,plain,
index_246 = index_249,
inference(copy,[status(thm)],[c_5925]) ).
cnf(c_5926,plain,
( select(q46,A) = select(queue_245,A)
| tail = A ),
inference(paramod,[status(thm)],[c_758,c_2]) ).
cnf(c_1416,plain,
( select(queue_245,A) = select(q46,A)
| tail = A ),
inference(copy,[status(thm)],[c_5926]) ).
cnf(c_1420,plain,
s(index_243) = index_249,
inference(paramod,[status(thm)],[c_1415,c_323]) ).
cnf(c_5927,plain,
select(q47,tail) = index_252,
inference(paramod,[status(thm)],[c_759,c_1]) ).
cnf(c_5928,plain,
index_255 = index_252,
inference(paramod,[status(thm)],[c_329,c_5927]) ).
cnf(c_1421,plain,
index_252 = index_255,
inference(copy,[status(thm)],[c_5928]) ).
cnf(c_5929,plain,
( select(q47,A) = select(queue_251,A)
| tail = A ),
inference(paramod,[status(thm)],[c_759,c_2]) ).
cnf(c_1422,plain,
( select(queue_251,A) = select(q47,A)
| tail = A ),
inference(copy,[status(thm)],[c_5929]) ).
cnf(c_1426,plain,
s(index_249) = index_255,
inference(paramod,[status(thm)],[c_1421,c_327]) ).
cnf(c_5930,plain,
select(q48,tail) = index_258,
inference(paramod,[status(thm)],[c_760,c_1]) ).
cnf(c_5931,plain,
index_261 = index_258,
inference(paramod,[status(thm)],[c_333,c_5930]) ).
cnf(c_1427,plain,
index_258 = index_261,
inference(copy,[status(thm)],[c_5931]) ).
cnf(c_5932,plain,
( select(q48,A) = select(queue_257,A)
| tail = A ),
inference(paramod,[status(thm)],[c_760,c_2]) ).
cnf(c_1428,plain,
( select(queue_257,A) = select(q48,A)
| tail = A ),
inference(copy,[status(thm)],[c_5932]) ).
cnf(c_1432,plain,
s(index_255) = index_261,
inference(paramod,[status(thm)],[c_1427,c_331]) ).
cnf(c_5933,plain,
select(q49,tail) = index_264,
inference(paramod,[status(thm)],[c_761,c_1]) ).
cnf(c_1433,plain,
index_299 = index_264,
inference(paramod,[status(thm)],[c_361,c_5933]) ).
cnf(c_5934,plain,
( select(q49,A) = select(queue_263,A)
| tail = A ),
inference(paramod,[status(thm)],[c_761,c_2]) ).
cnf(c_1434,plain,
( select(queue_263,A) = select(q49,A)
| tail = A ),
inference(copy,[status(thm)],[c_5934]) ).
cnf(c_5935,plain,
p(index_264) = index_300,
inference(paramod,[status(thm)],[c_1433,c_1036]) ).
cnf(c_5936,plain,
index_261 = index_300,
inference(paramod,[status(thm)],[c_1013,c_5935]) ).
cnf(c_1436,plain,
index_300 = index_261,
inference(copy,[status(thm)],[c_5936]) ).
cnf(c_1440,plain,
select(earray_296,index_261) = elem_301,
inference(paramod,[status(thm)],[c_1436,c_213]) ).
cnf(c_5937,plain,
select(q5,tail) = index_270,
inference(paramod,[status(thm)],[c_762,c_1]) ).
cnf(c_5938,plain,
index_273 = index_270,
inference(paramod,[status(thm)],[c_343,c_5937]) ).
cnf(c_1441,plain,
index_270 = index_273,
inference(copy,[status(thm)],[c_5938]) ).
cnf(c_5939,plain,
( select(q5,A) = select(queue_269,A)
| tail = A ),
inference(paramod,[status(thm)],[c_762,c_2]) ).
cnf(c_1442,plain,
( select(queue_269,A) = select(q5,A)
| tail = A ),
inference(copy,[status(thm)],[c_5939]) ).
cnf(c_1446,plain,
s(index_267) = index_273,
inference(paramod,[status(thm)],[c_1441,c_341]) ).
cnf(c_5940,plain,
select(q6,tail) = index_276,
inference(paramod,[status(thm)],[c_763,c_1]) ).
cnf(c_5941,plain,
index_279 = index_276,
inference(paramod,[status(thm)],[c_347,c_5940]) ).
cnf(c_1447,plain,
index_276 = index_279,
inference(copy,[status(thm)],[c_5941]) ).
cnf(c_5942,plain,
( select(q6,A) = select(queue_275,A)
| tail = A ),
inference(paramod,[status(thm)],[c_763,c_2]) ).
cnf(c_1448,plain,
( select(queue_275,A) = select(q6,A)
| tail = A ),
inference(copy,[status(thm)],[c_5942]) ).
cnf(c_1452,plain,
s(index_273) = index_279,
inference(paramod,[status(thm)],[c_1447,c_345]) ).
cnf(c_5943,plain,
select(q7,tail) = index_282,
inference(paramod,[status(thm)],[c_764,c_1]) ).
cnf(c_5944,plain,
index_285 = index_282,
inference(paramod,[status(thm)],[c_351,c_5943]) ).
cnf(c_1453,plain,
index_282 = index_285,
inference(copy,[status(thm)],[c_5944]) ).
cnf(c_5945,plain,
( select(q7,A) = select(queue_281,A)
| tail = A ),
inference(paramod,[status(thm)],[c_764,c_2]) ).
cnf(c_1454,plain,
( select(queue_281,A) = select(q7,A)
| tail = A ),
inference(copy,[status(thm)],[c_5945]) ).
cnf(c_1458,plain,
s(index_279) = index_285,
inference(paramod,[status(thm)],[c_1453,c_349]) ).
cnf(c_5946,plain,
select(q8,tail) = index_288,
inference(paramod,[status(thm)],[c_765,c_1]) ).
cnf(c_5947,plain,
index_291 = index_288,
inference(paramod,[status(thm)],[c_355,c_5946]) ).
cnf(c_1459,plain,
index_288 = index_291,
inference(copy,[status(thm)],[c_5947]) ).
cnf(c_5948,plain,
( select(q8,A) = select(queue_287,A)
| tail = A ),
inference(paramod,[status(thm)],[c_765,c_2]) ).
cnf(c_1460,plain,
( select(queue_287,A) = select(q8,A)
| tail = A ),
inference(copy,[status(thm)],[c_5948]) ).
cnf(c_1464,plain,
s(index_285) = index_291,
inference(paramod,[status(thm)],[c_1459,c_353]) ).
cnf(c_5949,plain,
select(q9,tail) = index_294,
inference(paramod,[status(thm)],[c_766,c_1]) ).
cnf(c_5950,plain,
index_9 = index_294,
inference(paramod,[status(thm)],[c_408,c_5949]) ).
cnf(c_1465,plain,
index_294 = index_9,
inference(copy,[status(thm)],[c_5950]) ).
cnf(c_5951,plain,
( select(q9,A) = select(queue_293,A)
| tail = A ),
inference(paramod,[status(thm)],[c_766,c_2]) ).
cnf(c_1466,plain,
( select(queue_293,A) = select(q9,A)
| tail = A ),
inference(copy,[status(thm)],[c_5951]) ).
cnf(c_1470,plain,
s(index_291) = index_9,
inference(paramod,[status(thm)],[c_1465,c_357]) ).
cnf(c_5952,plain,
s(s(index_69)) = index_3,
inference(paramod,[status(thm)],[c_1178,c_772]) ).
cnf(c_5953,plain,
s(index_135) = index_3,
inference(paramod,[status(thm)],[c_1246,c_5952]) ).
cnf(c_5954,plain,
index_201 = index_3,
inference(paramod,[status(thm)],[c_1312,c_5953]) ).
cnf(c_2029,plain,
index_3 = index_201,
inference(copy,[status(thm)],[c_5954]) ).
cnf(c_5955,plain,
s(index_201) = index_69,
inference(paramod,[status(thm)],[c_2029,c_1180]) ).
cnf(c_5956,plain,
index_267 = index_69,
inference(paramod,[status(thm)],[c_1378,c_5955]) ).
cnf(c_2035,plain,
index_69 = index_267,
inference(copy,[status(thm)],[c_5956]) ).
cnf(c_2039,plain,
select(q0,tail) = index_201,
inference(paramod,[status(thm)],[c_2029,c_363]) ).
cnf(c_5957,plain,
s(index_267) = index_135,
inference(paramod,[status(thm)],[c_2035,c_1246]) ).
cnf(c_2046,plain,
index_273 = index_135,
inference(paramod,[status(thm)],[c_1446,c_5957]) ).
cnf(c_5958,plain,
s(index_135) = index_279,
inference(paramod,[status(thm)],[c_2046,c_1452]) ).
cnf(c_5959,plain,
index_201 = index_279,
inference(paramod,[status(thm)],[c_1312,c_5958]) ).
cnf(c_2061,plain,
index_279 = index_201,
inference(copy,[status(thm)],[c_5959]) ).
cnf(c_2062,plain,
s(index_267) = index_135,
inference(paramod,[status(thm)],[c_2046,c_1446]) ).
cnf(c_5960,plain,
s(index_201) = index_285,
inference(paramod,[status(thm)],[c_2061,c_1458]) ).
cnf(c_5961,plain,
index_267 = index_285,
inference(paramod,[status(thm)],[c_1378,c_5960]) ).
cnf(c_2075,plain,
index_285 = index_267,
inference(copy,[status(thm)],[c_5961]) ).
cnf(c_5962,plain,
s(index_267) = index_291,
inference(paramod,[status(thm)],[c_2075,c_1464]) ).
cnf(c_5963,plain,
index_135 = index_291,
inference(paramod,[status(thm)],[c_2062,c_5962]) ).
cnf(c_2088,plain,
index_291 = index_135,
inference(copy,[status(thm)],[c_5963]) ).
cnf(c_5964,plain,
s(index_135) = index_9,
inference(paramod,[status(thm)],[c_2088,c_1470]) ).
cnf(c_5965,plain,
index_201 = index_9,
inference(paramod,[status(thm)],[c_1312,c_5964]) ).
cnf(c_2101,plain,
index_9 = index_201,
inference(copy,[status(thm)],[c_5965]) ).
cnf(c_5966,plain,
s(index_201) = index_15,
inference(paramod,[status(thm)],[c_2101,c_1186]) ).
cnf(c_2125,plain,
index_267 = index_15,
inference(paramod,[status(thm)],[c_1378,c_5966]) ).
cnf(c_5967,plain,
s(index_15) = index_135,
inference(paramod,[status(thm)],[c_2125,c_2062]) ).
cnf(c_2146,plain,
index_21 = index_135,
inference(paramod,[status(thm)],[c_1192,c_5967]) ).
cnf(c_2167,plain,
s(index_201) = index_15,
inference(paramod,[status(thm)],[c_2125,c_1378]) ).
cnf(c_5968,plain,
s(index_135) = index_27,
inference(paramod,[status(thm)],[c_2146,c_1198]) ).
cnf(c_5969,plain,
index_201 = index_27,
inference(paramod,[status(thm)],[c_1312,c_5968]) ).
cnf(c_2180,plain,
index_27 = index_201,
inference(copy,[status(thm)],[c_5969]) ).
cnf(c_2181,plain,
s(index_15) = index_135,
inference(paramod,[status(thm)],[c_2146,c_1192]) ).
cnf(c_5970,plain,
s(index_201) = index_33,
inference(paramod,[status(thm)],[c_2180,c_1204]) ).
cnf(c_5971,plain,
index_15 = index_33,
inference(paramod,[status(thm)],[c_2167,c_5970]) ).
cnf(c_2194,plain,
index_33 = index_15,
inference(copy,[status(thm)],[c_5971]) ).
cnf(c_5972,plain,
s(index_15) = index_39,
inference(paramod,[status(thm)],[c_2194,c_1210]) ).
cnf(c_5973,plain,
index_135 = index_39,
inference(paramod,[status(thm)],[c_2181,c_5972]) ).
cnf(c_2207,plain,
index_39 = index_135,
inference(copy,[status(thm)],[c_5973]) ).
cnf(c_5974,plain,
s(index_135) = index_45,
inference(paramod,[status(thm)],[c_2207,c_1216]) ).
cnf(c_5975,plain,
index_201 = index_45,
inference(paramod,[status(thm)],[c_1312,c_5974]) ).
cnf(c_2220,plain,
index_45 = index_201,
inference(copy,[status(thm)],[c_5975]) ).
cnf(c_5976,plain,
s(index_201) = index_51,
inference(paramod,[status(thm)],[c_2220,c_1222]) ).
cnf(c_5977,plain,
index_15 = index_51,
inference(paramod,[status(thm)],[c_2167,c_5976]) ).
cnf(c_2233,plain,
index_51 = index_15,
inference(copy,[status(thm)],[c_5977]) ).
cnf(c_5978,plain,
s(index_15) = index_57,
inference(paramod,[status(thm)],[c_2233,c_1228]) ).
cnf(c_5979,plain,
index_135 = index_57,
inference(paramod,[status(thm)],[c_2181,c_5978]) ).
cnf(c_2246,plain,
index_57 = index_135,
inference(copy,[status(thm)],[c_5979]) ).
cnf(c_5980,plain,
s(index_135) = index_63,
inference(paramod,[status(thm)],[c_2246,c_1234]) ).
cnf(c_5981,plain,
index_201 = index_63,
inference(paramod,[status(thm)],[c_1312,c_5980]) ).
cnf(c_2259,plain,
index_63 = index_201,
inference(copy,[status(thm)],[c_5981]) ).
cnf(c_5982,plain,
s(index_201) = index_75,
inference(paramod,[status(thm)],[c_2259,c_1240]) ).
cnf(c_5983,plain,
index_15 = index_75,
inference(paramod,[status(thm)],[c_2167,c_5982]) ).
cnf(c_2272,plain,
index_75 = index_15,
inference(copy,[status(thm)],[c_5983]) ).
cnf(c_5984,plain,
s(index_15) = index_81,
inference(paramod,[status(thm)],[c_2272,c_1252]) ).
cnf(c_5985,plain,
index_135 = index_81,
inference(paramod,[status(thm)],[c_2181,c_5984]) ).
cnf(c_2285,plain,
index_81 = index_135,
inference(copy,[status(thm)],[c_5985]) ).
cnf(c_5986,plain,
s(index_135) = index_87,
inference(paramod,[status(thm)],[c_2285,c_1258]) ).
cnf(c_5987,plain,
index_201 = index_87,
inference(paramod,[status(thm)],[c_1312,c_5986]) ).
cnf(c_2298,plain,
index_87 = index_201,
inference(copy,[status(thm)],[c_5987]) ).
cnf(c_5988,plain,
s(index_201) = index_93,
inference(paramod,[status(thm)],[c_2298,c_1264]) ).
cnf(c_5989,plain,
index_15 = index_93,
inference(paramod,[status(thm)],[c_2167,c_5988]) ).
cnf(c_2311,plain,
index_93 = index_15,
inference(copy,[status(thm)],[c_5989]) ).
cnf(c_5990,plain,
s(index_15) = index_99,
inference(paramod,[status(thm)],[c_2311,c_1270]) ).
cnf(c_5991,plain,
index_135 = index_99,
inference(paramod,[status(thm)],[c_2181,c_5990]) ).
cnf(c_2324,plain,
index_99 = index_135,
inference(copy,[status(thm)],[c_5991]) ).
cnf(c_5992,plain,
s(index_135) = index_105,
inference(paramod,[status(thm)],[c_2324,c_1276]) ).
cnf(c_2346,plain,
index_201 = index_105,
inference(paramod,[status(thm)],[c_1312,c_5992]) ).
cnf(c_5993,plain,
s(index_105) = index_15,
inference(paramod,[status(thm)],[c_2346,c_2167]) ).
cnf(c_5994,plain,
index_111 = index_15,
inference(paramod,[status(thm)],[c_1282,c_5993]) ).
cnf(c_2408,plain,
index_15 = index_111,
inference(copy,[status(thm)],[c_5994]) ).
cnf(c_2445,plain,
select(q0,tail) = index_105,
inference(paramod,[status(thm)],[c_2346,c_2039]) ).
cnf(c_2460,plain,
s(index_135) = index_105,
inference(paramod,[status(thm)],[c_2346,c_1312]) ).
cnf(c_5995,plain,
s(index_111) = index_135,
inference(paramod,[status(thm)],[c_2408,c_2181]) ).
cnf(c_5996,plain,
index_117 = index_135,
inference(paramod,[status(thm)],[c_1288,c_5995]) ).
cnf(c_2520,plain,
index_135 = index_117,
inference(copy,[status(thm)],[c_5996]) ).
cnf(c_5997,plain,
s(index_117) = index_105,
inference(paramod,[status(thm)],[c_2520,c_2460]) ).
cnf(c_2572,plain,
index_123 = index_105,
inference(paramod,[status(thm)],[c_1294,c_5997]) ).
cnf(c_5998,plain,
s(index_105) = index_129,
inference(paramod,[status(thm)],[c_2572,c_1300]) ).
cnf(c_5999,plain,
index_111 = index_129,
inference(paramod,[status(thm)],[c_1282,c_5998]) ).
cnf(c_2692,plain,
index_129 = index_111,
inference(copy,[status(thm)],[c_5999]) ).
cnf(c_2693,plain,
s(index_117) = index_105,
inference(paramod,[status(thm)],[c_2572,c_1294]) ).
cnf(c_6000,plain,
s(index_111) = index_141,
inference(paramod,[status(thm)],[c_2692,c_1306]) ).
cnf(c_6001,plain,
index_117 = index_141,
inference(paramod,[status(thm)],[c_1288,c_6000]) ).
cnf(c_2706,plain,
index_141 = index_117,
inference(copy,[status(thm)],[c_6001]) ).
cnf(c_6002,plain,
s(index_117) = index_147,
inference(paramod,[status(thm)],[c_2706,c_1318]) ).
cnf(c_6003,plain,
index_105 = index_147,
inference(paramod,[status(thm)],[c_2693,c_6002]) ).
cnf(c_2719,plain,
index_147 = index_105,
inference(copy,[status(thm)],[c_6003]) ).
cnf(c_6004,plain,
s(index_105) = index_153,
inference(paramod,[status(thm)],[c_2719,c_1324]) ).
cnf(c_6005,plain,
index_111 = index_153,
inference(paramod,[status(thm)],[c_1282,c_6004]) ).
cnf(c_2732,plain,
index_153 = index_111,
inference(copy,[status(thm)],[c_6005]) ).
cnf(c_6006,plain,
s(index_111) = index_159,
inference(paramod,[status(thm)],[c_2732,c_1330]) ).
cnf(c_6007,plain,
index_117 = index_159,
inference(paramod,[status(thm)],[c_1288,c_6006]) ).
cnf(c_2745,plain,
index_159 = index_117,
inference(copy,[status(thm)],[c_6007]) ).
cnf(c_6008,plain,
s(index_117) = index_165,
inference(paramod,[status(thm)],[c_2745,c_1336]) ).
cnf(c_6009,plain,
index_105 = index_165,
inference(paramod,[status(thm)],[c_2693,c_6008]) ).
cnf(c_2758,plain,
index_165 = index_105,
inference(copy,[status(thm)],[c_6009]) ).
cnf(c_6010,plain,
s(index_105) = index_171,
inference(paramod,[status(thm)],[c_2758,c_1342]) ).
cnf(c_6011,plain,
index_111 = index_171,
inference(paramod,[status(thm)],[c_1282,c_6010]) ).
cnf(c_2771,plain,
index_171 = index_111,
inference(copy,[status(thm)],[c_6011]) ).
cnf(c_6012,plain,
s(index_111) = index_177,
inference(paramod,[status(thm)],[c_2771,c_1348]) ).
cnf(c_6013,plain,
index_117 = index_177,
inference(paramod,[status(thm)],[c_1288,c_6012]) ).
cnf(c_2784,plain,
index_177 = index_117,
inference(copy,[status(thm)],[c_6013]) ).
cnf(c_6014,plain,
s(index_117) = index_183,
inference(paramod,[status(thm)],[c_2784,c_1354]) ).
cnf(c_6015,plain,
index_105 = index_183,
inference(paramod,[status(thm)],[c_2693,c_6014]) ).
cnf(c_2797,plain,
index_183 = index_105,
inference(copy,[status(thm)],[c_6015]) ).
cnf(c_6016,plain,
s(index_105) = index_189,
inference(paramod,[status(thm)],[c_2797,c_1360]) ).
cnf(c_6017,plain,
index_111 = index_189,
inference(paramod,[status(thm)],[c_1282,c_6016]) ).
cnf(c_2810,plain,
index_189 = index_111,
inference(copy,[status(thm)],[c_6017]) ).
cnf(c_6018,plain,
s(index_111) = index_195,
inference(paramod,[status(thm)],[c_2810,c_1366]) ).
cnf(c_6019,plain,
index_117 = index_195,
inference(paramod,[status(thm)],[c_1288,c_6018]) ).
cnf(c_2823,plain,
index_195 = index_117,
inference(copy,[status(thm)],[c_6019]) ).
cnf(c_6020,plain,
s(index_117) = index_207,
inference(paramod,[status(thm)],[c_2823,c_1372]) ).
cnf(c_6021,plain,
index_105 = index_207,
inference(paramod,[status(thm)],[c_2693,c_6020]) ).
cnf(c_2836,plain,
index_207 = index_105,
inference(copy,[status(thm)],[c_6021]) ).
cnf(c_6022,plain,
s(index_105) = index_213,
inference(paramod,[status(thm)],[c_2836,c_1384]) ).
cnf(c_6023,plain,
index_111 = index_213,
inference(paramod,[status(thm)],[c_1282,c_6022]) ).
cnf(c_2849,plain,
index_213 = index_111,
inference(copy,[status(thm)],[c_6023]) ).
cnf(c_6024,plain,
s(index_111) = index_219,
inference(paramod,[status(thm)],[c_2849,c_1390]) ).
cnf(c_6025,plain,
index_117 = index_219,
inference(paramod,[status(thm)],[c_1288,c_6024]) ).
cnf(c_2862,plain,
index_219 = index_117,
inference(copy,[status(thm)],[c_6025]) ).
cnf(c_6026,plain,
s(index_117) = index_225,
inference(paramod,[status(thm)],[c_2862,c_1396]) ).
cnf(c_6027,plain,
index_105 = index_225,
inference(paramod,[status(thm)],[c_2693,c_6026]) ).
cnf(c_2875,plain,
index_225 = index_105,
inference(copy,[status(thm)],[c_6027]) ).
cnf(c_6028,plain,
s(index_105) = index_231,
inference(paramod,[status(thm)],[c_2875,c_1402]) ).
cnf(c_6029,plain,
index_111 = index_231,
inference(paramod,[status(thm)],[c_1282,c_6028]) ).
cnf(c_2888,plain,
index_231 = index_111,
inference(copy,[status(thm)],[c_6029]) ).
cnf(c_6030,plain,
s(index_111) = index_237,
inference(paramod,[status(thm)],[c_2888,c_1408]) ).
cnf(c_6031,plain,
index_117 = index_237,
inference(paramod,[status(thm)],[c_1288,c_6030]) ).
cnf(c_2901,plain,
index_237 = index_117,
inference(copy,[status(thm)],[c_6031]) ).
cnf(c_6032,plain,
s(index_117) = index_243,
inference(paramod,[status(thm)],[c_2901,c_1414]) ).
cnf(c_6033,plain,
index_105 = index_243,
inference(paramod,[status(thm)],[c_2693,c_6032]) ).
cnf(c_2914,plain,
index_243 = index_105,
inference(copy,[status(thm)],[c_6033]) ).
cnf(c_6034,plain,
s(index_105) = index_249,
inference(paramod,[status(thm)],[c_2914,c_1420]) ).
cnf(c_6035,plain,
index_111 = index_249,
inference(paramod,[status(thm)],[c_1282,c_6034]) ).
cnf(c_2927,plain,
index_249 = index_111,
inference(copy,[status(thm)],[c_6035]) ).
cnf(c_6036,plain,
s(index_111) = index_255,
inference(paramod,[status(thm)],[c_2927,c_1426]) ).
cnf(c_6037,plain,
index_117 = index_255,
inference(paramod,[status(thm)],[c_1288,c_6036]) ).
cnf(c_2940,plain,
index_255 = index_117,
inference(copy,[status(thm)],[c_6037]) ).
cnf(c_6038,plain,
s(index_117) = index_261,
inference(paramod,[status(thm)],[c_2940,c_1432]) ).
cnf(c_6039,plain,
index_105 = index_261,
inference(paramod,[status(thm)],[c_2693,c_6038]) ).
cnf(c_2955,plain,
index_261 = index_105,
inference(copy,[status(thm)],[c_6039]) ).
cnf(c_2968,plain,
select(earray_296,index_105) = elem_301,
inference(paramod,[status(thm)],[c_2955,c_1440]) ).
cnf(c_2977,plain,
select(earray_262,index_105) = e48,
inference(paramod,[status(thm)],[c_2955,c_864]) ).
cnf(c_6040,plain,
( select(q0,tail) = index_0
| tail = head ),
inference(paramod,[status(thm)],[c_717,c_923]) ).
cnf(c_6041,plain,
( index_105 = index_0
| tail = head ),
inference(paramod,[status(thm)],[c_2445,c_6040]) ).
cnf(c_6042,plain,
( index_105 = index_0
| head = tail ),
inference(copy,[status(thm)],[c_6041]) ).
cnf(c_6043,plain,
( index_0 = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6042]) ).
cnf(c_3550,plain,
index_0 = index_105,
inference(resolve,[status(thm)],[c_3,c_6043]) ).
cnf(c_3558,plain,
select(q0,head) = index_105,
inference(paramod,[status(thm)],[c_3550,c_1173]) ).
cnf(c_6044,plain,
( select(queue_5,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_3558,c_1156]) ).
cnf(c_6045,plain,
( select(queue_5,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6044]) ).
cnf(c_3942,plain,
select(queue_5,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6045]) ).
cnf(c_6046,plain,
( select(q1,head) = index_105
| tail = head ),
inference(paramod,[status(thm)],[c_1176,c_3942]) ).
cnf(c_6047,plain,
( select(q1,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6046]) ).
cnf(c_4040,plain,
select(q1,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6047]) ).
cnf(c_6048,plain,
( select(queue_71,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_4040,c_1164]) ).
cnf(c_6049,plain,
( select(queue_71,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6048]) ).
cnf(c_4061,plain,
select(queue_71,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6049]) ).
cnf(c_6050,plain,
( select(q2,head) = index_105
| tail = head ),
inference(paramod,[status(thm)],[c_1242,c_4061]) ).
cnf(c_6051,plain,
( select(q2,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6050]) ).
cnf(c_4290,plain,
select(q2,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6051]) ).
cnf(c_6052,plain,
( select(queue_137,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_4290,c_1090]) ).
cnf(c_6053,plain,
( select(queue_137,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6052]) ).
cnf(c_4311,plain,
select(queue_137,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6053]) ).
cnf(c_6054,plain,
( select(q3,head) = index_105
| tail = head ),
inference(paramod,[status(thm)],[c_1308,c_4311]) ).
cnf(c_6055,plain,
( select(q3,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6054]) ).
cnf(c_4562,plain,
select(q3,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6055]) ).
cnf(c_6056,plain,
( select(queue_203,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_4562,c_1114]) ).
cnf(c_6057,plain,
( select(queue_203,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6056]) ).
cnf(c_4583,plain,
select(queue_203,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6057]) ).
cnf(c_6058,plain,
( select(q4,head) = index_105
| tail = head ),
inference(paramod,[status(thm)],[c_1374,c_4583]) ).
cnf(c_6059,plain,
( select(q4,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6058]) ).
cnf(c_4812,plain,
select(q4,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6059]) ).
cnf(c_6060,plain,
( select(queue_269,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_4812,c_1138]) ).
cnf(c_6061,plain,
( select(queue_269,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6060]) ).
cnf(c_4833,plain,
select(queue_269,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6061]) ).
cnf(c_6062,plain,
( select(queue_263,seq) = earray_296
| tail = seq ),
inference(paramod,[status(thm)],[c_159,c_1434]) ).
cnf(c_6063,plain,
( earray_262 = earray_296
| tail = seq ),
inference(paramod,[status(thm)],[c_1135,c_6062]) ).
cnf(c_6064,plain,
( earray_262 = earray_296
| seq = tail ),
inference(copy,[status(thm)],[c_6063]) ).
cnf(c_5036,plain,
earray_262 = earray_296,
inference(resolve,[status(thm)],[c_6,c_6064]) ).
cnf(c_6065,plain,
( select(queue_263,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_359,c_1434]) ).
cnf(c_6066,plain,
( select(queue_263,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6065]) ).
cnf(c_5037,plain,
select(queue_263,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6066]) ).
cnf(c_6067,plain,
select(earray_296,index_105) = e48,
inference(paramod,[status(thm)],[c_5036,c_2977]) ).
cnf(c_5050,plain,
elem_301 = e48,
inference(paramod,[status(thm)],[c_2968,c_6067]) ).
cnf(c_5058,plain,
select(earray_296,index_105) = e48,
inference(paramod,[status(thm)],[c_5050,c_2968]) ).
cnf(c_6068,plain,
e48 != elem_298,
inference(paramod,[status(thm)],[c_5050,c_716]) ).
cnf(c_5059,plain,
elem_298 != e48,
inference(copy,[status(thm)],[c_6068]) ).
cnf(c_6069,plain,
( select(q5,head) = index_105
| tail = head ),
inference(paramod,[status(thm)],[c_1442,c_4833]) ).
cnf(c_6070,plain,
( select(q5,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6069]) ).
cnf(c_5065,plain,
select(q5,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6070]) ).
cnf(c_6071,plain,
( index_297 = select(q48,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5037,c_1136]) ).
cnf(c_6072,plain,
( index_297 = select(q48,head)
| head = seq ),
inference(copy,[status(thm)],[c_6071]) ).
cnf(c_6073,plain,
( select(q48,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6072]) ).
cnf(c_5086,plain,
select(q48,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6073]) ).
cnf(c_6074,plain,
( select(queue_275,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5065,c_1140]) ).
cnf(c_6075,plain,
( select(queue_275,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6074]) ).
cnf(c_5090,plain,
select(queue_275,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6075]) ).
cnf(c_6076,plain,
( select(queue_257,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5086,c_1428]) ).
cnf(c_6077,plain,
( select(queue_257,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6076]) ).
cnf(c_5116,plain,
select(queue_257,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6077]) ).
cnf(c_6078,plain,
( index_105 = select(q6,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5090,c_1448]) ).
cnf(c_6079,plain,
( index_105 = select(q6,head)
| head = tail ),
inference(copy,[status(thm)],[c_6078]) ).
cnf(c_6080,plain,
( select(q6,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6079]) ).
cnf(c_5120,plain,
select(q6,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6080]) ).
cnf(c_6081,plain,
( index_297 = select(q47,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5116,c_1134]) ).
cnf(c_6082,plain,
( index_297 = select(q47,head)
| head = seq ),
inference(copy,[status(thm)],[c_6081]) ).
cnf(c_6083,plain,
( select(q47,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6082]) ).
cnf(c_5124,plain,
select(q47,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6083]) ).
cnf(c_6084,plain,
( select(queue_281,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5120,c_1142]) ).
cnf(c_6085,plain,
( select(queue_281,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6084]) ).
cnf(c_5128,plain,
select(queue_281,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6085]) ).
cnf(c_6086,plain,
( select(queue_251,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5124,c_1422]) ).
cnf(c_6087,plain,
( select(queue_251,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6086]) ).
cnf(c_5154,plain,
select(queue_251,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6087]) ).
cnf(c_6088,plain,
( index_105 = select(q7,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5128,c_1454]) ).
cnf(c_6089,plain,
( index_105 = select(q7,head)
| head = tail ),
inference(copy,[status(thm)],[c_6088]) ).
cnf(c_6090,plain,
( select(q7,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6089]) ).
cnf(c_5158,plain,
select(q7,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6090]) ).
cnf(c_6091,plain,
( index_297 = select(q46,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5154,c_1132]) ).
cnf(c_6092,plain,
( index_297 = select(q46,head)
| head = seq ),
inference(copy,[status(thm)],[c_6091]) ).
cnf(c_6093,plain,
( select(q46,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6092]) ).
cnf(c_5162,plain,
select(q46,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6093]) ).
cnf(c_6094,plain,
( select(queue_287,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5158,c_1144]) ).
cnf(c_6095,plain,
( select(queue_287,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6094]) ).
cnf(c_5166,plain,
select(queue_287,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6095]) ).
cnf(c_6096,plain,
( select(queue_245,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5162,c_1416]) ).
cnf(c_6097,plain,
( select(queue_245,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6096]) ).
cnf(c_5192,plain,
select(queue_245,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6097]) ).
cnf(c_6098,plain,
( index_105 = select(q8,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5166,c_1460]) ).
cnf(c_6099,plain,
( index_105 = select(q8,head)
| head = tail ),
inference(copy,[status(thm)],[c_6098]) ).
cnf(c_6100,plain,
( select(q8,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6099]) ).
cnf(c_5196,plain,
select(q8,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6100]) ).
cnf(c_6101,plain,
( index_297 = select(q45,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5192,c_1130]) ).
cnf(c_6102,plain,
( index_297 = select(q45,head)
| head = seq ),
inference(copy,[status(thm)],[c_6101]) ).
cnf(c_6103,plain,
( select(q45,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6102]) ).
cnf(c_5200,plain,
select(q45,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6103]) ).
cnf(c_6104,plain,
( select(queue_293,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5196,c_1148]) ).
cnf(c_6105,plain,
( select(queue_293,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6104]) ).
cnf(c_5204,plain,
select(queue_293,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6105]) ).
cnf(c_6106,plain,
( select(queue_239,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5200,c_1410]) ).
cnf(c_6107,plain,
( select(queue_239,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6106]) ).
cnf(c_5237,plain,
select(queue_239,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6107]) ).
cnf(c_6108,plain,
( index_105 = select(q9,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5204,c_1466]) ).
cnf(c_6109,plain,
( index_105 = select(q9,head)
| head = tail ),
inference(copy,[status(thm)],[c_6108]) ).
cnf(c_6110,plain,
( select(q9,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6109]) ).
cnf(c_5241,plain,
select(q9,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6110]) ).
cnf(c_6111,plain,
( index_297 = select(q44,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5237,c_1128]) ).
cnf(c_6112,plain,
( index_297 = select(q44,head)
| head = seq ),
inference(copy,[status(thm)],[c_6111]) ).
cnf(c_6113,plain,
( select(q44,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6112]) ).
cnf(c_5245,plain,
select(q44,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6113]) ).
cnf(c_6114,plain,
( select(queue_11,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5241,c_1080]) ).
cnf(c_6115,plain,
( select(queue_11,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6114]) ).
cnf(c_5249,plain,
select(queue_11,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6115]) ).
cnf(c_6116,plain,
( select(queue_233,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5245,c_1404]) ).
cnf(c_6117,plain,
( select(queue_233,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6116]) ).
cnf(c_5268,plain,
select(queue_233,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6117]) ).
cnf(c_6118,plain,
( index_105 = select(q10,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5249,c_1182]) ).
cnf(c_6119,plain,
( index_105 = select(q10,head)
| head = tail ),
inference(copy,[status(thm)],[c_6118]) ).
cnf(c_6120,plain,
( select(q10,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6119]) ).
cnf(c_5272,plain,
select(q10,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6120]) ).
cnf(c_6121,plain,
( index_297 = select(q43,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5268,c_1126]) ).
cnf(c_6122,plain,
( index_297 = select(q43,head)
| head = seq ),
inference(copy,[status(thm)],[c_6121]) ).
cnf(c_6123,plain,
( select(q43,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6122]) ).
cnf(c_5276,plain,
select(q43,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6123]) ).
cnf(c_6124,plain,
( select(queue_17,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5272,c_1102]) ).
cnf(c_6125,plain,
( select(queue_17,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6124]) ).
cnf(c_5280,plain,
select(queue_17,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6125]) ).
cnf(c_6126,plain,
( select(queue_227,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5276,c_1398]) ).
cnf(c_6127,plain,
( select(queue_227,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6126]) ).
cnf(c_5284,plain,
select(queue_227,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6127]) ).
cnf(c_6128,plain,
( index_105 = select(q11,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5280,c_1188]) ).
cnf(c_6129,plain,
( index_105 = select(q11,head)
| head = tail ),
inference(copy,[status(thm)],[c_6128]) ).
cnf(c_6130,plain,
( select(q11,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6129]) ).
cnf(c_5288,plain,
select(q11,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6130]) ).
cnf(c_6131,plain,
( index_297 = select(q42,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5284,c_1122]) ).
cnf(c_6132,plain,
( index_297 = select(q42,head)
| head = seq ),
inference(copy,[status(thm)],[c_6131]) ).
cnf(c_6133,plain,
( select(q42,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6132]) ).
cnf(c_5298,plain,
select(q42,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6133]) ).
cnf(c_6134,plain,
( select(queue_23,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5288,c_1124]) ).
cnf(c_6135,plain,
( select(queue_23,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6134]) ).
cnf(c_5302,plain,
select(queue_23,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6135]) ).
cnf(c_6136,plain,
( select(queue_221,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5298,c_1392]) ).
cnf(c_6137,plain,
( select(queue_221,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6136]) ).
cnf(c_5309,plain,
select(queue_221,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6137]) ).
cnf(c_6138,plain,
( index_105 = select(q12,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5302,c_1194]) ).
cnf(c_6139,plain,
( index_105 = select(q12,head)
| head = tail ),
inference(copy,[status(thm)],[c_6138]) ).
cnf(c_6140,plain,
( select(q12,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6139]) ).
cnf(c_5313,plain,
select(q12,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6140]) ).
cnf(c_6141,plain,
( index_297 = select(q41,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5309,c_1120]) ).
cnf(c_6142,plain,
( index_297 = select(q41,head)
| head = seq ),
inference(copy,[status(thm)],[c_6141]) ).
cnf(c_6143,plain,
( select(q41,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6142]) ).
cnf(c_5317,plain,
select(q41,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6143]) ).
cnf(c_6144,plain,
( select(queue_29,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5313,c_1146]) ).
cnf(c_6145,plain,
( select(queue_29,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6144]) ).
cnf(c_5327,plain,
select(queue_29,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6145]) ).
cnf(c_6146,plain,
( select(queue_215,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5317,c_1386]) ).
cnf(c_6147,plain,
( select(queue_215,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6146]) ).
cnf(c_5331,plain,
select(queue_215,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6147]) ).
cnf(c_6148,plain,
( index_105 = select(q13,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5327,c_1200]) ).
cnf(c_6149,plain,
( index_105 = select(q13,head)
| head = tail ),
inference(copy,[status(thm)],[c_6148]) ).
cnf(c_6150,plain,
( select(q13,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6149]) ).
cnf(c_5338,plain,
select(q13,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6150]) ).
cnf(c_6151,plain,
( index_297 = select(q40,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5331,c_1118]) ).
cnf(c_6152,plain,
( index_297 = select(q40,head)
| head = seq ),
inference(copy,[status(thm)],[c_6151]) ).
cnf(c_6153,plain,
( select(q40,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6152]) ).
cnf(c_5342,plain,
select(q40,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6153]) ).
cnf(c_6154,plain,
( select(queue_35,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5338,c_1150]) ).
cnf(c_6155,plain,
( select(queue_35,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6154]) ).
cnf(c_5346,plain,
select(queue_35,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6155]) ).
cnf(c_6156,plain,
( select(queue_209,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5342,c_1380]) ).
cnf(c_6157,plain,
( select(queue_209,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6156]) ).
cnf(c_5356,plain,
select(queue_209,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6157]) ).
cnf(c_6158,plain,
( index_105 = select(q14,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5346,c_1206]) ).
cnf(c_6159,plain,
( index_105 = select(q14,head)
| head = tail ),
inference(copy,[status(thm)],[c_6158]) ).
cnf(c_6160,plain,
( select(q14,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6159]) ).
cnf(c_5360,plain,
select(q14,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6160]) ).
cnf(c_6161,plain,
( index_297 = select(q39,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5356,c_1116]) ).
cnf(c_6162,plain,
( index_297 = select(q39,head)
| head = seq ),
inference(copy,[status(thm)],[c_6161]) ).
cnf(c_6163,plain,
( select(q39,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6162]) ).
cnf(c_5367,plain,
select(q39,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6163]) ).
cnf(c_6164,plain,
( select(queue_41,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5360,c_1152]) ).
cnf(c_6165,plain,
( select(queue_41,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6164]) ).
cnf(c_5371,plain,
select(queue_41,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6165]) ).
cnf(c_6166,plain,
( select(queue_197,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5367,c_1368]) ).
cnf(c_6167,plain,
( select(queue_197,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6166]) ).
cnf(c_5375,plain,
select(queue_197,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6167]) ).
cnf(c_6168,plain,
( index_105 = select(q15,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5371,c_1212]) ).
cnf(c_6169,plain,
( index_105 = select(q15,head)
| head = tail ),
inference(copy,[status(thm)],[c_6168]) ).
cnf(c_6170,plain,
( select(q15,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6169]) ).
cnf(c_5384,plain,
select(q15,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6170]) ).
cnf(c_6171,plain,
( index_297 = select(q38,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5375,c_1112]) ).
cnf(c_6172,plain,
( index_297 = select(q38,head)
| head = seq ),
inference(copy,[status(thm)],[c_6171]) ).
cnf(c_6173,plain,
( select(q38,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6172]) ).
cnf(c_5388,plain,
select(q38,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6173]) ).
cnf(c_6174,plain,
( select(queue_47,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5384,c_1154]) ).
cnf(c_6175,plain,
( select(queue_47,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6174]) ).
cnf(c_5392,plain,
select(queue_47,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6175]) ).
cnf(c_6176,plain,
( select(queue_191,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5388,c_1362]) ).
cnf(c_6177,plain,
( select(queue_191,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6176]) ).
cnf(c_5396,plain,
select(queue_191,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6177]) ).
cnf(c_6178,plain,
( index_105 = select(q16,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5392,c_1218]) ).
cnf(c_6179,plain,
( index_105 = select(q16,head)
| head = tail ),
inference(copy,[status(thm)],[c_6178]) ).
cnf(c_6180,plain,
( select(q16,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6179]) ).
cnf(c_5400,plain,
select(q16,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6180]) ).
cnf(c_6181,plain,
( index_297 = select(q37,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5396,c_1110]) ).
cnf(c_6182,plain,
( index_297 = select(q37,head)
| head = seq ),
inference(copy,[status(thm)],[c_6181]) ).
cnf(c_6183,plain,
( select(q37,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6182]) ).
cnf(c_5404,plain,
select(q37,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6183]) ).
cnf(c_6184,plain,
( select(queue_53,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5400,c_1158]) ).
cnf(c_6185,plain,
( select(queue_53,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6184]) ).
cnf(c_5413,plain,
select(queue_53,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6185]) ).
cnf(c_6186,plain,
( select(queue_185,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5404,c_1356]) ).
cnf(c_6187,plain,
( select(queue_185,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6186]) ).
cnf(c_5417,plain,
select(queue_185,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6187]) ).
cnf(c_6188,plain,
( index_105 = select(q17,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5413,c_1224]) ).
cnf(c_6189,plain,
( index_105 = select(q17,head)
| head = tail ),
inference(copy,[status(thm)],[c_6188]) ).
cnf(c_6190,plain,
( select(q17,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6189]) ).
cnf(c_5421,plain,
select(q17,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6190]) ).
cnf(c_6191,plain,
( index_297 = select(q36,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5417,c_1108]) ).
cnf(c_6192,plain,
( index_297 = select(q36,head)
| head = seq ),
inference(copy,[status(thm)],[c_6191]) ).
cnf(c_6193,plain,
( select(q36,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6192]) ).
cnf(c_5425,plain,
select(q36,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6193]) ).
cnf(c_6194,plain,
( select(queue_59,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5421,c_1160]) ).
cnf(c_6195,plain,
( select(queue_59,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6194]) ).
cnf(c_5429,plain,
select(queue_59,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6195]) ).
cnf(c_6196,plain,
( select(queue_179,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5425,c_1350]) ).
cnf(c_6197,plain,
( select(queue_179,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6196]) ).
cnf(c_5433,plain,
select(queue_179,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6197]) ).
cnf(c_6198,plain,
( index_105 = select(q18,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5429,c_1230]) ).
cnf(c_6199,plain,
( index_105 = select(q18,head)
| head = tail ),
inference(copy,[status(thm)],[c_6198]) ).
cnf(c_6200,plain,
( select(q18,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6199]) ).
cnf(c_5442,plain,
select(q18,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6200]) ).
cnf(c_6201,plain,
( index_297 = select(q35,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5433,c_1106]) ).
cnf(c_6202,plain,
( index_297 = select(q35,head)
| head = seq ),
inference(copy,[status(thm)],[c_6201]) ).
cnf(c_6203,plain,
( select(q35,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6202]) ).
cnf(c_5446,plain,
select(q35,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6203]) ).
cnf(c_6204,plain,
( select(queue_65,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5442,c_1162]) ).
cnf(c_6205,plain,
( select(queue_65,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6204]) ).
cnf(c_5450,plain,
select(queue_65,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6205]) ).
cnf(c_6206,plain,
( select(queue_173,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5446,c_1344]) ).
cnf(c_6207,plain,
( select(queue_173,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6206]) ).
cnf(c_5454,plain,
select(queue_173,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6207]) ).
cnf(c_6208,plain,
( index_105 = select(q19,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5450,c_1236]) ).
cnf(c_6209,plain,
( index_105 = select(q19,head)
| head = tail ),
inference(copy,[status(thm)],[c_6208]) ).
cnf(c_6210,plain,
( select(q19,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6209]) ).
cnf(c_5458,plain,
select(q19,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6210]) ).
cnf(c_6211,plain,
( index_297 = select(q34,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5454,c_1104]) ).
cnf(c_6212,plain,
( index_297 = select(q34,head)
| head = seq ),
inference(copy,[status(thm)],[c_6211]) ).
cnf(c_6213,plain,
( select(q34,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6212]) ).
cnf(c_5462,plain,
select(q34,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6213]) ).
cnf(c_6214,plain,
( select(queue_77,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5458,c_1166]) ).
cnf(c_6215,plain,
( select(queue_77,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6214]) ).
cnf(c_5471,plain,
select(queue_77,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6215]) ).
cnf(c_6216,plain,
( select(queue_167,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5462,c_1338]) ).
cnf(c_6217,plain,
( select(queue_167,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6216]) ).
cnf(c_5475,plain,
select(queue_167,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6217]) ).
cnf(c_6218,plain,
( index_105 = select(q20,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5471,c_1248]) ).
cnf(c_6219,plain,
( index_105 = select(q20,head)
| head = tail ),
inference(copy,[status(thm)],[c_6218]) ).
cnf(c_6220,plain,
( select(q20,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6219]) ).
cnf(c_5479,plain,
select(q20,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6220]) ).
cnf(c_6221,plain,
( index_297 = select(q33,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5475,c_1100]) ).
cnf(c_6222,plain,
( index_297 = select(q33,head)
| head = seq ),
inference(copy,[status(thm)],[c_6221]) ).
cnf(c_6223,plain,
( select(q33,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6222]) ).
cnf(c_5483,plain,
select(q33,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6223]) ).
cnf(c_6224,plain,
( select(queue_83,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5479,c_1168]) ).
cnf(c_6225,plain,
( select(queue_83,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6224]) ).
cnf(c_5487,plain,
select(queue_83,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6225]) ).
cnf(c_6226,plain,
( select(queue_161,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5483,c_1332]) ).
cnf(c_6227,plain,
( select(queue_161,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6226]) ).
cnf(c_5491,plain,
select(queue_161,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6227]) ).
cnf(c_6228,plain,
( index_105 = select(q21,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5487,c_1254]) ).
cnf(c_6229,plain,
( index_105 = select(q21,head)
| head = tail ),
inference(copy,[status(thm)],[c_6228]) ).
cnf(c_6230,plain,
( select(q21,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6229]) ).
cnf(c_5500,plain,
select(q21,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6230]) ).
cnf(c_6231,plain,
( index_297 = select(q32,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5491,c_1098]) ).
cnf(c_6232,plain,
( index_297 = select(q32,head)
| head = seq ),
inference(copy,[status(thm)],[c_6231]) ).
cnf(c_6233,plain,
( select(q32,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6232]) ).
cnf(c_5504,plain,
select(q32,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6233]) ).
cnf(c_6234,plain,
( select(queue_89,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5500,c_1170]) ).
cnf(c_6235,plain,
( select(queue_89,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6234]) ).
cnf(c_5508,plain,
select(queue_89,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6235]) ).
cnf(c_6236,plain,
( select(queue_155,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5504,c_1326]) ).
cnf(c_6237,plain,
( select(queue_155,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6236]) ).
cnf(c_5512,plain,
select(queue_155,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6237]) ).
cnf(c_6238,plain,
( index_105 = select(q22,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5508,c_1260]) ).
cnf(c_6239,plain,
( index_105 = select(q22,head)
| head = tail ),
inference(copy,[status(thm)],[c_6238]) ).
cnf(c_6240,plain,
( select(q22,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6239]) ).
cnf(c_5516,plain,
select(q22,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6240]) ).
cnf(c_6241,plain,
( index_297 = select(q31,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5512,c_1096]) ).
cnf(c_6242,plain,
( index_297 = select(q31,head)
| head = seq ),
inference(copy,[status(thm)],[c_6241]) ).
cnf(c_6243,plain,
( select(q31,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6242]) ).
cnf(c_5520,plain,
select(q31,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6243]) ).
cnf(c_6244,plain,
( select(queue_95,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5516,c_1172]) ).
cnf(c_6245,plain,
( select(queue_95,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6244]) ).
cnf(c_5529,plain,
select(queue_95,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6245]) ).
cnf(c_6246,plain,
( select(queue_149,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5520,c_1320]) ).
cnf(c_6247,plain,
( select(queue_149,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6246]) ).
cnf(c_5533,plain,
select(queue_149,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6247]) ).
cnf(c_6248,plain,
( index_105 = select(q23,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5529,c_1266]) ).
cnf(c_6249,plain,
( index_105 = select(q23,head)
| head = tail ),
inference(copy,[status(thm)],[c_6248]) ).
cnf(c_6250,plain,
( select(q23,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6249]) ).
cnf(c_5537,plain,
select(q23,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6250]) ).
cnf(c_6251,plain,
( index_297 = select(q30,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5533,c_1094]) ).
cnf(c_6252,plain,
( index_297 = select(q30,head)
| head = seq ),
inference(copy,[status(thm)],[c_6251]) ).
cnf(c_6253,plain,
( select(q30,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6252]) ).
cnf(c_5541,plain,
select(q30,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6253]) ).
cnf(c_6254,plain,
( select(queue_101,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5537,c_1076]) ).
cnf(c_6255,plain,
( select(queue_101,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6254]) ).
cnf(c_5545,plain,
select(queue_101,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6255]) ).
cnf(c_6256,plain,
( select(queue_143,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5541,c_1314]) ).
cnf(c_6257,plain,
( select(queue_143,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6256]) ).
cnf(c_5549,plain,
select(queue_143,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6257]) ).
cnf(c_6258,plain,
( index_105 = select(q24,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5545,c_1272]) ).
cnf(c_6259,plain,
( index_105 = select(q24,head)
| head = tail ),
inference(copy,[status(thm)],[c_6258]) ).
cnf(c_6260,plain,
( select(q24,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6259]) ).
cnf(c_5558,plain,
select(q24,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6260]) ).
cnf(c_6261,plain,
( index_297 = select(q29,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5549,c_1092]) ).
cnf(c_6262,plain,
( index_297 = select(q29,head)
| head = seq ),
inference(copy,[status(thm)],[c_6261]) ).
cnf(c_6263,plain,
( select(q29,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6262]) ).
cnf(c_5562,plain,
select(q29,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6263]) ).
cnf(c_6264,plain,
( select(queue_107,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5558,c_1078]) ).
cnf(c_6265,plain,
( select(queue_107,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6264]) ).
cnf(c_5566,plain,
select(queue_107,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6265]) ).
cnf(c_6266,plain,
( select(queue_131,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5562,c_1302]) ).
cnf(c_6267,plain,
( select(queue_131,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6266]) ).
cnf(c_5570,plain,
select(queue_131,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6267]) ).
cnf(c_6268,plain,
( index_105 = select(q25,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5566,c_1278]) ).
cnf(c_6269,plain,
( index_105 = select(q25,head)
| head = tail ),
inference(copy,[status(thm)],[c_6268]) ).
cnf(c_6270,plain,
( select(q25,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6269]) ).
cnf(c_5574,plain,
select(q25,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6270]) ).
cnf(c_6271,plain,
( index_297 = select(q28,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5570,c_1088]) ).
cnf(c_6272,plain,
( index_297 = select(q28,head)
| head = seq ),
inference(copy,[status(thm)],[c_6271]) ).
cnf(c_6273,plain,
( select(q28,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6272]) ).
cnf(c_5578,plain,
select(q28,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6273]) ).
cnf(c_6274,plain,
( select(queue_113,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5574,c_1082]) ).
cnf(c_6275,plain,
( select(queue_113,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6274]) ).
cnf(c_5587,plain,
select(queue_113,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6275]) ).
cnf(c_6276,plain,
( select(queue_125,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5578,c_1296]) ).
cnf(c_6277,plain,
( select(queue_125,head) = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6276]) ).
cnf(c_5591,plain,
select(queue_125,head) = index_297,
inference(resolve,[status(thm)],[c_3,c_6277]) ).
cnf(c_6278,plain,
( index_105 = select(q26,head)
| tail = head ),
inference(paramod,[status(thm)],[c_5587,c_1284]) ).
cnf(c_6279,plain,
( index_105 = select(q26,head)
| head = tail ),
inference(copy,[status(thm)],[c_6278]) ).
cnf(c_6280,plain,
( select(q26,head) = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6279]) ).
cnf(c_5595,plain,
select(q26,head) = index_105,
inference(resolve,[status(thm)],[c_3,c_6280]) ).
cnf(c_6281,plain,
( index_297 = select(q27,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5591,c_1086]) ).
cnf(c_6282,plain,
( index_297 = select(q27,head)
| head = seq ),
inference(copy,[status(thm)],[c_6281]) ).
cnf(c_6283,plain,
( select(q27,head) = index_297
| head = seq ),
inference(copy,[status(thm)],[c_6282]) ).
cnf(c_5599,plain,
select(q27,head) = index_297,
inference(resolve,[status(thm)],[c_4,c_6283]) ).
cnf(c_6284,plain,
( select(queue_119,head) = index_105
| seq = head ),
inference(paramod,[status(thm)],[c_5595,c_1084]) ).
cnf(c_6285,plain,
( select(queue_119,head) = index_105
| head = seq ),
inference(copy,[status(thm)],[c_6284]) ).
cnf(c_5603,plain,
select(queue_119,head) = index_105,
inference(resolve,[status(thm)],[c_4,c_6285]) ).
cnf(c_6286,plain,
( select(queue_119,head) = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5599,c_1290]) ).
cnf(c_6287,plain,
( index_105 = index_297
| tail = head ),
inference(paramod,[status(thm)],[c_5603,c_6286]) ).
cnf(c_6288,plain,
( index_105 = index_297
| head = tail ),
inference(copy,[status(thm)],[c_6287]) ).
cnf(c_6289,plain,
( index_297 = index_105
| head = tail ),
inference(copy,[status(thm)],[c_6288]) ).
cnf(c_5607,plain,
index_297 = index_105,
inference(resolve,[status(thm)],[c_3,c_6289]) ).
cnf(c_6290,plain,
select(earray_296,index_105) = elem_298,
inference(paramod,[status(thm)],[c_5607,c_211]) ).
cnf(c_6291,plain,
e48 = elem_298,
inference(paramod,[status(thm)],[c_5058,c_6290]) ).
cnf(c_6292,plain,
elem_298 = e48,
inference(copy,[status(thm)],[c_6291]) ).
cnf(c_5801,plain,
$false,
inference(resolve,[status(thm)],[c_5059,c_6292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n002.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sat Sep 26 14:34:25 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.39 % Process 1955393 was started by sandbox2 on n002,
% 0.11/5.39 % Sat Sep 26 14:34:25 2026
% 0.11/5.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/5.40
% 0.16/5.40 % From the command line: assign(max_seconds, 300).
% 29.65/9.74
% 29.65/9.74 % given #500 (T,wt=8): 2493 index_75 = index_111. [back_rewrite(2272),rewrite([2408(2)])].
% 29.65/9.74
% 29.65/9.74 % given #1000 (A,wt=20): 1200 tail = A | select(queue_29,A) = select(q13,A). [para(722(a,1),2(b,1,1)),flip(b)].
% 29.65/9.74
% 29.65/9.74 % SZS status Unsatisfiable for theBenchmark
% 29.65/9.74
% 29.65/9.74 % Proof 1 at 3.74 (+ 0.38) seconds.
% 29.65/9.74 % Length of proof is 935.
% 29.65/9.74 % Level of proof is 84.
% 29.65/9.74 % Maximum clause weight is 36.000.
% 29.65/9.74 % Given clauses 1287.
% 29.65/9.74
% 29.65/9.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------