%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:08 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.65s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 247
% Syntax : Number of formulae : 1007 (1007 unt; 0 def)
% Number of atoms : 1007 (1006 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 294 ( 294 usr; 286 con; 0-2 aty)
% Number of variables : 27 ( 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : p(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] : s(p(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : s(s(s(X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
elem_280 = select(earray_278,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
elem_283 = select(earray_278,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
index_0 = rselect_tail(q),
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 = rselect_tail(q24),
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 = rselect_tail(q25),
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 = rselect_tail(q26),
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 = rselect_tail(q27),
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 = rselect_tail(q28),
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 = rselect_tail(q2),
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 = rselect_tail(q29),
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 = rselect_tail(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_15 = rselect_tail(q10),
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 = rselect_tail(q31),
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 = rselect_tail(q32),
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 = rselect_tail(q33),
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 = rselect_tail(q34),
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 = rselect_tail(q35),
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 = rselect_tail(q36),
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 = rselect_tail(q37),
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 = rselect_tail(q38),
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 = rselect_tail(q3),
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 = rselect_tail(q39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_21 = rselect_tail(q11),
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 = rselect_tail(q40),
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 = rselect_tail(q41),
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 = rselect_tail(q42),
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 = rselect_tail(q43),
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 = rselect_tail(q44),
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 = rselect_tail(q45),
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 = rselect_tail(q4),
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 = rselect_tail(q5),
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 = rselect_tail(q6),
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 = rselect_tail(q7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_27 = rselect_tail(q12),
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 = rselect_tail(q8),
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 = rselect_head(q46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_281 = rselect_tail(q46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
s(index_282) = index_281,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_30 = s(index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_33 = rselect_tail(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_36 = s(index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_39 = rselect_tail(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_42 = s(index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_45 = rselect_tail(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_48 = s(index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_51 = rselect_tail(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_57 = rselect_tail(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_63 = rselect_tail(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_69 = rselect_tail(q1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_75 = rselect_tail(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_81 = rselect_tail(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
index_87 = rselect_tail(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
index_93 = rselect_tail(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
index_99 = rselect_tail(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
queue_101 = rstore_seq(q23,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
queue_107 = rstore_seq(q24,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_119 = rstore_seq(q26,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_131 = rstore_seq(q28,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_137 = rstore_seq(q2,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_149 = rstore_seq(q30,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_161 = rstore_seq(q32,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_173 = rstore_seq(q34,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_185 = rstore_seq(q36,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_197 = rstore_seq(q38,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_215 = rstore_seq(q40,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_227 = rstore_seq(q42,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_233 = rstore_seq(q43,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_239 = rstore_seq(q44,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_245 = rstore_seq(q45,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_251 = rstore_seq(q4,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_257 = rstore_seq(q5,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_263 = rstore_seq(q6,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_265 = rstore_tail(queue_263,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_269 = rstore_seq(q7,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_271 = rstore_tail(queue_269,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_275 = rstore_seq(q8,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_277 = rstore_tail(queue_275,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_29 = rstore_seq(q12,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_41 = rstore_seq(q14,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
queue_53 = rstore_seq(q16,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
queue_65 = rstore_seq(q18,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
queue_83 = rstore_seq(q20,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
queue_95 = rstore_seq(q22,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f327,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f328,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f329,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f330,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f331,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f332,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f333,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f334,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f335,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f336,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f337,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f338,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f339,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f340,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f342,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,hypothesis,
q5 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f344,hypothesis,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f345,hypothesis,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f346,hypothesis,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f347,hypothesis,
q9 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f348,negated_conjecture,
elem_280 != elem_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f353,plain,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f354,plain,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f357,plain,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f358,plain,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f360,plain,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f361,plain,
! [X0] : p(s(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f362,plain,
! [X0] : s(p(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f365,plain,
! [X0] : s(s(s(X0))) = X0,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f459,plain,
elem_280 = select(earray_278,index_279),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f460,plain,
elem_283 = select(earray_278,index_282),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f461,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f462,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f463,plain,
index_105 = rselect_tail(q24),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f464,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f465,plain,
index_111 = rselect_tail(q25),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f466,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f467,plain,
index_117 = rselect_tail(q26),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f468,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f469,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f470,plain,
index_123 = rselect_tail(q27),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f471,plain,
index_126 = s(index_123),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f472,plain,
index_129 = rselect_tail(q28),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f473,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f474,plain,
index_135 = rselect_tail(q2),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f475,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f476,plain,
index_141 = rselect_tail(q29),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f477,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f478,plain,
index_147 = rselect_tail(q30),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f479,plain,
index_15 = rselect_tail(q10),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f480,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f481,plain,
index_153 = rselect_tail(q31),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f482,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f483,plain,
index_159 = rselect_tail(q32),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f484,plain,
index_162 = s(index_159),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f485,plain,
index_165 = rselect_tail(q33),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f486,plain,
index_168 = s(index_165),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f487,plain,
index_171 = rselect_tail(q34),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f488,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f489,plain,
index_177 = rselect_tail(q35),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f490,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f491,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f492,plain,
index_183 = rselect_tail(q36),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f493,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f494,plain,
index_189 = rselect_tail(q37),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f495,plain,
index_192 = s(index_189),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f496,plain,
index_195 = rselect_tail(q38),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f497,plain,
index_198 = s(index_195),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f498,plain,
index_201 = rselect_tail(q3),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f499,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f500,plain,
index_207 = rselect_tail(q39),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f501,plain,
index_21 = rselect_tail(q11),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f502,plain,
index_210 = s(index_207),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f503,plain,
index_213 = rselect_tail(q40),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f504,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f505,plain,
index_219 = rselect_tail(q41),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f506,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f507,plain,
index_225 = rselect_tail(q42),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f508,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f509,plain,
index_231 = rselect_tail(q43),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f510,plain,
index_234 = s(index_231),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f511,plain,
index_237 = rselect_tail(q44),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f512,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f513,plain,
index_240 = s(index_237),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f514,plain,
index_243 = rselect_tail(q45),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f515,plain,
index_246 = s(index_243),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f516,plain,
index_249 = rselect_tail(q4),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f517,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f518,plain,
index_255 = rselect_tail(q5),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f519,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f520,plain,
index_261 = rselect_tail(q6),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f521,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f522,plain,
index_267 = rselect_tail(q7),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f523,plain,
index_27 = rselect_tail(q12),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f524,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f525,plain,
index_273 = rselect_tail(q8),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f526,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f527,plain,
index_279 = rselect_head(q46),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f528,plain,
index_281 = rselect_tail(q46),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f529,plain,
s(index_282) = index_281,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f530,plain,
index_3 = rselect_tail(q0),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f531,plain,
index_30 = s(index_27),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f532,plain,
index_33 = rselect_tail(q13),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f533,plain,
index_36 = s(index_33),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f534,plain,
index_39 = rselect_tail(q14),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f535,plain,
index_42 = s(index_39),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f536,plain,
index_45 = rselect_tail(q15),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f537,plain,
index_48 = s(index_45),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f538,plain,
index_51 = rselect_tail(q16),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f539,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f540,plain,
index_57 = rselect_tail(q17),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f541,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f542,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f543,plain,
index_63 = rselect_tail(q18),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f544,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f545,plain,
index_69 = rselect_tail(q1),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f546,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f547,plain,
index_75 = rselect_tail(q19),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f548,plain,
index_78 = s(index_75),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f549,plain,
index_81 = rselect_tail(q20),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f550,plain,
index_84 = s(index_81),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f551,plain,
index_87 = rselect_tail(q21),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f552,plain,
index_9 = rselect_tail(q9),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f553,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f554,plain,
index_93 = rselect_tail(q22),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f555,plain,
index_96 = s(index_93),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f556,plain,
index_99 = rselect_tail(q23),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f557,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f558,plain,
queue_101 = rstore_seq(q23,earray_100),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f559,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f560,plain,
queue_107 = rstore_seq(q24,earray_106),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f561,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f562,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f563,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f564,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f565,plain,
queue_119 = rstore_seq(q26,earray_118),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f566,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f567,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f568,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f569,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f570,plain,
queue_131 = rstore_seq(q28,earray_130),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f571,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f572,plain,
queue_137 = rstore_seq(q2,earray_136),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f573,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f574,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f575,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f576,plain,
queue_149 = rstore_seq(q30,earray_148),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f577,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f578,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f579,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f580,plain,
queue_161 = rstore_seq(q32,earray_160),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f581,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f582,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f583,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f584,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f585,plain,
queue_173 = rstore_seq(q34,earray_172),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f586,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f587,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f588,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f589,plain,
queue_185 = rstore_seq(q36,earray_184),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f590,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f591,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f592,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f593,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f594,plain,
queue_197 = rstore_seq(q38,earray_196),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f595,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f596,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f597,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f598,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f599,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f600,plain,
queue_215 = rstore_seq(q40,earray_214),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f601,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f602,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f603,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f604,plain,
queue_227 = rstore_seq(q42,earray_226),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f605,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f606,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f607,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f608,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f609,plain,
queue_239 = rstore_seq(q44,earray_238),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f610,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f611,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f612,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f613,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f614,plain,
queue_251 = rstore_seq(q4,earray_250),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f615,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f616,plain,
queue_257 = rstore_seq(q5,earray_256),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f617,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f618,plain,
queue_263 = rstore_seq(q6,earray_262),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f619,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f620,plain,
queue_269 = rstore_seq(q7,earray_268),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f621,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f622,plain,
queue_275 = rstore_seq(q8,earray_274),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f623,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f624,plain,
queue_29 = rstore_seq(q12,earray_28),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f625,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f626,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f627,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f628,plain,
queue_41 = rstore_seq(q14,earray_40),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f629,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f630,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f631,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f632,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f633,plain,
queue_53 = rstore_seq(q16,earray_52),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f634,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f635,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f636,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f637,plain,
queue_65 = rstore_seq(q18,earray_64),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f638,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f639,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f640,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f641,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f642,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f643,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f644,plain,
queue_83 = rstore_seq(q20,earray_82),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f645,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f646,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f647,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f648,plain,
queue_95 = rstore_seq(q22,earray_94),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f649,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f650,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f651,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f652,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f653,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f654,plain,
q12 = queue_25,
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f655,plain,
q13 = queue_31,
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f656,plain,
q14 = queue_37,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f657,plain,
q15 = queue_43,
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f658,plain,
q16 = queue_49,
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f659,plain,
q17 = queue_55,
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f660,plain,
q18 = queue_61,
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f661,plain,
q19 = queue_67,
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f662,plain,
q2 = queue_73,
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f663,plain,
q20 = queue_79,
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f664,plain,
q21 = queue_85,
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f665,plain,
q22 = queue_91,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f666,plain,
q23 = queue_97,
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f667,plain,
q24 = queue_103,
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f668,plain,
q25 = queue_109,
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f669,plain,
q26 = queue_115,
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f670,plain,
q27 = queue_121,
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f671,plain,
q28 = queue_127,
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f672,plain,
q29 = queue_133,
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f673,plain,
q3 = queue_139,
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f674,plain,
q30 = queue_145,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f675,plain,
q31 = queue_151,
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f676,plain,
q32 = queue_157,
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f677,plain,
q33 = queue_163,
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f678,plain,
q34 = queue_169,
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f679,plain,
q35 = queue_175,
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f680,plain,
q36 = queue_181,
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f681,plain,
q37 = queue_187,
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f682,plain,
q38 = queue_193,
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f683,plain,
q39 = queue_199,
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f684,plain,
q4 = queue_205,
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f685,plain,
q40 = queue_211,
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f686,plain,
q41 = queue_217,
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f687,plain,
q42 = queue_223,
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f688,plain,
q43 = queue_229,
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f689,plain,
q44 = queue_235,
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f690,plain,
q45 = queue_241,
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f691,plain,
q46 = queue_247,
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f692,plain,
q5 = queue_253,
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f693,plain,
q6 = queue_259,
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f694,plain,
q7 = queue_265,
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f695,plain,
q8 = queue_271,
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f696,plain,
q9 = queue_277,
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f697,plain,
elem_280 != elem_283,
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f698,plain,
queue_5 = rstore_seq(queue_1,earray_4),
inference(backward_demodulation,[status(thm)],[f650,f632]) ).
fof(f699,plain,
index_3 = rselect_tail(queue_1),
inference(backward_demodulation,[status(thm)],[f650,f530]) ).
fof(f701,plain,
queue_71 = rstore_seq(queue_7,earray_70),
inference(backward_demodulation,[status(thm)],[f651,f640]) ).
fof(f702,plain,
index_69 = rselect_tail(queue_7),
inference(backward_demodulation,[status(thm)],[f651,f545]) ).
fof(f704,plain,
queue_17 = rstore_seq(queue_13,earray_16),
inference(backward_demodulation,[status(thm)],[f652,f584]) ).
fof(f705,plain,
index_15 = rselect_tail(queue_13),
inference(backward_demodulation,[status(thm)],[f652,f479]) ).
fof(f707,plain,
queue_23 = rstore_seq(queue_19,earray_22),
inference(backward_demodulation,[status(thm)],[f653,f606]) ).
fof(f708,plain,
index_21 = rselect_tail(queue_19),
inference(backward_demodulation,[status(thm)],[f653,f501]) ).
fof(f710,plain,
queue_29 = rstore_seq(queue_25,earray_28),
inference(backward_demodulation,[status(thm)],[f654,f624]) ).
fof(f711,plain,
index_27 = rselect_tail(queue_25),
inference(backward_demodulation,[status(thm)],[f654,f523]) ).
fof(f713,plain,
queue_35 = rstore_seq(queue_31,earray_34),
inference(backward_demodulation,[status(thm)],[f655,f626]) ).
fof(f714,plain,
index_33 = rselect_tail(queue_31),
inference(backward_demodulation,[status(thm)],[f655,f532]) ).
fof(f716,plain,
queue_41 = rstore_seq(queue_37,earray_40),
inference(backward_demodulation,[status(thm)],[f656,f628]) ).
fof(f717,plain,
index_39 = rselect_tail(queue_37),
inference(backward_demodulation,[status(thm)],[f656,f534]) ).
fof(f719,plain,
queue_47 = rstore_seq(queue_43,earray_46),
inference(backward_demodulation,[status(thm)],[f657,f630]) ).
fof(f720,plain,
index_45 = rselect_tail(queue_43),
inference(backward_demodulation,[status(thm)],[f657,f536]) ).
fof(f722,plain,
queue_53 = rstore_seq(queue_49,earray_52),
inference(backward_demodulation,[status(thm)],[f658,f633]) ).
fof(f723,plain,
index_51 = rselect_tail(queue_49),
inference(backward_demodulation,[status(thm)],[f658,f538]) ).
fof(f725,plain,
queue_59 = rstore_seq(queue_55,earray_58),
inference(backward_demodulation,[status(thm)],[f659,f635]) ).
fof(f726,plain,
index_57 = rselect_tail(queue_55),
inference(backward_demodulation,[status(thm)],[f659,f540]) ).
fof(f728,plain,
queue_65 = rstore_seq(queue_61,earray_64),
inference(backward_demodulation,[status(thm)],[f660,f637]) ).
fof(f729,plain,
index_63 = rselect_tail(queue_61),
inference(backward_demodulation,[status(thm)],[f660,f543]) ).
fof(f731,plain,
queue_77 = rstore_seq(queue_67,earray_76),
inference(backward_demodulation,[status(thm)],[f661,f642]) ).
fof(f732,plain,
index_75 = rselect_tail(queue_67),
inference(backward_demodulation,[status(thm)],[f661,f547]) ).
fof(f734,plain,
queue_137 = rstore_seq(queue_73,earray_136),
inference(backward_demodulation,[status(thm)],[f662,f572]) ).
fof(f735,plain,
index_135 = rselect_tail(queue_73),
inference(backward_demodulation,[status(thm)],[f662,f474]) ).
fof(f737,plain,
queue_83 = rstore_seq(queue_79,earray_82),
inference(backward_demodulation,[status(thm)],[f663,f644]) ).
fof(f738,plain,
index_81 = rselect_tail(queue_79),
inference(backward_demodulation,[status(thm)],[f663,f549]) ).
fof(f740,plain,
queue_89 = rstore_seq(queue_85,earray_88),
inference(backward_demodulation,[status(thm)],[f664,f646]) ).
fof(f741,plain,
index_87 = rselect_tail(queue_85),
inference(backward_demodulation,[status(thm)],[f664,f551]) ).
fof(f743,plain,
queue_95 = rstore_seq(queue_91,earray_94),
inference(backward_demodulation,[status(thm)],[f665,f648]) ).
fof(f744,plain,
index_93 = rselect_tail(queue_91),
inference(backward_demodulation,[status(thm)],[f665,f554]) ).
fof(f746,plain,
queue_101 = rstore_seq(queue_97,earray_100),
inference(backward_demodulation,[status(thm)],[f666,f558]) ).
fof(f747,plain,
index_99 = rselect_tail(queue_97),
inference(backward_demodulation,[status(thm)],[f666,f556]) ).
fof(f749,plain,
queue_107 = rstore_seq(queue_103,earray_106),
inference(backward_demodulation,[status(thm)],[f667,f560]) ).
fof(f750,plain,
index_105 = rselect_tail(queue_103),
inference(backward_demodulation,[status(thm)],[f667,f463]) ).
fof(f752,plain,
queue_113 = rstore_seq(queue_109,earray_112),
inference(backward_demodulation,[status(thm)],[f668,f563]) ).
fof(f753,plain,
index_111 = rselect_tail(queue_109),
inference(backward_demodulation,[status(thm)],[f668,f465]) ).
fof(f755,plain,
queue_119 = rstore_seq(queue_115,earray_118),
inference(backward_demodulation,[status(thm)],[f669,f565]) ).
fof(f756,plain,
index_117 = rselect_tail(queue_115),
inference(backward_demodulation,[status(thm)],[f669,f467]) ).
fof(f758,plain,
queue_125 = rstore_seq(queue_121,earray_124),
inference(backward_demodulation,[status(thm)],[f670,f567]) ).
fof(f759,plain,
index_123 = rselect_tail(queue_121),
inference(backward_demodulation,[status(thm)],[f670,f470]) ).
fof(f761,plain,
queue_131 = rstore_seq(queue_127,earray_130),
inference(backward_demodulation,[status(thm)],[f671,f570]) ).
fof(f762,plain,
index_129 = rselect_tail(queue_127),
inference(backward_demodulation,[status(thm)],[f671,f472]) ).
fof(f764,plain,
queue_143 = rstore_seq(queue_133,earray_142),
inference(backward_demodulation,[status(thm)],[f672,f574]) ).
fof(f765,plain,
index_141 = rselect_tail(queue_133),
inference(backward_demodulation,[status(thm)],[f672,f476]) ).
fof(f767,plain,
queue_203 = rstore_seq(queue_139,earray_202),
inference(backward_demodulation,[status(thm)],[f673,f596]) ).
fof(f768,plain,
index_201 = rselect_tail(queue_139),
inference(backward_demodulation,[status(thm)],[f673,f498]) ).
fof(f770,plain,
queue_149 = rstore_seq(queue_145,earray_148),
inference(backward_demodulation,[status(thm)],[f674,f576]) ).
fof(f771,plain,
index_147 = rselect_tail(queue_145),
inference(backward_demodulation,[status(thm)],[f674,f478]) ).
fof(f773,plain,
queue_155 = rstore_seq(queue_151,earray_154),
inference(backward_demodulation,[status(thm)],[f675,f578]) ).
fof(f774,plain,
index_153 = rselect_tail(queue_151),
inference(backward_demodulation,[status(thm)],[f675,f481]) ).
fof(f776,plain,
queue_161 = rstore_seq(queue_157,earray_160),
inference(backward_demodulation,[status(thm)],[f676,f580]) ).
fof(f777,plain,
index_159 = rselect_tail(queue_157),
inference(backward_demodulation,[status(thm)],[f676,f483]) ).
fof(f779,plain,
queue_167 = rstore_seq(queue_163,earray_166),
inference(backward_demodulation,[status(thm)],[f677,f582]) ).
fof(f780,plain,
index_165 = rselect_tail(queue_163),
inference(backward_demodulation,[status(thm)],[f677,f485]) ).
fof(f782,plain,
queue_173 = rstore_seq(queue_169,earray_172),
inference(backward_demodulation,[status(thm)],[f678,f585]) ).
fof(f783,plain,
index_171 = rselect_tail(queue_169),
inference(backward_demodulation,[status(thm)],[f678,f487]) ).
fof(f785,plain,
queue_179 = rstore_seq(queue_175,earray_178),
inference(backward_demodulation,[status(thm)],[f679,f587]) ).
fof(f786,plain,
index_177 = rselect_tail(queue_175),
inference(backward_demodulation,[status(thm)],[f679,f489]) ).
fof(f788,plain,
queue_185 = rstore_seq(queue_181,earray_184),
inference(backward_demodulation,[status(thm)],[f680,f589]) ).
fof(f789,plain,
index_183 = rselect_tail(queue_181),
inference(backward_demodulation,[status(thm)],[f680,f492]) ).
fof(f791,plain,
queue_191 = rstore_seq(queue_187,earray_190),
inference(backward_demodulation,[status(thm)],[f681,f592]) ).
fof(f792,plain,
index_189 = rselect_tail(queue_187),
inference(backward_demodulation,[status(thm)],[f681,f494]) ).
fof(f794,plain,
queue_197 = rstore_seq(queue_193,earray_196),
inference(backward_demodulation,[status(thm)],[f682,f594]) ).
fof(f795,plain,
index_195 = rselect_tail(queue_193),
inference(backward_demodulation,[status(thm)],[f682,f496]) ).
fof(f797,plain,
queue_209 = rstore_seq(queue_199,earray_208),
inference(backward_demodulation,[status(thm)],[f683,f598]) ).
fof(f798,plain,
index_207 = rselect_tail(queue_199),
inference(backward_demodulation,[status(thm)],[f683,f500]) ).
fof(f800,plain,
queue_251 = rstore_seq(queue_205,earray_250),
inference(backward_demodulation,[status(thm)],[f684,f614]) ).
fof(f801,plain,
index_249 = rselect_tail(queue_205),
inference(backward_demodulation,[status(thm)],[f684,f516]) ).
fof(f803,plain,
queue_215 = rstore_seq(queue_211,earray_214),
inference(backward_demodulation,[status(thm)],[f685,f600]) ).
fof(f804,plain,
index_213 = rselect_tail(queue_211),
inference(backward_demodulation,[status(thm)],[f685,f503]) ).
fof(f806,plain,
queue_221 = rstore_seq(queue_217,earray_220),
inference(backward_demodulation,[status(thm)],[f686,f602]) ).
fof(f807,plain,
index_219 = rselect_tail(queue_217),
inference(backward_demodulation,[status(thm)],[f686,f505]) ).
fof(f809,plain,
queue_227 = rstore_seq(queue_223,earray_226),
inference(backward_demodulation,[status(thm)],[f687,f604]) ).
fof(f810,plain,
index_225 = rselect_tail(queue_223),
inference(backward_demodulation,[status(thm)],[f687,f507]) ).
fof(f812,plain,
queue_233 = rstore_seq(queue_229,earray_232),
inference(backward_demodulation,[status(thm)],[f688,f607]) ).
fof(f813,plain,
index_231 = rselect_tail(queue_229),
inference(backward_demodulation,[status(thm)],[f688,f509]) ).
fof(f815,plain,
queue_239 = rstore_seq(queue_235,earray_238),
inference(backward_demodulation,[status(thm)],[f689,f609]) ).
fof(f816,plain,
index_237 = rselect_tail(queue_235),
inference(backward_demodulation,[status(thm)],[f689,f511]) ).
fof(f818,plain,
queue_245 = rstore_seq(queue_241,earray_244),
inference(backward_demodulation,[status(thm)],[f690,f611]) ).
fof(f819,plain,
index_243 = rselect_tail(queue_241),
inference(backward_demodulation,[status(thm)],[f690,f514]) ).
fof(f821,plain,
index_281 = rselect_tail(queue_247),
inference(backward_demodulation,[status(thm)],[f691,f528]) ).
fof(f822,plain,
index_279 = rselect_head(queue_247),
inference(backward_demodulation,[status(thm)],[f691,f527]) ).
fof(f824,plain,
queue_257 = rstore_seq(queue_253,earray_256),
inference(backward_demodulation,[status(thm)],[f692,f616]) ).
fof(f825,plain,
index_255 = rselect_tail(queue_253),
inference(backward_demodulation,[status(thm)],[f692,f518]) ).
fof(f827,plain,
queue_263 = rstore_seq(queue_259,earray_262),
inference(backward_demodulation,[status(thm)],[f693,f618]) ).
fof(f828,plain,
index_261 = rselect_tail(queue_259),
inference(backward_demodulation,[status(thm)],[f693,f520]) ).
fof(f830,plain,
queue_269 = rstore_seq(queue_265,earray_268),
inference(backward_demodulation,[status(thm)],[f694,f620]) ).
fof(f831,plain,
index_267 = rselect_tail(queue_265),
inference(backward_demodulation,[status(thm)],[f694,f522]) ).
fof(f833,plain,
queue_275 = rstore_seq(queue_271,earray_274),
inference(backward_demodulation,[status(thm)],[f695,f622]) ).
fof(f834,plain,
index_273 = rselect_tail(queue_271),
inference(backward_demodulation,[status(thm)],[f695,f525]) ).
fof(f836,plain,
queue_11 = rstore_seq(queue_277,earray_10),
inference(backward_demodulation,[status(thm)],[f696,f562]) ).
fof(f837,plain,
index_9 = rselect_tail(queue_277),
inference(backward_demodulation,[status(thm)],[f696,f552]) ).
fof(f856,plain,
p(index_12) = index_9,
inference(paramodulation,[status(thm)],[f468,f361]) ).
fof(f862,plain,
p(index_126) = index_123,
inference(paramodulation,[status(thm)],[f471,f361]) ).
fof(f880,plain,
! [X0] : s(s(X0)) = p(X0),
inference(paramodulation,[status(thm)],[f362,f365]) ).
fof(f899,plain,
p(index_150) = index_147,
inference(paramodulation,[status(thm)],[f480,f361]) ).
fof(f907,plain,
p(index_168) = index_165,
inference(paramodulation,[status(thm)],[f486,f361]) ).
fof(f915,plain,
p(index_186) = index_183,
inference(paramodulation,[status(thm)],[f493,f361]) ).
fof(f925,plain,
p(index_204) = index_201,
inference(paramodulation,[status(thm)],[f499,f361]) ).
fof(f927,plain,
p(index_210) = index_207,
inference(paramodulation,[status(thm)],[f502,f361]) ).
fof(f933,plain,
p(index_228) = index_225,
inference(paramodulation,[status(thm)],[f508,f361]) ).
fof(f947,plain,
p(index_246) = index_243,
inference(paramodulation,[status(thm)],[f515,f361]) ).
fof(f955,plain,
p(index_264) = index_261,
inference(paramodulation,[status(thm)],[f521,f361]) ).
fof(f961,plain,
p(index_281) = index_282,
inference(paramodulation,[status(thm)],[f529,f361]) ).
fof(f963,plain,
p(index_30) = index_27,
inference(paramodulation,[status(thm)],[f531,f361]) ).
fof(f973,plain,
p(index_48) = index_45,
inference(paramodulation,[status(thm)],[f537,f361]) ).
fof(f977,plain,
p(index_6) = index_3,
inference(paramodulation,[status(thm)],[f541,f361]) ).
fof(f981,plain,
p(index_66) = index_63,
inference(paramodulation,[status(thm)],[f544,f361]) ).
fof(f983,plain,
p(index_72) = index_69,
inference(paramodulation,[status(thm)],[f546,f361]) ).
fof(f995,plain,
p(index_90) = index_87,
inference(paramodulation,[status(thm)],[f553,f361]) ).
fof(f997,plain,
p(index_96) = index_93,
inference(paramodulation,[status(thm)],[f555,f361]) ).
fof(f1255,plain,
rselect_tail(queue_1) = rselect_tail(q),
inference(paramodulation,[status(thm)],[f557,f360]) ).
fof(f1257,plain,
rselect_head(queue_1) = index_0,
inference(paramodulation,[status(thm)],[f557,f353]) ).
fof(f1258,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[status(thm)],[f699,f1255]) ).
fof(f1260,plain,
p(index_6) = index_0,
inference(backward_demodulation,[status(thm)],[f1267,f977]) ).
fof(f1267,plain,
index_3 = index_0,
inference(forward_demodulation,[status(thm)],[f461,f1258]) ).
fof(f1275,plain,
rselect_head(queue_103) = rselect_head(queue_101),
inference(paramodulation,[status(thm)],[f559,f357]) ).
fof(f1277,plain,
rselect_tail(queue_103) = index_102,
inference(paramodulation,[status(thm)],[f559,f354]) ).
fof(f1279,plain,
index_105 = index_102,
inference(backward_demodulation,[status(thm)],[f1277,f750]) ).
fof(f1285,plain,
index_108 = s(index_102),
inference(backward_demodulation,[status(thm)],[f1279,f464]) ).
fof(f1292,plain,
rselect_head(queue_109) = rselect_head(queue_107),
inference(paramodulation,[status(thm)],[f561,f357]) ).
fof(f1294,plain,
rselect_tail(queue_109) = index_108,
inference(paramodulation,[status(thm)],[f561,f354]) ).
fof(f1296,plain,
index_111 = index_108,
inference(backward_demodulation,[status(thm)],[f1294,f753]) ).
fof(f1302,plain,
index_114 = s(index_108),
inference(backward_demodulation,[status(thm)],[f1296,f466]) ).
fof(f1307,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(paramodulation,[status(thm)],[f564,f357]) ).
fof(f1309,plain,
rselect_tail(queue_115) = index_114,
inference(paramodulation,[status(thm)],[f564,f354]) ).
fof(f1311,plain,
index_117 = index_114,
inference(backward_demodulation,[status(thm)],[f1309,f756]) ).
fof(f1317,plain,
index_120 = s(index_114),
inference(backward_demodulation,[status(thm)],[f1311,f469]) ).
fof(f1322,plain,
rselect_head(queue_121) = rselect_head(queue_119),
inference(paramodulation,[status(thm)],[f566,f357]) ).
fof(f1324,plain,
rselect_tail(queue_121) = index_120,
inference(paramodulation,[status(thm)],[f566,f354]) ).
fof(f1326,plain,
index_123 = index_120,
inference(backward_demodulation,[status(thm)],[f1324,f759]) ).
fof(f1328,plain,
p(index_126) = index_120,
inference(backward_demodulation,[status(thm)],[f1326,f862]) ).
fof(f1349,plain,
rselect_head(queue_127) = rselect_head(queue_125),
inference(paramodulation,[status(thm)],[f568,f357]) ).
fof(f1351,plain,
rselect_tail(queue_127) = index_126,
inference(paramodulation,[status(thm)],[f568,f354]) ).
fof(f1353,plain,
index_129 = index_126,
inference(backward_demodulation,[status(thm)],[f1351,f762]) ).
fof(f1359,plain,
index_132 = s(index_126),
inference(backward_demodulation,[status(thm)],[f1353,f473]) ).
fof(f1364,plain,
rselect_head(queue_13) = rselect_head(queue_11),
inference(paramodulation,[status(thm)],[f569,f357]) ).
fof(f1366,plain,
rselect_tail(queue_13) = index_12,
inference(paramodulation,[status(thm)],[f569,f354]) ).
fof(f1368,plain,
index_15 = index_12,
inference(backward_demodulation,[status(thm)],[f1366,f705]) ).
fof(f1373,plain,
index_18 = s(index_12),
inference(backward_demodulation,[status(thm)],[f1368,f490]) ).
fof(f1402,plain,
rselect_head(queue_133) = rselect_head(queue_131),
inference(paramodulation,[status(thm)],[f571,f357]) ).
fof(f1404,plain,
rselect_tail(queue_133) = index_132,
inference(paramodulation,[status(thm)],[f571,f354]) ).
fof(f1406,plain,
index_141 = index_132,
inference(backward_demodulation,[status(thm)],[f1404,f765]) ).
fof(f1411,plain,
index_144 = s(index_132),
inference(backward_demodulation,[status(thm)],[f1406,f477]) ).
fof(f1416,plain,
rselect_head(queue_139) = rselect_head(queue_137),
inference(paramodulation,[status(thm)],[f573,f357]) ).
fof(f1418,plain,
rselect_tail(queue_139) = index_138,
inference(paramodulation,[status(thm)],[f573,f354]) ).
fof(f1420,plain,
index_201 = index_138,
inference(backward_demodulation,[status(thm)],[f1418,f768]) ).
fof(f1422,plain,
p(index_204) = index_138,
inference(backward_demodulation,[status(thm)],[f1420,f925]) ).
fof(f1425,plain,
index_204 = s(index_138),
inference(backward_demodulation,[status(thm)],[f1420,f499]) ).
fof(f1430,plain,
rselect_head(queue_145) = rselect_head(queue_143),
inference(paramodulation,[status(thm)],[f575,f357]) ).
fof(f1432,plain,
rselect_tail(queue_145) = index_144,
inference(paramodulation,[status(thm)],[f575,f354]) ).
fof(f1434,plain,
index_147 = index_144,
inference(backward_demodulation,[status(thm)],[f1432,f771]) ).
fof(f1436,plain,
p(index_150) = index_144,
inference(backward_demodulation,[status(thm)],[f1434,f899]) ).
fof(f1443,plain,
rselect_head(queue_151) = rselect_head(queue_149),
inference(paramodulation,[status(thm)],[f577,f357]) ).
fof(f1445,plain,
rselect_tail(queue_151) = index_150,
inference(paramodulation,[status(thm)],[f577,f354]) ).
fof(f1447,plain,
index_153 = index_150,
inference(backward_demodulation,[status(thm)],[f1445,f774]) ).
fof(f1452,plain,
index_156 = s(index_150),
inference(backward_demodulation,[status(thm)],[f1447,f482]) ).
fof(f1468,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(paramodulation,[status(thm)],[f579,f357]) ).
fof(f1470,plain,
rselect_tail(queue_157) = index_156,
inference(paramodulation,[status(thm)],[f579,f354]) ).
fof(f1472,plain,
index_159 = index_156,
inference(backward_demodulation,[status(thm)],[f1470,f777]) ).
fof(f1477,plain,
index_162 = s(index_156),
inference(backward_demodulation,[status(thm)],[f1472,f484]) ).
fof(f1481,plain,
rselect_head(queue_163) = rselect_head(queue_161),
inference(paramodulation,[status(thm)],[f581,f357]) ).
fof(f1483,plain,
rselect_tail(queue_163) = index_162,
inference(paramodulation,[status(thm)],[f581,f354]) ).
fof(f1485,plain,
index_165 = index_162,
inference(backward_demodulation,[status(thm)],[f1483,f780]) ).
fof(f1487,plain,
p(index_168) = index_162,
inference(backward_demodulation,[status(thm)],[f1485,f907]) ).
fof(f1518,plain,
rselect_head(queue_169) = rselect_head(queue_167),
inference(paramodulation,[status(thm)],[f583,f357]) ).
fof(f1520,plain,
rselect_tail(queue_169) = index_168,
inference(paramodulation,[status(thm)],[f583,f354]) ).
fof(f1522,plain,
index_171 = index_168,
inference(backward_demodulation,[status(thm)],[f1520,f783]) ).
fof(f1527,plain,
index_174 = s(index_168),
inference(backward_demodulation,[status(thm)],[f1522,f488]) ).
fof(f1531,plain,
rselect_head(queue_175) = rselect_head(queue_173),
inference(paramodulation,[status(thm)],[f586,f357]) ).
fof(f1533,plain,
rselect_tail(queue_175) = index_174,
inference(paramodulation,[status(thm)],[f586,f354]) ).
fof(f1535,plain,
index_177 = index_174,
inference(backward_demodulation,[status(thm)],[f1533,f786]) ).
fof(f1540,plain,
index_180 = s(index_174),
inference(backward_demodulation,[status(thm)],[f1535,f491]) ).
fof(f1544,plain,
rselect_head(queue_181) = rselect_head(queue_179),
inference(paramodulation,[status(thm)],[f588,f357]) ).
fof(f1546,plain,
rselect_tail(queue_181) = index_180,
inference(paramodulation,[status(thm)],[f588,f354]) ).
fof(f1548,plain,
index_183 = index_180,
inference(backward_demodulation,[status(thm)],[f1546,f789]) ).
fof(f1550,plain,
p(index_186) = index_180,
inference(backward_demodulation,[status(thm)],[f1548,f915]) ).
fof(f1557,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(paramodulation,[status(thm)],[f590,f357]) ).
fof(f1559,plain,
rselect_tail(queue_187) = index_186,
inference(paramodulation,[status(thm)],[f590,f354]) ).
fof(f1561,plain,
index_189 = index_186,
inference(backward_demodulation,[status(thm)],[f1559,f792]) ).
fof(f1566,plain,
index_192 = s(index_186),
inference(backward_demodulation,[status(thm)],[f1561,f495]) ).
fof(f1582,plain,
rselect_head(queue_19) = rselect_head(queue_17),
inference(paramodulation,[status(thm)],[f591,f357]) ).
fof(f1584,plain,
rselect_tail(queue_19) = index_18,
inference(paramodulation,[status(thm)],[f591,f354]) ).
fof(f1586,plain,
index_21 = index_18,
inference(backward_demodulation,[status(thm)],[f1584,f708]) ).
fof(f1591,plain,
index_24 = s(index_18),
inference(backward_demodulation,[status(thm)],[f1586,f512]) ).
fof(f1595,plain,
rselect_head(queue_193) = rselect_head(queue_191),
inference(paramodulation,[status(thm)],[f593,f357]) ).
fof(f1597,plain,
rselect_tail(queue_193) = index_192,
inference(paramodulation,[status(thm)],[f593,f354]) ).
fof(f1599,plain,
index_195 = index_192,
inference(backward_demodulation,[status(thm)],[f1597,f795]) ).
fof(f1604,plain,
index_198 = s(index_192),
inference(backward_demodulation,[status(thm)],[f1599,f497]) ).
fof(f1632,plain,
rselect_head(queue_199) = rselect_head(queue_197),
inference(paramodulation,[status(thm)],[f595,f357]) ).
fof(f1634,plain,
rselect_tail(queue_199) = index_198,
inference(paramodulation,[status(thm)],[f595,f354]) ).
fof(f1636,plain,
index_207 = index_198,
inference(backward_demodulation,[status(thm)],[f1634,f798]) ).
fof(f1638,plain,
p(index_210) = index_198,
inference(backward_demodulation,[status(thm)],[f1636,f927]) ).
fof(f1645,plain,
rselect_head(queue_205) = rselect_head(queue_203),
inference(paramodulation,[status(thm)],[f597,f357]) ).
fof(f1647,plain,
rselect_tail(queue_205) = index_204,
inference(paramodulation,[status(thm)],[f597,f354]) ).
fof(f1649,plain,
index_249 = index_204,
inference(backward_demodulation,[status(thm)],[f1647,f801]) ).
fof(f1654,plain,
index_252 = s(index_204),
inference(backward_demodulation,[status(thm)],[f1649,f517]) ).
fof(f1658,plain,
rselect_head(queue_211) = rselect_head(queue_209),
inference(paramodulation,[status(thm)],[f599,f357]) ).
fof(f1660,plain,
rselect_tail(queue_211) = index_210,
inference(paramodulation,[status(thm)],[f599,f354]) ).
fof(f1662,plain,
index_213 = index_210,
inference(backward_demodulation,[status(thm)],[f1660,f804]) ).
fof(f1667,plain,
index_216 = s(index_210),
inference(backward_demodulation,[status(thm)],[f1662,f504]) ).
fof(f1671,plain,
rselect_head(queue_217) = rselect_head(queue_215),
inference(paramodulation,[status(thm)],[f601,f357]) ).
fof(f1673,plain,
rselect_tail(queue_217) = index_216,
inference(paramodulation,[status(thm)],[f601,f354]) ).
fof(f1675,plain,
index_219 = index_216,
inference(backward_demodulation,[status(thm)],[f1673,f807]) ).
fof(f1680,plain,
index_222 = s(index_216),
inference(backward_demodulation,[status(thm)],[f1675,f506]) ).
fof(f1696,plain,
rselect_head(queue_223) = rselect_head(queue_221),
inference(paramodulation,[status(thm)],[f603,f357]) ).
fof(f1698,plain,
rselect_tail(queue_223) = index_222,
inference(paramodulation,[status(thm)],[f603,f354]) ).
fof(f1700,plain,
index_225 = index_222,
inference(backward_demodulation,[status(thm)],[f1698,f810]) ).
fof(f1702,plain,
p(index_228) = index_222,
inference(backward_demodulation,[status(thm)],[f1700,f933]) ).
fof(f1709,plain,
rselect_head(queue_229) = rselect_head(queue_227),
inference(paramodulation,[status(thm)],[f605,f357]) ).
fof(f1711,plain,
rselect_tail(queue_229) = index_228,
inference(paramodulation,[status(thm)],[f605,f354]) ).
fof(f1713,plain,
index_231 = index_228,
inference(backward_demodulation,[status(thm)],[f1711,f813]) ).
fof(f1718,plain,
index_234 = s(index_228),
inference(backward_demodulation,[status(thm)],[f1713,f510]) ).
fof(f1746,plain,
rselect_head(queue_235) = rselect_head(queue_233),
inference(paramodulation,[status(thm)],[f608,f357]) ).
fof(f1748,plain,
rselect_tail(queue_235) = index_234,
inference(paramodulation,[status(thm)],[f608,f354]) ).
fof(f1750,plain,
index_237 = index_234,
inference(backward_demodulation,[status(thm)],[f1748,f816]) ).
fof(f1755,plain,
index_240 = s(index_234),
inference(backward_demodulation,[status(thm)],[f1750,f513]) ).
fof(f1759,plain,
rselect_head(queue_241) = rselect_head(queue_239),
inference(paramodulation,[status(thm)],[f610,f357]) ).
fof(f1761,plain,
rselect_tail(queue_241) = index_240,
inference(paramodulation,[status(thm)],[f610,f354]) ).
fof(f1763,plain,
index_243 = index_240,
inference(backward_demodulation,[status(thm)],[f1761,f819]) ).
fof(f1765,plain,
p(index_246) = index_240,
inference(backward_demodulation,[status(thm)],[f1763,f947]) ).
fof(f1772,plain,
rselect_head(queue_247) = rselect_head(queue_245),
inference(paramodulation,[status(thm)],[f612,f357]) ).
fof(f1774,plain,
rselect_tail(queue_247) = index_246,
inference(paramodulation,[status(thm)],[f612,f354]) ).
fof(f1775,plain,
index_279 = rselect_head(queue_245),
inference(forward_demodulation,[status(thm)],[f822,f1772]) ).
fof(f1780,plain,
p(index_281) = index_240,
inference(backward_demodulation,[status(thm)],[f1782,f1765]) ).
fof(f1782,plain,
index_281 = index_246,
inference(forward_demodulation,[status(thm)],[f821,f1774]) ).
fof(f1783,plain,
index_240 = index_282,
inference(backward_demodulation,[status(thm)],[f1780,f961]) ).
fof(f1787,plain,
elem_283 = select(earray_278,index_240),
inference(backward_demodulation,[status(thm)],[f1783,f460]) ).
fof(f1789,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(paramodulation,[status(thm)],[f613,f357]) ).
fof(f1791,plain,
rselect_tail(queue_25) = index_24,
inference(paramodulation,[status(thm)],[f613,f354]) ).
fof(f1793,plain,
index_27 = index_24,
inference(backward_demodulation,[status(thm)],[f1791,f711]) ).
fof(f1795,plain,
p(index_30) = index_24,
inference(backward_demodulation,[status(thm)],[f1793,f963]) ).
fof(f1814,plain,
rselect_head(queue_253) = rselect_head(queue_251),
inference(paramodulation,[status(thm)],[f615,f357]) ).
fof(f1816,plain,
rselect_tail(queue_253) = index_252,
inference(paramodulation,[status(thm)],[f615,f354]) ).
fof(f1818,plain,
index_255 = index_252,
inference(backward_demodulation,[status(thm)],[f1816,f825]) ).
fof(f1823,plain,
index_258 = s(index_252),
inference(backward_demodulation,[status(thm)],[f1818,f519]) ).
fof(f1827,plain,
rselect_head(queue_259) = rselect_head(queue_257),
inference(paramodulation,[status(thm)],[f617,f357]) ).
fof(f1829,plain,
rselect_tail(queue_259) = index_258,
inference(paramodulation,[status(thm)],[f617,f354]) ).
fof(f1831,plain,
index_261 = index_258,
inference(backward_demodulation,[status(thm)],[f1829,f828]) ).
fof(f1833,plain,
p(index_264) = index_258,
inference(backward_demodulation,[status(thm)],[f1831,f955]) ).
fof(f1864,plain,
rselect_head(queue_265) = rselect_head(queue_263),
inference(paramodulation,[status(thm)],[f619,f357]) ).
fof(f1866,plain,
rselect_tail(queue_265) = index_264,
inference(paramodulation,[status(thm)],[f619,f354]) ).
fof(f1868,plain,
index_267 = index_264,
inference(backward_demodulation,[status(thm)],[f1866,f831]) ).
fof(f1873,plain,
index_270 = s(index_264),
inference(backward_demodulation,[status(thm)],[f1868,f524]) ).
fof(f1877,plain,
rselect_head(queue_271) = rselect_head(queue_269),
inference(paramodulation,[status(thm)],[f621,f357]) ).
fof(f1879,plain,
rselect_tail(queue_271) = index_270,
inference(paramodulation,[status(thm)],[f621,f354]) ).
fof(f1881,plain,
index_273 = index_270,
inference(backward_demodulation,[status(thm)],[f1879,f834]) ).
fof(f1886,plain,
index_276 = s(index_270),
inference(backward_demodulation,[status(thm)],[f1881,f526]) ).
fof(f1890,plain,
rselect_head(queue_277) = rselect_head(queue_275),
inference(paramodulation,[status(thm)],[f623,f357]) ).
fof(f1892,plain,
rselect_tail(queue_277) = index_276,
inference(paramodulation,[status(thm)],[f623,f354]) ).
fof(f1894,plain,
index_9 = index_276,
inference(backward_demodulation,[status(thm)],[f1892,f837]) ).
fof(f1897,plain,
p(index_12) = index_276,
inference(backward_demodulation,[status(thm)],[f1894,f856]) ).
fof(f1904,plain,
rselect_head(queue_31) = rselect_head(queue_29),
inference(paramodulation,[status(thm)],[f625,f357]) ).
fof(f1906,plain,
rselect_tail(queue_31) = index_30,
inference(paramodulation,[status(thm)],[f625,f354]) ).
fof(f1908,plain,
index_33 = index_30,
inference(backward_demodulation,[status(thm)],[f1906,f714]) ).
fof(f1913,plain,
index_36 = s(index_30),
inference(backward_demodulation,[status(thm)],[f1908,f533]) ).
fof(f1929,plain,
rselect_head(queue_37) = rselect_head(queue_35),
inference(paramodulation,[status(thm)],[f627,f357]) ).
fof(f1931,plain,
rselect_tail(queue_37) = index_36,
inference(paramodulation,[status(thm)],[f627,f354]) ).
fof(f1933,plain,
index_39 = index_36,
inference(backward_demodulation,[status(thm)],[f1931,f717]) ).
fof(f1938,plain,
index_42 = s(index_36),
inference(backward_demodulation,[status(thm)],[f1933,f535]) ).
fof(f1942,plain,
rselect_head(queue_43) = rselect_head(queue_41),
inference(paramodulation,[status(thm)],[f629,f357]) ).
fof(f1944,plain,
rselect_tail(queue_43) = index_42,
inference(paramodulation,[status(thm)],[f629,f354]) ).
fof(f1946,plain,
index_45 = index_42,
inference(backward_demodulation,[status(thm)],[f1944,f720]) ).
fof(f1949,plain,
p(index_48) = index_42,
inference(backward_demodulation,[status(thm)],[f1946,f973]) ).
fof(f1971,plain,
rselect_head(queue_49) = rselect_head(queue_47),
inference(paramodulation,[status(thm)],[f631,f357]) ).
fof(f1973,plain,
rselect_tail(queue_49) = index_48,
inference(paramodulation,[status(thm)],[f631,f354]) ).
fof(f1975,plain,
index_51 = index_48,
inference(backward_demodulation,[status(thm)],[f1973,f723]) ).
fof(f1980,plain,
index_54 = s(index_48),
inference(backward_demodulation,[status(thm)],[f1975,f539]) ).
fof(f1984,plain,
rselect_head(queue_55) = rselect_head(queue_53),
inference(paramodulation,[status(thm)],[f634,f357]) ).
fof(f1986,plain,
rselect_tail(queue_55) = index_54,
inference(paramodulation,[status(thm)],[f634,f354]) ).
fof(f1988,plain,
index_57 = index_54,
inference(backward_demodulation,[status(thm)],[f1986,f726]) ).
fof(f1993,plain,
index_60 = s(index_54),
inference(backward_demodulation,[status(thm)],[f1988,f542]) ).
fof(f1997,plain,
rselect_head(queue_61) = rselect_head(queue_59),
inference(paramodulation,[status(thm)],[f636,f357]) ).
fof(f1999,plain,
rselect_tail(queue_61) = index_60,
inference(paramodulation,[status(thm)],[f636,f354]) ).
fof(f2001,plain,
index_63 = index_60,
inference(backward_demodulation,[status(thm)],[f1999,f729]) ).
fof(f2004,plain,
p(index_66) = index_60,
inference(backward_demodulation,[status(thm)],[f2001,f981]) ).
fof(f2010,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(paramodulation,[status(thm)],[f638,f357]) ).
fof(f2012,plain,
rselect_tail(queue_67) = index_66,
inference(paramodulation,[status(thm)],[f638,f354]) ).
fof(f2014,plain,
index_75 = index_66,
inference(backward_demodulation,[status(thm)],[f2012,f732]) ).
fof(f2019,plain,
index_78 = s(index_66),
inference(backward_demodulation,[status(thm)],[f2014,f548]) ).
fof(f2039,plain,
rselect_head(queue_7) = rselect_head(queue_5),
inference(paramodulation,[status(thm)],[f639,f357]) ).
fof(f2041,plain,
rselect_tail(queue_7) = index_6,
inference(paramodulation,[status(thm)],[f639,f354]) ).
fof(f2043,plain,
index_69 = index_6,
inference(backward_demodulation,[status(thm)],[f2041,f702]) ).
fof(f2046,plain,
p(index_72) = index_6,
inference(backward_demodulation,[status(thm)],[f2043,f983]) ).
fof(f2048,plain,
index_72 = s(index_6),
inference(backward_demodulation,[status(thm)],[f2043,f546]) ).
fof(f2052,plain,
rselect_head(queue_73) = rselect_head(queue_71),
inference(paramodulation,[status(thm)],[f641,f357]) ).
fof(f2054,plain,
rselect_tail(queue_73) = index_72,
inference(paramodulation,[status(thm)],[f641,f354]) ).
fof(f2056,plain,
index_135 = index_72,
inference(backward_demodulation,[status(thm)],[f2054,f735]) ).
fof(f2062,plain,
index_138 = s(index_72),
inference(backward_demodulation,[status(thm)],[f2056,f475]) ).
fof(f2086,plain,
rselect_head(queue_79) = rselect_head(queue_77),
inference(paramodulation,[status(thm)],[f643,f357]) ).
fof(f2088,plain,
rselect_tail(queue_79) = index_78,
inference(paramodulation,[status(thm)],[f643,f354]) ).
fof(f2090,plain,
index_81 = index_78,
inference(backward_demodulation,[status(thm)],[f2088,f738]) ).
fof(f2095,plain,
index_84 = s(index_78),
inference(backward_demodulation,[status(thm)],[f2090,f550]) ).
fof(f2099,plain,
rselect_head(queue_85) = rselect_head(queue_83),
inference(paramodulation,[status(thm)],[f645,f357]) ).
fof(f2101,plain,
rselect_tail(queue_85) = index_84,
inference(paramodulation,[status(thm)],[f645,f354]) ).
fof(f2103,plain,
index_87 = index_84,
inference(backward_demodulation,[status(thm)],[f2101,f741]) ).
fof(f2106,plain,
p(index_90) = index_84,
inference(backward_demodulation,[status(thm)],[f2103,f995]) ).
fof(f2112,plain,
rselect_head(queue_91) = rselect_head(queue_89),
inference(paramodulation,[status(thm)],[f647,f357]) ).
fof(f2114,plain,
rselect_tail(queue_91) = index_90,
inference(paramodulation,[status(thm)],[f647,f354]) ).
fof(f2116,plain,
index_93 = index_90,
inference(backward_demodulation,[status(thm)],[f2114,f744]) ).
fof(f2119,plain,
p(index_96) = index_90,
inference(backward_demodulation,[status(thm)],[f2116,f997]) ).
fof(f2125,plain,
rselect_head(queue_97) = rselect_head(queue_95),
inference(paramodulation,[status(thm)],[f649,f357]) ).
fof(f2127,plain,
rselect_tail(queue_97) = index_96,
inference(paramodulation,[status(thm)],[f649,f354]) ).
fof(f2129,plain,
index_99 = index_96,
inference(backward_demodulation,[status(thm)],[f2127,f747]) ).
fof(f2135,plain,
index_102 = s(index_96),
inference(backward_demodulation,[status(thm)],[f2129,f462]) ).
fof(f2152,plain,
rselect_head(queue_5) = rselect_head(queue_1),
inference(paramodulation,[status(thm)],[f698,f358]) ).
fof(f2155,plain,
rselect_head(queue_7) = rselect_head(queue_1),
inference(forward_demodulation,[status(thm)],[f2039,f2152]) ).
fof(f2157,plain,
rselect_head(queue_7) = index_0,
inference(forward_demodulation,[status(thm)],[f1257,f2155]) ).
fof(f2164,plain,
rselect_head(queue_71) = rselect_head(queue_7),
inference(paramodulation,[status(thm)],[f701,f358]) ).
fof(f2167,plain,
rselect_head(queue_73) = rselect_head(queue_7),
inference(forward_demodulation,[status(thm)],[f2052,f2164]) ).
fof(f2169,plain,
rselect_head(queue_73) = index_0,
inference(forward_demodulation,[status(thm)],[f2157,f2167]) ).
fof(f2207,plain,
rselect_head(queue_17) = rselect_head(queue_13),
inference(paramodulation,[status(thm)],[f704,f358]) ).
fof(f2210,plain,
rselect_head(queue_19) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2211,f1364]) ).
fof(f2211,plain,
rselect_head(queue_19) = rselect_head(queue_13),
inference(forward_demodulation,[status(thm)],[f1582,f2207]) ).
fof(f2218,plain,
rselect_head(queue_23) = rselect_head(queue_19),
inference(paramodulation,[status(thm)],[f707,f358]) ).
fof(f2221,plain,
rselect_head(queue_25) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2224,f2210]) ).
fof(f2224,plain,
rselect_head(queue_25) = rselect_head(queue_19),
inference(forward_demodulation,[status(thm)],[f1789,f2218]) ).
fof(f2231,plain,
rselect_head(queue_29) = rselect_head(queue_25),
inference(paramodulation,[status(thm)],[f710,f358]) ).
fof(f2236,plain,
rselect_head(queue_31) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2239,f2221]) ).
fof(f2239,plain,
rselect_head(queue_31) = rselect_head(queue_25),
inference(forward_demodulation,[status(thm)],[f1904,f2231]) ).
fof(f2250,plain,
rselect_head(queue_35) = rselect_head(queue_31),
inference(paramodulation,[status(thm)],[f713,f358]) ).
fof(f2255,plain,
rselect_head(queue_37) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2260,f2236]) ).
fof(f2260,plain,
rselect_head(queue_37) = rselect_head(queue_31),
inference(forward_demodulation,[status(thm)],[f1929,f2250]) ).
fof(f2287,plain,
rselect_head(queue_41) = rselect_head(queue_37),
inference(paramodulation,[status(thm)],[f716,f358]) ).
fof(f2294,plain,
rselect_head(queue_43) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2299,f2255]) ).
fof(f2299,plain,
rselect_head(queue_43) = rselect_head(queue_37),
inference(forward_demodulation,[status(thm)],[f1942,f2287]) ).
fof(f2306,plain,
rselect_head(queue_47) = rselect_head(queue_43),
inference(paramodulation,[status(thm)],[f719,f358]) ).
fof(f2313,plain,
rselect_head(queue_49) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2320,f2294]) ).
fof(f2320,plain,
rselect_head(queue_49) = rselect_head(queue_43),
inference(forward_demodulation,[status(thm)],[f1971,f2306]) ).
fof(f2363,plain,
rselect_head(queue_53) = rselect_head(queue_49),
inference(paramodulation,[status(thm)],[f722,f358]) ).
fof(f2372,plain,
rselect_head(queue_55) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2379,f2313]) ).
fof(f2379,plain,
rselect_head(queue_55) = rselect_head(queue_49),
inference(forward_demodulation,[status(thm)],[f1984,f2363]) ).
fof(f2386,plain,
rselect_head(queue_59) = rselect_head(queue_55),
inference(paramodulation,[status(thm)],[f725,f358]) ).
fof(f2395,plain,
rselect_head(queue_61) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2404,f2372]) ).
fof(f2404,plain,
rselect_head(queue_61) = rselect_head(queue_55),
inference(forward_demodulation,[status(thm)],[f1997,f2386]) ).
fof(f2411,plain,
rselect_head(queue_65) = rselect_head(queue_61),
inference(paramodulation,[status(thm)],[f728,f358]) ).
fof(f2422,plain,
rselect_head(queue_67) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2431,f2395]) ).
fof(f2431,plain,
rselect_head(queue_67) = rselect_head(queue_61),
inference(forward_demodulation,[status(thm)],[f2010,f2411]) ).
fof(f2442,plain,
rselect_head(queue_77) = rselect_head(queue_67),
inference(paramodulation,[status(thm)],[f731,f358]) ).
fof(f2453,plain,
rselect_head(queue_79) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2464,f2422]) ).
fof(f2464,plain,
rselect_head(queue_79) = rselect_head(queue_67),
inference(forward_demodulation,[status(thm)],[f2086,f2442]) ).
fof(f2479,plain,
rselect_head(queue_137) = rselect_head(queue_73),
inference(paramodulation,[status(thm)],[f734,f358]) ).
fof(f2482,plain,
rselect_head(queue_139) = index_0,
inference(backward_demodulation,[status(thm)],[f2483,f1416]) ).
fof(f2483,plain,
rselect_head(queue_137) = index_0,
inference(forward_demodulation,[status(thm)],[f2169,f2479]) ).
fof(f2490,plain,
rselect_head(queue_83) = rselect_head(queue_79),
inference(paramodulation,[status(thm)],[f737,f358]) ).
fof(f2503,plain,
rselect_head(queue_85) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2514,f2453]) ).
fof(f2514,plain,
rselect_head(queue_85) = rselect_head(queue_79),
inference(forward_demodulation,[status(thm)],[f2099,f2490]) ).
fof(f2521,plain,
rselect_head(queue_89) = rselect_head(queue_85),
inference(paramodulation,[status(thm)],[f740,f358]) ).
fof(f2534,plain,
rselect_head(queue_91) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2547,f2503]) ).
fof(f2547,plain,
rselect_head(queue_91) = rselect_head(queue_85),
inference(forward_demodulation,[status(thm)],[f2112,f2521]) ).
fof(f2554,plain,
rselect_head(queue_95) = rselect_head(queue_91),
inference(paramodulation,[status(thm)],[f743,f358]) ).
fof(f2569,plain,
rselect_head(queue_97) = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2582,f2534]) ).
fof(f2582,plain,
rselect_head(queue_97) = rselect_head(queue_91),
inference(forward_demodulation,[status(thm)],[f2125,f2554]) ).
fof(f2588,plain,
rselect_head(queue_101) = rselect_head(queue_97),
inference(paramodulation,[status(thm)],[f746,f358]) ).
fof(f2591,plain,
rselect_head(queue_103) = rselect_head(queue_97),
inference(backward_demodulation,[status(thm)],[f2588,f1275]) ).
fof(f2598,plain,
rselect_head(queue_107) = rselect_head(queue_103),
inference(paramodulation,[status(thm)],[f749,f358]) ).
fof(f2601,plain,
rselect_head(queue_109) = rselect_head(queue_103),
inference(forward_demodulation,[status(thm)],[f1292,f2598]) ).
fof(f2603,plain,
rselect_head(queue_109) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2591,f2601]) ).
fof(f2610,plain,
rselect_head(queue_113) = rselect_head(queue_109),
inference(paramodulation,[status(thm)],[f752,f358]) ).
fof(f2613,plain,
rselect_head(queue_115) = rselect_head(queue_109),
inference(forward_demodulation,[status(thm)],[f1307,f2610]) ).
fof(f2615,plain,
rselect_head(queue_115) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2603,f2613]) ).
fof(f2622,plain,
rselect_head(queue_119) = rselect_head(queue_115),
inference(paramodulation,[status(thm)],[f755,f358]) ).
fof(f2625,plain,
rselect_head(queue_121) = rselect_head(queue_115),
inference(forward_demodulation,[status(thm)],[f1322,f2622]) ).
fof(f2627,plain,
rselect_head(queue_121) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2615,f2625]) ).
fof(f2634,plain,
rselect_head(queue_125) = rselect_head(queue_121),
inference(paramodulation,[status(thm)],[f758,f358]) ).
fof(f2637,plain,
rselect_head(queue_127) = rselect_head(queue_121),
inference(forward_demodulation,[status(thm)],[f1349,f2634]) ).
fof(f2639,plain,
rselect_head(queue_127) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2627,f2637]) ).
fof(f2646,plain,
rselect_head(queue_131) = rselect_head(queue_127),
inference(paramodulation,[status(thm)],[f761,f358]) ).
fof(f2649,plain,
rselect_head(queue_133) = rselect_head(queue_127),
inference(forward_demodulation,[status(thm)],[f1402,f2646]) ).
fof(f2651,plain,
rselect_head(queue_133) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2639,f2649]) ).
fof(f2658,plain,
rselect_head(queue_143) = rselect_head(queue_133),
inference(paramodulation,[status(thm)],[f764,f358]) ).
fof(f2661,plain,
rselect_head(queue_145) = rselect_head(queue_133),
inference(forward_demodulation,[status(thm)],[f1430,f2658]) ).
fof(f2663,plain,
rselect_head(queue_145) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2651,f2661]) ).
fof(f2670,plain,
rselect_head(queue_203) = rselect_head(queue_139),
inference(paramodulation,[status(thm)],[f767,f358]) ).
fof(f2673,plain,
rselect_head(queue_205) = rselect_head(queue_139),
inference(forward_demodulation,[status(thm)],[f1645,f2670]) ).
fof(f2675,plain,
rselect_head(queue_205) = index_0,
inference(forward_demodulation,[status(thm)],[f2482,f2673]) ).
fof(f2682,plain,
rselect_head(queue_149) = rselect_head(queue_145),
inference(paramodulation,[status(thm)],[f770,f358]) ).
fof(f2685,plain,
rselect_head(queue_151) = rselect_head(queue_145),
inference(forward_demodulation,[status(thm)],[f1443,f2682]) ).
fof(f2687,plain,
rselect_head(queue_151) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2663,f2685]) ).
fof(f2694,plain,
rselect_head(queue_155) = rselect_head(queue_151),
inference(paramodulation,[status(thm)],[f773,f358]) ).
fof(f2697,plain,
rselect_head(queue_157) = rselect_head(queue_151),
inference(forward_demodulation,[status(thm)],[f1468,f2694]) ).
fof(f2699,plain,
rselect_head(queue_157) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2687,f2697]) ).
fof(f2706,plain,
rselect_head(queue_161) = rselect_head(queue_157),
inference(paramodulation,[status(thm)],[f776,f358]) ).
fof(f2709,plain,
rselect_head(queue_163) = rselect_head(queue_157),
inference(forward_demodulation,[status(thm)],[f1481,f2706]) ).
fof(f2711,plain,
rselect_head(queue_163) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2699,f2709]) ).
fof(f2718,plain,
rselect_head(queue_167) = rselect_head(queue_163),
inference(paramodulation,[status(thm)],[f779,f358]) ).
fof(f2721,plain,
rselect_head(queue_169) = rselect_head(queue_163),
inference(forward_demodulation,[status(thm)],[f1518,f2718]) ).
fof(f2723,plain,
rselect_head(queue_169) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2711,f2721]) ).
fof(f2730,plain,
rselect_head(queue_173) = rselect_head(queue_169),
inference(paramodulation,[status(thm)],[f782,f358]) ).
fof(f2733,plain,
rselect_head(queue_175) = rselect_head(queue_169),
inference(forward_demodulation,[status(thm)],[f1531,f2730]) ).
fof(f2735,plain,
rselect_head(queue_175) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2723,f2733]) ).
fof(f2742,plain,
rselect_head(queue_179) = rselect_head(queue_175),
inference(paramodulation,[status(thm)],[f785,f358]) ).
fof(f2745,plain,
rselect_head(queue_181) = rselect_head(queue_175),
inference(forward_demodulation,[status(thm)],[f1544,f2742]) ).
fof(f2747,plain,
rselect_head(queue_181) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2735,f2745]) ).
fof(f2754,plain,
rselect_head(queue_185) = rselect_head(queue_181),
inference(paramodulation,[status(thm)],[f788,f358]) ).
fof(f2757,plain,
rselect_head(queue_187) = rselect_head(queue_181),
inference(forward_demodulation,[status(thm)],[f1557,f2754]) ).
fof(f2759,plain,
rselect_head(queue_187) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2747,f2757]) ).
fof(f2766,plain,
rselect_head(queue_191) = rselect_head(queue_187),
inference(paramodulation,[status(thm)],[f791,f358]) ).
fof(f2769,plain,
rselect_head(queue_193) = rselect_head(queue_187),
inference(forward_demodulation,[status(thm)],[f1595,f2766]) ).
fof(f2771,plain,
rselect_head(queue_193) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2759,f2769]) ).
fof(f2778,plain,
rselect_head(queue_197) = rselect_head(queue_193),
inference(paramodulation,[status(thm)],[f794,f358]) ).
fof(f2781,plain,
rselect_head(queue_199) = rselect_head(queue_193),
inference(forward_demodulation,[status(thm)],[f1632,f2778]) ).
fof(f2783,plain,
rselect_head(queue_199) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2771,f2781]) ).
fof(f2790,plain,
rselect_head(queue_209) = rselect_head(queue_199),
inference(paramodulation,[status(thm)],[f797,f358]) ).
fof(f2793,plain,
rselect_head(queue_211) = rselect_head(queue_199),
inference(forward_demodulation,[status(thm)],[f1658,f2790]) ).
fof(f2795,plain,
rselect_head(queue_211) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2783,f2793]) ).
fof(f2802,plain,
rselect_head(queue_251) = rselect_head(queue_205),
inference(paramodulation,[status(thm)],[f800,f358]) ).
fof(f2805,plain,
rselect_head(queue_253) = rselect_head(queue_205),
inference(forward_demodulation,[status(thm)],[f1814,f2802]) ).
fof(f2807,plain,
rselect_head(queue_253) = index_0,
inference(forward_demodulation,[status(thm)],[f2675,f2805]) ).
fof(f2814,plain,
rselect_head(queue_215) = rselect_head(queue_211),
inference(paramodulation,[status(thm)],[f803,f358]) ).
fof(f2817,plain,
rselect_head(queue_217) = rselect_head(queue_211),
inference(forward_demodulation,[status(thm)],[f1671,f2814]) ).
fof(f2819,plain,
rselect_head(queue_217) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2795,f2817]) ).
fof(f2826,plain,
rselect_head(queue_221) = rselect_head(queue_217),
inference(paramodulation,[status(thm)],[f806,f358]) ).
fof(f2829,plain,
rselect_head(queue_223) = rselect_head(queue_217),
inference(forward_demodulation,[status(thm)],[f1696,f2826]) ).
fof(f2831,plain,
rselect_head(queue_223) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2819,f2829]) ).
fof(f2838,plain,
rselect_head(queue_227) = rselect_head(queue_223),
inference(paramodulation,[status(thm)],[f809,f358]) ).
fof(f2841,plain,
rselect_head(queue_229) = rselect_head(queue_223),
inference(forward_demodulation,[status(thm)],[f1709,f2838]) ).
fof(f2843,plain,
rselect_head(queue_229) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2831,f2841]) ).
fof(f2850,plain,
rselect_head(queue_233) = rselect_head(queue_229),
inference(paramodulation,[status(thm)],[f812,f358]) ).
fof(f2853,plain,
rselect_head(queue_235) = rselect_head(queue_229),
inference(forward_demodulation,[status(thm)],[f1746,f2850]) ).
fof(f2855,plain,
rselect_head(queue_235) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2843,f2853]) ).
fof(f2862,plain,
rselect_head(queue_239) = rselect_head(queue_235),
inference(paramodulation,[status(thm)],[f815,f358]) ).
fof(f2865,plain,
rselect_head(queue_241) = rselect_head(queue_235),
inference(forward_demodulation,[status(thm)],[f1759,f2862]) ).
fof(f2867,plain,
rselect_head(queue_241) = rselect_head(queue_97),
inference(forward_demodulation,[status(thm)],[f2855,f2865]) ).
fof(f2874,plain,
rselect_head(queue_245) = rselect_head(queue_241),
inference(paramodulation,[status(thm)],[f818,f358]) ).
fof(f2877,plain,
index_279 = rselect_head(queue_97),
inference(backward_demodulation,[status(thm)],[f2878,f2867]) ).
fof(f2878,plain,
index_279 = rselect_head(queue_241),
inference(forward_demodulation,[status(thm)],[f1775,f2874]) ).
fof(f2939,plain,
index_279 = rselect_head(queue_11),
inference(backward_demodulation,[status(thm)],[f2877,f2569]) ).
fof(f2957,plain,
rselect_head(queue_257) = rselect_head(queue_253),
inference(paramodulation,[status(thm)],[f824,f358]) ).
fof(f2960,plain,
rselect_head(queue_259) = rselect_head(queue_253),
inference(forward_demodulation,[status(thm)],[f1827,f2957]) ).
fof(f2962,plain,
rselect_head(queue_259) = index_0,
inference(forward_demodulation,[status(thm)],[f2807,f2960]) ).
fof(f2969,plain,
rselect_head(queue_263) = rselect_head(queue_259),
inference(paramodulation,[status(thm)],[f827,f358]) ).
fof(f2972,plain,
rselect_head(queue_265) = rselect_head(queue_259),
inference(forward_demodulation,[status(thm)],[f1864,f2969]) ).
fof(f2974,plain,
rselect_head(queue_265) = index_0,
inference(forward_demodulation,[status(thm)],[f2962,f2972]) ).
fof(f2981,plain,
rselect_head(queue_269) = rselect_head(queue_265),
inference(paramodulation,[status(thm)],[f830,f358]) ).
fof(f2984,plain,
rselect_head(queue_271) = rselect_head(queue_265),
inference(forward_demodulation,[status(thm)],[f1877,f2981]) ).
fof(f2986,plain,
rselect_head(queue_271) = index_0,
inference(forward_demodulation,[status(thm)],[f2974,f2984]) ).
fof(f2995,plain,
rselect_head(queue_275) = rselect_head(queue_271),
inference(paramodulation,[status(thm)],[f833,f358]) ).
fof(f2998,plain,
rselect_head(queue_277) = rselect_head(queue_271),
inference(forward_demodulation,[status(thm)],[f1890,f2995]) ).
fof(f3000,plain,
rselect_head(queue_277) = index_0,
inference(forward_demodulation,[status(thm)],[f2986,f2998]) ).
fof(f3006,plain,
rselect_head(queue_11) = rselect_head(queue_277),
inference(paramodulation,[status(thm)],[f836,f358]) ).
fof(f3009,plain,
index_279 = rselect_head(queue_277),
inference(forward_demodulation,[status(thm)],[f2939,f3006]) ).
fof(f3024,plain,
elem_280 = select(earray_278,index_0),
inference(backward_demodulation,[status(thm)],[f3085,f459]) ).
fof(f3085,plain,
index_279 = index_0,
inference(forward_demodulation,[status(thm)],[f3000,f3009]) ).
fof(f3143,plain,
s(index_102) = p(index_96),
inference(paramodulation,[status(thm)],[f2135,f880]) ).
fof(f3147,plain,
s(index_138) = p(index_72),
inference(paramodulation,[status(thm)],[f2062,f880]) ).
fof(f3148,plain,
s(index_72) = p(index_6),
inference(paramodulation,[status(thm)],[f2048,f880]) ).
fof(f3149,plain,
s(index_78) = p(index_66),
inference(paramodulation,[status(thm)],[f2019,f880]) ).
fof(f3152,plain,
s(index_54) = p(index_48),
inference(paramodulation,[status(thm)],[f1980,f880]) ).
fof(f3155,plain,
s(index_36) = p(index_30),
inference(paramodulation,[status(thm)],[f1913,f880]) ).
fof(f3158,plain,
s(index_270) = p(index_264),
inference(paramodulation,[status(thm)],[f1873,f880]) ).
fof(f3164,plain,
s(index_234) = p(index_228),
inference(paramodulation,[status(thm)],[f1718,f880]) ).
fof(f3167,plain,
s(index_216) = p(index_210),
inference(paramodulation,[status(thm)],[f1667,f880]) ).
fof(f3168,plain,
s(index_252) = p(index_204),
inference(paramodulation,[status(thm)],[f1654,f880]) ).
fof(f3172,plain,
s(index_192) = p(index_186),
inference(paramodulation,[status(thm)],[f1566,f880]) ).
fof(f3175,plain,
s(index_174) = p(index_168),
inference(paramodulation,[status(thm)],[f1527,f880]) ).
fof(f3178,plain,
s(index_156) = p(index_150),
inference(paramodulation,[status(thm)],[f1452,f880]) ).
fof(f3182,plain,
s(index_18) = p(index_12),
inference(paramodulation,[status(thm)],[f1373,f880]) ).
fof(f3183,plain,
s(index_132) = p(index_126),
inference(paramodulation,[status(thm)],[f1359,f880]) ).
fof(f3186,plain,
s(index_114) = p(index_108),
inference(paramodulation,[status(thm)],[f1302,f880]) ).
fof(f3194,plain,
index_108 = p(index_96),
inference(forward_demodulation,[status(thm)],[f1285,f3143]) ).
fof(f3210,plain,
index_108 = index_90,
inference(forward_demodulation,[status(thm)],[f2119,f3194]) ).
fof(f3229,plain,
index_204 = p(index_72),
inference(forward_demodulation,[status(thm)],[f1425,f3147]) ).
fof(f3240,plain,
p(index_6) = index_138,
inference(backward_demodulation,[status(thm)],[f3245,f1422]) ).
fof(f3245,plain,
index_204 = index_6,
inference(forward_demodulation,[status(thm)],[f2046,f3229]) ).
fof(f3246,plain,
index_138 = index_0,
inference(backward_demodulation,[status(thm)],[f3247,f1260]) ).
fof(f3247,plain,
index_138 = p(index_6),
inference(forward_demodulation,[status(thm)],[f2062,f3148]) ).
fof(f3248,plain,
index_84 = index_60,
inference(backward_demodulation,[status(thm)],[f3249,f2004]) ).
fof(f3249,plain,
index_84 = p(index_66),
inference(forward_demodulation,[status(thm)],[f2095,f3149]) ).
fof(f3254,plain,
index_60 = index_42,
inference(backward_demodulation,[status(thm)],[f3255,f1949]) ).
fof(f3255,plain,
index_60 = p(index_48),
inference(forward_demodulation,[status(thm)],[f1993,f3152]) ).
fof(f3260,plain,
index_42 = index_24,
inference(backward_demodulation,[status(thm)],[f3261,f1795]) ).
fof(f3261,plain,
index_42 = p(index_30),
inference(forward_demodulation,[status(thm)],[f1938,f3155]) ).
fof(f3293,plain,
index_276 = index_258,
inference(backward_demodulation,[status(thm)],[f3294,f1833]) ).
fof(f3294,plain,
index_276 = p(index_264),
inference(forward_demodulation,[status(thm)],[f1886,f3158]) ).
fof(f3302,plain,
index_240 = index_222,
inference(backward_demodulation,[status(thm)],[f3303,f1702]) ).
fof(f3303,plain,
index_240 = p(index_228),
inference(forward_demodulation,[status(thm)],[f1755,f3164]) ).
fof(f3308,plain,
index_222 = index_198,
inference(backward_demodulation,[status(thm)],[f3309,f1638]) ).
fof(f3309,plain,
index_222 = p(index_210),
inference(forward_demodulation,[status(thm)],[f1680,f3167]) ).
fof(f3310,plain,
index_258 = p(index_204),
inference(forward_demodulation,[status(thm)],[f1823,f3168]) ).
fof(f3312,plain,
index_258 = p(index_6),
inference(forward_demodulation,[status(thm)],[f3245,f3310]) ).
fof(f3320,plain,
index_198 = index_180,
inference(backward_demodulation,[status(thm)],[f3321,f1550]) ).
fof(f3321,plain,
index_198 = p(index_186),
inference(forward_demodulation,[status(thm)],[f1604,f3172]) ).
fof(f3326,plain,
index_180 = index_162,
inference(backward_demodulation,[status(thm)],[f3327,f1487]) ).
fof(f3327,plain,
index_180 = p(index_168),
inference(forward_demodulation,[status(thm)],[f1540,f3175]) ).
fof(f3332,plain,
index_162 = index_144,
inference(backward_demodulation,[status(thm)],[f3333,f1436]) ).
fof(f3333,plain,
index_162 = p(index_150),
inference(forward_demodulation,[status(thm)],[f1477,f3178]) ).
fof(f3352,plain,
index_24 = p(index_12),
inference(forward_demodulation,[status(thm)],[f1591,f3182]) ).
fof(f3364,plain,
index_24 = index_276,
inference(forward_demodulation,[status(thm)],[f1897,f3352]) ).
fof(f3365,plain,
index_144 = index_120,
inference(backward_demodulation,[status(thm)],[f3366,f1328]) ).
fof(f3366,plain,
index_144 = p(index_126),
inference(forward_demodulation,[status(thm)],[f1411,f3183]) ).
fof(f3370,plain,
index_120 = p(index_108),
inference(forward_demodulation,[status(thm)],[f1317,f3186]) ).
fof(f3371,plain,
index_120 = p(index_90),
inference(forward_demodulation,[status(thm)],[f3210,f3370]) ).
fof(f3385,plain,
index_120 = index_84,
inference(forward_demodulation,[status(thm)],[f2106,f3371]) ).
fof(f3452,plain,
index_258 = index_138,
inference(forward_demodulation,[status(thm)],[f3312,f3240]) ).
fof(f3538,plain,
elem_280 = select(earray_278,index_258),
inference(backward_demodulation,[status(thm)],[f3561,f3024]) ).
fof(f3561,plain,
index_258 = index_0,
inference(forward_demodulation,[status(thm)],[f3452,f3246]) ).
fof(f3608,plain,
index_84 = index_42,
inference(forward_demodulation,[status(thm)],[f3248,f3254]) ).
fof(f3628,plain,
index_84 = index_276,
inference(backward_demodulation,[status(thm)],[f3629,f3364]) ).
fof(f3629,plain,
index_84 = index_24,
inference(forward_demodulation,[status(thm)],[f3608,f3260]) ).
fof(f3744,plain,
index_240 = index_198,
inference(forward_demodulation,[status(thm)],[f3302,f3308]) ).
fof(f3803,plain,
index_240 = index_180,
inference(forward_demodulation,[status(thm)],[f3744,f3320]) ).
fof(f3839,plain,
index_240 = index_162,
inference(forward_demodulation,[status(thm)],[f3803,f3326]) ).
fof(f3875,plain,
index_240 = index_144,
inference(forward_demodulation,[status(thm)],[f3839,f3332]) ).
fof(f3904,plain,
index_240 = index_120,
inference(forward_demodulation,[status(thm)],[f3875,f3365]) ).
fof(f3916,plain,
elem_283 = select(earray_278,index_84),
inference(backward_demodulation,[status(thm)],[f3924,f1787]) ).
fof(f3924,plain,
index_240 = index_84,
inference(forward_demodulation,[status(thm)],[f3385,f3904]) ).
fof(f4108,plain,
elem_280 = select(earray_278,index_276),
inference(forward_demodulation,[status(thm)],[f3293,f3538]) ).
fof(f4176,plain,
elem_280 = select(earray_278,index_84),
inference(backward_demodulation,[status(thm)],[f3628,f4108]) ).
fof(f4625,plain,
elem_280 = elem_283,
inference(forward_demodulation,[status(thm)],[f3916,f4176]) ).
fof(f4626,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4625,f697]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.43 % Computer : n014.cluster.edu
% 0.11/5.43 % Model : x86_64 x86_64
% 0.11/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.43 % Memory : 8046.5625MB
% 0.11/5.43 % OS : Linux 6.8.0-71-generic
% 0.11/5.43 % CPULimit : 300
% 0.11/5.43 % WCLimit : 300
% 0.11/5.43 % DateTime : Mon Sep 21 09:10:55 UTC 2026
% 0.11/5.43 % CPUTime :
% 0.11/5.45 % Drodi V4.1.1
% 0.14/5.65 % Refutation found
% 0.14/5.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/5.67 % Elapsed time: 0.229280 seconds
% 0.14/5.67 % CPU time: 1.566214 seconds
% 0.14/5.67 % Total memory used: 143.397 MB
% 0.14/5.67 % Net memory used: 142.554 MB
%------------------------------------------------------------------------------