%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:48 PM UTC 2026
% Result : Unsatisfiable 6.30s 1.71s
% Output : CNFRefutation 6.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 253
% Syntax : Number of formulae : 1131 (1131 unt; 0 def)
% Number of atoms : 1131 (1130 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 298 ( 298 usr; 289 con; 0-2 aty)
% Number of variables : 40 ( 0 sgn 40 !; 0 ?; 17 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : rselect_seq(rstore_seq(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_seq) ).
fof(f4,axiom,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_head) ).
fof(f5,axiom,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_tail) ).
fof(f7,axiom,
! [X0,X1] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_seq_tail) ).
fof(f8,plain,
! [X0,X1] : rselect_seq(X0) = rselect_seq(rstore_tail(X0,X1)),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_tail) ).
fof(f10,axiom,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_seq) ).
fof(f11,plain,
! [X0,X1] : rselect_head(X0) = rselect_head(rstore_seq(X0,X1)),
inference(reorient_equations,[],[f10]) ).
fof(f13,axiom,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_tail_head) ).
fof(f14,plain,
! [X0,X1] : rselect_tail(X0) = rselect_tail(rstore_head(X0,X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : p(s(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ps) ).
fof(f16,axiom,
! [X0] : s(p(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sp) ).
fof(f19,axiom,
! [X0] : s(s(s(X0))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circular) ).
fof(f32,axiom,
earray_134 = rselect_seq(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f86,axiom,
earray_278 = rselect_seq(q46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f105,axiom,
earray_8 = rselect_seq(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp85) ).
fof(f112,axiom,
earray_98 = rselect_seq(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
fof(f113,axiom,
elem_280 = select(earray_278,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f114,axiom,
elem_283 = select(earray_278,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f115,axiom,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f116,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f117,axiom,
index_105 = rselect_tail(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f118,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f119,axiom,
index_111 = rselect_tail(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f120,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f121,axiom,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f122,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f123,axiom,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f124,axiom,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f125,axiom,
index_126 = s(index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f126,axiom,
index_129 = rselect_tail(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f127,axiom,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f128,axiom,
index_135 = rselect_tail(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f129,axiom,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f130,axiom,
index_141 = rselect_tail(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f131,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f132,axiom,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f133,axiom,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f134,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f135,axiom,
index_153 = rselect_tail(q31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f136,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f137,axiom,
index_159 = rselect_tail(q32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f138,axiom,
index_162 = s(index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f139,axiom,
index_165 = rselect_tail(q33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f140,axiom,
index_168 = s(index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f141,axiom,
index_171 = rselect_tail(q34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f142,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f143,axiom,
index_177 = rselect_tail(q35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f144,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f145,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f146,axiom,
index_183 = rselect_tail(q36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f147,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f148,axiom,
index_189 = rselect_tail(q37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f149,axiom,
index_192 = s(index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f150,axiom,
index_195 = rselect_tail(q38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f151,axiom,
index_198 = s(index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f152,axiom,
index_201 = rselect_tail(q3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f153,axiom,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f154,axiom,
index_207 = rselect_tail(q39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f155,axiom,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f156,axiom,
index_210 = s(index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f157,axiom,
index_213 = rselect_tail(q40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f158,axiom,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f159,axiom,
index_219 = rselect_tail(q41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f160,axiom,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f161,axiom,
index_225 = rselect_tail(q42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f162,axiom,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f163,axiom,
index_231 = rselect_tail(q43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f164,axiom,
index_234 = s(index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f165,axiom,
index_237 = rselect_tail(q44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f166,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f167,axiom,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f168,axiom,
index_243 = rselect_tail(q45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f169,axiom,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f170,axiom,
index_249 = rselect_tail(q4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f171,axiom,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f172,axiom,
index_255 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f173,axiom,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f174,axiom,
index_261 = rselect_tail(q6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f175,axiom,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f176,axiom,
index_267 = rselect_tail(q7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f177,axiom,
index_27 = rselect_tail(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f178,axiom,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f179,axiom,
index_273 = rselect_tail(q8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f180,axiom,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f181,axiom,
index_279 = rselect_head(q46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f182,axiom,
index_281 = rselect_tail(q46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f183,axiom,
s(index_282) = index_281,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f184,plain,
index_281 = s(index_282),
inference(reorient_equations,[],[f183]) ).
fof(f185,axiom,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f186,axiom,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f187,axiom,
index_33 = rselect_tail(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f188,axiom,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f189,axiom,
index_39 = rselect_tail(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f190,axiom,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f191,axiom,
index_45 = rselect_tail(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f192,axiom,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f193,axiom,
index_51 = rselect_tail(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f194,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f195,axiom,
index_57 = rselect_tail(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f196,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f197,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f198,axiom,
index_63 = rselect_tail(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f199,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f200,axiom,
index_69 = rselect_tail(q1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f201,axiom,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f202,axiom,
index_75 = rselect_tail(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f203,axiom,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f204,axiom,
index_81 = rselect_tail(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f205,axiom,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f206,axiom,
index_87 = rselect_tail(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f207,axiom,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f208,axiom,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f209,axiom,
index_93 = rselect_tail(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f210,axiom,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f211,axiom,
index_99 = rselect_tail(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f212,axiom,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f213,axiom,
queue_101 = rstore_seq(q23,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f214,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f215,axiom,
queue_107 = rstore_seq(q24,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f216,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f217,axiom,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f218,axiom,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f219,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f220,axiom,
queue_119 = rstore_seq(q26,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f221,axiom,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f222,axiom,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f223,axiom,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f224,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f225,axiom,
queue_131 = rstore_seq(q28,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f226,axiom,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f227,axiom,
queue_137 = rstore_seq(q2,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f228,axiom,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f229,axiom,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f230,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f231,axiom,
queue_149 = rstore_seq(q30,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f232,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f233,axiom,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f234,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f235,axiom,
queue_161 = rstore_seq(q32,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f236,axiom,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f237,axiom,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f238,axiom,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f239,axiom,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f240,axiom,
queue_173 = rstore_seq(q34,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f241,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f242,axiom,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f243,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f244,axiom,
queue_185 = rstore_seq(q36,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f245,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f246,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f247,axiom,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f248,axiom,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f249,axiom,
queue_197 = rstore_seq(q38,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f250,axiom,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f251,axiom,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f252,axiom,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f253,axiom,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f254,axiom,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f255,axiom,
queue_215 = rstore_seq(q40,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f256,axiom,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f257,axiom,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f258,axiom,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f259,axiom,
queue_227 = rstore_seq(q42,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f260,axiom,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f261,axiom,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f262,axiom,
queue_233 = rstore_seq(q43,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f263,axiom,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f264,axiom,
queue_239 = rstore_seq(q44,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f265,axiom,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f266,axiom,
queue_245 = rstore_seq(q45,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f267,axiom,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f268,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f269,axiom,
queue_251 = rstore_seq(q4,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f270,axiom,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f271,axiom,
queue_257 = rstore_seq(q5,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f272,axiom,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f273,axiom,
queue_263 = rstore_seq(q6,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f274,axiom,
queue_265 = rstore_tail(queue_263,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f275,axiom,
queue_269 = rstore_seq(q7,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f276,axiom,
queue_271 = rstore_tail(queue_269,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f277,axiom,
queue_275 = rstore_seq(q8,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f278,axiom,
queue_277 = rstore_tail(queue_275,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f279,axiom,
queue_29 = rstore_seq(q12,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f280,axiom,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f281,axiom,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f282,axiom,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f283,axiom,
queue_41 = rstore_seq(q14,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f284,axiom,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f285,axiom,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f286,axiom,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f287,axiom,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp266) ).
fof(f288,axiom,
queue_53 = rstore_seq(q16,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f289,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f290,axiom,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f291,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f292,axiom,
queue_65 = rstore_seq(q18,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f293,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f294,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f295,axiom,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f296,axiom,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f297,axiom,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f298,axiom,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f299,axiom,
queue_83 = rstore_seq(q20,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f300,axiom,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f301,axiom,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f302,axiom,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f303,axiom,
queue_95 = rstore_seq(q22,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f304,axiom,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f305,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f306,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f307,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f308,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f309,axiom,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f310,axiom,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f311,axiom,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f312,axiom,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f313,axiom,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f314,axiom,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f315,axiom,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f316,axiom,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f317,axiom,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f318,axiom,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f319,axiom,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f320,axiom,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f321,axiom,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f322,axiom,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f323,axiom,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f324,axiom,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f325,axiom,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f326,axiom,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f327,axiom,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f328,axiom,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f329,axiom,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f330,axiom,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f331,axiom,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f332,axiom,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f333,axiom,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f334,axiom,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f335,axiom,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f336,axiom,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f337,axiom,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f338,axiom,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f339,axiom,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f340,axiom,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f341,axiom,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f342,axiom,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f343,axiom,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f344,axiom,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f345,axiom,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f346,axiom,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp325) ).
fof(f347,axiom,
q5 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp326) ).
fof(f348,axiom,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp327) ).
fof(f349,axiom,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp328) ).
fof(f350,axiom,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp329) ).
fof(f351,axiom,
q9 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp330) ).
fof(f352,negated_conjecture,
elem_280 != elem_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f358,plain,
earray_134 = rselect_seq(queue_73),
inference(definition_unfolding,[],[f32,f317]) ).
fof(f386,plain,
earray_278 = rselect_seq(queue_247),
inference(definition_unfolding,[],[f86,f346]) ).
fof(f395,plain,
earray_8 = rselect_seq(queue_277),
inference(definition_unfolding,[],[f105,f351]) ).
fof(f399,plain,
earray_98 = rselect_seq(queue_97),
inference(definition_unfolding,[],[f112,f321]) ).
fof(f400,plain,
index_105 = rselect_tail(queue_103),
inference(definition_unfolding,[],[f117,f322]) ).
fof(f401,plain,
index_111 = rselect_tail(queue_109),
inference(definition_unfolding,[],[f119,f323]) ).
fof(f402,plain,
index_117 = rselect_tail(queue_115),
inference(definition_unfolding,[],[f121,f324]) ).
fof(f403,plain,
index_123 = rselect_tail(queue_121),
inference(definition_unfolding,[],[f124,f325]) ).
fof(f404,plain,
index_129 = rselect_tail(queue_127),
inference(definition_unfolding,[],[f126,f326]) ).
fof(f405,plain,
index_135 = rselect_tail(queue_73),
inference(definition_unfolding,[],[f128,f317]) ).
fof(f406,plain,
index_141 = rselect_tail(queue_133),
inference(definition_unfolding,[],[f130,f327]) ).
fof(f407,plain,
index_147 = rselect_tail(queue_145),
inference(definition_unfolding,[],[f132,f329]) ).
fof(f408,plain,
index_15 = rselect_tail(queue_13),
inference(definition_unfolding,[],[f133,f307]) ).
fof(f409,plain,
index_153 = rselect_tail(queue_151),
inference(definition_unfolding,[],[f135,f330]) ).
fof(f410,plain,
index_159 = rselect_tail(queue_157),
inference(definition_unfolding,[],[f137,f331]) ).
fof(f411,plain,
index_165 = rselect_tail(queue_163),
inference(definition_unfolding,[],[f139,f332]) ).
fof(f412,plain,
index_171 = rselect_tail(queue_169),
inference(definition_unfolding,[],[f141,f333]) ).
fof(f413,plain,
index_177 = rselect_tail(queue_175),
inference(definition_unfolding,[],[f143,f334]) ).
fof(f414,plain,
index_183 = rselect_tail(queue_181),
inference(definition_unfolding,[],[f146,f335]) ).
fof(f415,plain,
index_189 = rselect_tail(queue_187),
inference(definition_unfolding,[],[f148,f336]) ).
fof(f416,plain,
index_195 = rselect_tail(queue_193),
inference(definition_unfolding,[],[f150,f337]) ).
fof(f417,plain,
index_201 = rselect_tail(queue_139),
inference(definition_unfolding,[],[f152,f328]) ).
fof(f418,plain,
index_207 = rselect_tail(queue_199),
inference(definition_unfolding,[],[f154,f338]) ).
fof(f419,plain,
index_21 = rselect_tail(queue_19),
inference(definition_unfolding,[],[f155,f308]) ).
fof(f420,plain,
index_213 = rselect_tail(queue_211),
inference(definition_unfolding,[],[f157,f340]) ).
fof(f421,plain,
index_219 = rselect_tail(queue_217),
inference(definition_unfolding,[],[f159,f341]) ).
fof(f422,plain,
index_225 = rselect_tail(queue_223),
inference(definition_unfolding,[],[f161,f342]) ).
fof(f423,plain,
index_231 = rselect_tail(queue_229),
inference(definition_unfolding,[],[f163,f343]) ).
fof(f424,plain,
index_237 = rselect_tail(queue_235),
inference(definition_unfolding,[],[f165,f344]) ).
fof(f425,plain,
index_243 = rselect_tail(queue_241),
inference(definition_unfolding,[],[f168,f345]) ).
fof(f426,plain,
index_249 = rselect_tail(queue_205),
inference(definition_unfolding,[],[f170,f339]) ).
fof(f427,plain,
index_255 = rselect_tail(queue_253),
inference(definition_unfolding,[],[f172,f347]) ).
fof(f428,plain,
index_261 = rselect_tail(queue_259),
inference(definition_unfolding,[],[f174,f348]) ).
fof(f429,plain,
index_267 = rselect_tail(queue_265),
inference(definition_unfolding,[],[f176,f349]) ).
fof(f430,plain,
index_27 = rselect_tail(queue_25),
inference(definition_unfolding,[],[f177,f309]) ).
fof(f431,plain,
index_273 = rselect_tail(queue_271),
inference(definition_unfolding,[],[f179,f350]) ).
fof(f432,plain,
index_279 = rselect_head(queue_247),
inference(definition_unfolding,[],[f181,f346]) ).
fof(f433,plain,
index_281 = rselect_tail(queue_247),
inference(definition_unfolding,[],[f182,f346]) ).
fof(f434,plain,
index_3 = rselect_tail(queue_1),
inference(definition_unfolding,[],[f185,f305]) ).
fof(f435,plain,
index_33 = rselect_tail(queue_31),
inference(definition_unfolding,[],[f187,f310]) ).
fof(f436,plain,
index_39 = rselect_tail(queue_37),
inference(definition_unfolding,[],[f189,f311]) ).
fof(f437,plain,
index_45 = rselect_tail(queue_43),
inference(definition_unfolding,[],[f191,f312]) ).
fof(f438,plain,
index_51 = rselect_tail(queue_49),
inference(definition_unfolding,[],[f193,f313]) ).
fof(f439,plain,
index_57 = rselect_tail(queue_55),
inference(definition_unfolding,[],[f195,f314]) ).
fof(f440,plain,
index_63 = rselect_tail(queue_61),
inference(definition_unfolding,[],[f198,f315]) ).
fof(f441,plain,
index_69 = rselect_tail(queue_7),
inference(definition_unfolding,[],[f200,f306]) ).
fof(f442,plain,
index_75 = rselect_tail(queue_67),
inference(definition_unfolding,[],[f202,f316]) ).
fof(f443,plain,
index_81 = rselect_tail(queue_79),
inference(definition_unfolding,[],[f204,f318]) ).
fof(f444,plain,
index_87 = rselect_tail(queue_85),
inference(definition_unfolding,[],[f206,f319]) ).
fof(f445,plain,
index_9 = rselect_tail(queue_277),
inference(definition_unfolding,[],[f207,f351]) ).
fof(f446,plain,
index_93 = rselect_tail(queue_91),
inference(definition_unfolding,[],[f209,f320]) ).
fof(f447,plain,
index_99 = rselect_tail(queue_97),
inference(definition_unfolding,[],[f211,f321]) ).
fof(f448,plain,
queue_101 = rstore_seq(queue_97,earray_100),
inference(definition_unfolding,[],[f213,f321]) ).
fof(f449,plain,
queue_107 = rstore_seq(queue_103,earray_106),
inference(definition_unfolding,[],[f215,f322]) ).
fof(f450,plain,
queue_11 = rstore_seq(queue_277,earray_10),
inference(definition_unfolding,[],[f217,f351]) ).
fof(f451,plain,
queue_113 = rstore_seq(queue_109,earray_112),
inference(definition_unfolding,[],[f218,f323]) ).
fof(f452,plain,
queue_119 = rstore_seq(queue_115,earray_118),
inference(definition_unfolding,[],[f220,f324]) ).
fof(f453,plain,
queue_125 = rstore_seq(queue_121,earray_124),
inference(definition_unfolding,[],[f222,f325]) ).
fof(f454,plain,
queue_131 = rstore_seq(queue_127,earray_130),
inference(definition_unfolding,[],[f225,f326]) ).
fof(f455,plain,
queue_137 = rstore_seq(queue_73,earray_136),
inference(definition_unfolding,[],[f227,f317]) ).
fof(f456,plain,
queue_143 = rstore_seq(queue_133,earray_142),
inference(definition_unfolding,[],[f229,f327]) ).
fof(f457,plain,
queue_149 = rstore_seq(queue_145,earray_148),
inference(definition_unfolding,[],[f231,f329]) ).
fof(f458,plain,
queue_155 = rstore_seq(queue_151,earray_154),
inference(definition_unfolding,[],[f233,f330]) ).
fof(f459,plain,
queue_161 = rstore_seq(queue_157,earray_160),
inference(definition_unfolding,[],[f235,f331]) ).
fof(f460,plain,
queue_167 = rstore_seq(queue_163,earray_166),
inference(definition_unfolding,[],[f237,f332]) ).
fof(f461,plain,
queue_17 = rstore_seq(queue_13,earray_16),
inference(definition_unfolding,[],[f239,f307]) ).
fof(f462,plain,
queue_173 = rstore_seq(queue_169,earray_172),
inference(definition_unfolding,[],[f240,f333]) ).
fof(f463,plain,
queue_179 = rstore_seq(queue_175,earray_178),
inference(definition_unfolding,[],[f242,f334]) ).
fof(f464,plain,
queue_185 = rstore_seq(queue_181,earray_184),
inference(definition_unfolding,[],[f244,f335]) ).
fof(f465,plain,
queue_191 = rstore_seq(queue_187,earray_190),
inference(definition_unfolding,[],[f247,f336]) ).
fof(f466,plain,
queue_197 = rstore_seq(queue_193,earray_196),
inference(definition_unfolding,[],[f249,f337]) ).
fof(f467,plain,
queue_203 = rstore_seq(queue_139,earray_202),
inference(definition_unfolding,[],[f251,f328]) ).
fof(f468,plain,
queue_209 = rstore_seq(queue_199,earray_208),
inference(definition_unfolding,[],[f253,f338]) ).
fof(f469,plain,
queue_215 = rstore_seq(queue_211,earray_214),
inference(definition_unfolding,[],[f255,f340]) ).
fof(f470,plain,
queue_221 = rstore_seq(queue_217,earray_220),
inference(definition_unfolding,[],[f257,f341]) ).
fof(f471,plain,
queue_227 = rstore_seq(queue_223,earray_226),
inference(definition_unfolding,[],[f259,f342]) ).
fof(f472,plain,
queue_23 = rstore_seq(queue_19,earray_22),
inference(definition_unfolding,[],[f261,f308]) ).
fof(f473,plain,
queue_233 = rstore_seq(queue_229,earray_232),
inference(definition_unfolding,[],[f262,f343]) ).
fof(f474,plain,
queue_239 = rstore_seq(queue_235,earray_238),
inference(definition_unfolding,[],[f264,f344]) ).
fof(f475,plain,
queue_245 = rstore_seq(queue_241,earray_244),
inference(definition_unfolding,[],[f266,f345]) ).
fof(f476,plain,
queue_251 = rstore_seq(queue_205,earray_250),
inference(definition_unfolding,[],[f269,f339]) ).
fof(f477,plain,
queue_257 = rstore_seq(queue_253,earray_256),
inference(definition_unfolding,[],[f271,f347]) ).
fof(f478,plain,
queue_263 = rstore_seq(queue_259,earray_262),
inference(definition_unfolding,[],[f273,f348]) ).
fof(f479,plain,
queue_269 = rstore_seq(queue_265,earray_268),
inference(definition_unfolding,[],[f275,f349]) ).
fof(f480,plain,
queue_275 = rstore_seq(queue_271,earray_274),
inference(definition_unfolding,[],[f277,f350]) ).
fof(f481,plain,
queue_29 = rstore_seq(queue_25,earray_28),
inference(definition_unfolding,[],[f279,f309]) ).
fof(f482,plain,
queue_35 = rstore_seq(queue_31,earray_34),
inference(definition_unfolding,[],[f281,f310]) ).
fof(f483,plain,
queue_41 = rstore_seq(queue_37,earray_40),
inference(definition_unfolding,[],[f283,f311]) ).
fof(f484,plain,
queue_47 = rstore_seq(queue_43,earray_46),
inference(definition_unfolding,[],[f285,f312]) ).
fof(f485,plain,
queue_5 = rstore_seq(queue_1,earray_4),
inference(definition_unfolding,[],[f287,f305]) ).
fof(f486,plain,
queue_53 = rstore_seq(queue_49,earray_52),
inference(definition_unfolding,[],[f288,f313]) ).
fof(f487,plain,
queue_59 = rstore_seq(queue_55,earray_58),
inference(definition_unfolding,[],[f290,f314]) ).
fof(f488,plain,
queue_65 = rstore_seq(queue_61,earray_64),
inference(definition_unfolding,[],[f292,f315]) ).
fof(f489,plain,
queue_71 = rstore_seq(queue_7,earray_70),
inference(definition_unfolding,[],[f295,f306]) ).
fof(f490,plain,
queue_77 = rstore_seq(queue_67,earray_76),
inference(definition_unfolding,[],[f297,f316]) ).
fof(f491,plain,
queue_83 = rstore_seq(queue_79,earray_82),
inference(definition_unfolding,[],[f299,f318]) ).
fof(f492,plain,
queue_89 = rstore_seq(queue_85,earray_88),
inference(definition_unfolding,[],[f301,f319]) ).
fof(f493,plain,
queue_95 = rstore_seq(queue_91,earray_94),
inference(definition_unfolding,[],[f303,f320]) ).
tcf(c_399,plain,
! [X0: $i,X1: $i] : rselect_seq(rstore_seq(X0,X1)) = X1,
inference(cnf_transformation,[],[f3]) ).
tcf(c_400,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[],[f4]) ).
tcf(c_401,plain,
! [X0: $i,X1: $i] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[],[f5]) ).
tcf(c_403,plain,
! [X0: $i,X1: $i] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_404,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[],[f9]) ).
tcf(c_405,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[],[f11]) ).
tcf(c_407,plain,
! [X0: $i,X1: $i] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[],[f14]) ).
tcf(c_408,plain,
! [X0: $i] : p(s(X0)) = X0,
inference(cnf_transformation,[],[f15]) ).
tcf(c_409,plain,
! [X0: $i] : s(p(X0)) = X0,
inference(cnf_transformation,[],[f16]) ).
tcf(c_412,plain,
! [X0: $i] : s(s(s(X0))) = X0,
inference(cnf_transformation,[],[f19]) ).
tcf(c_425,plain,
rselect_seq(queue_73) = earray_134,
inference(cnf_transformation,[],[f358]) ).
tcf(c_479,plain,
rselect_seq(queue_247) = earray_278,
inference(cnf_transformation,[],[f386]) ).
tcf(c_498,plain,
rselect_seq(queue_277) = earray_8,
inference(cnf_transformation,[],[f395]) ).
tcf(c_505,plain,
rselect_seq(queue_97) = earray_98,
inference(cnf_transformation,[],[f399]) ).
tcf(c_506,plain,
select(earray_278,index_279) = elem_280,
inference(cnf_transformation,[],[f113]) ).
tcf(c_507,plain,
select(earray_278,index_282) = elem_283,
inference(cnf_transformation,[],[f114]) ).
tcf(c_508,plain,
rselect_tail(q) = index_0,
inference(cnf_transformation,[],[f115]) ).
tcf(c_509,plain,
s(index_99) = index_102,
inference(cnf_transformation,[],[f116]) ).
tcf(c_510,plain,
rselect_tail(queue_103) = index_105,
inference(cnf_transformation,[],[f400]) ).
tcf(c_511,plain,
s(index_105) = index_108,
inference(cnf_transformation,[],[f118]) ).
tcf(c_512,plain,
rselect_tail(queue_109) = index_111,
inference(cnf_transformation,[],[f401]) ).
tcf(c_513,plain,
s(index_111) = index_114,
inference(cnf_transformation,[],[f120]) ).
tcf(c_514,plain,
rselect_tail(queue_115) = index_117,
inference(cnf_transformation,[],[f402]) ).
tcf(c_515,plain,
s(index_9) = index_12,
inference(cnf_transformation,[],[f122]) ).
tcf(c_516,plain,
s(index_117) = index_120,
inference(cnf_transformation,[],[f123]) ).
tcf(c_517,plain,
rselect_tail(queue_121) = index_123,
inference(cnf_transformation,[],[f403]) ).
tcf(c_518,plain,
s(index_123) = index_126,
inference(cnf_transformation,[],[f125]) ).
tcf(c_519,plain,
rselect_tail(queue_127) = index_129,
inference(cnf_transformation,[],[f404]) ).
tcf(c_520,plain,
s(index_129) = index_132,
inference(cnf_transformation,[],[f127]) ).
tcf(c_521,plain,
rselect_tail(queue_73) = index_135,
inference(cnf_transformation,[],[f405]) ).
tcf(c_522,plain,
s(index_135) = index_138,
inference(cnf_transformation,[],[f129]) ).
tcf(c_523,plain,
rselect_tail(queue_133) = index_141,
inference(cnf_transformation,[],[f406]) ).
tcf(c_524,plain,
s(index_141) = index_144,
inference(cnf_transformation,[],[f131]) ).
tcf(c_525,plain,
rselect_tail(queue_145) = index_147,
inference(cnf_transformation,[],[f407]) ).
tcf(c_526,plain,
rselect_tail(queue_13) = index_15,
inference(cnf_transformation,[],[f408]) ).
tcf(c_527,plain,
s(index_147) = index_150,
inference(cnf_transformation,[],[f134]) ).
tcf(c_528,plain,
rselect_tail(queue_151) = index_153,
inference(cnf_transformation,[],[f409]) ).
tcf(c_529,plain,
s(index_153) = index_156,
inference(cnf_transformation,[],[f136]) ).
tcf(c_530,plain,
rselect_tail(queue_157) = index_159,
inference(cnf_transformation,[],[f410]) ).
tcf(c_531,plain,
s(index_159) = index_162,
inference(cnf_transformation,[],[f138]) ).
tcf(c_532,plain,
rselect_tail(queue_163) = index_165,
inference(cnf_transformation,[],[f411]) ).
tcf(c_533,plain,
s(index_165) = index_168,
inference(cnf_transformation,[],[f140]) ).
tcf(c_534,plain,
rselect_tail(queue_169) = index_171,
inference(cnf_transformation,[],[f412]) ).
tcf(c_535,plain,
s(index_171) = index_174,
inference(cnf_transformation,[],[f142]) ).
tcf(c_536,plain,
rselect_tail(queue_175) = index_177,
inference(cnf_transformation,[],[f413]) ).
tcf(c_537,plain,
s(index_15) = index_18,
inference(cnf_transformation,[],[f144]) ).
tcf(c_538,plain,
s(index_177) = index_180,
inference(cnf_transformation,[],[f145]) ).
tcf(c_539,plain,
rselect_tail(queue_181) = index_183,
inference(cnf_transformation,[],[f414]) ).
tcf(c_540,plain,
s(index_183) = index_186,
inference(cnf_transformation,[],[f147]) ).
tcf(c_541,plain,
rselect_tail(queue_187) = index_189,
inference(cnf_transformation,[],[f415]) ).
tcf(c_542,plain,
s(index_189) = index_192,
inference(cnf_transformation,[],[f149]) ).
tcf(c_543,plain,
rselect_tail(queue_193) = index_195,
inference(cnf_transformation,[],[f416]) ).
tcf(c_544,plain,
s(index_195) = index_198,
inference(cnf_transformation,[],[f151]) ).
tcf(c_545,plain,
rselect_tail(queue_139) = index_201,
inference(cnf_transformation,[],[f417]) ).
tcf(c_546,plain,
s(index_201) = index_204,
inference(cnf_transformation,[],[f153]) ).
tcf(c_547,plain,
rselect_tail(queue_199) = index_207,
inference(cnf_transformation,[],[f418]) ).
tcf(c_548,plain,
rselect_tail(queue_19) = index_21,
inference(cnf_transformation,[],[f419]) ).
tcf(c_549,plain,
s(index_207) = index_210,
inference(cnf_transformation,[],[f156]) ).
tcf(c_550,plain,
rselect_tail(queue_211) = index_213,
inference(cnf_transformation,[],[f420]) ).
tcf(c_551,plain,
s(index_213) = index_216,
inference(cnf_transformation,[],[f158]) ).
tcf(c_552,plain,
rselect_tail(queue_217) = index_219,
inference(cnf_transformation,[],[f421]) ).
tcf(c_553,plain,
s(index_219) = index_222,
inference(cnf_transformation,[],[f160]) ).
tcf(c_554,plain,
rselect_tail(queue_223) = index_225,
inference(cnf_transformation,[],[f422]) ).
tcf(c_555,plain,
s(index_225) = index_228,
inference(cnf_transformation,[],[f162]) ).
tcf(c_556,plain,
rselect_tail(queue_229) = index_231,
inference(cnf_transformation,[],[f423]) ).
tcf(c_557,plain,
s(index_231) = index_234,
inference(cnf_transformation,[],[f164]) ).
tcf(c_558,plain,
rselect_tail(queue_235) = index_237,
inference(cnf_transformation,[],[f424]) ).
tcf(c_559,plain,
s(index_21) = index_24,
inference(cnf_transformation,[],[f166]) ).
tcf(c_560,plain,
s(index_237) = index_240,
inference(cnf_transformation,[],[f167]) ).
tcf(c_561,plain,
rselect_tail(queue_241) = index_243,
inference(cnf_transformation,[],[f425]) ).
tcf(c_562,plain,
s(index_243) = index_246,
inference(cnf_transformation,[],[f169]) ).
tcf(c_563,plain,
rselect_tail(queue_205) = index_249,
inference(cnf_transformation,[],[f426]) ).
tcf(c_564,plain,
s(index_249) = index_252,
inference(cnf_transformation,[],[f171]) ).
tcf(c_565,plain,
rselect_tail(queue_253) = index_255,
inference(cnf_transformation,[],[f427]) ).
tcf(c_566,plain,
s(index_255) = index_258,
inference(cnf_transformation,[],[f173]) ).
tcf(c_567,plain,
rselect_tail(queue_259) = index_261,
inference(cnf_transformation,[],[f428]) ).
tcf(c_568,plain,
s(index_261) = index_264,
inference(cnf_transformation,[],[f175]) ).
tcf(c_569,plain,
rselect_tail(queue_265) = index_267,
inference(cnf_transformation,[],[f429]) ).
tcf(c_570,plain,
rselect_tail(queue_25) = index_27,
inference(cnf_transformation,[],[f430]) ).
tcf(c_571,plain,
s(index_267) = index_270,
inference(cnf_transformation,[],[f178]) ).
tcf(c_572,plain,
rselect_tail(queue_271) = index_273,
inference(cnf_transformation,[],[f431]) ).
tcf(c_573,plain,
s(index_273) = index_276,
inference(cnf_transformation,[],[f180]) ).
tcf(c_574,plain,
rselect_head(queue_247) = index_279,
inference(cnf_transformation,[],[f432]) ).
tcf(c_575,plain,
rselect_tail(queue_247) = index_281,
inference(cnf_transformation,[],[f433]) ).
tcf(c_576,plain,
s(index_282) = index_281,
inference(cnf_transformation,[],[f184]) ).
tcf(c_577,plain,
rselect_tail(queue_1) = index_3,
inference(cnf_transformation,[],[f434]) ).
tcf(c_578,plain,
s(index_27) = index_30,
inference(cnf_transformation,[],[f186]) ).
tcf(c_579,plain,
rselect_tail(queue_31) = index_33,
inference(cnf_transformation,[],[f435]) ).
tcf(c_580,plain,
s(index_33) = index_36,
inference(cnf_transformation,[],[f188]) ).
tcf(c_581,plain,
rselect_tail(queue_37) = index_39,
inference(cnf_transformation,[],[f436]) ).
tcf(c_582,plain,
s(index_39) = index_42,
inference(cnf_transformation,[],[f190]) ).
tcf(c_583,plain,
rselect_tail(queue_43) = index_45,
inference(cnf_transformation,[],[f437]) ).
tcf(c_584,plain,
s(index_45) = index_48,
inference(cnf_transformation,[],[f192]) ).
tcf(c_585,plain,
rselect_tail(queue_49) = index_51,
inference(cnf_transformation,[],[f438]) ).
tcf(c_586,plain,
s(index_51) = index_54,
inference(cnf_transformation,[],[f194]) ).
tcf(c_587,plain,
rselect_tail(queue_55) = index_57,
inference(cnf_transformation,[],[f439]) ).
tcf(c_588,plain,
s(index_3) = index_6,
inference(cnf_transformation,[],[f196]) ).
tcf(c_589,plain,
s(index_57) = index_60,
inference(cnf_transformation,[],[f197]) ).
tcf(c_590,plain,
rselect_tail(queue_61) = index_63,
inference(cnf_transformation,[],[f440]) ).
tcf(c_591,plain,
s(index_63) = index_66,
inference(cnf_transformation,[],[f199]) ).
tcf(c_592,plain,
rselect_tail(queue_7) = index_69,
inference(cnf_transformation,[],[f441]) ).
tcf(c_593,plain,
s(index_69) = index_72,
inference(cnf_transformation,[],[f201]) ).
tcf(c_594,plain,
rselect_tail(queue_67) = index_75,
inference(cnf_transformation,[],[f442]) ).
tcf(c_595,plain,
s(index_75) = index_78,
inference(cnf_transformation,[],[f203]) ).
tcf(c_596,plain,
rselect_tail(queue_79) = index_81,
inference(cnf_transformation,[],[f443]) ).
tcf(c_597,plain,
s(index_81) = index_84,
inference(cnf_transformation,[],[f205]) ).
tcf(c_598,plain,
rselect_tail(queue_85) = index_87,
inference(cnf_transformation,[],[f444]) ).
tcf(c_599,plain,
rselect_tail(queue_277) = index_9,
inference(cnf_transformation,[],[f445]) ).
tcf(c_600,plain,
s(index_87) = index_90,
inference(cnf_transformation,[],[f208]) ).
tcf(c_601,plain,
rselect_tail(queue_91) = index_93,
inference(cnf_transformation,[],[f446]) ).
tcf(c_602,plain,
s(index_93) = index_96,
inference(cnf_transformation,[],[f210]) ).
tcf(c_603,plain,
rselect_tail(queue_97) = index_99,
inference(cnf_transformation,[],[f447]) ).
tcf(c_604,plain,
rstore_head(q,index_0) = queue_1,
inference(cnf_transformation,[],[f212]) ).
tcf(c_605,plain,
rstore_seq(queue_97,earray_100) = queue_101,
inference(cnf_transformation,[],[f448]) ).
tcf(c_606,plain,
rstore_tail(queue_101,index_102) = queue_103,
inference(cnf_transformation,[],[f214]) ).
tcf(c_607,plain,
rstore_seq(queue_103,earray_106) = queue_107,
inference(cnf_transformation,[],[f449]) ).
tcf(c_608,plain,
rstore_tail(queue_107,index_108) = queue_109,
inference(cnf_transformation,[],[f216]) ).
tcf(c_609,plain,
rstore_seq(queue_277,earray_10) = queue_11,
inference(cnf_transformation,[],[f450]) ).
tcf(c_610,plain,
rstore_seq(queue_109,earray_112) = queue_113,
inference(cnf_transformation,[],[f451]) ).
tcf(c_611,plain,
rstore_tail(queue_113,index_114) = queue_115,
inference(cnf_transformation,[],[f219]) ).
tcf(c_612,plain,
rstore_seq(queue_115,earray_118) = queue_119,
inference(cnf_transformation,[],[f452]) ).
tcf(c_613,plain,
rstore_tail(queue_119,index_120) = queue_121,
inference(cnf_transformation,[],[f221]) ).
tcf(c_614,plain,
rstore_seq(queue_121,earray_124) = queue_125,
inference(cnf_transformation,[],[f453]) ).
tcf(c_615,plain,
rstore_tail(queue_125,index_126) = queue_127,
inference(cnf_transformation,[],[f223]) ).
tcf(c_616,plain,
rstore_tail(queue_11,index_12) = queue_13,
inference(cnf_transformation,[],[f224]) ).
tcf(c_617,plain,
rstore_seq(queue_127,earray_130) = queue_131,
inference(cnf_transformation,[],[f454]) ).
tcf(c_618,plain,
rstore_tail(queue_131,index_132) = queue_133,
inference(cnf_transformation,[],[f226]) ).
tcf(c_619,plain,
rstore_seq(queue_73,earray_136) = queue_137,
inference(cnf_transformation,[],[f455]) ).
tcf(c_620,plain,
rstore_tail(queue_137,index_138) = queue_139,
inference(cnf_transformation,[],[f228]) ).
tcf(c_621,plain,
rstore_seq(queue_133,earray_142) = queue_143,
inference(cnf_transformation,[],[f456]) ).
tcf(c_622,plain,
rstore_tail(queue_143,index_144) = queue_145,
inference(cnf_transformation,[],[f230]) ).
tcf(c_623,plain,
rstore_seq(queue_145,earray_148) = queue_149,
inference(cnf_transformation,[],[f457]) ).
tcf(c_624,plain,
rstore_tail(queue_149,index_150) = queue_151,
inference(cnf_transformation,[],[f232]) ).
tcf(c_625,plain,
rstore_seq(queue_151,earray_154) = queue_155,
inference(cnf_transformation,[],[f458]) ).
tcf(c_626,plain,
rstore_tail(queue_155,index_156) = queue_157,
inference(cnf_transformation,[],[f234]) ).
tcf(c_627,plain,
rstore_seq(queue_157,earray_160) = queue_161,
inference(cnf_transformation,[],[f459]) ).
tcf(c_628,plain,
rstore_tail(queue_161,index_162) = queue_163,
inference(cnf_transformation,[],[f236]) ).
tcf(c_629,plain,
rstore_seq(queue_163,earray_166) = queue_167,
inference(cnf_transformation,[],[f460]) ).
tcf(c_630,plain,
rstore_tail(queue_167,index_168) = queue_169,
inference(cnf_transformation,[],[f238]) ).
tcf(c_631,plain,
rstore_seq(queue_13,earray_16) = queue_17,
inference(cnf_transformation,[],[f461]) ).
tcf(c_632,plain,
rstore_seq(queue_169,earray_172) = queue_173,
inference(cnf_transformation,[],[f462]) ).
tcf(c_633,plain,
rstore_tail(queue_173,index_174) = queue_175,
inference(cnf_transformation,[],[f241]) ).
tcf(c_634,plain,
rstore_seq(queue_175,earray_178) = queue_179,
inference(cnf_transformation,[],[f463]) ).
tcf(c_635,plain,
rstore_tail(queue_179,index_180) = queue_181,
inference(cnf_transformation,[],[f243]) ).
tcf(c_636,plain,
rstore_seq(queue_181,earray_184) = queue_185,
inference(cnf_transformation,[],[f464]) ).
tcf(c_637,plain,
rstore_tail(queue_185,index_186) = queue_187,
inference(cnf_transformation,[],[f245]) ).
tcf(c_638,plain,
rstore_tail(queue_17,index_18) = queue_19,
inference(cnf_transformation,[],[f246]) ).
tcf(c_639,plain,
rstore_seq(queue_187,earray_190) = queue_191,
inference(cnf_transformation,[],[f465]) ).
tcf(c_640,plain,
rstore_tail(queue_191,index_192) = queue_193,
inference(cnf_transformation,[],[f248]) ).
tcf(c_641,plain,
rstore_seq(queue_193,earray_196) = queue_197,
inference(cnf_transformation,[],[f466]) ).
tcf(c_642,plain,
rstore_tail(queue_197,index_198) = queue_199,
inference(cnf_transformation,[],[f250]) ).
tcf(c_643,plain,
rstore_seq(queue_139,earray_202) = queue_203,
inference(cnf_transformation,[],[f467]) ).
tcf(c_644,plain,
rstore_tail(queue_203,index_204) = queue_205,
inference(cnf_transformation,[],[f252]) ).
tcf(c_645,plain,
rstore_seq(queue_199,earray_208) = queue_209,
inference(cnf_transformation,[],[f468]) ).
tcf(c_646,plain,
rstore_tail(queue_209,index_210) = queue_211,
inference(cnf_transformation,[],[f254]) ).
tcf(c_647,plain,
rstore_seq(queue_211,earray_214) = queue_215,
inference(cnf_transformation,[],[f469]) ).
tcf(c_648,plain,
rstore_tail(queue_215,index_216) = queue_217,
inference(cnf_transformation,[],[f256]) ).
tcf(c_649,plain,
rstore_seq(queue_217,earray_220) = queue_221,
inference(cnf_transformation,[],[f470]) ).
tcf(c_650,plain,
rstore_tail(queue_221,index_222) = queue_223,
inference(cnf_transformation,[],[f258]) ).
tcf(c_651,plain,
rstore_seq(queue_223,earray_226) = queue_227,
inference(cnf_transformation,[],[f471]) ).
tcf(c_652,plain,
rstore_tail(queue_227,index_228) = queue_229,
inference(cnf_transformation,[],[f260]) ).
tcf(c_653,plain,
rstore_seq(queue_19,earray_22) = queue_23,
inference(cnf_transformation,[],[f472]) ).
tcf(c_654,plain,
rstore_seq(queue_229,earray_232) = queue_233,
inference(cnf_transformation,[],[f473]) ).
tcf(c_655,plain,
rstore_tail(queue_233,index_234) = queue_235,
inference(cnf_transformation,[],[f263]) ).
tcf(c_656,plain,
rstore_seq(queue_235,earray_238) = queue_239,
inference(cnf_transformation,[],[f474]) ).
tcf(c_657,plain,
rstore_tail(queue_239,index_240) = queue_241,
inference(cnf_transformation,[],[f265]) ).
tcf(c_658,plain,
rstore_seq(queue_241,earray_244) = queue_245,
inference(cnf_transformation,[],[f475]) ).
tcf(c_659,plain,
rstore_tail(queue_245,index_246) = queue_247,
inference(cnf_transformation,[],[f267]) ).
tcf(c_660,plain,
rstore_tail(queue_23,index_24) = queue_25,
inference(cnf_transformation,[],[f268]) ).
tcf(c_661,plain,
rstore_seq(queue_205,earray_250) = queue_251,
inference(cnf_transformation,[],[f476]) ).
tcf(c_662,plain,
rstore_tail(queue_251,index_252) = queue_253,
inference(cnf_transformation,[],[f270]) ).
tcf(c_663,plain,
rstore_seq(queue_253,earray_256) = queue_257,
inference(cnf_transformation,[],[f477]) ).
tcf(c_664,plain,
rstore_tail(queue_257,index_258) = queue_259,
inference(cnf_transformation,[],[f272]) ).
tcf(c_665,plain,
rstore_seq(queue_259,earray_262) = queue_263,
inference(cnf_transformation,[],[f478]) ).
tcf(c_666,plain,
rstore_tail(queue_263,index_264) = queue_265,
inference(cnf_transformation,[],[f274]) ).
tcf(c_667,plain,
rstore_seq(queue_265,earray_268) = queue_269,
inference(cnf_transformation,[],[f479]) ).
tcf(c_668,plain,
rstore_tail(queue_269,index_270) = queue_271,
inference(cnf_transformation,[],[f276]) ).
tcf(c_669,plain,
rstore_seq(queue_271,earray_274) = queue_275,
inference(cnf_transformation,[],[f480]) ).
tcf(c_670,plain,
rstore_tail(queue_275,index_276) = queue_277,
inference(cnf_transformation,[],[f278]) ).
tcf(c_671,plain,
rstore_seq(queue_25,earray_28) = queue_29,
inference(cnf_transformation,[],[f481]) ).
tcf(c_672,plain,
rstore_tail(queue_29,index_30) = queue_31,
inference(cnf_transformation,[],[f280]) ).
tcf(c_673,plain,
rstore_seq(queue_31,earray_34) = queue_35,
inference(cnf_transformation,[],[f482]) ).
tcf(c_674,plain,
rstore_tail(queue_35,index_36) = queue_37,
inference(cnf_transformation,[],[f282]) ).
tcf(c_675,plain,
rstore_seq(queue_37,earray_40) = queue_41,
inference(cnf_transformation,[],[f483]) ).
tcf(c_676,plain,
rstore_tail(queue_41,index_42) = queue_43,
inference(cnf_transformation,[],[f284]) ).
tcf(c_677,plain,
rstore_seq(queue_43,earray_46) = queue_47,
inference(cnf_transformation,[],[f484]) ).
tcf(c_678,plain,
rstore_tail(queue_47,index_48) = queue_49,
inference(cnf_transformation,[],[f286]) ).
tcf(c_679,plain,
rstore_seq(queue_1,earray_4) = queue_5,
inference(cnf_transformation,[],[f485]) ).
tcf(c_680,plain,
rstore_seq(queue_49,earray_52) = queue_53,
inference(cnf_transformation,[],[f486]) ).
tcf(c_681,plain,
rstore_tail(queue_53,index_54) = queue_55,
inference(cnf_transformation,[],[f289]) ).
tcf(c_682,plain,
rstore_seq(queue_55,earray_58) = queue_59,
inference(cnf_transformation,[],[f487]) ).
tcf(c_683,plain,
rstore_tail(queue_59,index_60) = queue_61,
inference(cnf_transformation,[],[f291]) ).
tcf(c_684,plain,
rstore_seq(queue_61,earray_64) = queue_65,
inference(cnf_transformation,[],[f488]) ).
tcf(c_685,plain,
rstore_tail(queue_65,index_66) = queue_67,
inference(cnf_transformation,[],[f293]) ).
tcf(c_686,plain,
rstore_tail(queue_5,index_6) = queue_7,
inference(cnf_transformation,[],[f294]) ).
tcf(c_687,plain,
rstore_seq(queue_7,earray_70) = queue_71,
inference(cnf_transformation,[],[f489]) ).
tcf(c_688,plain,
rstore_tail(queue_71,index_72) = queue_73,
inference(cnf_transformation,[],[f296]) ).
tcf(c_689,plain,
rstore_seq(queue_67,earray_76) = queue_77,
inference(cnf_transformation,[],[f490]) ).
tcf(c_690,plain,
rstore_tail(queue_77,index_78) = queue_79,
inference(cnf_transformation,[],[f298]) ).
tcf(c_691,plain,
rstore_seq(queue_79,earray_82) = queue_83,
inference(cnf_transformation,[],[f491]) ).
tcf(c_692,plain,
rstore_tail(queue_83,index_84) = queue_85,
inference(cnf_transformation,[],[f300]) ).
tcf(c_693,plain,
rstore_seq(queue_85,earray_88) = queue_89,
inference(cnf_transformation,[],[f492]) ).
tcf(c_694,plain,
rstore_tail(queue_89,index_90) = queue_91,
inference(cnf_transformation,[],[f302]) ).
tcf(c_695,plain,
rstore_seq(queue_91,earray_94) = queue_95,
inference(cnf_transformation,[],[f493]) ).
tcf(c_696,plain,
rstore_tail(queue_95,index_96) = queue_97,
inference(cnf_transformation,[],[f304]) ).
tcf(c_697,negated_conjecture,
elem_280 != elem_283,
inference(cnf_transformation,[],[f352]) ).
tcf(c_1332,negated_conjecture,
elem_280 != elem_283,
inference(demodulation,[status(thm)],[c_697]) ).
tcf(c_2024,plain,
p(index_102) = index_99,
inference(superposition,[status(thm)],[c_509,c_408]) ).
tcf(c_2025,plain,
p(index_108) = index_105,
inference(superposition,[status(thm)],[c_511,c_408]) ).
tcf(c_2026,plain,
p(index_114) = index_111,
inference(superposition,[status(thm)],[c_513,c_408]) ).
tcf(c_2027,plain,
p(index_12) = index_9,
inference(superposition,[status(thm)],[c_515,c_408]) ).
tcf(c_2038,plain,
p(index_18) = index_15,
inference(superposition,[status(thm)],[c_537,c_408]) ).
tcf(c_2043,plain,
p(index_204) = index_201,
inference(superposition,[status(thm)],[c_546,c_408]) ).
tcf(c_2049,plain,
p(index_24) = index_21,
inference(superposition,[status(thm)],[c_559,c_408]) ).
tcf(c_2051,plain,
p(index_246) = index_243,
inference(superposition,[status(thm)],[c_562,c_408]) ).
tcf(c_2052,plain,
p(index_252) = index_249,
inference(superposition,[status(thm)],[c_564,c_408]) ).
tcf(c_2054,plain,
p(index_264) = index_261,
inference(superposition,[status(thm)],[c_568,c_408]) ).
tcf(c_2055,plain,
p(index_270) = index_267,
inference(superposition,[status(thm)],[c_571,c_408]) ).
tcf(c_2056,plain,
p(index_276) = index_273,
inference(superposition,[status(thm)],[c_573,c_408]) ).
tcf(c_2057,plain,
p(index_281) = index_282,
inference(superposition,[status(thm)],[c_576,c_408]) ).
tcf(c_2059,plain,
p(index_36) = index_33,
inference(superposition,[status(thm)],[c_580,c_408]) ).
tcf(c_2060,plain,
p(index_42) = index_39,
inference(superposition,[status(thm)],[c_582,c_408]) ).
tcf(c_2061,plain,
p(index_48) = index_45,
inference(superposition,[status(thm)],[c_584,c_408]) ).
tcf(c_2062,plain,
p(index_54) = index_51,
inference(superposition,[status(thm)],[c_586,c_408]) ).
tcf(c_2063,plain,
p(index_6) = index_3,
inference(superposition,[status(thm)],[c_588,c_408]) ).
tcf(c_2064,plain,
p(index_60) = index_57,
inference(superposition,[status(thm)],[c_589,c_408]) ).
tcf(c_2065,plain,
p(index_66) = index_63,
inference(superposition,[status(thm)],[c_591,c_408]) ).
tcf(c_2066,plain,
p(index_72) = index_69,
inference(superposition,[status(thm)],[c_593,c_408]) ).
tcf(c_2067,plain,
p(index_78) = index_75,
inference(superposition,[status(thm)],[c_595,c_408]) ).
tcf(c_2068,plain,
p(index_84) = index_81,
inference(superposition,[status(thm)],[c_597,c_408]) ).
tcf(c_2069,plain,
p(index_90) = index_87,
inference(superposition,[status(thm)],[c_600,c_408]) ).
tcf(c_2070,plain,
p(index_96) = index_93,
inference(superposition,[status(thm)],[c_602,c_408]) ).
tcf(c_2129,plain,
rselect_head(queue_1) = index_0,
inference(superposition,[status(thm)],[c_604,c_400]) ).
tcf(c_2146,plain,
rselect_tail(queue_103) = index_102,
inference(superposition,[status(thm)],[c_606,c_401]) ).
tcf(c_2147,plain,
index_105 = index_102,
inference(light_normalisation,[status(thm)],[c_2146,c_510]) ).
tcf(c_2149,plain,
rstore_tail(queue_101,index_105) = queue_103,
inference(demodulation,[status(thm)],[c_606,c_2147]) ).
tcf(c_2150,plain,
p(index_105) = index_99,
inference(demodulation,[status(thm)],[c_2024,c_2147]) ).
tcf(c_2151,plain,
s(index_99) = index_105,
inference(demodulation,[status(thm)],[c_509,c_2147]) ).
tcf(c_2155,plain,
rselect_tail(queue_109) = index_108,
inference(superposition,[status(thm)],[c_608,c_401]) ).
tcf(c_2156,plain,
index_111 = index_108,
inference(light_normalisation,[status(thm)],[c_2155,c_512]) ).
tcf(c_2158,plain,
rstore_tail(queue_107,index_111) = queue_109,
inference(demodulation,[status(thm)],[c_608,c_2156]) ).
tcf(c_2159,plain,
p(index_111) = index_105,
inference(demodulation,[status(thm)],[c_2025,c_2156]) ).
tcf(c_2160,plain,
s(index_105) = index_111,
inference(demodulation,[status(thm)],[c_511,c_2156]) ).
tcf(c_2174,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm)],[c_611,c_401]) ).
tcf(c_2175,plain,
index_117 = index_114,
inference(light_normalisation,[status(thm)],[c_2174,c_514]) ).
tcf(c_2177,plain,
rstore_tail(queue_113,index_117) = queue_115,
inference(demodulation,[status(thm)],[c_611,c_2175]) ).
tcf(c_2178,plain,
p(index_117) = index_111,
inference(demodulation,[status(thm)],[c_2026,c_2175]) ).
tcf(c_2179,plain,
s(index_111) = index_117,
inference(demodulation,[status(thm)],[c_513,c_2175]) ).
tcf(c_2183,plain,
rselect_tail(queue_121) = index_120,
inference(superposition,[status(thm)],[c_613,c_401]) ).
tcf(c_2184,plain,
index_123 = index_120,
inference(light_normalisation,[status(thm)],[c_2183,c_517]) ).
tcf(c_2186,plain,
rstore_tail(queue_119,index_123) = queue_121,
inference(demodulation,[status(thm)],[c_613,c_2184]) ).
tcf(c_2188,plain,
s(index_117) = index_123,
inference(demodulation,[status(thm)],[c_516,c_2184]) ).
tcf(c_2201,plain,
rselect_tail(queue_127) = index_126,
inference(superposition,[status(thm)],[c_615,c_401]) ).
tcf(c_2202,plain,
index_129 = index_126,
inference(light_normalisation,[status(thm)],[c_2201,c_519]) ).
tcf(c_2204,plain,
rstore_tail(queue_125,index_129) = queue_127,
inference(demodulation,[status(thm)],[c_615,c_2202]) ).
tcf(c_2206,plain,
s(index_123) = index_129,
inference(demodulation,[status(thm)],[c_518,c_2202]) ).
tcf(c_2209,plain,
rselect_tail(queue_13) = index_12,
inference(superposition,[status(thm)],[c_616,c_401]) ).
tcf(c_2210,plain,
index_15 = index_12,
inference(light_normalisation,[status(thm)],[c_2209,c_526]) ).
tcf(c_2212,plain,
rstore_tail(queue_11,index_15) = queue_13,
inference(demodulation,[status(thm)],[c_616,c_2210]) ).
tcf(c_2213,plain,
p(index_15) = index_9,
inference(demodulation,[status(thm)],[c_2027,c_2210]) ).
tcf(c_2214,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[c_515,c_2210]) ).
tcf(c_2268,plain,
rselect_tail(queue_133) = index_132,
inference(superposition,[status(thm)],[c_618,c_401]) ).
tcf(c_2269,plain,
index_141 = index_132,
inference(light_normalisation,[status(thm)],[c_2268,c_523]) ).
tcf(c_2271,plain,
rstore_tail(queue_131,index_141) = queue_133,
inference(demodulation,[status(thm)],[c_618,c_2269]) ).
tcf(c_2273,plain,
s(index_129) = index_141,
inference(demodulation,[status(thm)],[c_520,c_2269]) ).
tcf(c_2277,plain,
rselect_tail(queue_139) = index_138,
inference(superposition,[status(thm)],[c_620,c_401]) ).
tcf(c_2278,plain,
index_201 = index_138,
inference(light_normalisation,[status(thm)],[c_2277,c_545]) ).
tcf(c_2280,plain,
rstore_tail(queue_137,index_201) = queue_139,
inference(demodulation,[status(thm)],[c_620,c_2278]) ).
tcf(c_2282,plain,
s(index_135) = index_201,
inference(demodulation,[status(thm)],[c_522,c_2278]) ).
tcf(c_2294,plain,
rselect_tail(queue_145) = index_144,
inference(superposition,[status(thm)],[c_622,c_401]) ).
tcf(c_2295,plain,
index_147 = index_144,
inference(light_normalisation,[status(thm)],[c_2294,c_525]) ).
tcf(c_2297,plain,
rstore_tail(queue_143,index_147) = queue_145,
inference(demodulation,[status(thm)],[c_622,c_2295]) ).
tcf(c_2300,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[c_524,c_2295]) ).
tcf(c_2304,plain,
rselect_tail(queue_151) = index_150,
inference(superposition,[status(thm)],[c_624,c_401]) ).
tcf(c_2305,plain,
index_153 = index_150,
inference(light_normalisation,[status(thm)],[c_2304,c_528]) ).
tcf(c_2307,plain,
rstore_tail(queue_149,index_153) = queue_151,
inference(demodulation,[status(thm)],[c_624,c_2305]) ).
tcf(c_2309,plain,
s(index_147) = index_153,
inference(demodulation,[status(thm)],[c_527,c_2305]) ).
tcf(c_2314,plain,
rselect_tail(queue_157) = index_156,
inference(superposition,[status(thm)],[c_626,c_401]) ).
tcf(c_2315,plain,
index_159 = index_156,
inference(light_normalisation,[status(thm)],[c_2314,c_530]) ).
tcf(c_2317,plain,
rstore_tail(queue_155,index_159) = queue_157,
inference(demodulation,[status(thm)],[c_626,c_2315]) ).
tcf(c_2320,plain,
s(index_153) = index_159,
inference(demodulation,[status(thm)],[c_529,c_2315]) ).
tcf(c_2324,plain,
rselect_tail(queue_163) = index_162,
inference(superposition,[status(thm)],[c_628,c_401]) ).
tcf(c_2325,plain,
index_165 = index_162,
inference(light_normalisation,[status(thm)],[c_2324,c_532]) ).
tcf(c_2327,plain,
rstore_tail(queue_161,index_165) = queue_163,
inference(demodulation,[status(thm)],[c_628,c_2325]) ).
tcf(c_2330,plain,
s(index_159) = index_165,
inference(demodulation,[status(thm)],[c_531,c_2325]) ).
tcf(c_2334,plain,
rselect_tail(queue_169) = index_168,
inference(superposition,[status(thm)],[c_630,c_401]) ).
tcf(c_2335,plain,
index_171 = index_168,
inference(light_normalisation,[status(thm)],[c_2334,c_534]) ).
tcf(c_2337,plain,
rstore_tail(queue_167,index_171) = queue_169,
inference(demodulation,[status(thm)],[c_630,c_2335]) ).
tcf(c_2340,plain,
s(index_165) = index_171,
inference(demodulation,[status(thm)],[c_533,c_2335]) ).
tcf(c_2345,plain,
rselect_tail(queue_175) = index_174,
inference(superposition,[status(thm)],[c_633,c_401]) ).
tcf(c_2346,plain,
index_177 = index_174,
inference(light_normalisation,[status(thm)],[c_2345,c_536]) ).
tcf(c_2348,plain,
rstore_tail(queue_173,index_177) = queue_175,
inference(demodulation,[status(thm)],[c_633,c_2346]) ).
tcf(c_2351,plain,
s(index_171) = index_177,
inference(demodulation,[status(thm)],[c_535,c_2346]) ).
tcf(c_2355,plain,
rselect_tail(queue_181) = index_180,
inference(superposition,[status(thm)],[c_635,c_401]) ).
tcf(c_2356,plain,
index_183 = index_180,
inference(light_normalisation,[status(thm)],[c_2355,c_539]) ).
tcf(c_2358,plain,
rstore_tail(queue_179,index_183) = queue_181,
inference(demodulation,[status(thm)],[c_635,c_2356]) ).
tcf(c_2361,plain,
s(index_177) = index_183,
inference(demodulation,[status(thm)],[c_538,c_2356]) ).
tcf(c_2365,plain,
rselect_tail(queue_187) = index_186,
inference(superposition,[status(thm)],[c_637,c_401]) ).
tcf(c_2366,plain,
index_189 = index_186,
inference(light_normalisation,[status(thm)],[c_2365,c_541]) ).
tcf(c_2368,plain,
rstore_tail(queue_185,index_189) = queue_187,
inference(demodulation,[status(thm)],[c_637,c_2366]) ).
tcf(c_2371,plain,
s(index_183) = index_189,
inference(demodulation,[status(thm)],[c_540,c_2366]) ).
tcf(c_2374,plain,
rselect_tail(queue_19) = index_18,
inference(superposition,[status(thm)],[c_638,c_401]) ).
tcf(c_2375,plain,
index_21 = index_18,
inference(light_normalisation,[status(thm)],[c_2374,c_548]) ).
tcf(c_2377,plain,
rstore_tail(queue_17,index_21) = queue_19,
inference(demodulation,[status(thm)],[c_638,c_2375]) ).
tcf(c_2379,plain,
p(index_21) = index_15,
inference(demodulation,[status(thm)],[c_2038,c_2375]) ).
tcf(c_2380,plain,
s(index_15) = index_21,
inference(demodulation,[status(thm)],[c_537,c_2375]) ).
tcf(c_2384,plain,
rselect_tail(queue_193) = index_192,
inference(superposition,[status(thm)],[c_640,c_401]) ).
tcf(c_2385,plain,
index_195 = index_192,
inference(light_normalisation,[status(thm)],[c_2384,c_543]) ).
tcf(c_2387,plain,
rstore_tail(queue_191,index_195) = queue_193,
inference(demodulation,[status(thm)],[c_640,c_2385]) ).
tcf(c_2390,plain,
s(index_189) = index_195,
inference(demodulation,[status(thm)],[c_542,c_2385]) ).
tcf(c_2400,plain,
rselect_tail(queue_199) = index_198,
inference(superposition,[status(thm)],[c_642,c_401]) ).
tcf(c_2401,plain,
index_207 = index_198,
inference(light_normalisation,[status(thm)],[c_2400,c_547]) ).
tcf(c_2403,plain,
rstore_tail(queue_197,index_207) = queue_199,
inference(demodulation,[status(thm)],[c_642,c_2401]) ).
tcf(c_2406,plain,
s(index_195) = index_207,
inference(demodulation,[status(thm)],[c_544,c_2401]) ).
tcf(c_2410,plain,
rselect_tail(queue_205) = index_204,
inference(superposition,[status(thm)],[c_644,c_401]) ).
tcf(c_2411,plain,
index_249 = index_204,
inference(light_normalisation,[status(thm)],[c_2410,c_563]) ).
tcf(c_2413,plain,
rstore_tail(queue_203,index_249) = queue_205,
inference(demodulation,[status(thm)],[c_644,c_2411]) ).
tcf(c_2415,plain,
p(index_249) = index_201,
inference(demodulation,[status(thm)],[c_2043,c_2411]) ).
tcf(c_2416,plain,
s(index_201) = index_249,
inference(demodulation,[status(thm)],[c_546,c_2411]) ).
tcf(c_2430,plain,
rselect_tail(queue_211) = index_210,
inference(superposition,[status(thm)],[c_646,c_401]) ).
tcf(c_2431,plain,
index_213 = index_210,
inference(light_normalisation,[status(thm)],[c_2430,c_550]) ).
tcf(c_2433,plain,
rstore_tail(queue_209,index_213) = queue_211,
inference(demodulation,[status(thm)],[c_646,c_2431]) ).
tcf(c_2436,plain,
s(index_207) = index_213,
inference(demodulation,[status(thm)],[c_549,c_2431]) ).
tcf(c_2440,plain,
rselect_tail(queue_217) = index_216,
inference(superposition,[status(thm)],[c_648,c_401]) ).
tcf(c_2441,plain,
index_219 = index_216,
inference(light_normalisation,[status(thm)],[c_2440,c_552]) ).
tcf(c_2443,plain,
rstore_tail(queue_215,index_219) = queue_217,
inference(demodulation,[status(thm)],[c_648,c_2441]) ).
tcf(c_2446,plain,
s(index_213) = index_219,
inference(demodulation,[status(thm)],[c_551,c_2441]) ).
tcf(c_2460,plain,
rselect_tail(queue_223) = index_222,
inference(superposition,[status(thm)],[c_650,c_401]) ).
tcf(c_2461,plain,
index_225 = index_222,
inference(light_normalisation,[status(thm)],[c_2460,c_554]) ).
tcf(c_2463,plain,
rstore_tail(queue_221,index_225) = queue_223,
inference(demodulation,[status(thm)],[c_650,c_2461]) ).
tcf(c_2466,plain,
s(index_219) = index_225,
inference(demodulation,[status(thm)],[c_553,c_2461]) ).
tcf(c_2470,plain,
rselect_tail(queue_229) = index_228,
inference(superposition,[status(thm)],[c_652,c_401]) ).
tcf(c_2471,plain,
index_231 = index_228,
inference(light_normalisation,[status(thm)],[c_2470,c_556]) ).
tcf(c_2473,plain,
rstore_tail(queue_227,index_231) = queue_229,
inference(demodulation,[status(thm)],[c_652,c_2471]) ).
tcf(c_2476,plain,
s(index_225) = index_231,
inference(demodulation,[status(thm)],[c_555,c_2471]) ).
tcf(c_2491,plain,
rselect_tail(queue_235) = index_234,
inference(superposition,[status(thm)],[c_655,c_401]) ).
tcf(c_2492,plain,
index_237 = index_234,
inference(light_normalisation,[status(thm)],[c_2491,c_558]) ).
tcf(c_2494,plain,
rstore_tail(queue_233,index_237) = queue_235,
inference(demodulation,[status(thm)],[c_655,c_2492]) ).
tcf(c_2497,plain,
s(index_231) = index_237,
inference(demodulation,[status(thm)],[c_557,c_2492]) ).
tcf(c_2501,plain,
rselect_tail(queue_241) = index_240,
inference(superposition,[status(thm)],[c_657,c_401]) ).
tcf(c_2502,plain,
index_243 = index_240,
inference(light_normalisation,[status(thm)],[c_2501,c_561]) ).
tcf(c_2504,plain,
rstore_tail(queue_239,index_243) = queue_241,
inference(demodulation,[status(thm)],[c_657,c_2502]) ).
tcf(c_2507,plain,
s(index_237) = index_243,
inference(demodulation,[status(thm)],[c_560,c_2502]) ).
tcf(c_2519,plain,
rselect_seq(queue_245) = earray_244,
inference(superposition,[status(thm)],[c_658,c_399]) ).
tcf(c_2520,plain,
rselect_seq(queue_245) = rselect_seq(queue_247),
inference(superposition,[status(thm)],[c_659,c_403]) ).
tcf(c_2521,plain,
rselect_tail(queue_247) = index_246,
inference(superposition,[status(thm)],[c_659,c_401]) ).
tcf(c_2522,plain,
earray_244 = earray_278,
inference(light_normalisation,[status(thm)],[c_2520,c_479,c_2519]) ).
tcf(c_2523,plain,
index_246 = index_281,
inference(demodulation,[status(thm)],[c_575,c_2521]) ).
tcf(c_2525,plain,
p(index_246) = index_282,
inference(demodulation,[status(thm)],[c_2057,c_2523]) ).
tcf(c_2527,plain,
index_243 = index_282,
inference(light_normalisation,[status(thm)],[c_2525,c_2051]) ).
tcf(c_2528,plain,
select(earray_278,index_243) = elem_283,
inference(demodulation,[status(thm)],[c_507,c_2527]) ).
tcf(c_2529,plain,
rstore_seq(queue_241,earray_278) = queue_245,
inference(demodulation,[status(thm)],[c_658,c_2522]) ).
tcf(c_2531,plain,
rselect_tail(queue_25) = index_24,
inference(superposition,[status(thm)],[c_660,c_401]) ).
tcf(c_2532,plain,
index_27 = index_24,
inference(light_normalisation,[status(thm)],[c_2531,c_570]) ).
tcf(c_2534,plain,
rstore_tail(queue_23,index_27) = queue_25,
inference(demodulation,[status(thm)],[c_660,c_2532]) ).
tcf(c_2536,plain,
p(index_27) = index_21,
inference(demodulation,[status(thm)],[c_2049,c_2532]) ).
tcf(c_2537,plain,
s(index_21) = index_27,
inference(demodulation,[status(thm)],[c_559,c_2532]) ).
tcf(c_2545,plain,
rselect_tail(queue_253) = index_252,
inference(superposition,[status(thm)],[c_662,c_401]) ).
tcf(c_2546,plain,
index_255 = index_252,
inference(light_normalisation,[status(thm)],[c_2545,c_565]) ).
tcf(c_2548,plain,
rstore_tail(queue_251,index_255) = queue_253,
inference(demodulation,[status(thm)],[c_662,c_2546]) ).
tcf(c_2550,plain,
p(index_255) = index_249,
inference(demodulation,[status(thm)],[c_2052,c_2546]) ).
tcf(c_2551,plain,
s(index_249) = index_255,
inference(demodulation,[status(thm)],[c_564,c_2546]) ).
tcf(c_2555,plain,
rselect_tail(queue_259) = index_258,
inference(superposition,[status(thm)],[c_664,c_401]) ).
tcf(c_2556,plain,
index_261 = index_258,
inference(light_normalisation,[status(thm)],[c_2555,c_567]) ).
tcf(c_2558,plain,
rstore_tail(queue_257,index_261) = queue_259,
inference(demodulation,[status(thm)],[c_664,c_2556]) ).
tcf(c_2561,plain,
s(index_255) = index_261,
inference(demodulation,[status(thm)],[c_566,c_2556]) ).
tcf(c_2575,plain,
rselect_tail(queue_265) = index_264,
inference(superposition,[status(thm)],[c_666,c_401]) ).
tcf(c_2576,plain,
index_267 = index_264,
inference(light_normalisation,[status(thm)],[c_2575,c_569]) ).
tcf(c_2578,plain,
rstore_tail(queue_263,index_267) = queue_265,
inference(demodulation,[status(thm)],[c_666,c_2576]) ).
tcf(c_2580,plain,
p(index_267) = index_261,
inference(demodulation,[status(thm)],[c_2054,c_2576]) ).
tcf(c_2585,plain,
rselect_tail(queue_271) = index_270,
inference(superposition,[status(thm)],[c_668,c_401]) ).
tcf(c_2586,plain,
index_273 = index_270,
inference(light_normalisation,[status(thm)],[c_2585,c_572]) ).
tcf(c_2588,plain,
rstore_tail(queue_269,index_273) = queue_271,
inference(demodulation,[status(thm)],[c_668,c_2586]) ).
tcf(c_2590,plain,
p(index_273) = index_267,
inference(demodulation,[status(thm)],[c_2055,c_2586]) ).
tcf(c_2593,plain,
rselect_seq(queue_275) = earray_274,
inference(superposition,[status(thm)],[c_669,c_399]) ).
tcf(c_2600,plain,
rselect_seq(queue_275) = rselect_seq(queue_277),
inference(superposition,[status(thm)],[c_670,c_403]) ).
tcf(c_2601,plain,
rselect_tail(queue_277) = index_276,
inference(superposition,[status(thm)],[c_670,c_401]) ).
tcf(c_2602,plain,
index_9 = index_276,
inference(light_normalisation,[status(thm)],[c_2601,c_599]) ).
tcf(c_2603,plain,
earray_8 = earray_274,
inference(light_normalisation,[status(thm)],[c_2600,c_498,c_2593]) ).
tcf(c_2604,plain,
rstore_tail(queue_275,index_9) = queue_277,
inference(demodulation,[status(thm)],[c_670,c_2602]) ).
tcf(c_2606,plain,
p(index_9) = index_273,
inference(demodulation,[status(thm)],[c_2056,c_2602]) ).
tcf(c_2608,plain,
rstore_seq(queue_271,earray_8) = queue_275,
inference(demodulation,[status(thm)],[c_669,c_2603]) ).
tcf(c_2611,plain,
rselect_tail(queue_31) = index_30,
inference(superposition,[status(thm)],[c_672,c_401]) ).
tcf(c_2612,plain,
index_33 = index_30,
inference(light_normalisation,[status(thm)],[c_2611,c_579]) ).
tcf(c_2614,plain,
rstore_tail(queue_29,index_33) = queue_31,
inference(demodulation,[status(thm)],[c_672,c_2612]) ).
tcf(c_2617,plain,
s(index_27) = index_33,
inference(demodulation,[status(thm)],[c_578,c_2612]) ).
tcf(c_2631,plain,
rselect_tail(queue_37) = index_36,
inference(superposition,[status(thm)],[c_674,c_401]) ).
tcf(c_2632,plain,
index_39 = index_36,
inference(light_normalisation,[status(thm)],[c_2631,c_581]) ).
tcf(c_2634,plain,
rstore_tail(queue_35,index_39) = queue_37,
inference(demodulation,[status(thm)],[c_674,c_2632]) ).
tcf(c_2636,plain,
p(index_39) = index_33,
inference(demodulation,[status(thm)],[c_2059,c_2632]) ).
tcf(c_2641,plain,
rselect_tail(queue_43) = index_42,
inference(superposition,[status(thm)],[c_676,c_401]) ).
tcf(c_2642,plain,
index_45 = index_42,
inference(light_normalisation,[status(thm)],[c_2641,c_583]) ).
tcf(c_2644,plain,
rstore_tail(queue_41,index_45) = queue_43,
inference(demodulation,[status(thm)],[c_676,c_2642]) ).
tcf(c_2646,plain,
p(index_45) = index_39,
inference(demodulation,[status(thm)],[c_2060,c_2642]) ).
tcf(c_2661,plain,
rselect_tail(queue_49) = index_48,
inference(superposition,[status(thm)],[c_678,c_401]) ).
tcf(c_2662,plain,
index_51 = index_48,
inference(light_normalisation,[status(thm)],[c_2661,c_585]) ).
tcf(c_2664,plain,
rstore_tail(queue_47,index_51) = queue_49,
inference(demodulation,[status(thm)],[c_678,c_2662]) ).
tcf(c_2666,plain,
p(index_51) = index_45,
inference(demodulation,[status(thm)],[c_2061,c_2662]) ).
tcf(c_2672,plain,
rselect_tail(queue_55) = index_54,
inference(superposition,[status(thm)],[c_681,c_401]) ).
tcf(c_2673,plain,
index_57 = index_54,
inference(light_normalisation,[status(thm)],[c_2672,c_587]) ).
tcf(c_2675,plain,
rstore_tail(queue_53,index_57) = queue_55,
inference(demodulation,[status(thm)],[c_681,c_2673]) ).
tcf(c_2677,plain,
p(index_57) = index_51,
inference(demodulation,[status(thm)],[c_2062,c_2673]) ).
tcf(c_2688,plain,
rselect_tail(queue_61) = index_60,
inference(superposition,[status(thm)],[c_683,c_401]) ).
tcf(c_2689,plain,
index_63 = index_60,
inference(light_normalisation,[status(thm)],[c_2688,c_590]) ).
tcf(c_2691,plain,
rstore_tail(queue_59,index_63) = queue_61,
inference(demodulation,[status(thm)],[c_683,c_2689]) ).
tcf(c_2693,plain,
p(index_63) = index_57,
inference(demodulation,[status(thm)],[c_2064,c_2689]) ).
tcf(c_2698,plain,
rselect_tail(queue_67) = index_66,
inference(superposition,[status(thm)],[c_685,c_401]) ).
tcf(c_2699,plain,
index_75 = index_66,
inference(light_normalisation,[status(thm)],[c_2698,c_594]) ).
tcf(c_2701,plain,
rstore_tail(queue_65,index_75) = queue_67,
inference(demodulation,[status(thm)],[c_685,c_2699]) ).
tcf(c_2703,plain,
p(index_75) = index_63,
inference(demodulation,[status(thm)],[c_2065,c_2699]) ).
tcf(c_2717,plain,
rselect_tail(queue_7) = index_6,
inference(superposition,[status(thm)],[c_686,c_401]) ).
tcf(c_2718,plain,
index_69 = index_6,
inference(light_normalisation,[status(thm)],[c_2717,c_592]) ).
tcf(c_2720,plain,
rstore_tail(queue_5,index_69) = queue_7,
inference(demodulation,[status(thm)],[c_686,c_2718]) ).
tcf(c_2722,plain,
p(index_69) = index_3,
inference(demodulation,[status(thm)],[c_2063,c_2718]) ).
tcf(c_2725,plain,
rselect_seq(queue_71) = earray_70,
inference(superposition,[status(thm)],[c_687,c_399]) ).
tcf(c_2726,plain,
rselect_seq(queue_71) = rselect_seq(queue_73),
inference(superposition,[status(thm)],[c_688,c_403]) ).
tcf(c_2727,plain,
rselect_tail(queue_73) = index_72,
inference(superposition,[status(thm)],[c_688,c_401]) ).
tcf(c_2728,plain,
index_135 = index_72,
inference(light_normalisation,[status(thm)],[c_2727,c_521]) ).
tcf(c_2729,plain,
earray_134 = earray_70,
inference(light_normalisation,[status(thm)],[c_2726,c_425,c_2725]) ).
tcf(c_2730,plain,
rstore_tail(queue_71,index_135) = queue_73,
inference(demodulation,[status(thm)],[c_688,c_2728]) ).
tcf(c_2732,plain,
p(index_135) = index_69,
inference(demodulation,[status(thm)],[c_2066,c_2728]) ).
tcf(c_2734,plain,
rstore_seq(queue_7,earray_134) = queue_71,
inference(demodulation,[status(thm)],[c_687,c_2729]) ).
tcf(c_2745,plain,
rselect_tail(queue_79) = index_78,
inference(superposition,[status(thm)],[c_690,c_401]) ).
tcf(c_2746,plain,
index_81 = index_78,
inference(light_normalisation,[status(thm)],[c_2745,c_596]) ).
tcf(c_2748,plain,
rstore_tail(queue_77,index_81) = queue_79,
inference(demodulation,[status(thm)],[c_690,c_2746]) ).
tcf(c_2750,plain,
p(index_81) = index_75,
inference(demodulation,[status(thm)],[c_2067,c_2746]) ).
tcf(c_2755,plain,
rselect_tail(queue_85) = index_84,
inference(superposition,[status(thm)],[c_692,c_401]) ).
tcf(c_2756,plain,
index_87 = index_84,
inference(light_normalisation,[status(thm)],[c_2755,c_598]) ).
tcf(c_2758,plain,
rstore_tail(queue_83,index_87) = queue_85,
inference(demodulation,[status(thm)],[c_692,c_2756]) ).
tcf(c_2760,plain,
p(index_87) = index_81,
inference(demodulation,[status(thm)],[c_2068,c_2756]) ).
tcf(c_2773,plain,
rselect_tail(queue_91) = index_90,
inference(superposition,[status(thm)],[c_694,c_401]) ).
tcf(c_2774,plain,
index_93 = index_90,
inference(light_normalisation,[status(thm)],[c_2773,c_601]) ).
tcf(c_2776,plain,
rstore_tail(queue_89,index_93) = queue_91,
inference(demodulation,[status(thm)],[c_694,c_2774]) ).
tcf(c_2778,plain,
p(index_93) = index_87,
inference(demodulation,[status(thm)],[c_2069,c_2774]) ).
tcf(c_2781,plain,
rselect_seq(queue_95) = earray_94,
inference(superposition,[status(thm)],[c_695,c_399]) ).
tcf(c_2782,plain,
rselect_seq(queue_95) = rselect_seq(queue_97),
inference(superposition,[status(thm)],[c_696,c_403]) ).
tcf(c_2783,plain,
rselect_tail(queue_97) = index_96,
inference(superposition,[status(thm)],[c_696,c_401]) ).
tcf(c_2784,plain,
index_99 = index_96,
inference(light_normalisation,[status(thm)],[c_2783,c_603]) ).
tcf(c_2785,plain,
earray_98 = earray_94,
inference(light_normalisation,[status(thm)],[c_2782,c_505,c_2781]) ).
tcf(c_2786,plain,
rstore_tail(queue_95,index_99) = queue_97,
inference(demodulation,[status(thm)],[c_696,c_2784]) ).
tcf(c_2788,plain,
p(index_99) = index_93,
inference(demodulation,[status(thm)],[c_2070,c_2784]) ).
tcf(c_2790,plain,
rstore_seq(queue_91,earray_98) = queue_95,
inference(demodulation,[status(thm)],[c_695,c_2785]) ).
tcf(c_2878,plain,
s(s(index_105)) = index_99,
inference(superposition,[status(thm)],[c_2151,c_412]) ).
tcf(c_2879,plain,
s(s(index_111)) = index_105,
inference(superposition,[status(thm)],[c_2160,c_412]) ).
tcf(c_2880,plain,
s(s(index_117)) = index_111,
inference(superposition,[status(thm)],[c_2179,c_412]) ).
tcf(c_2881,plain,
s(s(index_15)) = index_9,
inference(superposition,[status(thm)],[c_2214,c_412]) ).
tcf(c_2882,plain,
s(s(index_123)) = index_117,
inference(superposition,[status(thm)],[c_2188,c_412]) ).
tcf(c_2883,plain,
s(s(index_129)) = index_123,
inference(superposition,[status(thm)],[c_2206,c_412]) ).
tcf(c_2884,plain,
s(s(index_141)) = index_129,
inference(superposition,[status(thm)],[c_2273,c_412]) ).
tcf(c_2885,plain,
s(s(index_201)) = index_135,
inference(superposition,[status(thm)],[c_2282,c_412]) ).
tcf(c_2886,plain,
s(s(index_147)) = index_141,
inference(superposition,[status(thm)],[c_2300,c_412]) ).
tcf(c_2887,plain,
s(s(index_153)) = index_147,
inference(superposition,[status(thm)],[c_2309,c_412]) ).
tcf(c_2888,plain,
s(s(index_159)) = index_153,
inference(superposition,[status(thm)],[c_2320,c_412]) ).
tcf(c_2889,plain,
s(s(index_165)) = index_159,
inference(superposition,[status(thm)],[c_2330,c_412]) ).
tcf(c_2890,plain,
s(s(index_171)) = index_165,
inference(superposition,[status(thm)],[c_2340,c_412]) ).
tcf(c_2891,plain,
s(s(index_177)) = index_171,
inference(superposition,[status(thm)],[c_2351,c_412]) ).
tcf(c_2892,plain,
s(s(index_21)) = index_15,
inference(superposition,[status(thm)],[c_2380,c_412]) ).
tcf(c_2893,plain,
s(s(index_183)) = index_177,
inference(superposition,[status(thm)],[c_2361,c_412]) ).
tcf(c_2894,plain,
s(s(index_189)) = index_183,
inference(superposition,[status(thm)],[c_2371,c_412]) ).
tcf(c_2895,plain,
s(s(index_195)) = index_189,
inference(superposition,[status(thm)],[c_2390,c_412]) ).
tcf(c_2896,plain,
s(s(index_207)) = index_195,
inference(superposition,[status(thm)],[c_2406,c_412]) ).
tcf(c_2897,plain,
s(s(index_249)) = index_201,
inference(superposition,[status(thm)],[c_2416,c_412]) ).
tcf(c_2898,plain,
s(s(index_213)) = index_207,
inference(superposition,[status(thm)],[c_2436,c_412]) ).
tcf(c_2899,plain,
s(s(index_219)) = index_213,
inference(superposition,[status(thm)],[c_2446,c_412]) ).
tcf(c_2900,plain,
s(s(index_225)) = index_219,
inference(superposition,[status(thm)],[c_2466,c_412]) ).
tcf(c_2901,plain,
s(s(index_231)) = index_225,
inference(superposition,[status(thm)],[c_2476,c_412]) ).
tcf(c_2907,plain,
index_225 = index_243,
inference(light_normalisation,[status(thm)],[c_2901,c_2497,c_2507]) ).
tcf(c_2908,plain,
index_219 = index_237,
inference(light_normalisation,[status(thm)],[c_2900,c_2476,c_2497]) ).
tcf(c_2909,plain,
index_213 = index_231,
inference(light_normalisation,[status(thm)],[c_2899,c_2466,c_2476]) ).
tcf(c_2910,plain,
index_207 = index_225,
inference(light_normalisation,[status(thm)],[c_2898,c_2446,c_2466]) ).
tcf(c_2911,plain,
index_201 = index_261,
inference(light_normalisation,[status(thm)],[c_2897,c_2551,c_2561]) ).
tcf(c_2912,plain,
index_195 = index_219,
inference(light_normalisation,[status(thm)],[c_2896,c_2436,c_2446]) ).
tcf(c_2913,plain,
index_189 = index_213,
inference(light_normalisation,[status(thm)],[c_2895,c_2406,c_2436]) ).
tcf(c_2914,plain,
index_183 = index_207,
inference(light_normalisation,[status(thm)],[c_2894,c_2390,c_2406]) ).
tcf(c_2915,plain,
index_177 = index_195,
inference(light_normalisation,[status(thm)],[c_2893,c_2371,c_2390]) ).
tcf(c_2916,plain,
index_15 = index_33,
inference(light_normalisation,[status(thm)],[c_2892,c_2537,c_2617]) ).
tcf(c_2917,plain,
index_171 = index_189,
inference(light_normalisation,[status(thm)],[c_2891,c_2361,c_2371]) ).
tcf(c_2918,plain,
index_165 = index_183,
inference(light_normalisation,[status(thm)],[c_2890,c_2351,c_2361]) ).
tcf(c_2919,plain,
index_159 = index_177,
inference(light_normalisation,[status(thm)],[c_2889,c_2340,c_2351]) ).
tcf(c_2920,plain,
index_153 = index_171,
inference(light_normalisation,[status(thm)],[c_2888,c_2330,c_2340]) ).
tcf(c_2921,plain,
index_147 = index_165,
inference(light_normalisation,[status(thm)],[c_2887,c_2320,c_2330]) ).
tcf(c_2922,plain,
index_141 = index_159,
inference(light_normalisation,[status(thm)],[c_2886,c_2309,c_2320]) ).
tcf(c_2923,plain,
index_135 = index_255,
inference(light_normalisation,[status(thm)],[c_2885,c_2416,c_2551]) ).
tcf(c_2924,plain,
index_129 = index_153,
inference(light_normalisation,[status(thm)],[c_2884,c_2300,c_2309]) ).
tcf(c_2925,plain,
index_123 = index_147,
inference(light_normalisation,[status(thm)],[c_2883,c_2273,c_2300]) ).
tcf(c_2926,plain,
index_117 = index_141,
inference(light_normalisation,[status(thm)],[c_2882,c_2206,c_2273]) ).
tcf(c_2927,plain,
index_9 = index_27,
inference(light_normalisation,[status(thm)],[c_2881,c_2380,c_2537]) ).
tcf(c_2928,plain,
index_111 = index_129,
inference(light_normalisation,[status(thm)],[c_2880,c_2188,c_2206]) ).
tcf(c_2929,plain,
index_105 = index_123,
inference(light_normalisation,[status(thm)],[c_2879,c_2179,c_2188]) ).
tcf(c_2930,plain,
index_99 = index_117,
inference(light_normalisation,[status(thm)],[c_2878,c_2160,c_2179]) ).
tcf(c_2933,plain,
select(earray_278,index_225) = elem_283,
inference(demodulation,[status(thm)],[c_2528,c_2907]) ).
tcf(c_2938,plain,
s(index_225) = index_246,
inference(demodulation,[status(thm)],[c_562,c_2907]) ).
tcf(c_2940,plain,
index_231 = index_246,
inference(light_normalisation,[status(thm)],[c_2938,c_2476]) ).
tcf(c_2942,plain,
rstore_tail(queue_245,index_231) = queue_247,
inference(demodulation,[status(thm)],[c_659,c_2940]) ).
tcf(c_3000,plain,
rstore_tail(queue_173,index_159) = queue_175,
inference(demodulation,[status(thm)],[c_2348,c_2919]) ).
tcf(c_3007,plain,
rstore_tail(queue_167,index_153) = queue_169,
inference(demodulation,[status(thm)],[c_2337,c_2920]) ).
tcf(c_3014,plain,
rstore_tail(queue_161,index_147) = queue_163,
inference(demodulation,[status(thm)],[c_2327,c_2921]) ).
tcf(c_3021,plain,
rstore_tail(queue_155,index_141) = queue_157,
inference(demodulation,[status(thm)],[c_2317,c_2922]) ).
tcf(c_3030,plain,
rstore_tail(queue_149,index_129) = queue_151,
inference(demodulation,[status(thm)],[c_2307,c_2924]) ).
tcf(c_3037,plain,
rstore_tail(queue_143,index_123) = queue_145,
inference(demodulation,[status(thm)],[c_2297,c_2925]) ).
tcf(c_3044,plain,
rstore_tail(queue_131,index_117) = queue_133,
inference(demodulation,[status(thm)],[c_2271,c_2926]) ).
tcf(c_3053,plain,
rstore_tail(queue_125,index_111) = queue_127,
inference(demodulation,[status(thm)],[c_2204,c_2928]) ).
tcf(c_3060,plain,
rstore_tail(queue_119,index_105) = queue_121,
inference(demodulation,[status(thm)],[c_2186,c_2929]) ).
tcf(c_3067,plain,
rstore_tail(queue_113,index_99) = queue_115,
inference(demodulation,[status(thm)],[c_2177,c_2930]) ).
tcf(c_3069,plain,
p(index_99) = index_111,
inference(demodulation,[status(thm)],[c_2178,c_2930]) ).
tcf(c_3090,plain,
index_105 = index_243,
inference(light_normalisation,[status(thm)],[c_2907,c_2910,c_2914,c_2918,c_2921,c_2925,c_2929]) ).
tcf(c_3091,plain,
index_99 = index_237,
inference(light_normalisation,[status(thm)],[c_2908,c_2912,c_2915,c_2919,c_2922,c_2926,c_2930]) ).
tcf(c_3092,plain,
index_111 = index_231,
inference(light_normalisation,[status(thm)],[c_2909,c_2913,c_2917,c_2920,c_2924,c_2928]) ).
tcf(c_3093,plain,
index_105 = index_225,
inference(light_normalisation,[status(thm)],[c_2910,c_2914,c_2918,c_2921,c_2925,c_2929]) ).
tcf(c_3094,plain,
index_99 = index_219,
inference(light_normalisation,[status(thm)],[c_2912,c_2915,c_2919,c_2922,c_2926,c_2930]) ).
tcf(c_3095,plain,
index_111 = index_213,
inference(light_normalisation,[status(thm)],[c_2913,c_2917,c_2920,c_2924,c_2928]) ).
tcf(c_3096,plain,
index_105 = index_207,
inference(light_normalisation,[status(thm)],[c_2914,c_2918,c_2921,c_2925,c_2929]) ).
tcf(c_3097,plain,
index_99 = index_195,
inference(light_normalisation,[status(thm)],[c_2915,c_2919,c_2922,c_2926,c_2930]) ).
tcf(c_3098,plain,
index_111 = index_189,
inference(light_normalisation,[status(thm)],[c_2917,c_2920,c_2924,c_2928]) ).
tcf(c_3099,plain,
index_105 = index_183,
inference(light_normalisation,[status(thm)],[c_2918,c_2921,c_2925,c_2929]) ).
tcf(c_3100,plain,
select(earray_278,index_105) = elem_283,
inference(light_normalisation,[status(thm)],[c_2933,c_3093]) ).
tcf(c_3128,plain,
index_99 = index_159,
inference(light_normalisation,[status(thm)],[c_2922,c_2926,c_2930]) ).
tcf(c_3129,plain,
index_111 = index_153,
inference(light_normalisation,[status(thm)],[c_2924,c_2928]) ).
tcf(c_3130,plain,
index_105 = index_147,
inference(light_normalisation,[status(thm)],[c_2925,c_2929]) ).
tcf(c_3131,plain,
index_99 = index_141,
inference(light_normalisation,[status(thm)],[c_2926,c_2930]) ).
tcf(c_3132,plain,
rstore_tail(queue_179,index_105) = queue_181,
inference(light_normalisation,[status(thm)],[c_2358,c_3099]) ).
tcf(c_3225,plain,
rstore_tail(queue_185,index_111) = queue_187,
inference(light_normalisation,[status(thm)],[c_2368,c_3098]) ).
tcf(c_3293,plain,
rstore_tail(queue_191,index_99) = queue_193,
inference(light_normalisation,[status(thm)],[c_2387,c_3097]) ).
tcf(c_3323,plain,
index_21 = index_273,
inference(light_normalisation,[status(thm)],[c_2536,c_2606,c_2927]) ).
tcf(c_3326,plain,
s(index_21) = index_9,
inference(light_normalisation,[status(thm)],[c_2537,c_2927]) ).
tcf(c_3328,plain,
p(index_9) = index_21,
inference(superposition,[status(thm)],[c_3326,c_408]) ).
tcf(c_3330,plain,
index_249 = index_69,
inference(light_normalisation,[status(thm)],[c_2550,c_2732,c_2923]) ).
tcf(c_3333,plain,
s(index_249) = index_135,
inference(light_normalisation,[status(thm)],[c_2551,c_2923]) ).
tcf(c_3336,plain,
rstore_tail(queue_197,index_105) = queue_199,
inference(light_normalisation,[status(thm)],[c_2403,c_3096]) ).
tcf(c_3367,plain,
p(index_267) = index_201,
inference(light_normalisation,[status(thm)],[c_2580,c_2911]) ).
tcf(c_3369,plain,
s(index_201) = index_267,
inference(superposition,[status(thm)],[c_3367,c_409]) ).
tcf(c_3370,plain,
index_249 = index_267,
inference(light_normalisation,[status(thm)],[c_3369,c_2416]) ).
tcf(c_3405,plain,
index_15 = index_249,
inference(light_normalisation,[status(thm)],[c_2590,c_2379,c_3323,c_3370]) ).
tcf(c_3408,plain,
rstore_tail(queue_203,index_15) = queue_205,
inference(demodulation,[status(thm)],[c_2413,c_3405]) ).
tcf(c_3410,plain,
index_15 = index_267,
inference(demodulation,[status(thm)],[c_3370,c_3405]) ).
tcf(c_3411,plain,
s(index_15) = index_135,
inference(demodulation,[status(thm)],[c_3333,c_3405]) ).
tcf(c_3413,plain,
index_15 = index_69,
inference(demodulation,[status(thm)],[c_3330,c_3405]) ).
tcf(c_3415,plain,
p(index_15) = index_201,
inference(demodulation,[status(thm)],[c_2415,c_3405]) ).
tcf(c_3419,plain,
index_9 = index_201,
inference(light_normalisation,[status(thm)],[c_3415,c_2213]) ).
tcf(c_3420,plain,
index_135 = index_21,
inference(demodulation,[status(thm)],[c_2380,c_3411]) ).
tcf(c_3421,plain,
s(index_135) = index_9,
inference(demodulation,[status(thm)],[c_3326,c_3420]) ).
tcf(c_3423,plain,
index_135 = index_273,
inference(demodulation,[status(thm)],[c_3323,c_3420]) ).
tcf(c_3425,plain,
rstore_tail(queue_17,index_135) = queue_19,
inference(demodulation,[status(thm)],[c_2377,c_3420]) ).
tcf(c_3434,plain,
index_9 = index_261,
inference(demodulation,[status(thm)],[c_2911,c_3419]) ).
tcf(c_3435,plain,
rstore_tail(queue_137,index_9) = queue_139,
inference(demodulation,[status(thm)],[c_2280,c_3419]) ).
tcf(c_3471,plain,
rstore_tail(queue_209,index_111) = queue_211,
inference(light_normalisation,[status(thm)],[c_2433,c_3095]) ).
tcf(c_3501,plain,
p(index_39) = index_15,
inference(light_normalisation,[status(thm)],[c_2636,c_2916]) ).
tcf(c_3503,plain,
s(index_15) = index_39,
inference(superposition,[status(thm)],[c_3501,c_409]) ).
tcf(c_3504,plain,
index_135 = index_39,
inference(light_normalisation,[status(thm)],[c_3503,c_3411]) ).
tcf(c_3511,plain,
rstore_tail(queue_215,index_99) = queue_217,
inference(light_normalisation,[status(thm)],[c_2443,c_3094]) ).
tcf(c_3539,plain,
p(index_45) = index_135,
inference(light_normalisation,[status(thm)],[c_2646,c_3504]) ).
tcf(c_3541,plain,
s(index_135) = index_45,
inference(superposition,[status(thm)],[c_3539,c_409]) ).
tcf(c_3542,plain,
index_9 = index_45,
inference(light_normalisation,[status(thm)],[c_3541,c_3421]) ).
tcf(c_3550,plain,
p(index_51) = index_9,
inference(light_normalisation,[status(thm)],[c_2666,c_3542]) ).
tcf(c_3552,plain,
s(index_9) = index_51,
inference(superposition,[status(thm)],[c_3550,c_409]) ).
tcf(c_3553,plain,
index_15 = index_51,
inference(light_normalisation,[status(thm)],[c_3552,c_2214]) ).
tcf(c_3559,plain,
rstore_tail(queue_221,index_105) = queue_223,
inference(light_normalisation,[status(thm)],[c_2463,c_3093]) ).
tcf(c_3580,plain,
rselect_head(queue_101) = rselect_head(queue_103),
inference(superposition,[status(thm)],[c_2149,c_404]) ).
tcf(c_3581,plain,
rselect_head(queue_107) = rselect_head(queue_109),
inference(superposition,[status(thm)],[c_2158,c_404]) ).
tcf(c_3582,plain,
rselect_head(queue_11) = rselect_head(queue_13),
inference(superposition,[status(thm)],[c_2212,c_404]) ).
tcf(c_3583,plain,
rselect_head(queue_179) = rselect_head(queue_181),
inference(superposition,[status(thm)],[c_3132,c_404]) ).
tcf(c_3584,plain,
rselect_head(queue_185) = rselect_head(queue_187),
inference(superposition,[status(thm)],[c_3225,c_404]) ).
tcf(c_3585,plain,
rselect_head(queue_191) = rselect_head(queue_193),
inference(superposition,[status(thm)],[c_3293,c_404]) ).
tcf(c_3586,plain,
rselect_head(queue_197) = rselect_head(queue_199),
inference(superposition,[status(thm)],[c_3336,c_404]) ).
tcf(c_3587,plain,
rselect_head(queue_209) = rselect_head(queue_211),
inference(superposition,[status(thm)],[c_3471,c_404]) ).
tcf(c_3588,plain,
rselect_head(queue_215) = rselect_head(queue_217),
inference(superposition,[status(thm)],[c_3511,c_404]) ).
tcf(c_3589,plain,
rselect_head(queue_221) = rselect_head(queue_223),
inference(superposition,[status(thm)],[c_3559,c_404]) ).
tcf(c_3592,plain,
p(index_57) = index_15,
inference(light_normalisation,[status(thm)],[c_2677,c_3553]) ).
tcf(c_3594,plain,
s(index_15) = index_57,
inference(superposition,[status(thm)],[c_3592,c_409]) ).
tcf(c_3595,plain,
index_135 = index_57,
inference(light_normalisation,[status(thm)],[c_3594,c_3411]) ).
tcf(c_3603,plain,
rstore_tail(queue_227,index_111) = queue_229,
inference(light_normalisation,[status(thm)],[c_2473,c_3092]) ).
tcf(c_3604,plain,
rselect_head(queue_227) = rselect_head(queue_229),
inference(superposition,[status(thm)],[c_3603,c_404]) ).
tcf(c_3607,plain,
rselect_head(queue_101) = rselect_head(queue_97),
inference(superposition,[status(thm)],[c_605,c_405]) ).
tcf(c_3608,plain,
rselect_head(queue_103) = rselect_head(queue_107),
inference(superposition,[status(thm)],[c_607,c_405]) ).
tcf(c_3609,plain,
rselect_head(queue_11) = rselect_head(queue_277),
inference(superposition,[status(thm)],[c_609,c_405]) ).
tcf(c_3610,plain,
rselect_head(queue_109) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c_610,c_405]) ).
tcf(c_3611,plain,
rselect_head(queue_115) = rselect_head(queue_119),
inference(superposition,[status(thm)],[c_612,c_405]) ).
tcf(c_3612,plain,
rselect_head(queue_121) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c_614,c_405]) ).
tcf(c_3613,plain,
rselect_head(queue_127) = rselect_head(queue_131),
inference(superposition,[status(thm)],[c_617,c_405]) ).
tcf(c_3614,plain,
rselect_head(queue_137) = rselect_head(queue_73),
inference(superposition,[status(thm)],[c_619,c_405]) ).
tcf(c_3615,plain,
rselect_head(queue_133) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c_621,c_405]) ).
tcf(c_3616,plain,
rselect_head(queue_145) = rselect_head(queue_149),
inference(superposition,[status(thm)],[c_623,c_405]) ).
tcf(c_3617,plain,
rselect_head(queue_151) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c_625,c_405]) ).
tcf(c_3618,plain,
rselect_head(queue_157) = rselect_head(queue_161),
inference(superposition,[status(thm)],[c_627,c_405]) ).
tcf(c_3619,plain,
rselect_head(queue_163) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c_629,c_405]) ).
tcf(c_3620,plain,
rselect_head(queue_13) = rselect_head(queue_17),
inference(superposition,[status(thm)],[c_631,c_405]) ).
tcf(c_3621,plain,
rselect_head(queue_169) = rselect_head(queue_173),
inference(superposition,[status(thm)],[c_632,c_405]) ).
tcf(c_3622,plain,
rselect_head(queue_175) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c_634,c_405]) ).
tcf(c_3623,plain,
rselect_head(queue_181) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c_636,c_405]) ).
tcf(c_3624,plain,
rselect_head(queue_187) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c_639,c_405]) ).
tcf(c_3625,plain,
rselect_head(queue_193) = rselect_head(queue_197),
inference(superposition,[status(thm)],[c_641,c_405]) ).
tcf(c_3626,plain,
rselect_head(queue_139) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c_643,c_405]) ).
tcf(c_3627,plain,
rselect_head(queue_199) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c_645,c_405]) ).
tcf(c_3628,plain,
rselect_head(queue_211) = rselect_head(queue_215),
inference(superposition,[status(thm)],[c_647,c_405]) ).
tcf(c_3629,plain,
rselect_head(queue_217) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c_649,c_405]) ).
tcf(c_3630,plain,
rselect_head(queue_223) = rselect_head(queue_227),
inference(superposition,[status(thm)],[c_651,c_405]) ).
tcf(c_3631,plain,
rselect_head(queue_19) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c_653,c_405]) ).
tcf(c_3632,plain,
rselect_head(queue_229) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c_654,c_405]) ).
tcf(c_3633,plain,
rselect_head(queue_235) = rselect_head(queue_239),
inference(superposition,[status(thm)],[c_656,c_405]) ).
tcf(c_3634,plain,
rselect_head(queue_205) = rselect_head(queue_251),
inference(superposition,[status(thm)],[c_661,c_405]) ).
tcf(c_3635,plain,
rselect_head(queue_253) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c_663,c_405]) ).
tcf(c_3636,plain,
rselect_head(queue_259) = rselect_head(queue_263),
inference(superposition,[status(thm)],[c_665,c_405]) ).
tcf(c_3637,plain,
rselect_head(queue_265) = rselect_head(queue_269),
inference(superposition,[status(thm)],[c_667,c_405]) ).
tcf(c_3638,plain,
rselect_head(queue_25) = rselect_head(queue_29),
inference(superposition,[status(thm)],[c_671,c_405]) ).
tcf(c_3639,plain,
rselect_head(queue_31) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c_673,c_405]) ).
tcf(c_3640,plain,
rselect_head(queue_37) = rselect_head(queue_41),
inference(superposition,[status(thm)],[c_675,c_405]) ).
tcf(c_3641,plain,
rselect_head(queue_43) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c_677,c_405]) ).
tcf(c_3642,plain,
rselect_head(queue_1) = rselect_head(queue_5),
inference(superposition,[status(thm)],[c_679,c_405]) ).
tcf(c_3643,plain,
rselect_head(queue_49) = rselect_head(queue_53),
inference(superposition,[status(thm)],[c_680,c_405]) ).
tcf(c_3644,plain,
rselect_head(queue_55) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c_682,c_405]) ).
tcf(c_3645,plain,
rselect_head(queue_61) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c_684,c_405]) ).
tcf(c_3646,plain,
rselect_head(queue_67) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c_689,c_405]) ).
tcf(c_3647,plain,
rselect_head(queue_79) = rselect_head(queue_83),
inference(superposition,[status(thm)],[c_691,c_405]) ).
tcf(c_3648,plain,
rselect_head(queue_85) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c_693,c_405]) ).
tcf(c_3649,plain,
rselect_head(queue_5) = index_0,
inference(light_normalisation,[status(thm)],[c_3642,c_2129]) ).
tcf(c_3650,plain,
rselect_head(queue_13) = rselect_head(queue_277),
inference(light_normalisation,[status(thm)],[c_3609,c_3582]) ).
tcf(c_3651,plain,
rselect_head(queue_103) = rselect_head(queue_97),
inference(light_normalisation,[status(thm)],[c_3607,c_3580]) ).
tcf(c_3834,plain,
rselect_tail(q) = rselect_tail(queue_1),
inference(superposition,[status(thm)],[c_604,c_407]) ).
tcf(c_3835,plain,
index_3 = index_0,
inference(light_normalisation,[status(thm)],[c_3834,c_508,c_577]) ).
tcf(c_3843,plain,
p(index_63) = index_135,
inference(light_normalisation,[status(thm)],[c_2693,c_3595]) ).
tcf(c_3845,plain,
s(index_135) = index_63,
inference(superposition,[status(thm)],[c_3843,c_409]) ).
tcf(c_3846,plain,
index_9 = index_63,
inference(light_normalisation,[status(thm)],[c_3845,c_3421]) ).
tcf(c_3854,plain,
p(index_75) = index_9,
inference(light_normalisation,[status(thm)],[c_2703,c_3846]) ).
tcf(c_3856,plain,
s(index_9) = index_75,
inference(superposition,[status(thm)],[c_3854,c_409]) ).
tcf(c_3857,plain,
index_15 = index_75,
inference(light_normalisation,[status(thm)],[c_3856,c_2214]) ).
tcf(c_3864,plain,
rstore_tail(queue_233,index_99) = queue_235,
inference(light_normalisation,[status(thm)],[c_2494,c_3091]) ).
tcf(c_3865,plain,
rselect_head(queue_233) = rselect_head(queue_235),
inference(superposition,[status(thm)],[c_3864,c_404]) ).
tcf(c_3868,plain,
rselect_head(queue_229) = rselect_head(queue_235),
inference(light_normalisation,[status(thm)],[c_3865,c_3632]) ).
tcf(c_3870,plain,
index_9 = index_3,
inference(light_normalisation,[status(thm)],[c_2722,c_2213,c_3413]) ).
tcf(c_3872,plain,
index_9 = index_0,
inference(demodulation,[status(thm)],[c_3835,c_3870]) ).
tcf(c_3881,plain,
p(index_81) = index_15,
inference(light_normalisation,[status(thm)],[c_2750,c_3857]) ).
tcf(c_3883,plain,
s(index_15) = index_81,
inference(superposition,[status(thm)],[c_3881,c_409]) ).
tcf(c_3884,plain,
index_135 = index_81,
inference(light_normalisation,[status(thm)],[c_3883,c_3411]) ).
tcf(c_3891,plain,
rstore_tail(queue_239,index_105) = queue_241,
inference(light_normalisation,[status(thm)],[c_2504,c_3090]) ).
tcf(c_3892,plain,
rselect_head(queue_239) = rselect_head(queue_241),
inference(superposition,[status(thm)],[c_3891,c_404]) ).
tcf(c_3895,plain,
rselect_head(queue_229) = rselect_head(queue_241),
inference(light_normalisation,[status(thm)],[c_3892,c_3633,c_3868]) ).
tcf(c_3897,plain,
p(index_87) = index_135,
inference(light_normalisation,[status(thm)],[c_2760,c_3884]) ).
tcf(c_3899,plain,
s(index_135) = index_87,
inference(superposition,[status(thm)],[c_3897,c_409]) ).
tcf(c_3900,plain,
index_9 = index_87,
inference(light_normalisation,[status(thm)],[c_3899,c_3421]) ).
tcf(c_3908,plain,
p(index_93) = index_9,
inference(light_normalisation,[status(thm)],[c_2778,c_3900]) ).
tcf(c_3910,plain,
s(index_9) = index_93,
inference(superposition,[status(thm)],[c_3908,c_409]) ).
tcf(c_3911,plain,
index_15 = index_93,
inference(light_normalisation,[status(thm)],[c_3910,c_2214]) ).
tcf(c_3921,plain,
rselect_head(queue_241) = rselect_head(queue_245),
inference(superposition,[status(thm)],[c_2529,c_405]) ).
tcf(c_3923,plain,
rselect_head(queue_229) = rselect_head(queue_245),
inference(light_normalisation,[status(thm)],[c_3921,c_3895]) ).
tcf(c_3925,plain,
index_111 = index_15,
inference(light_normalisation,[status(thm)],[c_2788,c_3069,c_3911]) ).
tcf(c_3928,plain,
index_111 = index_93,
inference(demodulation,[status(thm)],[c_3911,c_3925]) ).
tcf(c_3930,plain,
index_111 = index_75,
inference(demodulation,[status(thm)],[c_3857,c_3925]) ).
tcf(c_3932,plain,
index_111 = index_51,
inference(demodulation,[status(thm)],[c_3553,c_3925]) ).
tcf(c_3937,plain,
index_111 = index_69,
inference(demodulation,[status(thm)],[c_3413,c_3925]) ).
tcf(c_3939,plain,
index_111 = index_267,
inference(demodulation,[status(thm)],[c_3410,c_3925]) ).
tcf(c_3944,plain,
index_111 = index_33,
inference(demodulation,[status(thm)],[c_2916,c_3925]) ).
tcf(c_3947,plain,
p(index_111) = index_9,
inference(demodulation,[status(thm)],[c_2213,c_3925]) ).
tcf(c_3951,plain,
index_9 = index_105,
inference(demodulation,[status(thm)],[c_2159,c_3947]) ).
tcf(c_3970,plain,
index_9 = index_123,
inference(demodulation,[status(thm)],[c_2929,c_3951]) ).
tcf(c_3971,plain,
index_9 = index_147,
inference(demodulation,[status(thm)],[c_3130,c_3951]) ).
tcf(c_3974,plain,
select(earray_278,index_9) = elem_283,
inference(demodulation,[status(thm)],[c_3100,c_3951]) ).
tcf(c_3983,plain,
p(index_9) = index_99,
inference(demodulation,[status(thm)],[c_2150,c_3951]) ).
tcf(c_4008,plain,
rstore_tail(queue_23,index_9) = queue_25,
inference(light_normalisation,[status(thm)],[c_2534,c_2927]) ).
tcf(c_4009,plain,
rselect_head(queue_23) = rselect_head(queue_25),
inference(superposition,[status(thm)],[c_4008,c_404]) ).
tcf(c_4012,plain,
rselect_head(queue_19) = rselect_head(queue_25),
inference(light_normalisation,[status(thm)],[c_4009,c_3631]) ).
tcf(c_4028,plain,
rstore_tail(queue_251,index_135) = queue_253,
inference(light_normalisation,[status(thm)],[c_2548,c_2923]) ).
tcf(c_4029,plain,
rselect_head(queue_251) = rselect_head(queue_253),
inference(superposition,[status(thm)],[c_4028,c_404]) ).
tcf(c_4032,plain,
rselect_head(queue_205) = rselect_head(queue_253),
inference(light_normalisation,[status(thm)],[c_4029,c_3634]) ).
tcf(c_4049,plain,
rstore_tail(queue_257,index_9) = queue_259,
inference(light_normalisation,[status(thm)],[c_2558,c_3434]) ).
tcf(c_4050,plain,
rselect_head(queue_257) = rselect_head(queue_259),
inference(superposition,[status(thm)],[c_4049,c_404]) ).
tcf(c_4053,plain,
rselect_head(queue_205) = rselect_head(queue_259),
inference(light_normalisation,[status(thm)],[c_4050,c_3635,c_4032]) ).
tcf(c_4068,plain,
rstore_tail(queue_263,index_111) = queue_265,
inference(light_normalisation,[status(thm)],[c_2578,c_3939]) ).
tcf(c_4069,plain,
rselect_head(queue_263) = rselect_head(queue_265),
inference(superposition,[status(thm)],[c_4068,c_404]) ).
tcf(c_4072,plain,
rselect_head(queue_205) = rselect_head(queue_265),
inference(light_normalisation,[status(thm)],[c_4069,c_3636,c_4053]) ).
tcf(c_4082,plain,
index_99 = index_135,
inference(light_normalisation,[status(thm)],[c_3328,c_3420,c_3983]) ).
tcf(c_4088,plain,
index_99 = index_81,
inference(demodulation,[status(thm)],[c_3884,c_4082]) ).
tcf(c_4090,plain,
index_99 = index_57,
inference(demodulation,[status(thm)],[c_3595,c_4082]) ).
tcf(c_4092,plain,
index_99 = index_39,
inference(demodulation,[status(thm)],[c_3504,c_4082]) ).
tcf(c_4094,plain,
index_99 = index_273,
inference(demodulation,[status(thm)],[c_3423,c_4082]) ).
tcf(c_4104,plain,
rstore_tail(queue_269,index_99) = queue_271,
inference(light_normalisation,[status(thm)],[c_2588,c_4094]) ).
tcf(c_4105,plain,
rselect_head(queue_269) = rselect_head(queue_271),
inference(superposition,[status(thm)],[c_4104,c_404]) ).
tcf(c_4108,plain,
rselect_head(queue_205) = rselect_head(queue_271),
inference(light_normalisation,[status(thm)],[c_4105,c_3637,c_4072]) ).
tcf(c_4116,plain,
rselect_head(queue_275) = rselect_head(queue_277),
inference(superposition,[status(thm)],[c_2604,c_404]) ).
tcf(c_4119,plain,
rselect_head(queue_13) = rselect_head(queue_275),
inference(light_normalisation,[status(thm)],[c_4116,c_3650]) ).
tcf(c_4132,plain,
rselect_head(queue_271) = rselect_head(queue_275),
inference(superposition,[status(thm)],[c_2608,c_405]) ).
tcf(c_4134,plain,
rselect_head(queue_13) = rselect_head(queue_205),
inference(light_normalisation,[status(thm)],[c_4132,c_4108,c_4119]) ).
tcf(c_4136,plain,
rselect_head(queue_5) = index_9,
inference(light_normalisation,[status(thm)],[c_3649,c_3872]) ).
tcf(c_4149,plain,
rstore_tail(queue_29,index_111) = queue_31,
inference(light_normalisation,[status(thm)],[c_2614,c_3944]) ).
tcf(c_4150,plain,
rselect_head(queue_29) = rselect_head(queue_31),
inference(superposition,[status(thm)],[c_4149,c_404]) ).
tcf(c_4153,plain,
rselect_head(queue_19) = rselect_head(queue_31),
inference(light_normalisation,[status(thm)],[c_4150,c_3638,c_4012]) ).
tcf(c_4160,plain,
rstore_tail(queue_35,index_99) = queue_37,
inference(light_normalisation,[status(thm)],[c_2634,c_4092]) ).
tcf(c_4161,plain,
rselect_head(queue_35) = rselect_head(queue_37),
inference(superposition,[status(thm)],[c_4160,c_404]) ).
tcf(c_4164,plain,
rselect_head(queue_19) = rselect_head(queue_37),
inference(light_normalisation,[status(thm)],[c_4161,c_3639,c_4153]) ).
tcf(c_4172,plain,
rstore_tail(queue_41,index_9) = queue_43,
inference(light_normalisation,[status(thm)],[c_2644,c_3542]) ).
tcf(c_4173,plain,
rselect_head(queue_41) = rselect_head(queue_43),
inference(superposition,[status(thm)],[c_4172,c_404]) ).
tcf(c_4176,plain,
rselect_head(queue_19) = rselect_head(queue_43),
inference(light_normalisation,[status(thm)],[c_4173,c_3640,c_4164]) ).
tcf(c_4189,plain,
rstore_tail(queue_47,index_111) = queue_49,
inference(light_normalisation,[status(thm)],[c_2664,c_3932]) ).
tcf(c_4190,plain,
rselect_head(queue_47) = rselect_head(queue_49),
inference(superposition,[status(thm)],[c_4189,c_404]) ).
tcf(c_4193,plain,
rselect_head(queue_19) = rselect_head(queue_49),
inference(light_normalisation,[status(thm)],[c_4190,c_3641,c_4176]) ).
tcf(c_4194,plain,
rstore_tail(queue_53,index_99) = queue_55,
inference(light_normalisation,[status(thm)],[c_2675,c_4090]) ).
tcf(c_4195,plain,
rselect_head(queue_53) = rselect_head(queue_55),
inference(superposition,[status(thm)],[c_4194,c_404]) ).
tcf(c_4198,plain,
rselect_head(queue_19) = rselect_head(queue_55),
inference(light_normalisation,[status(thm)],[c_4195,c_3643,c_4193]) ).
tcf(c_4199,plain,
rstore_tail(queue_59,index_9) = queue_61,
inference(light_normalisation,[status(thm)],[c_2691,c_3846]) ).
tcf(c_4200,plain,
rselect_head(queue_59) = rselect_head(queue_61),
inference(superposition,[status(thm)],[c_4199,c_404]) ).
tcf(c_4203,plain,
rselect_head(queue_19) = rselect_head(queue_61),
inference(light_normalisation,[status(thm)],[c_4200,c_3644,c_4198]) ).
tcf(c_4204,plain,
rstore_tail(queue_65,index_111) = queue_67,
inference(light_normalisation,[status(thm)],[c_2701,c_3930]) ).
tcf(c_4205,plain,
rselect_head(queue_65) = rselect_head(queue_67),
inference(superposition,[status(thm)],[c_4204,c_404]) ).
tcf(c_4208,plain,
rselect_head(queue_19) = rselect_head(queue_67),
inference(light_normalisation,[status(thm)],[c_4205,c_3645,c_4203]) ).
tcf(c_4209,plain,
rstore_tail(queue_5,index_111) = queue_7,
inference(light_normalisation,[status(thm)],[c_2720,c_3937]) ).
tcf(c_4210,plain,
rselect_head(queue_5) = rselect_head(queue_7),
inference(superposition,[status(thm)],[c_4209,c_404]) ).
tcf(c_4213,plain,
rselect_head(queue_7) = index_9,
inference(light_normalisation,[status(thm)],[c_4210,c_4136]) ).
tcf(c_4214,plain,
rstore_tail(queue_71,index_99) = queue_73,
inference(light_normalisation,[status(thm)],[c_2730,c_4082]) ).
tcf(c_4215,plain,
rselect_head(queue_71) = rselect_head(queue_73),
inference(superposition,[status(thm)],[c_4214,c_404]) ).
tcf(c_4219,plain,
rselect_head(queue_7) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c_2734,c_405]) ).
tcf(c_4221,plain,
rselect_head(queue_71) = index_9,
inference(light_normalisation,[status(thm)],[c_4219,c_4213,c_4215]) ).
tcf(c_4223,plain,
rstore_tail(queue_77,index_99) = queue_79,
inference(light_normalisation,[status(thm)],[c_2748,c_4088]) ).
tcf(c_4224,plain,
rselect_head(queue_77) = rselect_head(queue_79),
inference(superposition,[status(thm)],[c_4223,c_404]) ).
tcf(c_4227,plain,
rselect_head(queue_19) = rselect_head(queue_79),
inference(light_normalisation,[status(thm)],[c_4224,c_3646,c_4208]) ).
tcf(c_4228,plain,
rstore_tail(queue_83,index_9) = queue_85,
inference(light_normalisation,[status(thm)],[c_2758,c_3900]) ).
tcf(c_4229,plain,
rselect_head(queue_83) = rselect_head(queue_85),
inference(superposition,[status(thm)],[c_4228,c_404]) ).
tcf(c_4232,plain,
rselect_head(queue_19) = rselect_head(queue_85),
inference(light_normalisation,[status(thm)],[c_4229,c_3647,c_4227]) ).
tcf(c_4233,plain,
rstore_tail(queue_89,index_111) = queue_91,
inference(light_normalisation,[status(thm)],[c_2776,c_3928]) ).
tcf(c_4234,plain,
rselect_head(queue_89) = rselect_head(queue_91),
inference(superposition,[status(thm)],[c_4233,c_404]) ).
tcf(c_4237,plain,
rselect_head(queue_19) = rselect_head(queue_91),
inference(light_normalisation,[status(thm)],[c_4234,c_3648,c_4232]) ).
tcf(c_4238,plain,
rselect_head(queue_95) = rselect_head(queue_97),
inference(superposition,[status(thm)],[c_2786,c_404]) ).
tcf(c_4241,plain,
rselect_head(queue_103) = rselect_head(queue_95),
inference(light_normalisation,[status(thm)],[c_4238,c_3651]) ).
tcf(c_4243,plain,
rselect_head(queue_91) = rselect_head(queue_95),
inference(superposition,[status(thm)],[c_2790,c_405]) ).
tcf(c_4245,plain,
rselect_head(queue_103) = rselect_head(queue_19),
inference(light_normalisation,[status(thm)],[c_4243,c_4237,c_4241]) ).
tcf(c_4249,plain,
rstore_tail(queue_245,index_111) = queue_247,
inference(light_normalisation,[status(thm)],[c_2942,c_3092]) ).
tcf(c_4250,plain,
rselect_head(queue_245) = rselect_head(queue_247),
inference(superposition,[status(thm)],[c_4249,c_404]) ).
tcf(c_4253,plain,
rselect_head(queue_229) = index_279,
inference(light_normalisation,[status(thm)],[c_4250,c_574,c_3923]) ).
tcf(c_4254,plain,
rstore_tail(queue_173,index_99) = queue_175,
inference(light_normalisation,[status(thm)],[c_3000,c_3128]) ).
tcf(c_4255,plain,
rselect_head(queue_173) = rselect_head(queue_175),
inference(superposition,[status(thm)],[c_4254,c_404]) ).
tcf(c_4258,plain,
rselect_head(queue_169) = rselect_head(queue_175),
inference(light_normalisation,[status(thm)],[c_4255,c_3621]) ).
tcf(c_4259,plain,
rstore_tail(queue_167,index_111) = queue_169,
inference(light_normalisation,[status(thm)],[c_3007,c_3129]) ).
tcf(c_4260,plain,
rselect_head(queue_167) = rselect_head(queue_169),
inference(superposition,[status(thm)],[c_4259,c_404]) ).
tcf(c_4263,plain,
rselect_head(queue_163) = rselect_head(queue_169),
inference(light_normalisation,[status(thm)],[c_4260,c_3619]) ).
tcf(c_4264,plain,
rstore_tail(queue_161,index_9) = queue_163,
inference(light_normalisation,[status(thm)],[c_3014,c_3971]) ).
tcf(c_4265,plain,
rselect_head(queue_161) = rselect_head(queue_163),
inference(superposition,[status(thm)],[c_4264,c_404]) ).
tcf(c_4268,plain,
rselect_head(queue_157) = rselect_head(queue_163),
inference(light_normalisation,[status(thm)],[c_4265,c_3618]) ).
tcf(c_4269,plain,
rstore_tail(queue_155,index_99) = queue_157,
inference(light_normalisation,[status(thm)],[c_3021,c_3131]) ).
tcf(c_4270,plain,
rselect_head(queue_155) = rselect_head(queue_157),
inference(superposition,[status(thm)],[c_4269,c_404]) ).
tcf(c_4273,plain,
rselect_head(queue_151) = rselect_head(queue_157),
inference(light_normalisation,[status(thm)],[c_4270,c_3617]) ).
tcf(c_4274,plain,
rstore_tail(queue_149,index_111) = queue_151,
inference(light_normalisation,[status(thm)],[c_3030,c_2928]) ).
tcf(c_4275,plain,
rselect_head(queue_149) = rselect_head(queue_151),
inference(superposition,[status(thm)],[c_4274,c_404]) ).
tcf(c_4278,plain,
rselect_head(queue_145) = rselect_head(queue_151),
inference(light_normalisation,[status(thm)],[c_4275,c_3616]) ).
tcf(c_4279,plain,
rstore_tail(queue_143,index_9) = queue_145,
inference(light_normalisation,[status(thm)],[c_3037,c_3970]) ).
tcf(c_4280,plain,
rselect_head(queue_143) = rselect_head(queue_145),
inference(superposition,[status(thm)],[c_4279,c_404]) ).
tcf(c_4283,plain,
rselect_head(queue_133) = rselect_head(queue_145),
inference(light_normalisation,[status(thm)],[c_4280,c_3615]) ).
tcf(c_4284,plain,
rstore_tail(queue_131,index_99) = queue_133,
inference(light_normalisation,[status(thm)],[c_3044,c_2930]) ).
tcf(c_4285,plain,
rselect_head(queue_131) = rselect_head(queue_133),
inference(superposition,[status(thm)],[c_4284,c_404]) ).
tcf(c_4288,plain,
rselect_head(queue_127) = rselect_head(queue_133),
inference(light_normalisation,[status(thm)],[c_4285,c_3613]) ).
tcf(c_4289,plain,
rselect_head(queue_125) = rselect_head(queue_127),
inference(superposition,[status(thm)],[c_3053,c_404]) ).
tcf(c_4292,plain,
rselect_head(queue_121) = rselect_head(queue_127),
inference(light_normalisation,[status(thm)],[c_4289,c_3612]) ).
tcf(c_4293,plain,
rstore_tail(queue_119,index_9) = queue_121,
inference(light_normalisation,[status(thm)],[c_3060,c_3951]) ).
tcf(c_4294,plain,
rselect_head(queue_119) = rselect_head(queue_121),
inference(superposition,[status(thm)],[c_4293,c_404]) ).
tcf(c_4297,plain,
rselect_head(queue_115) = rselect_head(queue_121),
inference(light_normalisation,[status(thm)],[c_4294,c_3611]) ).
tcf(c_4298,plain,
rselect_head(queue_113) = rselect_head(queue_115),
inference(superposition,[status(thm)],[c_3067,c_404]) ).
tcf(c_4301,plain,
rselect_head(queue_109) = rselect_head(queue_115),
inference(light_normalisation,[status(thm)],[c_4298,c_3610]) ).
tcf(c_4336,plain,
rstore_tail(queue_203,index_111) = queue_205,
inference(light_normalisation,[status(thm)],[c_3408,c_3925]) ).
tcf(c_4337,plain,
rselect_head(queue_203) = rselect_head(queue_205),
inference(superposition,[status(thm)],[c_4336,c_404]) ).
tcf(c_4340,plain,
rselect_head(queue_13) = rselect_head(queue_139),
inference(light_normalisation,[status(thm)],[c_4337,c_3626,c_4134]) ).
tcf(c_4341,plain,
rstore_tail(queue_17,index_99) = queue_19,
inference(light_normalisation,[status(thm)],[c_3425,c_4082]) ).
tcf(c_4342,plain,
rselect_head(queue_17) = rselect_head(queue_19),
inference(superposition,[status(thm)],[c_4341,c_404]) ).
tcf(c_4345,plain,
rselect_head(queue_103) = rselect_head(queue_13),
inference(light_normalisation,[status(thm)],[c_4342,c_3620,c_4245]) ).
tcf(c_4346,plain,
rselect_head(queue_137) = rselect_head(queue_139),
inference(superposition,[status(thm)],[c_3435,c_404]) ).
tcf(c_4349,plain,
rselect_head(queue_103) = rselect_head(queue_137),
inference(light_normalisation,[status(thm)],[c_4346,c_3614,c_4340,c_4345]) ).
tcf(c_4378,plain,
rselect_head(queue_103) = rselect_head(queue_109),
inference(light_normalisation,[status(thm)],[c_3581,c_3608]) ).
tcf(c_4380,plain,
rselect_head(queue_103) = rselect_head(queue_181),
inference(light_normalisation,[status(thm)],[c_3583,c_3622,c_4258,c_4263,c_4268,c_4273,c_4278,c_4283,c_4288,c_4292,c_4297,c_4301,c_4378]) ).
tcf(c_4381,plain,
rselect_head(queue_103) = rselect_head(queue_187),
inference(light_normalisation,[status(thm)],[c_3584,c_3623,c_4380]) ).
tcf(c_4382,plain,
rselect_head(queue_103) = rselect_head(queue_193),
inference(light_normalisation,[status(thm)],[c_3585,c_3624,c_4381]) ).
tcf(c_4383,plain,
rselect_head(queue_103) = rselect_head(queue_199),
inference(light_normalisation,[status(thm)],[c_3586,c_3625,c_4382]) ).
tcf(c_4384,plain,
rselect_head(queue_103) = rselect_head(queue_211),
inference(light_normalisation,[status(thm)],[c_3587,c_3627,c_4383]) ).
tcf(c_4385,plain,
rselect_head(queue_103) = rselect_head(queue_217),
inference(light_normalisation,[status(thm)],[c_3588,c_3628,c_4384]) ).
tcf(c_4386,plain,
rselect_head(queue_103) = rselect_head(queue_223),
inference(light_normalisation,[status(thm)],[c_3589,c_3629,c_4385]) ).
tcf(c_4387,plain,
rselect_head(queue_103) = index_279,
inference(light_normalisation,[status(thm)],[c_3604,c_3630,c_4253,c_4386]) ).
tcf(c_4412,plain,
rselect_head(queue_73) = index_279,
inference(light_normalisation,[status(thm)],[c_3614,c_4349,c_4387]) ).
tcf(c_4517,plain,
index_9 = index_279,
inference(light_normalisation,[status(thm)],[c_4215,c_4221,c_4412]) ).
tcf(c_4589,plain,
select(earray_278,index_9) = elem_280,
inference(demodulation,[status(thm)],[c_506,c_4517]) ).
tcf(c_4590,plain,
elem_280 = elem_283,
inference(demodulation,[status(thm)],[c_3974,c_4589]) ).
tcf(c_4591,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4590,c_1332]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 20:38:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 6.30/1.71 % SZS status Started for theBenchmark.p
% 6.30/1.71 % SZS status Unsatisfiable for theBenchmark.p
% 6.30/1.71
% 6.30/1.71 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.30/1.71
% 6.30/1.71 % ------ iProver source info
% 6.30/1.71
% 6.30/1.71 % git: date: 2026-07-19 20:42:38 +0200
% 6.30/1.71 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.30/1.71 % git: non_committed_changes: false
% 6.30/1.71
% 6.30/1.71 % ------ Parsing...% successful
% 6.30/1.71
% 6.30/1.71
% 6.30/1.71 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.30/1.71
% 6.30/1.71 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.30/1.71
% 6.30/1.71 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.30/1.71
% 6.30/1.71 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.30/1.71 % ------ Proving...
% 6.30/1.71 % ------ Problem Properties
% 6.30/1.71
% 6.30/1.71 %
% 6.30/1.71 % clauses 301
% 6.30/1.71 % conjectures 1
% 6.30/1.71 % EPR 1
% 6.30/1.71 % Horn 300
% 6.30/1.71 % unary 300
% 6.30/1.71 % binary 1
% 6.30/1.71 % lits 302
% 6.30/1.71 % lits eq 302
% 6.30/1.71 % fd_pure 0
% 6.30/1.71 % fd_pseudo 0
% 6.30/1.71 % fd_cond 0
% 6.30/1.71 % fd_pseudo_cond 1
% 6.30/1.71 % AC symbols 0
% 6.30/1.71
% 6.30/1.71 % ------ Schedule dynamic 5 is on
% 6.30/1.71
% 6.30/1.71 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.30/1.71
% 6.30/1.71
% 6.30/1.71 % ------
% 6.30/1.71 % Current options:
% 6.30/1.71 % ------
% 6.30/1.71
% 6.30/1.71
% 6.30/1.71 %
% 6.30/1.71
% 6.30/1.71 % ------ Proving...
% 6.30/1.71 %
% 6.30/1.71
% 6.30/1.71 % SZS status Unsatisfiable for theBenchmark.p
% 6.30/1.71
% 6.30/1.71 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.30/1.74
% 6.30/1.74
%------------------------------------------------------------------------------