%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:44 AM UTC 2026
% Result : Unsatisfiable 3.38s 0.88s
% Output : CNFRefutation 3.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 135
% Number of leaves : 251
% Syntax : Number of formulae : 1321 (1321 unt; 0 def)
% Number of atoms : 1321 (1320 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 298 ( 298 usr; 288 con; 0-3 aty)
% Number of variables : 40 ( 8 sgn 19 !; 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(a1_seq,axiom,
! [VAR_0,VAR_1] : rselect_seq(rstore_seq(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_seq) ).
cnf(c_3,plain,
rselect_seq(rstore_seq(A,B)) = B,
inference(clausify,[status(thm)],[a1_seq]) ).
fof(a1_head,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_head(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_head) ).
cnf(c_4,plain,
rselect_head(rstore_head(A,B)) = B,
inference(clausify,[status(thm)],[a1_head]) ).
fof(a1_tail,axiom,
! [VAR_0,VAR_1] : rselect_tail(rstore_tail(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_tail) ).
cnf(c_5,plain,
rselect_tail(rstore_tail(A,B)) = B,
inference(clausify,[status(thm)],[a1_tail]) ).
fof(a2_seq_tail,axiom,
! [VAR_0,VAR_1] : rselect_seq(rstore_tail(VAR_0,VAR_1)) = rselect_seq(VAR_0),
file('theBenchmark.p',a2_seq_tail) ).
cnf(c_7,plain,
rselect_seq(rstore_tail(A,B)) = rselect_seq(A),
inference(clausify,[status(thm)],[a2_seq_tail]) ).
fof(a2_head_tail,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_tail(VAR_0,VAR_1)) = rselect_head(VAR_0),
file('theBenchmark.p',a2_head_tail) ).
cnf(c_8,plain,
rselect_head(rstore_tail(A,B)) = rselect_head(A),
inference(clausify,[status(thm)],[a2_head_tail]) ).
fof(a2_head_seq,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_seq(VAR_0,VAR_1)) = rselect_head(VAR_0),
file('theBenchmark.p',a2_head_seq) ).
cnf(c_9,plain,
rselect_head(rstore_seq(A,B)) = rselect_head(A),
inference(clausify,[status(thm)],[a2_head_seq]) ).
fof(a2_tail_head,axiom,
! [VAR_0,VAR_1] : rselect_tail(rstore_head(VAR_0,VAR_1)) = rselect_tail(VAR_0),
file('theBenchmark.p',a2_tail_head) ).
cnf(c_11,plain,
rselect_tail(rstore_head(A,B)) = rselect_tail(A),
inference(clausify,[status(thm)],[a2_tail_head]) ).
fof(ps,axiom,
! [VAR_0] : p(s(VAR_0)) = VAR_0,
file('theBenchmark.p',ps) ).
cnf(c_12,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_16,plain,
s(s(s(A))) = A,
inference(clausify,[status(thm)],[circular]) ).
fof(hyp54,axiom,
earray_244 = store(earray_242,index_243,e45),
file('theBenchmark.p',hyp54) ).
cnf(c_125,plain,
earray_244 = store(earray_242,index_243,e45),
inference(clausify,[status(thm)],[hyp54]) ).
cnf(c_126,plain,
store(earray_242,index_243,e45) = earray_244,
inference(copy,[status(thm)],[c_125]) ).
fof(hyp66,axiom,
earray_278 = rselect_seq(q46),
file('theBenchmark.p',hyp66) ).
cnf(c_149,plain,
earray_278 = rselect_seq(q46),
inference(clausify,[status(thm)],[hyp66]) ).
cnf(c_150,plain,
rselect_seq(q46) = earray_278,
inference(copy,[status(thm)],[c_149]) ).
fof(hyp93,axiom,
elem_280 = select(earray_278,index_279),
file('theBenchmark.p',hyp93) ).
cnf(c_203,plain,
elem_280 = select(earray_278,index_279),
inference(clausify,[status(thm)],[hyp93]) ).
cnf(c_204,plain,
select(earray_278,index_279) = elem_280,
inference(copy,[status(thm)],[c_203]) ).
fof(hyp94,axiom,
elem_283 = select(earray_278,index_282),
file('theBenchmark.p',hyp94) ).
cnf(c_205,plain,
elem_283 = select(earray_278,index_282),
inference(clausify,[status(thm)],[hyp94]) ).
cnf(c_206,plain,
select(earray_278,index_282) = elem_283,
inference(copy,[status(thm)],[c_205]) ).
fof(hyp95,axiom,
index_0 = rselect_tail(q),
file('theBenchmark.p',hyp95) ).
cnf(c_207,plain,
index_0 = rselect_tail(q),
inference(clausify,[status(thm)],[hyp95]) ).
cnf(c_208,plain,
rselect_tail(q) = index_0,
inference(copy,[status(thm)],[c_207]) ).
fof(hyp96,axiom,
index_102 = s(index_99),
file('theBenchmark.p',hyp96) ).
cnf(c_209,plain,
index_102 = s(index_99),
inference(clausify,[status(thm)],[hyp96]) ).
cnf(c_210,plain,
s(index_99) = index_102,
inference(copy,[status(thm)],[c_209]) ).
fof(hyp97,axiom,
index_105 = rselect_tail(q24),
file('theBenchmark.p',hyp97) ).
cnf(c_211,plain,
index_105 = rselect_tail(q24),
inference(clausify,[status(thm)],[hyp97]) ).
cnf(c_212,plain,
rselect_tail(q24) = index_105,
inference(copy,[status(thm)],[c_211]) ).
fof(hyp98,axiom,
index_108 = s(index_105),
file('theBenchmark.p',hyp98) ).
cnf(c_213,plain,
index_108 = s(index_105),
inference(clausify,[status(thm)],[hyp98]) ).
cnf(c_214,plain,
s(index_105) = index_108,
inference(copy,[status(thm)],[c_213]) ).
fof(hyp99,axiom,
index_111 = rselect_tail(q25),
file('theBenchmark.p',hyp99) ).
cnf(c_215,plain,
index_111 = rselect_tail(q25),
inference(clausify,[status(thm)],[hyp99]) ).
cnf(c_216,plain,
rselect_tail(q25) = index_111,
inference(copy,[status(thm)],[c_215]) ).
fof(hyp100,axiom,
index_114 = s(index_111),
file('theBenchmark.p',hyp100) ).
cnf(c_217,plain,
index_114 = s(index_111),
inference(clausify,[status(thm)],[hyp100]) ).
cnf(c_218,plain,
s(index_111) = index_114,
inference(copy,[status(thm)],[c_217]) ).
fof(hyp101,axiom,
index_117 = rselect_tail(q26),
file('theBenchmark.p',hyp101) ).
cnf(c_219,plain,
index_117 = rselect_tail(q26),
inference(clausify,[status(thm)],[hyp101]) ).
cnf(c_220,plain,
rselect_tail(q26) = index_117,
inference(copy,[status(thm)],[c_219]) ).
fof(hyp102,axiom,
index_12 = s(index_9),
file('theBenchmark.p',hyp102) ).
cnf(c_221,plain,
index_12 = s(index_9),
inference(clausify,[status(thm)],[hyp102]) ).
cnf(c_222,plain,
s(index_9) = index_12,
inference(copy,[status(thm)],[c_221]) ).
fof(hyp103,axiom,
index_120 = s(index_117),
file('theBenchmark.p',hyp103) ).
cnf(c_223,plain,
index_120 = s(index_117),
inference(clausify,[status(thm)],[hyp103]) ).
cnf(c_224,plain,
s(index_117) = index_120,
inference(copy,[status(thm)],[c_223]) ).
fof(hyp104,axiom,
index_123 = rselect_tail(q27),
file('theBenchmark.p',hyp104) ).
cnf(c_225,plain,
index_123 = rselect_tail(q27),
inference(clausify,[status(thm)],[hyp104]) ).
cnf(c_226,plain,
rselect_tail(q27) = index_123,
inference(copy,[status(thm)],[c_225]) ).
fof(hyp105,axiom,
index_126 = s(index_123),
file('theBenchmark.p',hyp105) ).
cnf(c_227,plain,
index_126 = s(index_123),
inference(clausify,[status(thm)],[hyp105]) ).
cnf(c_228,plain,
s(index_123) = index_126,
inference(copy,[status(thm)],[c_227]) ).
fof(hyp106,axiom,
index_129 = rselect_tail(q28),
file('theBenchmark.p',hyp106) ).
cnf(c_229,plain,
index_129 = rselect_tail(q28),
inference(clausify,[status(thm)],[hyp106]) ).
cnf(c_230,plain,
rselect_tail(q28) = index_129,
inference(copy,[status(thm)],[c_229]) ).
fof(hyp107,axiom,
index_132 = s(index_129),
file('theBenchmark.p',hyp107) ).
cnf(c_231,plain,
index_132 = s(index_129),
inference(clausify,[status(thm)],[hyp107]) ).
cnf(c_232,plain,
s(index_129) = index_132,
inference(copy,[status(thm)],[c_231]) ).
fof(hyp108,axiom,
index_135 = rselect_tail(q2),
file('theBenchmark.p',hyp108) ).
cnf(c_233,plain,
index_135 = rselect_tail(q2),
inference(clausify,[status(thm)],[hyp108]) ).
cnf(c_234,plain,
rselect_tail(q2) = index_135,
inference(copy,[status(thm)],[c_233]) ).
fof(hyp109,axiom,
index_138 = s(index_135),
file('theBenchmark.p',hyp109) ).
cnf(c_235,plain,
index_138 = s(index_135),
inference(clausify,[status(thm)],[hyp109]) ).
cnf(c_236,plain,
s(index_135) = index_138,
inference(copy,[status(thm)],[c_235]) ).
fof(hyp110,axiom,
index_141 = rselect_tail(q29),
file('theBenchmark.p',hyp110) ).
cnf(c_237,plain,
index_141 = rselect_tail(q29),
inference(clausify,[status(thm)],[hyp110]) ).
cnf(c_238,plain,
rselect_tail(q29) = index_141,
inference(copy,[status(thm)],[c_237]) ).
fof(hyp111,axiom,
index_144 = s(index_141),
file('theBenchmark.p',hyp111) ).
cnf(c_239,plain,
index_144 = s(index_141),
inference(clausify,[status(thm)],[hyp111]) ).
cnf(c_240,plain,
s(index_141) = index_144,
inference(copy,[status(thm)],[c_239]) ).
fof(hyp112,axiom,
index_147 = rselect_tail(q30),
file('theBenchmark.p',hyp112) ).
cnf(c_241,plain,
index_147 = rselect_tail(q30),
inference(clausify,[status(thm)],[hyp112]) ).
cnf(c_242,plain,
rselect_tail(q30) = index_147,
inference(copy,[status(thm)],[c_241]) ).
fof(hyp113,axiom,
index_15 = rselect_tail(q10),
file('theBenchmark.p',hyp113) ).
cnf(c_243,plain,
index_15 = rselect_tail(q10),
inference(clausify,[status(thm)],[hyp113]) ).
cnf(c_244,plain,
rselect_tail(q10) = index_15,
inference(copy,[status(thm)],[c_243]) ).
fof(hyp114,axiom,
index_150 = s(index_147),
file('theBenchmark.p',hyp114) ).
cnf(c_245,plain,
index_150 = s(index_147),
inference(clausify,[status(thm)],[hyp114]) ).
cnf(c_246,plain,
s(index_147) = index_150,
inference(copy,[status(thm)],[c_245]) ).
fof(hyp115,axiom,
index_153 = rselect_tail(q31),
file('theBenchmark.p',hyp115) ).
cnf(c_247,plain,
index_153 = rselect_tail(q31),
inference(clausify,[status(thm)],[hyp115]) ).
cnf(c_248,plain,
rselect_tail(q31) = index_153,
inference(copy,[status(thm)],[c_247]) ).
fof(hyp116,axiom,
index_156 = s(index_153),
file('theBenchmark.p',hyp116) ).
cnf(c_249,plain,
index_156 = s(index_153),
inference(clausify,[status(thm)],[hyp116]) ).
cnf(c_250,plain,
s(index_153) = index_156,
inference(copy,[status(thm)],[c_249]) ).
fof(hyp117,axiom,
index_159 = rselect_tail(q32),
file('theBenchmark.p',hyp117) ).
cnf(c_251,plain,
index_159 = rselect_tail(q32),
inference(clausify,[status(thm)],[hyp117]) ).
cnf(c_252,plain,
rselect_tail(q32) = index_159,
inference(copy,[status(thm)],[c_251]) ).
fof(hyp118,axiom,
index_162 = s(index_159),
file('theBenchmark.p',hyp118) ).
cnf(c_253,plain,
index_162 = s(index_159),
inference(clausify,[status(thm)],[hyp118]) ).
cnf(c_254,plain,
s(index_159) = index_162,
inference(copy,[status(thm)],[c_253]) ).
fof(hyp119,axiom,
index_165 = rselect_tail(q33),
file('theBenchmark.p',hyp119) ).
cnf(c_255,plain,
index_165 = rselect_tail(q33),
inference(clausify,[status(thm)],[hyp119]) ).
cnf(c_256,plain,
rselect_tail(q33) = index_165,
inference(copy,[status(thm)],[c_255]) ).
fof(hyp120,axiom,
index_168 = s(index_165),
file('theBenchmark.p',hyp120) ).
cnf(c_257,plain,
index_168 = s(index_165),
inference(clausify,[status(thm)],[hyp120]) ).
cnf(c_258,plain,
s(index_165) = index_168,
inference(copy,[status(thm)],[c_257]) ).
fof(hyp121,axiom,
index_171 = rselect_tail(q34),
file('theBenchmark.p',hyp121) ).
cnf(c_259,plain,
index_171 = rselect_tail(q34),
inference(clausify,[status(thm)],[hyp121]) ).
cnf(c_260,plain,
rselect_tail(q34) = index_171,
inference(copy,[status(thm)],[c_259]) ).
fof(hyp122,axiom,
index_174 = s(index_171),
file('theBenchmark.p',hyp122) ).
cnf(c_261,plain,
index_174 = s(index_171),
inference(clausify,[status(thm)],[hyp122]) ).
cnf(c_262,plain,
s(index_171) = index_174,
inference(copy,[status(thm)],[c_261]) ).
fof(hyp123,axiom,
index_177 = rselect_tail(q35),
file('theBenchmark.p',hyp123) ).
cnf(c_263,plain,
index_177 = rselect_tail(q35),
inference(clausify,[status(thm)],[hyp123]) ).
cnf(c_264,plain,
rselect_tail(q35) = index_177,
inference(copy,[status(thm)],[c_263]) ).
fof(hyp124,axiom,
index_18 = s(index_15),
file('theBenchmark.p',hyp124) ).
cnf(c_265,plain,
index_18 = s(index_15),
inference(clausify,[status(thm)],[hyp124]) ).
cnf(c_266,plain,
s(index_15) = index_18,
inference(copy,[status(thm)],[c_265]) ).
fof(hyp125,axiom,
index_180 = s(index_177),
file('theBenchmark.p',hyp125) ).
cnf(c_267,plain,
index_180 = s(index_177),
inference(clausify,[status(thm)],[hyp125]) ).
cnf(c_268,plain,
s(index_177) = index_180,
inference(copy,[status(thm)],[c_267]) ).
fof(hyp126,axiom,
index_183 = rselect_tail(q36),
file('theBenchmark.p',hyp126) ).
cnf(c_269,plain,
index_183 = rselect_tail(q36),
inference(clausify,[status(thm)],[hyp126]) ).
cnf(c_270,plain,
rselect_tail(q36) = index_183,
inference(copy,[status(thm)],[c_269]) ).
fof(hyp127,axiom,
index_186 = s(index_183),
file('theBenchmark.p',hyp127) ).
cnf(c_271,plain,
index_186 = s(index_183),
inference(clausify,[status(thm)],[hyp127]) ).
cnf(c_272,plain,
s(index_183) = index_186,
inference(copy,[status(thm)],[c_271]) ).
fof(hyp128,axiom,
index_189 = rselect_tail(q37),
file('theBenchmark.p',hyp128) ).
cnf(c_273,plain,
index_189 = rselect_tail(q37),
inference(clausify,[status(thm)],[hyp128]) ).
cnf(c_274,plain,
rselect_tail(q37) = index_189,
inference(copy,[status(thm)],[c_273]) ).
fof(hyp129,axiom,
index_192 = s(index_189),
file('theBenchmark.p',hyp129) ).
cnf(c_275,plain,
index_192 = s(index_189),
inference(clausify,[status(thm)],[hyp129]) ).
cnf(c_276,plain,
s(index_189) = index_192,
inference(copy,[status(thm)],[c_275]) ).
fof(hyp130,axiom,
index_195 = rselect_tail(q38),
file('theBenchmark.p',hyp130) ).
cnf(c_277,plain,
index_195 = rselect_tail(q38),
inference(clausify,[status(thm)],[hyp130]) ).
cnf(c_278,plain,
rselect_tail(q38) = index_195,
inference(copy,[status(thm)],[c_277]) ).
fof(hyp131,axiom,
index_198 = s(index_195),
file('theBenchmark.p',hyp131) ).
cnf(c_279,plain,
index_198 = s(index_195),
inference(clausify,[status(thm)],[hyp131]) ).
cnf(c_280,plain,
s(index_195) = index_198,
inference(copy,[status(thm)],[c_279]) ).
fof(hyp132,axiom,
index_201 = rselect_tail(q3),
file('theBenchmark.p',hyp132) ).
cnf(c_281,plain,
index_201 = rselect_tail(q3),
inference(clausify,[status(thm)],[hyp132]) ).
cnf(c_282,plain,
rselect_tail(q3) = index_201,
inference(copy,[status(thm)],[c_281]) ).
fof(hyp133,axiom,
index_204 = s(index_201),
file('theBenchmark.p',hyp133) ).
cnf(c_283,plain,
index_204 = s(index_201),
inference(clausify,[status(thm)],[hyp133]) ).
cnf(c_284,plain,
s(index_201) = index_204,
inference(copy,[status(thm)],[c_283]) ).
fof(hyp134,axiom,
index_207 = rselect_tail(q39),
file('theBenchmark.p',hyp134) ).
cnf(c_285,plain,
index_207 = rselect_tail(q39),
inference(clausify,[status(thm)],[hyp134]) ).
cnf(c_286,plain,
rselect_tail(q39) = index_207,
inference(copy,[status(thm)],[c_285]) ).
fof(hyp135,axiom,
index_21 = rselect_tail(q11),
file('theBenchmark.p',hyp135) ).
cnf(c_287,plain,
index_21 = rselect_tail(q11),
inference(clausify,[status(thm)],[hyp135]) ).
cnf(c_288,plain,
rselect_tail(q11) = index_21,
inference(copy,[status(thm)],[c_287]) ).
fof(hyp136,axiom,
index_210 = s(index_207),
file('theBenchmark.p',hyp136) ).
cnf(c_289,plain,
index_210 = s(index_207),
inference(clausify,[status(thm)],[hyp136]) ).
cnf(c_290,plain,
s(index_207) = index_210,
inference(copy,[status(thm)],[c_289]) ).
fof(hyp137,axiom,
index_213 = rselect_tail(q40),
file('theBenchmark.p',hyp137) ).
cnf(c_291,plain,
index_213 = rselect_tail(q40),
inference(clausify,[status(thm)],[hyp137]) ).
cnf(c_292,plain,
rselect_tail(q40) = index_213,
inference(copy,[status(thm)],[c_291]) ).
fof(hyp138,axiom,
index_216 = s(index_213),
file('theBenchmark.p',hyp138) ).
cnf(c_293,plain,
index_216 = s(index_213),
inference(clausify,[status(thm)],[hyp138]) ).
cnf(c_294,plain,
s(index_213) = index_216,
inference(copy,[status(thm)],[c_293]) ).
fof(hyp139,axiom,
index_219 = rselect_tail(q41),
file('theBenchmark.p',hyp139) ).
cnf(c_295,plain,
index_219 = rselect_tail(q41),
inference(clausify,[status(thm)],[hyp139]) ).
cnf(c_296,plain,
rselect_tail(q41) = index_219,
inference(copy,[status(thm)],[c_295]) ).
fof(hyp140,axiom,
index_222 = s(index_219),
file('theBenchmark.p',hyp140) ).
cnf(c_297,plain,
index_222 = s(index_219),
inference(clausify,[status(thm)],[hyp140]) ).
cnf(c_298,plain,
s(index_219) = index_222,
inference(copy,[status(thm)],[c_297]) ).
fof(hyp141,axiom,
index_225 = rselect_tail(q42),
file('theBenchmark.p',hyp141) ).
cnf(c_299,plain,
index_225 = rselect_tail(q42),
inference(clausify,[status(thm)],[hyp141]) ).
cnf(c_300,plain,
rselect_tail(q42) = index_225,
inference(copy,[status(thm)],[c_299]) ).
fof(hyp142,axiom,
index_228 = s(index_225),
file('theBenchmark.p',hyp142) ).
cnf(c_301,plain,
index_228 = s(index_225),
inference(clausify,[status(thm)],[hyp142]) ).
cnf(c_302,plain,
s(index_225) = index_228,
inference(copy,[status(thm)],[c_301]) ).
fof(hyp143,axiom,
index_231 = rselect_tail(q43),
file('theBenchmark.p',hyp143) ).
cnf(c_303,plain,
index_231 = rselect_tail(q43),
inference(clausify,[status(thm)],[hyp143]) ).
cnf(c_304,plain,
rselect_tail(q43) = index_231,
inference(copy,[status(thm)],[c_303]) ).
fof(hyp144,axiom,
index_234 = s(index_231),
file('theBenchmark.p',hyp144) ).
cnf(c_305,plain,
index_234 = s(index_231),
inference(clausify,[status(thm)],[hyp144]) ).
cnf(c_306,plain,
s(index_231) = index_234,
inference(copy,[status(thm)],[c_305]) ).
fof(hyp145,axiom,
index_237 = rselect_tail(q44),
file('theBenchmark.p',hyp145) ).
cnf(c_307,plain,
index_237 = rselect_tail(q44),
inference(clausify,[status(thm)],[hyp145]) ).
cnf(c_308,plain,
rselect_tail(q44) = index_237,
inference(copy,[status(thm)],[c_307]) ).
fof(hyp146,axiom,
index_24 = s(index_21),
file('theBenchmark.p',hyp146) ).
cnf(c_309,plain,
index_24 = s(index_21),
inference(clausify,[status(thm)],[hyp146]) ).
cnf(c_310,plain,
s(index_21) = index_24,
inference(copy,[status(thm)],[c_309]) ).
fof(hyp147,axiom,
index_240 = s(index_237),
file('theBenchmark.p',hyp147) ).
cnf(c_311,plain,
index_240 = s(index_237),
inference(clausify,[status(thm)],[hyp147]) ).
cnf(c_312,plain,
s(index_237) = index_240,
inference(copy,[status(thm)],[c_311]) ).
fof(hyp148,axiom,
index_243 = rselect_tail(q45),
file('theBenchmark.p',hyp148) ).
cnf(c_313,plain,
index_243 = rselect_tail(q45),
inference(clausify,[status(thm)],[hyp148]) ).
cnf(c_314,plain,
rselect_tail(q45) = index_243,
inference(copy,[status(thm)],[c_313]) ).
fof(hyp149,axiom,
index_246 = s(index_243),
file('theBenchmark.p',hyp149) ).
cnf(c_315,plain,
index_246 = s(index_243),
inference(clausify,[status(thm)],[hyp149]) ).
cnf(c_316,plain,
s(index_243) = index_246,
inference(copy,[status(thm)],[c_315]) ).
fof(hyp150,axiom,
index_249 = rselect_tail(q4),
file('theBenchmark.p',hyp150) ).
cnf(c_317,plain,
index_249 = rselect_tail(q4),
inference(clausify,[status(thm)],[hyp150]) ).
cnf(c_318,plain,
rselect_tail(q4) = index_249,
inference(copy,[status(thm)],[c_317]) ).
fof(hyp151,axiom,
index_252 = s(index_249),
file('theBenchmark.p',hyp151) ).
cnf(c_319,plain,
index_252 = s(index_249),
inference(clausify,[status(thm)],[hyp151]) ).
cnf(c_320,plain,
s(index_249) = index_252,
inference(copy,[status(thm)],[c_319]) ).
fof(hyp152,axiom,
index_255 = rselect_tail(q5),
file('theBenchmark.p',hyp152) ).
cnf(c_321,plain,
index_255 = rselect_tail(q5),
inference(clausify,[status(thm)],[hyp152]) ).
cnf(c_322,plain,
rselect_tail(q5) = index_255,
inference(copy,[status(thm)],[c_321]) ).
fof(hyp153,axiom,
index_258 = s(index_255),
file('theBenchmark.p',hyp153) ).
cnf(c_323,plain,
index_258 = s(index_255),
inference(clausify,[status(thm)],[hyp153]) ).
cnf(c_324,plain,
s(index_255) = index_258,
inference(copy,[status(thm)],[c_323]) ).
fof(hyp154,axiom,
index_261 = rselect_tail(q6),
file('theBenchmark.p',hyp154) ).
cnf(c_325,plain,
index_261 = rselect_tail(q6),
inference(clausify,[status(thm)],[hyp154]) ).
cnf(c_326,plain,
rselect_tail(q6) = index_261,
inference(copy,[status(thm)],[c_325]) ).
fof(hyp155,axiom,
index_264 = s(index_261),
file('theBenchmark.p',hyp155) ).
cnf(c_327,plain,
index_264 = s(index_261),
inference(clausify,[status(thm)],[hyp155]) ).
cnf(c_328,plain,
s(index_261) = index_264,
inference(copy,[status(thm)],[c_327]) ).
fof(hyp156,axiom,
index_267 = rselect_tail(q7),
file('theBenchmark.p',hyp156) ).
cnf(c_329,plain,
index_267 = rselect_tail(q7),
inference(clausify,[status(thm)],[hyp156]) ).
cnf(c_330,plain,
rselect_tail(q7) = index_267,
inference(copy,[status(thm)],[c_329]) ).
fof(hyp157,axiom,
index_27 = rselect_tail(q12),
file('theBenchmark.p',hyp157) ).
cnf(c_331,plain,
index_27 = rselect_tail(q12),
inference(clausify,[status(thm)],[hyp157]) ).
cnf(c_332,plain,
rselect_tail(q12) = index_27,
inference(copy,[status(thm)],[c_331]) ).
fof(hyp158,axiom,
index_270 = s(index_267),
file('theBenchmark.p',hyp158) ).
cnf(c_333,plain,
index_270 = s(index_267),
inference(clausify,[status(thm)],[hyp158]) ).
cnf(c_334,plain,
s(index_267) = index_270,
inference(copy,[status(thm)],[c_333]) ).
fof(hyp159,axiom,
index_273 = rselect_tail(q8),
file('theBenchmark.p',hyp159) ).
cnf(c_335,plain,
index_273 = rselect_tail(q8),
inference(clausify,[status(thm)],[hyp159]) ).
cnf(c_336,plain,
rselect_tail(q8) = index_273,
inference(copy,[status(thm)],[c_335]) ).
fof(hyp160,axiom,
index_276 = s(index_273),
file('theBenchmark.p',hyp160) ).
cnf(c_337,plain,
index_276 = s(index_273),
inference(clausify,[status(thm)],[hyp160]) ).
cnf(c_338,plain,
s(index_273) = index_276,
inference(copy,[status(thm)],[c_337]) ).
fof(hyp161,axiom,
index_279 = rselect_head(q46),
file('theBenchmark.p',hyp161) ).
cnf(c_339,plain,
index_279 = rselect_head(q46),
inference(clausify,[status(thm)],[hyp161]) ).
cnf(c_340,plain,
rselect_head(q46) = index_279,
inference(copy,[status(thm)],[c_339]) ).
fof(hyp162,axiom,
index_281 = rselect_tail(q46),
file('theBenchmark.p',hyp162) ).
cnf(c_341,plain,
index_281 = rselect_tail(q46),
inference(clausify,[status(thm)],[hyp162]) ).
cnf(c_342,plain,
rselect_tail(q46) = index_281,
inference(copy,[status(thm)],[c_341]) ).
fof(hyp163,axiom,
s(index_282) = index_281,
file('theBenchmark.p',hyp163) ).
cnf(c_343,plain,
s(index_282) = index_281,
inference(clausify,[status(thm)],[hyp163]) ).
fof(hyp164,axiom,
index_3 = rselect_tail(q0),
file('theBenchmark.p',hyp164) ).
cnf(c_344,plain,
index_3 = rselect_tail(q0),
inference(clausify,[status(thm)],[hyp164]) ).
cnf(c_345,plain,
rselect_tail(q0) = index_3,
inference(copy,[status(thm)],[c_344]) ).
fof(hyp165,axiom,
index_30 = s(index_27),
file('theBenchmark.p',hyp165) ).
cnf(c_346,plain,
index_30 = s(index_27),
inference(clausify,[status(thm)],[hyp165]) ).
cnf(c_347,plain,
s(index_27) = index_30,
inference(copy,[status(thm)],[c_346]) ).
fof(hyp166,axiom,
index_33 = rselect_tail(q13),
file('theBenchmark.p',hyp166) ).
cnf(c_348,plain,
index_33 = rselect_tail(q13),
inference(clausify,[status(thm)],[hyp166]) ).
cnf(c_349,plain,
rselect_tail(q13) = index_33,
inference(copy,[status(thm)],[c_348]) ).
fof(hyp167,axiom,
index_36 = s(index_33),
file('theBenchmark.p',hyp167) ).
cnf(c_350,plain,
index_36 = s(index_33),
inference(clausify,[status(thm)],[hyp167]) ).
cnf(c_351,plain,
s(index_33) = index_36,
inference(copy,[status(thm)],[c_350]) ).
fof(hyp168,axiom,
index_39 = rselect_tail(q14),
file('theBenchmark.p',hyp168) ).
cnf(c_352,plain,
index_39 = rselect_tail(q14),
inference(clausify,[status(thm)],[hyp168]) ).
cnf(c_353,plain,
rselect_tail(q14) = index_39,
inference(copy,[status(thm)],[c_352]) ).
fof(hyp169,axiom,
index_42 = s(index_39),
file('theBenchmark.p',hyp169) ).
cnf(c_354,plain,
index_42 = s(index_39),
inference(clausify,[status(thm)],[hyp169]) ).
cnf(c_355,plain,
s(index_39) = index_42,
inference(copy,[status(thm)],[c_354]) ).
fof(hyp170,axiom,
index_45 = rselect_tail(q15),
file('theBenchmark.p',hyp170) ).
cnf(c_356,plain,
index_45 = rselect_tail(q15),
inference(clausify,[status(thm)],[hyp170]) ).
cnf(c_357,plain,
rselect_tail(q15) = index_45,
inference(copy,[status(thm)],[c_356]) ).
fof(hyp171,axiom,
index_48 = s(index_45),
file('theBenchmark.p',hyp171) ).
cnf(c_358,plain,
index_48 = s(index_45),
inference(clausify,[status(thm)],[hyp171]) ).
cnf(c_359,plain,
s(index_45) = index_48,
inference(copy,[status(thm)],[c_358]) ).
fof(hyp172,axiom,
index_51 = rselect_tail(q16),
file('theBenchmark.p',hyp172) ).
cnf(c_360,plain,
index_51 = rselect_tail(q16),
inference(clausify,[status(thm)],[hyp172]) ).
cnf(c_361,plain,
rselect_tail(q16) = index_51,
inference(copy,[status(thm)],[c_360]) ).
fof(hyp173,axiom,
index_54 = s(index_51),
file('theBenchmark.p',hyp173) ).
cnf(c_362,plain,
index_54 = s(index_51),
inference(clausify,[status(thm)],[hyp173]) ).
cnf(c_363,plain,
s(index_51) = index_54,
inference(copy,[status(thm)],[c_362]) ).
fof(hyp174,axiom,
index_57 = rselect_tail(q17),
file('theBenchmark.p',hyp174) ).
cnf(c_364,plain,
index_57 = rselect_tail(q17),
inference(clausify,[status(thm)],[hyp174]) ).
cnf(c_365,plain,
rselect_tail(q17) = index_57,
inference(copy,[status(thm)],[c_364]) ).
fof(hyp175,axiom,
index_6 = s(index_3),
file('theBenchmark.p',hyp175) ).
cnf(c_366,plain,
index_6 = s(index_3),
inference(clausify,[status(thm)],[hyp175]) ).
cnf(c_367,plain,
s(index_3) = index_6,
inference(copy,[status(thm)],[c_366]) ).
fof(hyp176,axiom,
index_60 = s(index_57),
file('theBenchmark.p',hyp176) ).
cnf(c_368,plain,
index_60 = s(index_57),
inference(clausify,[status(thm)],[hyp176]) ).
cnf(c_369,plain,
s(index_57) = index_60,
inference(copy,[status(thm)],[c_368]) ).
fof(hyp177,axiom,
index_63 = rselect_tail(q18),
file('theBenchmark.p',hyp177) ).
cnf(c_370,plain,
index_63 = rselect_tail(q18),
inference(clausify,[status(thm)],[hyp177]) ).
cnf(c_371,plain,
rselect_tail(q18) = index_63,
inference(copy,[status(thm)],[c_370]) ).
fof(hyp178,axiom,
index_66 = s(index_63),
file('theBenchmark.p',hyp178) ).
cnf(c_372,plain,
index_66 = s(index_63),
inference(clausify,[status(thm)],[hyp178]) ).
cnf(c_373,plain,
s(index_63) = index_66,
inference(copy,[status(thm)],[c_372]) ).
fof(hyp179,axiom,
index_69 = rselect_tail(q1),
file('theBenchmark.p',hyp179) ).
cnf(c_374,plain,
index_69 = rselect_tail(q1),
inference(clausify,[status(thm)],[hyp179]) ).
cnf(c_375,plain,
rselect_tail(q1) = index_69,
inference(copy,[status(thm)],[c_374]) ).
fof(hyp180,axiom,
index_72 = s(index_69),
file('theBenchmark.p',hyp180) ).
cnf(c_376,plain,
index_72 = s(index_69),
inference(clausify,[status(thm)],[hyp180]) ).
cnf(c_377,plain,
s(index_69) = index_72,
inference(copy,[status(thm)],[c_376]) ).
fof(hyp181,axiom,
index_75 = rselect_tail(q19),
file('theBenchmark.p',hyp181) ).
cnf(c_378,plain,
index_75 = rselect_tail(q19),
inference(clausify,[status(thm)],[hyp181]) ).
cnf(c_379,plain,
rselect_tail(q19) = index_75,
inference(copy,[status(thm)],[c_378]) ).
fof(hyp182,axiom,
index_78 = s(index_75),
file('theBenchmark.p',hyp182) ).
cnf(c_380,plain,
index_78 = s(index_75),
inference(clausify,[status(thm)],[hyp182]) ).
cnf(c_381,plain,
s(index_75) = index_78,
inference(copy,[status(thm)],[c_380]) ).
fof(hyp183,axiom,
index_81 = rselect_tail(q20),
file('theBenchmark.p',hyp183) ).
cnf(c_382,plain,
index_81 = rselect_tail(q20),
inference(clausify,[status(thm)],[hyp183]) ).
cnf(c_383,plain,
rselect_tail(q20) = index_81,
inference(copy,[status(thm)],[c_382]) ).
fof(hyp184,axiom,
index_84 = s(index_81),
file('theBenchmark.p',hyp184) ).
cnf(c_384,plain,
index_84 = s(index_81),
inference(clausify,[status(thm)],[hyp184]) ).
cnf(c_385,plain,
s(index_81) = index_84,
inference(copy,[status(thm)],[c_384]) ).
fof(hyp185,axiom,
index_87 = rselect_tail(q21),
file('theBenchmark.p',hyp185) ).
cnf(c_386,plain,
index_87 = rselect_tail(q21),
inference(clausify,[status(thm)],[hyp185]) ).
cnf(c_387,plain,
rselect_tail(q21) = index_87,
inference(copy,[status(thm)],[c_386]) ).
fof(hyp186,axiom,
index_9 = rselect_tail(q9),
file('theBenchmark.p',hyp186) ).
cnf(c_388,plain,
index_9 = rselect_tail(q9),
inference(clausify,[status(thm)],[hyp186]) ).
cnf(c_389,plain,
rselect_tail(q9) = index_9,
inference(copy,[status(thm)],[c_388]) ).
fof(hyp187,axiom,
index_90 = s(index_87),
file('theBenchmark.p',hyp187) ).
cnf(c_390,plain,
index_90 = s(index_87),
inference(clausify,[status(thm)],[hyp187]) ).
cnf(c_391,plain,
s(index_87) = index_90,
inference(copy,[status(thm)],[c_390]) ).
fof(hyp188,axiom,
index_93 = rselect_tail(q22),
file('theBenchmark.p',hyp188) ).
cnf(c_392,plain,
index_93 = rselect_tail(q22),
inference(clausify,[status(thm)],[hyp188]) ).
cnf(c_393,plain,
rselect_tail(q22) = index_93,
inference(copy,[status(thm)],[c_392]) ).
fof(hyp189,axiom,
index_96 = s(index_93),
file('theBenchmark.p',hyp189) ).
cnf(c_394,plain,
index_96 = s(index_93),
inference(clausify,[status(thm)],[hyp189]) ).
cnf(c_395,plain,
s(index_93) = index_96,
inference(copy,[status(thm)],[c_394]) ).
fof(hyp190,axiom,
index_99 = rselect_tail(q23),
file('theBenchmark.p',hyp190) ).
cnf(c_396,plain,
index_99 = rselect_tail(q23),
inference(clausify,[status(thm)],[hyp190]) ).
cnf(c_397,plain,
rselect_tail(q23) = index_99,
inference(copy,[status(thm)],[c_396]) ).
fof(hyp191,axiom,
queue_1 = rstore_head(q,index_0),
file('theBenchmark.p',hyp191) ).
cnf(c_398,plain,
queue_1 = rstore_head(q,index_0),
inference(clausify,[status(thm)],[hyp191]) ).
cnf(c_399,plain,
rstore_head(q,index_0) = queue_1,
inference(copy,[status(thm)],[c_398]) ).
fof(hyp192,axiom,
queue_101 = rstore_seq(q23,earray_100),
file('theBenchmark.p',hyp192) ).
cnf(c_400,plain,
queue_101 = rstore_seq(q23,earray_100),
inference(clausify,[status(thm)],[hyp192]) ).
cnf(c_401,plain,
rstore_seq(q23,earray_100) = queue_101,
inference(copy,[status(thm)],[c_400]) ).
fof(hyp193,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file('theBenchmark.p',hyp193) ).
cnf(c_402,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(clausify,[status(thm)],[hyp193]) ).
cnf(c_403,plain,
rstore_tail(queue_101,index_102) = queue_103,
inference(copy,[status(thm)],[c_402]) ).
fof(hyp194,axiom,
queue_107 = rstore_seq(q24,earray_106),
file('theBenchmark.p',hyp194) ).
cnf(c_404,plain,
queue_107 = rstore_seq(q24,earray_106),
inference(clausify,[status(thm)],[hyp194]) ).
cnf(c_405,plain,
rstore_seq(q24,earray_106) = queue_107,
inference(copy,[status(thm)],[c_404]) ).
fof(hyp195,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file('theBenchmark.p',hyp195) ).
cnf(c_406,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(clausify,[status(thm)],[hyp195]) ).
cnf(c_407,plain,
rstore_tail(queue_107,index_108) = queue_109,
inference(copy,[status(thm)],[c_406]) ).
fof(hyp196,axiom,
queue_11 = rstore_seq(q9,earray_10),
file('theBenchmark.p',hyp196) ).
cnf(c_408,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(clausify,[status(thm)],[hyp196]) ).
cnf(c_409,plain,
rstore_seq(q9,earray_10) = queue_11,
inference(copy,[status(thm)],[c_408]) ).
fof(hyp197,axiom,
queue_113 = rstore_seq(q25,earray_112),
file('theBenchmark.p',hyp197) ).
cnf(c_410,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(clausify,[status(thm)],[hyp197]) ).
cnf(c_411,plain,
rstore_seq(q25,earray_112) = queue_113,
inference(copy,[status(thm)],[c_410]) ).
fof(hyp198,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file('theBenchmark.p',hyp198) ).
cnf(c_412,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(clausify,[status(thm)],[hyp198]) ).
cnf(c_413,plain,
rstore_tail(queue_113,index_114) = queue_115,
inference(copy,[status(thm)],[c_412]) ).
fof(hyp199,axiom,
queue_119 = rstore_seq(q26,earray_118),
file('theBenchmark.p',hyp199) ).
cnf(c_414,plain,
queue_119 = rstore_seq(q26,earray_118),
inference(clausify,[status(thm)],[hyp199]) ).
cnf(c_415,plain,
rstore_seq(q26,earray_118) = queue_119,
inference(copy,[status(thm)],[c_414]) ).
fof(hyp200,axiom,
queue_121 = rstore_tail(queue_119,index_120),
file('theBenchmark.p',hyp200) ).
cnf(c_416,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(clausify,[status(thm)],[hyp200]) ).
cnf(c_417,plain,
rstore_tail(queue_119,index_120) = queue_121,
inference(copy,[status(thm)],[c_416]) ).
fof(hyp201,axiom,
queue_125 = rstore_seq(q27,earray_124),
file('theBenchmark.p',hyp201) ).
cnf(c_418,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(clausify,[status(thm)],[hyp201]) ).
cnf(c_419,plain,
rstore_seq(q27,earray_124) = queue_125,
inference(copy,[status(thm)],[c_418]) ).
fof(hyp202,axiom,
queue_127 = rstore_tail(queue_125,index_126),
file('theBenchmark.p',hyp202) ).
cnf(c_420,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(clausify,[status(thm)],[hyp202]) ).
cnf(c_421,plain,
rstore_tail(queue_125,index_126) = queue_127,
inference(copy,[status(thm)],[c_420]) ).
fof(hyp203,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file('theBenchmark.p',hyp203) ).
cnf(c_422,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(clausify,[status(thm)],[hyp203]) ).
cnf(c_423,plain,
rstore_tail(queue_11,index_12) = queue_13,
inference(copy,[status(thm)],[c_422]) ).
fof(hyp204,axiom,
queue_131 = rstore_seq(q28,earray_130),
file('theBenchmark.p',hyp204) ).
cnf(c_424,plain,
queue_131 = rstore_seq(q28,earray_130),
inference(clausify,[status(thm)],[hyp204]) ).
cnf(c_425,plain,
rstore_seq(q28,earray_130) = queue_131,
inference(copy,[status(thm)],[c_424]) ).
fof(hyp205,axiom,
queue_133 = rstore_tail(queue_131,index_132),
file('theBenchmark.p',hyp205) ).
cnf(c_426,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(clausify,[status(thm)],[hyp205]) ).
cnf(c_427,plain,
rstore_tail(queue_131,index_132) = queue_133,
inference(copy,[status(thm)],[c_426]) ).
fof(hyp206,axiom,
queue_137 = rstore_seq(q2,earray_136),
file('theBenchmark.p',hyp206) ).
cnf(c_428,plain,
queue_137 = rstore_seq(q2,earray_136),
inference(clausify,[status(thm)],[hyp206]) ).
cnf(c_429,plain,
rstore_seq(q2,earray_136) = queue_137,
inference(copy,[status(thm)],[c_428]) ).
fof(hyp207,axiom,
queue_139 = rstore_tail(queue_137,index_138),
file('theBenchmark.p',hyp207) ).
cnf(c_430,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(clausify,[status(thm)],[hyp207]) ).
cnf(c_431,plain,
rstore_tail(queue_137,index_138) = queue_139,
inference(copy,[status(thm)],[c_430]) ).
fof(hyp208,axiom,
queue_143 = rstore_seq(q29,earray_142),
file('theBenchmark.p',hyp208) ).
cnf(c_432,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(clausify,[status(thm)],[hyp208]) ).
cnf(c_433,plain,
rstore_seq(q29,earray_142) = queue_143,
inference(copy,[status(thm)],[c_432]) ).
fof(hyp209,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file('theBenchmark.p',hyp209) ).
cnf(c_434,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(clausify,[status(thm)],[hyp209]) ).
cnf(c_435,plain,
rstore_tail(queue_143,index_144) = queue_145,
inference(copy,[status(thm)],[c_434]) ).
fof(hyp210,axiom,
queue_149 = rstore_seq(q30,earray_148),
file('theBenchmark.p',hyp210) ).
cnf(c_436,plain,
queue_149 = rstore_seq(q30,earray_148),
inference(clausify,[status(thm)],[hyp210]) ).
cnf(c_437,plain,
rstore_seq(q30,earray_148) = queue_149,
inference(copy,[status(thm)],[c_436]) ).
fof(hyp211,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file('theBenchmark.p',hyp211) ).
cnf(c_438,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(clausify,[status(thm)],[hyp211]) ).
cnf(c_439,plain,
rstore_tail(queue_149,index_150) = queue_151,
inference(copy,[status(thm)],[c_438]) ).
fof(hyp212,axiom,
queue_155 = rstore_seq(q31,earray_154),
file('theBenchmark.p',hyp212) ).
cnf(c_440,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(clausify,[status(thm)],[hyp212]) ).
cnf(c_441,plain,
rstore_seq(q31,earray_154) = queue_155,
inference(copy,[status(thm)],[c_440]) ).
fof(hyp213,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file('theBenchmark.p',hyp213) ).
cnf(c_442,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(clausify,[status(thm)],[hyp213]) ).
cnf(c_443,plain,
rstore_tail(queue_155,index_156) = queue_157,
inference(copy,[status(thm)],[c_442]) ).
fof(hyp214,axiom,
queue_161 = rstore_seq(q32,earray_160),
file('theBenchmark.p',hyp214) ).
cnf(c_444,plain,
queue_161 = rstore_seq(q32,earray_160),
inference(clausify,[status(thm)],[hyp214]) ).
cnf(c_445,plain,
rstore_seq(q32,earray_160) = queue_161,
inference(copy,[status(thm)],[c_444]) ).
fof(hyp215,axiom,
queue_163 = rstore_tail(queue_161,index_162),
file('theBenchmark.p',hyp215) ).
cnf(c_446,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(clausify,[status(thm)],[hyp215]) ).
cnf(c_447,plain,
rstore_tail(queue_161,index_162) = queue_163,
inference(copy,[status(thm)],[c_446]) ).
fof(hyp216,axiom,
queue_167 = rstore_seq(q33,earray_166),
file('theBenchmark.p',hyp216) ).
cnf(c_448,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(clausify,[status(thm)],[hyp216]) ).
cnf(c_449,plain,
rstore_seq(q33,earray_166) = queue_167,
inference(copy,[status(thm)],[c_448]) ).
fof(hyp217,axiom,
queue_169 = rstore_tail(queue_167,index_168),
file('theBenchmark.p',hyp217) ).
cnf(c_450,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(clausify,[status(thm)],[hyp217]) ).
cnf(c_451,plain,
rstore_tail(queue_167,index_168) = queue_169,
inference(copy,[status(thm)],[c_450]) ).
fof(hyp218,axiom,
queue_17 = rstore_seq(q10,earray_16),
file('theBenchmark.p',hyp218) ).
cnf(c_452,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(clausify,[status(thm)],[hyp218]) ).
cnf(c_453,plain,
rstore_seq(q10,earray_16) = queue_17,
inference(copy,[status(thm)],[c_452]) ).
fof(hyp219,axiom,
queue_173 = rstore_seq(q34,earray_172),
file('theBenchmark.p',hyp219) ).
cnf(c_454,plain,
queue_173 = rstore_seq(q34,earray_172),
inference(clausify,[status(thm)],[hyp219]) ).
cnf(c_455,plain,
rstore_seq(q34,earray_172) = queue_173,
inference(copy,[status(thm)],[c_454]) ).
fof(hyp220,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file('theBenchmark.p',hyp220) ).
cnf(c_456,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(clausify,[status(thm)],[hyp220]) ).
cnf(c_457,plain,
rstore_tail(queue_173,index_174) = queue_175,
inference(copy,[status(thm)],[c_456]) ).
fof(hyp221,axiom,
queue_179 = rstore_seq(q35,earray_178),
file('theBenchmark.p',hyp221) ).
cnf(c_458,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(clausify,[status(thm)],[hyp221]) ).
cnf(c_459,plain,
rstore_seq(q35,earray_178) = queue_179,
inference(copy,[status(thm)],[c_458]) ).
fof(hyp222,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file('theBenchmark.p',hyp222) ).
cnf(c_460,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(clausify,[status(thm)],[hyp222]) ).
cnf(c_461,plain,
rstore_tail(queue_179,index_180) = queue_181,
inference(copy,[status(thm)],[c_460]) ).
fof(hyp223,axiom,
queue_185 = rstore_seq(q36,earray_184),
file('theBenchmark.p',hyp223) ).
cnf(c_462,plain,
queue_185 = rstore_seq(q36,earray_184),
inference(clausify,[status(thm)],[hyp223]) ).
cnf(c_463,plain,
rstore_seq(q36,earray_184) = queue_185,
inference(copy,[status(thm)],[c_462]) ).
fof(hyp224,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file('theBenchmark.p',hyp224) ).
cnf(c_464,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(clausify,[status(thm)],[hyp224]) ).
cnf(c_465,plain,
rstore_tail(queue_185,index_186) = queue_187,
inference(copy,[status(thm)],[c_464]) ).
fof(hyp225,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file('theBenchmark.p',hyp225) ).
cnf(c_466,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(clausify,[status(thm)],[hyp225]) ).
cnf(c_467,plain,
rstore_tail(queue_17,index_18) = queue_19,
inference(copy,[status(thm)],[c_466]) ).
fof(hyp226,axiom,
queue_191 = rstore_seq(q37,earray_190),
file('theBenchmark.p',hyp226) ).
cnf(c_468,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(clausify,[status(thm)],[hyp226]) ).
cnf(c_469,plain,
rstore_seq(q37,earray_190) = queue_191,
inference(copy,[status(thm)],[c_468]) ).
fof(hyp227,axiom,
queue_193 = rstore_tail(queue_191,index_192),
file('theBenchmark.p',hyp227) ).
cnf(c_470,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(clausify,[status(thm)],[hyp227]) ).
cnf(c_471,plain,
rstore_tail(queue_191,index_192) = queue_193,
inference(copy,[status(thm)],[c_470]) ).
fof(hyp228,axiom,
queue_197 = rstore_seq(q38,earray_196),
file('theBenchmark.p',hyp228) ).
cnf(c_472,plain,
queue_197 = rstore_seq(q38,earray_196),
inference(clausify,[status(thm)],[hyp228]) ).
cnf(c_473,plain,
rstore_seq(q38,earray_196) = queue_197,
inference(copy,[status(thm)],[c_472]) ).
fof(hyp229,axiom,
queue_199 = rstore_tail(queue_197,index_198),
file('theBenchmark.p',hyp229) ).
cnf(c_474,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(clausify,[status(thm)],[hyp229]) ).
cnf(c_475,plain,
rstore_tail(queue_197,index_198) = queue_199,
inference(copy,[status(thm)],[c_474]) ).
fof(hyp230,axiom,
queue_203 = rstore_seq(q3,earray_202),
file('theBenchmark.p',hyp230) ).
cnf(c_476,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(clausify,[status(thm)],[hyp230]) ).
cnf(c_477,plain,
rstore_seq(q3,earray_202) = queue_203,
inference(copy,[status(thm)],[c_476]) ).
fof(hyp231,axiom,
queue_205 = rstore_tail(queue_203,index_204),
file('theBenchmark.p',hyp231) ).
cnf(c_478,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(clausify,[status(thm)],[hyp231]) ).
cnf(c_479,plain,
rstore_tail(queue_203,index_204) = queue_205,
inference(copy,[status(thm)],[c_478]) ).
fof(hyp232,axiom,
queue_209 = rstore_seq(q39,earray_208),
file('theBenchmark.p',hyp232) ).
cnf(c_480,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(clausify,[status(thm)],[hyp232]) ).
cnf(c_481,plain,
rstore_seq(q39,earray_208) = queue_209,
inference(copy,[status(thm)],[c_480]) ).
fof(hyp233,axiom,
queue_211 = rstore_tail(queue_209,index_210),
file('theBenchmark.p',hyp233) ).
cnf(c_482,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(clausify,[status(thm)],[hyp233]) ).
cnf(c_483,plain,
rstore_tail(queue_209,index_210) = queue_211,
inference(copy,[status(thm)],[c_482]) ).
fof(hyp234,axiom,
queue_215 = rstore_seq(q40,earray_214),
file('theBenchmark.p',hyp234) ).
cnf(c_484,plain,
queue_215 = rstore_seq(q40,earray_214),
inference(clausify,[status(thm)],[hyp234]) ).
cnf(c_485,plain,
rstore_seq(q40,earray_214) = queue_215,
inference(copy,[status(thm)],[c_484]) ).
fof(hyp235,axiom,
queue_217 = rstore_tail(queue_215,index_216),
file('theBenchmark.p',hyp235) ).
cnf(c_486,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(clausify,[status(thm)],[hyp235]) ).
cnf(c_487,plain,
rstore_tail(queue_215,index_216) = queue_217,
inference(copy,[status(thm)],[c_486]) ).
fof(hyp236,axiom,
queue_221 = rstore_seq(q41,earray_220),
file('theBenchmark.p',hyp236) ).
cnf(c_488,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(clausify,[status(thm)],[hyp236]) ).
cnf(c_489,plain,
rstore_seq(q41,earray_220) = queue_221,
inference(copy,[status(thm)],[c_488]) ).
fof(hyp237,axiom,
queue_223 = rstore_tail(queue_221,index_222),
file('theBenchmark.p',hyp237) ).
cnf(c_490,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(clausify,[status(thm)],[hyp237]) ).
cnf(c_491,plain,
rstore_tail(queue_221,index_222) = queue_223,
inference(copy,[status(thm)],[c_490]) ).
fof(hyp238,axiom,
queue_227 = rstore_seq(q42,earray_226),
file('theBenchmark.p',hyp238) ).
cnf(c_492,plain,
queue_227 = rstore_seq(q42,earray_226),
inference(clausify,[status(thm)],[hyp238]) ).
cnf(c_493,plain,
rstore_seq(q42,earray_226) = queue_227,
inference(copy,[status(thm)],[c_492]) ).
fof(hyp239,axiom,
queue_229 = rstore_tail(queue_227,index_228),
file('theBenchmark.p',hyp239) ).
cnf(c_494,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(clausify,[status(thm)],[hyp239]) ).
cnf(c_495,plain,
rstore_tail(queue_227,index_228) = queue_229,
inference(copy,[status(thm)],[c_494]) ).
fof(hyp240,axiom,
queue_23 = rstore_seq(q11,earray_22),
file('theBenchmark.p',hyp240) ).
cnf(c_496,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(clausify,[status(thm)],[hyp240]) ).
cnf(c_497,plain,
rstore_seq(q11,earray_22) = queue_23,
inference(copy,[status(thm)],[c_496]) ).
fof(hyp241,axiom,
queue_233 = rstore_seq(q43,earray_232),
file('theBenchmark.p',hyp241) ).
cnf(c_498,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(clausify,[status(thm)],[hyp241]) ).
cnf(c_499,plain,
rstore_seq(q43,earray_232) = queue_233,
inference(copy,[status(thm)],[c_498]) ).
fof(hyp242,axiom,
queue_235 = rstore_tail(queue_233,index_234),
file('theBenchmark.p',hyp242) ).
cnf(c_500,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(clausify,[status(thm)],[hyp242]) ).
cnf(c_501,plain,
rstore_tail(queue_233,index_234) = queue_235,
inference(copy,[status(thm)],[c_500]) ).
fof(hyp243,axiom,
queue_239 = rstore_seq(q44,earray_238),
file('theBenchmark.p',hyp243) ).
cnf(c_502,plain,
queue_239 = rstore_seq(q44,earray_238),
inference(clausify,[status(thm)],[hyp243]) ).
cnf(c_503,plain,
rstore_seq(q44,earray_238) = queue_239,
inference(copy,[status(thm)],[c_502]) ).
fof(hyp244,axiom,
queue_241 = rstore_tail(queue_239,index_240),
file('theBenchmark.p',hyp244) ).
cnf(c_504,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(clausify,[status(thm)],[hyp244]) ).
cnf(c_505,plain,
rstore_tail(queue_239,index_240) = queue_241,
inference(copy,[status(thm)],[c_504]) ).
fof(hyp245,axiom,
queue_245 = rstore_seq(q45,earray_244),
file('theBenchmark.p',hyp245) ).
cnf(c_506,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(clausify,[status(thm)],[hyp245]) ).
cnf(c_507,plain,
rstore_seq(q45,earray_244) = queue_245,
inference(copy,[status(thm)],[c_506]) ).
fof(hyp246,axiom,
queue_247 = rstore_tail(queue_245,index_246),
file('theBenchmark.p',hyp246) ).
cnf(c_508,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(clausify,[status(thm)],[hyp246]) ).
cnf(c_509,plain,
rstore_tail(queue_245,index_246) = queue_247,
inference(copy,[status(thm)],[c_508]) ).
fof(hyp247,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file('theBenchmark.p',hyp247) ).
cnf(c_510,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(clausify,[status(thm)],[hyp247]) ).
cnf(c_511,plain,
rstore_tail(queue_23,index_24) = queue_25,
inference(copy,[status(thm)],[c_510]) ).
fof(hyp248,axiom,
queue_251 = rstore_seq(q4,earray_250),
file('theBenchmark.p',hyp248) ).
cnf(c_512,plain,
queue_251 = rstore_seq(q4,earray_250),
inference(clausify,[status(thm)],[hyp248]) ).
cnf(c_513,plain,
rstore_seq(q4,earray_250) = queue_251,
inference(copy,[status(thm)],[c_512]) ).
fof(hyp249,axiom,
queue_253 = rstore_tail(queue_251,index_252),
file('theBenchmark.p',hyp249) ).
cnf(c_514,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(clausify,[status(thm)],[hyp249]) ).
cnf(c_515,plain,
rstore_tail(queue_251,index_252) = queue_253,
inference(copy,[status(thm)],[c_514]) ).
fof(hyp250,axiom,
queue_257 = rstore_seq(q5,earray_256),
file('theBenchmark.p',hyp250) ).
cnf(c_516,plain,
queue_257 = rstore_seq(q5,earray_256),
inference(clausify,[status(thm)],[hyp250]) ).
cnf(c_517,plain,
rstore_seq(q5,earray_256) = queue_257,
inference(copy,[status(thm)],[c_516]) ).
fof(hyp251,axiom,
queue_259 = rstore_tail(queue_257,index_258),
file('theBenchmark.p',hyp251) ).
cnf(c_518,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(clausify,[status(thm)],[hyp251]) ).
cnf(c_519,plain,
rstore_tail(queue_257,index_258) = queue_259,
inference(copy,[status(thm)],[c_518]) ).
fof(hyp252,axiom,
queue_263 = rstore_seq(q6,earray_262),
file('theBenchmark.p',hyp252) ).
cnf(c_520,plain,
queue_263 = rstore_seq(q6,earray_262),
inference(clausify,[status(thm)],[hyp252]) ).
cnf(c_521,plain,
rstore_seq(q6,earray_262) = queue_263,
inference(copy,[status(thm)],[c_520]) ).
fof(hyp253,axiom,
queue_265 = rstore_tail(queue_263,index_264),
file('theBenchmark.p',hyp253) ).
cnf(c_522,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(clausify,[status(thm)],[hyp253]) ).
cnf(c_523,plain,
rstore_tail(queue_263,index_264) = queue_265,
inference(copy,[status(thm)],[c_522]) ).
fof(hyp254,axiom,
queue_269 = rstore_seq(q7,earray_268),
file('theBenchmark.p',hyp254) ).
cnf(c_524,plain,
queue_269 = rstore_seq(q7,earray_268),
inference(clausify,[status(thm)],[hyp254]) ).
cnf(c_525,plain,
rstore_seq(q7,earray_268) = queue_269,
inference(copy,[status(thm)],[c_524]) ).
fof(hyp255,axiom,
queue_271 = rstore_tail(queue_269,index_270),
file('theBenchmark.p',hyp255) ).
cnf(c_526,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(clausify,[status(thm)],[hyp255]) ).
cnf(c_527,plain,
rstore_tail(queue_269,index_270) = queue_271,
inference(copy,[status(thm)],[c_526]) ).
fof(hyp256,axiom,
queue_275 = rstore_seq(q8,earray_274),
file('theBenchmark.p',hyp256) ).
cnf(c_528,plain,
queue_275 = rstore_seq(q8,earray_274),
inference(clausify,[status(thm)],[hyp256]) ).
cnf(c_529,plain,
rstore_seq(q8,earray_274) = queue_275,
inference(copy,[status(thm)],[c_528]) ).
fof(hyp257,axiom,
queue_277 = rstore_tail(queue_275,index_276),
file('theBenchmark.p',hyp257) ).
cnf(c_530,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(clausify,[status(thm)],[hyp257]) ).
cnf(c_531,plain,
rstore_tail(queue_275,index_276) = queue_277,
inference(copy,[status(thm)],[c_530]) ).
fof(hyp258,axiom,
queue_29 = rstore_seq(q12,earray_28),
file('theBenchmark.p',hyp258) ).
cnf(c_532,plain,
queue_29 = rstore_seq(q12,earray_28),
inference(clausify,[status(thm)],[hyp258]) ).
cnf(c_533,plain,
rstore_seq(q12,earray_28) = queue_29,
inference(copy,[status(thm)],[c_532]) ).
fof(hyp259,axiom,
queue_31 = rstore_tail(queue_29,index_30),
file('theBenchmark.p',hyp259) ).
cnf(c_534,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(clausify,[status(thm)],[hyp259]) ).
cnf(c_535,plain,
rstore_tail(queue_29,index_30) = queue_31,
inference(copy,[status(thm)],[c_534]) ).
fof(hyp260,axiom,
queue_35 = rstore_seq(q13,earray_34),
file('theBenchmark.p',hyp260) ).
cnf(c_536,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(clausify,[status(thm)],[hyp260]) ).
cnf(c_537,plain,
rstore_seq(q13,earray_34) = queue_35,
inference(copy,[status(thm)],[c_536]) ).
fof(hyp261,axiom,
queue_37 = rstore_tail(queue_35,index_36),
file('theBenchmark.p',hyp261) ).
cnf(c_538,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(clausify,[status(thm)],[hyp261]) ).
cnf(c_539,plain,
rstore_tail(queue_35,index_36) = queue_37,
inference(copy,[status(thm)],[c_538]) ).
fof(hyp262,axiom,
queue_41 = rstore_seq(q14,earray_40),
file('theBenchmark.p',hyp262) ).
cnf(c_540,plain,
queue_41 = rstore_seq(q14,earray_40),
inference(clausify,[status(thm)],[hyp262]) ).
cnf(c_541,plain,
rstore_seq(q14,earray_40) = queue_41,
inference(copy,[status(thm)],[c_540]) ).
fof(hyp263,axiom,
queue_43 = rstore_tail(queue_41,index_42),
file('theBenchmark.p',hyp263) ).
cnf(c_542,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(clausify,[status(thm)],[hyp263]) ).
cnf(c_543,plain,
rstore_tail(queue_41,index_42) = queue_43,
inference(copy,[status(thm)],[c_542]) ).
fof(hyp264,axiom,
queue_47 = rstore_seq(q15,earray_46),
file('theBenchmark.p',hyp264) ).
cnf(c_544,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(clausify,[status(thm)],[hyp264]) ).
cnf(c_545,plain,
rstore_seq(q15,earray_46) = queue_47,
inference(copy,[status(thm)],[c_544]) ).
fof(hyp265,axiom,
queue_49 = rstore_tail(queue_47,index_48),
file('theBenchmark.p',hyp265) ).
cnf(c_546,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(clausify,[status(thm)],[hyp265]) ).
cnf(c_547,plain,
rstore_tail(queue_47,index_48) = queue_49,
inference(copy,[status(thm)],[c_546]) ).
fof(hyp266,axiom,
queue_5 = rstore_seq(q0,earray_4),
file('theBenchmark.p',hyp266) ).
cnf(c_548,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(clausify,[status(thm)],[hyp266]) ).
cnf(c_549,plain,
rstore_seq(q0,earray_4) = queue_5,
inference(copy,[status(thm)],[c_548]) ).
fof(hyp267,axiom,
queue_53 = rstore_seq(q16,earray_52),
file('theBenchmark.p',hyp267) ).
cnf(c_550,plain,
queue_53 = rstore_seq(q16,earray_52),
inference(clausify,[status(thm)],[hyp267]) ).
cnf(c_551,plain,
rstore_seq(q16,earray_52) = queue_53,
inference(copy,[status(thm)],[c_550]) ).
fof(hyp268,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file('theBenchmark.p',hyp268) ).
cnf(c_552,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(clausify,[status(thm)],[hyp268]) ).
cnf(c_553,plain,
rstore_tail(queue_53,index_54) = queue_55,
inference(copy,[status(thm)],[c_552]) ).
fof(hyp269,axiom,
queue_59 = rstore_seq(q17,earray_58),
file('theBenchmark.p',hyp269) ).
cnf(c_554,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(clausify,[status(thm)],[hyp269]) ).
cnf(c_555,plain,
rstore_seq(q17,earray_58) = queue_59,
inference(copy,[status(thm)],[c_554]) ).
fof(hyp270,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file('theBenchmark.p',hyp270) ).
cnf(c_556,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(clausify,[status(thm)],[hyp270]) ).
cnf(c_557,plain,
rstore_tail(queue_59,index_60) = queue_61,
inference(copy,[status(thm)],[c_556]) ).
fof(hyp271,axiom,
queue_65 = rstore_seq(q18,earray_64),
file('theBenchmark.p',hyp271) ).
cnf(c_558,plain,
queue_65 = rstore_seq(q18,earray_64),
inference(clausify,[status(thm)],[hyp271]) ).
cnf(c_559,plain,
rstore_seq(q18,earray_64) = queue_65,
inference(copy,[status(thm)],[c_558]) ).
fof(hyp272,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file('theBenchmark.p',hyp272) ).
cnf(c_560,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(clausify,[status(thm)],[hyp272]) ).
cnf(c_561,plain,
rstore_tail(queue_65,index_66) = queue_67,
inference(copy,[status(thm)],[c_560]) ).
fof(hyp273,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file('theBenchmark.p',hyp273) ).
cnf(c_562,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(clausify,[status(thm)],[hyp273]) ).
cnf(c_563,plain,
rstore_tail(queue_5,index_6) = queue_7,
inference(copy,[status(thm)],[c_562]) ).
fof(hyp274,axiom,
queue_71 = rstore_seq(q1,earray_70),
file('theBenchmark.p',hyp274) ).
cnf(c_564,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(clausify,[status(thm)],[hyp274]) ).
cnf(c_565,plain,
rstore_seq(q1,earray_70) = queue_71,
inference(copy,[status(thm)],[c_564]) ).
fof(hyp275,axiom,
queue_73 = rstore_tail(queue_71,index_72),
file('theBenchmark.p',hyp275) ).
cnf(c_566,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(clausify,[status(thm)],[hyp275]) ).
cnf(c_567,plain,
rstore_tail(queue_71,index_72) = queue_73,
inference(copy,[status(thm)],[c_566]) ).
fof(hyp276,axiom,
queue_77 = rstore_seq(q19,earray_76),
file('theBenchmark.p',hyp276) ).
cnf(c_568,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(clausify,[status(thm)],[hyp276]) ).
cnf(c_569,plain,
rstore_seq(q19,earray_76) = queue_77,
inference(copy,[status(thm)],[c_568]) ).
fof(hyp277,axiom,
queue_79 = rstore_tail(queue_77,index_78),
file('theBenchmark.p',hyp277) ).
cnf(c_570,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(clausify,[status(thm)],[hyp277]) ).
cnf(c_571,plain,
rstore_tail(queue_77,index_78) = queue_79,
inference(copy,[status(thm)],[c_570]) ).
fof(hyp278,axiom,
queue_83 = rstore_seq(q20,earray_82),
file('theBenchmark.p',hyp278) ).
cnf(c_572,plain,
queue_83 = rstore_seq(q20,earray_82),
inference(clausify,[status(thm)],[hyp278]) ).
cnf(c_573,plain,
rstore_seq(q20,earray_82) = queue_83,
inference(copy,[status(thm)],[c_572]) ).
fof(hyp279,axiom,
queue_85 = rstore_tail(queue_83,index_84),
file('theBenchmark.p',hyp279) ).
cnf(c_574,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(clausify,[status(thm)],[hyp279]) ).
cnf(c_575,plain,
rstore_tail(queue_83,index_84) = queue_85,
inference(copy,[status(thm)],[c_574]) ).
fof(hyp280,axiom,
queue_89 = rstore_seq(q21,earray_88),
file('theBenchmark.p',hyp280) ).
cnf(c_576,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(clausify,[status(thm)],[hyp280]) ).
cnf(c_577,plain,
rstore_seq(q21,earray_88) = queue_89,
inference(copy,[status(thm)],[c_576]) ).
fof(hyp281,axiom,
queue_91 = rstore_tail(queue_89,index_90),
file('theBenchmark.p',hyp281) ).
cnf(c_578,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(clausify,[status(thm)],[hyp281]) ).
cnf(c_579,plain,
rstore_tail(queue_89,index_90) = queue_91,
inference(copy,[status(thm)],[c_578]) ).
fof(hyp282,axiom,
queue_95 = rstore_seq(q22,earray_94),
file('theBenchmark.p',hyp282) ).
cnf(c_580,plain,
queue_95 = rstore_seq(q22,earray_94),
inference(clausify,[status(thm)],[hyp282]) ).
cnf(c_581,plain,
rstore_seq(q22,earray_94) = queue_95,
inference(copy,[status(thm)],[c_580]) ).
fof(hyp283,axiom,
queue_97 = rstore_tail(queue_95,index_96),
file('theBenchmark.p',hyp283) ).
cnf(c_582,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(clausify,[status(thm)],[hyp283]) ).
cnf(c_583,plain,
rstore_tail(queue_95,index_96) = queue_97,
inference(copy,[status(thm)],[c_582]) ).
fof(hyp284,axiom,
q0 = queue_1,
file('theBenchmark.p',hyp284) ).
cnf(c_584,plain,
q0 = queue_1,
inference(clausify,[status(thm)],[hyp284]) ).
cnf(c_585,plain,
queue_1 = q0,
inference(copy,[status(thm)],[c_584]) ).
fof(hyp285,axiom,
q1 = queue_7,
file('theBenchmark.p',hyp285) ).
cnf(c_586,plain,
q1 = queue_7,
inference(clausify,[status(thm)],[hyp285]) ).
cnf(c_587,plain,
queue_7 = q1,
inference(copy,[status(thm)],[c_586]) ).
fof(hyp286,axiom,
q10 = queue_13,
file('theBenchmark.p',hyp286) ).
cnf(c_588,plain,
q10 = queue_13,
inference(clausify,[status(thm)],[hyp286]) ).
cnf(c_589,plain,
queue_13 = q10,
inference(copy,[status(thm)],[c_588]) ).
fof(hyp287,axiom,
q11 = queue_19,
file('theBenchmark.p',hyp287) ).
cnf(c_590,plain,
q11 = queue_19,
inference(clausify,[status(thm)],[hyp287]) ).
cnf(c_591,plain,
queue_19 = q11,
inference(copy,[status(thm)],[c_590]) ).
fof(hyp288,axiom,
q12 = queue_25,
file('theBenchmark.p',hyp288) ).
cnf(c_592,plain,
q12 = queue_25,
inference(clausify,[status(thm)],[hyp288]) ).
cnf(c_593,plain,
queue_25 = q12,
inference(copy,[status(thm)],[c_592]) ).
fof(hyp289,axiom,
q13 = queue_31,
file('theBenchmark.p',hyp289) ).
cnf(c_594,plain,
q13 = queue_31,
inference(clausify,[status(thm)],[hyp289]) ).
cnf(c_595,plain,
queue_31 = q13,
inference(copy,[status(thm)],[c_594]) ).
fof(hyp290,axiom,
q14 = queue_37,
file('theBenchmark.p',hyp290) ).
cnf(c_596,plain,
q14 = queue_37,
inference(clausify,[status(thm)],[hyp290]) ).
cnf(c_597,plain,
queue_37 = q14,
inference(copy,[status(thm)],[c_596]) ).
fof(hyp291,axiom,
q15 = queue_43,
file('theBenchmark.p',hyp291) ).
cnf(c_598,plain,
q15 = queue_43,
inference(clausify,[status(thm)],[hyp291]) ).
cnf(c_599,plain,
queue_43 = q15,
inference(copy,[status(thm)],[c_598]) ).
fof(hyp292,axiom,
q16 = queue_49,
file('theBenchmark.p',hyp292) ).
cnf(c_600,plain,
q16 = queue_49,
inference(clausify,[status(thm)],[hyp292]) ).
cnf(c_601,plain,
queue_49 = q16,
inference(copy,[status(thm)],[c_600]) ).
fof(hyp293,axiom,
q17 = queue_55,
file('theBenchmark.p',hyp293) ).
cnf(c_602,plain,
q17 = queue_55,
inference(clausify,[status(thm)],[hyp293]) ).
cnf(c_603,plain,
queue_55 = q17,
inference(copy,[status(thm)],[c_602]) ).
fof(hyp294,axiom,
q18 = queue_61,
file('theBenchmark.p',hyp294) ).
cnf(c_604,plain,
q18 = queue_61,
inference(clausify,[status(thm)],[hyp294]) ).
cnf(c_605,plain,
queue_61 = q18,
inference(copy,[status(thm)],[c_604]) ).
fof(hyp295,axiom,
q19 = queue_67,
file('theBenchmark.p',hyp295) ).
cnf(c_606,plain,
q19 = queue_67,
inference(clausify,[status(thm)],[hyp295]) ).
cnf(c_607,plain,
queue_67 = q19,
inference(copy,[status(thm)],[c_606]) ).
fof(hyp296,axiom,
q2 = queue_73,
file('theBenchmark.p',hyp296) ).
cnf(c_608,plain,
q2 = queue_73,
inference(clausify,[status(thm)],[hyp296]) ).
cnf(c_609,plain,
queue_73 = q2,
inference(copy,[status(thm)],[c_608]) ).
fof(hyp297,axiom,
q20 = queue_79,
file('theBenchmark.p',hyp297) ).
cnf(c_610,plain,
q20 = queue_79,
inference(clausify,[status(thm)],[hyp297]) ).
cnf(c_611,plain,
queue_79 = q20,
inference(copy,[status(thm)],[c_610]) ).
fof(hyp298,axiom,
q21 = queue_85,
file('theBenchmark.p',hyp298) ).
cnf(c_612,plain,
q21 = queue_85,
inference(clausify,[status(thm)],[hyp298]) ).
cnf(c_613,plain,
queue_85 = q21,
inference(copy,[status(thm)],[c_612]) ).
fof(hyp299,axiom,
q22 = queue_91,
file('theBenchmark.p',hyp299) ).
cnf(c_614,plain,
q22 = queue_91,
inference(clausify,[status(thm)],[hyp299]) ).
cnf(c_615,plain,
queue_91 = q22,
inference(copy,[status(thm)],[c_614]) ).
fof(hyp300,axiom,
q23 = queue_97,
file('theBenchmark.p',hyp300) ).
cnf(c_616,plain,
q23 = queue_97,
inference(clausify,[status(thm)],[hyp300]) ).
cnf(c_617,plain,
queue_97 = q23,
inference(copy,[status(thm)],[c_616]) ).
fof(hyp301,axiom,
q24 = queue_103,
file('theBenchmark.p',hyp301) ).
cnf(c_618,plain,
q24 = queue_103,
inference(clausify,[status(thm)],[hyp301]) ).
cnf(c_619,plain,
queue_103 = q24,
inference(copy,[status(thm)],[c_618]) ).
fof(hyp302,axiom,
q25 = queue_109,
file('theBenchmark.p',hyp302) ).
cnf(c_620,plain,
q25 = queue_109,
inference(clausify,[status(thm)],[hyp302]) ).
cnf(c_621,plain,
queue_109 = q25,
inference(copy,[status(thm)],[c_620]) ).
fof(hyp303,axiom,
q26 = queue_115,
file('theBenchmark.p',hyp303) ).
cnf(c_622,plain,
q26 = queue_115,
inference(clausify,[status(thm)],[hyp303]) ).
cnf(c_623,plain,
queue_115 = q26,
inference(copy,[status(thm)],[c_622]) ).
fof(hyp304,axiom,
q27 = queue_121,
file('theBenchmark.p',hyp304) ).
cnf(c_624,plain,
q27 = queue_121,
inference(clausify,[status(thm)],[hyp304]) ).
cnf(c_625,plain,
queue_121 = q27,
inference(copy,[status(thm)],[c_624]) ).
fof(hyp305,axiom,
q28 = queue_127,
file('theBenchmark.p',hyp305) ).
cnf(c_626,plain,
q28 = queue_127,
inference(clausify,[status(thm)],[hyp305]) ).
cnf(c_627,plain,
queue_127 = q28,
inference(copy,[status(thm)],[c_626]) ).
fof(hyp306,axiom,
q29 = queue_133,
file('theBenchmark.p',hyp306) ).
cnf(c_628,plain,
q29 = queue_133,
inference(clausify,[status(thm)],[hyp306]) ).
cnf(c_629,plain,
queue_133 = q29,
inference(copy,[status(thm)],[c_628]) ).
fof(hyp307,axiom,
q3 = queue_139,
file('theBenchmark.p',hyp307) ).
cnf(c_630,plain,
q3 = queue_139,
inference(clausify,[status(thm)],[hyp307]) ).
cnf(c_631,plain,
queue_139 = q3,
inference(copy,[status(thm)],[c_630]) ).
fof(hyp308,axiom,
q30 = queue_145,
file('theBenchmark.p',hyp308) ).
cnf(c_632,plain,
q30 = queue_145,
inference(clausify,[status(thm)],[hyp308]) ).
cnf(c_633,plain,
queue_145 = q30,
inference(copy,[status(thm)],[c_632]) ).
fof(hyp309,axiom,
q31 = queue_151,
file('theBenchmark.p',hyp309) ).
cnf(c_634,plain,
q31 = queue_151,
inference(clausify,[status(thm)],[hyp309]) ).
cnf(c_635,plain,
queue_151 = q31,
inference(copy,[status(thm)],[c_634]) ).
fof(hyp310,axiom,
q32 = queue_157,
file('theBenchmark.p',hyp310) ).
cnf(c_636,plain,
q32 = queue_157,
inference(clausify,[status(thm)],[hyp310]) ).
cnf(c_637,plain,
queue_157 = q32,
inference(copy,[status(thm)],[c_636]) ).
fof(hyp311,axiom,
q33 = queue_163,
file('theBenchmark.p',hyp311) ).
cnf(c_638,plain,
q33 = queue_163,
inference(clausify,[status(thm)],[hyp311]) ).
cnf(c_639,plain,
queue_163 = q33,
inference(copy,[status(thm)],[c_638]) ).
fof(hyp312,axiom,
q34 = queue_169,
file('theBenchmark.p',hyp312) ).
cnf(c_640,plain,
q34 = queue_169,
inference(clausify,[status(thm)],[hyp312]) ).
cnf(c_641,plain,
queue_169 = q34,
inference(copy,[status(thm)],[c_640]) ).
fof(hyp313,axiom,
q35 = queue_175,
file('theBenchmark.p',hyp313) ).
cnf(c_642,plain,
q35 = queue_175,
inference(clausify,[status(thm)],[hyp313]) ).
cnf(c_643,plain,
queue_175 = q35,
inference(copy,[status(thm)],[c_642]) ).
fof(hyp314,axiom,
q36 = queue_181,
file('theBenchmark.p',hyp314) ).
cnf(c_644,plain,
q36 = queue_181,
inference(clausify,[status(thm)],[hyp314]) ).
cnf(c_645,plain,
queue_181 = q36,
inference(copy,[status(thm)],[c_644]) ).
fof(hyp315,axiom,
q37 = queue_187,
file('theBenchmark.p',hyp315) ).
cnf(c_646,plain,
q37 = queue_187,
inference(clausify,[status(thm)],[hyp315]) ).
cnf(c_647,plain,
queue_187 = q37,
inference(copy,[status(thm)],[c_646]) ).
fof(hyp316,axiom,
q38 = queue_193,
file('theBenchmark.p',hyp316) ).
cnf(c_648,plain,
q38 = queue_193,
inference(clausify,[status(thm)],[hyp316]) ).
cnf(c_649,plain,
queue_193 = q38,
inference(copy,[status(thm)],[c_648]) ).
fof(hyp317,axiom,
q39 = queue_199,
file('theBenchmark.p',hyp317) ).
cnf(c_650,plain,
q39 = queue_199,
inference(clausify,[status(thm)],[hyp317]) ).
cnf(c_651,plain,
queue_199 = q39,
inference(copy,[status(thm)],[c_650]) ).
fof(hyp318,axiom,
q4 = queue_205,
file('theBenchmark.p',hyp318) ).
cnf(c_652,plain,
q4 = queue_205,
inference(clausify,[status(thm)],[hyp318]) ).
cnf(c_653,plain,
queue_205 = q4,
inference(copy,[status(thm)],[c_652]) ).
fof(hyp319,axiom,
q40 = queue_211,
file('theBenchmark.p',hyp319) ).
cnf(c_654,plain,
q40 = queue_211,
inference(clausify,[status(thm)],[hyp319]) ).
cnf(c_655,plain,
queue_211 = q40,
inference(copy,[status(thm)],[c_654]) ).
fof(hyp320,axiom,
q41 = queue_217,
file('theBenchmark.p',hyp320) ).
cnf(c_656,plain,
q41 = queue_217,
inference(clausify,[status(thm)],[hyp320]) ).
cnf(c_657,plain,
queue_217 = q41,
inference(copy,[status(thm)],[c_656]) ).
fof(hyp321,axiom,
q42 = queue_223,
file('theBenchmark.p',hyp321) ).
cnf(c_658,plain,
q42 = queue_223,
inference(clausify,[status(thm)],[hyp321]) ).
cnf(c_659,plain,
queue_223 = q42,
inference(copy,[status(thm)],[c_658]) ).
fof(hyp322,axiom,
q43 = queue_229,
file('theBenchmark.p',hyp322) ).
cnf(c_660,plain,
q43 = queue_229,
inference(clausify,[status(thm)],[hyp322]) ).
cnf(c_661,plain,
queue_229 = q43,
inference(copy,[status(thm)],[c_660]) ).
fof(hyp323,axiom,
q44 = queue_235,
file('theBenchmark.p',hyp323) ).
cnf(c_662,plain,
q44 = queue_235,
inference(clausify,[status(thm)],[hyp323]) ).
cnf(c_663,plain,
queue_235 = q44,
inference(copy,[status(thm)],[c_662]) ).
fof(hyp324,axiom,
q45 = queue_241,
file('theBenchmark.p',hyp324) ).
cnf(c_664,plain,
q45 = queue_241,
inference(clausify,[status(thm)],[hyp324]) ).
cnf(c_665,plain,
queue_241 = q45,
inference(copy,[status(thm)],[c_664]) ).
fof(hyp325,axiom,
q46 = queue_247,
file('theBenchmark.p',hyp325) ).
cnf(c_666,plain,
q46 = queue_247,
inference(clausify,[status(thm)],[hyp325]) ).
cnf(c_667,plain,
queue_247 = q46,
inference(copy,[status(thm)],[c_666]) ).
fof(hyp326,axiom,
q5 = queue_253,
file('theBenchmark.p',hyp326) ).
cnf(c_668,plain,
q5 = queue_253,
inference(clausify,[status(thm)],[hyp326]) ).
cnf(c_669,plain,
queue_253 = q5,
inference(copy,[status(thm)],[c_668]) ).
fof(hyp327,axiom,
q6 = queue_259,
file('theBenchmark.p',hyp327) ).
cnf(c_670,plain,
q6 = queue_259,
inference(clausify,[status(thm)],[hyp327]) ).
cnf(c_671,plain,
queue_259 = q6,
inference(copy,[status(thm)],[c_670]) ).
fof(hyp328,axiom,
q7 = queue_265,
file('theBenchmark.p',hyp328) ).
cnf(c_672,plain,
q7 = queue_265,
inference(clausify,[status(thm)],[hyp328]) ).
cnf(c_673,plain,
queue_265 = q7,
inference(copy,[status(thm)],[c_672]) ).
fof(hyp329,axiom,
q8 = queue_271,
file('theBenchmark.p',hyp329) ).
cnf(c_674,plain,
q8 = queue_271,
inference(clausify,[status(thm)],[hyp329]) ).
cnf(c_675,plain,
queue_271 = q8,
inference(copy,[status(thm)],[c_674]) ).
fof(hyp330,axiom,
q9 = queue_277,
file('theBenchmark.p',hyp330) ).
cnf(c_676,plain,
q9 = queue_277,
inference(clausify,[status(thm)],[hyp330]) ).
cnf(c_677,plain,
queue_277 = q9,
inference(copy,[status(thm)],[c_676]) ).
fof(goal,axiom,
elem_280 != elem_283,
file('theBenchmark.p',goal) ).
cnf(c_678,plain,
elem_280 != elem_283,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_679,plain,
elem_283 != elem_280,
inference(copy,[status(thm)],[c_678]) ).
cnf(c_680,plain,
rstore_head(q,index_0) = q0,
inference(paramod,[status(thm)],[c_585,c_399]) ).
cnf(c_681,plain,
rstore_tail(queue_5,index_6) = q1,
inference(paramod,[status(thm)],[c_587,c_563]) ).
cnf(c_682,plain,
rstore_tail(queue_11,index_12) = q10,
inference(paramod,[status(thm)],[c_589,c_423]) ).
cnf(c_683,plain,
rstore_tail(queue_17,index_18) = q11,
inference(paramod,[status(thm)],[c_591,c_467]) ).
cnf(c_684,plain,
rstore_tail(queue_23,index_24) = q12,
inference(paramod,[status(thm)],[c_593,c_511]) ).
cnf(c_685,plain,
rstore_tail(queue_29,index_30) = q13,
inference(paramod,[status(thm)],[c_595,c_535]) ).
cnf(c_686,plain,
rstore_tail(queue_35,index_36) = q14,
inference(paramod,[status(thm)],[c_597,c_539]) ).
cnf(c_687,plain,
rstore_tail(queue_41,index_42) = q15,
inference(paramod,[status(thm)],[c_599,c_543]) ).
cnf(c_688,plain,
rstore_tail(queue_47,index_48) = q16,
inference(paramod,[status(thm)],[c_601,c_547]) ).
cnf(c_689,plain,
rstore_tail(queue_53,index_54) = q17,
inference(paramod,[status(thm)],[c_603,c_553]) ).
cnf(c_690,plain,
rstore_tail(queue_59,index_60) = q18,
inference(paramod,[status(thm)],[c_605,c_557]) ).
cnf(c_691,plain,
rstore_tail(queue_65,index_66) = q19,
inference(paramod,[status(thm)],[c_607,c_561]) ).
cnf(c_692,plain,
rstore_tail(queue_71,index_72) = q2,
inference(paramod,[status(thm)],[c_609,c_567]) ).
cnf(c_693,plain,
rstore_tail(queue_77,index_78) = q20,
inference(paramod,[status(thm)],[c_611,c_571]) ).
cnf(c_694,plain,
rstore_tail(queue_83,index_84) = q21,
inference(paramod,[status(thm)],[c_613,c_575]) ).
cnf(c_695,plain,
rstore_tail(queue_89,index_90) = q22,
inference(paramod,[status(thm)],[c_615,c_579]) ).
cnf(c_696,plain,
rstore_tail(queue_95,index_96) = q23,
inference(paramod,[status(thm)],[c_617,c_583]) ).
cnf(c_697,plain,
rstore_tail(queue_101,index_102) = q24,
inference(paramod,[status(thm)],[c_619,c_403]) ).
cnf(c_698,plain,
rstore_tail(queue_107,index_108) = q25,
inference(paramod,[status(thm)],[c_621,c_407]) ).
cnf(c_699,plain,
rstore_tail(queue_113,index_114) = q26,
inference(paramod,[status(thm)],[c_623,c_413]) ).
cnf(c_700,plain,
rstore_tail(queue_119,index_120) = q27,
inference(paramod,[status(thm)],[c_625,c_417]) ).
cnf(c_701,plain,
rstore_tail(queue_125,index_126) = q28,
inference(paramod,[status(thm)],[c_627,c_421]) ).
cnf(c_702,plain,
rstore_tail(queue_131,index_132) = q29,
inference(paramod,[status(thm)],[c_629,c_427]) ).
cnf(c_703,plain,
rstore_tail(queue_137,index_138) = q3,
inference(paramod,[status(thm)],[c_631,c_431]) ).
cnf(c_704,plain,
rstore_tail(queue_143,index_144) = q30,
inference(paramod,[status(thm)],[c_633,c_435]) ).
cnf(c_705,plain,
rstore_tail(queue_149,index_150) = q31,
inference(paramod,[status(thm)],[c_635,c_439]) ).
cnf(c_706,plain,
rstore_tail(queue_155,index_156) = q32,
inference(paramod,[status(thm)],[c_637,c_443]) ).
cnf(c_707,plain,
rstore_tail(queue_161,index_162) = q33,
inference(paramod,[status(thm)],[c_639,c_447]) ).
cnf(c_708,plain,
rstore_tail(queue_167,index_168) = q34,
inference(paramod,[status(thm)],[c_641,c_451]) ).
cnf(c_709,plain,
rstore_tail(queue_173,index_174) = q35,
inference(paramod,[status(thm)],[c_643,c_457]) ).
cnf(c_710,plain,
rstore_tail(queue_179,index_180) = q36,
inference(paramod,[status(thm)],[c_645,c_461]) ).
cnf(c_711,plain,
rstore_tail(queue_185,index_186) = q37,
inference(paramod,[status(thm)],[c_647,c_465]) ).
cnf(c_712,plain,
rstore_tail(queue_191,index_192) = q38,
inference(paramod,[status(thm)],[c_649,c_471]) ).
cnf(c_713,plain,
rstore_tail(queue_197,index_198) = q39,
inference(paramod,[status(thm)],[c_651,c_475]) ).
cnf(c_714,plain,
rstore_tail(queue_203,index_204) = q4,
inference(paramod,[status(thm)],[c_653,c_479]) ).
cnf(c_715,plain,
rstore_tail(queue_209,index_210) = q40,
inference(paramod,[status(thm)],[c_655,c_483]) ).
cnf(c_716,plain,
rstore_tail(queue_215,index_216) = q41,
inference(paramod,[status(thm)],[c_657,c_487]) ).
cnf(c_717,plain,
rstore_tail(queue_221,index_222) = q42,
inference(paramod,[status(thm)],[c_659,c_491]) ).
cnf(c_718,plain,
rstore_tail(queue_227,index_228) = q43,
inference(paramod,[status(thm)],[c_661,c_495]) ).
cnf(c_719,plain,
rstore_tail(queue_233,index_234) = q44,
inference(paramod,[status(thm)],[c_663,c_501]) ).
cnf(c_720,plain,
rstore_tail(queue_239,index_240) = q45,
inference(paramod,[status(thm)],[c_665,c_505]) ).
cnf(c_721,plain,
rstore_tail(queue_245,index_246) = q46,
inference(paramod,[status(thm)],[c_667,c_509]) ).
cnf(c_722,plain,
rstore_tail(queue_251,index_252) = q5,
inference(paramod,[status(thm)],[c_669,c_515]) ).
cnf(c_723,plain,
rstore_tail(queue_257,index_258) = q6,
inference(paramod,[status(thm)],[c_671,c_519]) ).
cnf(c_724,plain,
rstore_tail(queue_263,index_264) = q7,
inference(paramod,[status(thm)],[c_673,c_523]) ).
cnf(c_725,plain,
rstore_tail(queue_269,index_270) = q8,
inference(paramod,[status(thm)],[c_675,c_527]) ).
cnf(c_726,plain,
rstore_tail(queue_275,index_276) = q9,
inference(paramod,[status(thm)],[c_677,c_531]) ).
cnf(c_2298,plain,
p(A) = s(s(A)),
inference(paramod,[status(thm)],[c_16,c_12]) ).
cnf(c_729,plain,
s(s(A)) = p(A),
inference(copy,[status(thm)],[c_2298]) ).
cnf(c_757,plain,
select(earray_244,index_243) = e45,
inference(paramod,[status(thm)],[c_126,c_1]) ).
cnf(c_830,plain,
p(index_246) = index_243,
inference(paramod,[status(thm)],[c_316,c_12]) ).
cnf(c_842,plain,
p(index_281) = index_282,
inference(paramod,[status(thm)],[c_343,c_12]) ).
cnf(c_854,plain,
p(index_6) = index_3,
inference(paramod,[status(thm)],[c_367,c_12]) ).
cnf(c_871,plain,
rselect_head(queue_101) = rselect_head(q23),
inference(paramod,[status(thm)],[c_401,c_9]) ).
cnf(c_874,plain,
rselect_head(queue_107) = rselect_head(q24),
inference(paramod,[status(thm)],[c_405,c_9]) ).
cnf(c_877,plain,
rselect_head(queue_11) = rselect_head(q9),
inference(paramod,[status(thm)],[c_409,c_9]) ).
cnf(c_880,plain,
rselect_head(queue_113) = rselect_head(q25),
inference(paramod,[status(thm)],[c_411,c_9]) ).
cnf(c_883,plain,
rselect_head(queue_119) = rselect_head(q26),
inference(paramod,[status(thm)],[c_415,c_9]) ).
cnf(c_886,plain,
rselect_head(queue_125) = rselect_head(q27),
inference(paramod,[status(thm)],[c_419,c_9]) ).
cnf(c_889,plain,
rselect_head(queue_131) = rselect_head(q28),
inference(paramod,[status(thm)],[c_425,c_9]) ).
cnf(c_892,plain,
rselect_head(queue_137) = rselect_head(q2),
inference(paramod,[status(thm)],[c_429,c_9]) ).
cnf(c_895,plain,
rselect_head(queue_143) = rselect_head(q29),
inference(paramod,[status(thm)],[c_433,c_9]) ).
cnf(c_898,plain,
rselect_head(queue_149) = rselect_head(q30),
inference(paramod,[status(thm)],[c_437,c_9]) ).
cnf(c_901,plain,
rselect_head(queue_155) = rselect_head(q31),
inference(paramod,[status(thm)],[c_441,c_9]) ).
cnf(c_904,plain,
rselect_head(queue_161) = rselect_head(q32),
inference(paramod,[status(thm)],[c_445,c_9]) ).
cnf(c_907,plain,
rselect_head(queue_167) = rselect_head(q33),
inference(paramod,[status(thm)],[c_449,c_9]) ).
cnf(c_910,plain,
rselect_head(queue_17) = rselect_head(q10),
inference(paramod,[status(thm)],[c_453,c_9]) ).
cnf(c_913,plain,
rselect_head(queue_173) = rselect_head(q34),
inference(paramod,[status(thm)],[c_455,c_9]) ).
cnf(c_916,plain,
rselect_head(queue_179) = rselect_head(q35),
inference(paramod,[status(thm)],[c_459,c_9]) ).
cnf(c_919,plain,
rselect_head(queue_185) = rselect_head(q36),
inference(paramod,[status(thm)],[c_463,c_9]) ).
cnf(c_922,plain,
rselect_head(queue_191) = rselect_head(q37),
inference(paramod,[status(thm)],[c_469,c_9]) ).
cnf(c_925,plain,
rselect_head(queue_197) = rselect_head(q38),
inference(paramod,[status(thm)],[c_473,c_9]) ).
cnf(c_928,plain,
rselect_head(queue_203) = rselect_head(q3),
inference(paramod,[status(thm)],[c_477,c_9]) ).
cnf(c_931,plain,
rselect_head(queue_209) = rselect_head(q39),
inference(paramod,[status(thm)],[c_481,c_9]) ).
cnf(c_934,plain,
rselect_head(queue_215) = rselect_head(q40),
inference(paramod,[status(thm)],[c_485,c_9]) ).
cnf(c_937,plain,
rselect_head(queue_221) = rselect_head(q41),
inference(paramod,[status(thm)],[c_489,c_9]) ).
cnf(c_940,plain,
rselect_head(queue_227) = rselect_head(q42),
inference(paramod,[status(thm)],[c_493,c_9]) ).
cnf(c_943,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(paramod,[status(thm)],[c_497,c_9]) ).
cnf(c_946,plain,
rselect_head(queue_233) = rselect_head(q43),
inference(paramod,[status(thm)],[c_499,c_9]) ).
cnf(c_949,plain,
rselect_head(queue_239) = rselect_head(q44),
inference(paramod,[status(thm)],[c_503,c_9]) ).
cnf(c_951,plain,
rselect_seq(queue_245) = earray_244,
inference(paramod,[status(thm)],[c_507,c_3]) ).
cnf(c_952,plain,
rselect_head(queue_245) = rselect_head(q45),
inference(paramod,[status(thm)],[c_507,c_9]) ).
cnf(c_955,plain,
rselect_head(queue_251) = rselect_head(q4),
inference(paramod,[status(thm)],[c_513,c_9]) ).
cnf(c_958,plain,
rselect_head(queue_257) = rselect_head(q5),
inference(paramod,[status(thm)],[c_517,c_9]) ).
cnf(c_961,plain,
rselect_head(queue_263) = rselect_head(q6),
inference(paramod,[status(thm)],[c_521,c_9]) ).
cnf(c_964,plain,
rselect_head(queue_269) = rselect_head(q7),
inference(paramod,[status(thm)],[c_525,c_9]) ).
cnf(c_967,plain,
rselect_head(queue_275) = rselect_head(q8),
inference(paramod,[status(thm)],[c_529,c_9]) ).
cnf(c_970,plain,
rselect_head(queue_29) = rselect_head(q12),
inference(paramod,[status(thm)],[c_533,c_9]) ).
cnf(c_973,plain,
rselect_head(queue_35) = rselect_head(q13),
inference(paramod,[status(thm)],[c_537,c_9]) ).
cnf(c_976,plain,
rselect_head(queue_41) = rselect_head(q14),
inference(paramod,[status(thm)],[c_541,c_9]) ).
cnf(c_979,plain,
rselect_head(queue_47) = rselect_head(q15),
inference(paramod,[status(thm)],[c_545,c_9]) ).
cnf(c_982,plain,
rselect_head(queue_5) = rselect_head(q0),
inference(paramod,[status(thm)],[c_549,c_9]) ).
cnf(c_985,plain,
rselect_head(queue_53) = rselect_head(q16),
inference(paramod,[status(thm)],[c_551,c_9]) ).
cnf(c_988,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(paramod,[status(thm)],[c_555,c_9]) ).
cnf(c_991,plain,
rselect_head(queue_65) = rselect_head(q18),
inference(paramod,[status(thm)],[c_559,c_9]) ).
cnf(c_994,plain,
rselect_head(queue_71) = rselect_head(q1),
inference(paramod,[status(thm)],[c_565,c_9]) ).
cnf(c_997,plain,
rselect_head(queue_77) = rselect_head(q19),
inference(paramod,[status(thm)],[c_569,c_9]) ).
cnf(c_1000,plain,
rselect_head(queue_83) = rselect_head(q20),
inference(paramod,[status(thm)],[c_573,c_9]) ).
cnf(c_1003,plain,
rselect_head(queue_89) = rselect_head(q21),
inference(paramod,[status(thm)],[c_577,c_9]) ).
cnf(c_1006,plain,
rselect_head(queue_95) = rselect_head(q22),
inference(paramod,[status(thm)],[c_581,c_9]) ).
cnf(c_1008,plain,
rselect_head(q0) = index_0,
inference(paramod,[status(thm)],[c_680,c_4]) ).
cnf(c_2299,plain,
rselect_tail(q0) = rselect_tail(q),
inference(paramod,[status(thm)],[c_680,c_11]) ).
cnf(c_2300,plain,
index_3 = rselect_tail(q),
inference(paramod,[status(thm)],[c_345,c_2299]) ).
cnf(c_2301,plain,
index_3 = index_0,
inference(paramod,[status(thm)],[c_208,c_2300]) ).
cnf(c_1010,plain,
index_0 = index_3,
inference(copy,[status(thm)],[c_2301]) ).
cnf(c_2302,plain,
rselect_head(queue_5) = index_0,
inference(paramod,[status(thm)],[c_1008,c_982]) ).
cnf(c_1011,plain,
rselect_head(queue_5) = index_3,
inference(paramod,[status(thm)],[c_1010,c_2302]) ).
cnf(c_2303,plain,
rselect_tail(q1) = index_6,
inference(paramod,[status(thm)],[c_681,c_5]) ).
cnf(c_2304,plain,
index_69 = index_6,
inference(paramod,[status(thm)],[c_375,c_2303]) ).
cnf(c_1015,plain,
index_6 = index_69,
inference(copy,[status(thm)],[c_2304]) ).
cnf(c_2305,plain,
rselect_head(q1) = rselect_head(queue_5),
inference(paramod,[status(thm)],[c_681,c_8]) ).
cnf(c_1017,plain,
rselect_head(q1) = index_3,
inference(paramod,[status(thm)],[c_1011,c_2305]) ).
cnf(c_1019,plain,
p(index_69) = index_3,
inference(paramod,[status(thm)],[c_1015,c_854]) ).
cnf(c_1021,plain,
s(index_3) = index_69,
inference(paramod,[status(thm)],[c_1015,c_367]) ).
cnf(c_1024,plain,
rselect_head(queue_71) = index_3,
inference(paramod,[status(thm)],[c_1017,c_994]) ).
cnf(c_2306,plain,
rselect_tail(q10) = index_12,
inference(paramod,[status(thm)],[c_682,c_5]) ).
cnf(c_2307,plain,
index_15 = index_12,
inference(paramod,[status(thm)],[c_244,c_2306]) ).
cnf(c_1025,plain,
index_12 = index_15,
inference(copy,[status(thm)],[c_2307]) ).
cnf(c_2308,plain,
rselect_head(q10) = rselect_head(queue_11),
inference(paramod,[status(thm)],[c_682,c_8]) ).
cnf(c_2309,plain,
rselect_head(q10) = rselect_head(q9),
inference(paramod,[status(thm)],[c_877,c_2308]) ).
cnf(c_1027,plain,
rselect_head(q9) = rselect_head(q10),
inference(copy,[status(thm)],[c_2309]) ).
cnf(c_1031,plain,
s(index_9) = index_15,
inference(paramod,[status(thm)],[c_1025,c_222]) ).
cnf(c_2310,plain,
rselect_tail(q11) = index_18,
inference(paramod,[status(thm)],[c_683,c_5]) ).
cnf(c_2311,plain,
index_21 = index_18,
inference(paramod,[status(thm)],[c_288,c_2310]) ).
cnf(c_1035,plain,
index_18 = index_21,
inference(copy,[status(thm)],[c_2311]) ).
cnf(c_2312,plain,
rselect_head(q11) = rselect_head(queue_17),
inference(paramod,[status(thm)],[c_683,c_8]) ).
cnf(c_1037,plain,
rselect_head(q11) = rselect_head(q10),
inference(paramod,[status(thm)],[c_910,c_2312]) ).
cnf(c_1041,plain,
s(index_15) = index_21,
inference(paramod,[status(thm)],[c_1035,c_266]) ).
cnf(c_1044,plain,
rselect_head(queue_23) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1037,c_943]) ).
cnf(c_2313,plain,
rselect_tail(q12) = index_24,
inference(paramod,[status(thm)],[c_684,c_5]) ).
cnf(c_2314,plain,
index_27 = index_24,
inference(paramod,[status(thm)],[c_332,c_2313]) ).
cnf(c_1045,plain,
index_24 = index_27,
inference(copy,[status(thm)],[c_2314]) ).
cnf(c_2315,plain,
rselect_head(q12) = rselect_head(queue_23),
inference(paramod,[status(thm)],[c_684,c_8]) ).
cnf(c_1047,plain,
rselect_head(q12) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1044,c_2315]) ).
cnf(c_1051,plain,
s(index_21) = index_27,
inference(paramod,[status(thm)],[c_1045,c_310]) ).
cnf(c_1054,plain,
rselect_head(queue_29) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1047,c_970]) ).
cnf(c_2316,plain,
rselect_tail(q13) = index_30,
inference(paramod,[status(thm)],[c_685,c_5]) ).
cnf(c_2317,plain,
index_33 = index_30,
inference(paramod,[status(thm)],[c_349,c_2316]) ).
cnf(c_1055,plain,
index_30 = index_33,
inference(copy,[status(thm)],[c_2317]) ).
cnf(c_2318,plain,
rselect_head(q13) = rselect_head(queue_29),
inference(paramod,[status(thm)],[c_685,c_8]) ).
cnf(c_1057,plain,
rselect_head(q13) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1054,c_2318]) ).
cnf(c_1061,plain,
s(index_27) = index_33,
inference(paramod,[status(thm)],[c_1055,c_347]) ).
cnf(c_1064,plain,
rselect_head(queue_35) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1057,c_973]) ).
cnf(c_2319,plain,
rselect_tail(q14) = index_36,
inference(paramod,[status(thm)],[c_686,c_5]) ).
cnf(c_2320,plain,
index_39 = index_36,
inference(paramod,[status(thm)],[c_353,c_2319]) ).
cnf(c_1065,plain,
index_36 = index_39,
inference(copy,[status(thm)],[c_2320]) ).
cnf(c_2321,plain,
rselect_head(q14) = rselect_head(queue_35),
inference(paramod,[status(thm)],[c_686,c_8]) ).
cnf(c_1067,plain,
rselect_head(q14) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1064,c_2321]) ).
cnf(c_1071,plain,
s(index_33) = index_39,
inference(paramod,[status(thm)],[c_1065,c_351]) ).
cnf(c_1074,plain,
rselect_head(queue_41) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1067,c_976]) ).
cnf(c_2322,plain,
rselect_tail(q15) = index_42,
inference(paramod,[status(thm)],[c_687,c_5]) ).
cnf(c_2323,plain,
index_45 = index_42,
inference(paramod,[status(thm)],[c_357,c_2322]) ).
cnf(c_1075,plain,
index_42 = index_45,
inference(copy,[status(thm)],[c_2323]) ).
cnf(c_2324,plain,
rselect_head(q15) = rselect_head(queue_41),
inference(paramod,[status(thm)],[c_687,c_8]) ).
cnf(c_1077,plain,
rselect_head(q15) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1074,c_2324]) ).
cnf(c_1081,plain,
s(index_39) = index_45,
inference(paramod,[status(thm)],[c_1075,c_355]) ).
cnf(c_1084,plain,
rselect_head(queue_47) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1077,c_979]) ).
cnf(c_2325,plain,
rselect_tail(q16) = index_48,
inference(paramod,[status(thm)],[c_688,c_5]) ).
cnf(c_2326,plain,
index_51 = index_48,
inference(paramod,[status(thm)],[c_361,c_2325]) ).
cnf(c_1085,plain,
index_48 = index_51,
inference(copy,[status(thm)],[c_2326]) ).
cnf(c_2327,plain,
rselect_head(q16) = rselect_head(queue_47),
inference(paramod,[status(thm)],[c_688,c_8]) ).
cnf(c_1087,plain,
rselect_head(q16) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1084,c_2327]) ).
cnf(c_1091,plain,
s(index_45) = index_51,
inference(paramod,[status(thm)],[c_1085,c_359]) ).
cnf(c_1094,plain,
rselect_head(queue_53) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1087,c_985]) ).
cnf(c_2328,plain,
rselect_tail(q17) = index_54,
inference(paramod,[status(thm)],[c_689,c_5]) ).
cnf(c_2329,plain,
index_57 = index_54,
inference(paramod,[status(thm)],[c_365,c_2328]) ).
cnf(c_1095,plain,
index_54 = index_57,
inference(copy,[status(thm)],[c_2329]) ).
cnf(c_2330,plain,
rselect_head(q17) = rselect_head(queue_53),
inference(paramod,[status(thm)],[c_689,c_8]) ).
cnf(c_1097,plain,
rselect_head(q17) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1094,c_2330]) ).
cnf(c_1101,plain,
s(index_51) = index_57,
inference(paramod,[status(thm)],[c_1095,c_363]) ).
cnf(c_1104,plain,
rselect_head(queue_59) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1097,c_988]) ).
cnf(c_2331,plain,
rselect_tail(q18) = index_60,
inference(paramod,[status(thm)],[c_690,c_5]) ).
cnf(c_2332,plain,
index_63 = index_60,
inference(paramod,[status(thm)],[c_371,c_2331]) ).
cnf(c_1105,plain,
index_60 = index_63,
inference(copy,[status(thm)],[c_2332]) ).
cnf(c_2333,plain,
rselect_head(q18) = rselect_head(queue_59),
inference(paramod,[status(thm)],[c_690,c_8]) ).
cnf(c_1107,plain,
rselect_head(q18) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1104,c_2333]) ).
cnf(c_1111,plain,
s(index_57) = index_63,
inference(paramod,[status(thm)],[c_1105,c_369]) ).
cnf(c_1114,plain,
rselect_head(queue_65) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1107,c_991]) ).
cnf(c_2334,plain,
rselect_tail(q19) = index_66,
inference(paramod,[status(thm)],[c_691,c_5]) ).
cnf(c_2335,plain,
index_75 = index_66,
inference(paramod,[status(thm)],[c_379,c_2334]) ).
cnf(c_1115,plain,
index_66 = index_75,
inference(copy,[status(thm)],[c_2335]) ).
cnf(c_2336,plain,
rselect_head(q19) = rselect_head(queue_65),
inference(paramod,[status(thm)],[c_691,c_8]) ).
cnf(c_1117,plain,
rselect_head(q19) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1114,c_2336]) ).
cnf(c_1121,plain,
s(index_63) = index_75,
inference(paramod,[status(thm)],[c_1115,c_373]) ).
cnf(c_1124,plain,
rselect_head(queue_77) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1117,c_997]) ).
cnf(c_2337,plain,
rselect_tail(q2) = index_72,
inference(paramod,[status(thm)],[c_692,c_5]) ).
cnf(c_2338,plain,
index_135 = index_72,
inference(paramod,[status(thm)],[c_234,c_2337]) ).
cnf(c_1125,plain,
index_72 = index_135,
inference(copy,[status(thm)],[c_2338]) ).
cnf(c_2339,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(paramod,[status(thm)],[c_692,c_8]) ).
cnf(c_1127,plain,
rselect_head(q2) = index_3,
inference(paramod,[status(thm)],[c_1024,c_2339]) ).
cnf(c_1131,plain,
s(index_69) = index_135,
inference(paramod,[status(thm)],[c_1125,c_377]) ).
cnf(c_1136,plain,
rselect_head(queue_137) = index_3,
inference(paramod,[status(thm)],[c_1127,c_892]) ).
cnf(c_2340,plain,
rselect_tail(q20) = index_78,
inference(paramod,[status(thm)],[c_693,c_5]) ).
cnf(c_2341,plain,
index_81 = index_78,
inference(paramod,[status(thm)],[c_383,c_2340]) ).
cnf(c_1137,plain,
index_78 = index_81,
inference(copy,[status(thm)],[c_2341]) ).
cnf(c_2342,plain,
rselect_head(q20) = rselect_head(queue_77),
inference(paramod,[status(thm)],[c_693,c_8]) ).
cnf(c_1139,plain,
rselect_head(q20) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1124,c_2342]) ).
cnf(c_1143,plain,
s(index_75) = index_81,
inference(paramod,[status(thm)],[c_1137,c_381]) ).
cnf(c_1146,plain,
rselect_head(queue_83) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1139,c_1000]) ).
cnf(c_2343,plain,
rselect_tail(q21) = index_84,
inference(paramod,[status(thm)],[c_694,c_5]) ).
cnf(c_2344,plain,
index_87 = index_84,
inference(paramod,[status(thm)],[c_387,c_2343]) ).
cnf(c_1147,plain,
index_84 = index_87,
inference(copy,[status(thm)],[c_2344]) ).
cnf(c_2345,plain,
rselect_head(q21) = rselect_head(queue_83),
inference(paramod,[status(thm)],[c_694,c_8]) ).
cnf(c_1149,plain,
rselect_head(q21) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1146,c_2345]) ).
cnf(c_1153,plain,
s(index_81) = index_87,
inference(paramod,[status(thm)],[c_1147,c_385]) ).
cnf(c_1156,plain,
rselect_head(queue_89) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1149,c_1003]) ).
cnf(c_2346,plain,
rselect_tail(q22) = index_90,
inference(paramod,[status(thm)],[c_695,c_5]) ).
cnf(c_2347,plain,
index_93 = index_90,
inference(paramod,[status(thm)],[c_393,c_2346]) ).
cnf(c_1157,plain,
index_90 = index_93,
inference(copy,[status(thm)],[c_2347]) ).
cnf(c_2348,plain,
rselect_head(q22) = rselect_head(queue_89),
inference(paramod,[status(thm)],[c_695,c_8]) ).
cnf(c_1159,plain,
rselect_head(q22) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1156,c_2348]) ).
cnf(c_1163,plain,
s(index_87) = index_93,
inference(paramod,[status(thm)],[c_1157,c_391]) ).
cnf(c_1166,plain,
rselect_head(queue_95) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1159,c_1006]) ).
cnf(c_2349,plain,
rselect_tail(q23) = index_96,
inference(paramod,[status(thm)],[c_696,c_5]) ).
cnf(c_2350,plain,
index_99 = index_96,
inference(paramod,[status(thm)],[c_397,c_2349]) ).
cnf(c_1167,plain,
index_96 = index_99,
inference(copy,[status(thm)],[c_2350]) ).
cnf(c_2351,plain,
rselect_head(q23) = rselect_head(queue_95),
inference(paramod,[status(thm)],[c_696,c_8]) ).
cnf(c_1169,plain,
rselect_head(q23) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1166,c_2351]) ).
cnf(c_1173,plain,
s(index_93) = index_99,
inference(paramod,[status(thm)],[c_1167,c_395]) ).
cnf(c_1176,plain,
rselect_head(queue_101) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1169,c_871]) ).
cnf(c_2352,plain,
rselect_tail(q24) = index_102,
inference(paramod,[status(thm)],[c_697,c_5]) ).
cnf(c_2353,plain,
index_105 = index_102,
inference(paramod,[status(thm)],[c_212,c_2352]) ).
cnf(c_1177,plain,
index_102 = index_105,
inference(copy,[status(thm)],[c_2353]) ).
cnf(c_2354,plain,
rselect_head(q24) = rselect_head(queue_101),
inference(paramod,[status(thm)],[c_697,c_8]) ).
cnf(c_1179,plain,
rselect_head(q24) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1176,c_2354]) ).
cnf(c_1183,plain,
s(index_99) = index_105,
inference(paramod,[status(thm)],[c_1177,c_210]) ).
cnf(c_1186,plain,
rselect_head(queue_107) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1179,c_874]) ).
cnf(c_2355,plain,
rselect_tail(q25) = index_108,
inference(paramod,[status(thm)],[c_698,c_5]) ).
cnf(c_2356,plain,
index_111 = index_108,
inference(paramod,[status(thm)],[c_216,c_2355]) ).
cnf(c_1187,plain,
index_108 = index_111,
inference(copy,[status(thm)],[c_2356]) ).
cnf(c_2357,plain,
rselect_head(q25) = rselect_head(queue_107),
inference(paramod,[status(thm)],[c_698,c_8]) ).
cnf(c_1189,plain,
rselect_head(q25) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1186,c_2357]) ).
cnf(c_1193,plain,
s(index_105) = index_111,
inference(paramod,[status(thm)],[c_1187,c_214]) ).
cnf(c_1196,plain,
rselect_head(queue_113) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1189,c_880]) ).
cnf(c_2358,plain,
rselect_tail(q26) = index_114,
inference(paramod,[status(thm)],[c_699,c_5]) ).
cnf(c_2359,plain,
index_117 = index_114,
inference(paramod,[status(thm)],[c_220,c_2358]) ).
cnf(c_1197,plain,
index_114 = index_117,
inference(copy,[status(thm)],[c_2359]) ).
cnf(c_2360,plain,
rselect_head(q26) = rselect_head(queue_113),
inference(paramod,[status(thm)],[c_699,c_8]) ).
cnf(c_1199,plain,
rselect_head(q26) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1196,c_2360]) ).
cnf(c_1203,plain,
s(index_111) = index_117,
inference(paramod,[status(thm)],[c_1197,c_218]) ).
cnf(c_1206,plain,
rselect_head(queue_119) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1199,c_883]) ).
cnf(c_2361,plain,
rselect_tail(q27) = index_120,
inference(paramod,[status(thm)],[c_700,c_5]) ).
cnf(c_2362,plain,
index_123 = index_120,
inference(paramod,[status(thm)],[c_226,c_2361]) ).
cnf(c_1207,plain,
index_120 = index_123,
inference(copy,[status(thm)],[c_2362]) ).
cnf(c_2363,plain,
rselect_head(q27) = rselect_head(queue_119),
inference(paramod,[status(thm)],[c_700,c_8]) ).
cnf(c_1209,plain,
rselect_head(q27) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1206,c_2363]) ).
cnf(c_1213,plain,
s(index_117) = index_123,
inference(paramod,[status(thm)],[c_1207,c_224]) ).
cnf(c_1216,plain,
rselect_head(queue_125) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1209,c_886]) ).
cnf(c_2364,plain,
rselect_tail(q28) = index_126,
inference(paramod,[status(thm)],[c_701,c_5]) ).
cnf(c_2365,plain,
index_129 = index_126,
inference(paramod,[status(thm)],[c_230,c_2364]) ).
cnf(c_1217,plain,
index_126 = index_129,
inference(copy,[status(thm)],[c_2365]) ).
cnf(c_2366,plain,
rselect_head(q28) = rselect_head(queue_125),
inference(paramod,[status(thm)],[c_701,c_8]) ).
cnf(c_1219,plain,
rselect_head(q28) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1216,c_2366]) ).
cnf(c_1223,plain,
s(index_123) = index_129,
inference(paramod,[status(thm)],[c_1217,c_228]) ).
cnf(c_1226,plain,
rselect_head(queue_131) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1219,c_889]) ).
cnf(c_2367,plain,
rselect_tail(q29) = index_132,
inference(paramod,[status(thm)],[c_702,c_5]) ).
cnf(c_2368,plain,
index_141 = index_132,
inference(paramod,[status(thm)],[c_238,c_2367]) ).
cnf(c_1227,plain,
index_132 = index_141,
inference(copy,[status(thm)],[c_2368]) ).
cnf(c_2369,plain,
rselect_head(q29) = rselect_head(queue_131),
inference(paramod,[status(thm)],[c_702,c_8]) ).
cnf(c_1229,plain,
rselect_head(q29) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1226,c_2369]) ).
cnf(c_1233,plain,
s(index_129) = index_141,
inference(paramod,[status(thm)],[c_1227,c_232]) ).
cnf(c_1236,plain,
rselect_head(queue_143) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1229,c_895]) ).
cnf(c_2370,plain,
rselect_tail(q3) = index_138,
inference(paramod,[status(thm)],[c_703,c_5]) ).
cnf(c_2371,plain,
index_201 = index_138,
inference(paramod,[status(thm)],[c_282,c_2370]) ).
cnf(c_1237,plain,
index_138 = index_201,
inference(copy,[status(thm)],[c_2371]) ).
cnf(c_2372,plain,
rselect_head(q3) = rselect_head(queue_137),
inference(paramod,[status(thm)],[c_703,c_8]) ).
cnf(c_1239,plain,
rselect_head(q3) = index_3,
inference(paramod,[status(thm)],[c_1136,c_2372]) ).
cnf(c_1243,plain,
s(index_135) = index_201,
inference(paramod,[status(thm)],[c_1237,c_236]) ).
cnf(c_1246,plain,
rselect_head(queue_203) = index_3,
inference(paramod,[status(thm)],[c_1239,c_928]) ).
cnf(c_2373,plain,
rselect_tail(q30) = index_144,
inference(paramod,[status(thm)],[c_704,c_5]) ).
cnf(c_2374,plain,
index_147 = index_144,
inference(paramod,[status(thm)],[c_242,c_2373]) ).
cnf(c_1247,plain,
index_144 = index_147,
inference(copy,[status(thm)],[c_2374]) ).
cnf(c_2375,plain,
rselect_head(q30) = rselect_head(queue_143),
inference(paramod,[status(thm)],[c_704,c_8]) ).
cnf(c_1249,plain,
rselect_head(q30) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1236,c_2375]) ).
cnf(c_1253,plain,
s(index_141) = index_147,
inference(paramod,[status(thm)],[c_1247,c_240]) ).
cnf(c_1256,plain,
rselect_head(queue_149) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1249,c_898]) ).
cnf(c_2376,plain,
rselect_tail(q31) = index_150,
inference(paramod,[status(thm)],[c_705,c_5]) ).
cnf(c_2377,plain,
index_153 = index_150,
inference(paramod,[status(thm)],[c_248,c_2376]) ).
cnf(c_1257,plain,
index_150 = index_153,
inference(copy,[status(thm)],[c_2377]) ).
cnf(c_2378,plain,
rselect_head(q31) = rselect_head(queue_149),
inference(paramod,[status(thm)],[c_705,c_8]) ).
cnf(c_1259,plain,
rselect_head(q31) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1256,c_2378]) ).
cnf(c_1263,plain,
s(index_147) = index_153,
inference(paramod,[status(thm)],[c_1257,c_246]) ).
cnf(c_1266,plain,
rselect_head(queue_155) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1259,c_901]) ).
cnf(c_2379,plain,
rselect_tail(q32) = index_156,
inference(paramod,[status(thm)],[c_706,c_5]) ).
cnf(c_2380,plain,
index_159 = index_156,
inference(paramod,[status(thm)],[c_252,c_2379]) ).
cnf(c_1267,plain,
index_156 = index_159,
inference(copy,[status(thm)],[c_2380]) ).
cnf(c_2381,plain,
rselect_head(q32) = rselect_head(queue_155),
inference(paramod,[status(thm)],[c_706,c_8]) ).
cnf(c_1269,plain,
rselect_head(q32) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1266,c_2381]) ).
cnf(c_1273,plain,
s(index_153) = index_159,
inference(paramod,[status(thm)],[c_1267,c_250]) ).
cnf(c_1276,plain,
rselect_head(queue_161) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1269,c_904]) ).
cnf(c_2382,plain,
rselect_tail(q33) = index_162,
inference(paramod,[status(thm)],[c_707,c_5]) ).
cnf(c_2383,plain,
index_165 = index_162,
inference(paramod,[status(thm)],[c_256,c_2382]) ).
cnf(c_1277,plain,
index_162 = index_165,
inference(copy,[status(thm)],[c_2383]) ).
cnf(c_2384,plain,
rselect_head(q33) = rselect_head(queue_161),
inference(paramod,[status(thm)],[c_707,c_8]) ).
cnf(c_1279,plain,
rselect_head(q33) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1276,c_2384]) ).
cnf(c_1283,plain,
s(index_159) = index_165,
inference(paramod,[status(thm)],[c_1277,c_254]) ).
cnf(c_1286,plain,
rselect_head(queue_167) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1279,c_907]) ).
cnf(c_2385,plain,
rselect_tail(q34) = index_168,
inference(paramod,[status(thm)],[c_708,c_5]) ).
cnf(c_2386,plain,
index_171 = index_168,
inference(paramod,[status(thm)],[c_260,c_2385]) ).
cnf(c_1287,plain,
index_168 = index_171,
inference(copy,[status(thm)],[c_2386]) ).
cnf(c_2387,plain,
rselect_head(q34) = rselect_head(queue_167),
inference(paramod,[status(thm)],[c_708,c_8]) ).
cnf(c_1289,plain,
rselect_head(q34) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1286,c_2387]) ).
cnf(c_1293,plain,
s(index_165) = index_171,
inference(paramod,[status(thm)],[c_1287,c_258]) ).
cnf(c_1296,plain,
rselect_head(queue_173) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1289,c_913]) ).
cnf(c_2388,plain,
rselect_tail(q35) = index_174,
inference(paramod,[status(thm)],[c_709,c_5]) ).
cnf(c_2389,plain,
index_177 = index_174,
inference(paramod,[status(thm)],[c_264,c_2388]) ).
cnf(c_1297,plain,
index_174 = index_177,
inference(copy,[status(thm)],[c_2389]) ).
cnf(c_2390,plain,
rselect_head(q35) = rselect_head(queue_173),
inference(paramod,[status(thm)],[c_709,c_8]) ).
cnf(c_1299,plain,
rselect_head(q35) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1296,c_2390]) ).
cnf(c_1303,plain,
s(index_171) = index_177,
inference(paramod,[status(thm)],[c_1297,c_262]) ).
cnf(c_1306,plain,
rselect_head(queue_179) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1299,c_916]) ).
cnf(c_2391,plain,
rselect_tail(q36) = index_180,
inference(paramod,[status(thm)],[c_710,c_5]) ).
cnf(c_2392,plain,
index_183 = index_180,
inference(paramod,[status(thm)],[c_270,c_2391]) ).
cnf(c_1307,plain,
index_180 = index_183,
inference(copy,[status(thm)],[c_2392]) ).
cnf(c_2393,plain,
rselect_head(q36) = rselect_head(queue_179),
inference(paramod,[status(thm)],[c_710,c_8]) ).
cnf(c_1309,plain,
rselect_head(q36) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1306,c_2393]) ).
cnf(c_1313,plain,
s(index_177) = index_183,
inference(paramod,[status(thm)],[c_1307,c_268]) ).
cnf(c_1316,plain,
rselect_head(queue_185) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1309,c_919]) ).
cnf(c_2394,plain,
rselect_tail(q37) = index_186,
inference(paramod,[status(thm)],[c_711,c_5]) ).
cnf(c_2395,plain,
index_189 = index_186,
inference(paramod,[status(thm)],[c_274,c_2394]) ).
cnf(c_1317,plain,
index_186 = index_189,
inference(copy,[status(thm)],[c_2395]) ).
cnf(c_2396,plain,
rselect_head(q37) = rselect_head(queue_185),
inference(paramod,[status(thm)],[c_711,c_8]) ).
cnf(c_1319,plain,
rselect_head(q37) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1316,c_2396]) ).
cnf(c_1323,plain,
s(index_183) = index_189,
inference(paramod,[status(thm)],[c_1317,c_272]) ).
cnf(c_1326,plain,
rselect_head(queue_191) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1319,c_922]) ).
cnf(c_2397,plain,
rselect_tail(q38) = index_192,
inference(paramod,[status(thm)],[c_712,c_5]) ).
cnf(c_2398,plain,
index_195 = index_192,
inference(paramod,[status(thm)],[c_278,c_2397]) ).
cnf(c_1327,plain,
index_192 = index_195,
inference(copy,[status(thm)],[c_2398]) ).
cnf(c_2399,plain,
rselect_head(q38) = rselect_head(queue_191),
inference(paramod,[status(thm)],[c_712,c_8]) ).
cnf(c_1329,plain,
rselect_head(q38) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1326,c_2399]) ).
cnf(c_1333,plain,
s(index_189) = index_195,
inference(paramod,[status(thm)],[c_1327,c_276]) ).
cnf(c_1336,plain,
rselect_head(queue_197) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1329,c_925]) ).
cnf(c_2400,plain,
rselect_tail(q39) = index_198,
inference(paramod,[status(thm)],[c_713,c_5]) ).
cnf(c_2401,plain,
index_207 = index_198,
inference(paramod,[status(thm)],[c_286,c_2400]) ).
cnf(c_1337,plain,
index_198 = index_207,
inference(copy,[status(thm)],[c_2401]) ).
cnf(c_2402,plain,
rselect_head(q39) = rselect_head(queue_197),
inference(paramod,[status(thm)],[c_713,c_8]) ).
cnf(c_1339,plain,
rselect_head(q39) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1336,c_2402]) ).
cnf(c_1343,plain,
s(index_195) = index_207,
inference(paramod,[status(thm)],[c_1337,c_280]) ).
cnf(c_1346,plain,
rselect_head(queue_209) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1339,c_931]) ).
cnf(c_2403,plain,
rselect_tail(q4) = index_204,
inference(paramod,[status(thm)],[c_714,c_5]) ).
cnf(c_2404,plain,
index_249 = index_204,
inference(paramod,[status(thm)],[c_318,c_2403]) ).
cnf(c_1347,plain,
index_204 = index_249,
inference(copy,[status(thm)],[c_2404]) ).
cnf(c_2405,plain,
rselect_head(q4) = rselect_head(queue_203),
inference(paramod,[status(thm)],[c_714,c_8]) ).
cnf(c_1349,plain,
rselect_head(q4) = index_3,
inference(paramod,[status(thm)],[c_1246,c_2405]) ).
cnf(c_1353,plain,
s(index_201) = index_249,
inference(paramod,[status(thm)],[c_1347,c_284]) ).
cnf(c_1356,plain,
rselect_head(queue_251) = index_3,
inference(paramod,[status(thm)],[c_1349,c_955]) ).
cnf(c_2406,plain,
rselect_tail(q40) = index_210,
inference(paramod,[status(thm)],[c_715,c_5]) ).
cnf(c_2407,plain,
index_213 = index_210,
inference(paramod,[status(thm)],[c_292,c_2406]) ).
cnf(c_1357,plain,
index_210 = index_213,
inference(copy,[status(thm)],[c_2407]) ).
cnf(c_2408,plain,
rselect_head(q40) = rselect_head(queue_209),
inference(paramod,[status(thm)],[c_715,c_8]) ).
cnf(c_1359,plain,
rselect_head(q40) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1346,c_2408]) ).
cnf(c_1363,plain,
s(index_207) = index_213,
inference(paramod,[status(thm)],[c_1357,c_290]) ).
cnf(c_1366,plain,
rselect_head(queue_215) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1359,c_934]) ).
cnf(c_2409,plain,
rselect_tail(q41) = index_216,
inference(paramod,[status(thm)],[c_716,c_5]) ).
cnf(c_2410,plain,
index_219 = index_216,
inference(paramod,[status(thm)],[c_296,c_2409]) ).
cnf(c_1367,plain,
index_216 = index_219,
inference(copy,[status(thm)],[c_2410]) ).
cnf(c_2411,plain,
rselect_head(q41) = rselect_head(queue_215),
inference(paramod,[status(thm)],[c_716,c_8]) ).
cnf(c_1369,plain,
rselect_head(q41) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1366,c_2411]) ).
cnf(c_1373,plain,
s(index_213) = index_219,
inference(paramod,[status(thm)],[c_1367,c_294]) ).
cnf(c_1376,plain,
rselect_head(queue_221) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1369,c_937]) ).
cnf(c_2412,plain,
rselect_tail(q42) = index_222,
inference(paramod,[status(thm)],[c_717,c_5]) ).
cnf(c_2413,plain,
index_225 = index_222,
inference(paramod,[status(thm)],[c_300,c_2412]) ).
cnf(c_1377,plain,
index_222 = index_225,
inference(copy,[status(thm)],[c_2413]) ).
cnf(c_2414,plain,
rselect_head(q42) = rselect_head(queue_221),
inference(paramod,[status(thm)],[c_717,c_8]) ).
cnf(c_1379,plain,
rselect_head(q42) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1376,c_2414]) ).
cnf(c_1383,plain,
s(index_219) = index_225,
inference(paramod,[status(thm)],[c_1377,c_298]) ).
cnf(c_1386,plain,
rselect_head(queue_227) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1379,c_940]) ).
cnf(c_2415,plain,
rselect_tail(q43) = index_228,
inference(paramod,[status(thm)],[c_718,c_5]) ).
cnf(c_2416,plain,
index_231 = index_228,
inference(paramod,[status(thm)],[c_304,c_2415]) ).
cnf(c_1387,plain,
index_228 = index_231,
inference(copy,[status(thm)],[c_2416]) ).
cnf(c_2417,plain,
rselect_head(q43) = rselect_head(queue_227),
inference(paramod,[status(thm)],[c_718,c_8]) ).
cnf(c_1389,plain,
rselect_head(q43) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1386,c_2417]) ).
cnf(c_1393,plain,
s(index_225) = index_231,
inference(paramod,[status(thm)],[c_1387,c_302]) ).
cnf(c_1396,plain,
rselect_head(queue_233) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1389,c_946]) ).
cnf(c_2418,plain,
rselect_tail(q44) = index_234,
inference(paramod,[status(thm)],[c_719,c_5]) ).
cnf(c_2419,plain,
index_237 = index_234,
inference(paramod,[status(thm)],[c_308,c_2418]) ).
cnf(c_1397,plain,
index_234 = index_237,
inference(copy,[status(thm)],[c_2419]) ).
cnf(c_2420,plain,
rselect_head(q44) = rselect_head(queue_233),
inference(paramod,[status(thm)],[c_719,c_8]) ).
cnf(c_1399,plain,
rselect_head(q44) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1396,c_2420]) ).
cnf(c_1403,plain,
s(index_231) = index_237,
inference(paramod,[status(thm)],[c_1397,c_306]) ).
cnf(c_1406,plain,
rselect_head(queue_239) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1399,c_949]) ).
cnf(c_2421,plain,
rselect_tail(q45) = index_240,
inference(paramod,[status(thm)],[c_720,c_5]) ).
cnf(c_2422,plain,
index_243 = index_240,
inference(paramod,[status(thm)],[c_314,c_2421]) ).
cnf(c_1407,plain,
index_240 = index_243,
inference(copy,[status(thm)],[c_2422]) ).
cnf(c_2423,plain,
rselect_head(q45) = rselect_head(queue_239),
inference(paramod,[status(thm)],[c_720,c_8]) ).
cnf(c_1409,plain,
rselect_head(q45) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1406,c_2423]) ).
cnf(c_1413,plain,
s(index_237) = index_243,
inference(paramod,[status(thm)],[c_1407,c_312]) ).
cnf(c_1416,plain,
rselect_head(queue_245) = rselect_head(q10),
inference(paramod,[status(thm)],[c_1409,c_952]) ).
cnf(c_2424,plain,
rselect_tail(q46) = index_246,
inference(paramod,[status(thm)],[c_721,c_5]) ).
cnf(c_1417,plain,
index_281 = index_246,
inference(paramod,[status(thm)],[c_342,c_2424]) ).
cnf(c_2425,plain,
rselect_seq(q46) = rselect_seq(queue_245),
inference(paramod,[status(thm)],[c_721,c_7]) ).
cnf(c_2426,plain,
earray_278 = rselect_seq(queue_245),
inference(paramod,[status(thm)],[c_150,c_2425]) ).
cnf(c_2427,plain,
earray_278 = earray_244,
inference(paramod,[status(thm)],[c_951,c_2426]) ).
cnf(c_1418,plain,
earray_244 = earray_278,
inference(copy,[status(thm)],[c_2427]) ).
cnf(c_2428,plain,
rselect_head(q46) = rselect_head(queue_245),
inference(paramod,[status(thm)],[c_721,c_8]) ).
cnf(c_2429,plain,
index_279 = rselect_head(queue_245),
inference(paramod,[status(thm)],[c_340,c_2428]) ).
cnf(c_2430,plain,
index_279 = rselect_head(q10),
inference(paramod,[status(thm)],[c_1416,c_2429]) ).
cnf(c_1419,plain,
rselect_head(q10) = index_279,
inference(copy,[status(thm)],[c_2430]) ).
cnf(c_2431,plain,
p(index_246) = index_282,
inference(paramod,[status(thm)],[c_1417,c_842]) ).
cnf(c_2432,plain,
index_243 = index_282,
inference(paramod,[status(thm)],[c_830,c_2431]) ).
cnf(c_1421,plain,
index_282 = index_243,
inference(copy,[status(thm)],[c_2432]) ).
cnf(c_1425,plain,
select(earray_278,index_243) = e45,
inference(paramod,[status(thm)],[c_1418,c_757]) ).
cnf(c_1498,plain,
rselect_head(q9) = index_279,
inference(paramod,[status(thm)],[c_1419,c_1027]) ).
cnf(c_2433,plain,
select(earray_278,index_243) = elem_283,
inference(paramod,[status(thm)],[c_1421,c_206]) ).
cnf(c_2434,plain,
e45 = elem_283,
inference(paramod,[status(thm)],[c_1425,c_2433]) ).
cnf(c_1500,plain,
elem_283 = e45,
inference(copy,[status(thm)],[c_2434]) ).
cnf(c_2435,plain,
e45 != elem_280,
inference(paramod,[status(thm)],[c_1500,c_679]) ).
cnf(c_1501,plain,
elem_280 != e45,
inference(copy,[status(thm)],[c_2435]) ).
cnf(c_2436,plain,
rselect_tail(q5) = index_252,
inference(paramod,[status(thm)],[c_722,c_5]) ).
cnf(c_2437,plain,
index_255 = index_252,
inference(paramod,[status(thm)],[c_322,c_2436]) ).
cnf(c_1502,plain,
index_252 = index_255,
inference(copy,[status(thm)],[c_2437]) ).
cnf(c_2438,plain,
rselect_head(q5) = rselect_head(queue_251),
inference(paramod,[status(thm)],[c_722,c_8]) ).
cnf(c_1504,plain,
rselect_head(q5) = index_3,
inference(paramod,[status(thm)],[c_1356,c_2438]) ).
cnf(c_1508,plain,
s(index_249) = index_255,
inference(paramod,[status(thm)],[c_1502,c_320]) ).
cnf(c_1511,plain,
rselect_head(queue_257) = index_3,
inference(paramod,[status(thm)],[c_1504,c_958]) ).
cnf(c_2439,plain,
rselect_tail(q6) = index_258,
inference(paramod,[status(thm)],[c_723,c_5]) ).
cnf(c_2440,plain,
index_261 = index_258,
inference(paramod,[status(thm)],[c_326,c_2439]) ).
cnf(c_1512,plain,
index_258 = index_261,
inference(copy,[status(thm)],[c_2440]) ).
cnf(c_2441,plain,
rselect_head(q6) = rselect_head(queue_257),
inference(paramod,[status(thm)],[c_723,c_8]) ).
cnf(c_1514,plain,
rselect_head(q6) = index_3,
inference(paramod,[status(thm)],[c_1511,c_2441]) ).
cnf(c_1518,plain,
s(index_255) = index_261,
inference(paramod,[status(thm)],[c_1512,c_324]) ).
cnf(c_1521,plain,
rselect_head(queue_263) = index_3,
inference(paramod,[status(thm)],[c_1514,c_961]) ).
cnf(c_2442,plain,
rselect_tail(q7) = index_264,
inference(paramod,[status(thm)],[c_724,c_5]) ).
cnf(c_2443,plain,
index_267 = index_264,
inference(paramod,[status(thm)],[c_330,c_2442]) ).
cnf(c_1522,plain,
index_264 = index_267,
inference(copy,[status(thm)],[c_2443]) ).
cnf(c_2444,plain,
rselect_head(q7) = rselect_head(queue_263),
inference(paramod,[status(thm)],[c_724,c_8]) ).
cnf(c_1524,plain,
rselect_head(q7) = index_3,
inference(paramod,[status(thm)],[c_1521,c_2444]) ).
cnf(c_1528,plain,
s(index_261) = index_267,
inference(paramod,[status(thm)],[c_1522,c_328]) ).
cnf(c_1531,plain,
rselect_head(queue_269) = index_3,
inference(paramod,[status(thm)],[c_1524,c_964]) ).
cnf(c_2445,plain,
rselect_tail(q8) = index_270,
inference(paramod,[status(thm)],[c_725,c_5]) ).
cnf(c_2446,plain,
index_273 = index_270,
inference(paramod,[status(thm)],[c_336,c_2445]) ).
cnf(c_1532,plain,
index_270 = index_273,
inference(copy,[status(thm)],[c_2446]) ).
cnf(c_2447,plain,
rselect_head(q8) = rselect_head(queue_269),
inference(paramod,[status(thm)],[c_725,c_8]) ).
cnf(c_1534,plain,
rselect_head(q8) = index_3,
inference(paramod,[status(thm)],[c_1531,c_2447]) ).
cnf(c_1538,plain,
s(index_267) = index_273,
inference(paramod,[status(thm)],[c_1532,c_334]) ).
cnf(c_1541,plain,
rselect_head(queue_275) = index_3,
inference(paramod,[status(thm)],[c_1534,c_967]) ).
cnf(c_2448,plain,
rselect_tail(q9) = index_276,
inference(paramod,[status(thm)],[c_726,c_5]) ).
cnf(c_2449,plain,
index_9 = index_276,
inference(paramod,[status(thm)],[c_389,c_2448]) ).
cnf(c_1542,plain,
index_276 = index_9,
inference(copy,[status(thm)],[c_2449]) ).
cnf(c_2450,plain,
rselect_head(q9) = rselect_head(queue_275),
inference(paramod,[status(thm)],[c_726,c_8]) ).
cnf(c_2451,plain,
index_279 = rselect_head(queue_275),
inference(paramod,[status(thm)],[c_1498,c_2450]) ).
cnf(c_1544,plain,
index_279 = index_3,
inference(paramod,[status(thm)],[c_1541,c_2451]) ).
cnf(c_1548,plain,
s(index_273) = index_9,
inference(paramod,[status(thm)],[c_1542,c_338]) ).
cnf(c_1626,plain,
select(earray_278,index_3) = elem_280,
inference(paramod,[status(thm)],[c_1544,c_204]) ).
cnf(c_2452,plain,
s(s(index_69)) = index_3,
inference(paramod,[status(thm)],[c_1019,c_729]) ).
cnf(c_2453,plain,
s(index_135) = index_3,
inference(paramod,[status(thm)],[c_1131,c_2452]) ).
cnf(c_2454,plain,
index_201 = index_3,
inference(paramod,[status(thm)],[c_1243,c_2453]) ).
cnf(c_1632,plain,
index_3 = index_201,
inference(copy,[status(thm)],[c_2454]) ).
cnf(c_1633,plain,
select(earray_278,index_201) = elem_280,
inference(paramod,[status(thm)],[c_1632,c_1626]) ).
cnf(c_2455,plain,
s(index_201) = index_69,
inference(paramod,[status(thm)],[c_1632,c_1021]) ).
cnf(c_2456,plain,
index_249 = index_69,
inference(paramod,[status(thm)],[c_1353,c_2455]) ).
cnf(c_1725,plain,
index_69 = index_249,
inference(copy,[status(thm)],[c_2456]) ).
cnf(c_2457,plain,
s(index_249) = index_135,
inference(paramod,[status(thm)],[c_1725,c_1131]) ).
cnf(c_1738,plain,
index_255 = index_135,
inference(paramod,[status(thm)],[c_1508,c_2457]) ).
cnf(c_2458,plain,
s(index_135) = index_261,
inference(paramod,[status(thm)],[c_1738,c_1518]) ).
cnf(c_2459,plain,
index_201 = index_261,
inference(paramod,[status(thm)],[c_1243,c_2458]) ).
cnf(c_1745,plain,
index_261 = index_201,
inference(copy,[status(thm)],[c_2459]) ).
cnf(c_1747,plain,
s(index_249) = index_135,
inference(paramod,[status(thm)],[c_1738,c_1508]) ).
cnf(c_2460,plain,
s(index_201) = index_267,
inference(paramod,[status(thm)],[c_1745,c_1528]) ).
cnf(c_2461,plain,
index_249 = index_267,
inference(paramod,[status(thm)],[c_1353,c_2460]) ).
cnf(c_1753,plain,
index_267 = index_249,
inference(copy,[status(thm)],[c_2461]) ).
cnf(c_2462,plain,
s(index_249) = index_273,
inference(paramod,[status(thm)],[c_1753,c_1538]) ).
cnf(c_2463,plain,
index_135 = index_273,
inference(paramod,[status(thm)],[c_1747,c_2462]) ).
cnf(c_1760,plain,
index_273 = index_135,
inference(copy,[status(thm)],[c_2463]) ).
cnf(c_2464,plain,
s(index_135) = index_9,
inference(paramod,[status(thm)],[c_1760,c_1548]) ).
cnf(c_2465,plain,
index_201 = index_9,
inference(paramod,[status(thm)],[c_1243,c_2464]) ).
cnf(c_1767,plain,
index_9 = index_201,
inference(copy,[status(thm)],[c_2465]) ).
cnf(c_2466,plain,
s(index_201) = index_15,
inference(paramod,[status(thm)],[c_1767,c_1031]) ).
cnf(c_1777,plain,
index_249 = index_15,
inference(paramod,[status(thm)],[c_1353,c_2466]) ).
cnf(c_2467,plain,
s(index_15) = index_135,
inference(paramod,[status(thm)],[c_1777,c_1747]) ).
cnf(c_1790,plain,
index_21 = index_135,
inference(paramod,[status(thm)],[c_1041,c_2467]) ).
cnf(c_1801,plain,
s(index_201) = index_15,
inference(paramod,[status(thm)],[c_1777,c_1353]) ).
cnf(c_2468,plain,
s(index_135) = index_27,
inference(paramod,[status(thm)],[c_1790,c_1051]) ).
cnf(c_2469,plain,
index_201 = index_27,
inference(paramod,[status(thm)],[c_1243,c_2468]) ).
cnf(c_1807,plain,
index_27 = index_201,
inference(copy,[status(thm)],[c_2469]) ).
cnf(c_1809,plain,
s(index_15) = index_135,
inference(paramod,[status(thm)],[c_1790,c_1041]) ).
cnf(c_2470,plain,
s(index_201) = index_33,
inference(paramod,[status(thm)],[c_1807,c_1061]) ).
cnf(c_2471,plain,
index_15 = index_33,
inference(paramod,[status(thm)],[c_1801,c_2470]) ).
cnf(c_1815,plain,
index_33 = index_15,
inference(copy,[status(thm)],[c_2471]) ).
cnf(c_2472,plain,
s(index_15) = index_39,
inference(paramod,[status(thm)],[c_1815,c_1071]) ).
cnf(c_2473,plain,
index_135 = index_39,
inference(paramod,[status(thm)],[c_1809,c_2472]) ).
cnf(c_1822,plain,
index_39 = index_135,
inference(copy,[status(thm)],[c_2473]) ).
cnf(c_2474,plain,
s(index_135) = index_45,
inference(paramod,[status(thm)],[c_1822,c_1081]) ).
cnf(c_2475,plain,
index_201 = index_45,
inference(paramod,[status(thm)],[c_1243,c_2474]) ).
cnf(c_1829,plain,
index_45 = index_201,
inference(copy,[status(thm)],[c_2475]) ).
cnf(c_2476,plain,
s(index_201) = index_51,
inference(paramod,[status(thm)],[c_1829,c_1091]) ).
cnf(c_2477,plain,
index_15 = index_51,
inference(paramod,[status(thm)],[c_1801,c_2476]) ).
cnf(c_1836,plain,
index_51 = index_15,
inference(copy,[status(thm)],[c_2477]) ).
cnf(c_2478,plain,
s(index_15) = index_57,
inference(paramod,[status(thm)],[c_1836,c_1101]) ).
cnf(c_2479,plain,
index_135 = index_57,
inference(paramod,[status(thm)],[c_1809,c_2478]) ).
cnf(c_1843,plain,
index_57 = index_135,
inference(copy,[status(thm)],[c_2479]) ).
cnf(c_2480,plain,
s(index_135) = index_63,
inference(paramod,[status(thm)],[c_1843,c_1111]) ).
cnf(c_2481,plain,
index_201 = index_63,
inference(paramod,[status(thm)],[c_1243,c_2480]) ).
cnf(c_1850,plain,
index_63 = index_201,
inference(copy,[status(thm)],[c_2481]) ).
cnf(c_2482,plain,
s(index_201) = index_75,
inference(paramod,[status(thm)],[c_1850,c_1121]) ).
cnf(c_2483,plain,
index_15 = index_75,
inference(paramod,[status(thm)],[c_1801,c_2482]) ).
cnf(c_1857,plain,
index_75 = index_15,
inference(copy,[status(thm)],[c_2483]) ).
cnf(c_2484,plain,
s(index_15) = index_81,
inference(paramod,[status(thm)],[c_1857,c_1143]) ).
cnf(c_2485,plain,
index_135 = index_81,
inference(paramod,[status(thm)],[c_1809,c_2484]) ).
cnf(c_1864,plain,
index_81 = index_135,
inference(copy,[status(thm)],[c_2485]) ).
cnf(c_2486,plain,
s(index_135) = index_87,
inference(paramod,[status(thm)],[c_1864,c_1153]) ).
cnf(c_2487,plain,
index_201 = index_87,
inference(paramod,[status(thm)],[c_1243,c_2486]) ).
cnf(c_1871,plain,
index_87 = index_201,
inference(copy,[status(thm)],[c_2487]) ).
cnf(c_2488,plain,
s(index_201) = index_93,
inference(paramod,[status(thm)],[c_1871,c_1163]) ).
cnf(c_2489,plain,
index_15 = index_93,
inference(paramod,[status(thm)],[c_1801,c_2488]) ).
cnf(c_1878,plain,
index_93 = index_15,
inference(copy,[status(thm)],[c_2489]) ).
cnf(c_2490,plain,
s(index_15) = index_99,
inference(paramod,[status(thm)],[c_1878,c_1173]) ).
cnf(c_2491,plain,
index_135 = index_99,
inference(paramod,[status(thm)],[c_1809,c_2490]) ).
cnf(c_1885,plain,
index_99 = index_135,
inference(copy,[status(thm)],[c_2491]) ).
cnf(c_2492,plain,
s(index_135) = index_105,
inference(paramod,[status(thm)],[c_1885,c_1183]) ).
cnf(c_1892,plain,
index_201 = index_105,
inference(paramod,[status(thm)],[c_1243,c_2492]) ).
cnf(c_2493,plain,
s(index_105) = index_15,
inference(paramod,[status(thm)],[c_1892,c_1801]) ).
cnf(c_2494,plain,
index_111 = index_15,
inference(paramod,[status(thm)],[c_1193,c_2493]) ).
cnf(c_1929,plain,
index_15 = index_111,
inference(copy,[status(thm)],[c_2494]) ).
cnf(c_2045,plain,
select(earray_278,index_105) = elem_280,
inference(paramod,[status(thm)],[c_1892,c_1633]) ).
cnf(c_2048,plain,
s(index_135) = index_105,
inference(paramod,[status(thm)],[c_1892,c_1243]) ).
cnf(c_2495,plain,
s(index_111) = index_135,
inference(paramod,[status(thm)],[c_1929,c_1809]) ).
cnf(c_2496,plain,
index_117 = index_135,
inference(paramod,[status(thm)],[c_1203,c_2495]) ).
cnf(c_2082,plain,
index_135 = index_117,
inference(copy,[status(thm)],[c_2496]) ).
cnf(c_2497,plain,
s(index_117) = index_105,
inference(paramod,[status(thm)],[c_2082,c_2048]) ).
cnf(c_2110,plain,
index_123 = index_105,
inference(paramod,[status(thm)],[c_1213,c_2497]) ).
cnf(c_2498,plain,
s(index_105) = index_129,
inference(paramod,[status(thm)],[c_2110,c_1223]) ).
cnf(c_2499,plain,
index_111 = index_129,
inference(paramod,[status(thm)],[c_1193,c_2498]) ).
cnf(c_2168,plain,
index_129 = index_111,
inference(copy,[status(thm)],[c_2499]) ).
cnf(c_2170,plain,
s(index_117) = index_105,
inference(paramod,[status(thm)],[c_2110,c_1213]) ).
cnf(c_2500,plain,
s(index_111) = index_141,
inference(paramod,[status(thm)],[c_2168,c_1233]) ).
cnf(c_2501,plain,
index_117 = index_141,
inference(paramod,[status(thm)],[c_1203,c_2500]) ).
cnf(c_2176,plain,
index_141 = index_117,
inference(copy,[status(thm)],[c_2501]) ).
cnf(c_2502,plain,
s(index_117) = index_147,
inference(paramod,[status(thm)],[c_2176,c_1253]) ).
cnf(c_2503,plain,
index_105 = index_147,
inference(paramod,[status(thm)],[c_2170,c_2502]) ).
cnf(c_2183,plain,
index_147 = index_105,
inference(copy,[status(thm)],[c_2503]) ).
cnf(c_2504,plain,
s(index_105) = index_153,
inference(paramod,[status(thm)],[c_2183,c_1263]) ).
cnf(c_2505,plain,
index_111 = index_153,
inference(paramod,[status(thm)],[c_1193,c_2504]) ).
cnf(c_2190,plain,
index_153 = index_111,
inference(copy,[status(thm)],[c_2505]) ).
cnf(c_2506,plain,
s(index_111) = index_159,
inference(paramod,[status(thm)],[c_2190,c_1273]) ).
cnf(c_2507,plain,
index_117 = index_159,
inference(paramod,[status(thm)],[c_1203,c_2506]) ).
cnf(c_2197,plain,
index_159 = index_117,
inference(copy,[status(thm)],[c_2507]) ).
cnf(c_2508,plain,
s(index_117) = index_165,
inference(paramod,[status(thm)],[c_2197,c_1283]) ).
cnf(c_2509,plain,
index_105 = index_165,
inference(paramod,[status(thm)],[c_2170,c_2508]) ).
cnf(c_2204,plain,
index_165 = index_105,
inference(copy,[status(thm)],[c_2509]) ).
cnf(c_2510,plain,
s(index_105) = index_171,
inference(paramod,[status(thm)],[c_2204,c_1293]) ).
cnf(c_2511,plain,
index_111 = index_171,
inference(paramod,[status(thm)],[c_1193,c_2510]) ).
cnf(c_2211,plain,
index_171 = index_111,
inference(copy,[status(thm)],[c_2511]) ).
cnf(c_2512,plain,
s(index_111) = index_177,
inference(paramod,[status(thm)],[c_2211,c_1303]) ).
cnf(c_2513,plain,
index_117 = index_177,
inference(paramod,[status(thm)],[c_1203,c_2512]) ).
cnf(c_2218,plain,
index_177 = index_117,
inference(copy,[status(thm)],[c_2513]) ).
cnf(c_2514,plain,
s(index_117) = index_183,
inference(paramod,[status(thm)],[c_2218,c_1313]) ).
cnf(c_2515,plain,
index_105 = index_183,
inference(paramod,[status(thm)],[c_2170,c_2514]) ).
cnf(c_2225,plain,
index_183 = index_105,
inference(copy,[status(thm)],[c_2515]) ).
cnf(c_2516,plain,
s(index_105) = index_189,
inference(paramod,[status(thm)],[c_2225,c_1323]) ).
cnf(c_2517,plain,
index_111 = index_189,
inference(paramod,[status(thm)],[c_1193,c_2516]) ).
cnf(c_2232,plain,
index_189 = index_111,
inference(copy,[status(thm)],[c_2517]) ).
cnf(c_2518,plain,
s(index_111) = index_195,
inference(paramod,[status(thm)],[c_2232,c_1333]) ).
cnf(c_2519,plain,
index_117 = index_195,
inference(paramod,[status(thm)],[c_1203,c_2518]) ).
cnf(c_2239,plain,
index_195 = index_117,
inference(copy,[status(thm)],[c_2519]) ).
cnf(c_2520,plain,
s(index_117) = index_207,
inference(paramod,[status(thm)],[c_2239,c_1343]) ).
cnf(c_2521,plain,
index_105 = index_207,
inference(paramod,[status(thm)],[c_2170,c_2520]) ).
cnf(c_2246,plain,
index_207 = index_105,
inference(copy,[status(thm)],[c_2521]) ).
cnf(c_2522,plain,
s(index_105) = index_213,
inference(paramod,[status(thm)],[c_2246,c_1363]) ).
cnf(c_2523,plain,
index_111 = index_213,
inference(paramod,[status(thm)],[c_1193,c_2522]) ).
cnf(c_2253,plain,
index_213 = index_111,
inference(copy,[status(thm)],[c_2523]) ).
cnf(c_2524,plain,
s(index_111) = index_219,
inference(paramod,[status(thm)],[c_2253,c_1373]) ).
cnf(c_2525,plain,
index_117 = index_219,
inference(paramod,[status(thm)],[c_1203,c_2524]) ).
cnf(c_2260,plain,
index_219 = index_117,
inference(copy,[status(thm)],[c_2525]) ).
cnf(c_2526,plain,
s(index_117) = index_225,
inference(paramod,[status(thm)],[c_2260,c_1383]) ).
cnf(c_2527,plain,
index_105 = index_225,
inference(paramod,[status(thm)],[c_2170,c_2526]) ).
cnf(c_2267,plain,
index_225 = index_105,
inference(copy,[status(thm)],[c_2527]) ).
cnf(c_2528,plain,
s(index_105) = index_231,
inference(paramod,[status(thm)],[c_2267,c_1393]) ).
cnf(c_2529,plain,
index_111 = index_231,
inference(paramod,[status(thm)],[c_1193,c_2528]) ).
cnf(c_2274,plain,
index_231 = index_111,
inference(copy,[status(thm)],[c_2529]) ).
cnf(c_2530,plain,
s(index_111) = index_237,
inference(paramod,[status(thm)],[c_2274,c_1403]) ).
cnf(c_2531,plain,
index_117 = index_237,
inference(paramod,[status(thm)],[c_1203,c_2530]) ).
cnf(c_2281,plain,
index_237 = index_117,
inference(copy,[status(thm)],[c_2531]) ).
cnf(c_2532,plain,
s(index_117) = index_243,
inference(paramod,[status(thm)],[c_2281,c_1413]) ).
cnf(c_2533,plain,
index_105 = index_243,
inference(paramod,[status(thm)],[c_2170,c_2532]) ).
cnf(c_2290,plain,
index_243 = index_105,
inference(copy,[status(thm)],[c_2533]) ).
cnf(c_2534,plain,
select(earray_278,index_105) = e45,
inference(paramod,[status(thm)],[c_2290,c_1425]) ).
cnf(c_2535,plain,
elem_280 = e45,
inference(paramod,[status(thm)],[c_2045,c_2534]) ).
cnf(c_2297,plain,
$false,
inference(resolve,[status(thm)],[c_1501,c_2535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 14:30:59 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 789280 was started by sandbox2 on n011,
% 0.10/0.37 % Sat Sep 26 14:30:59 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 3.38/0.88
% 3.38/0.88 % given #500 (W,wt=8): 1513 earray_260 = earray_256. [para(723(a,1),7(a,1,1)),rewrite([138(2),957(3)])].
% 3.38/0.88
% 3.38/0.88 % SZS status Unsatisfiable for theBenchmark
% 3.38/0.88
% 3.38/0.88 % Proof 1 at 0.36 (+ 0.10) seconds.
% 3.38/0.88 % Length of proof is 832.
% 3.38/0.88 % Level of proof is 79.
% 3.38/0.88 % Maximum clause weight is 30.000.
% 3.38/0.88 % Given clauses 622.
% 3.38/0.88
% 3.38/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------