%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 02:49:09 PM UTC 2026
% Result : Unsatisfiable 0.15s 1.13s
% Output : CNFRefutation 3.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 264
% Syntax : Number of formulae : 1139 ( 885 unt; 0 def)
% Number of atoms : 1558 (1557 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 428 ( 9 ~; 419 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 313 ( 313 usr; 309 con; 0-3 aty)
% Number of variables : 217 ( 217 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : p(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : s(p(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] : s(s(s(X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
earray_262 = store(earray_260,index_261,e48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,hypothesis,
earray_296 = select(q49,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
elem_298 = select(earray_296,index_297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
elem_301 = select(earray_296,index_300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
index_105 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
index_111 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
index_117 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,hypothesis,
index_123 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,hypothesis,
index_126 = s(index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
index_129 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,hypothesis,
index_135 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,hypothesis,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,hypothesis,
index_141 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
index_147 = select(q30,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,hypothesis,
index_153 = select(q31,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,hypothesis,
index_159 = select(q32,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
index_162 = s(index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
index_165 = select(q33,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
index_168 = s(index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
index_171 = select(q34,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
index_177 = select(q35,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
index_183 = select(q36,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
index_189 = select(q37,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
index_192 = s(index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
index_195 = select(q38,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
index_198 = s(index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
index_201 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,hypothesis,
index_207 = select(q39,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
index_210 = s(index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_213 = select(q40,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_219 = select(q41,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_225 = select(q42,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_231 = select(q43,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_234 = s(index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_237 = select(q44,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_243 = select(q45,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_249 = select(q46,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_255 = select(q47,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_261 = select(q48,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_267 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_27 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_273 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_279 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_282 = s(index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_285 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_288 = s(index_285),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_291 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_294 = s(index_291),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_297 = select(q49,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_299 = select(q49,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
s(index_300) = index_299,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_33 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_39 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_45 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_51 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_57 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_63 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
index_69 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
index_75 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
index_81 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
index_87 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
index_93 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
index_99 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_101 = store(q23,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_107 = store(q24,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_113 = store(q25,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_119 = store(q26,seq,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_121 = store(queue_119,tail,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_125 = store(q27,seq,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_127 = store(queue_125,tail,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_131 = store(q28,seq,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_133 = store(queue_131,tail,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_137 = store(q2,seq,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_139 = store(queue_137,tail,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_143 = store(q29,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_149 = store(q30,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_155 = store(q31,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_161 = store(q32,seq,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_163 = store(queue_161,tail,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_167 = store(q33,seq,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_169 = store(queue_167,tail,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_173 = store(q34,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_179 = store(q35,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_185 = store(q36,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_191 = store(q37,seq,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_193 = store(queue_191,tail,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_197 = store(q38,seq,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_199 = store(queue_197,tail,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_203 = store(q3,seq,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_205 = store(queue_203,tail,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_209 = store(q39,seq,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_211 = store(queue_209,tail,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_215 = store(q40,seq,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_221 = store(q41,seq,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_227 = store(q42,seq,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_233 = store(q43,seq,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_235 = store(queue_233,tail,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_239 = store(q44,seq,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_241 = store(queue_239,tail,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_245 = store(q45,seq,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_247 = store(queue_245,tail,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_251 = store(q46,seq,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_253 = store(queue_251,tail,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_257 = store(q47,seq,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_259 = store(queue_257,tail,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_263 = store(q48,seq,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_269 = store(q4,seq,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_275 = store(q5,seq,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_281 = store(q6,seq,earray_280),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_283 = store(queue_281,tail,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
queue_287 = store(q7,seq,earray_286),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
queue_289 = store(queue_287,tail,index_288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
queue_29 = store(q12,seq,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
queue_293 = store(q8,seq,earray_292),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
queue_295 = store(queue_293,tail,index_294),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
queue_31 = store(queue_29,tail,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
queue_35 = store(q13,seq,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
queue_37 = store(queue_35,tail,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
queue_41 = store(q14,seq,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
queue_43 = store(queue_41,tail,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
queue_47 = store(q15,seq,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
queue_49 = store(queue_47,tail,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
queue_53 = store(q16,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
queue_59 = store(q17,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
queue_65 = store(q18,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
queue_71 = store(q1,seq,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
queue_73 = store(queue_71,tail,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
queue_77 = store(q19,seq,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
queue_79 = store(queue_77,tail,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
queue_83 = store(q20,seq,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
queue_85 = store(queue_83,tail,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
queue_89 = store(q21,seq,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
queue_91 = store(queue_89,tail,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
queue_95 = store(q22,seq,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
queue_97 = store(queue_95,tail,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f327,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f328,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f329,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f330,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f331,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f332,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f333,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f334,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f335,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f336,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f337,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f338,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f339,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f340,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f342,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f344,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f345,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f346,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f347,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f348,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f349,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f350,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f351,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f352,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f353,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f354,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f355,hypothesis,
q47 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f356,hypothesis,
q48 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f357,hypothesis,
q49 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f358,hypothesis,
q5 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f359,hypothesis,
q6 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f360,hypothesis,
q7 = queue_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f361,hypothesis,
q8 = queue_289,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f362,hypothesis,
q9 = queue_295,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f363,negated_conjecture,
elem_298 != elem_301,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f364,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f365,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f366,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f365]) ).
fof(f367,plain,
head != tail,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f368,plain,
head != seq,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f369,plain,
tail != seq,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f370,plain,
! [X0] : p(s(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f371,plain,
! [X0] : s(p(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f374,plain,
! [X0] : s(s(s(X0))) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f436,plain,
earray_262 = store(earray_260,index_261,e48),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f448,plain,
earray_296 = select(q49,seq),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f474,plain,
elem_298 = select(earray_296,index_297),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f475,plain,
elem_301 = select(earray_296,index_300),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f476,plain,
index_0 = select(q,tail),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f477,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f478,plain,
index_105 = select(q24,tail),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f479,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f480,plain,
index_111 = select(q25,tail),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f481,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f482,plain,
index_117 = select(q26,tail),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f483,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f484,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f485,plain,
index_123 = select(q27,tail),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f486,plain,
index_126 = s(index_123),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f487,plain,
index_129 = select(q28,tail),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f488,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f489,plain,
index_135 = select(q2,tail),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f490,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f491,plain,
index_141 = select(q29,tail),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f492,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f493,plain,
index_147 = select(q30,tail),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f494,plain,
index_15 = select(q10,tail),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f495,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f496,plain,
index_153 = select(q31,tail),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f497,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f498,plain,
index_159 = select(q32,tail),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f499,plain,
index_162 = s(index_159),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f500,plain,
index_165 = select(q33,tail),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f501,plain,
index_168 = s(index_165),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f502,plain,
index_171 = select(q34,tail),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f503,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f504,plain,
index_177 = select(q35,tail),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f505,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f506,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f507,plain,
index_183 = select(q36,tail),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f508,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f509,plain,
index_189 = select(q37,tail),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f510,plain,
index_192 = s(index_189),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f511,plain,
index_195 = select(q38,tail),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f512,plain,
index_198 = s(index_195),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f513,plain,
index_201 = select(q3,tail),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f514,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f515,plain,
index_207 = select(q39,tail),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f516,plain,
index_21 = select(q11,tail),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f517,plain,
index_210 = s(index_207),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f518,plain,
index_213 = select(q40,tail),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f519,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f520,plain,
index_219 = select(q41,tail),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f521,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f522,plain,
index_225 = select(q42,tail),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f523,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f524,plain,
index_231 = select(q43,tail),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f525,plain,
index_234 = s(index_231),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f526,plain,
index_237 = select(q44,tail),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f527,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f528,plain,
index_240 = s(index_237),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f529,plain,
index_243 = select(q45,tail),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f530,plain,
index_246 = s(index_243),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f531,plain,
index_249 = select(q46,tail),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f532,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f533,plain,
index_255 = select(q47,tail),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f534,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f535,plain,
index_261 = select(q48,tail),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f536,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f537,plain,
index_267 = select(q4,tail),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f538,plain,
index_27 = select(q12,tail),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f539,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f540,plain,
index_273 = select(q5,tail),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f541,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f542,plain,
index_279 = select(q6,tail),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f543,plain,
index_282 = s(index_279),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f544,plain,
index_285 = select(q7,tail),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f545,plain,
index_288 = s(index_285),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f546,plain,
index_291 = select(q8,tail),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f547,plain,
index_294 = s(index_291),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f548,plain,
index_297 = select(q49,head),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f549,plain,
index_299 = select(q49,tail),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f550,plain,
index_3 = select(q0,tail),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f551,plain,
index_30 = s(index_27),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f552,plain,
s(index_300) = index_299,
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f553,plain,
index_33 = select(q13,tail),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f554,plain,
index_36 = s(index_33),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f555,plain,
index_39 = select(q14,tail),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f556,plain,
index_42 = s(index_39),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f557,plain,
index_45 = select(q15,tail),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f558,plain,
index_48 = s(index_45),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f559,plain,
index_51 = select(q16,tail),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f560,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f561,plain,
index_57 = select(q17,tail),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f562,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f563,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f564,plain,
index_63 = select(q18,tail),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f565,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f566,plain,
index_69 = select(q1,tail),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f567,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f568,plain,
index_75 = select(q19,tail),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f569,plain,
index_78 = s(index_75),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f570,plain,
index_81 = select(q20,tail),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f571,plain,
index_84 = s(index_81),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f572,plain,
index_87 = select(q21,tail),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f573,plain,
index_9 = select(q9,tail),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f574,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f575,plain,
index_93 = select(q22,tail),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f576,plain,
index_96 = s(index_93),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f577,plain,
index_99 = select(q23,tail),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f578,plain,
queue_1 = store(q,head,index_0),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f579,plain,
queue_101 = store(q23,seq,earray_100),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f580,plain,
queue_103 = store(queue_101,tail,index_102),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f581,plain,
queue_107 = store(q24,seq,earray_106),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f582,plain,
queue_109 = store(queue_107,tail,index_108),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f583,plain,
queue_11 = store(q9,seq,earray_10),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f584,plain,
queue_113 = store(q25,seq,earray_112),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f585,plain,
queue_115 = store(queue_113,tail,index_114),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f586,plain,
queue_119 = store(q26,seq,earray_118),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f587,plain,
queue_121 = store(queue_119,tail,index_120),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f588,plain,
queue_125 = store(q27,seq,earray_124),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f589,plain,
queue_127 = store(queue_125,tail,index_126),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f590,plain,
queue_13 = store(queue_11,tail,index_12),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f591,plain,
queue_131 = store(q28,seq,earray_130),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f592,plain,
queue_133 = store(queue_131,tail,index_132),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f593,plain,
queue_137 = store(q2,seq,earray_136),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f594,plain,
queue_139 = store(queue_137,tail,index_138),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f595,plain,
queue_143 = store(q29,seq,earray_142),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f596,plain,
queue_145 = store(queue_143,tail,index_144),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f597,plain,
queue_149 = store(q30,seq,earray_148),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f598,plain,
queue_151 = store(queue_149,tail,index_150),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f599,plain,
queue_155 = store(q31,seq,earray_154),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f600,plain,
queue_157 = store(queue_155,tail,index_156),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f601,plain,
queue_161 = store(q32,seq,earray_160),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f602,plain,
queue_163 = store(queue_161,tail,index_162),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f603,plain,
queue_167 = store(q33,seq,earray_166),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f604,plain,
queue_169 = store(queue_167,tail,index_168),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f605,plain,
queue_17 = store(q10,seq,earray_16),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f606,plain,
queue_173 = store(q34,seq,earray_172),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f607,plain,
queue_175 = store(queue_173,tail,index_174),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f608,plain,
queue_179 = store(q35,seq,earray_178),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f609,plain,
queue_181 = store(queue_179,tail,index_180),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f610,plain,
queue_185 = store(q36,seq,earray_184),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f611,plain,
queue_187 = store(queue_185,tail,index_186),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f612,plain,
queue_19 = store(queue_17,tail,index_18),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f613,plain,
queue_191 = store(q37,seq,earray_190),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f614,plain,
queue_193 = store(queue_191,tail,index_192),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f615,plain,
queue_197 = store(q38,seq,earray_196),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f616,plain,
queue_199 = store(queue_197,tail,index_198),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f617,plain,
queue_203 = store(q3,seq,earray_202),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f618,plain,
queue_205 = store(queue_203,tail,index_204),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f619,plain,
queue_209 = store(q39,seq,earray_208),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f620,plain,
queue_211 = store(queue_209,tail,index_210),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f621,plain,
queue_215 = store(q40,seq,earray_214),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f622,plain,
queue_217 = store(queue_215,tail,index_216),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f623,plain,
queue_221 = store(q41,seq,earray_220),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f624,plain,
queue_223 = store(queue_221,tail,index_222),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f625,plain,
queue_227 = store(q42,seq,earray_226),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f626,plain,
queue_229 = store(queue_227,tail,index_228),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f627,plain,
queue_23 = store(q11,seq,earray_22),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f628,plain,
queue_233 = store(q43,seq,earray_232),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f629,plain,
queue_235 = store(queue_233,tail,index_234),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f630,plain,
queue_239 = store(q44,seq,earray_238),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f631,plain,
queue_241 = store(queue_239,tail,index_240),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f632,plain,
queue_245 = store(q45,seq,earray_244),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f633,plain,
queue_247 = store(queue_245,tail,index_246),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f634,plain,
queue_25 = store(queue_23,tail,index_24),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f635,plain,
queue_251 = store(q46,seq,earray_250),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f636,plain,
queue_253 = store(queue_251,tail,index_252),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f637,plain,
queue_257 = store(q47,seq,earray_256),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f638,plain,
queue_259 = store(queue_257,tail,index_258),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f639,plain,
queue_263 = store(q48,seq,earray_262),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f640,plain,
queue_265 = store(queue_263,tail,index_264),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f641,plain,
queue_269 = store(q4,seq,earray_268),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f642,plain,
queue_271 = store(queue_269,tail,index_270),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f643,plain,
queue_275 = store(q5,seq,earray_274),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f644,plain,
queue_277 = store(queue_275,tail,index_276),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f645,plain,
queue_281 = store(q6,seq,earray_280),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f646,plain,
queue_283 = store(queue_281,tail,index_282),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f647,plain,
queue_287 = store(q7,seq,earray_286),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f648,plain,
queue_289 = store(queue_287,tail,index_288),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f649,plain,
queue_29 = store(q12,seq,earray_28),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f650,plain,
queue_293 = store(q8,seq,earray_292),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f651,plain,
queue_295 = store(queue_293,tail,index_294),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f652,plain,
queue_31 = store(queue_29,tail,index_30),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f653,plain,
queue_35 = store(q13,seq,earray_34),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f654,plain,
queue_37 = store(queue_35,tail,index_36),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f655,plain,
queue_41 = store(q14,seq,earray_40),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f656,plain,
queue_43 = store(queue_41,tail,index_42),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f657,plain,
queue_47 = store(q15,seq,earray_46),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f658,plain,
queue_49 = store(queue_47,tail,index_48),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f659,plain,
queue_5 = store(q0,seq,earray_4),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f660,plain,
queue_53 = store(q16,seq,earray_52),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f661,plain,
queue_55 = store(queue_53,tail,index_54),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f662,plain,
queue_59 = store(q17,seq,earray_58),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f663,plain,
queue_61 = store(queue_59,tail,index_60),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f664,plain,
queue_65 = store(q18,seq,earray_64),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f665,plain,
queue_67 = store(queue_65,tail,index_66),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f666,plain,
queue_7 = store(queue_5,tail,index_6),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f667,plain,
queue_71 = store(q1,seq,earray_70),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f668,plain,
queue_73 = store(queue_71,tail,index_72),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f669,plain,
queue_77 = store(q19,seq,earray_76),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f670,plain,
queue_79 = store(queue_77,tail,index_78),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f671,plain,
queue_83 = store(q20,seq,earray_82),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f672,plain,
queue_85 = store(queue_83,tail,index_84),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f673,plain,
queue_89 = store(q21,seq,earray_88),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f674,plain,
queue_91 = store(queue_89,tail,index_90),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f675,plain,
queue_95 = store(q22,seq,earray_94),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f676,plain,
queue_97 = store(queue_95,tail,index_96),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f677,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f678,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f679,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f680,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f681,plain,
q12 = queue_25,
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f682,plain,
q13 = queue_31,
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f683,plain,
q14 = queue_37,
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f684,plain,
q15 = queue_43,
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f685,plain,
q16 = queue_49,
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f686,plain,
q17 = queue_55,
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f687,plain,
q18 = queue_61,
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f688,plain,
q19 = queue_67,
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f689,plain,
q2 = queue_73,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f690,plain,
q20 = queue_79,
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f691,plain,
q21 = queue_85,
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f692,plain,
q22 = queue_91,
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f693,plain,
q23 = queue_97,
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f694,plain,
q24 = queue_103,
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f695,plain,
q25 = queue_109,
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f696,plain,
q26 = queue_115,
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f697,plain,
q27 = queue_121,
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f698,plain,
q28 = queue_127,
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f699,plain,
q29 = queue_133,
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f700,plain,
q3 = queue_139,
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f701,plain,
q30 = queue_145,
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f702,plain,
q31 = queue_151,
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f703,plain,
q32 = queue_157,
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f704,plain,
q33 = queue_163,
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f705,plain,
q34 = queue_169,
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f706,plain,
q35 = queue_175,
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f707,plain,
q36 = queue_181,
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f708,plain,
q37 = queue_187,
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f709,plain,
q38 = queue_193,
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f710,plain,
q39 = queue_199,
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f711,plain,
q4 = queue_205,
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f712,plain,
q40 = queue_211,
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f713,plain,
q41 = queue_217,
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f714,plain,
q42 = queue_223,
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f715,plain,
q43 = queue_229,
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f716,plain,
q44 = queue_235,
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f717,plain,
q45 = queue_241,
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f718,plain,
q46 = queue_247,
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f719,plain,
q47 = queue_253,
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f720,plain,
q48 = queue_259,
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f721,plain,
q49 = queue_265,
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f722,plain,
q5 = queue_271,
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f723,plain,
q6 = queue_277,
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f724,plain,
q7 = queue_283,
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f725,plain,
q8 = queue_289,
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f726,plain,
q9 = queue_295,
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f727,plain,
elem_298 != elem_301,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f736,plain,
! [X0] : s(s(X0)) = p(X0),
inference(paramodulation,[status(thm)],[f371,f374]) ).
fof(f748,plain,
p(index_102) = index_99,
inference(paramodulation,[status(thm)],[f477,f370]) ).
fof(f752,plain,
p(index_108) = index_105,
inference(paramodulation,[status(thm)],[f479,f370]) ).
fof(f756,plain,
p(index_114) = index_111,
inference(paramodulation,[status(thm)],[f481,f370]) ).
fof(f760,plain,
p(index_12) = index_9,
inference(paramodulation,[status(thm)],[f483,f370]) ).
fof(f788,plain,
p(index_150) = index_147,
inference(paramodulation,[status(thm)],[f495,f370]) ).
fof(f830,plain,
p(index_204) = index_201,
inference(paramodulation,[status(thm)],[f514,f370]) ).
fof(f838,plain,
p(index_216) = index_213,
inference(paramodulation,[status(thm)],[f519,f370]) ).
fof(f850,plain,
p(index_234) = index_231,
inference(paramodulation,[status(thm)],[f525,f370]) ).
fof(f886,plain,
p(index_276) = index_273,
inference(paramodulation,[status(thm)],[f541,f370]) ).
fof(f890,plain,
p(index_282) = index_279,
inference(paramodulation,[status(thm)],[f543,f370]) ).
fof(f904,plain,
p(index_30) = index_27,
inference(paramodulation,[status(thm)],[f551,f370]) ).
fof(f908,plain,
p(index_299) = index_300,
inference(paramodulation,[status(thm)],[f552,f370]) ).
fof(f928,plain,
p(index_6) = index_3,
inference(paramodulation,[status(thm)],[f562,f370]) ).
fof(f942,plain,
p(index_72) = index_69,
inference(paramodulation,[status(thm)],[f567,f370]) ).
fof(f948,plain,
p(index_78) = index_75,
inference(paramodulation,[status(thm)],[f569,f370]) ).
fof(f960,plain,
p(index_96) = index_93,
inference(paramodulation,[status(thm)],[f576,f370]) ).
fof(f1154,plain,
select(earray_262,index_261) = e48,
inference(paramodulation,[status(thm)],[f436,f364]) ).
fof(f1163,plain,
s(index_84) = p(index_81),
inference(paramodulation,[status(thm)],[f571,f736]) ).
fof(f1170,plain,
s(index_48) = p(index_45),
inference(paramodulation,[status(thm)],[f558,f736]) ).
fof(f1172,plain,
s(index_36) = p(index_33),
inference(paramodulation,[status(thm)],[f554,f736]) ).
fof(f1176,plain,
s(index_288) = p(index_285),
inference(paramodulation,[status(thm)],[f545,f736]) ).
fof(f1181,plain,
s(index_258) = p(index_255),
inference(paramodulation,[status(thm)],[f534,f736]) ).
fof(f1184,plain,
s(index_240) = p(index_237),
inference(paramodulation,[status(thm)],[f528,f736]) ).
fof(f1188,plain,
s(index_222) = p(index_219),
inference(paramodulation,[status(thm)],[f521,f736]) ).
fof(f1194,plain,
s(index_186) = p(index_183),
inference(paramodulation,[status(thm)],[f508,f736]) ).
fof(f1198,plain,
s(index_168) = p(index_165),
inference(paramodulation,[status(thm)],[f501,f736]) ).
fof(f1200,plain,
s(index_156) = p(index_153),
inference(paramodulation,[status(thm)],[f497,f736]) ).
fof(f1203,plain,
s(index_138) = p(index_135),
inference(paramodulation,[status(thm)],[f490,f736]) ).
fof(f1206,plain,
s(index_120) = p(index_117),
inference(paramodulation,[status(thm)],[f484,f736]) ).
fof(f1207,plain,
s(index_12) = p(index_9),
inference(paramodulation,[status(thm)],[f483,f736]) ).
fof(f1408,plain,
q0 = store(q,head,index_0),
inference(forward_demodulation,[status(thm)],[f677,f578]) ).
fof(f1409,plain,
! [X0] :
( select(q0,X0) = select(q,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f1408,f366]) ).
fof(f1410,plain,
select(q0,head) = index_0,
inference(paramodulation,[status(thm)],[f1408,f364]) ).
fof(f1411,plain,
! [X0] :
( select(queue_101,X0) = select(q23,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f579,f366]) ).
fof(f1503,plain,
q24 = store(queue_101,tail,index_102),
inference(forward_demodulation,[status(thm)],[f694,f580]) ).
fof(f1504,plain,
! [X0] :
( select(q24,X0) = select(queue_101,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1503,f366]) ).
fof(f1505,plain,
select(q24,tail) = index_102,
inference(paramodulation,[status(thm)],[f1503,f364]) ).
fof(f1506,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f478,f1505]) ).
fof(f1507,plain,
! [X0] :
( select(queue_107,X0) = select(q24,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f581,f366]) ).
fof(f1509,plain,
q25 = store(queue_107,tail,index_108),
inference(forward_demodulation,[status(thm)],[f695,f582]) ).
fof(f1510,plain,
! [X0] :
( select(q25,X0) = select(queue_107,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1509,f366]) ).
fof(f1511,plain,
select(q25,tail) = index_108,
inference(paramodulation,[status(thm)],[f1509,f364]) ).
fof(f1512,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f480,f1511]) ).
fof(f1514,plain,
p(index_105) = index_99,
inference(backward_demodulation,[status(thm)],[f1506,f748]) ).
fof(f1517,plain,
index_105 = s(index_99),
inference(backward_demodulation,[status(thm)],[f1506,f477]) ).
fof(f1520,plain,
p(index_111) = index_105,
inference(backward_demodulation,[status(thm)],[f1512,f752]) ).
fof(f1523,plain,
index_111 = s(index_105),
inference(backward_demodulation,[status(thm)],[f1512,f479]) ).
fof(f1526,plain,
! [X0] :
( select(queue_11,X0) = select(q9,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f583,f366]) ).
fof(f1538,plain,
s(index_111) = p(index_105),
inference(paramodulation,[status(thm)],[f1523,f736]) ).
fof(f1541,plain,
index_114 = p(index_105),
inference(forward_demodulation,[status(thm)],[f481,f1538]) ).
fof(f1542,plain,
index_114 = index_99,
inference(forward_demodulation,[status(thm)],[f1514,f1541]) ).
fof(f1544,plain,
p(index_99) = index_111,
inference(backward_demodulation,[status(thm)],[f1542,f756]) ).
fof(f1547,plain,
index_99 = s(index_111),
inference(backward_demodulation,[status(thm)],[f1542,f481]) ).
fof(f1563,plain,
! [X0] :
( select(queue_113,X0) = select(q25,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f584,f366]) ).
fof(f1565,plain,
q26 = store(queue_113,tail,index_114),
inference(forward_demodulation,[status(thm)],[f696,f585]) ).
fof(f1566,plain,
q26 = store(queue_113,tail,index_99),
inference(forward_demodulation,[status(thm)],[f1542,f1565]) ).
fof(f1567,plain,
! [X0] :
( select(q26,X0) = select(queue_113,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1566,f366]) ).
fof(f1568,plain,
select(q26,tail) = index_99,
inference(paramodulation,[status(thm)],[f1566,f364]) ).
fof(f1759,plain,
! [X0] :
( select(queue_119,X0) = select(q26,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f586,f366]) ).
fof(f1761,plain,
q27 = store(queue_119,tail,index_120),
inference(forward_demodulation,[status(thm)],[f697,f587]) ).
fof(f1762,plain,
! [X0] :
( select(q27,X0) = select(queue_119,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1761,f366]) ).
fof(f1763,plain,
select(q27,tail) = index_120,
inference(paramodulation,[status(thm)],[f1761,f364]) ).
fof(f1764,plain,
index_123 = index_120,
inference(forward_demodulation,[status(thm)],[f485,f1763]) ).
fof(f1765,plain,
! [X0] :
( select(queue_125,X0) = select(q27,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f588,f366]) ).
fof(f1768,plain,
s(index_123) = p(index_117),
inference(backward_demodulation,[status(thm)],[f1764,f1206]) ).
fof(f1773,plain,
index_126 = p(index_117),
inference(forward_demodulation,[status(thm)],[f486,f1768]) ).
fof(f1778,plain,
s(index_126) = index_117,
inference(paramodulation,[status(thm)],[f1773,f371]) ).
fof(f1791,plain,
q28 = store(queue_125,tail,index_126),
inference(forward_demodulation,[status(thm)],[f698,f589]) ).
fof(f1792,plain,
! [X0] :
( select(q28,X0) = select(queue_125,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1791,f366]) ).
fof(f1793,plain,
select(q28,tail) = index_126,
inference(paramodulation,[status(thm)],[f1791,f364]) ).
fof(f1794,plain,
index_129 = index_126,
inference(forward_demodulation,[status(thm)],[f487,f1793]) ).
fof(f1805,plain,
index_132 = index_117,
inference(backward_demodulation,[status(thm)],[f1806,f488]) ).
fof(f1806,plain,
s(index_129) = index_117,
inference(forward_demodulation,[status(thm)],[f1794,f1778]) ).
fof(f1831,plain,
q10 = store(queue_11,tail,index_12),
inference(forward_demodulation,[status(thm)],[f679,f590]) ).
fof(f1832,plain,
! [X0] :
( select(q10,X0) = select(queue_11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1831,f366]) ).
fof(f1833,plain,
select(q10,tail) = index_12,
inference(paramodulation,[status(thm)],[f1831,f364]) ).
fof(f1834,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f494,f1833]) ).
fof(f1835,plain,
! [X0] :
( select(queue_131,X0) = select(q28,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f591,f366]) ).
fof(f1838,plain,
s(index_15) = p(index_9),
inference(backward_demodulation,[status(thm)],[f1834,f1207]) ).
fof(f1839,plain,
p(index_15) = index_9,
inference(backward_demodulation,[status(thm)],[f1834,f760]) ).
fof(f1842,plain,
index_15 = s(index_9),
inference(backward_demodulation,[status(thm)],[f1834,f483]) ).
fof(f1843,plain,
index_18 = p(index_9),
inference(forward_demodulation,[status(thm)],[f505,f1838]) ).
fof(f1852,plain,
s(index_18) = index_9,
inference(paramodulation,[status(thm)],[f1843,f371]) ).
fof(f1871,plain,
q29 = store(queue_131,tail,index_132),
inference(forward_demodulation,[status(thm)],[f699,f592]) ).
fof(f1872,plain,
q29 = store(queue_131,tail,index_117),
inference(forward_demodulation,[status(thm)],[f1805,f1871]) ).
fof(f1873,plain,
! [X0] :
( select(q29,X0) = select(queue_131,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1872,f366]) ).
fof(f1874,plain,
select(q29,tail) = index_117,
inference(paramodulation,[status(thm)],[f1872,f364]) ).
fof(f1875,plain,
! [X0] :
( select(queue_137,X0) = select(q2,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f593,f366]) ).
fof(f1877,plain,
q3 = store(queue_137,tail,index_138),
inference(forward_demodulation,[status(thm)],[f700,f594]) ).
fof(f1878,plain,
! [X0] :
( select(q3,X0) = select(queue_137,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1877,f366]) ).
fof(f1879,plain,
select(q3,tail) = index_138,
inference(paramodulation,[status(thm)],[f1877,f364]) ).
fof(f1880,plain,
index_201 = index_138,
inference(forward_demodulation,[status(thm)],[f513,f1879]) ).
fof(f1882,plain,
s(index_201) = p(index_135),
inference(backward_demodulation,[status(thm)],[f1880,f1203]) ).
fof(f1886,plain,
index_201 = s(index_135),
inference(backward_demodulation,[status(thm)],[f1880,f490]) ).
fof(f1887,plain,
index_204 = p(index_135),
inference(forward_demodulation,[status(thm)],[f514,f1882]) ).
fof(f1892,plain,
s(index_204) = index_135,
inference(paramodulation,[status(thm)],[f1887,f371]) ).
fof(f1905,plain,
! [X0] :
( select(queue_143,X0) = select(q29,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f595,f366]) ).
fof(f1913,plain,
q30 = store(queue_143,tail,index_144),
inference(forward_demodulation,[status(thm)],[f701,f596]) ).
fof(f1914,plain,
! [X0] :
( select(q30,X0) = select(queue_143,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1913,f366]) ).
fof(f1915,plain,
select(q30,tail) = index_144,
inference(paramodulation,[status(thm)],[f1913,f364]) ).
fof(f1916,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f493,f1915]) ).
fof(f1917,plain,
! [X0] :
( select(queue_149,X0) = select(q30,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f597,f366]) ).
fof(f1924,plain,
index_147 = s(index_141),
inference(backward_demodulation,[status(thm)],[f1916,f492]) ).
fof(f1950,plain,
q31 = store(queue_149,tail,index_150),
inference(forward_demodulation,[status(thm)],[f702,f598]) ).
fof(f1951,plain,
! [X0] :
( select(q31,X0) = select(queue_149,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1950,f366]) ).
fof(f1952,plain,
select(q31,tail) = index_150,
inference(paramodulation,[status(thm)],[f1950,f364]) ).
fof(f1953,plain,
index_153 = index_150,
inference(forward_demodulation,[status(thm)],[f496,f1952]) ).
fof(f1954,plain,
! [X0] :
( select(queue_155,X0) = select(q31,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f599,f366]) ).
fof(f1956,plain,
q32 = store(queue_155,tail,index_156),
inference(forward_demodulation,[status(thm)],[f703,f600]) ).
fof(f1957,plain,
! [X0] :
( select(q32,X0) = select(queue_155,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1956,f366]) ).
fof(f1958,plain,
select(q32,tail) = index_156,
inference(paramodulation,[status(thm)],[f1956,f364]) ).
fof(f1959,plain,
index_159 = index_156,
inference(forward_demodulation,[status(thm)],[f498,f1958]) ).
fof(f1964,plain,
p(index_153) = index_147,
inference(backward_demodulation,[status(thm)],[f1953,f788]) ).
fof(f1968,plain,
s(index_159) = p(index_153),
inference(backward_demodulation,[status(thm)],[f1959,f1200]) ).
fof(f1973,plain,
index_162 = p(index_153),
inference(forward_demodulation,[status(thm)],[f499,f1968]) ).
fof(f1975,plain,
! [X0] :
( select(queue_161,X0) = select(q32,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f601,f366]) ).
fof(f2003,plain,
index_162 = index_147,
inference(forward_demodulation,[status(thm)],[f1964,f1973]) ).
fof(f2015,plain,
q33 = store(queue_161,tail,index_162),
inference(forward_demodulation,[status(thm)],[f704,f602]) ).
fof(f2016,plain,
q33 = store(queue_161,tail,index_147),
inference(forward_demodulation,[status(thm)],[f2003,f2015]) ).
fof(f2017,plain,
! [X0] :
( select(q33,X0) = select(queue_161,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2016,f366]) ).
fof(f2018,plain,
select(q33,tail) = index_147,
inference(paramodulation,[status(thm)],[f2016,f364]) ).
fof(f2019,plain,
! [X0] :
( select(queue_167,X0) = select(q33,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f603,f366]) ).
fof(f2023,plain,
index_117 = index_99,
inference(backward_demodulation,[status(thm)],[f1568,f482]) ).
fof(f2053,plain,
q34 = store(queue_167,tail,index_168),
inference(forward_demodulation,[status(thm)],[f705,f604]) ).
fof(f2054,plain,
! [X0] :
( select(q34,X0) = select(queue_167,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2053,f366]) ).
fof(f2055,plain,
select(q34,tail) = index_168,
inference(paramodulation,[status(thm)],[f2053,f364]) ).
fof(f2056,plain,
index_171 = index_168,
inference(forward_demodulation,[status(thm)],[f502,f2055]) ).
fof(f2057,plain,
! [X0] :
( select(queue_17,X0) = select(q10,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f605,f366]) ).
fof(f2059,plain,
! [X0] :
( select(queue_173,X0) = select(q34,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f606,f366]) ).
fof(f2062,plain,
s(index_171) = p(index_165),
inference(backward_demodulation,[status(thm)],[f2056,f1198]) ).
fof(f2067,plain,
index_174 = p(index_165),
inference(forward_demodulation,[status(thm)],[f503,f2062]) ).
fof(f2073,plain,
s(index_174) = index_165,
inference(paramodulation,[status(thm)],[f2067,f371]) ).
fof(f2082,plain,
q35 = store(queue_173,tail,index_174),
inference(forward_demodulation,[status(thm)],[f706,f607]) ).
fof(f2083,plain,
! [X0] :
( select(q35,X0) = select(queue_173,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2082,f366]) ).
fof(f2084,plain,
select(q35,tail) = index_174,
inference(paramodulation,[status(thm)],[f2082,f364]) ).
fof(f2085,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f504,f2084]) ).
fof(f2099,plain,
index_180 = index_165,
inference(backward_demodulation,[status(thm)],[f2100,f506]) ).
fof(f2100,plain,
s(index_177) = index_165,
inference(forward_demodulation,[status(thm)],[f2085,f2073]) ).
fof(f2119,plain,
! [X0] :
( select(queue_179,X0) = select(q35,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f608,f366]) ).
fof(f2121,plain,
q36 = store(queue_179,tail,index_180),
inference(forward_demodulation,[status(thm)],[f707,f609]) ).
fof(f2122,plain,
q36 = store(queue_179,tail,index_165),
inference(forward_demodulation,[status(thm)],[f2099,f2121]) ).
fof(f2123,plain,
! [X0] :
( select(q36,X0) = select(queue_179,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2122,f366]) ).
fof(f2124,plain,
select(q36,tail) = index_165,
inference(paramodulation,[status(thm)],[f2122,f364]) ).
fof(f2135,plain,
index_141 = index_99,
inference(backward_demodulation,[status(thm)],[f2136,f491]) ).
fof(f2136,plain,
select(q29,tail) = index_99,
inference(forward_demodulation,[status(thm)],[f2023,f1874]) ).
fof(f2142,plain,
index_147 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2135,f1924]) ).
fof(f2148,plain,
index_147 = index_105,
inference(forward_demodulation,[status(thm)],[f1517,f2142]) ).
fof(f2164,plain,
! [X0] :
( select(queue_185,X0) = select(q36,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f610,f366]) ).
fof(f2166,plain,
q37 = store(queue_185,tail,index_186),
inference(forward_demodulation,[status(thm)],[f708,f611]) ).
fof(f2167,plain,
! [X0] :
( select(q37,X0) = select(queue_185,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2166,f366]) ).
fof(f2168,plain,
select(q37,tail) = index_186,
inference(paramodulation,[status(thm)],[f2166,f364]) ).
fof(f2169,plain,
index_189 = index_186,
inference(forward_demodulation,[status(thm)],[f509,f2168]) ).
fof(f2170,plain,
q11 = store(queue_17,tail,index_18),
inference(forward_demodulation,[status(thm)],[f680,f612]) ).
fof(f2171,plain,
! [X0] :
( select(q11,X0) = select(queue_17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2170,f366]) ).
fof(f2172,plain,
select(q11,tail) = index_18,
inference(paramodulation,[status(thm)],[f2170,f364]) ).
fof(f2173,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f516,f2172]) ).
fof(f2176,plain,
! [X0] :
( select(queue_191,X0) = select(q37,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f613,f366]) ).
fof(f2179,plain,
s(index_189) = p(index_183),
inference(backward_demodulation,[status(thm)],[f2169,f1194]) ).
fof(f2184,plain,
index_192 = p(index_183),
inference(forward_demodulation,[status(thm)],[f510,f2179]) ).
fof(f2187,plain,
s(index_21) = index_9,
inference(backward_demodulation,[status(thm)],[f2173,f1852]) ).
fof(f2188,plain,
index_21 = p(index_9),
inference(backward_demodulation,[status(thm)],[f2173,f1843]) ).
fof(f2192,plain,
index_21 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2173,f505]) ).
fof(f2199,plain,
s(index_192) = index_183,
inference(paramodulation,[status(thm)],[f2184,f371]) ).
fof(f2212,plain,
q38 = store(queue_191,tail,index_192),
inference(forward_demodulation,[status(thm)],[f709,f614]) ).
fof(f2213,plain,
! [X0] :
( select(q38,X0) = select(queue_191,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2212,f366]) ).
fof(f2214,plain,
select(q38,tail) = index_192,
inference(paramodulation,[status(thm)],[f2212,f364]) ).
fof(f2215,plain,
index_195 = index_192,
inference(forward_demodulation,[status(thm)],[f511,f2214]) ).
fof(f2216,plain,
! [X0] :
( select(queue_197,X0) = select(q38,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f615,f366]) ).
fof(f2226,plain,
index_24 = index_9,
inference(backward_demodulation,[status(thm)],[f2187,f527]) ).
fof(f2255,plain,
index_198 = index_183,
inference(backward_demodulation,[status(thm)],[f2256,f512]) ).
fof(f2256,plain,
s(index_195) = index_183,
inference(forward_demodulation,[status(thm)],[f2215,f2199]) ).
fof(f2285,plain,
q39 = store(queue_197,tail,index_198),
inference(forward_demodulation,[status(thm)],[f710,f616]) ).
fof(f2286,plain,
q39 = store(queue_197,tail,index_183),
inference(forward_demodulation,[status(thm)],[f2255,f2285]) ).
fof(f2287,plain,
! [X0] :
( select(q39,X0) = select(queue_197,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2286,f366]) ).
fof(f2288,plain,
select(q39,tail) = index_183,
inference(paramodulation,[status(thm)],[f2286,f364]) ).
fof(f2289,plain,
! [X0] :
( select(queue_203,X0) = select(q3,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f617,f366]) ).
fof(f2291,plain,
q4 = store(queue_203,tail,index_204),
inference(forward_demodulation,[status(thm)],[f711,f618]) ).
fof(f2292,plain,
! [X0] :
( select(q4,X0) = select(queue_203,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2291,f366]) ).
fof(f2293,plain,
select(q4,tail) = index_204,
inference(paramodulation,[status(thm)],[f2291,f364]) ).
fof(f2294,plain,
index_267 = index_204,
inference(forward_demodulation,[status(thm)],[f537,f2293]) ).
fof(f2296,plain,
s(index_267) = index_135,
inference(backward_demodulation,[status(thm)],[f2294,f1892]) ).
fof(f2297,plain,
index_267 = p(index_135),
inference(backward_demodulation,[status(thm)],[f2294,f1887]) ).
fof(f2299,plain,
p(index_267) = index_201,
inference(backward_demodulation,[status(thm)],[f2294,f830]) ).
fof(f2302,plain,
! [X0] :
( select(queue_209,X0) = select(q39,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f619,f366]) ).
fof(f2304,plain,
index_270 = index_135,
inference(backward_demodulation,[status(thm)],[f2296,f539]) ).
fof(f2321,plain,
q40 = store(queue_209,tail,index_210),
inference(forward_demodulation,[status(thm)],[f712,f620]) ).
fof(f2322,plain,
! [X0] :
( select(q40,X0) = select(queue_209,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2321,f366]) ).
fof(f2323,plain,
select(q40,tail) = index_210,
inference(paramodulation,[status(thm)],[f2321,f364]) ).
fof(f2324,plain,
index_213 = index_210,
inference(forward_demodulation,[status(thm)],[f518,f2323]) ).
fof(f2325,plain,
! [X0] :
( select(queue_215,X0) = select(q40,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f621,f366]) ).
fof(f2332,plain,
index_213 = s(index_207),
inference(backward_demodulation,[status(thm)],[f2324,f517]) ).
fof(f2367,plain,
q41 = store(queue_215,tail,index_216),
inference(forward_demodulation,[status(thm)],[f713,f622]) ).
fof(f2368,plain,
! [X0] :
( select(q41,X0) = select(queue_215,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2367,f366]) ).
fof(f2369,plain,
select(q41,tail) = index_216,
inference(paramodulation,[status(thm)],[f2367,f364]) ).
fof(f2370,plain,
index_219 = index_216,
inference(forward_demodulation,[status(thm)],[f520,f2369]) ).
fof(f2371,plain,
! [X0] :
( select(queue_221,X0) = select(q41,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f623,f366]) ).
fof(f2373,plain,
q42 = store(queue_221,tail,index_222),
inference(forward_demodulation,[status(thm)],[f714,f624]) ).
fof(f2374,plain,
! [X0] :
( select(q42,X0) = select(queue_221,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2373,f366]) ).
fof(f2375,plain,
select(q42,tail) = index_222,
inference(paramodulation,[status(thm)],[f2373,f364]) ).
fof(f2376,plain,
index_225 = index_222,
inference(forward_demodulation,[status(thm)],[f522,f2375]) ).
fof(f2381,plain,
p(index_219) = index_213,
inference(backward_demodulation,[status(thm)],[f2370,f838]) ).
fof(f2385,plain,
s(index_225) = p(index_219),
inference(backward_demodulation,[status(thm)],[f2376,f1188]) ).
fof(f2390,plain,
index_228 = p(index_219),
inference(forward_demodulation,[status(thm)],[f523,f2385]) ).
fof(f2392,plain,
! [X0] :
( select(queue_227,X0) = select(q42,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f625,f366]) ).
fof(f2420,plain,
index_228 = index_213,
inference(forward_demodulation,[status(thm)],[f2381,f2390]) ).
fof(f2432,plain,
q43 = store(queue_227,tail,index_228),
inference(forward_demodulation,[status(thm)],[f715,f626]) ).
fof(f2433,plain,
q43 = store(queue_227,tail,index_213),
inference(forward_demodulation,[status(thm)],[f2420,f2432]) ).
fof(f2434,plain,
! [X0] :
( select(q43,X0) = select(queue_227,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2433,f366]) ).
fof(f2435,plain,
select(q43,tail) = index_213,
inference(paramodulation,[status(thm)],[f2433,f364]) ).
fof(f2436,plain,
! [X0] :
( select(queue_23,X0) = select(q11,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f627,f366]) ).
fof(f2442,plain,
index_165 = index_105,
inference(backward_demodulation,[status(thm)],[f2443,f500]) ).
fof(f2443,plain,
select(q33,tail) = index_105,
inference(forward_demodulation,[status(thm)],[f2148,f2018]) ).
fof(f2469,plain,
! [X0] :
( select(queue_233,X0) = select(q43,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f628,f366]) ).
fof(f2471,plain,
q44 = store(queue_233,tail,index_234),
inference(forward_demodulation,[status(thm)],[f716,f629]) ).
fof(f2472,plain,
! [X0] :
( select(q44,X0) = select(queue_233,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2471,f366]) ).
fof(f2473,plain,
select(q44,tail) = index_234,
inference(paramodulation,[status(thm)],[f2471,f364]) ).
fof(f2474,plain,
index_237 = index_234,
inference(forward_demodulation,[status(thm)],[f526,f2473]) ).
fof(f2475,plain,
! [X0] :
( select(queue_239,X0) = select(q44,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f630,f366]) ).
fof(f2481,plain,
p(index_237) = index_231,
inference(backward_demodulation,[status(thm)],[f2474,f850]) ).
fof(f2484,plain,
index_237 = s(index_231),
inference(backward_demodulation,[status(thm)],[f2474,f525]) ).
fof(f2487,plain,
q45 = store(queue_239,tail,index_240),
inference(forward_demodulation,[status(thm)],[f717,f631]) ).
fof(f2488,plain,
! [X0] :
( select(q45,X0) = select(queue_239,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2487,f366]) ).
fof(f2489,plain,
select(q45,tail) = index_240,
inference(paramodulation,[status(thm)],[f2487,f364]) ).
fof(f2490,plain,
index_243 = index_240,
inference(forward_demodulation,[status(thm)],[f529,f2489]) ).
fof(f2493,plain,
s(index_243) = p(index_237),
inference(backward_demodulation,[status(thm)],[f2490,f1184]) ).
fof(f2498,plain,
index_246 = p(index_237),
inference(forward_demodulation,[status(thm)],[f530,f2493]) ).
fof(f2517,plain,
! [X0] :
( select(queue_245,X0) = select(q45,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f632,f366]) ).
fof(f2519,plain,
q46 = store(queue_245,tail,index_246),
inference(forward_demodulation,[status(thm)],[f718,f633]) ).
fof(f2520,plain,
! [X0] :
( select(q46,X0) = select(queue_245,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2519,f366]) ).
fof(f2521,plain,
select(q46,tail) = index_246,
inference(paramodulation,[status(thm)],[f2519,f364]) ).
fof(f2522,plain,
index_249 = index_246,
inference(forward_demodulation,[status(thm)],[f531,f2521]) ).
fof(f2532,plain,
index_249 = p(index_237),
inference(forward_demodulation,[status(thm)],[f2522,f2498]) ).
fof(f2543,plain,
index_252 = s(index_231),
inference(backward_demodulation,[status(thm)],[f2544,f532]) ).
fof(f2544,plain,
index_249 = index_231,
inference(forward_demodulation,[status(thm)],[f2481,f2532]) ).
fof(f2546,plain,
index_252 = index_237,
inference(forward_demodulation,[status(thm)],[f2484,f2543]) ).
fof(f2566,plain,
q12 = store(queue_23,tail,index_24),
inference(forward_demodulation,[status(thm)],[f681,f634]) ).
fof(f2567,plain,
q12 = store(queue_23,tail,index_9),
inference(forward_demodulation,[status(thm)],[f2226,f2566]) ).
fof(f2568,plain,
! [X0] :
( select(q12,X0) = select(queue_23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2567,f366]) ).
fof(f2569,plain,
select(q12,tail) = index_9,
inference(paramodulation,[status(thm)],[f2567,f364]) ).
fof(f2570,plain,
! [X0] :
( select(queue_251,X0) = select(q46,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f635,f366]) ).
fof(f2572,plain,
q47 = store(queue_251,tail,index_252),
inference(forward_demodulation,[status(thm)],[f719,f636]) ).
fof(f2573,plain,
q47 = store(queue_251,tail,index_237),
inference(forward_demodulation,[status(thm)],[f2546,f2572]) ).
fof(f2574,plain,
! [X0] :
( select(q47,X0) = select(queue_251,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2573,f366]) ).
fof(f2575,plain,
select(q47,tail) = index_237,
inference(paramodulation,[status(thm)],[f2573,f364]) ).
fof(f2582,plain,
! [X0] :
( select(queue_257,X0) = select(q47,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f637,f366]) ).
fof(f2587,plain,
q48 = store(queue_257,tail,index_258),
inference(forward_demodulation,[status(thm)],[f720,f638]) ).
fof(f2588,plain,
! [X0] :
( select(q48,X0) = select(queue_257,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2587,f366]) ).
fof(f2589,plain,
select(q48,tail) = index_258,
inference(paramodulation,[status(thm)],[f2587,f364]) ).
fof(f2590,plain,
index_261 = index_258,
inference(forward_demodulation,[status(thm)],[f535,f2589]) ).
fof(f2591,plain,
! [X0] :
( select(queue_263,X0) = select(q48,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f639,f366]) ).
fof(f2592,plain,
select(queue_263,seq) = earray_262,
inference(paramodulation,[status(thm)],[f639,f364]) ).
fof(f2594,plain,
s(index_261) = p(index_255),
inference(backward_demodulation,[status(thm)],[f2590,f1181]) ).
fof(f2598,plain,
index_261 = s(index_255),
inference(backward_demodulation,[status(thm)],[f2590,f534]) ).
fof(f2599,plain,
index_264 = p(index_255),
inference(forward_demodulation,[status(thm)],[f536,f2594]) ).
fof(f2623,plain,
index_183 = index_105,
inference(backward_demodulation,[status(thm)],[f2624,f507]) ).
fof(f2624,plain,
select(q36,tail) = index_105,
inference(forward_demodulation,[status(thm)],[f2442,f2124]) ).
fof(f2651,plain,
q49 = store(queue_263,tail,index_264),
inference(forward_demodulation,[status(thm)],[f721,f640]) ).
fof(f2652,plain,
! [X0] :
( select(q49,X0) = select(queue_263,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2651,f366]) ).
fof(f2653,plain,
select(q49,tail) = index_264,
inference(paramodulation,[status(thm)],[f2651,f364]) ).
fof(f2654,plain,
! [X0] :
( select(queue_269,X0) = select(q4,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f641,f366]) ).
fof(f2656,plain,
q5 = store(queue_269,tail,index_270),
inference(forward_demodulation,[status(thm)],[f722,f642]) ).
fof(f2657,plain,
q5 = store(queue_269,tail,index_135),
inference(forward_demodulation,[status(thm)],[f2304,f2656]) ).
fof(f2658,plain,
! [X0] :
( select(q5,X0) = select(queue_269,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2657,f366]) ).
fof(f2659,plain,
select(q5,tail) = index_135,
inference(paramodulation,[status(thm)],[f2657,f364]) ).
fof(f2663,plain,
! [X0] :
( select(queue_275,X0) = select(q5,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f643,f366]) ).
fof(f2666,plain,
index_207 = index_105,
inference(backward_demodulation,[status(thm)],[f2667,f515]) ).
fof(f2667,plain,
select(q39,tail) = index_105,
inference(forward_demodulation,[status(thm)],[f2623,f2288]) ).
fof(f2673,plain,
index_213 = s(index_105),
inference(backward_demodulation,[status(thm)],[f2666,f2332]) ).
fof(f2679,plain,
index_213 = index_111,
inference(forward_demodulation,[status(thm)],[f1523,f2673]) ).
fof(f2680,plain,
q6 = store(queue_275,tail,index_276),
inference(forward_demodulation,[status(thm)],[f723,f644]) ).
fof(f2681,plain,
! [X0] :
( select(q6,X0) = select(queue_275,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2680,f366]) ).
fof(f2682,plain,
select(q6,tail) = index_276,
inference(paramodulation,[status(thm)],[f2680,f364]) ).
fof(f2683,plain,
index_279 = index_276,
inference(forward_demodulation,[status(thm)],[f542,f2682]) ).
fof(f2684,plain,
! [X0] :
( select(queue_281,X0) = select(q6,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f645,f366]) ).
fof(f2704,plain,
p(index_279) = index_273,
inference(backward_demodulation,[status(thm)],[f2683,f886]) ).
fof(f2726,plain,
q7 = store(queue_281,tail,index_282),
inference(forward_demodulation,[status(thm)],[f724,f646]) ).
fof(f2727,plain,
! [X0] :
( select(q7,X0) = select(queue_281,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2726,f366]) ).
fof(f2728,plain,
select(q7,tail) = index_282,
inference(paramodulation,[status(thm)],[f2726,f364]) ).
fof(f2729,plain,
index_285 = index_282,
inference(forward_demodulation,[status(thm)],[f544,f2728]) ).
fof(f2730,plain,
! [X0] :
( select(queue_287,X0) = select(q7,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f647,f366]) ).
fof(f2732,plain,
q8 = store(queue_287,tail,index_288),
inference(forward_demodulation,[status(thm)],[f725,f648]) ).
fof(f2733,plain,
! [X0] :
( select(q8,X0) = select(queue_287,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2732,f366]) ).
fof(f2734,plain,
select(q8,tail) = index_288,
inference(paramodulation,[status(thm)],[f2732,f364]) ).
fof(f2735,plain,
index_291 = index_288,
inference(forward_demodulation,[status(thm)],[f546,f2734]) ).
fof(f2739,plain,
p(index_285) = index_279,
inference(backward_demodulation,[status(thm)],[f2729,f890]) ).
fof(f2745,plain,
s(index_291) = p(index_285),
inference(backward_demodulation,[status(thm)],[f2735,f1176]) ).
fof(f2750,plain,
index_294 = p(index_285),
inference(forward_demodulation,[status(thm)],[f547,f2745]) ).
fof(f2753,plain,
! [X0] :
( select(queue_29,X0) = select(q12,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f649,f366]) ).
fof(f2788,plain,
index_294 = index_279,
inference(forward_demodulation,[status(thm)],[f2739,f2750]) ).
fof(f2798,plain,
! [X0] :
( select(queue_293,X0) = select(q8,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f650,f366]) ).
fof(f2800,plain,
q9 = store(queue_293,tail,index_294),
inference(forward_demodulation,[status(thm)],[f726,f651]) ).
fof(f2801,plain,
q9 = store(queue_293,tail,index_279),
inference(forward_demodulation,[status(thm)],[f2788,f2800]) ).
fof(f2802,plain,
! [X0] :
( select(q9,X0) = select(queue_293,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2801,f366]) ).
fof(f2803,plain,
select(q9,tail) = index_279,
inference(paramodulation,[status(thm)],[f2801,f364]) ).
fof(f2804,plain,
index_9 = index_279,
inference(forward_demodulation,[status(thm)],[f573,f2803]) ).
fof(f2811,plain,
p(index_9) = index_273,
inference(backward_demodulation,[status(thm)],[f2804,f2704]) ).
fof(f2818,plain,
index_21 = index_273,
inference(forward_demodulation,[status(thm)],[f2188,f2811]) ).
fof(f2832,plain,
index_21 = select(q5,tail),
inference(backward_demodulation,[status(thm)],[f2818,f540]) ).
fof(f2845,plain,
q13 = store(queue_29,tail,index_30),
inference(forward_demodulation,[status(thm)],[f682,f652]) ).
fof(f2846,plain,
! [X0] :
( select(q13,X0) = select(queue_29,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2845,f366]) ).
fof(f2847,plain,
select(q13,tail) = index_30,
inference(paramodulation,[status(thm)],[f2845,f364]) ).
fof(f2848,plain,
index_33 = index_30,
inference(forward_demodulation,[status(thm)],[f553,f2847]) ).
fof(f2849,plain,
! [X0] :
( select(queue_35,X0) = select(q13,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f653,f366]) ).
fof(f2851,plain,
q14 = store(queue_35,tail,index_36),
inference(forward_demodulation,[status(thm)],[f683,f654]) ).
fof(f2852,plain,
! [X0] :
( select(q14,X0) = select(queue_35,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2851,f366]) ).
fof(f2853,plain,
select(q14,tail) = index_36,
inference(paramodulation,[status(thm)],[f2851,f364]) ).
fof(f2854,plain,
index_39 = index_36,
inference(forward_demodulation,[status(thm)],[f555,f2853]) ).
fof(f2857,plain,
p(index_33) = index_27,
inference(backward_demodulation,[status(thm)],[f2848,f904]) ).
fof(f2864,plain,
s(index_39) = p(index_33),
inference(backward_demodulation,[status(thm)],[f2854,f1172]) ).
fof(f2869,plain,
index_42 = p(index_33),
inference(forward_demodulation,[status(thm)],[f556,f2864]) ).
fof(f2872,plain,
! [X0] :
( select(queue_41,X0) = select(q14,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f655,f366]) ).
fof(f2903,plain,
index_42 = index_27,
inference(forward_demodulation,[status(thm)],[f2857,f2869]) ).
fof(f2915,plain,
q15 = store(queue_41,tail,index_42),
inference(forward_demodulation,[status(thm)],[f684,f656]) ).
fof(f2916,plain,
q15 = store(queue_41,tail,index_27),
inference(forward_demodulation,[status(thm)],[f2903,f2915]) ).
fof(f2917,plain,
! [X0] :
( select(q15,X0) = select(queue_41,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2916,f366]) ).
fof(f2918,plain,
select(q15,tail) = index_27,
inference(paramodulation,[status(thm)],[f2916,f364]) ).
fof(f2919,plain,
! [X0] :
( select(queue_47,X0) = select(q15,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f657,f366]) ).
fof(f2929,plain,
q16 = store(queue_47,tail,index_48),
inference(forward_demodulation,[status(thm)],[f685,f658]) ).
fof(f2930,plain,
! [X0] :
( select(q16,X0) = select(queue_47,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2929,f366]) ).
fof(f2931,plain,
select(q16,tail) = index_48,
inference(paramodulation,[status(thm)],[f2929,f364]) ).
fof(f2932,plain,
index_51 = index_48,
inference(forward_demodulation,[status(thm)],[f559,f2931]) ).
fof(f2933,plain,
! [X0] :
( select(queue_5,X0) = select(q0,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f659,f366]) ).
fof(f2935,plain,
! [X0] :
( select(queue_53,X0) = select(q16,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f660,f366]) ).
fof(f2938,plain,
s(index_51) = p(index_45),
inference(backward_demodulation,[status(thm)],[f2932,f1170]) ).
fof(f2943,plain,
index_54 = p(index_45),
inference(forward_demodulation,[status(thm)],[f560,f2938]) ).
fof(f2948,plain,
s(index_54) = index_45,
inference(paramodulation,[status(thm)],[f2943,f371]) ).
fof(f2961,plain,
q17 = store(queue_53,tail,index_54),
inference(forward_demodulation,[status(thm)],[f686,f661]) ).
fof(f2962,plain,
! [X0] :
( select(q17,X0) = select(queue_53,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2961,f366]) ).
fof(f2963,plain,
select(q17,tail) = index_54,
inference(paramodulation,[status(thm)],[f2961,f364]) ).
fof(f2964,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f561,f2963]) ).
fof(f2975,plain,
index_60 = index_45,
inference(backward_demodulation,[status(thm)],[f2976,f563]) ).
fof(f2976,plain,
s(index_57) = index_45,
inference(forward_demodulation,[status(thm)],[f2964,f2948]) ).
fof(f3001,plain,
! [X0] :
( select(queue_59,X0) = select(q17,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f662,f366]) ).
fof(f3003,plain,
q18 = store(queue_59,tail,index_60),
inference(forward_demodulation,[status(thm)],[f687,f663]) ).
fof(f3004,plain,
q18 = store(queue_59,tail,index_45),
inference(forward_demodulation,[status(thm)],[f2975,f3003]) ).
fof(f3005,plain,
! [X0] :
( select(q18,X0) = select(queue_59,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3004,f366]) ).
fof(f3006,plain,
select(q18,tail) = index_45,
inference(paramodulation,[status(thm)],[f3004,f364]) ).
fof(f3012,plain,
index_231 = index_111,
inference(backward_demodulation,[status(thm)],[f3013,f524]) ).
fof(f3013,plain,
select(q43,tail) = index_111,
inference(forward_demodulation,[status(thm)],[f2679,f2435]) ).
fof(f3017,plain,
index_237 = s(index_111),
inference(backward_demodulation,[status(thm)],[f3012,f2484]) ).
fof(f3024,plain,
index_237 = index_99,
inference(forward_demodulation,[status(thm)],[f1547,f3017]) ).
fof(f3042,plain,
! [X0] :
( select(queue_65,X0) = select(q18,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f664,f366]) ).
fof(f3044,plain,
q19 = store(queue_65,tail,index_66),
inference(forward_demodulation,[status(thm)],[f688,f665]) ).
fof(f3045,plain,
! [X0] :
( select(q19,X0) = select(queue_65,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3044,f366]) ).
fof(f3046,plain,
select(q19,tail) = index_66,
inference(paramodulation,[status(thm)],[f3044,f364]) ).
fof(f3047,plain,
index_75 = index_66,
inference(forward_demodulation,[status(thm)],[f568,f3046]) ).
fof(f3048,plain,
q1 = store(queue_5,tail,index_6),
inference(forward_demodulation,[status(thm)],[f678,f666]) ).
fof(f3049,plain,
! [X0] :
( select(q1,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3048,f366]) ).
fof(f3050,plain,
select(q1,tail) = index_6,
inference(paramodulation,[status(thm)],[f3048,f364]) ).
fof(f3051,plain,
index_69 = index_6,
inference(forward_demodulation,[status(thm)],[f566,f3050]) ).
fof(f3058,plain,
index_75 = s(index_63),
inference(backward_demodulation,[status(thm)],[f3047,f565]) ).
fof(f3063,plain,
p(index_69) = index_3,
inference(backward_demodulation,[status(thm)],[f3051,f928]) ).
fof(f3069,plain,
! [X0] :
( select(queue_71,X0) = select(q1,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f667,f366]) ).
fof(f3106,plain,
q2 = store(queue_71,tail,index_72),
inference(forward_demodulation,[status(thm)],[f689,f668]) ).
fof(f3107,plain,
! [X0] :
( select(q2,X0) = select(queue_71,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3106,f366]) ).
fof(f3108,plain,
select(q2,tail) = index_72,
inference(paramodulation,[status(thm)],[f3106,f364]) ).
fof(f3109,plain,
index_135 = index_72,
inference(forward_demodulation,[status(thm)],[f489,f3108]) ).
fof(f3110,plain,
! [X0] :
( select(queue_77,X0) = select(q19,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f669,f366]) ).
fof(f3115,plain,
p(index_135) = index_69,
inference(backward_demodulation,[status(thm)],[f3109,f942]) ).
fof(f3119,plain,
index_267 = index_69,
inference(forward_demodulation,[status(thm)],[f2297,f3115]) ).
fof(f3122,plain,
p(index_267) = index_3,
inference(backward_demodulation,[status(thm)],[f3119,f3063]) ).
fof(f3128,plain,
index_201 = index_3,
inference(forward_demodulation,[status(thm)],[f2299,f3122]) ).
fof(f3134,plain,
index_201 = select(q0,tail),
inference(backward_demodulation,[status(thm)],[f3128,f550]) ).
fof(f3153,plain,
q20 = store(queue_77,tail,index_78),
inference(forward_demodulation,[status(thm)],[f690,f670]) ).
fof(f3154,plain,
! [X0] :
( select(q20,X0) = select(queue_77,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3153,f366]) ).
fof(f3155,plain,
select(q20,tail) = index_78,
inference(paramodulation,[status(thm)],[f3153,f364]) ).
fof(f3156,plain,
index_81 = index_78,
inference(forward_demodulation,[status(thm)],[f570,f3155]) ).
fof(f3157,plain,
! [X0] :
( select(queue_83,X0) = select(q20,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f671,f366]) ).
fof(f3159,plain,
q21 = store(queue_83,tail,index_84),
inference(forward_demodulation,[status(thm)],[f691,f672]) ).
fof(f3160,plain,
! [X0] :
( select(q21,X0) = select(queue_83,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3159,f366]) ).
fof(f3161,plain,
select(q21,tail) = index_84,
inference(paramodulation,[status(thm)],[f3159,f364]) ).
fof(f3162,plain,
index_87 = index_84,
inference(forward_demodulation,[status(thm)],[f572,f3161]) ).
fof(f3167,plain,
p(index_81) = index_75,
inference(backward_demodulation,[status(thm)],[f3156,f948]) ).
fof(f3171,plain,
s(index_87) = p(index_81),
inference(backward_demodulation,[status(thm)],[f3162,f1163]) ).
fof(f3176,plain,
index_90 = p(index_81),
inference(forward_demodulation,[status(thm)],[f574,f3171]) ).
fof(f3178,plain,
! [X0] :
( select(queue_89,X0) = select(q21,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f673,f366]) ).
fof(f3209,plain,
index_90 = index_75,
inference(forward_demodulation,[status(thm)],[f3167,f3176]) ).
fof(f3220,plain,
q22 = store(queue_89,tail,index_90),
inference(forward_demodulation,[status(thm)],[f692,f674]) ).
fof(f3221,plain,
q22 = store(queue_89,tail,index_75),
inference(forward_demodulation,[status(thm)],[f3209,f3220]) ).
fof(f3222,plain,
! [X0] :
( select(q22,X0) = select(queue_89,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3221,f366]) ).
fof(f3223,plain,
select(q22,tail) = index_75,
inference(paramodulation,[status(thm)],[f3221,f364]) ).
fof(f3224,plain,
! [X0] :
( select(queue_95,X0) = select(q22,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f675,f366]) ).
fof(f3233,plain,
q23 = store(queue_95,tail,index_96),
inference(forward_demodulation,[status(thm)],[f693,f676]) ).
fof(f3234,plain,
! [X0] :
( select(q23,X0) = select(queue_95,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3233,f366]) ).
fof(f3235,plain,
select(q23,tail) = index_96,
inference(paramodulation,[status(thm)],[f3233,f364]) ).
fof(f3236,plain,
index_99 = index_96,
inference(forward_demodulation,[status(thm)],[f577,f3235]) ).
fof(f3243,plain,
p(index_99) = index_93,
inference(backward_demodulation,[status(thm)],[f3236,f960]) ).
fof(f3248,plain,
index_111 = index_93,
inference(forward_demodulation,[status(thm)],[f1544,f3243]) ).
fof(f3252,plain,
index_111 = select(q22,tail),
inference(backward_demodulation,[status(thm)],[f3248,f575]) ).
fof(f3261,plain,
index_27 = index_9,
inference(backward_demodulation,[status(thm)],[f2569,f538]) ).
fof(f3297,plain,
index_255 = index_99,
inference(backward_demodulation,[status(thm)],[f3298,f533]) ).
fof(f3298,plain,
select(q47,tail) = index_99,
inference(forward_demodulation,[status(thm)],[f3024,f2575]) ).
fof(f3300,plain,
index_261 = s(index_99),
inference(backward_demodulation,[status(thm)],[f3297,f2598]) ).
fof(f3302,plain,
index_264 = p(index_99),
inference(backward_demodulation,[status(thm)],[f3297,f2599]) ).
fof(f3307,plain,
index_261 = index_105,
inference(forward_demodulation,[status(thm)],[f1517,f3300]) ).
fof(f3308,plain,
index_264 = index_111,
inference(forward_demodulation,[status(thm)],[f1544,f3302]) ).
fof(f3310,plain,
select(earray_262,index_105) = e48,
inference(backward_demodulation,[status(thm)],[f3307,f1154]) ).
fof(f3332,plain,
index_299 = index_111,
inference(backward_demodulation,[status(thm)],[f3333,f549]) ).
fof(f3333,plain,
select(q49,tail) = index_111,
inference(forward_demodulation,[status(thm)],[f3308,f2653]) ).
fof(f3338,plain,
p(index_111) = index_300,
inference(backward_demodulation,[status(thm)],[f3332,f908]) ).
fof(f3343,plain,
index_105 = index_300,
inference(forward_demodulation,[status(thm)],[f1520,f3338]) ).
fof(f3345,plain,
elem_301 = select(earray_296,index_105),
inference(backward_demodulation,[status(thm)],[f3343,f475]) ).
fof(f3368,plain,
index_135 = s(index_15),
inference(backward_demodulation,[status(thm)],[f3378,f2192]) ).
fof(f3378,plain,
index_21 = index_135,
inference(forward_demodulation,[status(thm)],[f2659,f2832]) ).
fof(f3388,plain,
s(index_135) = p(index_15),
inference(paramodulation,[status(thm)],[f3368,f736]) ).
fof(f3391,plain,
index_201 = p(index_15),
inference(forward_demodulation,[status(thm)],[f1886,f3388]) ).
fof(f3392,plain,
index_201 = index_9,
inference(forward_demodulation,[status(thm)],[f1839,f3391]) ).
fof(f3441,plain,
index_45 = index_9,
inference(backward_demodulation,[status(thm)],[f3442,f557]) ).
fof(f3442,plain,
select(q15,tail) = index_9,
inference(forward_demodulation,[status(thm)],[f3261,f2918]) ).
fof(f3482,plain,
index_63 = index_9,
inference(backward_demodulation,[status(thm)],[f3483,f564]) ).
fof(f3483,plain,
select(q18,tail) = index_9,
inference(forward_demodulation,[status(thm)],[f3441,f3006]) ).
fof(f3489,plain,
index_75 = s(index_9),
inference(backward_demodulation,[status(thm)],[f3482,f3058]) ).
fof(f3495,plain,
index_75 = index_15,
inference(forward_demodulation,[status(thm)],[f1842,f3489]) ).
fof(f3534,plain,
index_9 = select(q0,tail),
inference(forward_demodulation,[status(thm)],[f3392,f3134]) ).
fof(f3540,plain,
select(q22,tail) = index_15,
inference(forward_demodulation,[status(thm)],[f3495,f3223]) ).
fof(f3541,plain,
index_111 = index_15,
inference(backward_demodulation,[status(thm)],[f3252,f3540]) ).
fof(f3565,plain,
p(index_111) = index_9,
inference(backward_demodulation,[status(thm)],[f3541,f1839]) ).
fof(f3614,plain,
index_9 = index_105,
inference(backward_demodulation,[status(thm)],[f3565,f1520]) ).
fof(f3631,plain,
elem_301 = select(earray_296,index_9),
inference(backward_demodulation,[status(thm)],[f3614,f3345]) ).
fof(f3704,plain,
select(earray_262,index_9) = e48,
inference(forward_demodulation,[status(thm)],[f3614,f3310]) ).
fof(f4029,plain,
( select(q0,tail) = index_0
| head = tail ),
inference(paramodulation,[status(thm)],[f476,f1409]) ).
fof(f4031,plain,
( index_9 = index_0
| head = tail ),
inference(forward_demodulation,[status(thm)],[f3534,f4029]) ).
fof(f4032,plain,
index_9 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[f4031,f367]) ).
fof(f4035,plain,
select(q0,head) = index_9,
inference(backward_demodulation,[status(thm)],[f4032,f1410]) ).
fof(f4045,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1411,f1504]) ).
fof(f4055,plain,
! [X0] :
( seq = X0
| select(q25,X0) = select(q24,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1507,f1510]) ).
fof(f4077,plain,
! [X0] :
( seq = X0
| select(q26,X0) = select(q25,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1563,f1567]) ).
fof(f4092,plain,
! [X0] :
( seq = X0
| select(q27,X0) = select(q26,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1759,f1762]) ).
fof(f4107,plain,
! [X0] :
( seq = X0
| select(q28,X0) = select(q27,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1765,f1792]) ).
fof(f4120,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q9,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1526,f1832]) ).
fof(f4135,plain,
! [X0] :
( seq = X0
| select(q29,X0) = select(q28,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1835,f1873]) ).
fof(f4150,plain,
! [X0] :
( seq = X0
| select(q3,X0) = select(q2,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1875,f1878]) ).
fof(f4160,plain,
! [X0] :
( seq = X0
| select(q30,X0) = select(q29,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1905,f1914]) ).
fof(f4180,plain,
! [X0] :
( seq = X0
| select(q31,X0) = select(q30,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1917,f1951]) ).
fof(f4195,plain,
! [X0] :
( seq = X0
| select(q32,X0) = select(q31,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1954,f1957]) ).
fof(f4210,plain,
! [X0] :
( seq = X0
| select(q33,X0) = select(q32,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f1975,f2017]) ).
fof(f4225,plain,
! [X0] :
( seq = X0
| select(q34,X0) = select(q33,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2019,f2054]) ).
fof(f4242,plain,
! [X0] :
( seq = X0
| select(q35,X0) = select(q34,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2059,f2083]) ).
fof(f4257,plain,
! [X0] :
( seq = X0
| select(q36,X0) = select(q35,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2119,f2123]) ).
fof(f4272,plain,
! [X0] :
( seq = X0
| select(q37,X0) = select(q36,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2164,f2167]) ).
fof(f4285,plain,
! [X0] :
( seq = X0
| select(q11,X0) = select(q10,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2057,f2171]) ).
fof(f4300,plain,
! [X0] :
( seq = X0
| select(q38,X0) = select(q37,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2176,f2213]) ).
fof(f4315,plain,
! [X0] :
( seq = X0
| select(q39,X0) = select(q38,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2216,f2287]) ).
fof(f4330,plain,
! [X0] :
( seq = X0
| select(q4,X0) = select(q3,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2289,f2292]) ).
fof(f4345,plain,
! [X0] :
( seq = X0
| select(q40,X0) = select(q39,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2302,f2322]) ).
fof(f4360,plain,
! [X0] :
( seq = X0
| select(q41,X0) = select(q40,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2325,f2368]) ).
fof(f4370,plain,
! [X0] :
( seq = X0
| select(q42,X0) = select(q41,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2371,f2374]) ).
fof(f4390,plain,
! [X0] :
( seq = X0
| select(q43,X0) = select(q42,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2392,f2434]) ).
fof(f4407,plain,
! [X0] :
( seq = X0
| select(q44,X0) = select(q43,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2469,f2472]) ).
fof(f4422,plain,
! [X0] :
( seq = X0
| select(q45,X0) = select(q44,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2475,f2488]) ).
fof(f4437,plain,
! [X0] :
( seq = X0
| select(q46,X0) = select(q45,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2517,f2520]) ).
fof(f4450,plain,
! [X0] :
( seq = X0
| select(q12,X0) = select(q11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2436,f2568]) ).
fof(f4465,plain,
! [X0] :
( seq = X0
| select(q47,X0) = select(q46,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2570,f2574]) ).
fof(f4475,plain,
! [X0] :
( seq = X0
| select(q48,X0) = select(q47,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2582,f2588]) ).
fof(f4494,plain,
( select(q49,seq) = earray_262
| tail = seq ),
inference(paramodulation,[status(thm)],[f2592,f2652]) ).
fof(f4495,plain,
! [X0] :
( seq = X0
| select(q49,X0) = select(q48,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2591,f2652]) ).
fof(f4498,plain,
( earray_296 = earray_262
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f448,f4494]) ).
fof(f4499,plain,
earray_296 = earray_262,
inference(forward_subsumption_resolution,[status(thm)],[f4498,f369]) ).
fof(f4502,plain,
elem_301 = select(earray_262,index_9),
inference(backward_demodulation,[status(thm)],[f4499,f3631]) ).
fof(f4504,plain,
elem_298 = select(earray_262,index_297),
inference(backward_demodulation,[status(thm)],[f4499,f474]) ).
fof(f4505,plain,
elem_301 = e48,
inference(forward_demodulation,[status(thm)],[f3704,f4502]) ).
fof(f4506,plain,
elem_298 != e48,
inference(backward_demodulation,[status(thm)],[f4505,f727]) ).
fof(f4510,plain,
! [X0] :
( seq = X0
| select(q5,X0) = select(q4,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2654,f2658]) ).
fof(f4520,plain,
! [X0] :
( seq = X0
| select(q6,X0) = select(q5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2663,f2681]) ).
fof(f4540,plain,
! [X0] :
( seq = X0
| select(q7,X0) = select(q6,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2684,f2727]) ).
fof(f4555,plain,
! [X0] :
( seq = X0
| select(q8,X0) = select(q7,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2730,f2733]) ).
fof(f4572,plain,
! [X0] :
( seq = X0
| select(q9,X0) = select(q8,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2798,f2802]) ).
fof(f4596,plain,
! [X0] :
( seq = X0
| select(q13,X0) = select(q12,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2753,f2846]) ).
fof(f4611,plain,
! [X0] :
( seq = X0
| select(q14,X0) = select(q13,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2849,f2852]) ).
fof(f4626,plain,
! [X0] :
( seq = X0
| select(q15,X0) = select(q14,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2872,f2917]) ).
fof(f4641,plain,
! [X0] :
( seq = X0
| select(q16,X0) = select(q15,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2919,f2930]) ).
fof(f4658,plain,
! [X0] :
( seq = X0
| select(q17,X0) = select(q16,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2935,f2962]) ).
fof(f4673,plain,
! [X0] :
( seq = X0
| select(q18,X0) = select(q17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3001,f3005]) ).
fof(f4688,plain,
! [X0] :
( seq = X0
| select(q19,X0) = select(q18,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3042,f3045]) ).
fof(f4701,plain,
! [X0] :
( seq = X0
| select(q1,X0) = select(q0,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2933,f3049]) ).
fof(f4716,plain,
! [X0] :
( seq = X0
| select(q2,X0) = select(q1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3069,f3107]) ).
fof(f4738,plain,
! [X0] :
( seq = X0
| select(q20,X0) = select(q19,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3110,f3154]) ).
fof(f4753,plain,
! [X0] :
( seq = X0
| select(q21,X0) = select(q20,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3157,f3160]) ).
fof(f4768,plain,
! [X0] :
( seq = X0
| select(q22,X0) = select(q21,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3178,f3222]) ).
fof(f4783,plain,
! [X0] :
( seq = X0
| select(q23,X0) = select(q22,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3224,f3234]) ).
fof(f5193,plain,
( seq = head
| index_297 = select(q48,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f548,f4495]) ).
fof(f5197,plain,
( seq = head
| index_297 = select(q48,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5193,f367]) ).
fof(f5199,plain,
index_297 = select(q48,head),
inference(forward_subsumption_resolution,[status(thm)],[f5197,f368]) ).
fof(f5200,plain,
( seq = head
| tail = head
| index_297 = select(q47,head) ),
inference(paramodulation,[status(thm)],[f4475,f5199]) ).
fof(f5202,plain,
( seq = head
| index_297 = select(q47,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5200,f367]) ).
fof(f5204,plain,
index_297 = select(q47,head),
inference(forward_subsumption_resolution,[status(thm)],[f5202,f368]) ).
fof(f5205,plain,
( seq = head
| tail = head
| index_297 = select(q46,head) ),
inference(paramodulation,[status(thm)],[f4465,f5204]) ).
fof(f5207,plain,
( seq = head
| index_297 = select(q46,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5205,f367]) ).
fof(f5213,plain,
index_297 = select(q46,head),
inference(forward_subsumption_resolution,[status(thm)],[f5207,f368]) ).
fof(f5214,plain,
( seq = head
| tail = head
| index_297 = select(q45,head) ),
inference(paramodulation,[status(thm)],[f4437,f5213]) ).
fof(f5216,plain,
( seq = head
| index_297 = select(q45,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5214,f367]) ).
fof(f5218,plain,
index_297 = select(q45,head),
inference(forward_subsumption_resolution,[status(thm)],[f5216,f368]) ).
fof(f5219,plain,
( seq = head
| tail = head
| index_297 = select(q44,head) ),
inference(paramodulation,[status(thm)],[f4422,f5218]) ).
fof(f5221,plain,
( seq = head
| index_297 = select(q44,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5219,f367]) ).
fof(f5223,plain,
index_297 = select(q44,head),
inference(forward_subsumption_resolution,[status(thm)],[f5221,f368]) ).
fof(f5224,plain,
( seq = head
| tail = head
| index_297 = select(q43,head) ),
inference(paramodulation,[status(thm)],[f4407,f5223]) ).
fof(f5226,plain,
( seq = head
| index_297 = select(q43,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5224,f367]) ).
fof(f5228,plain,
index_297 = select(q43,head),
inference(forward_subsumption_resolution,[status(thm)],[f5226,f368]) ).
fof(f5229,plain,
( seq = head
| tail = head
| index_297 = select(q42,head) ),
inference(paramodulation,[status(thm)],[f4390,f5228]) ).
fof(f5231,plain,
( seq = head
| index_297 = select(q42,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5229,f367]) ).
fof(f5233,plain,
index_297 = select(q42,head),
inference(forward_subsumption_resolution,[status(thm)],[f5231,f368]) ).
fof(f5234,plain,
( seq = head
| tail = head
| index_297 = select(q41,head) ),
inference(paramodulation,[status(thm)],[f4370,f5233]) ).
fof(f5236,plain,
( seq = head
| index_297 = select(q41,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5234,f367]) ).
fof(f5238,plain,
index_297 = select(q41,head),
inference(forward_subsumption_resolution,[status(thm)],[f5236,f368]) ).
fof(f5239,plain,
( seq = head
| tail = head
| index_297 = select(q40,head) ),
inference(paramodulation,[status(thm)],[f4360,f5238]) ).
fof(f5241,plain,
( seq = head
| index_297 = select(q40,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5239,f367]) ).
fof(f5243,plain,
index_297 = select(q40,head),
inference(forward_subsumption_resolution,[status(thm)],[f5241,f368]) ).
fof(f5244,plain,
( seq = head
| tail = head
| index_297 = select(q39,head) ),
inference(paramodulation,[status(thm)],[f4345,f5243]) ).
fof(f5246,plain,
( seq = head
| index_297 = select(q39,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5244,f367]) ).
fof(f5248,plain,
index_297 = select(q39,head),
inference(forward_subsumption_resolution,[status(thm)],[f5246,f368]) ).
fof(f5249,plain,
( seq = head
| tail = head
| index_297 = select(q38,head) ),
inference(paramodulation,[status(thm)],[f4315,f5248]) ).
fof(f5251,plain,
( seq = head
| index_297 = select(q38,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5249,f367]) ).
fof(f5253,plain,
index_297 = select(q38,head),
inference(forward_subsumption_resolution,[status(thm)],[f5251,f368]) ).
fof(f5254,plain,
( seq = head
| tail = head
| index_297 = select(q37,head) ),
inference(paramodulation,[status(thm)],[f4300,f5253]) ).
fof(f5256,plain,
( seq = head
| index_297 = select(q37,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5254,f367]) ).
fof(f5262,plain,
index_297 = select(q37,head),
inference(forward_subsumption_resolution,[status(thm)],[f5256,f368]) ).
fof(f5263,plain,
( seq = head
| tail = head
| index_297 = select(q36,head) ),
inference(paramodulation,[status(thm)],[f4272,f5262]) ).
fof(f5265,plain,
( seq = head
| index_297 = select(q36,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5263,f367]) ).
fof(f5267,plain,
index_297 = select(q36,head),
inference(forward_subsumption_resolution,[status(thm)],[f5265,f368]) ).
fof(f5268,plain,
( seq = head
| tail = head
| index_297 = select(q35,head) ),
inference(paramodulation,[status(thm)],[f4257,f5267]) ).
fof(f5270,plain,
( seq = head
| index_297 = select(q35,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5268,f367]) ).
fof(f5272,plain,
index_297 = select(q35,head),
inference(forward_subsumption_resolution,[status(thm)],[f5270,f368]) ).
fof(f5273,plain,
( seq = head
| tail = head
| index_297 = select(q34,head) ),
inference(paramodulation,[status(thm)],[f4242,f5272]) ).
fof(f5275,plain,
( seq = head
| index_297 = select(q34,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5273,f367]) ).
fof(f5281,plain,
index_297 = select(q34,head),
inference(forward_subsumption_resolution,[status(thm)],[f5275,f368]) ).
fof(f5282,plain,
( seq = head
| tail = head
| index_297 = select(q33,head) ),
inference(paramodulation,[status(thm)],[f4225,f5281]) ).
fof(f5284,plain,
( seq = head
| index_297 = select(q33,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5282,f367]) ).
fof(f5286,plain,
index_297 = select(q33,head),
inference(forward_subsumption_resolution,[status(thm)],[f5284,f368]) ).
fof(f5287,plain,
( seq = head
| tail = head
| index_297 = select(q32,head) ),
inference(paramodulation,[status(thm)],[f4210,f5286]) ).
fof(f5289,plain,
( seq = head
| index_297 = select(q32,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5287,f367]) ).
fof(f5291,plain,
index_297 = select(q32,head),
inference(forward_subsumption_resolution,[status(thm)],[f5289,f368]) ).
fof(f5292,plain,
( seq = head
| tail = head
| index_297 = select(q31,head) ),
inference(paramodulation,[status(thm)],[f4195,f5291]) ).
fof(f5294,plain,
( seq = head
| index_297 = select(q31,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5292,f367]) ).
fof(f5296,plain,
index_297 = select(q31,head),
inference(forward_subsumption_resolution,[status(thm)],[f5294,f368]) ).
fof(f5297,plain,
( seq = head
| tail = head
| index_297 = select(q30,head) ),
inference(paramodulation,[status(thm)],[f4180,f5296]) ).
fof(f5299,plain,
( seq = head
| index_297 = select(q30,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5297,f367]) ).
fof(f5301,plain,
index_297 = select(q30,head),
inference(forward_subsumption_resolution,[status(thm)],[f5299,f368]) ).
fof(f5302,plain,
( seq = head
| tail = head
| index_297 = select(q29,head) ),
inference(paramodulation,[status(thm)],[f4160,f5301]) ).
fof(f5304,plain,
( seq = head
| index_297 = select(q29,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5302,f367]) ).
fof(f5306,plain,
index_297 = select(q29,head),
inference(forward_subsumption_resolution,[status(thm)],[f5304,f368]) ).
fof(f5307,plain,
( seq = head
| tail = head
| index_297 = select(q28,head) ),
inference(paramodulation,[status(thm)],[f4135,f5306]) ).
fof(f5309,plain,
( seq = head
| index_297 = select(q28,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5307,f367]) ).
fof(f5315,plain,
index_297 = select(q28,head),
inference(forward_subsumption_resolution,[status(thm)],[f5309,f368]) ).
fof(f5316,plain,
( seq = head
| tail = head
| index_297 = select(q27,head) ),
inference(paramodulation,[status(thm)],[f4107,f5315]) ).
fof(f5318,plain,
( seq = head
| index_297 = select(q27,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5316,f367]) ).
fof(f5320,plain,
index_297 = select(q27,head),
inference(forward_subsumption_resolution,[status(thm)],[f5318,f368]) ).
fof(f5321,plain,
( seq = head
| tail = head
| index_297 = select(q26,head) ),
inference(paramodulation,[status(thm)],[f4092,f5320]) ).
fof(f5323,plain,
( seq = head
| index_297 = select(q26,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5321,f367]) ).
fof(f5325,plain,
index_297 = select(q26,head),
inference(forward_subsumption_resolution,[status(thm)],[f5323,f368]) ).
fof(f5326,plain,
( seq = head
| tail = head
| index_297 = select(q25,head) ),
inference(paramodulation,[status(thm)],[f4077,f5325]) ).
fof(f5328,plain,
( seq = head
| index_297 = select(q25,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5326,f367]) ).
fof(f5330,plain,
index_297 = select(q25,head),
inference(forward_subsumption_resolution,[status(thm)],[f5328,f368]) ).
fof(f5331,plain,
( seq = head
| tail = head
| index_297 = select(q24,head) ),
inference(paramodulation,[status(thm)],[f4055,f5330]) ).
fof(f5333,plain,
( seq = head
| index_297 = select(q24,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f5331,f367]) ).
fof(f5335,plain,
index_297 = select(q24,head),
inference(forward_subsumption_resolution,[status(thm)],[f5333,f368]) ).
fof(f5338,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q8,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4120,f4572]) ).
fof(f5342,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q8,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5338]) ).
fof(f5378,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q2,X0) = select(q0,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4701,f4716]) ).
fof(f5382,plain,
! [X0] :
( seq = X0
| select(q2,X0) = select(q0,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5378]) ).
fof(f5398,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q22,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4045,f4783]) ).
fof(f5402,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q22,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5398]) ).
fof(f5424,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q7,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4555,f5342]) ).
fof(f5428,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q7,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5424]) ).
fof(f5430,plain,
( seq = head
| select(q2,head) = index_9
| tail = head ),
inference(paramodulation,[status(thm)],[f4035,f5382]) ).
fof(f5436,plain,
( seq = head
| select(q2,head) = index_9 ),
inference(forward_subsumption_resolution,[status(thm)],[f5430,f367]) ).
fof(f5438,plain,
select(q2,head) = index_9,
inference(forward_subsumption_resolution,[status(thm)],[f5436,f368]) ).
fof(f5441,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q21,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4768,f5402]) ).
fof(f5445,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q21,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5441]) ).
fof(f5449,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q6,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4540,f5428]) ).
fof(f5453,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q6,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5449]) ).
fof(f5469,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q20,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4753,f5445]) ).
fof(f5473,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q20,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5469]) ).
fof(f5477,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4520,f5453]) ).
fof(f5481,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q5,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5477]) ).
fof(f5485,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q19,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4738,f5473]) ).
fof(f5489,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q19,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5485]) ).
fof(f5493,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q4,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4510,f5481]) ).
fof(f5497,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q4,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5493]) ).
fof(f5501,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q18,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4688,f5489]) ).
fof(f5505,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q18,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5501]) ).
fof(f5509,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q3,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4330,f5497]) ).
fof(f5513,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q3,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5509]) ).
fof(f5517,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4673,f5505]) ).
fof(f5521,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q17,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5517]) ).
fof(f5525,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q10,X0) = select(q2,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4150,f5513]) ).
fof(f5529,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q2,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5525]) ).
fof(f5533,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q16,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4658,f5521]) ).
fof(f5537,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q16,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5533]) ).
fof(f5551,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q15,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4641,f5537]) ).
fof(f5555,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q15,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5551]) ).
fof(f5559,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q14,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4626,f5555]) ).
fof(f5563,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q14,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5559]) ).
fof(f5567,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q13,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4611,f5563]) ).
fof(f5571,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q13,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5567]) ).
fof(f5575,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q12,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4596,f5571]) ).
fof(f5579,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q12,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5575]) ).
fof(f5583,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4450,f5579]) ).
fof(f5587,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q11,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5583]) ).
fof(f5591,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q10,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4285,f5587]) ).
fof(f5595,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q10,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5591]) ).
fof(f5599,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q24,X0) = select(q2,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f5529,f5595]) ).
fof(f5603,plain,
! [X0] :
( seq = X0
| select(q24,X0) = select(q2,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f5599]) ).
fof(f5605,plain,
( seq = head
| select(q24,head) = index_9
| tail = head ),
inference(paramodulation,[status(thm)],[f5438,f5603]) ).
fof(f5611,plain,
( seq = head
| index_297 = index_9
| tail = head ),
inference(forward_demodulation,[status(thm)],[f5335,f5605]) ).
fof(f5612,plain,
( seq = head
| index_297 = index_9 ),
inference(forward_subsumption_resolution,[status(thm)],[f5611,f367]) ).
fof(f5665,plain,
elem_298 = select(earray_262,index_9),
inference(backward_demodulation,[status(thm)],[f5667,f4504]) ).
fof(f5667,plain,
index_297 = index_9,
inference(forward_subsumption_resolution,[status(thm)],[f5612,f368]) ).
fof(f5668,plain,
elem_298 = e48,
inference(forward_demodulation,[status(thm)],[f3704,f5665]) ).
fof(f5669,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5668,f4506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.57 % Computer : n016.cluster.edu
% 0.12/0.57 % Model : x86_64 x86_64
% 0.12/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.57 % Memory : 8046.5625MB
% 0.12/0.57 % OS : Linux 6.8.0-71-generic
% 0.12/0.57 % CPULimit : 300
% 0.12/0.57 % WCLimit : 300
% 0.12/0.57 % DateTime : Mon Sep 21 09:15:53 UTC 2026
% 0.12/0.58 % CPUTime :
% 0.12/0.59 % Drodi V4.1.1
% 0.15/1.13 % Refutation found
% 0.15/1.13 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/1.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.74/1.16 % Elapsed time: 0.573665 seconds
% 3.74/1.16 % CPU time: 4.310052 seconds
% 3.74/1.16 % Total memory used: 165.002 MB
% 3.74/1.16 % Net memory used: 162.392 MB
%------------------------------------------------------------------------------