%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 1.03s 0.57s
% Output : CNFRefutation 1.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 231
% Syntax : Number of formulae : 932 ( 932 unt; 0 def)
% Number of atoms : 932 ( 931 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 : 276 ( 276 usr; 268 con; 0-2 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : p(s(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : s(s(s(X))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
elem_262 = select(earray_260,index_261),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
elem_265 = select(earray_260,index_264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
index_105 = rselect_tail(q24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
index_111 = rselect_tail(q25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
index_126 = s(index_123),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
index_129 = rselect_tail(q28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
index_135 = rselect_tail(q2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
index_138 = s(index_135),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,hypothesis,
index_141 = rselect_tail(q29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,hypothesis,
index_153 = rselect_tail(q31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,hypothesis,
index_159 = rselect_tail(q32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
index_162 = s(index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_165 = rselect_tail(q33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,hypothesis,
index_168 = s(index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,hypothesis,
index_171 = rselect_tail(q34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,hypothesis,
index_177 = rselect_tail(q35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
index_183 = rselect_tail(q36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
index_189 = rselect_tail(q37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
index_192 = s(index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
index_195 = rselect_tail(q38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
index_198 = s(index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
index_201 = rselect_tail(q3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
index_204 = s(index_201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
index_207 = rselect_tail(q39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
index_210 = s(index_207),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
index_213 = rselect_tail(q40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
index_219 = rselect_tail(q41),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_225 = rselect_tail(q42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_231 = rselect_tail(q4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_234 = s(index_231),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_237 = rselect_tail(q5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_240 = s(index_237),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_243 = rselect_tail(q6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_246 = s(index_243),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_249 = rselect_tail(q7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_252 = s(index_249),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_255 = rselect_tail(q8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_258 = s(index_255),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_261 = rselect_head(q43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_263 = rselect_tail(q43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
s(index_264) = index_263,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_27 = rselect_tail(q12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_30 = s(index_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_33 = rselect_tail(q13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_36 = s(index_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_39 = rselect_tail(q14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_42 = s(index_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_45 = rselect_tail(q15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_48 = s(index_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_51 = rselect_tail(q16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_57 = rselect_tail(q17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_63 = rselect_tail(q18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_69 = rselect_tail(q1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_75 = rselect_tail(q19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_78 = s(index_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_81 = rselect_tail(q20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_84 = s(index_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_87 = rselect_tail(q21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_93 = rselect_tail(q22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_96 = s(index_93),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_99 = rselect_tail(q23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
queue_101 = rstore_seq(q23,earray_100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
queue_107 = rstore_seq(q24,earray_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
queue_119 = rstore_seq(q26,earray_118),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
queue_131 = rstore_seq(q28,earray_130),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
queue_137 = rstore_seq(q2,earray_136),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_149 = rstore_seq(q30,earray_148),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_161 = rstore_seq(q32,earray_160),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_173 = rstore_seq(q34,earray_172),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_185 = rstore_seq(q36,earray_184),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_197 = rstore_seq(q38,earray_196),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_215 = rstore_seq(q40,earray_214),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_227 = rstore_seq(q42,earray_226),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_233 = rstore_seq(q4,earray_232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_239 = rstore_seq(q5,earray_238),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_245 = rstore_seq(q6,earray_244),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_251 = rstore_seq(q7,earray_250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_257 = rstore_seq(q8,earray_256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_29 = rstore_seq(q12,earray_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_41 = rstore_seq(q14,earray_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_53 = rstore_seq(q16,earray_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_65 = rstore_seq(q18,earray_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_83 = rstore_seq(q20,earray_82),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_95 = rstore_seq(q22,earray_94),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
q5 = queue_235,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
q6 = queue_241,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
q7 = queue_247,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
q8 = queue_253,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
q9 = queue_259,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f327,negated_conjecture,
elem_262 != elem_265,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f332,plain,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f333,plain,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f336,plain,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f337,plain,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f339,plain,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f340,plain,
! [X0] : p(s(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f344,plain,
! [X0] : s(s(s(X0))) = X0,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f432,plain,
elem_262 = select(earray_260,index_261),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f433,plain,
elem_265 = select(earray_260,index_264),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f434,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f435,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f436,plain,
index_105 = rselect_tail(q24),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f437,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f438,plain,
index_111 = rselect_tail(q25),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f439,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f440,plain,
index_117 = rselect_tail(q26),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f441,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f442,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f443,plain,
index_123 = rselect_tail(q27),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f444,plain,
index_126 = s(index_123),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f445,plain,
index_129 = rselect_tail(q28),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f446,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f447,plain,
index_135 = rselect_tail(q2),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f448,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f449,plain,
index_141 = rselect_tail(q29),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f450,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f451,plain,
index_147 = rselect_tail(q30),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f452,plain,
index_15 = rselect_tail(q10),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f453,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f454,plain,
index_153 = rselect_tail(q31),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f455,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f456,plain,
index_159 = rselect_tail(q32),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f457,plain,
index_162 = s(index_159),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f458,plain,
index_165 = rselect_tail(q33),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f459,plain,
index_168 = s(index_165),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f460,plain,
index_171 = rselect_tail(q34),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f461,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f462,plain,
index_177 = rselect_tail(q35),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f463,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f464,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f465,plain,
index_183 = rselect_tail(q36),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f466,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f467,plain,
index_189 = rselect_tail(q37),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f468,plain,
index_192 = s(index_189),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f469,plain,
index_195 = rselect_tail(q38),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f470,plain,
index_198 = s(index_195),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f471,plain,
index_201 = rselect_tail(q3),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f472,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f473,plain,
index_207 = rselect_tail(q39),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f474,plain,
index_21 = rselect_tail(q11),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f475,plain,
index_210 = s(index_207),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f476,plain,
index_213 = rselect_tail(q40),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f477,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f478,plain,
index_219 = rselect_tail(q41),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f479,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f480,plain,
index_225 = rselect_tail(q42),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f481,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f482,plain,
index_231 = rselect_tail(q4),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f483,plain,
index_234 = s(index_231),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f484,plain,
index_237 = rselect_tail(q5),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f485,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f486,plain,
index_240 = s(index_237),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f487,plain,
index_243 = rselect_tail(q6),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f488,plain,
index_246 = s(index_243),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f489,plain,
index_249 = rselect_tail(q7),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f490,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f491,plain,
index_255 = rselect_tail(q8),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f492,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f493,plain,
index_261 = rselect_head(q43),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f494,plain,
index_263 = rselect_tail(q43),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f495,plain,
s(index_264) = index_263,
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f496,plain,
index_27 = rselect_tail(q12),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f497,plain,
index_3 = rselect_tail(q0),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f498,plain,
index_30 = s(index_27),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f499,plain,
index_33 = rselect_tail(q13),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f500,plain,
index_36 = s(index_33),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f501,plain,
index_39 = rselect_tail(q14),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f502,plain,
index_42 = s(index_39),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f503,plain,
index_45 = rselect_tail(q15),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f504,plain,
index_48 = s(index_45),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f505,plain,
index_51 = rselect_tail(q16),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f506,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f507,plain,
index_57 = rselect_tail(q17),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f508,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f509,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f510,plain,
index_63 = rselect_tail(q18),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f511,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f512,plain,
index_69 = rselect_tail(q1),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f513,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f514,plain,
index_75 = rselect_tail(q19),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f515,plain,
index_78 = s(index_75),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f516,plain,
index_81 = rselect_tail(q20),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f517,plain,
index_84 = s(index_81),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f518,plain,
index_87 = rselect_tail(q21),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f519,plain,
index_9 = rselect_tail(q9),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f520,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f521,plain,
index_93 = rselect_tail(q22),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f522,plain,
index_96 = s(index_93),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f523,plain,
index_99 = rselect_tail(q23),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f524,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f525,plain,
queue_101 = rstore_seq(q23,earray_100),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f526,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f527,plain,
queue_107 = rstore_seq(q24,earray_106),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f528,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f529,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f530,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f531,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f532,plain,
queue_119 = rstore_seq(q26,earray_118),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f533,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f534,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f535,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f536,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f537,plain,
queue_131 = rstore_seq(q28,earray_130),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f538,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f539,plain,
queue_137 = rstore_seq(q2,earray_136),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f540,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f541,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f542,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f543,plain,
queue_149 = rstore_seq(q30,earray_148),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f544,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f545,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f546,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f547,plain,
queue_161 = rstore_seq(q32,earray_160),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f548,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f549,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f550,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f551,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f552,plain,
queue_173 = rstore_seq(q34,earray_172),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f553,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f554,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f555,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f556,plain,
queue_185 = rstore_seq(q36,earray_184),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f557,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f558,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f559,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f560,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f561,plain,
queue_197 = rstore_seq(q38,earray_196),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f562,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f563,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f564,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f565,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f566,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f567,plain,
queue_215 = rstore_seq(q40,earray_214),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f568,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f569,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f570,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f571,plain,
queue_227 = rstore_seq(q42,earray_226),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f572,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f573,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f574,plain,
queue_233 = rstore_seq(q4,earray_232),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f575,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f576,plain,
queue_239 = rstore_seq(q5,earray_238),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f577,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f578,plain,
queue_245 = rstore_seq(q6,earray_244),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f579,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f580,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f581,plain,
queue_251 = rstore_seq(q7,earray_250),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f582,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f583,plain,
queue_257 = rstore_seq(q8,earray_256),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f584,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f585,plain,
queue_29 = rstore_seq(q12,earray_28),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f586,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f587,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f588,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f589,plain,
queue_41 = rstore_seq(q14,earray_40),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f590,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f591,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f592,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f593,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f594,plain,
queue_53 = rstore_seq(q16,earray_52),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f595,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f596,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f597,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f598,plain,
queue_65 = rstore_seq(q18,earray_64),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f599,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f600,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f601,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f602,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f603,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f604,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f605,plain,
queue_83 = rstore_seq(q20,earray_82),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f606,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f607,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f608,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f609,plain,
queue_95 = rstore_seq(q22,earray_94),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f610,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f611,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f612,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f613,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f614,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f615,plain,
q12 = queue_25,
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f616,plain,
q13 = queue_31,
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f617,plain,
q14 = queue_37,
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f618,plain,
q15 = queue_43,
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f619,plain,
q16 = queue_49,
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f620,plain,
q17 = queue_55,
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f621,plain,
q18 = queue_61,
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f622,plain,
q19 = queue_67,
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f623,plain,
q2 = queue_73,
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f624,plain,
q20 = queue_79,
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f625,plain,
q21 = queue_85,
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f626,plain,
q22 = queue_91,
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f627,plain,
q23 = queue_97,
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f628,plain,
q24 = queue_103,
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f629,plain,
q25 = queue_109,
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f630,plain,
q26 = queue_115,
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f631,plain,
q27 = queue_121,
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f632,plain,
q28 = queue_127,
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f633,plain,
q29 = queue_133,
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f634,plain,
q3 = queue_139,
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f635,plain,
q30 = queue_145,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f636,plain,
q31 = queue_151,
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f637,plain,
q32 = queue_157,
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f638,plain,
q33 = queue_163,
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f639,plain,
q34 = queue_169,
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f640,plain,
q35 = queue_175,
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f641,plain,
q36 = queue_181,
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f642,plain,
q37 = queue_187,
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f643,plain,
q38 = queue_193,
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f644,plain,
q39 = queue_199,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f645,plain,
q4 = queue_205,
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f646,plain,
q40 = queue_211,
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f647,plain,
q41 = queue_217,
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f648,plain,
q42 = queue_223,
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f649,plain,
q43 = queue_229,
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f650,plain,
q5 = queue_235,
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f651,plain,
q6 = queue_241,
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f652,plain,
q7 = queue_247,
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f653,plain,
q8 = queue_253,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f654,plain,
q9 = queue_259,
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f655,plain,
elem_262 != elem_265,
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f770,plain,
p(index_12) = index_9,
inference(paramodulation,[status(thm)],[f441,f340]) ).
fof(f814,plain,
p(index_18) = index_15,
inference(paramodulation,[status(thm)],[f463,f340]) ).
fof(f834,plain,
p(index_204) = index_201,
inference(paramodulation,[status(thm)],[f472,f340]) ).
fof(f854,plain,
p(index_234) = index_231,
inference(paramodulation,[status(thm)],[f483,f340]) ).
fof(f866,plain,
p(index_246) = index_243,
inference(paramodulation,[status(thm)],[f488,f340]) ).
fof(f870,plain,
p(index_252) = index_249,
inference(paramodulation,[status(thm)],[f490,f340]) ).
fof(f878,plain,
p(index_263) = index_264,
inference(paramodulation,[status(thm)],[f495,f340]) ).
fof(f882,plain,
p(index_30) = index_27,
inference(paramodulation,[status(thm)],[f498,f340]) ).
fof(f932,plain,
q0 = rstore_head(q,index_0),
inference(forward_demodulation,[status(thm)],[f611,f524]) ).
fof(f933,plain,
rselect_tail(q0) = rselect_tail(q),
inference(paramodulation,[status(thm)],[f932,f339]) ).
fof(f935,plain,
rselect_head(q0) = index_0,
inference(paramodulation,[status(thm)],[f932,f332]) ).
fof(f936,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[status(thm)],[f497,f933]) ).
fof(f939,plain,
rselect_head(queue_101) = rselect_head(q23),
inference(paramodulation,[status(thm)],[f525,f337]) ).
fof(f942,plain,
q24 = rstore_tail(queue_101,index_102),
inference(forward_demodulation,[status(thm)],[f628,f526]) ).
fof(f943,plain,
rselect_head(q24) = rselect_head(queue_101),
inference(paramodulation,[status(thm)],[f942,f336]) ).
fof(f945,plain,
rselect_tail(q24) = index_102,
inference(paramodulation,[status(thm)],[f942,f333]) ).
fof(f947,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f436,f945]) ).
fof(f950,plain,
index_105 = s(index_99),
inference(backward_demodulation,[status(thm)],[f947,f435]) ).
fof(f952,plain,
rselect_head(queue_107) = rselect_head(q24),
inference(paramodulation,[status(thm)],[f527,f337]) ).
fof(f956,plain,
q25 = rstore_tail(queue_107,index_108),
inference(forward_demodulation,[status(thm)],[f629,f528]) ).
fof(f957,plain,
rselect_head(q25) = rselect_head(queue_107),
inference(paramodulation,[status(thm)],[f956,f336]) ).
fof(f959,plain,
rselect_tail(q25) = index_108,
inference(paramodulation,[status(thm)],[f956,f333]) ).
fof(f961,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f438,f959]) ).
fof(f963,plain,
rselect_head(queue_11) = rselect_head(q9),
inference(paramodulation,[status(thm)],[f529,f337]) ).
fof(f968,plain,
index_111 = s(index_105),
inference(backward_demodulation,[status(thm)],[f961,f437]) ).
fof(f971,plain,
rselect_head(queue_113) = rselect_head(q25),
inference(paramodulation,[status(thm)],[f530,f337]) ).
fof(f974,plain,
q26 = rstore_tail(queue_113,index_114),
inference(forward_demodulation,[status(thm)],[f630,f531]) ).
fof(f975,plain,
rselect_head(q26) = rselect_head(queue_113),
inference(paramodulation,[status(thm)],[f974,f336]) ).
fof(f977,plain,
rselect_tail(q26) = index_114,
inference(paramodulation,[status(thm)],[f974,f333]) ).
fof(f979,plain,
index_117 = index_114,
inference(forward_demodulation,[status(thm)],[f440,f977]) ).
fof(f981,plain,
rselect_head(queue_119) = rselect_head(q26),
inference(paramodulation,[status(thm)],[f532,f337]) ).
fof(f986,plain,
index_117 = s(index_111),
inference(backward_demodulation,[status(thm)],[f979,f439]) ).
fof(f987,plain,
q27 = rstore_tail(queue_119,index_120),
inference(forward_demodulation,[status(thm)],[f631,f533]) ).
fof(f988,plain,
rselect_head(q27) = rselect_head(queue_119),
inference(paramodulation,[status(thm)],[f987,f336]) ).
fof(f990,plain,
rselect_tail(q27) = index_120,
inference(paramodulation,[status(thm)],[f987,f333]) ).
fof(f992,plain,
index_123 = index_120,
inference(forward_demodulation,[status(thm)],[f443,f990]) ).
fof(f995,plain,
index_123 = s(index_117),
inference(backward_demodulation,[status(thm)],[f992,f442]) ).
fof(f997,plain,
rselect_head(queue_125) = rselect_head(q27),
inference(paramodulation,[status(thm)],[f534,f337]) ).
fof(f1000,plain,
q28 = rstore_tail(queue_125,index_126),
inference(forward_demodulation,[status(thm)],[f632,f535]) ).
fof(f1001,plain,
rselect_head(q28) = rselect_head(queue_125),
inference(paramodulation,[status(thm)],[f1000,f336]) ).
fof(f1003,plain,
rselect_tail(q28) = index_126,
inference(paramodulation,[status(thm)],[f1000,f333]) ).
fof(f1005,plain,
index_129 = index_126,
inference(forward_demodulation,[status(thm)],[f445,f1003]) ).
fof(f1008,plain,
index_129 = s(index_123),
inference(backward_demodulation,[status(thm)],[f1005,f444]) ).
fof(f1009,plain,
q10 = rstore_tail(queue_11,index_12),
inference(forward_demodulation,[status(thm)],[f613,f536]) ).
fof(f1010,plain,
rselect_head(q10) = rselect_head(queue_11),
inference(paramodulation,[status(thm)],[f1009,f336]) ).
fof(f1012,plain,
rselect_tail(q10) = index_12,
inference(paramodulation,[status(thm)],[f1009,f333]) ).
fof(f1014,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f452,f1012]) ).
fof(f1016,plain,
rselect_head(queue_131) = rselect_head(q28),
inference(paramodulation,[status(thm)],[f537,f337]) ).
fof(f1019,plain,
q29 = rstore_tail(queue_131,index_132),
inference(forward_demodulation,[status(thm)],[f633,f538]) ).
fof(f1020,plain,
rselect_head(q29) = rselect_head(queue_131),
inference(paramodulation,[status(thm)],[f1019,f336]) ).
fof(f1022,plain,
rselect_tail(q29) = index_132,
inference(paramodulation,[status(thm)],[f1019,f333]) ).
fof(f1024,plain,
index_141 = index_132,
inference(forward_demodulation,[status(thm)],[f449,f1022]) ).
fof(f1027,plain,
index_15 = s(index_9),
inference(backward_demodulation,[status(thm)],[f1014,f441]) ).
fof(f1029,plain,
rselect_head(queue_137) = rselect_head(q2),
inference(paramodulation,[status(thm)],[f539,f337]) ).
fof(f1034,plain,
index_141 = s(index_129),
inference(backward_demodulation,[status(thm)],[f1024,f446]) ).
fof(f1035,plain,
q3 = rstore_tail(queue_137,index_138),
inference(forward_demodulation,[status(thm)],[f634,f540]) ).
fof(f1036,plain,
rselect_head(q3) = rselect_head(queue_137),
inference(paramodulation,[status(thm)],[f1035,f336]) ).
fof(f1038,plain,
rselect_tail(q3) = index_138,
inference(paramodulation,[status(thm)],[f1035,f333]) ).
fof(f1040,plain,
index_201 = index_138,
inference(forward_demodulation,[status(thm)],[f471,f1038]) ).
fof(f1042,plain,
rselect_head(queue_143) = rselect_head(q29),
inference(paramodulation,[status(thm)],[f541,f337]) ).
fof(f1047,plain,
index_201 = s(index_135),
inference(backward_demodulation,[status(thm)],[f1040,f448]) ).
fof(f1048,plain,
q30 = rstore_tail(queue_143,index_144),
inference(forward_demodulation,[status(thm)],[f635,f542]) ).
fof(f1049,plain,
rselect_head(q30) = rselect_head(queue_143),
inference(paramodulation,[status(thm)],[f1048,f336]) ).
fof(f1051,plain,
rselect_tail(q30) = index_144,
inference(paramodulation,[status(thm)],[f1048,f333]) ).
fof(f1053,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f451,f1051]) ).
fof(f1055,plain,
rselect_head(queue_149) = rselect_head(q30),
inference(paramodulation,[status(thm)],[f543,f337]) ).
fof(f1058,plain,
q31 = rstore_tail(queue_149,index_150),
inference(forward_demodulation,[status(thm)],[f636,f544]) ).
fof(f1059,plain,
rselect_head(q31) = rselect_head(queue_149),
inference(paramodulation,[status(thm)],[f1058,f336]) ).
fof(f1061,plain,
rselect_tail(q31) = index_150,
inference(paramodulation,[status(thm)],[f1058,f333]) ).
fof(f1063,plain,
index_153 = index_150,
inference(forward_demodulation,[status(thm)],[f454,f1061]) ).
fof(f1066,plain,
index_147 = s(index_141),
inference(backward_demodulation,[status(thm)],[f1053,f450]) ).
fof(f1068,plain,
rselect_head(queue_155) = rselect_head(q31),
inference(paramodulation,[status(thm)],[f545,f337]) ).
fof(f1073,plain,
index_153 = s(index_147),
inference(backward_demodulation,[status(thm)],[f1063,f453]) ).
fof(f1074,plain,
q32 = rstore_tail(queue_155,index_156),
inference(forward_demodulation,[status(thm)],[f637,f546]) ).
fof(f1075,plain,
rselect_head(q32) = rselect_head(queue_155),
inference(paramodulation,[status(thm)],[f1074,f336]) ).
fof(f1077,plain,
rselect_tail(q32) = index_156,
inference(paramodulation,[status(thm)],[f1074,f333]) ).
fof(f1079,plain,
index_159 = index_156,
inference(forward_demodulation,[status(thm)],[f456,f1077]) ).
fof(f1081,plain,
rselect_head(queue_161) = rselect_head(q32),
inference(paramodulation,[status(thm)],[f547,f337]) ).
fof(f1086,plain,
index_159 = s(index_153),
inference(backward_demodulation,[status(thm)],[f1079,f455]) ).
fof(f1087,plain,
q33 = rstore_tail(queue_161,index_162),
inference(forward_demodulation,[status(thm)],[f638,f548]) ).
fof(f1088,plain,
rselect_head(q33) = rselect_head(queue_161),
inference(paramodulation,[status(thm)],[f1087,f336]) ).
fof(f1090,plain,
rselect_tail(q33) = index_162,
inference(paramodulation,[status(thm)],[f1087,f333]) ).
fof(f1092,plain,
index_165 = index_162,
inference(forward_demodulation,[status(thm)],[f458,f1090]) ).
fof(f1094,plain,
rselect_head(queue_167) = rselect_head(q33),
inference(paramodulation,[status(thm)],[f549,f337]) ).
fof(f1097,plain,
q34 = rstore_tail(queue_167,index_168),
inference(forward_demodulation,[status(thm)],[f639,f550]) ).
fof(f1098,plain,
rselect_head(q34) = rselect_head(queue_167),
inference(paramodulation,[status(thm)],[f1097,f336]) ).
fof(f1100,plain,
rselect_tail(q34) = index_168,
inference(paramodulation,[status(thm)],[f1097,f333]) ).
fof(f1102,plain,
index_171 = index_168,
inference(forward_demodulation,[status(thm)],[f460,f1100]) ).
fof(f1105,plain,
index_165 = s(index_159),
inference(backward_demodulation,[status(thm)],[f1092,f457]) ).
fof(f1107,plain,
rselect_head(queue_17) = rselect_head(q10),
inference(paramodulation,[status(thm)],[f551,f337]) ).
fof(f1112,plain,
index_171 = s(index_165),
inference(backward_demodulation,[status(thm)],[f1102,f459]) ).
fof(f1114,plain,
rselect_head(queue_173) = rselect_head(q34),
inference(paramodulation,[status(thm)],[f552,f337]) ).
fof(f1117,plain,
q35 = rstore_tail(queue_173,index_174),
inference(forward_demodulation,[status(thm)],[f640,f553]) ).
fof(f1118,plain,
rselect_head(q35) = rselect_head(queue_173),
inference(paramodulation,[status(thm)],[f1117,f336]) ).
fof(f1120,plain,
rselect_tail(q35) = index_174,
inference(paramodulation,[status(thm)],[f1117,f333]) ).
fof(f1122,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f462,f1120]) ).
fof(f1125,plain,
index_177 = s(index_171),
inference(backward_demodulation,[status(thm)],[f1122,f461]) ).
fof(f1127,plain,
rselect_head(queue_179) = rselect_head(q35),
inference(paramodulation,[status(thm)],[f554,f337]) ).
fof(f1130,plain,
q36 = rstore_tail(queue_179,index_180),
inference(forward_demodulation,[status(thm)],[f641,f555]) ).
fof(f1131,plain,
rselect_head(q36) = rselect_head(queue_179),
inference(paramodulation,[status(thm)],[f1130,f336]) ).
fof(f1133,plain,
rselect_tail(q36) = index_180,
inference(paramodulation,[status(thm)],[f1130,f333]) ).
fof(f1135,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f465,f1133]) ).
fof(f1137,plain,
rselect_head(queue_185) = rselect_head(q36),
inference(paramodulation,[status(thm)],[f556,f337]) ).
fof(f1142,plain,
index_183 = s(index_177),
inference(backward_demodulation,[status(thm)],[f1135,f464]) ).
fof(f1143,plain,
q37 = rstore_tail(queue_185,index_186),
inference(forward_demodulation,[status(thm)],[f642,f557]) ).
fof(f1144,plain,
rselect_head(q37) = rselect_head(queue_185),
inference(paramodulation,[status(thm)],[f1143,f336]) ).
fof(f1146,plain,
rselect_tail(q37) = index_186,
inference(paramodulation,[status(thm)],[f1143,f333]) ).
fof(f1148,plain,
index_189 = index_186,
inference(forward_demodulation,[status(thm)],[f467,f1146]) ).
fof(f1151,plain,
index_189 = s(index_183),
inference(backward_demodulation,[status(thm)],[f1148,f466]) ).
fof(f1152,plain,
q11 = rstore_tail(queue_17,index_18),
inference(forward_demodulation,[status(thm)],[f614,f558]) ).
fof(f1153,plain,
rselect_head(q11) = rselect_head(queue_17),
inference(paramodulation,[status(thm)],[f1152,f336]) ).
fof(f1155,plain,
rselect_tail(q11) = index_18,
inference(paramodulation,[status(thm)],[f1152,f333]) ).
fof(f1157,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f474,f1155]) ).
fof(f1159,plain,
rselect_head(queue_191) = rselect_head(q37),
inference(paramodulation,[status(thm)],[f559,f337]) ).
fof(f1164,plain,
index_21 = s(index_15),
inference(backward_demodulation,[status(thm)],[f1157,f463]) ).
fof(f1165,plain,
q38 = rstore_tail(queue_191,index_192),
inference(forward_demodulation,[status(thm)],[f643,f560]) ).
fof(f1166,plain,
rselect_head(q38) = rselect_head(queue_191),
inference(paramodulation,[status(thm)],[f1165,f336]) ).
fof(f1168,plain,
rselect_tail(q38) = index_192,
inference(paramodulation,[status(thm)],[f1165,f333]) ).
fof(f1170,plain,
index_195 = index_192,
inference(forward_demodulation,[status(thm)],[f469,f1168]) ).
fof(f1172,plain,
rselect_head(queue_197) = rselect_head(q38),
inference(paramodulation,[status(thm)],[f561,f337]) ).
fof(f1175,plain,
q39 = rstore_tail(queue_197,index_198),
inference(forward_demodulation,[status(thm)],[f644,f562]) ).
fof(f1176,plain,
rselect_head(q39) = rselect_head(queue_197),
inference(paramodulation,[status(thm)],[f1175,f336]) ).
fof(f1178,plain,
rselect_tail(q39) = index_198,
inference(paramodulation,[status(thm)],[f1175,f333]) ).
fof(f1180,plain,
index_207 = index_198,
inference(forward_demodulation,[status(thm)],[f473,f1178]) ).
fof(f1183,plain,
index_195 = s(index_189),
inference(backward_demodulation,[status(thm)],[f1170,f468]) ).
fof(f1185,plain,
rselect_head(queue_203) = rselect_head(q3),
inference(paramodulation,[status(thm)],[f563,f337]) ).
fof(f1190,plain,
index_207 = s(index_195),
inference(backward_demodulation,[status(thm)],[f1180,f470]) ).
fof(f1191,plain,
q4 = rstore_tail(queue_203,index_204),
inference(forward_demodulation,[status(thm)],[f645,f564]) ).
fof(f1192,plain,
rselect_head(q4) = rselect_head(queue_203),
inference(paramodulation,[status(thm)],[f1191,f336]) ).
fof(f1194,plain,
rselect_tail(q4) = index_204,
inference(paramodulation,[status(thm)],[f1191,f333]) ).
fof(f1196,plain,
index_231 = index_204,
inference(forward_demodulation,[status(thm)],[f482,f1194]) ).
fof(f1198,plain,
rselect_head(queue_209) = rselect_head(q39),
inference(paramodulation,[status(thm)],[f565,f337]) ).
fof(f1203,plain,
index_231 = s(index_201),
inference(backward_demodulation,[status(thm)],[f1196,f472]) ).
fof(f1204,plain,
q40 = rstore_tail(queue_209,index_210),
inference(forward_demodulation,[status(thm)],[f646,f566]) ).
fof(f1205,plain,
rselect_head(q40) = rselect_head(queue_209),
inference(paramodulation,[status(thm)],[f1204,f336]) ).
fof(f1207,plain,
rselect_tail(q40) = index_210,
inference(paramodulation,[status(thm)],[f1204,f333]) ).
fof(f1209,plain,
index_213 = index_210,
inference(forward_demodulation,[status(thm)],[f476,f1207]) ).
fof(f1211,plain,
rselect_head(queue_215) = rselect_head(q40),
inference(paramodulation,[status(thm)],[f567,f337]) ).
fof(f1214,plain,
q41 = rstore_tail(queue_215,index_216),
inference(forward_demodulation,[status(thm)],[f647,f568]) ).
fof(f1215,plain,
rselect_head(q41) = rselect_head(queue_215),
inference(paramodulation,[status(thm)],[f1214,f336]) ).
fof(f1217,plain,
rselect_tail(q41) = index_216,
inference(paramodulation,[status(thm)],[f1214,f333]) ).
fof(f1219,plain,
index_219 = index_216,
inference(forward_demodulation,[status(thm)],[f478,f1217]) ).
fof(f1222,plain,
index_213 = s(index_207),
inference(backward_demodulation,[status(thm)],[f1209,f475]) ).
fof(f1224,plain,
rselect_head(queue_221) = rselect_head(q41),
inference(paramodulation,[status(thm)],[f569,f337]) ).
fof(f1229,plain,
index_219 = s(index_213),
inference(backward_demodulation,[status(thm)],[f1219,f477]) ).
fof(f1230,plain,
q42 = rstore_tail(queue_221,index_222),
inference(forward_demodulation,[status(thm)],[f648,f570]) ).
fof(f1231,plain,
rselect_head(q42) = rselect_head(queue_221),
inference(paramodulation,[status(thm)],[f1230,f336]) ).
fof(f1233,plain,
rselect_tail(q42) = index_222,
inference(paramodulation,[status(thm)],[f1230,f333]) ).
fof(f1235,plain,
index_225 = index_222,
inference(forward_demodulation,[status(thm)],[f480,f1233]) ).
fof(f1237,plain,
rselect_head(queue_227) = rselect_head(q42),
inference(paramodulation,[status(thm)],[f571,f337]) ).
fof(f1242,plain,
index_225 = s(index_219),
inference(backward_demodulation,[status(thm)],[f1235,f479]) ).
fof(f1243,plain,
q43 = rstore_tail(queue_227,index_228),
inference(forward_demodulation,[status(thm)],[f649,f572]) ).
fof(f1244,plain,
rselect_head(q43) = rselect_head(queue_227),
inference(paramodulation,[status(thm)],[f1243,f336]) ).
fof(f1246,plain,
rselect_tail(q43) = index_228,
inference(paramodulation,[status(thm)],[f1243,f333]) ).
fof(f1247,plain,
index_261 = rselect_head(queue_227),
inference(forward_demodulation,[status(thm)],[f493,f1244]) ).
fof(f1250,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(paramodulation,[status(thm)],[f573,f337]) ).
fof(f1254,plain,
rselect_head(queue_233) = rselect_head(q4),
inference(paramodulation,[status(thm)],[f574,f337]) ).
fof(f1261,plain,
q5 = rstore_tail(queue_233,index_234),
inference(forward_demodulation,[status(thm)],[f650,f575]) ).
fof(f1262,plain,
rselect_head(q5) = rselect_head(queue_233),
inference(paramodulation,[status(thm)],[f1261,f336]) ).
fof(f1264,plain,
rselect_tail(q5) = index_234,
inference(paramodulation,[status(thm)],[f1261,f333]) ).
fof(f1266,plain,
index_237 = index_234,
inference(forward_demodulation,[status(thm)],[f484,f1264]) ).
fof(f1269,plain,
index_237 = s(index_231),
inference(backward_demodulation,[status(thm)],[f1266,f483]) ).
fof(f1271,plain,
rselect_head(queue_239) = rselect_head(q5),
inference(paramodulation,[status(thm)],[f576,f337]) ).
fof(f1274,plain,
q6 = rstore_tail(queue_239,index_240),
inference(forward_demodulation,[status(thm)],[f651,f577]) ).
fof(f1275,plain,
rselect_head(q6) = rselect_head(queue_239),
inference(paramodulation,[status(thm)],[f1274,f336]) ).
fof(f1277,plain,
rselect_tail(q6) = index_240,
inference(paramodulation,[status(thm)],[f1274,f333]) ).
fof(f1279,plain,
index_243 = index_240,
inference(forward_demodulation,[status(thm)],[f487,f1277]) ).
fof(f1282,plain,
index_243 = s(index_237),
inference(backward_demodulation,[status(thm)],[f1279,f486]) ).
fof(f1285,plain,
rselect_head(queue_245) = rselect_head(q6),
inference(paramodulation,[status(thm)],[f578,f337]) ).
fof(f1288,plain,
q7 = rstore_tail(queue_245,index_246),
inference(forward_demodulation,[status(thm)],[f652,f579]) ).
fof(f1289,plain,
rselect_head(q7) = rselect_head(queue_245),
inference(paramodulation,[status(thm)],[f1288,f336]) ).
fof(f1291,plain,
rselect_tail(q7) = index_246,
inference(paramodulation,[status(thm)],[f1288,f333]) ).
fof(f1293,plain,
index_249 = index_246,
inference(forward_demodulation,[status(thm)],[f489,f1291]) ).
fof(f1294,plain,
q12 = rstore_tail(queue_23,index_24),
inference(forward_demodulation,[status(thm)],[f615,f580]) ).
fof(f1295,plain,
rselect_head(q12) = rselect_head(queue_23),
inference(paramodulation,[status(thm)],[f1294,f336]) ).
fof(f1297,plain,
rselect_tail(q12) = index_24,
inference(paramodulation,[status(thm)],[f1294,f333]) ).
fof(f1299,plain,
index_27 = index_24,
inference(forward_demodulation,[status(thm)],[f496,f1297]) ).
fof(f1304,plain,
rselect_head(queue_251) = rselect_head(q7),
inference(paramodulation,[status(thm)],[f581,f337]) ).
fof(f1309,plain,
index_27 = s(index_21),
inference(backward_demodulation,[status(thm)],[f1299,f485]) ).
fof(f1310,plain,
q8 = rstore_tail(queue_251,index_252),
inference(forward_demodulation,[status(thm)],[f653,f582]) ).
fof(f1311,plain,
rselect_head(q8) = rselect_head(queue_251),
inference(paramodulation,[status(thm)],[f1310,f336]) ).
fof(f1313,plain,
rselect_tail(q8) = index_252,
inference(paramodulation,[status(thm)],[f1310,f333]) ).
fof(f1315,plain,
index_255 = index_252,
inference(forward_demodulation,[status(thm)],[f491,f1313]) ).
fof(f1317,plain,
rselect_head(queue_257) = rselect_head(q8),
inference(paramodulation,[status(thm)],[f583,f337]) ).
fof(f1323,plain,
q9 = rstore_tail(queue_257,index_258),
inference(forward_demodulation,[status(thm)],[f654,f584]) ).
fof(f1324,plain,
rselect_head(q9) = rselect_head(queue_257),
inference(paramodulation,[status(thm)],[f1323,f336]) ).
fof(f1326,plain,
rselect_tail(q9) = index_258,
inference(paramodulation,[status(thm)],[f1323,f333]) ).
fof(f1328,plain,
index_9 = index_258,
inference(forward_demodulation,[status(thm)],[f519,f1326]) ).
fof(f1330,plain,
rselect_head(queue_29) = rselect_head(q12),
inference(paramodulation,[status(thm)],[f585,f337]) ).
fof(f1333,plain,
q13 = rstore_tail(queue_29,index_30),
inference(forward_demodulation,[status(thm)],[f616,f586]) ).
fof(f1334,plain,
rselect_head(q13) = rselect_head(queue_29),
inference(paramodulation,[status(thm)],[f1333,f336]) ).
fof(f1336,plain,
rselect_tail(q13) = index_30,
inference(paramodulation,[status(thm)],[f1333,f333]) ).
fof(f1338,plain,
index_33 = index_30,
inference(forward_demodulation,[status(thm)],[f499,f1336]) ).
fof(f1341,plain,
index_9 = s(index_255),
inference(backward_demodulation,[status(thm)],[f1328,f492]) ).
fof(f1343,plain,
rselect_head(queue_35) = rselect_head(q13),
inference(paramodulation,[status(thm)],[f587,f337]) ).
fof(f1348,plain,
index_33 = s(index_27),
inference(backward_demodulation,[status(thm)],[f1338,f498]) ).
fof(f1349,plain,
q14 = rstore_tail(queue_35,index_36),
inference(forward_demodulation,[status(thm)],[f617,f588]) ).
fof(f1350,plain,
rselect_head(q14) = rselect_head(queue_35),
inference(paramodulation,[status(thm)],[f1349,f336]) ).
fof(f1352,plain,
rselect_tail(q14) = index_36,
inference(paramodulation,[status(thm)],[f1349,f333]) ).
fof(f1354,plain,
index_39 = index_36,
inference(forward_demodulation,[status(thm)],[f501,f1352]) ).
fof(f1356,plain,
rselect_head(queue_41) = rselect_head(q14),
inference(paramodulation,[status(thm)],[f589,f337]) ).
fof(f1361,plain,
index_39 = s(index_33),
inference(backward_demodulation,[status(thm)],[f1354,f500]) ).
fof(f1362,plain,
q15 = rstore_tail(queue_41,index_42),
inference(forward_demodulation,[status(thm)],[f618,f590]) ).
fof(f1363,plain,
rselect_head(q15) = rselect_head(queue_41),
inference(paramodulation,[status(thm)],[f1362,f336]) ).
fof(f1365,plain,
rselect_tail(q15) = index_42,
inference(paramodulation,[status(thm)],[f1362,f333]) ).
fof(f1367,plain,
index_45 = index_42,
inference(forward_demodulation,[status(thm)],[f503,f1365]) ).
fof(f1369,plain,
rselect_head(queue_47) = rselect_head(q15),
inference(paramodulation,[status(thm)],[f591,f337]) ).
fof(f1372,plain,
q16 = rstore_tail(queue_47,index_48),
inference(forward_demodulation,[status(thm)],[f619,f592]) ).
fof(f1373,plain,
rselect_head(q16) = rselect_head(queue_47),
inference(paramodulation,[status(thm)],[f1372,f336]) ).
fof(f1375,plain,
rselect_tail(q16) = index_48,
inference(paramodulation,[status(thm)],[f1372,f333]) ).
fof(f1377,plain,
index_51 = index_48,
inference(forward_demodulation,[status(thm)],[f505,f1375]) ).
fof(f1380,plain,
index_45 = s(index_39),
inference(backward_demodulation,[status(thm)],[f1367,f502]) ).
fof(f1382,plain,
rselect_head(queue_5) = rselect_head(q0),
inference(paramodulation,[status(thm)],[f593,f337]) ).
fof(f1387,plain,
index_51 = s(index_45),
inference(backward_demodulation,[status(thm)],[f1377,f504]) ).
fof(f1389,plain,
rselect_head(queue_53) = rselect_head(q16),
inference(paramodulation,[status(thm)],[f594,f337]) ).
fof(f1392,plain,
q17 = rstore_tail(queue_53,index_54),
inference(forward_demodulation,[status(thm)],[f620,f595]) ).
fof(f1393,plain,
rselect_head(q17) = rselect_head(queue_53),
inference(paramodulation,[status(thm)],[f1392,f336]) ).
fof(f1395,plain,
rselect_tail(q17) = index_54,
inference(paramodulation,[status(thm)],[f1392,f333]) ).
fof(f1397,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f507,f1395]) ).
fof(f1400,plain,
index_57 = s(index_51),
inference(backward_demodulation,[status(thm)],[f1397,f506]) ).
fof(f1402,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(paramodulation,[status(thm)],[f596,f337]) ).
fof(f1405,plain,
q18 = rstore_tail(queue_59,index_60),
inference(forward_demodulation,[status(thm)],[f621,f597]) ).
fof(f1406,plain,
rselect_head(q18) = rselect_head(queue_59),
inference(paramodulation,[status(thm)],[f1405,f336]) ).
fof(f1408,plain,
rselect_tail(q18) = index_60,
inference(paramodulation,[status(thm)],[f1405,f333]) ).
fof(f1410,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f510,f1408]) ).
fof(f1412,plain,
rselect_head(queue_65) = rselect_head(q18),
inference(paramodulation,[status(thm)],[f598,f337]) ).
fof(f1417,plain,
index_63 = s(index_57),
inference(backward_demodulation,[status(thm)],[f1410,f509]) ).
fof(f1418,plain,
q19 = rstore_tail(queue_65,index_66),
inference(forward_demodulation,[status(thm)],[f622,f599]) ).
fof(f1419,plain,
rselect_head(q19) = rselect_head(queue_65),
inference(paramodulation,[status(thm)],[f1418,f336]) ).
fof(f1421,plain,
rselect_tail(q19) = index_66,
inference(paramodulation,[status(thm)],[f1418,f333]) ).
fof(f1423,plain,
index_75 = index_66,
inference(forward_demodulation,[status(thm)],[f514,f1421]) ).
fof(f1426,plain,
index_75 = s(index_63),
inference(backward_demodulation,[status(thm)],[f1423,f511]) ).
fof(f1427,plain,
q1 = rstore_tail(queue_5,index_6),
inference(forward_demodulation,[status(thm)],[f612,f600]) ).
fof(f1428,plain,
rselect_head(q1) = rselect_head(queue_5),
inference(paramodulation,[status(thm)],[f1427,f336]) ).
fof(f1430,plain,
rselect_tail(q1) = index_6,
inference(paramodulation,[status(thm)],[f1427,f333]) ).
fof(f1432,plain,
index_69 = index_6,
inference(forward_demodulation,[status(thm)],[f512,f1430]) ).
fof(f1434,plain,
rselect_head(queue_71) = rselect_head(q1),
inference(paramodulation,[status(thm)],[f601,f337]) ).
fof(f1439,plain,
index_69 = s(index_3),
inference(backward_demodulation,[status(thm)],[f1432,f508]) ).
fof(f1440,plain,
q2 = rstore_tail(queue_71,index_72),
inference(forward_demodulation,[status(thm)],[f623,f602]) ).
fof(f1441,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(paramodulation,[status(thm)],[f1440,f336]) ).
fof(f1443,plain,
rselect_tail(q2) = index_72,
inference(paramodulation,[status(thm)],[f1440,f333]) ).
fof(f1445,plain,
index_135 = index_72,
inference(forward_demodulation,[status(thm)],[f447,f1443]) ).
fof(f1447,plain,
rselect_head(queue_77) = rselect_head(q19),
inference(paramodulation,[status(thm)],[f603,f337]) ).
fof(f1450,plain,
q20 = rstore_tail(queue_77,index_78),
inference(forward_demodulation,[status(thm)],[f624,f604]) ).
fof(f1451,plain,
rselect_head(q20) = rselect_head(queue_77),
inference(paramodulation,[status(thm)],[f1450,f336]) ).
fof(f1453,plain,
rselect_tail(q20) = index_78,
inference(paramodulation,[status(thm)],[f1450,f333]) ).
fof(f1455,plain,
index_81 = index_78,
inference(forward_demodulation,[status(thm)],[f516,f1453]) ).
fof(f1458,plain,
index_135 = s(index_69),
inference(backward_demodulation,[status(thm)],[f1445,f513]) ).
fof(f1460,plain,
rselect_head(queue_83) = rselect_head(q20),
inference(paramodulation,[status(thm)],[f605,f337]) ).
fof(f1465,plain,
index_81 = s(index_75),
inference(backward_demodulation,[status(thm)],[f1455,f515]) ).
fof(f1466,plain,
q21 = rstore_tail(queue_83,index_84),
inference(forward_demodulation,[status(thm)],[f625,f606]) ).
fof(f1467,plain,
rselect_head(q21) = rselect_head(queue_83),
inference(paramodulation,[status(thm)],[f1466,f336]) ).
fof(f1469,plain,
rselect_tail(q21) = index_84,
inference(paramodulation,[status(thm)],[f1466,f333]) ).
fof(f1471,plain,
index_87 = index_84,
inference(forward_demodulation,[status(thm)],[f518,f1469]) ).
fof(f1473,plain,
rselect_head(queue_89) = rselect_head(q21),
inference(paramodulation,[status(thm)],[f607,f337]) ).
fof(f1478,plain,
index_87 = s(index_81),
inference(backward_demodulation,[status(thm)],[f1471,f517]) ).
fof(f1479,plain,
q22 = rstore_tail(queue_89,index_90),
inference(forward_demodulation,[status(thm)],[f626,f608]) ).
fof(f1480,plain,
rselect_head(q22) = rselect_head(queue_89),
inference(paramodulation,[status(thm)],[f1479,f336]) ).
fof(f1482,plain,
rselect_tail(q22) = index_90,
inference(paramodulation,[status(thm)],[f1479,f333]) ).
fof(f1484,plain,
index_93 = index_90,
inference(forward_demodulation,[status(thm)],[f521,f1482]) ).
fof(f1486,plain,
rselect_head(queue_95) = rselect_head(q22),
inference(paramodulation,[status(thm)],[f609,f337]) ).
fof(f1489,plain,
q23 = rstore_tail(queue_95,index_96),
inference(forward_demodulation,[status(thm)],[f627,f610]) ).
fof(f1490,plain,
rselect_head(q23) = rselect_head(queue_95),
inference(paramodulation,[status(thm)],[f1489,f336]) ).
fof(f1492,plain,
rselect_tail(q23) = index_96,
inference(paramodulation,[status(thm)],[f1489,f333]) ).
fof(f1494,plain,
index_99 = index_96,
inference(forward_demodulation,[status(thm)],[f523,f1492]) ).
fof(f1497,plain,
index_93 = s(index_87),
inference(backward_demodulation,[status(thm)],[f1484,f520]) ).
fof(f1504,plain,
index_99 = s(index_93),
inference(backward_demodulation,[status(thm)],[f1494,f522]) ).
fof(f1550,plain,
p(index_15) = index_9,
inference(forward_demodulation,[status(thm)],[f1014,f770]) ).
fof(f1719,plain,
p(index_21) = index_15,
inference(forward_demodulation,[status(thm)],[f1157,f814]) ).
fof(f1802,plain,
p(index_231) = index_201,
inference(forward_demodulation,[status(thm)],[f1196,f834]) ).
fof(f1884,plain,
s(s(index_9)) = index_255,
inference(paramodulation,[status(thm)],[f1341,f344]) ).
fof(f1888,plain,
s(index_15) = index_255,
inference(forward_demodulation,[status(thm)],[f1027,f1884]) ).
fof(f1889,plain,
index_21 = index_255,
inference(forward_demodulation,[status(thm)],[f1164,f1888]) ).
fof(f1899,plain,
index_9 = s(index_21),
inference(backward_demodulation,[status(thm)],[f1889,f1341]) ).
fof(f1904,plain,
index_21 = index_252,
inference(backward_demodulation,[status(thm)],[f1889,f1315]) ).
fof(f1920,plain,
p(index_237) = index_231,
inference(forward_demodulation,[status(thm)],[f1266,f854]) ).
fof(f1964,plain,
p(index_249) = index_243,
inference(forward_demodulation,[status(thm)],[f1293,f866]) ).
fof(f1982,plain,
p(index_21) = index_249,
inference(forward_demodulation,[status(thm)],[f1904,f870]) ).
fof(f1984,plain,
p(index_15) = index_243,
inference(backward_demodulation,[status(thm)],[f1994,f1964]) ).
fof(f1994,plain,
index_15 = index_249,
inference(forward_demodulation,[status(thm)],[f1719,f1982]) ).
fof(f1995,plain,
index_9 = index_243,
inference(forward_demodulation,[status(thm)],[f1550,f1984]) ).
fof(f2003,plain,
index_9 = s(index_237),
inference(backward_demodulation,[status(thm)],[f1995,f1282]) ).
fof(f2019,plain,
s(s(index_135)) = index_69,
inference(paramodulation,[status(thm)],[f1458,f344]) ).
fof(f2023,plain,
s(index_201) = index_69,
inference(forward_demodulation,[status(thm)],[f1047,f2019]) ).
fof(f2024,plain,
index_231 = index_69,
inference(forward_demodulation,[status(thm)],[f1203,f2023]) ).
fof(f2046,plain,
index_135 = s(index_231),
inference(backward_demodulation,[status(thm)],[f2024,f1458]) ).
fof(f2047,plain,
index_231 = s(index_3),
inference(backward_demodulation,[status(thm)],[f2024,f1439]) ).
fof(f2063,plain,
s(s(index_99)) = index_93,
inference(paramodulation,[status(thm)],[f1504,f344]) ).
fof(f2067,plain,
s(index_105) = index_93,
inference(forward_demodulation,[status(thm)],[f950,f2063]) ).
fof(f2068,plain,
index_111 = index_93,
inference(forward_demodulation,[status(thm)],[f968,f2067]) ).
fof(f2070,plain,
index_27 = index_9,
inference(backward_demodulation,[status(thm)],[f1899,f1309]) ).
fof(f2077,plain,
index_99 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2068,f1504]) ).
fof(f2078,plain,
index_111 = s(index_87),
inference(backward_demodulation,[status(thm)],[f2068,f1497]) ).
fof(f2092,plain,
index_33 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2070,f1348]) ).
fof(f2100,plain,
index_33 = index_15,
inference(forward_demodulation,[status(thm)],[f1027,f2092]) ).
fof(f2105,plain,
index_39 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2100,f1361]) ).
fof(f2108,plain,
index_15 = index_30,
inference(backward_demodulation,[status(thm)],[f2100,f1338]) ).
fof(f2111,plain,
index_39 = index_21,
inference(forward_demodulation,[status(thm)],[f1164,f2105]) ).
fof(f2119,plain,
index_45 = s(index_21),
inference(backward_demodulation,[status(thm)],[f2111,f1380]) ).
fof(f2125,plain,
index_45 = index_9,
inference(forward_demodulation,[status(thm)],[f1899,f2119]) ).
fof(f2127,plain,
s(s(index_9)) = index_237,
inference(paramodulation,[status(thm)],[f2003,f344]) ).
fof(f2131,plain,
s(index_15) = index_237,
inference(forward_demodulation,[status(thm)],[f1027,f2127]) ).
fof(f2132,plain,
index_21 = index_237,
inference(forward_demodulation,[status(thm)],[f1164,f2131]) ).
fof(f2138,plain,
index_51 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2125,f1387]) ).
fof(f2144,plain,
index_51 = index_15,
inference(forward_demodulation,[status(thm)],[f1027,f2138]) ).
fof(f2148,plain,
index_237 = index_135,
inference(backward_demodulation,[status(thm)],[f2046,f1269]) ).
fof(f2155,plain,
s(s(index_231)) = index_3,
inference(paramodulation,[status(thm)],[f2047,f344]) ).
fof(f2159,plain,
s(index_135) = index_3,
inference(forward_demodulation,[status(thm)],[f2046,f2155]) ).
fof(f2160,plain,
index_201 = index_3,
inference(forward_demodulation,[status(thm)],[f1047,f2159]) ).
fof(f2166,plain,
p(index_21) = index_231,
inference(backward_demodulation,[status(thm)],[f2132,f1920]) ).
fof(f2173,plain,
index_15 = index_231,
inference(forward_demodulation,[status(thm)],[f1719,f2166]) ).
fof(f2174,plain,
index_57 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2144,f1400]) ).
fof(f2180,plain,
index_57 = index_21,
inference(forward_demodulation,[status(thm)],[f1164,f2174]) ).
fof(f2188,plain,
index_117 = index_99,
inference(backward_demodulation,[status(thm)],[f2077,f986]) ).
fof(f2195,plain,
index_21 = index_135,
inference(backward_demodulation,[status(thm)],[f2148,f2132]) ).
fof(f2200,plain,
s(s(index_111)) = index_87,
inference(paramodulation,[status(thm)],[f2078,f344]) ).
fof(f2204,plain,
s(index_99) = index_87,
inference(forward_demodulation,[status(thm)],[f2077,f2200]) ).
fof(f2205,plain,
index_105 = index_87,
inference(forward_demodulation,[status(thm)],[f950,f2204]) ).
fof(f2216,plain,
index_135 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2173,f2046]) ).
fof(f2220,plain,
p(index_15) = index_201,
inference(backward_demodulation,[status(thm)],[f2173,f1802]) ).
fof(f2228,plain,
index_9 = index_201,
inference(forward_demodulation,[status(thm)],[f1550,f2220]) ).
fof(f2242,plain,
index_63 = s(index_21),
inference(backward_demodulation,[status(thm)],[f2180,f1417]) ).
fof(f2248,plain,
index_63 = index_9,
inference(forward_demodulation,[status(thm)],[f1899,f2242]) ).
fof(f2258,plain,
index_123 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2188,f995]) ).
fof(f2267,plain,
index_123 = index_105,
inference(forward_demodulation,[status(thm)],[f950,f2258]) ).
fof(f2278,plain,
index_9 = s(index_135),
inference(backward_demodulation,[status(thm)],[f2195,f1899]) ).
fof(f2291,plain,
index_105 = s(index_81),
inference(backward_demodulation,[status(thm)],[f2205,f1478]) ).
fof(f2313,plain,
index_9 = index_3,
inference(backward_demodulation,[status(thm)],[f2228,f2160]) ).
fof(f2329,plain,
index_75 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2248,f1426]) ).
fof(f2335,plain,
index_75 = index_15,
inference(forward_demodulation,[status(thm)],[f1027,f2329]) ).
fof(f2349,plain,
index_129 = s(index_105),
inference(backward_demodulation,[status(thm)],[f2267,f1008]) ).
fof(f2356,plain,
index_129 = index_111,
inference(forward_demodulation,[status(thm)],[f968,f2349]) ).
fof(f2394,plain,
index_81 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2335,f1465]) ).
fof(f2400,plain,
index_81 = index_135,
inference(forward_demodulation,[status(thm)],[f2216,f2394]) ).
fof(f2419,plain,
index_141 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2356,f1034]) ).
fof(f2425,plain,
index_141 = index_99,
inference(forward_demodulation,[status(thm)],[f2077,f2419]) ).
fof(f2441,plain,
index_105 = s(index_135),
inference(backward_demodulation,[status(thm)],[f2400,f2291]) ).
fof(f2447,plain,
index_105 = index_9,
inference(forward_demodulation,[status(thm)],[f2278,f2441]) ).
fof(f2458,plain,
index_147 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2425,f1066]) ).
fof(f2464,plain,
index_147 = index_105,
inference(forward_demodulation,[status(thm)],[f950,f2458]) ).
fof(f2488,plain,
index_111 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2447,f968]) ).
fof(f2490,plain,
index_9 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2447,f950]) ).
fof(f2506,plain,
index_153 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2512,f1073]) ).
fof(f2512,plain,
index_147 = index_9,
inference(forward_demodulation,[status(thm)],[f2447,f2464]) ).
fof(f2585,plain,
index_15 = index_111,
inference(backward_demodulation,[status(thm)],[f2488,f1027]) ).
fof(f2608,plain,
index_159 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2614,f1086]) ).
fof(f2614,plain,
index_153 = index_111,
inference(forward_demodulation,[status(thm)],[f2488,f2506]) ).
fof(f2615,plain,
index_159 = index_99,
inference(forward_demodulation,[status(thm)],[f2077,f2608]) ).
fof(f2656,plain,
index_111 = index_30,
inference(backward_demodulation,[status(thm)],[f2585,f2108]) ).
fof(f2672,plain,
index_165 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2615,f1105]) ).
fof(f2678,plain,
index_165 = index_9,
inference(forward_demodulation,[status(thm)],[f2490,f2672]) ).
fof(f2716,plain,
index_171 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2678,f1112]) ).
fof(f2722,plain,
index_171 = index_111,
inference(forward_demodulation,[status(thm)],[f2488,f2716]) ).
fof(f2735,plain,
index_177 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2722,f1125]) ).
fof(f2741,plain,
index_177 = index_99,
inference(forward_demodulation,[status(thm)],[f2077,f2735]) ).
fof(f2756,plain,
index_183 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2741,f1142]) ).
fof(f2762,plain,
index_183 = index_9,
inference(forward_demodulation,[status(thm)],[f2490,f2756]) ).
fof(f2773,plain,
index_189 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2762,f1151]) ).
fof(f2779,plain,
index_189 = index_111,
inference(forward_demodulation,[status(thm)],[f2488,f2773]) ).
fof(f2792,plain,
index_195 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2779,f1183]) ).
fof(f2798,plain,
index_195 = index_99,
inference(forward_demodulation,[status(thm)],[f2077,f2792]) ).
fof(f2813,plain,
index_207 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2798,f1190]) ).
fof(f2819,plain,
index_207 = index_9,
inference(forward_demodulation,[status(thm)],[f2490,f2813]) ).
fof(f2830,plain,
index_213 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2819,f1222]) ).
fof(f2836,plain,
index_213 = index_111,
inference(forward_demodulation,[status(thm)],[f2488,f2830]) ).
fof(f2851,plain,
index_219 = s(index_111),
inference(backward_demodulation,[status(thm)],[f2836,f1229]) ).
fof(f2857,plain,
index_219 = index_99,
inference(forward_demodulation,[status(thm)],[f2077,f2851]) ).
fof(f2870,plain,
index_225 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2857,f1242]) ).
fof(f2876,plain,
index_225 = index_9,
inference(forward_demodulation,[status(thm)],[f2490,f2870]) ).
fof(f2890,plain,
index_228 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2876,f481]) ).
fof(f2893,plain,
index_228 = index_111,
inference(forward_demodulation,[status(thm)],[f2488,f2890]) ).
fof(f2937,plain,
p(index_111) = index_27,
inference(forward_demodulation,[status(thm)],[f2656,f882]) ).
fof(f2938,plain,
p(index_111) = index_9,
inference(forward_demodulation,[status(thm)],[f2070,f2937]) ).
fof(f3091,plain,
index_0 = index_9,
inference(backward_demodulation,[status(thm)],[f3092,f434]) ).
fof(f3092,plain,
index_9 = rselect_tail(q),
inference(forward_demodulation,[status(thm)],[f2313,f936]) ).
fof(f3116,plain,
rselect_head(q0) = index_9,
inference(forward_demodulation,[status(thm)],[f3091,f935]) ).
fof(f3402,plain,
index_263 = index_111,
inference(backward_demodulation,[status(thm)],[f3403,f494]) ).
fof(f3403,plain,
rselect_tail(q43) = index_111,
inference(forward_demodulation,[status(thm)],[f2893,f1246]) ).
fof(f3404,plain,
p(index_111) = index_264,
inference(backward_demodulation,[status(thm)],[f3402,f878]) ).
fof(f3408,plain,
index_9 = index_264,
inference(forward_demodulation,[status(thm)],[f2938,f3404]) ).
fof(f3423,plain,
elem_265 = select(earray_260,index_9),
inference(backward_demodulation,[status(thm)],[f3408,f433]) ).
fof(f4029,plain,
rselect_head(q24) = rselect_head(q23),
inference(backward_demodulation,[status(thm)],[f943,f939]) ).
fof(f4035,plain,
rselect_head(q25) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f952,f957]) ).
fof(f4042,plain,
rselect_head(queue_113) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4035,f971]) ).
fof(f4043,plain,
rselect_head(q26) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4042,f975]) ).
fof(f4044,plain,
rselect_head(queue_119) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4043,f981]) ).
fof(f4046,plain,
rselect_head(q27) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4044,f988]) ).
fof(f4052,plain,
rselect_head(queue_125) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4046,f997]) ).
fof(f4053,plain,
rselect_head(q28) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4052,f1001]) ).
fof(f4060,plain,
rselect_head(q10) = rselect_head(q9),
inference(backward_demodulation,[status(thm)],[f1010,f963]) ).
fof(f4061,plain,
rselect_head(queue_131) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4053,f1016]) ).
fof(f4062,plain,
rselect_head(q29) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4061,f1020]) ).
fof(f4069,plain,
rselect_head(q3) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f1029,f1036]) ).
fof(f4070,plain,
rselect_head(queue_143) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4062,f1042]) ).
fof(f4077,plain,
rselect_head(q30) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4070,f1049]) ).
fof(f4078,plain,
rselect_head(queue_149) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4077,f1055]) ).
fof(f4079,plain,
rselect_head(q31) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4078,f1059]) ).
fof(f4080,plain,
rselect_head(queue_155) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4079,f1068]) ).
fof(f4083,plain,
rselect_head(q32) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4080,f1075]) ).
fof(f4084,plain,
rselect_head(queue_161) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4083,f1081]) ).
fof(f4091,plain,
rselect_head(q33) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4084,f1088]) ).
fof(f4092,plain,
rselect_head(queue_167) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4091,f1094]) ).
fof(f4093,plain,
rselect_head(q34) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4092,f1098]) ).
fof(f4100,plain,
rselect_head(queue_173) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4093,f1114]) ).
fof(f4101,plain,
rselect_head(q35) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4100,f1118]) ).
fof(f4108,plain,
rselect_head(queue_179) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4101,f1127]) ).
fof(f4109,plain,
rselect_head(q36) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4108,f1131]) ).
fof(f4110,plain,
rselect_head(queue_185) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4109,f1137]) ).
fof(f4114,plain,
rselect_head(q37) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4110,f1144]) ).
fof(f4118,plain,
rselect_head(q11) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f1107,f1153]) ).
fof(f4119,plain,
rselect_head(queue_191) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4114,f1159]) ).
fof(f4126,plain,
rselect_head(q38) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4119,f1166]) ).
fof(f4127,plain,
rselect_head(queue_197) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4126,f1172]) ).
fof(f4128,plain,
rselect_head(q39) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4127,f1176]) ).
fof(f4132,plain,
rselect_head(queue_203) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4069,f1185]) ).
fof(f4136,plain,
rselect_head(q4) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4132,f1192]) ).
fof(f4137,plain,
rselect_head(queue_209) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4128,f1198]) ).
fof(f4144,plain,
rselect_head(q40) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4137,f1205]) ).
fof(f4145,plain,
rselect_head(queue_215) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4144,f1211]) ).
fof(f4146,plain,
rselect_head(q41) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4145,f1215]) ).
fof(f4148,plain,
rselect_head(queue_221) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4146,f1224]) ).
fof(f4154,plain,
rselect_head(q42) = rselect_head(q24),
inference(forward_demodulation,[status(thm)],[f4148,f1231]) ).
fof(f4155,plain,
index_261 = rselect_head(q24),
inference(backward_demodulation,[status(thm)],[f4156,f4154]) ).
fof(f4156,plain,
index_261 = rselect_head(q42),
inference(forward_demodulation,[status(thm)],[f1247,f1237]) ).
fof(f4160,plain,
rselect_head(queue_23) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4118,f1250]) ).
fof(f4161,plain,
rselect_head(queue_233) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4136,f1254]) ).
fof(f4162,plain,
rselect_head(q5) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4161,f1262]) ).
fof(f4166,plain,
rselect_head(queue_239) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4162,f1271]) ).
fof(f4170,plain,
rselect_head(q6) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4166,f1275]) ).
fof(f4171,plain,
rselect_head(queue_245) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4170,f1285]) ).
fof(f4178,plain,
rselect_head(q7) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4171,f1289]) ).
fof(f4179,plain,
rselect_head(q12) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4160,f1295]) ).
fof(f4180,plain,
rselect_head(queue_251) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4178,f1304]) ).
fof(f4184,plain,
rselect_head(q8) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4180,f1311]) ).
fof(f4187,plain,
rselect_head(queue_257) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4184,f1317]) ).
fof(f4188,plain,
rselect_head(q9) = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f4187,f1324]) ).
fof(f4192,plain,
rselect_head(queue_29) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4179,f1330]) ).
fof(f4193,plain,
rselect_head(q13) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4192,f1334]) ).
fof(f4194,plain,
rselect_head(queue_35) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4193,f1343]) ).
fof(f4196,plain,
rselect_head(q14) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4194,f1350]) ).
fof(f4199,plain,
rselect_head(queue_41) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4196,f1356]) ).
fof(f4200,plain,
rselect_head(q15) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4199,f1363]) ).
fof(f4204,plain,
rselect_head(queue_47) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4200,f1369]) ).
fof(f4205,plain,
rselect_head(q16) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4204,f1373]) ).
fof(f4206,plain,
rselect_head(queue_5) = index_9,
inference(forward_demodulation,[status(thm)],[f3116,f1382]) ).
fof(f4207,plain,
rselect_head(queue_53) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4205,f1389]) ).
fof(f4211,plain,
rselect_head(q17) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4207,f1393]) ).
fof(f4212,plain,
rselect_head(queue_59) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4211,f1402]) ).
fof(f4215,plain,
rselect_head(q18) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4212,f1406]) ).
fof(f4216,plain,
rselect_head(queue_65) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4215,f1412]) ).
fof(f4217,plain,
rselect_head(q19) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4216,f1419]) ).
fof(f4218,plain,
rselect_head(q1) = index_9,
inference(forward_demodulation,[status(thm)],[f4206,f1428]) ).
fof(f4220,plain,
rselect_head(queue_71) = index_9,
inference(forward_demodulation,[status(thm)],[f4218,f1434]) ).
fof(f4221,plain,
rselect_head(q9) = index_9,
inference(backward_demodulation,[status(thm)],[f4235,f4188]) ).
fof(f4235,plain,
rselect_head(q2) = index_9,
inference(forward_demodulation,[status(thm)],[f4220,f1441]) ).
fof(f4239,plain,
rselect_head(queue_77) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4217,f1447]) ).
fof(f4240,plain,
rselect_head(q20) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4239,f1451]) ).
fof(f4241,plain,
rselect_head(queue_83) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4240,f1460]) ).
fof(f4243,plain,
rselect_head(q21) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4241,f1467]) ).
fof(f4245,plain,
rselect_head(queue_89) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4243,f1473]) ).
fof(f4246,plain,
rselect_head(q22) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4245,f1480]) ).
fof(f4250,plain,
rselect_head(queue_95) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4246,f1486]) ).
fof(f4251,plain,
rselect_head(q23) = rselect_head(q10),
inference(forward_demodulation,[status(thm)],[f4250,f1490]) ).
fof(f4833,plain,
index_261 = rselect_head(q10),
inference(backward_demodulation,[status(thm)],[f4834,f4251]) ).
fof(f4834,plain,
index_261 = rselect_head(q23),
inference(forward_demodulation,[status(thm)],[f4155,f4029]) ).
fof(f4864,plain,
index_261 = rselect_head(q9),
inference(forward_demodulation,[status(thm)],[f4833,f4060]) ).
fof(f4927,plain,
elem_262 = select(earray_260,index_9),
inference(backward_demodulation,[status(thm)],[f4928,f432]) ).
fof(f4928,plain,
index_261 = index_9,
inference(forward_demodulation,[status(thm)],[f4221,f4864]) ).
fof(f4929,plain,
elem_265 = elem_262,
inference(backward_demodulation,[status(thm)],[f4927,f3423]) ).
fof(f4930,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4929,f655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:13:39 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 1.03/0.57 % Refutation found
% 1.03/0.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.03/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.03/0.61 % Elapsed time: 0.217960 seconds
% 1.03/0.61 % CPU time: 1.404551 seconds
% 1.03/0.61 % Total memory used: 139.079 MB
% 1.03/0.61 % Net memory used: 138.041 MB
%------------------------------------------------------------------------------