%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:18:59 PM UTC 2026
% Result : Unsatisfiable 2.92s 1.13s
% Output : Refutation 4.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 236
% Syntax : Number of formulae : 743 ( 743 unt; 0 def)
% Number of atoms : 743 ( 742 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 279 ( 279 usr; 270 con; 0-3 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
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(f19,axiom,
! [X0] : s(s(s(X0))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circular) ).
fof(f67,axiom,
earray_224 = rselect_seq(q42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f68,axiom,
earray_226 = store(earray_224,index_225,e42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f80,axiom,
earray_260 = rselect_seq(q43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
fof(f107,axiom,
elem_262 = select(earray_260,index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp87) ).
fof(f108,axiom,
elem_265 = select(earray_260,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp88) ).
fof(f109,axiom,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp89) ).
fof(f110,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp90) ).
fof(f111,axiom,
index_105 = rselect_tail(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp91) ).
fof(f112,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
fof(f113,axiom,
index_111 = rselect_tail(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f114,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f115,axiom,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f116,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f117,axiom,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f118,axiom,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f119,axiom,
index_126 = s(index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f120,axiom,
index_129 = rselect_tail(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f121,axiom,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f122,axiom,
index_135 = rselect_tail(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f123,axiom,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f124,axiom,
index_141 = rselect_tail(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f125,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f126,axiom,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f127,axiom,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f128,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f129,axiom,
index_153 = rselect_tail(q31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f130,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f131,axiom,
index_159 = rselect_tail(q32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f132,axiom,
index_162 = s(index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f133,axiom,
index_165 = rselect_tail(q33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f134,axiom,
index_168 = s(index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f135,axiom,
index_171 = rselect_tail(q34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f136,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f137,axiom,
index_177 = rselect_tail(q35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f138,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f139,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f140,axiom,
index_183 = rselect_tail(q36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f141,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f142,axiom,
index_189 = rselect_tail(q37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f143,axiom,
index_192 = s(index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f144,axiom,
index_195 = rselect_tail(q38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f145,axiom,
index_198 = s(index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f146,axiom,
index_201 = rselect_tail(q3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f147,axiom,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f148,axiom,
index_207 = rselect_tail(q39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f149,axiom,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f150,axiom,
index_210 = s(index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f151,axiom,
index_213 = rselect_tail(q40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f152,axiom,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f153,axiom,
index_219 = rselect_tail(q41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f154,axiom,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f155,axiom,
index_225 = rselect_tail(q42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f156,axiom,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f157,axiom,
index_231 = rselect_tail(q4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f158,axiom,
index_234 = s(index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f159,axiom,
index_237 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f160,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f161,axiom,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f162,axiom,
index_243 = rselect_tail(q6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f163,axiom,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f164,axiom,
index_249 = rselect_tail(q7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f165,axiom,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f166,axiom,
index_255 = rselect_tail(q8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f167,axiom,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f168,axiom,
index_261 = rselect_head(q43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f169,axiom,
index_263 = rselect_tail(q43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f170,axiom,
s(index_264) = index_263,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f171,plain,
index_263 = s(index_264),
inference(reorient_equations,[],[f170]) ).
fof(f172,axiom,
index_27 = rselect_tail(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f173,axiom,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f174,axiom,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f175,axiom,
index_33 = rselect_tail(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f176,axiom,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f177,axiom,
index_39 = rselect_tail(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f178,axiom,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f179,axiom,
index_45 = rselect_tail(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f180,axiom,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f181,axiom,
index_51 = rselect_tail(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f182,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f183,axiom,
index_57 = rselect_tail(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f184,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f185,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f186,axiom,
index_63 = rselect_tail(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f187,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f188,axiom,
index_69 = rselect_tail(q1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f189,axiom,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f190,axiom,
index_75 = rselect_tail(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f191,axiom,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f192,axiom,
index_81 = rselect_tail(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f193,axiom,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f194,axiom,
index_87 = rselect_tail(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f195,axiom,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f196,axiom,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f197,axiom,
index_93 = rselect_tail(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f198,axiom,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f199,axiom,
index_99 = rselect_tail(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f200,axiom,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f201,axiom,
queue_101 = rstore_seq(q23,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f202,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f203,axiom,
queue_107 = rstore_seq(q24,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f204,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f205,axiom,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f206,axiom,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f207,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f208,axiom,
queue_119 = rstore_seq(q26,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f209,axiom,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f210,axiom,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f211,axiom,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f212,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f213,axiom,
queue_131 = rstore_seq(q28,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f214,axiom,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f215,axiom,
queue_137 = rstore_seq(q2,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f216,axiom,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f217,axiom,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f218,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f219,axiom,
queue_149 = rstore_seq(q30,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f220,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f221,axiom,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f222,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f223,axiom,
queue_161 = rstore_seq(q32,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f224,axiom,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f225,axiom,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f226,axiom,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f227,axiom,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f228,axiom,
queue_173 = rstore_seq(q34,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f229,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f230,axiom,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f231,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f232,axiom,
queue_185 = rstore_seq(q36,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f233,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f234,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f235,axiom,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f236,axiom,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f237,axiom,
queue_197 = rstore_seq(q38,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f238,axiom,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f239,axiom,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f240,axiom,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f241,axiom,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f242,axiom,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f243,axiom,
queue_215 = rstore_seq(q40,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f244,axiom,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f245,axiom,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f246,axiom,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f247,axiom,
queue_227 = rstore_seq(q42,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f248,axiom,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f249,axiom,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f250,axiom,
queue_233 = rstore_seq(q4,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f251,axiom,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f252,axiom,
queue_239 = rstore_seq(q5,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f253,axiom,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f254,axiom,
queue_245 = rstore_seq(q6,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f255,axiom,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f256,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f257,axiom,
queue_251 = rstore_seq(q7,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f258,axiom,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f259,axiom,
queue_257 = rstore_seq(q8,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f260,axiom,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f261,axiom,
queue_29 = rstore_seq(q12,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f262,axiom,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f263,axiom,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f264,axiom,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f265,axiom,
queue_41 = rstore_seq(q14,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f266,axiom,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f267,axiom,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f268,axiom,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f269,axiom,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f270,axiom,
queue_53 = rstore_seq(q16,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f271,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f272,axiom,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f273,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f274,axiom,
queue_65 = rstore_seq(q18,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f275,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f276,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f277,axiom,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f278,axiom,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f279,axiom,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f280,axiom,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f281,axiom,
queue_83 = rstore_seq(q20,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f282,axiom,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f283,axiom,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f284,axiom,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f285,axiom,
queue_95 = rstore_seq(q22,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f286,axiom,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f287,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp266) ).
fof(f288,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f289,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f290,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f291,axiom,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f292,axiom,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f293,axiom,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f294,axiom,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f295,axiom,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f296,axiom,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f297,axiom,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f298,axiom,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f299,axiom,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f300,axiom,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f301,axiom,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f302,axiom,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f303,axiom,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f304,axiom,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f305,axiom,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f306,axiom,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f307,axiom,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f308,axiom,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f309,axiom,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f310,axiom,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f311,axiom,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f312,axiom,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f313,axiom,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f314,axiom,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f315,axiom,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f316,axiom,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f317,axiom,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f318,axiom,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f319,axiom,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f320,axiom,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f321,axiom,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f322,axiom,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f323,axiom,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f324,axiom,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f325,axiom,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f326,axiom,
q5 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f327,axiom,
q6 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f328,axiom,
q7 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f329,axiom,
q8 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f330,axiom,
q9 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f331,negated_conjecture,
elem_262 != elem_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f334,plain,
index_99 = s(s(index_102)),
inference(superposition,[],[f19,f110]) ).
fof(f343,plain,
index_9 = s(s(index_12)),
inference(superposition,[],[f19,f116]) ).
fof(f355,plain,
index_135 = s(s(index_138)),
inference(superposition,[],[f19,f123]) ).
fof(f424,plain,
index_264 = s(s(index_263)),
inference(superposition,[],[f19,f171]) ).
fof(f442,plain,
index_3 = s(s(index_6)),
inference(superposition,[],[f19,f184]) ).
fof(f464,plain,
q0 = rstore_head(q,index_0),
inference(forward_demodulation,[],[f200,f287]) ).
fof(f467,plain,
rselect_head(q23) = rselect_head(queue_101),
inference(superposition,[],[f11,f201]) ).
fof(f469,plain,
q24 = rstore_tail(queue_101,index_102),
inference(forward_demodulation,[],[f202,f304]) ).
fof(f472,plain,
rselect_head(q24) = rselect_head(queue_107),
inference(superposition,[],[f11,f203]) ).
fof(f474,plain,
q25 = rstore_tail(queue_107,index_108),
inference(forward_demodulation,[],[f204,f305]) ).
fof(f477,plain,
rselect_head(q9) = rselect_head(queue_11),
inference(superposition,[],[f11,f205]) ).
fof(f481,plain,
rselect_head(q25) = rselect_head(queue_113),
inference(superposition,[],[f11,f206]) ).
fof(f483,plain,
q26 = rstore_tail(queue_113,index_114),
inference(forward_demodulation,[],[f207,f306]) ).
fof(f486,plain,
rselect_head(q26) = rselect_head(queue_119),
inference(superposition,[],[f11,f208]) ).
fof(f488,plain,
q27 = rstore_tail(queue_119,index_120),
inference(forward_demodulation,[],[f209,f307]) ).
fof(f491,plain,
rselect_head(q27) = rselect_head(queue_125),
inference(superposition,[],[f11,f210]) ).
fof(f493,plain,
q28 = rstore_tail(queue_125,index_126),
inference(forward_demodulation,[],[f211,f308]) ).
fof(f494,plain,
q10 = rstore_tail(queue_11,index_12),
inference(forward_demodulation,[],[f212,f289]) ).
fof(f497,plain,
rselect_head(q28) = rselect_head(queue_131),
inference(superposition,[],[f11,f213]) ).
fof(f499,plain,
q29 = rstore_tail(queue_131,index_132),
inference(forward_demodulation,[],[f214,f309]) ).
fof(f502,plain,
rselect_head(q2) = rselect_head(queue_137),
inference(superposition,[],[f11,f215]) ).
fof(f504,plain,
q3 = rstore_tail(queue_137,index_138),
inference(forward_demodulation,[],[f216,f310]) ).
fof(f507,plain,
rselect_head(q29) = rselect_head(queue_143),
inference(superposition,[],[f11,f217]) ).
fof(f509,plain,
q30 = rstore_tail(queue_143,index_144),
inference(forward_demodulation,[],[f218,f311]) ).
fof(f512,plain,
rselect_head(q30) = rselect_head(queue_149),
inference(superposition,[],[f11,f219]) ).
fof(f514,plain,
q31 = rstore_tail(queue_149,index_150),
inference(forward_demodulation,[],[f220,f312]) ).
fof(f517,plain,
rselect_head(q31) = rselect_head(queue_155),
inference(superposition,[],[f11,f221]) ).
fof(f519,plain,
q32 = rstore_tail(queue_155,index_156),
inference(forward_demodulation,[],[f222,f313]) ).
fof(f522,plain,
rselect_head(q32) = rselect_head(queue_161),
inference(superposition,[],[f11,f223]) ).
fof(f524,plain,
q33 = rstore_tail(queue_161,index_162),
inference(forward_demodulation,[],[f224,f314]) ).
fof(f527,plain,
rselect_head(q33) = rselect_head(queue_167),
inference(superposition,[],[f11,f225]) ).
fof(f529,plain,
q34 = rstore_tail(queue_167,index_168),
inference(forward_demodulation,[],[f226,f315]) ).
fof(f532,plain,
rselect_head(q10) = rselect_head(queue_17),
inference(superposition,[],[f11,f227]) ).
fof(f536,plain,
rselect_head(q34) = rselect_head(queue_173),
inference(superposition,[],[f11,f228]) ).
fof(f538,plain,
q35 = rstore_tail(queue_173,index_174),
inference(forward_demodulation,[],[f229,f316]) ).
fof(f541,plain,
rselect_head(q35) = rselect_head(queue_179),
inference(superposition,[],[f11,f230]) ).
fof(f543,plain,
q36 = rstore_tail(queue_179,index_180),
inference(forward_demodulation,[],[f231,f317]) ).
fof(f546,plain,
rselect_head(q36) = rselect_head(queue_185),
inference(superposition,[],[f11,f232]) ).
fof(f548,plain,
q37 = rstore_tail(queue_185,index_186),
inference(forward_demodulation,[],[f233,f318]) ).
fof(f549,plain,
q11 = rstore_tail(queue_17,index_18),
inference(forward_demodulation,[],[f234,f290]) ).
fof(f552,plain,
rselect_head(q37) = rselect_head(queue_191),
inference(superposition,[],[f11,f235]) ).
fof(f554,plain,
q38 = rstore_tail(queue_191,index_192),
inference(forward_demodulation,[],[f236,f319]) ).
fof(f557,plain,
rselect_head(q38) = rselect_head(queue_197),
inference(superposition,[],[f11,f237]) ).
fof(f559,plain,
q39 = rstore_tail(queue_197,index_198),
inference(forward_demodulation,[],[f238,f320]) ).
fof(f562,plain,
rselect_head(q3) = rselect_head(queue_203),
inference(superposition,[],[f11,f239]) ).
fof(f564,plain,
q4 = rstore_tail(queue_203,index_204),
inference(forward_demodulation,[],[f240,f321]) ).
fof(f567,plain,
rselect_head(q39) = rselect_head(queue_209),
inference(superposition,[],[f11,f241]) ).
fof(f569,plain,
q40 = rstore_tail(queue_209,index_210),
inference(forward_demodulation,[],[f242,f322]) ).
fof(f572,plain,
rselect_head(q40) = rselect_head(queue_215),
inference(superposition,[],[f11,f243]) ).
fof(f574,plain,
q41 = rstore_tail(queue_215,index_216),
inference(forward_demodulation,[],[f244,f323]) ).
fof(f575,plain,
earray_220 = rselect_seq(queue_221),
inference(superposition,[],[f3,f245]) ).
fof(f577,plain,
rselect_head(q41) = rselect_head(queue_221),
inference(superposition,[],[f11,f245]) ).
fof(f579,plain,
q42 = rstore_tail(queue_221,index_222),
inference(forward_demodulation,[],[f246,f324]) ).
fof(f580,plain,
earray_226 = rselect_seq(queue_227),
inference(superposition,[],[f3,f247]) ).
fof(f582,plain,
rselect_head(q42) = rselect_head(queue_227),
inference(superposition,[],[f11,f247]) ).
fof(f584,plain,
q43 = rstore_tail(queue_227,index_228),
inference(forward_demodulation,[],[f248,f325]) ).
fof(f587,plain,
rselect_head(q11) = rselect_head(queue_23),
inference(superposition,[],[f11,f249]) ).
fof(f591,plain,
rselect_head(q4) = rselect_head(queue_233),
inference(superposition,[],[f11,f250]) ).
fof(f593,plain,
q5 = rstore_tail(queue_233,index_234),
inference(forward_demodulation,[],[f251,f326]) ).
fof(f596,plain,
rselect_head(q5) = rselect_head(queue_239),
inference(superposition,[],[f11,f252]) ).
fof(f598,plain,
q6 = rstore_tail(queue_239,index_240),
inference(forward_demodulation,[],[f253,f327]) ).
fof(f601,plain,
rselect_head(q6) = rselect_head(queue_245),
inference(superposition,[],[f11,f254]) ).
fof(f603,plain,
q7 = rstore_tail(queue_245,index_246),
inference(forward_demodulation,[],[f255,f328]) ).
fof(f604,plain,
q12 = rstore_tail(queue_23,index_24),
inference(forward_demodulation,[],[f256,f291]) ).
fof(f607,plain,
rselect_head(q7) = rselect_head(queue_251),
inference(superposition,[],[f11,f257]) ).
fof(f609,plain,
q8 = rstore_tail(queue_251,index_252),
inference(forward_demodulation,[],[f258,f329]) ).
fof(f612,plain,
rselect_head(q8) = rselect_head(queue_257),
inference(superposition,[],[f11,f259]) ).
fof(f614,plain,
q9 = rstore_tail(queue_257,index_258),
inference(forward_demodulation,[],[f260,f330]) ).
fof(f617,plain,
rselect_head(q12) = rselect_head(queue_29),
inference(superposition,[],[f11,f261]) ).
fof(f619,plain,
q13 = rstore_tail(queue_29,index_30),
inference(forward_demodulation,[],[f262,f292]) ).
fof(f622,plain,
rselect_head(q13) = rselect_head(queue_35),
inference(superposition,[],[f11,f263]) ).
fof(f624,plain,
q14 = rstore_tail(queue_35,index_36),
inference(forward_demodulation,[],[f264,f293]) ).
fof(f627,plain,
rselect_head(q14) = rselect_head(queue_41),
inference(superposition,[],[f11,f265]) ).
fof(f629,plain,
q15 = rstore_tail(queue_41,index_42),
inference(forward_demodulation,[],[f266,f294]) ).
fof(f632,plain,
rselect_head(q15) = rselect_head(queue_47),
inference(superposition,[],[f11,f267]) ).
fof(f634,plain,
q16 = rstore_tail(queue_47,index_48),
inference(forward_demodulation,[],[f268,f295]) ).
fof(f637,plain,
rselect_head(q0) = rselect_head(queue_5),
inference(superposition,[],[f11,f269]) ).
fof(f641,plain,
rselect_head(q16) = rselect_head(queue_53),
inference(superposition,[],[f11,f270]) ).
fof(f643,plain,
q17 = rstore_tail(queue_53,index_54),
inference(forward_demodulation,[],[f271,f296]) ).
fof(f646,plain,
rselect_head(q17) = rselect_head(queue_59),
inference(superposition,[],[f11,f272]) ).
fof(f648,plain,
q18 = rstore_tail(queue_59,index_60),
inference(forward_demodulation,[],[f273,f297]) ).
fof(f651,plain,
rselect_head(q18) = rselect_head(queue_65),
inference(superposition,[],[f11,f274]) ).
fof(f653,plain,
q19 = rstore_tail(queue_65,index_66),
inference(forward_demodulation,[],[f275,f298]) ).
fof(f654,plain,
q1 = rstore_tail(queue_5,index_6),
inference(forward_demodulation,[],[f276,f288]) ).
fof(f657,plain,
rselect_head(q1) = rselect_head(queue_71),
inference(superposition,[],[f11,f277]) ).
fof(f659,plain,
q2 = rstore_tail(queue_71,index_72),
inference(forward_demodulation,[],[f278,f299]) ).
fof(f662,plain,
rselect_head(q19) = rselect_head(queue_77),
inference(superposition,[],[f11,f279]) ).
fof(f664,plain,
q20 = rstore_tail(queue_77,index_78),
inference(forward_demodulation,[],[f280,f300]) ).
fof(f667,plain,
rselect_head(q20) = rselect_head(queue_83),
inference(superposition,[],[f11,f281]) ).
fof(f669,plain,
q21 = rstore_tail(queue_83,index_84),
inference(forward_demodulation,[],[f282,f301]) ).
fof(f672,plain,
rselect_head(q21) = rselect_head(queue_89),
inference(superposition,[],[f11,f283]) ).
fof(f674,plain,
q22 = rstore_tail(queue_89,index_90),
inference(forward_demodulation,[],[f284,f302]) ).
fof(f677,plain,
rselect_head(q22) = rselect_head(queue_95),
inference(superposition,[],[f11,f285]) ).
fof(f679,plain,
q23 = rstore_tail(queue_95,index_96),
inference(forward_demodulation,[],[f286,f303]) ).
fof(f681,plain,
rselect_tail(q) = rselect_tail(q0),
inference(superposition,[],[f14,f464]) ).
fof(f682,plain,
index_0 = rselect_head(q0),
inference(superposition,[],[f4,f464]) ).
fof(f683,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[],[f681,f173]) ).
fof(f685,plain,
index_3 = index_0,
inference(forward_demodulation,[],[f683,f109]) ).
fof(f687,plain,
index_3 = rselect_head(q0),
inference(forward_demodulation,[],[f682,f685]) ).
fof(f688,plain,
index_102 = rselect_tail(q24),
inference(superposition,[],[f5,f469]) ).
fof(f690,plain,
rselect_head(queue_101) = rselect_head(q24),
inference(superposition,[],[f9,f469]) ).
fof(f692,plain,
index_105 = index_102,
inference(forward_demodulation,[],[f688,f111]) ).
fof(f698,plain,
index_108 = rselect_tail(q25),
inference(superposition,[],[f5,f474]) ).
fof(f700,plain,
rselect_head(queue_107) = rselect_head(q25),
inference(superposition,[],[f9,f474]) ).
fof(f702,plain,
index_111 = index_108,
inference(forward_demodulation,[],[f698,f113]) ).
fof(f709,plain,
index_114 = rselect_tail(q26),
inference(superposition,[],[f5,f483]) ).
fof(f711,plain,
rselect_head(queue_113) = rselect_head(q26),
inference(superposition,[],[f9,f483]) ).
fof(f713,plain,
index_117 = index_114,
inference(forward_demodulation,[],[f709,f115]) ).
fof(f719,plain,
index_120 = rselect_tail(q27),
inference(superposition,[],[f5,f488]) ).
fof(f721,plain,
rselect_head(queue_119) = rselect_head(q27),
inference(superposition,[],[f9,f488]) ).
fof(f723,plain,
index_123 = index_120,
inference(forward_demodulation,[],[f719,f118]) ).
fof(f730,plain,
index_126 = rselect_tail(q28),
inference(superposition,[],[f5,f493]) ).
fof(f732,plain,
rselect_head(queue_125) = rselect_head(q28),
inference(superposition,[],[f9,f493]) ).
fof(f734,plain,
index_129 = index_126,
inference(forward_demodulation,[],[f730,f120]) ).
fof(f740,plain,
index_12 = rselect_tail(q10),
inference(superposition,[],[f5,f494]) ).
fof(f742,plain,
rselect_head(queue_11) = rselect_head(q10),
inference(superposition,[],[f9,f494]) ).
fof(f744,plain,
index_15 = index_12,
inference(forward_demodulation,[],[f740,f127]) ).
fof(f750,plain,
index_132 = rselect_tail(q29),
inference(superposition,[],[f5,f499]) ).
fof(f752,plain,
rselect_head(queue_131) = rselect_head(q29),
inference(superposition,[],[f9,f499]) ).
fof(f754,plain,
index_141 = index_132,
inference(forward_demodulation,[],[f750,f124]) ).
fof(f761,plain,
index_138 = rselect_tail(q3),
inference(superposition,[],[f5,f504]) ).
fof(f763,plain,
rselect_head(queue_137) = rselect_head(q3),
inference(superposition,[],[f9,f504]) ).
fof(f765,plain,
index_201 = index_138,
inference(forward_demodulation,[],[f761,f146]) ).
fof(f771,plain,
index_144 = rselect_tail(q30),
inference(superposition,[],[f5,f509]) ).
fof(f773,plain,
rselect_head(queue_143) = rselect_head(q30),
inference(superposition,[],[f9,f509]) ).
fof(f775,plain,
index_147 = index_144,
inference(forward_demodulation,[],[f771,f126]) ).
fof(f782,plain,
index_150 = rselect_tail(q31),
inference(superposition,[],[f5,f514]) ).
fof(f784,plain,
rselect_head(queue_149) = rselect_head(q31),
inference(superposition,[],[f9,f514]) ).
fof(f786,plain,
index_153 = index_150,
inference(forward_demodulation,[],[f782,f129]) ).
fof(f792,plain,
index_156 = rselect_tail(q32),
inference(superposition,[],[f5,f519]) ).
fof(f794,plain,
rselect_head(queue_155) = rselect_head(q32),
inference(superposition,[],[f9,f519]) ).
fof(f796,plain,
index_159 = index_156,
inference(forward_demodulation,[],[f792,f131]) ).
fof(f802,plain,
index_162 = rselect_tail(q33),
inference(superposition,[],[f5,f524]) ).
fof(f804,plain,
rselect_head(queue_161) = rselect_head(q33),
inference(superposition,[],[f9,f524]) ).
fof(f806,plain,
index_165 = index_162,
inference(forward_demodulation,[],[f802,f133]) ).
fof(f813,plain,
index_168 = rselect_tail(q34),
inference(superposition,[],[f5,f529]) ).
fof(f815,plain,
rselect_head(queue_167) = rselect_head(q34),
inference(superposition,[],[f9,f529]) ).
fof(f817,plain,
index_171 = index_168,
inference(forward_demodulation,[],[f813,f135]) ).
fof(f823,plain,
index_174 = rselect_tail(q35),
inference(superposition,[],[f5,f538]) ).
fof(f825,plain,
rselect_head(queue_173) = rselect_head(q35),
inference(superposition,[],[f9,f538]) ).
fof(f827,plain,
index_177 = index_174,
inference(forward_demodulation,[],[f823,f137]) ).
fof(f833,plain,
index_180 = rselect_tail(q36),
inference(superposition,[],[f5,f543]) ).
fof(f835,plain,
rselect_head(queue_179) = rselect_head(q36),
inference(superposition,[],[f9,f543]) ).
fof(f837,plain,
index_183 = index_180,
inference(forward_demodulation,[],[f833,f140]) ).
fof(f843,plain,
index_186 = rselect_tail(q37),
inference(superposition,[],[f5,f548]) ).
fof(f845,plain,
rselect_head(queue_185) = rselect_head(q37),
inference(superposition,[],[f9,f548]) ).
fof(f847,plain,
index_189 = index_186,
inference(forward_demodulation,[],[f843,f142]) ).
fof(f854,plain,
index_18 = rselect_tail(q11),
inference(superposition,[],[f5,f549]) ).
fof(f856,plain,
rselect_head(queue_17) = rselect_head(q11),
inference(superposition,[],[f9,f549]) ).
fof(f858,plain,
index_21 = index_18,
inference(forward_demodulation,[],[f854,f149]) ).
fof(f865,plain,
index_192 = rselect_tail(q38),
inference(superposition,[],[f5,f554]) ).
fof(f867,plain,
rselect_head(queue_191) = rselect_head(q38),
inference(superposition,[],[f9,f554]) ).
fof(f869,plain,
index_195 = index_192,
inference(forward_demodulation,[],[f865,f144]) ).
fof(f875,plain,
index_198 = rselect_tail(q39),
inference(superposition,[],[f5,f559]) ).
fof(f877,plain,
rselect_head(queue_197) = rselect_head(q39),
inference(superposition,[],[f9,f559]) ).
fof(f879,plain,
index_207 = index_198,
inference(forward_demodulation,[],[f875,f148]) ).
fof(f885,plain,
index_204 = rselect_tail(q4),
inference(superposition,[],[f5,f564]) ).
fof(f887,plain,
rselect_head(queue_203) = rselect_head(q4),
inference(superposition,[],[f9,f564]) ).
fof(f889,plain,
index_231 = index_204,
inference(forward_demodulation,[],[f885,f157]) ).
fof(f896,plain,
index_210 = rselect_tail(q40),
inference(superposition,[],[f5,f569]) ).
fof(f898,plain,
rselect_head(queue_209) = rselect_head(q40),
inference(superposition,[],[f9,f569]) ).
fof(f900,plain,
index_213 = index_210,
inference(forward_demodulation,[],[f896,f151]) ).
fof(f907,plain,
index_216 = rselect_tail(q41),
inference(superposition,[],[f5,f574]) ).
fof(f909,plain,
rselect_head(queue_215) = rselect_head(q41),
inference(superposition,[],[f9,f574]) ).
fof(f911,plain,
index_219 = index_216,
inference(forward_demodulation,[],[f907,f153]) ).
fof(f917,plain,
index_222 = rselect_tail(q42),
inference(superposition,[],[f5,f579]) ).
fof(f918,plain,
rselect_seq(q42) = rselect_seq(queue_221),
inference(superposition,[],[f8,f579]) ).
fof(f919,plain,
rselect_head(queue_221) = rselect_head(q42),
inference(superposition,[],[f9,f579]) ).
fof(f920,plain,
earray_220 = rselect_seq(q42),
inference(forward_demodulation,[],[f918,f575]) ).
fof(f921,plain,
index_225 = index_222,
inference(forward_demodulation,[],[f917,f155]) ).
fof(f922,plain,
earray_220 = earray_224,
inference(forward_demodulation,[],[f920,f67]) ).
fof(f927,plain,
index_228 = rselect_tail(q43),
inference(superposition,[],[f5,f584]) ).
fof(f928,plain,
rselect_seq(q43) = rselect_seq(queue_227),
inference(superposition,[],[f8,f584]) ).
fof(f929,plain,
rselect_head(q43) = rselect_head(queue_227),
inference(superposition,[],[f9,f584]) ).
fof(f930,plain,
index_261 = rselect_head(queue_227),
inference(forward_demodulation,[],[f929,f168]) ).
fof(f931,plain,
earray_226 = rselect_seq(q43),
inference(forward_demodulation,[],[f928,f580]) ).
fof(f932,plain,
index_228 = index_263,
inference(forward_demodulation,[],[f927,f169]) ).
fof(f933,plain,
earray_226 = earray_260,
inference(forward_demodulation,[],[f931,f80]) ).
fof(f938,plain,
index_234 = rselect_tail(q5),
inference(superposition,[],[f5,f593]) ).
fof(f940,plain,
rselect_head(queue_233) = rselect_head(q5),
inference(superposition,[],[f9,f593]) ).
fof(f942,plain,
index_237 = index_234,
inference(forward_demodulation,[],[f938,f159]) ).
fof(f948,plain,
index_240 = rselect_tail(q6),
inference(superposition,[],[f5,f598]) ).
fof(f950,plain,
rselect_head(queue_239) = rselect_head(q6),
inference(superposition,[],[f9,f598]) ).
fof(f952,plain,
index_243 = index_240,
inference(forward_demodulation,[],[f948,f162]) ).
fof(f959,plain,
index_246 = rselect_tail(q7),
inference(superposition,[],[f5,f603]) ).
fof(f961,plain,
rselect_head(queue_245) = rselect_head(q7),
inference(superposition,[],[f9,f603]) ).
fof(f963,plain,
index_249 = index_246,
inference(forward_demodulation,[],[f959,f164]) ).
fof(f969,plain,
index_24 = rselect_tail(q12),
inference(superposition,[],[f5,f604]) ).
fof(f971,plain,
rselect_head(queue_23) = rselect_head(q12),
inference(superposition,[],[f9,f604]) ).
fof(f973,plain,
index_27 = index_24,
inference(forward_demodulation,[],[f969,f172]) ).
fof(f980,plain,
index_252 = rselect_tail(q8),
inference(superposition,[],[f5,f609]) ).
fof(f982,plain,
rselect_head(queue_251) = rselect_head(q8),
inference(superposition,[],[f9,f609]) ).
fof(f984,plain,
index_255 = index_252,
inference(forward_demodulation,[],[f980,f166]) ).
fof(f990,plain,
index_258 = rselect_tail(q9),
inference(superposition,[],[f5,f614]) ).
fof(f992,plain,
rselect_head(q9) = rselect_head(queue_257),
inference(superposition,[],[f9,f614]) ).
fof(f994,plain,
index_9 = index_258,
inference(forward_demodulation,[],[f990,f195]) ).
fof(f1002,plain,
index_30 = rselect_tail(q13),
inference(superposition,[],[f5,f619]) ).
fof(f1004,plain,
rselect_head(queue_29) = rselect_head(q13),
inference(superposition,[],[f9,f619]) ).
fof(f1006,plain,
index_33 = index_30,
inference(forward_demodulation,[],[f1002,f175]) ).
fof(f1013,plain,
index_36 = rselect_tail(q14),
inference(superposition,[],[f5,f624]) ).
fof(f1015,plain,
rselect_head(queue_35) = rselect_head(q14),
inference(superposition,[],[f9,f624]) ).
fof(f1017,plain,
index_39 = index_36,
inference(forward_demodulation,[],[f1013,f177]) ).
fof(f1023,plain,
index_42 = rselect_tail(q15),
inference(superposition,[],[f5,f629]) ).
fof(f1025,plain,
rselect_head(queue_41) = rselect_head(q15),
inference(superposition,[],[f9,f629]) ).
fof(f1027,plain,
index_45 = index_42,
inference(forward_demodulation,[],[f1023,f179]) ).
fof(f1034,plain,
index_48 = rselect_tail(q16),
inference(superposition,[],[f5,f634]) ).
fof(f1036,plain,
rselect_head(queue_47) = rselect_head(q16),
inference(superposition,[],[f9,f634]) ).
fof(f1038,plain,
index_51 = index_48,
inference(forward_demodulation,[],[f1034,f181]) ).
fof(f1044,plain,
index_54 = rselect_tail(q17),
inference(superposition,[],[f5,f643]) ).
fof(f1046,plain,
rselect_head(queue_53) = rselect_head(q17),
inference(superposition,[],[f9,f643]) ).
fof(f1048,plain,
index_57 = index_54,
inference(forward_demodulation,[],[f1044,f183]) ).
fof(f1055,plain,
index_60 = rselect_tail(q18),
inference(superposition,[],[f5,f648]) ).
fof(f1057,plain,
rselect_head(queue_59) = rselect_head(q18),
inference(superposition,[],[f9,f648]) ).
fof(f1059,plain,
index_63 = index_60,
inference(forward_demodulation,[],[f1055,f186]) ).
fof(f1065,plain,
index_66 = rselect_tail(q19),
inference(superposition,[],[f5,f653]) ).
fof(f1067,plain,
rselect_head(queue_65) = rselect_head(q19),
inference(superposition,[],[f9,f653]) ).
fof(f1069,plain,
index_75 = index_66,
inference(forward_demodulation,[],[f1065,f190]) ).
fof(f1076,plain,
index_6 = rselect_tail(q1),
inference(superposition,[],[f5,f654]) ).
fof(f1078,plain,
rselect_head(queue_5) = rselect_head(q1),
inference(superposition,[],[f9,f654]) ).
fof(f1080,plain,
index_69 = index_6,
inference(forward_demodulation,[],[f1076,f188]) ).
fof(f1086,plain,
rselect_tail(q2) = index_72,
inference(superposition,[],[f5,f659]) ).
fof(f1088,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(superposition,[],[f9,f659]) ).
fof(f1090,plain,
index_135 = index_72,
inference(forward_demodulation,[],[f1086,f122]) ).
fof(f1098,plain,
index_78 = rselect_tail(q20),
inference(superposition,[],[f5,f664]) ).
fof(f1100,plain,
rselect_head(queue_77) = rselect_head(q20),
inference(superposition,[],[f9,f664]) ).
fof(f1102,plain,
index_81 = index_78,
inference(forward_demodulation,[],[f1098,f192]) ).
fof(f1109,plain,
index_84 = rselect_tail(q21),
inference(superposition,[],[f5,f669]) ).
fof(f1111,plain,
rselect_head(queue_83) = rselect_head(q21),
inference(superposition,[],[f9,f669]) ).
fof(f1113,plain,
index_87 = index_84,
inference(forward_demodulation,[],[f1109,f194]) ).
fof(f1119,plain,
index_90 = rselect_tail(q22),
inference(superposition,[],[f5,f674]) ).
fof(f1121,plain,
rselect_head(queue_89) = rselect_head(q22),
inference(superposition,[],[f9,f674]) ).
fof(f1123,plain,
index_93 = index_90,
inference(forward_demodulation,[],[f1119,f197]) ).
fof(f1130,plain,
index_96 = rselect_tail(q23),
inference(superposition,[],[f5,f679]) ).
fof(f1132,plain,
rselect_head(q23) = rselect_head(queue_95),
inference(superposition,[],[f9,f679]) ).
fof(f1134,plain,
index_99 = index_96,
inference(forward_demodulation,[],[f1130,f199]) ).
fof(f1189,plain,
earray_226 = store(earray_220,index_225,e42),
inference(forward_demodulation,[],[f68,f922]) ).
fof(f1190,plain,
earray_260 = store(earray_220,index_225,e42),
inference(forward_demodulation,[],[f1189,f933]) ).
fof(f1195,plain,
index_99 = s(s(index_105)),
inference(forward_demodulation,[],[f334,f692]) ).
fof(f1196,plain,
index_99 = s(index_108),
inference(forward_demodulation,[],[f1195,f112]) ).
fof(f1197,plain,
index_99 = s(index_111),
inference(forward_demodulation,[],[f1196,f702]) ).
fof(f1198,plain,
index_99 = index_114,
inference(forward_demodulation,[],[f1197,f114]) ).
fof(f1199,plain,
index_99 = index_117,
inference(forward_demodulation,[],[f1198,f713]) ).
fof(f1202,plain,
s(index_99) = index_120,
inference(superposition,[],[f117,f1199]) ).
fof(f1203,plain,
index_123 = s(index_99),
inference(forward_demodulation,[],[f1202,f723]) ).
fof(f1204,plain,
index_123 = index_102,
inference(forward_demodulation,[],[f1203,f110]) ).
fof(f1205,plain,
index_105 = index_123,
inference(forward_demodulation,[],[f1204,f692]) ).
fof(f1208,plain,
s(index_105) = index_126,
inference(superposition,[],[f119,f1205]) ).
fof(f1209,plain,
index_129 = s(index_105),
inference(forward_demodulation,[],[f1208,f734]) ).
fof(f1210,plain,
index_129 = index_108,
inference(forward_demodulation,[],[f1209,f112]) ).
fof(f1211,plain,
index_111 = index_129,
inference(forward_demodulation,[],[f1210,f702]) ).
fof(f1216,plain,
s(index_111) = index_132,
inference(superposition,[],[f121,f1211]) ).
fof(f1217,plain,
index_141 = s(index_111),
inference(forward_demodulation,[],[f1216,f754]) ).
fof(f1218,plain,
index_141 = index_114,
inference(forward_demodulation,[],[f1217,f114]) ).
fof(f1219,plain,
index_117 = index_141,
inference(forward_demodulation,[],[f1218,f713]) ).
fof(f1220,plain,
index_99 = index_141,
inference(forward_demodulation,[],[f1219,f1199]) ).
fof(f1223,plain,
s(index_99) = index_144,
inference(superposition,[],[f125,f1220]) ).
fof(f1224,plain,
index_147 = s(index_99),
inference(forward_demodulation,[],[f1223,f775]) ).
fof(f1227,plain,
index_147 = index_102,
inference(forward_demodulation,[],[f1224,f110]) ).
fof(f1228,plain,
index_105 = index_147,
inference(forward_demodulation,[],[f1227,f692]) ).
fof(f1231,plain,
s(index_105) = index_150,
inference(superposition,[],[f128,f1228]) ).
fof(f1232,plain,
index_153 = s(index_105),
inference(forward_demodulation,[],[f1231,f786]) ).
fof(f1235,plain,
index_153 = index_108,
inference(forward_demodulation,[],[f1232,f112]) ).
fof(f1236,plain,
index_111 = index_153,
inference(forward_demodulation,[],[f1235,f702]) ).
fof(f1240,plain,
s(index_111) = index_156,
inference(superposition,[],[f130,f1236]) ).
fof(f1241,plain,
index_159 = s(index_111),
inference(forward_demodulation,[],[f1240,f796]) ).
fof(f1244,plain,
index_159 = index_114,
inference(forward_demodulation,[],[f1241,f114]) ).
fof(f1245,plain,
index_117 = index_159,
inference(forward_demodulation,[],[f1244,f713]) ).
fof(f1246,plain,
index_99 = index_159,
inference(forward_demodulation,[],[f1245,f1199]) ).
fof(f1249,plain,
s(index_99) = index_162,
inference(superposition,[],[f132,f1246]) ).
fof(f1250,plain,
index_165 = s(index_99),
inference(forward_demodulation,[],[f1249,f806]) ).
fof(f1253,plain,
index_165 = index_102,
inference(forward_demodulation,[],[f1250,f110]) ).
fof(f1254,plain,
index_105 = index_165,
inference(forward_demodulation,[],[f1253,f692]) ).
fof(f1257,plain,
s(index_105) = index_168,
inference(superposition,[],[f134,f1254]) ).
fof(f1258,plain,
index_171 = s(index_105),
inference(forward_demodulation,[],[f1257,f817]) ).
fof(f1261,plain,
index_171 = index_108,
inference(forward_demodulation,[],[f1258,f112]) ).
fof(f1262,plain,
index_111 = index_171,
inference(forward_demodulation,[],[f1261,f702]) ).
fof(f1266,plain,
s(index_111) = index_174,
inference(superposition,[],[f136,f1262]) ).
fof(f1267,plain,
index_177 = s(index_111),
inference(forward_demodulation,[],[f1266,f827]) ).
fof(f1270,plain,
index_177 = index_114,
inference(forward_demodulation,[],[f1267,f114]) ).
fof(f1271,plain,
index_117 = index_177,
inference(forward_demodulation,[],[f1270,f713]) ).
fof(f1272,plain,
index_99 = index_177,
inference(forward_demodulation,[],[f1271,f1199]) ).
fof(f1275,plain,
s(index_99) = index_180,
inference(superposition,[],[f139,f1272]) ).
fof(f1276,plain,
index_183 = s(index_99),
inference(forward_demodulation,[],[f1275,f837]) ).
fof(f1279,plain,
index_183 = index_102,
inference(forward_demodulation,[],[f1276,f110]) ).
fof(f1280,plain,
index_105 = index_183,
inference(forward_demodulation,[],[f1279,f692]) ).
fof(f1283,plain,
s(index_105) = index_186,
inference(superposition,[],[f141,f1280]) ).
fof(f1284,plain,
index_189 = s(index_105),
inference(forward_demodulation,[],[f1283,f847]) ).
fof(f1287,plain,
index_189 = index_108,
inference(forward_demodulation,[],[f1284,f112]) ).
fof(f1288,plain,
index_111 = index_189,
inference(forward_demodulation,[],[f1287,f702]) ).
fof(f1293,plain,
s(index_111) = index_192,
inference(superposition,[],[f143,f1288]) ).
fof(f1294,plain,
index_195 = s(index_111),
inference(forward_demodulation,[],[f1293,f869]) ).
fof(f1297,plain,
index_195 = index_114,
inference(forward_demodulation,[],[f1294,f114]) ).
fof(f1298,plain,
index_117 = index_195,
inference(forward_demodulation,[],[f1297,f713]) ).
fof(f1299,plain,
index_99 = index_195,
inference(forward_demodulation,[],[f1298,f1199]) ).
fof(f1302,plain,
s(index_99) = index_198,
inference(superposition,[],[f145,f1299]) ).
fof(f1303,plain,
index_207 = s(index_99),
inference(forward_demodulation,[],[f1302,f879]) ).
fof(f1306,plain,
index_207 = index_102,
inference(forward_demodulation,[],[f1303,f110]) ).
fof(f1307,plain,
index_105 = index_207,
inference(forward_demodulation,[],[f1306,f692]) ).
fof(f1310,plain,
s(index_105) = index_210,
inference(superposition,[],[f150,f1307]) ).
fof(f1311,plain,
index_213 = s(index_105),
inference(forward_demodulation,[],[f1310,f900]) ).
fof(f1314,plain,
index_213 = index_108,
inference(forward_demodulation,[],[f1311,f112]) ).
fof(f1315,plain,
index_111 = index_213,
inference(forward_demodulation,[],[f1314,f702]) ).
fof(f1319,plain,
s(index_111) = index_216,
inference(superposition,[],[f152,f1315]) ).
fof(f1320,plain,
index_219 = s(index_111),
inference(forward_demodulation,[],[f1319,f911]) ).
fof(f1323,plain,
index_219 = index_114,
inference(forward_demodulation,[],[f1320,f114]) ).
fof(f1324,plain,
index_117 = index_219,
inference(forward_demodulation,[],[f1323,f713]) ).
fof(f1325,plain,
index_99 = index_219,
inference(forward_demodulation,[],[f1324,f1199]) ).
fof(f1328,plain,
s(index_99) = index_222,
inference(superposition,[],[f154,f1325]) ).
fof(f1329,plain,
index_225 = s(index_99),
inference(forward_demodulation,[],[f1328,f921]) ).
fof(f1332,plain,
index_225 = index_102,
inference(forward_demodulation,[],[f1329,f110]) ).
fof(f1333,plain,
index_105 = index_225,
inference(forward_demodulation,[],[f1332,f692]) ).
fof(f1336,plain,
s(index_105) = index_228,
inference(superposition,[],[f156,f1333]) ).
fof(f1337,plain,
index_108 = index_228,
inference(forward_demodulation,[],[f1336,f112]) ).
fof(f1340,plain,
index_111 = index_228,
inference(forward_demodulation,[],[f1337,f702]) ).
fof(f1367,plain,
index_9 = s(s(index_15)),
inference(forward_demodulation,[],[f343,f744]) ).
fof(f1368,plain,
index_9 = s(index_18),
inference(forward_demodulation,[],[f1367,f138]) ).
fof(f1369,plain,
index_9 = s(index_21),
inference(forward_demodulation,[],[f1368,f858]) ).
fof(f1370,plain,
index_9 = index_24,
inference(forward_demodulation,[],[f1369,f160]) ).
fof(f1371,plain,
index_9 = index_27,
inference(forward_demodulation,[],[f1370,f973]) ).
fof(f1375,plain,
s(index_9) = index_30,
inference(superposition,[],[f174,f1371]) ).
fof(f1376,plain,
index_33 = s(index_9),
inference(forward_demodulation,[],[f1375,f1006]) ).
fof(f1377,plain,
index_33 = index_12,
inference(forward_demodulation,[],[f1376,f116]) ).
fof(f1378,plain,
index_15 = index_33,
inference(forward_demodulation,[],[f1377,f744]) ).
fof(f1381,plain,
s(index_15) = index_36,
inference(superposition,[],[f176,f1378]) ).
fof(f1382,plain,
index_39 = s(index_15),
inference(forward_demodulation,[],[f1381,f1017]) ).
fof(f1383,plain,
index_39 = index_18,
inference(forward_demodulation,[],[f1382,f138]) ).
fof(f1384,plain,
index_21 = index_39,
inference(forward_demodulation,[],[f1383,f858]) ).
fof(f1387,plain,
s(index_21) = index_42,
inference(superposition,[],[f178,f1384]) ).
fof(f1388,plain,
index_45 = s(index_21),
inference(forward_demodulation,[],[f1387,f1027]) ).
fof(f1389,plain,
index_45 = index_24,
inference(forward_demodulation,[],[f1388,f160]) ).
fof(f1390,plain,
index_27 = index_45,
inference(forward_demodulation,[],[f1389,f973]) ).
fof(f1391,plain,
index_9 = index_45,
inference(forward_demodulation,[],[f1390,f1371]) ).
fof(f1395,plain,
s(index_9) = index_48,
inference(superposition,[],[f180,f1391]) ).
fof(f1396,plain,
index_51 = s(index_9),
inference(forward_demodulation,[],[f1395,f1038]) ).
fof(f1399,plain,
index_51 = index_12,
inference(forward_demodulation,[],[f1396,f116]) ).
fof(f1400,plain,
index_15 = index_51,
inference(forward_demodulation,[],[f1399,f744]) ).
fof(f1403,plain,
s(index_15) = index_54,
inference(superposition,[],[f182,f1400]) ).
fof(f1404,plain,
index_57 = s(index_15),
inference(forward_demodulation,[],[f1403,f1048]) ).
fof(f1407,plain,
index_57 = index_18,
inference(forward_demodulation,[],[f1404,f138]) ).
fof(f1408,plain,
index_21 = index_57,
inference(forward_demodulation,[],[f1407,f858]) ).
fof(f1411,plain,
s(index_21) = index_60,
inference(superposition,[],[f185,f1408]) ).
fof(f1412,plain,
index_63 = s(index_21),
inference(forward_demodulation,[],[f1411,f1059]) ).
fof(f1415,plain,
index_63 = index_24,
inference(forward_demodulation,[],[f1412,f160]) ).
fof(f1416,plain,
index_27 = index_63,
inference(forward_demodulation,[],[f1415,f973]) ).
fof(f1417,plain,
index_9 = index_63,
inference(forward_demodulation,[],[f1416,f1371]) ).
fof(f1422,plain,
s(index_9) = index_66,
inference(superposition,[],[f187,f1417]) ).
fof(f1423,plain,
index_75 = s(index_9),
inference(forward_demodulation,[],[f1422,f1069]) ).
fof(f1426,plain,
index_75 = index_12,
inference(forward_demodulation,[],[f1423,f116]) ).
fof(f1427,plain,
index_15 = index_75,
inference(forward_demodulation,[],[f1426,f744]) ).
fof(f1430,plain,
s(index_15) = index_78,
inference(superposition,[],[f191,f1427]) ).
fof(f1431,plain,
index_81 = s(index_15),
inference(forward_demodulation,[],[f1430,f1102]) ).
fof(f1434,plain,
index_81 = index_18,
inference(forward_demodulation,[],[f1431,f138]) ).
fof(f1435,plain,
index_21 = index_81,
inference(forward_demodulation,[],[f1434,f858]) ).
fof(f1438,plain,
s(index_21) = index_84,
inference(superposition,[],[f193,f1435]) ).
fof(f1439,plain,
index_87 = s(index_21),
inference(forward_demodulation,[],[f1438,f1113]) ).
fof(f1442,plain,
index_87 = index_24,
inference(forward_demodulation,[],[f1439,f160]) ).
fof(f1443,plain,
index_27 = index_87,
inference(forward_demodulation,[],[f1442,f973]) ).
fof(f1444,plain,
index_9 = index_87,
inference(forward_demodulation,[],[f1443,f1371]) ).
fof(f1450,plain,
s(index_9) = index_90,
inference(superposition,[],[f196,f1444]) ).
fof(f1451,plain,
index_93 = s(index_9),
inference(forward_demodulation,[],[f1450,f1123]) ).
fof(f1454,plain,
index_93 = index_12,
inference(forward_demodulation,[],[f1451,f116]) ).
fof(f1455,plain,
index_15 = index_93,
inference(forward_demodulation,[],[f1454,f744]) ).
fof(f1460,plain,
s(index_15) = index_96,
inference(superposition,[],[f198,f1455]) ).
fof(f1461,plain,
index_99 = s(index_15),
inference(forward_demodulation,[],[f1460,f1134]) ).
fof(f1464,plain,
index_99 = index_18,
inference(forward_demodulation,[],[f1461,f138]) ).
fof(f1465,plain,
index_99 = index_21,
inference(forward_demodulation,[],[f1464,f858]) ).
fof(f1470,plain,
s(index_99) = index_24,
inference(superposition,[],[f160,f1465]) ).
fof(f1471,plain,
index_27 = s(index_99),
inference(forward_demodulation,[],[f1470,f973]) ).
fof(f1472,plain,
index_27 = index_102,
inference(forward_demodulation,[],[f1471,f110]) ).
fof(f1473,plain,
index_105 = index_27,
inference(forward_demodulation,[],[f1472,f692]) ).
fof(f1474,plain,
index_9 = index_105,
inference(forward_demodulation,[],[f1473,f1371]) ).
fof(f1513,plain,
index_135 = s(s(index_201)),
inference(forward_demodulation,[],[f355,f765]) ).
fof(f1514,plain,
index_135 = s(index_204),
inference(forward_demodulation,[],[f1513,f147]) ).
fof(f1515,plain,
index_135 = s(index_231),
inference(forward_demodulation,[],[f1514,f889]) ).
fof(f1516,plain,
index_135 = index_234,
inference(forward_demodulation,[],[f1515,f158]) ).
fof(f1517,plain,
index_135 = index_237,
inference(forward_demodulation,[],[f1516,f942]) ).
fof(f1520,plain,
s(index_135) = index_240,
inference(superposition,[],[f161,f1517]) ).
fof(f1521,plain,
index_243 = s(index_135),
inference(forward_demodulation,[],[f1520,f952]) ).
fof(f1522,plain,
index_243 = index_138,
inference(forward_demodulation,[],[f1521,f123]) ).
fof(f1523,plain,
index_201 = index_243,
inference(forward_demodulation,[],[f1522,f765]) ).
fof(f1526,plain,
s(index_201) = index_246,
inference(superposition,[],[f163,f1523]) ).
fof(f1527,plain,
index_249 = s(index_201),
inference(forward_demodulation,[],[f1526,f963]) ).
fof(f1528,plain,
index_249 = index_204,
inference(forward_demodulation,[],[f1527,f147]) ).
fof(f1529,plain,
index_231 = index_249,
inference(forward_demodulation,[],[f1528,f889]) ).
fof(f1535,plain,
s(index_231) = index_252,
inference(superposition,[],[f165,f1529]) ).
fof(f1536,plain,
index_255 = s(index_231),
inference(forward_demodulation,[],[f1535,f984]) ).
fof(f1537,plain,
index_255 = index_234,
inference(forward_demodulation,[],[f1536,f158]) ).
fof(f1538,plain,
index_237 = index_255,
inference(forward_demodulation,[],[f1537,f942]) ).
fof(f1539,plain,
index_135 = index_255,
inference(forward_demodulation,[],[f1538,f1517]) ).
fof(f1544,plain,
s(index_135) = index_258,
inference(superposition,[],[f167,f1539]) ).
fof(f1545,plain,
index_9 = s(index_135),
inference(forward_demodulation,[],[f1544,f994]) ).
fof(f1549,plain,
index_9 = index_138,
inference(forward_demodulation,[],[f1545,f123]) ).
fof(f1550,plain,
index_9 = index_201,
inference(forward_demodulation,[],[f1549,f765]) ).
fof(f1717,plain,
index_264 = s(s(index_228)),
inference(forward_demodulation,[],[f424,f932]) ).
fof(f1718,plain,
index_264 = s(s(index_111)),
inference(forward_demodulation,[],[f1717,f1340]) ).
fof(f1719,plain,
index_264 = s(index_114),
inference(forward_demodulation,[],[f1718,f114]) ).
fof(f1720,plain,
index_264 = s(index_117),
inference(forward_demodulation,[],[f1719,f713]) ).
fof(f1721,plain,
index_264 = index_120,
inference(forward_demodulation,[],[f1720,f117]) ).
fof(f1722,plain,
index_123 = index_264,
inference(forward_demodulation,[],[f1721,f723]) ).
fof(f1723,plain,
index_105 = index_264,
inference(forward_demodulation,[],[f1722,f1205]) ).
fof(f1724,plain,
index_9 = index_264,
inference(forward_demodulation,[],[f1723,f1474]) ).
fof(f1727,plain,
elem_265 = select(earray_260,index_9),
inference(superposition,[],[f108,f1724]) ).
fof(f1766,plain,
index_3 = s(s(index_69)),
inference(forward_demodulation,[],[f442,f1080]) ).
fof(f1767,plain,
index_3 = s(index_72),
inference(forward_demodulation,[],[f1766,f189]) ).
fof(f1768,plain,
index_3 = s(index_135),
inference(forward_demodulation,[],[f1767,f1090]) ).
fof(f1769,plain,
index_3 = index_138,
inference(forward_demodulation,[],[f1768,f123]) ).
fof(f1770,plain,
index_201 = index_3,
inference(forward_demodulation,[],[f1769,f765]) ).
fof(f1771,plain,
index_9 = index_3,
inference(forward_demodulation,[],[f1770,f1550]) ).
fof(f1839,plain,
earray_260 = store(earray_220,index_105,e42),
inference(forward_demodulation,[],[f1190,f1333]) ).
fof(f1840,plain,
earray_260 = store(earray_220,index_9,e42),
inference(forward_demodulation,[],[f1839,f1474]) ).
fof(f1846,plain,
index_261 = rselect_head(q42),
inference(forward_demodulation,[],[f582,f930]) ).
fof(f1854,plain,
index_3 = rselect_head(queue_5),
inference(forward_demodulation,[],[f637,f687]) ).
fof(f1855,plain,
index_9 = rselect_head(queue_5),
inference(forward_demodulation,[],[f1854,f1771]) ).
fof(f1861,plain,
rselect_head(q23) = rselect_head(q24),
inference(forward_demodulation,[],[f690,f467]) ).
fof(f1864,plain,
rselect_head(q24) = rselect_head(q25),
inference(forward_demodulation,[],[f700,f472]) ).
fof(f1865,plain,
rselect_head(q25) = rselect_head(q26),
inference(forward_demodulation,[],[f711,f481]) ).
fof(f1866,plain,
rselect_head(q26) = rselect_head(q27),
inference(forward_demodulation,[],[f721,f486]) ).
fof(f1868,plain,
rselect_head(q27) = rselect_head(q28),
inference(forward_demodulation,[],[f732,f491]) ).
fof(f1869,plain,
rselect_head(q9) = rselect_head(q10),
inference(forward_demodulation,[],[f742,f477]) ).
fof(f1870,plain,
rselect_head(q28) = rselect_head(q29),
inference(forward_demodulation,[],[f752,f497]) ).
fof(f1872,plain,
rselect_head(q2) = rselect_head(q3),
inference(forward_demodulation,[],[f763,f502]) ).
fof(f1873,plain,
rselect_head(q29) = rselect_head(q30),
inference(forward_demodulation,[],[f773,f507]) ).
fof(f1874,plain,
rselect_head(q30) = rselect_head(q31),
inference(forward_demodulation,[],[f784,f512]) ).
fof(f1876,plain,
rselect_head(q31) = rselect_head(q32),
inference(forward_demodulation,[],[f794,f517]) ).
fof(f1877,plain,
rselect_head(q32) = rselect_head(q33),
inference(forward_demodulation,[],[f804,f522]) ).
fof(f1878,plain,
rselect_head(q33) = rselect_head(q34),
inference(forward_demodulation,[],[f815,f527]) ).
fof(f1880,plain,
rselect_head(q34) = rselect_head(q35),
inference(forward_demodulation,[],[f825,f536]) ).
fof(f1881,plain,
rselect_head(q35) = rselect_head(q36),
inference(forward_demodulation,[],[f835,f541]) ).
fof(f1882,plain,
rselect_head(q36) = rselect_head(q37),
inference(forward_demodulation,[],[f845,f546]) ).
fof(f1885,plain,
rselect_head(q10) = rselect_head(q11),
inference(forward_demodulation,[],[f856,f532]) ).
fof(f1886,plain,
rselect_head(q37) = rselect_head(q38),
inference(forward_demodulation,[],[f867,f552]) ).
fof(f1887,plain,
rselect_head(q38) = rselect_head(q39),
inference(forward_demodulation,[],[f877,f557]) ).
fof(f1890,plain,
rselect_head(q3) = rselect_head(q4),
inference(forward_demodulation,[],[f887,f562]) ).
fof(f1891,plain,
rselect_head(q39) = rselect_head(q40),
inference(forward_demodulation,[],[f898,f567]) ).
fof(f1894,plain,
rselect_head(q40) = rselect_head(q41),
inference(forward_demodulation,[],[f909,f572]) ).
fof(f1897,plain,
index_261 = rselect_head(queue_221),
inference(forward_demodulation,[],[f919,f1846]) ).
fof(f1898,plain,
index_261 = rselect_head(q41),
inference(forward_demodulation,[],[f1897,f577]) ).
fof(f1899,plain,
rselect_head(q4) = rselect_head(q5),
inference(forward_demodulation,[],[f940,f591]) ).
fof(f1902,plain,
rselect_head(q5) = rselect_head(q6),
inference(forward_demodulation,[],[f950,f596]) ).
fof(f1903,plain,
rselect_head(q6) = rselect_head(q7),
inference(forward_demodulation,[],[f961,f601]) ).
fof(f1904,plain,
rselect_head(q11) = rselect_head(q12),
inference(forward_demodulation,[],[f971,f587]) ).
fof(f1907,plain,
rselect_head(q7) = rselect_head(q8),
inference(forward_demodulation,[],[f982,f607]) ).
fof(f1908,plain,
rselect_head(q9) = rselect_head(q8),
inference(forward_demodulation,[],[f992,f612]) ).
fof(f1909,plain,
rselect_head(q12) = rselect_head(q13),
inference(forward_demodulation,[],[f1004,f617]) ).
fof(f1912,plain,
rselect_head(q13) = rselect_head(q14),
inference(forward_demodulation,[],[f1015,f622]) ).
fof(f1913,plain,
rselect_head(q14) = rselect_head(q15),
inference(forward_demodulation,[],[f1025,f627]) ).
fof(f1914,plain,
rselect_head(q15) = rselect_head(q16),
inference(forward_demodulation,[],[f1036,f632]) ).
fof(f1917,plain,
rselect_head(q16) = rselect_head(q17),
inference(forward_demodulation,[],[f1046,f641]) ).
fof(f1918,plain,
rselect_head(q17) = rselect_head(q18),
inference(forward_demodulation,[],[f1057,f646]) ).
fof(f1919,plain,
rselect_head(q18) = rselect_head(q19),
inference(forward_demodulation,[],[f1067,f651]) ).
fof(f1922,plain,
index_9 = rselect_head(q1),
inference(forward_demodulation,[],[f1078,f1855]) ).
fof(f1923,plain,
rselect_head(q2) = rselect_head(q1),
inference(forward_demodulation,[],[f1088,f657]) ).
fof(f1924,plain,
index_9 = rselect_head(q2),
inference(forward_demodulation,[],[f1923,f1922]) ).
fof(f1927,plain,
rselect_head(q19) = rselect_head(q20),
inference(forward_demodulation,[],[f1100,f662]) ).
fof(f1928,plain,
rselect_head(q20) = rselect_head(q21),
inference(forward_demodulation,[],[f1111,f667]) ).
fof(f1931,plain,
rselect_head(q21) = rselect_head(q22),
inference(forward_demodulation,[],[f1121,f672]) ).
fof(f1932,plain,
rselect_head(q23) = rselect_head(q22),
inference(forward_demodulation,[],[f1132,f677]) ).
fof(f1941,plain,
rselect_head(q24) = rselect_head(q26),
inference(forward_demodulation,[],[f1865,f1864]) ).
fof(f1942,plain,
rselect_head(q26) = rselect_head(q28),
inference(forward_demodulation,[],[f1868,f1866]) ).
fof(f1945,plain,
index_9 = rselect_head(q3),
inference(forward_demodulation,[],[f1872,f1924]) ).
fof(f1948,plain,
rselect_head(q28) = rselect_head(q30),
inference(forward_demodulation,[],[f1873,f1870]) ).
fof(f1951,plain,
rselect_head(q30) = rselect_head(q32),
inference(forward_demodulation,[],[f1876,f1874]) ).
fof(f1952,plain,
rselect_head(q32) = rselect_head(q34),
inference(forward_demodulation,[],[f1878,f1877]) ).
fof(f1955,plain,
rselect_head(q34) = rselect_head(q36),
inference(forward_demodulation,[],[f1881,f1880]) ).
fof(f1962,plain,
rselect_head(q36) = rselect_head(q38),
inference(forward_demodulation,[],[f1886,f1882]) ).
fof(f1969,plain,
index_9 = rselect_head(q4),
inference(forward_demodulation,[],[f1890,f1945]) ).
fof(f1972,plain,
rselect_head(q38) = rselect_head(q40),
inference(forward_demodulation,[],[f1891,f1887]) ).
fof(f1973,plain,
index_261 = rselect_head(q40),
inference(forward_demodulation,[],[f1894,f1898]) ).
fof(f1976,plain,
index_9 = rselect_head(q5),
inference(forward_demodulation,[],[f1899,f1969]) ).
fof(f1979,plain,
index_9 = rselect_head(q6),
inference(forward_demodulation,[],[f1902,f1976]) ).
fof(f1980,plain,
e42 = select(earray_260,index_9),
inference(superposition,[],[f1,f1840]) ).
fof(f1982,plain,
index_9 = rselect_head(q7),
inference(forward_demodulation,[],[f1903,f1979]) ).
fof(f1987,plain,
rselect_head(q10) = rselect_head(q12),
inference(forward_demodulation,[],[f1904,f1885]) ).
fof(f1988,plain,
index_9 = rselect_head(q8),
inference(forward_demodulation,[],[f1907,f1982]) ).
fof(f1991,plain,
index_9 = rselect_head(q9),
inference(forward_demodulation,[],[f1908,f1988]) ).
fof(f1992,plain,
index_9 = rselect_head(q10),
inference(forward_demodulation,[],[f1991,f1869]) ).
fof(f1995,plain,
rselect_head(q12) = rselect_head(q14),
inference(forward_demodulation,[],[f1912,f1909]) ).
fof(f1998,plain,
rselect_head(q14) = rselect_head(q16),
inference(forward_demodulation,[],[f1914,f1913]) ).
fof(f2003,plain,
rselect_head(q16) = rselect_head(q18),
inference(forward_demodulation,[],[f1918,f1917]) ).
fof(f2006,plain,
rselect_head(q18) = rselect_head(q20),
inference(forward_demodulation,[],[f1927,f1919]) ).
fof(f2009,plain,
rselect_head(q20) = rselect_head(q22),
inference(forward_demodulation,[],[f1931,f1928]) ).
fof(f2014,plain,
rselect_head(q24) = rselect_head(q22),
inference(forward_demodulation,[],[f1932,f1861]) ).
fof(f2023,plain,
rselect_head(q24) = rselect_head(q28),
inference(forward_demodulation,[],[f1942,f1941]) ).
fof(f2028,plain,
rselect_head(q28) = rselect_head(q32),
inference(forward_demodulation,[],[f1951,f1948]) ).
fof(f2039,plain,
rselect_head(q32) = rselect_head(q36),
inference(forward_demodulation,[],[f1955,f1952]) ).
fof(f2048,plain,
index_261 = rselect_head(q38),
inference(forward_demodulation,[],[f1972,f1973]) ).
fof(f2049,plain,
index_261 = rselect_head(q36),
inference(forward_demodulation,[],[f2048,f1962]) ).
fof(f2058,plain,
index_9 = rselect_head(q12),
inference(forward_demodulation,[],[f1987,f1992]) ).
fof(f2067,plain,
index_9 = rselect_head(q14),
inference(forward_demodulation,[],[f1995,f2058]) ).
fof(f2072,plain,
index_9 = rselect_head(q16),
inference(forward_demodulation,[],[f1998,f2067]) ).
fof(f2077,plain,
index_9 = rselect_head(q18),
inference(forward_demodulation,[],[f2003,f2072]) ).
fof(f2078,plain,
index_9 = rselect_head(q20),
inference(forward_demodulation,[],[f2006,f2077]) ).
fof(f2083,plain,
index_9 = rselect_head(q22),
inference(forward_demodulation,[],[f2009,f2078]) ).
fof(f2084,plain,
index_9 = rselect_head(q24),
inference(forward_demodulation,[],[f2014,f2083]) ).
fof(f2089,plain,
index_9 = rselect_head(q28),
inference(forward_demodulation,[],[f2023,f2084]) ).
fof(f2090,plain,
index_9 = rselect_head(q32),
inference(forward_demodulation,[],[f2028,f2089]) ).
fof(f2095,plain,
index_261 = rselect_head(q32),
inference(forward_demodulation,[],[f2039,f2049]) ).
fof(f2096,plain,
index_9 = index_261,
inference(forward_demodulation,[],[f2095,f2090]) ).
fof(f2097,plain,
elem_262 = select(earray_260,index_9),
inference(superposition,[],[f107,f2096]) ).
fof(f2098,plain,
e42 = elem_262,
inference(forward_demodulation,[],[f2097,f1980]) ).
fof(f2233,plain,
e42 = elem_265,
inference(forward_demodulation,[],[f1727,f1980]) ).
fof(f2234,plain,
e42 != elem_262,
inference(superposition,[],[f331,f2233]) ).
fof(f2235,plain,
$false,
inference(forward_subsumption_resolution,[],[f2234,f2098]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n006.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:53:25 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.92/1.13 % (3914279)Input is clausal, will run a generic CNF schedule.
% 2.92/1.13 % (3914287)lrs+10_1_sil=8000:sp=occurrence:random_seed=1790858141:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.92/1.13 % (3914287)Instruction limit reached!
% 2.92/1.13 % (3914287)------------------------------
% 2.92/1.13 % (3914287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.13 % (3914287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.13 % (3914287)CaDiCaL version: 2.1.3
% 2.92/1.13 % (3914287)Termination reason: Instruction limit
% 2.92/1.13 % (3914287)Termination phase: Saturation
% 2.92/1.13 % (3914287)Time elapsed: 0.033 s
% 2.92/1.13 % (3914287)Peak memory usage: 89 MB
% 2.92/1.13 % (3914287)Instructions burned: 110 (million)
% 2.92/1.13 % (3914285)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2163679175:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.92/1.13 % (3914284)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2033204265:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.92/1.13 % (3914289)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2178434584:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.92/1.13 % (3914290)dis-21_1_sil=8000:lcm=predicate:random_seed=830474642:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.92/1.13 % (3914286)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2832351014:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.92/1.13 % (3914288)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=814142560:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.92/1.13 % (3914290)Refutation not found, incomplete strategy
% 2.92/1.13 % (3914290)------------------------------
% 2.92/1.13 % (3914290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.13 % (3914290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.13 % (3914290)CaDiCaL version: 2.1.3
% 2.92/1.13 % (3914290)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.13 % (3914290)Time elapsed: 0.006 s
% 2.92/1.13 % (3914290)Peak memory usage: 88 MB
% 2.92/1.13 % (3914290)Instructions burned: 12 (million)
% 2.92/1.13 % (3914288)Instruction limit reached!
% 2.92/1.13 % (3914288)------------------------------
% 2.92/1.13 % (3914288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.13 % (3914288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.13 % (3914288)CaDiCaL version: 2.1.3
% 2.92/1.13 % (3914288)Termination reason: Instruction limit
% 2.92/1.13 % (3914288)Termination phase: Saturation
% 2.92/1.13 % (3914288)Time elapsed: 0.064 s
% 2.92/1.13 % (3914288)Peak memory usage: 89 MB
% 2.92/1.13 % (3914288)Instructions burned: 115 (million)
% 2.92/1.13 % (3914292)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3216746301:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.92/1.13 % (3914289)Instruction limit reached!
% 2.92/1.13 % (3914289)------------------------------
% 2.92/1.13 % (3914289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.13 % (3914289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.13 % (3914289)CaDiCaL version: 2.1.3
% 2.92/1.13 % (3914289)Termination reason: Instruction limit
% 2.92/1.13 % (3914289)Termination phase: Saturation
% 2.92/1.13 % (3914289)Time elapsed: 0.130 s
% 2.92/1.13 % (3914289)Peak memory usage: 89 MB
% 2.92/1.13 % (3914289)Instructions burned: 181 (million)
% 2.92/1.13 % (3914292)First to succeed.
% 2.92/1.13 % (3914292)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3914279"
% 2.92/1.13 % (3914299)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2749296571:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.92/1.13 % (3914290)------------------------------
% 2.92/1.13 % (3914290)------------------------------
% 2.92/1.13 % (3914301)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2238205385:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 2.92/1.13 % (3914292)Refutation found. Thanks to Tanya!
% 2.92/1.13 % SZS status Unsatisfiable for theBenchmark
% 2.92/1.13 % SZS output start Proof for theBenchmark
% See solution above
% 4.08/1.33 % (3914292)------------------------------
% 4.08/1.33 % (3914292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.08/1.33 % (3914292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.08/1.33 % (3914292)CaDiCaL version: 2.1.3
% 4.08/1.33 % (3914292)Termination reason: Refutation
% 4.08/1.33 % (3914292)Time elapsed: 0.042 s
% 4.08/1.33 % (3914292)Peak memory usage: 90 MB
% 4.08/1.33 % (3914292)Instructions burned: 129 (million)
% 4.08/1.33 % (3914292)------------------------------
% 4.08/1.33 % (3914292)------------------------------
% 4.08/1.33 % (3914279)Success in time 0.492 s
% 4.08/1.33 % Vampire exiting
%------------------------------------------------------------------------------