%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:52:50 PM UTC 2026
% Result : Unsatisfiable 0.23s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.49 % Computer : n002.cluster.edu
% 0.19/0.49 % Model : x86_64 x86_64
% 0.19/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.49 % Memory : 8046.5625MB
% 0.19/0.49 % OS : Linux 6.8.0-71-generic
% 0.19/0.49 % CPULimit : 300
% 0.19/0.50 % WCLimit : 300
% 0.19/0.50 % DateTime : Mon Sep 21 09:13:35 UTC 2026
% 0.19/0.50 % CPUTime :
% 0.19/0.55 % Drodi V4.1.1
% 0.23/0.85 % Refutation found
% 0.23/0.85 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/0.85 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.85 fof(f1,axiom,(
% 0.23/0.85 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f3,axiom,(
% 0.23/0.85 (![A,E]: (rselect_seq(rstore_seq(A,E)) = E ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f4,axiom,(
% 0.23/0.85 (![A,E]: (rselect_head(rstore_head(A,E)) = E ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f5,axiom,(
% 0.23/0.85 (![A,E]: (rselect_tail(rstore_tail(A,E)) = E ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f7,axiom,(
% 0.23/0.85 (![A,E]: (rselect_seq(rstore_tail(A,E)) = rselect_seq(A) ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f8,axiom,(
% 0.23/0.85 (![A,E]: (rselect_head(rstore_tail(A,E)) = rselect_head(A) ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f9,axiom,(
% 0.23/0.85 (![A,E]: (rselect_head(rstore_seq(A,E)) = rselect_head(A) ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f11,axiom,(
% 0.23/0.85 (![A,E]: (rselect_tail(rstore_head(A,E)) = rselect_tail(A) ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f12,axiom,(
% 0.23/0.85 (![X]: (p(s(X)) = X ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f13,axiom,(
% 0.23/0.85 (![X]: (s(p(X)) = X ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f16,axiom,(
% 0.23/0.85 (![X]: (s(s(s(X))) = X ))),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f71,hypothesis,(
% 0.23/0.85 earray_244 = store(earray_242,index_243,e45) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f83,hypothesis,(
% 0.23/0.85 earray_278 = rselect_seq(q46) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f110,hypothesis,(
% 0.23/0.85 elem_280 = select(earray_278,index_279) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f111,hypothesis,(
% 0.23/0.85 elem_283 = select(earray_278,index_282) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f112,hypothesis,(
% 0.23/0.85 index_0 = rselect_tail(q) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f113,hypothesis,(
% 0.23/0.85 index_102 = s(index_99) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f114,hypothesis,(
% 0.23/0.85 index_105 = rselect_tail(q24) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f115,hypothesis,(
% 0.23/0.85 index_108 = s(index_105) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f116,hypothesis,(
% 0.23/0.85 index_111 = rselect_tail(q25) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f117,hypothesis,(
% 0.23/0.85 index_114 = s(index_111) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f118,hypothesis,(
% 0.23/0.85 index_117 = rselect_tail(q26) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f119,hypothesis,(
% 0.23/0.85 index_12 = s(index_9) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f120,hypothesis,(
% 0.23/0.85 index_120 = s(index_117) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f121,hypothesis,(
% 0.23/0.85 index_123 = rselect_tail(q27) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f122,hypothesis,(
% 0.23/0.85 index_126 = s(index_123) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f123,hypothesis,(
% 0.23/0.85 index_129 = rselect_tail(q28) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f124,hypothesis,(
% 0.23/0.85 index_132 = s(index_129) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f125,hypothesis,(
% 0.23/0.85 index_135 = rselect_tail(q2) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f126,hypothesis,(
% 0.23/0.85 index_138 = s(index_135) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f127,hypothesis,(
% 0.23/0.85 index_141 = rselect_tail(q29) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f128,hypothesis,(
% 0.23/0.85 index_144 = s(index_141) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f129,hypothesis,(
% 0.23/0.85 index_147 = rselect_tail(q30) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f130,hypothesis,(
% 0.23/0.85 index_15 = rselect_tail(q10) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f131,hypothesis,(
% 0.23/0.85 index_150 = s(index_147) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f132,hypothesis,(
% 0.23/0.85 index_153 = rselect_tail(q31) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f133,hypothesis,(
% 0.23/0.85 index_156 = s(index_153) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f134,hypothesis,(
% 0.23/0.85 index_159 = rselect_tail(q32) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f135,hypothesis,(
% 0.23/0.85 index_162 = s(index_159) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f136,hypothesis,(
% 0.23/0.85 index_165 = rselect_tail(q33) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f137,hypothesis,(
% 0.23/0.85 index_168 = s(index_165) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f138,hypothesis,(
% 0.23/0.85 index_171 = rselect_tail(q34) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f139,hypothesis,(
% 0.23/0.85 index_174 = s(index_171) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f140,hypothesis,(
% 0.23/0.85 index_177 = rselect_tail(q35) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f141,hypothesis,(
% 0.23/0.85 index_18 = s(index_15) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f142,hypothesis,(
% 0.23/0.85 index_180 = s(index_177) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f143,hypothesis,(
% 0.23/0.85 index_183 = rselect_tail(q36) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f144,hypothesis,(
% 0.23/0.85 index_186 = s(index_183) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f145,hypothesis,(
% 0.23/0.85 index_189 = rselect_tail(q37) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f146,hypothesis,(
% 0.23/0.85 index_192 = s(index_189) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f147,hypothesis,(
% 0.23/0.85 index_195 = rselect_tail(q38) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f148,hypothesis,(
% 0.23/0.85 index_198 = s(index_195) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f149,hypothesis,(
% 0.23/0.85 index_201 = rselect_tail(q3) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f150,hypothesis,(
% 0.23/0.85 index_204 = s(index_201) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f151,hypothesis,(
% 0.23/0.85 index_207 = rselect_tail(q39) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f152,hypothesis,(
% 0.23/0.85 index_21 = rselect_tail(q11) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f153,hypothesis,(
% 0.23/0.85 index_210 = s(index_207) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f154,hypothesis,(
% 0.23/0.85 index_213 = rselect_tail(q40) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f155,hypothesis,(
% 0.23/0.85 index_216 = s(index_213) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f156,hypothesis,(
% 0.23/0.85 index_219 = rselect_tail(q41) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f157,hypothesis,(
% 0.23/0.85 index_222 = s(index_219) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f158,hypothesis,(
% 0.23/0.85 index_225 = rselect_tail(q42) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f159,hypothesis,(
% 0.23/0.85 index_228 = s(index_225) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f160,hypothesis,(
% 0.23/0.85 index_231 = rselect_tail(q43) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f161,hypothesis,(
% 0.23/0.85 index_234 = s(index_231) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f162,hypothesis,(
% 0.23/0.85 index_237 = rselect_tail(q44) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f163,hypothesis,(
% 0.23/0.85 index_24 = s(index_21) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f164,hypothesis,(
% 0.23/0.85 index_240 = s(index_237) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f165,hypothesis,(
% 0.23/0.85 index_243 = rselect_tail(q45) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f166,hypothesis,(
% 0.23/0.85 index_246 = s(index_243) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f167,hypothesis,(
% 0.23/0.85 index_249 = rselect_tail(q4) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f168,hypothesis,(
% 0.23/0.85 index_252 = s(index_249) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f169,hypothesis,(
% 0.23/0.85 index_255 = rselect_tail(q5) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f170,hypothesis,(
% 0.23/0.85 index_258 = s(index_255) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f171,hypothesis,(
% 0.23/0.85 index_261 = rselect_tail(q6) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f172,hypothesis,(
% 0.23/0.85 index_264 = s(index_261) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f173,hypothesis,(
% 0.23/0.85 index_267 = rselect_tail(q7) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f174,hypothesis,(
% 0.23/0.85 index_27 = rselect_tail(q12) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f175,hypothesis,(
% 0.23/0.85 index_270 = s(index_267) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f176,hypothesis,(
% 0.23/0.85 index_273 = rselect_tail(q8) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f177,hypothesis,(
% 0.23/0.85 index_276 = s(index_273) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f178,hypothesis,(
% 0.23/0.85 index_279 = rselect_head(q46) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f179,hypothesis,(
% 0.23/0.85 index_281 = rselect_tail(q46) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f180,hypothesis,(
% 0.23/0.85 s(index_282) = index_281 ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f181,hypothesis,(
% 0.23/0.85 index_3 = rselect_tail(q0) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f182,hypothesis,(
% 0.23/0.85 index_30 = s(index_27) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f183,hypothesis,(
% 0.23/0.85 index_33 = rselect_tail(q13) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f184,hypothesis,(
% 0.23/0.85 index_36 = s(index_33) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f185,hypothesis,(
% 0.23/0.85 index_39 = rselect_tail(q14) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f186,hypothesis,(
% 0.23/0.85 index_42 = s(index_39) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f187,hypothesis,(
% 0.23/0.85 index_45 = rselect_tail(q15) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f188,hypothesis,(
% 0.23/0.85 index_48 = s(index_45) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f189,hypothesis,(
% 0.23/0.85 index_51 = rselect_tail(q16) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f190,hypothesis,(
% 0.23/0.85 index_54 = s(index_51) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f191,hypothesis,(
% 0.23/0.85 index_57 = rselect_tail(q17) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f192,hypothesis,(
% 0.23/0.85 index_6 = s(index_3) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f193,hypothesis,(
% 0.23/0.85 index_60 = s(index_57) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f194,hypothesis,(
% 0.23/0.85 index_63 = rselect_tail(q18) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f195,hypothesis,(
% 0.23/0.85 index_66 = s(index_63) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f196,hypothesis,(
% 0.23/0.85 index_69 = rselect_tail(q1) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f197,hypothesis,(
% 0.23/0.85 index_72 = s(index_69) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f198,hypothesis,(
% 0.23/0.85 index_75 = rselect_tail(q19) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f199,hypothesis,(
% 0.23/0.85 index_78 = s(index_75) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f200,hypothesis,(
% 0.23/0.85 index_81 = rselect_tail(q20) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f201,hypothesis,(
% 0.23/0.85 index_84 = s(index_81) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f202,hypothesis,(
% 0.23/0.85 index_87 = rselect_tail(q21) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f203,hypothesis,(
% 0.23/0.85 index_9 = rselect_tail(q9) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f204,hypothesis,(
% 0.23/0.85 index_90 = s(index_87) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f205,hypothesis,(
% 0.23/0.85 index_93 = rselect_tail(q22) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f206,hypothesis,(
% 0.23/0.85 index_96 = s(index_93) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f207,hypothesis,(
% 0.23/0.85 index_99 = rselect_tail(q23) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f208,hypothesis,(
% 0.23/0.85 queue_1 = rstore_head(q,index_0) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f209,hypothesis,(
% 0.23/0.85 queue_101 = rstore_seq(q23,earray_100) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f210,hypothesis,(
% 0.23/0.85 queue_103 = rstore_tail(queue_101,index_102) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f211,hypothesis,(
% 0.23/0.85 queue_107 = rstore_seq(q24,earray_106) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f212,hypothesis,(
% 0.23/0.85 queue_109 = rstore_tail(queue_107,index_108) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f213,hypothesis,(
% 0.23/0.85 queue_11 = rstore_seq(q9,earray_10) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f214,hypothesis,(
% 0.23/0.85 queue_113 = rstore_seq(q25,earray_112) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f215,hypothesis,(
% 0.23/0.85 queue_115 = rstore_tail(queue_113,index_114) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f216,hypothesis,(
% 0.23/0.85 queue_119 = rstore_seq(q26,earray_118) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f217,hypothesis,(
% 0.23/0.85 queue_121 = rstore_tail(queue_119,index_120) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f218,hypothesis,(
% 0.23/0.85 queue_125 = rstore_seq(q27,earray_124) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f219,hypothesis,(
% 0.23/0.85 queue_127 = rstore_tail(queue_125,index_126) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f220,hypothesis,(
% 0.23/0.85 queue_13 = rstore_tail(queue_11,index_12) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f221,hypothesis,(
% 0.23/0.85 queue_131 = rstore_seq(q28,earray_130) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f222,hypothesis,(
% 0.23/0.85 queue_133 = rstore_tail(queue_131,index_132) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f223,hypothesis,(
% 0.23/0.85 queue_137 = rstore_seq(q2,earray_136) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f224,hypothesis,(
% 0.23/0.85 queue_139 = rstore_tail(queue_137,index_138) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f225,hypothesis,(
% 0.23/0.85 queue_143 = rstore_seq(q29,earray_142) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f226,hypothesis,(
% 0.23/0.85 queue_145 = rstore_tail(queue_143,index_144) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f227,hypothesis,(
% 0.23/0.85 queue_149 = rstore_seq(q30,earray_148) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f228,hypothesis,(
% 0.23/0.85 queue_151 = rstore_tail(queue_149,index_150) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f229,hypothesis,(
% 0.23/0.85 queue_155 = rstore_seq(q31,earray_154) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f230,hypothesis,(
% 0.23/0.85 queue_157 = rstore_tail(queue_155,index_156) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f231,hypothesis,(
% 0.23/0.85 queue_161 = rstore_seq(q32,earray_160) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f232,hypothesis,(
% 0.23/0.85 queue_163 = rstore_tail(queue_161,index_162) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f233,hypothesis,(
% 0.23/0.85 queue_167 = rstore_seq(q33,earray_166) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f234,hypothesis,(
% 0.23/0.85 queue_169 = rstore_tail(queue_167,index_168) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f235,hypothesis,(
% 0.23/0.85 queue_17 = rstore_seq(q10,earray_16) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f236,hypothesis,(
% 0.23/0.85 queue_173 = rstore_seq(q34,earray_172) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f237,hypothesis,(
% 0.23/0.85 queue_175 = rstore_tail(queue_173,index_174) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f238,hypothesis,(
% 0.23/0.85 queue_179 = rstore_seq(q35,earray_178) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f239,hypothesis,(
% 0.23/0.85 queue_181 = rstore_tail(queue_179,index_180) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f240,hypothesis,(
% 0.23/0.85 queue_185 = rstore_seq(q36,earray_184) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f241,hypothesis,(
% 0.23/0.85 queue_187 = rstore_tail(queue_185,index_186) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f242,hypothesis,(
% 0.23/0.85 queue_19 = rstore_tail(queue_17,index_18) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f243,hypothesis,(
% 0.23/0.85 queue_191 = rstore_seq(q37,earray_190) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f244,hypothesis,(
% 0.23/0.85 queue_193 = rstore_tail(queue_191,index_192) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f245,hypothesis,(
% 0.23/0.85 queue_197 = rstore_seq(q38,earray_196) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f246,hypothesis,(
% 0.23/0.85 queue_199 = rstore_tail(queue_197,index_198) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f247,hypothesis,(
% 0.23/0.85 queue_203 = rstore_seq(q3,earray_202) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f248,hypothesis,(
% 0.23/0.85 queue_205 = rstore_tail(queue_203,index_204) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f249,hypothesis,(
% 0.23/0.85 queue_209 = rstore_seq(q39,earray_208) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f250,hypothesis,(
% 0.23/0.85 queue_211 = rstore_tail(queue_209,index_210) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f251,hypothesis,(
% 0.23/0.85 queue_215 = rstore_seq(q40,earray_214) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f252,hypothesis,(
% 0.23/0.85 queue_217 = rstore_tail(queue_215,index_216) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f253,hypothesis,(
% 0.23/0.85 queue_221 = rstore_seq(q41,earray_220) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f254,hypothesis,(
% 0.23/0.85 queue_223 = rstore_tail(queue_221,index_222) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f255,hypothesis,(
% 0.23/0.85 queue_227 = rstore_seq(q42,earray_226) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f256,hypothesis,(
% 0.23/0.85 queue_229 = rstore_tail(queue_227,index_228) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f257,hypothesis,(
% 0.23/0.85 queue_23 = rstore_seq(q11,earray_22) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f258,hypothesis,(
% 0.23/0.85 queue_233 = rstore_seq(q43,earray_232) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f259,hypothesis,(
% 0.23/0.85 queue_235 = rstore_tail(queue_233,index_234) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f260,hypothesis,(
% 0.23/0.85 queue_239 = rstore_seq(q44,earray_238) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f261,hypothesis,(
% 0.23/0.85 queue_241 = rstore_tail(queue_239,index_240) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f262,hypothesis,(
% 0.23/0.85 queue_245 = rstore_seq(q45,earray_244) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f263,hypothesis,(
% 0.23/0.85 queue_247 = rstore_tail(queue_245,index_246) ),
% 0.23/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.85 fof(f264,hypothesis,(
% 0.23/0.86 queue_25 = rstore_tail(queue_23,index_24) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f265,hypothesis,(
% 0.23/0.86 queue_251 = rstore_seq(q4,earray_250) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f266,hypothesis,(
% 0.23/0.86 queue_253 = rstore_tail(queue_251,index_252) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f267,hypothesis,(
% 0.23/0.86 queue_257 = rstore_seq(q5,earray_256) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f268,hypothesis,(
% 0.23/0.86 queue_259 = rstore_tail(queue_257,index_258) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f269,hypothesis,(
% 0.23/0.86 queue_263 = rstore_seq(q6,earray_262) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f270,hypothesis,(
% 0.23/0.86 queue_265 = rstore_tail(queue_263,index_264) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f271,hypothesis,(
% 0.23/0.86 queue_269 = rstore_seq(q7,earray_268) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f272,hypothesis,(
% 0.23/0.86 queue_271 = rstore_tail(queue_269,index_270) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f273,hypothesis,(
% 0.23/0.86 queue_275 = rstore_seq(q8,earray_274) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f274,hypothesis,(
% 0.23/0.86 queue_277 = rstore_tail(queue_275,index_276) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f275,hypothesis,(
% 0.23/0.86 queue_29 = rstore_seq(q12,earray_28) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f276,hypothesis,(
% 0.23/0.86 queue_31 = rstore_tail(queue_29,index_30) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f277,hypothesis,(
% 0.23/0.86 queue_35 = rstore_seq(q13,earray_34) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f278,hypothesis,(
% 0.23/0.86 queue_37 = rstore_tail(queue_35,index_36) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f279,hypothesis,(
% 0.23/0.86 queue_41 = rstore_seq(q14,earray_40) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f280,hypothesis,(
% 0.23/0.86 queue_43 = rstore_tail(queue_41,index_42) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f281,hypothesis,(
% 0.23/0.86 queue_47 = rstore_seq(q15,earray_46) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f282,hypothesis,(
% 0.23/0.86 queue_49 = rstore_tail(queue_47,index_48) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f283,hypothesis,(
% 0.23/0.86 queue_5 = rstore_seq(q0,earray_4) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f284,hypothesis,(
% 0.23/0.86 queue_53 = rstore_seq(q16,earray_52) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f285,hypothesis,(
% 0.23/0.86 queue_55 = rstore_tail(queue_53,index_54) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f286,hypothesis,(
% 0.23/0.86 queue_59 = rstore_seq(q17,earray_58) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f287,hypothesis,(
% 0.23/0.86 queue_61 = rstore_tail(queue_59,index_60) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f288,hypothesis,(
% 0.23/0.86 queue_65 = rstore_seq(q18,earray_64) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f289,hypothesis,(
% 0.23/0.86 queue_67 = rstore_tail(queue_65,index_66) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f290,hypothesis,(
% 0.23/0.86 queue_7 = rstore_tail(queue_5,index_6) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f291,hypothesis,(
% 0.23/0.86 queue_71 = rstore_seq(q1,earray_70) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f292,hypothesis,(
% 0.23/0.86 queue_73 = rstore_tail(queue_71,index_72) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f293,hypothesis,(
% 0.23/0.86 queue_77 = rstore_seq(q19,earray_76) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f294,hypothesis,(
% 0.23/0.86 queue_79 = rstore_tail(queue_77,index_78) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f295,hypothesis,(
% 0.23/0.86 queue_83 = rstore_seq(q20,earray_82) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f296,hypothesis,(
% 0.23/0.86 queue_85 = rstore_tail(queue_83,index_84) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f297,hypothesis,(
% 0.23/0.86 queue_89 = rstore_seq(q21,earray_88) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f298,hypothesis,(
% 0.23/0.86 queue_91 = rstore_tail(queue_89,index_90) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f299,hypothesis,(
% 0.23/0.86 queue_95 = rstore_seq(q22,earray_94) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f300,hypothesis,(
% 0.23/0.86 queue_97 = rstore_tail(queue_95,index_96) ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f301,hypothesis,(
% 0.23/0.86 q0 = queue_1 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f302,hypothesis,(
% 0.23/0.86 q1 = queue_7 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f303,hypothesis,(
% 0.23/0.86 q10 = queue_13 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f304,hypothesis,(
% 0.23/0.86 q11 = queue_19 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f305,hypothesis,(
% 0.23/0.86 q12 = queue_25 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f306,hypothesis,(
% 0.23/0.86 q13 = queue_31 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f307,hypothesis,(
% 0.23/0.86 q14 = queue_37 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f308,hypothesis,(
% 0.23/0.86 q15 = queue_43 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f309,hypothesis,(
% 0.23/0.86 q16 = queue_49 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f310,hypothesis,(
% 0.23/0.86 q17 = queue_55 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f311,hypothesis,(
% 0.23/0.86 q18 = queue_61 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f312,hypothesis,(
% 0.23/0.86 q19 = queue_67 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f313,hypothesis,(
% 0.23/0.86 q2 = queue_73 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f314,hypothesis,(
% 0.23/0.86 q20 = queue_79 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f315,hypothesis,(
% 0.23/0.86 q21 = queue_85 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f316,hypothesis,(
% 0.23/0.86 q22 = queue_91 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f317,hypothesis,(
% 0.23/0.86 q23 = queue_97 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f318,hypothesis,(
% 0.23/0.86 q24 = queue_103 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f319,hypothesis,(
% 0.23/0.86 q25 = queue_109 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f320,hypothesis,(
% 0.23/0.86 q26 = queue_115 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f321,hypothesis,(
% 0.23/0.86 q27 = queue_121 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f322,hypothesis,(
% 0.23/0.86 q28 = queue_127 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f323,hypothesis,(
% 0.23/0.86 q29 = queue_133 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f324,hypothesis,(
% 0.23/0.86 q3 = queue_139 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f325,hypothesis,(
% 0.23/0.86 q30 = queue_145 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f326,hypothesis,(
% 0.23/0.86 q31 = queue_151 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f327,hypothesis,(
% 0.23/0.86 q32 = queue_157 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f328,hypothesis,(
% 0.23/0.86 q33 = queue_163 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f329,hypothesis,(
% 0.23/0.86 q34 = queue_169 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f330,hypothesis,(
% 0.23/0.86 q35 = queue_175 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f331,hypothesis,(
% 0.23/0.86 q36 = queue_181 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f332,hypothesis,(
% 0.23/0.86 q37 = queue_187 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f333,hypothesis,(
% 0.23/0.86 q38 = queue_193 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f334,hypothesis,(
% 0.23/0.86 q39 = queue_199 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f335,hypothesis,(
% 0.23/0.86 q4 = queue_205 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f336,hypothesis,(
% 0.23/0.86 q40 = queue_211 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f337,hypothesis,(
% 0.23/0.86 q41 = queue_217 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f338,hypothesis,(
% 0.23/0.86 q42 = queue_223 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f339,hypothesis,(
% 0.23/0.86 q43 = queue_229 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f340,hypothesis,(
% 0.23/0.86 q44 = queue_235 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f341,hypothesis,(
% 0.23/0.86 q45 = queue_241 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f342,hypothesis,(
% 0.23/0.86 q46 = queue_247 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f343,hypothesis,(
% 0.23/0.86 q5 = queue_253 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f344,hypothesis,(
% 0.23/0.86 q6 = queue_259 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f345,hypothesis,(
% 0.23/0.86 q7 = queue_265 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f346,hypothesis,(
% 0.23/0.86 q8 = queue_271 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f347,hypothesis,(
% 0.23/0.86 q9 = queue_277 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f348,negated_conjecture,(
% 0.23/0.86 elem_280 != elem_283 ),
% 0.23/0.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.86 fof(f349,plain,(
% 0.23/0.86 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f1])).
% 0.23/0.86 fof(f352,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_seq(rstore_seq(X0,X1))=X1)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f3])).
% 0.23/0.86 fof(f353,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_head(rstore_head(X0,X1))=X1)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f4])).
% 0.23/0.86 fof(f354,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_tail(rstore_tail(X0,X1))=X1)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f5])).
% 0.23/0.86 fof(f356,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_seq(rstore_tail(X0,X1))=rselect_seq(X0))),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f7])).
% 0.23/0.86 fof(f357,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_head(rstore_tail(X0,X1))=rselect_head(X0))),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f8])).
% 0.23/0.86 fof(f358,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_head(rstore_seq(X0,X1))=rselect_head(X0))),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f9])).
% 0.23/0.86 fof(f360,plain,(
% 0.23/0.86 ![X0,X1]: (rselect_tail(rstore_head(X0,X1))=rselect_tail(X0))),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f11])).
% 0.23/0.86 fof(f361,plain,(
% 0.23/0.86 ![X0]: (p(s(X0))=X0)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f12])).
% 0.23/0.86 fof(f362,plain,(
% 0.23/0.86 ![X0]: (s(p(X0))=X0)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f13])).
% 0.23/0.86 fof(f365,plain,(
% 0.23/0.86 ![X0]: (s(s(s(X0)))=X0)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f16])).
% 0.23/0.86 fof(f420,plain,(
% 0.23/0.86 earray_244=store(earray_242,index_243,e45)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f71])).
% 0.23/0.86 fof(f432,plain,(
% 0.23/0.86 earray_278=rselect_seq(q46)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f83])).
% 0.23/0.86 fof(f459,plain,(
% 0.23/0.86 elem_280=select(earray_278,index_279)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f110])).
% 0.23/0.86 fof(f460,plain,(
% 0.23/0.86 elem_283=select(earray_278,index_282)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f111])).
% 0.23/0.86 fof(f461,plain,(
% 0.23/0.86 index_0=rselect_tail(q)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f112])).
% 0.23/0.86 fof(f462,plain,(
% 0.23/0.86 index_102=s(index_99)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f113])).
% 0.23/0.86 fof(f463,plain,(
% 0.23/0.86 index_105=rselect_tail(q24)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f114])).
% 0.23/0.86 fof(f464,plain,(
% 0.23/0.86 index_108=s(index_105)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f115])).
% 0.23/0.86 fof(f465,plain,(
% 0.23/0.86 index_111=rselect_tail(q25)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f116])).
% 0.23/0.86 fof(f466,plain,(
% 0.23/0.86 index_114=s(index_111)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f117])).
% 0.23/0.86 fof(f467,plain,(
% 0.23/0.86 index_117=rselect_tail(q26)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f118])).
% 0.23/0.86 fof(f468,plain,(
% 0.23/0.86 index_12=s(index_9)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f119])).
% 0.23/0.86 fof(f469,plain,(
% 0.23/0.86 index_120=s(index_117)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f120])).
% 0.23/0.86 fof(f470,plain,(
% 0.23/0.86 index_123=rselect_tail(q27)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f121])).
% 0.23/0.86 fof(f471,plain,(
% 0.23/0.86 index_126=s(index_123)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f122])).
% 0.23/0.86 fof(f472,plain,(
% 0.23/0.86 index_129=rselect_tail(q28)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f123])).
% 0.23/0.86 fof(f473,plain,(
% 0.23/0.86 index_132=s(index_129)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f124])).
% 0.23/0.86 fof(f474,plain,(
% 0.23/0.86 index_135=rselect_tail(q2)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f125])).
% 0.23/0.86 fof(f475,plain,(
% 0.23/0.86 index_138=s(index_135)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f126])).
% 0.23/0.86 fof(f476,plain,(
% 0.23/0.86 index_141=rselect_tail(q29)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f127])).
% 0.23/0.86 fof(f477,plain,(
% 0.23/0.86 index_144=s(index_141)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f128])).
% 0.23/0.86 fof(f478,plain,(
% 0.23/0.86 index_147=rselect_tail(q30)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f129])).
% 0.23/0.86 fof(f479,plain,(
% 0.23/0.86 index_15=rselect_tail(q10)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f130])).
% 0.23/0.86 fof(f480,plain,(
% 0.23/0.86 index_150=s(index_147)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f131])).
% 0.23/0.86 fof(f481,plain,(
% 0.23/0.86 index_153=rselect_tail(q31)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.86 fof(f482,plain,(
% 0.23/0.86 index_156=s(index_153)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f133])).
% 0.23/0.86 fof(f483,plain,(
% 0.23/0.86 index_159=rselect_tail(q32)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f134])).
% 0.23/0.86 fof(f484,plain,(
% 0.23/0.86 index_162=s(index_159)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f135])).
% 0.23/0.86 fof(f485,plain,(
% 0.23/0.86 index_165=rselect_tail(q33)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f136])).
% 0.23/0.86 fof(f486,plain,(
% 0.23/0.86 index_168=s(index_165)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f137])).
% 0.23/0.86 fof(f487,plain,(
% 0.23/0.86 index_171=rselect_tail(q34)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f138])).
% 0.23/0.86 fof(f488,plain,(
% 0.23/0.86 index_174=s(index_171)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f139])).
% 0.23/0.86 fof(f489,plain,(
% 0.23/0.86 index_177=rselect_tail(q35)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f140])).
% 0.23/0.86 fof(f490,plain,(
% 0.23/0.86 index_18=s(index_15)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f141])).
% 0.23/0.86 fof(f491,plain,(
% 0.23/0.86 index_180=s(index_177)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f142])).
% 0.23/0.86 fof(f492,plain,(
% 0.23/0.86 index_183=rselect_tail(q36)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f143])).
% 0.23/0.86 fof(f493,plain,(
% 0.23/0.86 index_186=s(index_183)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f144])).
% 0.23/0.86 fof(f494,plain,(
% 0.23/0.86 index_189=rselect_tail(q37)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f145])).
% 0.23/0.86 fof(f495,plain,(
% 0.23/0.86 index_192=s(index_189)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f146])).
% 0.23/0.86 fof(f496,plain,(
% 0.23/0.86 index_195=rselect_tail(q38)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f147])).
% 0.23/0.86 fof(f497,plain,(
% 0.23/0.86 index_198=s(index_195)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f148])).
% 0.23/0.86 fof(f498,plain,(
% 0.23/0.86 index_201=rselect_tail(q3)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f149])).
% 0.23/0.86 fof(f499,plain,(
% 0.23/0.86 index_204=s(index_201)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f150])).
% 0.23/0.86 fof(f500,plain,(
% 0.23/0.86 index_207=rselect_tail(q39)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f151])).
% 0.23/0.86 fof(f501,plain,(
% 0.23/0.86 index_21=rselect_tail(q11)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f152])).
% 0.23/0.86 fof(f502,plain,(
% 0.23/0.86 index_210=s(index_207)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f153])).
% 0.23/0.86 fof(f503,plain,(
% 0.23/0.86 index_213=rselect_tail(q40)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f154])).
% 0.23/0.86 fof(f504,plain,(
% 0.23/0.86 index_216=s(index_213)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f155])).
% 0.23/0.86 fof(f505,plain,(
% 0.23/0.86 index_219=rselect_tail(q41)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f156])).
% 0.23/0.86 fof(f506,plain,(
% 0.23/0.86 index_222=s(index_219)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f157])).
% 0.23/0.86 fof(f507,plain,(
% 0.23/0.86 index_225=rselect_tail(q42)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f158])).
% 0.23/0.86 fof(f508,plain,(
% 0.23/0.86 index_228=s(index_225)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f159])).
% 0.23/0.86 fof(f509,plain,(
% 0.23/0.86 index_231=rselect_tail(q43)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f160])).
% 0.23/0.86 fof(f510,plain,(
% 0.23/0.86 index_234=s(index_231)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f161])).
% 0.23/0.86 fof(f511,plain,(
% 0.23/0.86 index_237=rselect_tail(q44)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f162])).
% 0.23/0.86 fof(f512,plain,(
% 0.23/0.86 index_24=s(index_21)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f163])).
% 0.23/0.86 fof(f513,plain,(
% 0.23/0.86 index_240=s(index_237)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f164])).
% 0.23/0.86 fof(f514,plain,(
% 0.23/0.86 index_243=rselect_tail(q45)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f165])).
% 0.23/0.86 fof(f515,plain,(
% 0.23/0.86 index_246=s(index_243)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f166])).
% 0.23/0.86 fof(f516,plain,(
% 0.23/0.86 index_249=rselect_tail(q4)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f167])).
% 0.23/0.86 fof(f517,plain,(
% 0.23/0.86 index_252=s(index_249)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f168])).
% 0.23/0.86 fof(f518,plain,(
% 0.23/0.86 index_255=rselect_tail(q5)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f169])).
% 0.23/0.86 fof(f519,plain,(
% 0.23/0.86 index_258=s(index_255)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f170])).
% 0.23/0.86 fof(f520,plain,(
% 0.23/0.86 index_261=rselect_tail(q6)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f171])).
% 0.23/0.86 fof(f521,plain,(
% 0.23/0.86 index_264=s(index_261)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f172])).
% 0.23/0.86 fof(f522,plain,(
% 0.23/0.86 index_267=rselect_tail(q7)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f173])).
% 0.23/0.86 fof(f523,plain,(
% 0.23/0.86 index_27=rselect_tail(q12)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f174])).
% 0.23/0.86 fof(f524,plain,(
% 0.23/0.86 index_270=s(index_267)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f175])).
% 0.23/0.86 fof(f525,plain,(
% 0.23/0.86 index_273=rselect_tail(q8)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f176])).
% 0.23/0.86 fof(f526,plain,(
% 0.23/0.86 index_276=s(index_273)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f177])).
% 0.23/0.86 fof(f527,plain,(
% 0.23/0.86 index_279=rselect_head(q46)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f178])).
% 0.23/0.86 fof(f528,plain,(
% 0.23/0.86 index_281=rselect_tail(q46)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f179])).
% 0.23/0.86 fof(f529,plain,(
% 0.23/0.86 s(index_282)=index_281),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f180])).
% 0.23/0.86 fof(f530,plain,(
% 0.23/0.86 index_3=rselect_tail(q0)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f181])).
% 0.23/0.86 fof(f531,plain,(
% 0.23/0.86 index_30=s(index_27)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f182])).
% 0.23/0.86 fof(f532,plain,(
% 0.23/0.86 index_33=rselect_tail(q13)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f183])).
% 0.23/0.86 fof(f533,plain,(
% 0.23/0.86 index_36=s(index_33)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f184])).
% 0.23/0.86 fof(f534,plain,(
% 0.23/0.86 index_39=rselect_tail(q14)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f185])).
% 0.23/0.86 fof(f535,plain,(
% 0.23/0.86 index_42=s(index_39)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f186])).
% 0.23/0.86 fof(f536,plain,(
% 0.23/0.86 index_45=rselect_tail(q15)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f187])).
% 0.23/0.86 fof(f537,plain,(
% 0.23/0.86 index_48=s(index_45)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f188])).
% 0.23/0.86 fof(f538,plain,(
% 0.23/0.86 index_51=rselect_tail(q16)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f189])).
% 0.23/0.86 fof(f539,plain,(
% 0.23/0.86 index_54=s(index_51)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f190])).
% 0.23/0.86 fof(f540,plain,(
% 0.23/0.86 index_57=rselect_tail(q17)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f191])).
% 0.23/0.86 fof(f541,plain,(
% 0.23/0.86 index_6=s(index_3)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f192])).
% 0.23/0.86 fof(f542,plain,(
% 0.23/0.86 index_60=s(index_57)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.86 fof(f543,plain,(
% 0.23/0.86 index_63=rselect_tail(q18)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f194])).
% 0.23/0.86 fof(f544,plain,(
% 0.23/0.86 index_66=s(index_63)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f195])).
% 0.23/0.86 fof(f545,plain,(
% 0.23/0.86 index_69=rselect_tail(q1)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f196])).
% 0.23/0.86 fof(f546,plain,(
% 0.23/0.86 index_72=s(index_69)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f197])).
% 0.23/0.86 fof(f547,plain,(
% 0.23/0.86 index_75=rselect_tail(q19)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f198])).
% 0.23/0.86 fof(f548,plain,(
% 0.23/0.86 index_78=s(index_75)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f199])).
% 0.23/0.86 fof(f549,plain,(
% 0.23/0.86 index_81=rselect_tail(q20)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f200])).
% 0.23/0.86 fof(f550,plain,(
% 0.23/0.86 index_84=s(index_81)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f201])).
% 0.23/0.86 fof(f551,plain,(
% 0.23/0.86 index_87=rselect_tail(q21)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f202])).
% 0.23/0.86 fof(f552,plain,(
% 0.23/0.86 index_9=rselect_tail(q9)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f203])).
% 0.23/0.86 fof(f553,plain,(
% 0.23/0.86 index_90=s(index_87)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f204])).
% 0.23/0.86 fof(f554,plain,(
% 0.23/0.86 index_93=rselect_tail(q22)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f205])).
% 0.23/0.86 fof(f555,plain,(
% 0.23/0.86 index_96=s(index_93)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f206])).
% 0.23/0.86 fof(f556,plain,(
% 0.23/0.86 index_99=rselect_tail(q23)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f207])).
% 0.23/0.86 fof(f557,plain,(
% 0.23/0.86 queue_1=rstore_head(q,index_0)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f208])).
% 0.23/0.86 fof(f558,plain,(
% 0.23/0.86 queue_101=rstore_seq(q23,earray_100)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f209])).
% 0.23/0.86 fof(f559,plain,(
% 0.23/0.86 queue_103=rstore_tail(queue_101,index_102)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f210])).
% 0.23/0.86 fof(f560,plain,(
% 0.23/0.86 queue_107=rstore_seq(q24,earray_106)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f211])).
% 0.23/0.86 fof(f561,plain,(
% 0.23/0.86 queue_109=rstore_tail(queue_107,index_108)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f212])).
% 0.23/0.86 fof(f562,plain,(
% 0.23/0.86 queue_11=rstore_seq(q9,earray_10)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f213])).
% 0.23/0.86 fof(f563,plain,(
% 0.23/0.86 queue_113=rstore_seq(q25,earray_112)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f214])).
% 0.23/0.86 fof(f564,plain,(
% 0.23/0.86 queue_115=rstore_tail(queue_113,index_114)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f215])).
% 0.23/0.86 fof(f565,plain,(
% 0.23/0.86 queue_119=rstore_seq(q26,earray_118)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f216])).
% 0.23/0.86 fof(f566,plain,(
% 0.23/0.86 queue_121=rstore_tail(queue_119,index_120)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f217])).
% 0.23/0.86 fof(f567,plain,(
% 0.23/0.86 queue_125=rstore_seq(q27,earray_124)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f218])).
% 0.23/0.86 fof(f568,plain,(
% 0.23/0.86 queue_127=rstore_tail(queue_125,index_126)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f219])).
% 0.23/0.86 fof(f569,plain,(
% 0.23/0.86 queue_13=rstore_tail(queue_11,index_12)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f220])).
% 0.23/0.86 fof(f570,plain,(
% 0.23/0.86 queue_131=rstore_seq(q28,earray_130)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f221])).
% 0.23/0.86 fof(f571,plain,(
% 0.23/0.86 queue_133=rstore_tail(queue_131,index_132)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f222])).
% 0.23/0.86 fof(f572,plain,(
% 0.23/0.86 queue_137=rstore_seq(q2,earray_136)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f223])).
% 0.23/0.86 fof(f573,plain,(
% 0.23/0.86 queue_139=rstore_tail(queue_137,index_138)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f224])).
% 0.23/0.86 fof(f574,plain,(
% 0.23/0.86 queue_143=rstore_seq(q29,earray_142)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f225])).
% 0.23/0.86 fof(f575,plain,(
% 0.23/0.86 queue_145=rstore_tail(queue_143,index_144)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f226])).
% 0.23/0.86 fof(f576,plain,(
% 0.23/0.86 queue_149=rstore_seq(q30,earray_148)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f227])).
% 0.23/0.86 fof(f577,plain,(
% 0.23/0.86 queue_151=rstore_tail(queue_149,index_150)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f228])).
% 0.23/0.86 fof(f578,plain,(
% 0.23/0.86 queue_155=rstore_seq(q31,earray_154)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f229])).
% 0.23/0.86 fof(f579,plain,(
% 0.23/0.86 queue_157=rstore_tail(queue_155,index_156)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f230])).
% 0.23/0.86 fof(f580,plain,(
% 0.23/0.86 queue_161=rstore_seq(q32,earray_160)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f231])).
% 0.23/0.86 fof(f581,plain,(
% 0.23/0.86 queue_163=rstore_tail(queue_161,index_162)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f232])).
% 0.23/0.86 fof(f582,plain,(
% 0.23/0.86 queue_167=rstore_seq(q33,earray_166)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f233])).
% 0.23/0.86 fof(f583,plain,(
% 0.23/0.86 queue_169=rstore_tail(queue_167,index_168)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f234])).
% 0.23/0.86 fof(f584,plain,(
% 0.23/0.86 queue_17=rstore_seq(q10,earray_16)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f235])).
% 0.23/0.86 fof(f585,plain,(
% 0.23/0.86 queue_173=rstore_seq(q34,earray_172)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f236])).
% 0.23/0.86 fof(f586,plain,(
% 0.23/0.86 queue_175=rstore_tail(queue_173,index_174)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f237])).
% 0.23/0.86 fof(f587,plain,(
% 0.23/0.86 queue_179=rstore_seq(q35,earray_178)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f238])).
% 0.23/0.86 fof(f588,plain,(
% 0.23/0.86 queue_181=rstore_tail(queue_179,index_180)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f239])).
% 0.23/0.86 fof(f589,plain,(
% 0.23/0.86 queue_185=rstore_seq(q36,earray_184)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f240])).
% 0.23/0.86 fof(f590,plain,(
% 0.23/0.86 queue_187=rstore_tail(queue_185,index_186)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f241])).
% 0.23/0.86 fof(f591,plain,(
% 0.23/0.86 queue_19=rstore_tail(queue_17,index_18)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f242])).
% 0.23/0.86 fof(f592,plain,(
% 0.23/0.86 queue_191=rstore_seq(q37,earray_190)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f243])).
% 0.23/0.86 fof(f593,plain,(
% 0.23/0.86 queue_193=rstore_tail(queue_191,index_192)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f244])).
% 0.23/0.86 fof(f594,plain,(
% 0.23/0.86 queue_197=rstore_seq(q38,earray_196)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f245])).
% 0.23/0.86 fof(f595,plain,(
% 0.23/0.86 queue_199=rstore_tail(queue_197,index_198)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f246])).
% 0.23/0.86 fof(f596,plain,(
% 0.23/0.86 queue_203=rstore_seq(q3,earray_202)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f247])).
% 0.23/0.86 fof(f597,plain,(
% 0.23/0.86 queue_205=rstore_tail(queue_203,index_204)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f248])).
% 0.23/0.86 fof(f598,plain,(
% 0.23/0.86 queue_209=rstore_seq(q39,earray_208)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f249])).
% 0.23/0.86 fof(f599,plain,(
% 0.23/0.86 queue_211=rstore_tail(queue_209,index_210)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f250])).
% 0.23/0.86 fof(f600,plain,(
% 0.23/0.86 queue_215=rstore_seq(q40,earray_214)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f251])).
% 0.23/0.86 fof(f601,plain,(
% 0.23/0.86 queue_217=rstore_tail(queue_215,index_216)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f252])).
% 0.23/0.86 fof(f602,plain,(
% 0.23/0.86 queue_221=rstore_seq(q41,earray_220)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f253])).
% 0.23/0.86 fof(f603,plain,(
% 0.23/0.86 queue_223=rstore_tail(queue_221,index_222)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f254])).
% 0.23/0.86 fof(f604,plain,(
% 0.23/0.86 queue_227=rstore_seq(q42,earray_226)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f255])).
% 0.23/0.86 fof(f605,plain,(
% 0.23/0.86 queue_229=rstore_tail(queue_227,index_228)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f256])).
% 0.23/0.86 fof(f606,plain,(
% 0.23/0.86 queue_23=rstore_seq(q11,earray_22)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f257])).
% 0.23/0.86 fof(f607,plain,(
% 0.23/0.86 queue_233=rstore_seq(q43,earray_232)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f258])).
% 0.23/0.86 fof(f608,plain,(
% 0.23/0.86 queue_235=rstore_tail(queue_233,index_234)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f259])).
% 0.23/0.86 fof(f609,plain,(
% 0.23/0.86 queue_239=rstore_seq(q44,earray_238)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f260])).
% 0.23/0.86 fof(f610,plain,(
% 0.23/0.86 queue_241=rstore_tail(queue_239,index_240)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f261])).
% 0.23/0.86 fof(f611,plain,(
% 0.23/0.86 queue_245=rstore_seq(q45,earray_244)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f262])).
% 0.23/0.86 fof(f612,plain,(
% 0.23/0.86 queue_247=rstore_tail(queue_245,index_246)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f263])).
% 0.23/0.86 fof(f613,plain,(
% 0.23/0.86 queue_25=rstore_tail(queue_23,index_24)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f264])).
% 0.23/0.86 fof(f614,plain,(
% 0.23/0.86 queue_251=rstore_seq(q4,earray_250)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f265])).
% 0.23/0.86 fof(f615,plain,(
% 0.23/0.86 queue_253=rstore_tail(queue_251,index_252)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f266])).
% 0.23/0.86 fof(f616,plain,(
% 0.23/0.86 queue_257=rstore_seq(q5,earray_256)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f267])).
% 0.23/0.86 fof(f617,plain,(
% 0.23/0.86 queue_259=rstore_tail(queue_257,index_258)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f268])).
% 0.23/0.86 fof(f618,plain,(
% 0.23/0.86 queue_263=rstore_seq(q6,earray_262)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f269])).
% 0.23/0.86 fof(f619,plain,(
% 0.23/0.86 queue_265=rstore_tail(queue_263,index_264)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f270])).
% 0.23/0.86 fof(f620,plain,(
% 0.23/0.86 queue_269=rstore_seq(q7,earray_268)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f271])).
% 0.23/0.86 fof(f621,plain,(
% 0.23/0.86 queue_271=rstore_tail(queue_269,index_270)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f272])).
% 0.23/0.86 fof(f622,plain,(
% 0.23/0.86 queue_275=rstore_seq(q8,earray_274)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f273])).
% 0.23/0.86 fof(f623,plain,(
% 0.23/0.86 queue_277=rstore_tail(queue_275,index_276)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f274])).
% 0.23/0.86 fof(f624,plain,(
% 0.23/0.86 queue_29=rstore_seq(q12,earray_28)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f275])).
% 0.23/0.86 fof(f625,plain,(
% 0.23/0.86 queue_31=rstore_tail(queue_29,index_30)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f276])).
% 0.23/0.86 fof(f626,plain,(
% 0.23/0.86 queue_35=rstore_seq(q13,earray_34)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f277])).
% 0.23/0.86 fof(f627,plain,(
% 0.23/0.86 queue_37=rstore_tail(queue_35,index_36)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f278])).
% 0.23/0.86 fof(f628,plain,(
% 0.23/0.86 queue_41=rstore_seq(q14,earray_40)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f279])).
% 0.23/0.86 fof(f629,plain,(
% 0.23/0.86 queue_43=rstore_tail(queue_41,index_42)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f280])).
% 0.23/0.86 fof(f630,plain,(
% 0.23/0.86 queue_47=rstore_seq(q15,earray_46)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f281])).
% 0.23/0.86 fof(f631,plain,(
% 0.23/0.86 queue_49=rstore_tail(queue_47,index_48)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f282])).
% 0.23/0.86 fof(f632,plain,(
% 0.23/0.86 queue_5=rstore_seq(q0,earray_4)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f283])).
% 0.23/0.86 fof(f633,plain,(
% 0.23/0.86 queue_53=rstore_seq(q16,earray_52)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f284])).
% 0.23/0.86 fof(f634,plain,(
% 0.23/0.86 queue_55=rstore_tail(queue_53,index_54)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f285])).
% 0.23/0.86 fof(f635,plain,(
% 0.23/0.86 queue_59=rstore_seq(q17,earray_58)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f286])).
% 0.23/0.86 fof(f636,plain,(
% 0.23/0.86 queue_61=rstore_tail(queue_59,index_60)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f287])).
% 0.23/0.86 fof(f637,plain,(
% 0.23/0.86 queue_65=rstore_seq(q18,earray_64)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f288])).
% 0.23/0.86 fof(f638,plain,(
% 0.23/0.86 queue_67=rstore_tail(queue_65,index_66)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f289])).
% 0.23/0.86 fof(f639,plain,(
% 0.23/0.86 queue_7=rstore_tail(queue_5,index_6)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f290])).
% 0.23/0.86 fof(f640,plain,(
% 0.23/0.86 queue_71=rstore_seq(q1,earray_70)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f291])).
% 0.23/0.86 fof(f641,plain,(
% 0.23/0.86 queue_73=rstore_tail(queue_71,index_72)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f292])).
% 0.23/0.86 fof(f642,plain,(
% 0.23/0.86 queue_77=rstore_seq(q19,earray_76)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f293])).
% 0.23/0.86 fof(f643,plain,(
% 0.23/0.86 queue_79=rstore_tail(queue_77,index_78)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f294])).
% 0.23/0.86 fof(f644,plain,(
% 0.23/0.86 queue_83=rstore_seq(q20,earray_82)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f295])).
% 0.23/0.86 fof(f645,plain,(
% 0.23/0.86 queue_85=rstore_tail(queue_83,index_84)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f296])).
% 0.23/0.86 fof(f646,plain,(
% 0.23/0.86 queue_89=rstore_seq(q21,earray_88)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f297])).
% 0.23/0.86 fof(f647,plain,(
% 0.23/0.86 queue_91=rstore_tail(queue_89,index_90)),
% 0.23/0.86 inference(cnf_transformation,[status(thm)],[f298])).
% 0.23/0.86 fof(f648,plain,(
% 0.23/0.86 queue_95=rstore_seq(q22,earray_94)),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f299])).
% 0.23/0.87 fof(f649,plain,(
% 0.23/0.87 queue_97=rstore_tail(queue_95,index_96)),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f300])).
% 0.23/0.87 fof(f650,plain,(
% 0.23/0.87 q0=queue_1),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f301])).
% 0.23/0.87 fof(f651,plain,(
% 0.23/0.87 q1=queue_7),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f302])).
% 0.23/0.87 fof(f652,plain,(
% 0.23/0.87 q10=queue_13),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f303])).
% 0.23/0.87 fof(f653,plain,(
% 0.23/0.87 q11=queue_19),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f304])).
% 0.23/0.87 fof(f654,plain,(
% 0.23/0.87 q12=queue_25),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f305])).
% 0.23/0.87 fof(f655,plain,(
% 0.23/0.87 q13=queue_31),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f306])).
% 0.23/0.87 fof(f656,plain,(
% 0.23/0.87 q14=queue_37),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f307])).
% 0.23/0.87 fof(f657,plain,(
% 0.23/0.87 q15=queue_43),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f308])).
% 0.23/0.87 fof(f658,plain,(
% 0.23/0.87 q16=queue_49),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f309])).
% 0.23/0.87 fof(f659,plain,(
% 0.23/0.87 q17=queue_55),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f310])).
% 0.23/0.87 fof(f660,plain,(
% 0.23/0.87 q18=queue_61),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f311])).
% 0.23/0.87 fof(f661,plain,(
% 0.23/0.87 q19=queue_67),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f312])).
% 0.23/0.87 fof(f662,plain,(
% 0.23/0.87 q2=queue_73),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f313])).
% 0.23/0.87 fof(f663,plain,(
% 0.23/0.87 q20=queue_79),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f314])).
% 0.23/0.87 fof(f664,plain,(
% 0.23/0.87 q21=queue_85),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f315])).
% 0.23/0.87 fof(f665,plain,(
% 0.23/0.87 q22=queue_91),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f316])).
% 0.23/0.87 fof(f666,plain,(
% 0.23/0.87 q23=queue_97),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f317])).
% 0.23/0.87 fof(f667,plain,(
% 0.23/0.87 q24=queue_103),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f318])).
% 0.23/0.87 fof(f668,plain,(
% 0.23/0.87 q25=queue_109),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f319])).
% 0.23/0.87 fof(f669,plain,(
% 0.23/0.87 q26=queue_115),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f320])).
% 0.23/0.87 fof(f670,plain,(
% 0.23/0.87 q27=queue_121),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f321])).
% 0.23/0.87 fof(f671,plain,(
% 0.23/0.87 q28=queue_127),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f322])).
% 0.23/0.87 fof(f672,plain,(
% 0.23/0.87 q29=queue_133),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f323])).
% 0.23/0.87 fof(f673,plain,(
% 0.23/0.87 q3=queue_139),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f324])).
% 0.23/0.87 fof(f674,plain,(
% 0.23/0.87 q30=queue_145),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f325])).
% 0.23/0.87 fof(f675,plain,(
% 0.23/0.87 q31=queue_151),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f326])).
% 0.23/0.87 fof(f676,plain,(
% 0.23/0.87 q32=queue_157),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f327])).
% 0.23/0.87 fof(f677,plain,(
% 0.23/0.87 q33=queue_163),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f328])).
% 0.23/0.87 fof(f678,plain,(
% 0.23/0.87 q34=queue_169),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f329])).
% 0.23/0.87 fof(f679,plain,(
% 0.23/0.87 q35=queue_175),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f330])).
% 0.23/0.87 fof(f680,plain,(
% 0.23/0.87 q36=queue_181),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f331])).
% 0.23/0.87 fof(f681,plain,(
% 0.23/0.87 q37=queue_187),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f332])).
% 0.23/0.87 fof(f682,plain,(
% 0.23/0.87 q38=queue_193),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f333])).
% 0.23/0.87 fof(f683,plain,(
% 0.23/0.87 q39=queue_199),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f334])).
% 0.23/0.87 fof(f684,plain,(
% 0.23/0.87 q4=queue_205),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f335])).
% 0.23/0.87 fof(f685,plain,(
% 0.23/0.87 q40=queue_211),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f336])).
% 0.23/0.87 fof(f686,plain,(
% 0.23/0.87 q41=queue_217),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f337])).
% 0.23/0.87 fof(f687,plain,(
% 0.23/0.87 q42=queue_223),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f338])).
% 0.23/0.87 fof(f688,plain,(
% 0.23/0.87 q43=queue_229),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f339])).
% 0.23/0.87 fof(f689,plain,(
% 0.23/0.87 q44=queue_235),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f340])).
% 0.23/0.87 fof(f690,plain,(
% 0.23/0.87 q45=queue_241),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f341])).
% 0.23/0.87 fof(f691,plain,(
% 0.23/0.87 q46=queue_247),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f342])).
% 0.23/0.87 fof(f692,plain,(
% 0.23/0.87 q5=queue_253),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f343])).
% 0.23/0.87 fof(f693,plain,(
% 0.23/0.87 q6=queue_259),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f344])).
% 0.23/0.87 fof(f694,plain,(
% 0.23/0.87 q7=queue_265),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f345])).
% 0.23/0.87 fof(f695,plain,(
% 0.23/0.87 q8=queue_271),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f346])).
% 0.23/0.87 fof(f696,plain,(
% 0.23/0.87 q9=queue_277),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f347])).
% 0.23/0.87 fof(f697,plain,(
% 0.23/0.87 ~elem_280=elem_283),
% 0.23/0.87 inference(cnf_transformation,[status(thm)],[f348])).
% 0.23/0.87 fof(f712,plain,(
% 0.23/0.87 p(index_281)=index_282),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f529,f361])).
% 0.23/0.87 fof(f746,plain,(
% 0.23/0.87 p(index_102)=index_99),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f462,f361])).
% 0.23/0.87 fof(f752,plain,(
% 0.23/0.87 p(index_108)=index_105),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f464,f361])).
% 0.23/0.87 fof(f756,plain,(
% 0.23/0.87 p(index_114)=index_111),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f466,f361])).
% 0.23/0.87 fof(f760,plain,(
% 0.23/0.87 p(index_12)=index_9),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f468,f361])).
% 0.23/0.87 fof(f764,plain,(
% 0.23/0.87 p(index_120)=index_117),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f469,f361])).
% 0.23/0.87 fof(f772,plain,(
% 0.23/0.87 p(index_126)=index_123),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f471,f361])).
% 0.23/0.87 fof(f776,plain,(
% 0.23/0.87 p(index_132)=index_129),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f473,f361])).
% 0.23/0.87 fof(f784,plain,(
% 0.23/0.87 p(index_144)=index_141),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f477,f361])).
% 0.23/0.87 fof(f792,plain,(
% 0.23/0.87 p(index_156)=index_153),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f482,f361])).
% 0.23/0.87 fof(f802,plain,(
% 0.23/0.87 p(index_162)=index_159),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f484,f361])).
% 0.23/0.87 fof(f806,plain,(
% 0.23/0.87 p(index_168)=index_165),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f486,f361])).
% 0.23/0.87 fof(f812,plain,(
% 0.23/0.87 p(index_174)=index_171),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f488,f361])).
% 0.23/0.87 fof(f816,plain,(
% 0.23/0.87 p(index_18)=index_15),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f490,f361])).
% 0.23/0.87 fof(f820,plain,(
% 0.23/0.87 p(index_180)=index_177),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f491,f361])).
% 0.23/0.87 fof(f824,plain,(
% 0.23/0.87 p(index_186)=index_183),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f493,f361])).
% 0.23/0.87 fof(f832,plain,(
% 0.23/0.87 p(index_192)=index_189),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f495,f361])).
% 0.23/0.87 fof(f836,plain,(
% 0.23/0.87 p(index_198)=index_195),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f497,f361])).
% 0.23/0.87 fof(f840,plain,(
% 0.23/0.87 p(index_204)=index_201),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f499,f361])).
% 0.23/0.87 fof(f844,plain,(
% 0.23/0.87 p(index_210)=index_207),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f502,f361])).
% 0.23/0.87 fof(f848,plain,(
% 0.23/0.87 p(index_216)=index_213),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f504,f361])).
% 0.23/0.87 fof(f852,plain,(
% 0.23/0.87 p(index_222)=index_219),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f506,f361])).
% 0.23/0.87 fof(f862,plain,(
% 0.23/0.87 p(index_228)=index_225),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f508,f361])).
% 0.23/0.87 fof(f866,plain,(
% 0.23/0.87 p(index_234)=index_231),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f510,f361])).
% 0.23/0.87 fof(f876,plain,(
% 0.23/0.87 p(index_240)=index_237),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f513,f361])).
% 0.23/0.87 fof(f892,plain,(
% 0.23/0.87 p(index_258)=index_255),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f519,f361])).
% 0.23/0.87 fof(f896,plain,(
% 0.23/0.87 p(index_264)=index_261),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f521,f361])).
% 0.23/0.87 fof(f900,plain,(
% 0.23/0.87 p(index_270)=index_267),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f524,f361])).
% 0.23/0.87 fof(f904,plain,(
% 0.23/0.87 p(index_276)=index_273),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f526,f361])).
% 0.23/0.87 fof(f908,plain,(
% 0.23/0.87 p(index_30)=index_27),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f531,f361])).
% 0.23/0.87 fof(f914,plain,(
% 0.23/0.87 select(earray_244,index_243)=e45),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f420,f349])).
% 0.23/0.87 fof(f918,plain,(
% 0.23/0.87 p(index_36)=index_33),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f533,f361])).
% 0.23/0.87 fof(f922,plain,(
% 0.23/0.87 p(index_42)=index_39),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f535,f361])).
% 0.23/0.87 fof(f928,plain,(
% 0.23/0.87 p(index_48)=index_45),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f537,f361])).
% 0.23/0.87 fof(f932,plain,(
% 0.23/0.87 p(index_54)=index_51),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f539,f361])).
% 0.23/0.87 fof(f936,plain,(
% 0.23/0.87 p(index_6)=index_3),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f541,f361])).
% 0.23/0.87 fof(f940,plain,(
% 0.23/0.87 p(index_60)=index_57),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f542,f361])).
% 0.23/0.87 fof(f944,plain,(
% 0.23/0.87 p(index_66)=index_63),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f544,f361])).
% 0.23/0.87 fof(f952,plain,(
% 0.23/0.87 p(index_72)=index_69),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f546,f361])).
% 0.23/0.87 fof(f956,plain,(
% 0.23/0.87 p(index_78)=index_75),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f548,f361])).
% 0.23/0.87 fof(f960,plain,(
% 0.23/0.87 p(index_84)=index_81),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f550,f361])).
% 0.23/0.87 fof(f964,plain,(
% 0.23/0.87 p(index_90)=index_87),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f553,f361])).
% 0.23/0.87 fof(f968,plain,(
% 0.23/0.87 p(index_96)=index_93),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f555,f361])).
% 0.23/0.87 fof(f1102,plain,(
% 0.23/0.87 q0=rstore_head(q,index_0)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f650,f557])).
% 0.23/0.87 fof(f1103,plain,(
% 0.23/0.87 rselect_tail(q0)=rselect_tail(q)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1102,f360])).
% 0.23/0.87 fof(f1105,plain,(
% 0.23/0.87 rselect_head(q0)=index_0),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1102,f353])).
% 0.23/0.87 fof(f1106,plain,(
% 0.23/0.87 index_3=rselect_tail(q)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f530,f1103])).
% 0.23/0.87 fof(f1118,plain,(
% 0.23/0.87 rselect_head(queue_101)=rselect_head(q23)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f558,f358])).
% 0.23/0.87 fof(f1139,plain,(
% 0.23/0.87 q24=rstore_tail(queue_101,index_102)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f667,f559])).
% 0.23/0.87 fof(f1140,plain,(
% 0.23/0.87 rselect_tail(q24)=index_102),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1139,f354])).
% 0.23/0.87 fof(f1141,plain,(
% 0.23/0.87 rselect_head(q24)=rselect_head(queue_101)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1139,f357])).
% 0.23/0.87 fof(f1143,plain,(
% 0.23/0.87 index_105=index_102),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f463,f1140])).
% 0.23/0.87 fof(f1146,plain,(
% 0.23/0.87 rselect_head(queue_107)=rselect_head(q24)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f560,f358])).
% 0.23/0.87 fof(f1150,plain,(
% 0.23/0.87 p(index_105)=index_99),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1143,f746])).
% 0.23/0.87 fof(f1153,plain,(
% 0.23/0.87 index_105=s(index_99)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1143,f462])).
% 0.23/0.87 fof(f1167,plain,(
% 0.23/0.87 index_0=index_3),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1106,f461])).
% 0.23/0.87 fof(f1169,plain,(
% 0.23/0.87 rselect_head(q0)=index_3),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1167,f1105])).
% 0.23/0.87 fof(f1173,plain,(
% 0.23/0.87 q25=rstore_tail(queue_107,index_108)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f668,f561])).
% 0.23/0.87 fof(f1174,plain,(
% 0.23/0.87 rselect_tail(q25)=index_108),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1173,f354])).
% 0.23/0.87 fof(f1175,plain,(
% 0.23/0.87 rselect_head(q25)=rselect_head(queue_107)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1173,f357])).
% 0.23/0.87 fof(f1177,plain,(
% 0.23/0.87 index_111=index_108),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f465,f1174])).
% 0.23/0.87 fof(f1180,plain,(
% 0.23/0.87 rselect_head(queue_11)=rselect_head(q9)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f562,f358])).
% 0.23/0.87 fof(f1184,plain,(
% 0.23/0.87 rselect_head(queue_113)=rselect_head(q25)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f563,f358])).
% 0.23/0.87 fof(f1189,plain,(
% 0.23/0.87 p(index_111)=index_105),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1177,f752])).
% 0.23/0.87 fof(f1192,plain,(
% 0.23/0.87 index_111=s(index_105)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1177,f464])).
% 0.23/0.87 fof(f1197,plain,(
% 0.23/0.87 q26=rstore_tail(queue_113,index_114)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f669,f564])).
% 0.23/0.87 fof(f1198,plain,(
% 0.23/0.87 rselect_tail(q26)=index_114),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1197,f354])).
% 0.23/0.87 fof(f1199,plain,(
% 0.23/0.87 rselect_head(q26)=rselect_head(queue_113)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1197,f357])).
% 0.23/0.87 fof(f1201,plain,(
% 0.23/0.87 index_117=index_114),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f467,f1198])).
% 0.23/0.87 fof(f1205,plain,(
% 0.23/0.87 p(index_117)=index_111),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1201,f756])).
% 0.23/0.87 fof(f1221,plain,(
% 0.23/0.87 rselect_head(queue_119)=rselect_head(q26)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f565,f358])).
% 0.23/0.87 fof(f1224,plain,(
% 0.23/0.87 q27=rstore_tail(queue_119,index_120)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f670,f566])).
% 0.23/0.87 fof(f1225,plain,(
% 0.23/0.87 rselect_tail(q27)=index_120),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1224,f354])).
% 0.23/0.87 fof(f1226,plain,(
% 0.23/0.87 rselect_head(q27)=rselect_head(queue_119)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1224,f357])).
% 0.23/0.87 fof(f1228,plain,(
% 0.23/0.87 index_123=index_120),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f470,f1225])).
% 0.23/0.87 fof(f1232,plain,(
% 0.23/0.87 p(index_123)=index_117),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1228,f764])).
% 0.23/0.87 fof(f1262,plain,(
% 0.23/0.87 rselect_head(queue_125)=rselect_head(q27)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f567,f358])).
% 0.23/0.87 fof(f1265,plain,(
% 0.23/0.87 q28=rstore_tail(queue_125,index_126)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f671,f568])).
% 0.23/0.87 fof(f1266,plain,(
% 0.23/0.87 rselect_tail(q28)=index_126),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1265,f354])).
% 0.23/0.87 fof(f1267,plain,(
% 0.23/0.87 rselect_head(q28)=rselect_head(queue_125)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1265,f357])).
% 0.23/0.87 fof(f1269,plain,(
% 0.23/0.87 index_129=index_126),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f472,f1266])).
% 0.23/0.87 fof(f1271,plain,(
% 0.23/0.87 q10=rstore_tail(queue_11,index_12)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f652,f569])).
% 0.23/0.87 fof(f1272,plain,(
% 0.23/0.87 rselect_tail(q10)=index_12),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1271,f354])).
% 0.23/0.87 fof(f1273,plain,(
% 0.23/0.87 rselect_head(q10)=rselect_head(queue_11)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1271,f357])).
% 0.23/0.87 fof(f1275,plain,(
% 0.23/0.87 index_15=index_12),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f479,f1272])).
% 0.23/0.87 fof(f1280,plain,(
% 0.23/0.87 p(index_129)=index_123),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1269,f772])).
% 0.23/0.87 fof(f1286,plain,(
% 0.23/0.87 p(index_15)=index_9),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1275,f760])).
% 0.23/0.87 fof(f1289,plain,(
% 0.23/0.87 index_15=s(index_9)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1275,f468])).
% 0.23/0.87 fof(f1294,plain,(
% 0.23/0.87 rselect_head(queue_131)=rselect_head(q28)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f570,f358])).
% 0.23/0.87 fof(f1304,plain,(
% 0.23/0.87 q29=rstore_tail(queue_131,index_132)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f672,f571])).
% 0.23/0.87 fof(f1305,plain,(
% 0.23/0.87 rselect_tail(q29)=index_132),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1304,f354])).
% 0.23/0.87 fof(f1306,plain,(
% 0.23/0.87 rselect_head(q29)=rselect_head(queue_131)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1304,f357])).
% 0.23/0.87 fof(f1308,plain,(
% 0.23/0.87 index_141=index_132),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f476,f1305])).
% 0.23/0.87 fof(f1311,plain,(
% 0.23/0.87 rselect_head(queue_137)=rselect_head(q2)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f572,f358])).
% 0.23/0.87 fof(f1316,plain,(
% 0.23/0.87 p(index_141)=index_129),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1308,f776])).
% 0.23/0.87 fof(f1319,plain,(
% 0.23/0.87 index_141=s(index_129)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1308,f473])).
% 0.23/0.87 fof(f1337,plain,(
% 0.23/0.87 s(s(index_15))=index_9),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1289,f365])).
% 0.23/0.87 fof(f1340,plain,(
% 0.23/0.87 s(index_18)=index_9),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f490,f1337])).
% 0.23/0.87 fof(f1351,plain,(
% 0.23/0.87 s(s(index_141))=index_129),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1319,f365])).
% 0.23/0.87 fof(f1354,plain,(
% 0.23/0.87 s(index_144)=index_129),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f477,f1351])).
% 0.23/0.87 fof(f1355,plain,(
% 0.23/0.87 q3=rstore_tail(queue_137,index_138)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f673,f573])).
% 0.23/0.87 fof(f1356,plain,(
% 0.23/0.87 rselect_tail(q3)=index_138),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1355,f354])).
% 0.23/0.87 fof(f1357,plain,(
% 0.23/0.87 rselect_head(q3)=rselect_head(queue_137)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1355,f357])).
% 0.23/0.87 fof(f1359,plain,(
% 0.23/0.87 index_201=index_138),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f498,f1356])).
% 0.23/0.87 fof(f1363,plain,(
% 0.23/0.87 rselect_head(queue_143)=rselect_head(q29)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f574,f358])).
% 0.23/0.87 fof(f1366,plain,(
% 0.23/0.87 q30=rstore_tail(queue_143,index_144)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f674,f575])).
% 0.23/0.87 fof(f1367,plain,(
% 0.23/0.87 rselect_tail(q30)=index_144),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1366,f354])).
% 0.23/0.87 fof(f1368,plain,(
% 0.23/0.87 rselect_head(q30)=rselect_head(queue_143)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1366,f357])).
% 0.23/0.87 fof(f1370,plain,(
% 0.23/0.87 index_147=index_144),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f478,f1367])).
% 0.23/0.87 fof(f1376,plain,(
% 0.23/0.87 index_201=s(index_135)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1359,f475])).
% 0.23/0.87 fof(f1382,plain,(
% 0.23/0.87 p(index_147)=index_141),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1370,f784])).
% 0.23/0.87 fof(f1388,plain,(
% 0.23/0.87 rselect_head(queue_149)=rselect_head(q30)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f576,f358])).
% 0.23/0.87 fof(f1395,plain,(
% 0.23/0.87 p(index_9)=index_18),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1340,f361])).
% 0.23/0.87 fof(f1400,plain,(
% 0.23/0.87 index_150=index_129),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1401,f480])).
% 0.23/0.87 fof(f1401,plain,(
% 0.23/0.87 s(index_147)=index_129),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1370,f1354])).
% 0.23/0.87 fof(f1403,plain,(
% 0.23/0.87 p(index_129)=index_147),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1401,f361])).
% 0.23/0.87 fof(f1407,plain,(
% 0.23/0.87 index_123=index_147),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1280,f1403])).
% 0.23/0.87 fof(f1415,plain,(
% 0.23/0.87 q31=rstore_tail(queue_149,index_150)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f675,f577])).
% 0.23/0.87 fof(f1416,plain,(
% 0.23/0.87 q31=rstore_tail(queue_149,index_129)),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1400,f1415])).
% 0.23/0.87 fof(f1417,plain,(
% 0.23/0.87 rselect_tail(q31)=index_129),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1416,f354])).
% 0.23/0.87 fof(f1418,plain,(
% 0.23/0.87 rselect_head(q31)=rselect_head(queue_149)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1416,f357])).
% 0.23/0.87 fof(f1422,plain,(
% 0.23/0.87 rselect_head(queue_155)=rselect_head(q31)),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f578,f358])).
% 0.23/0.87 fof(f1439,plain,(
% 0.23/0.87 s(s(index_201))=index_135),
% 0.23/0.87 inference(paramodulation,[status(thm)],[f1376,f365])).
% 0.23/0.87 fof(f1442,plain,(
% 0.23/0.87 s(index_204)=index_135),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f499,f1439])).
% 0.23/0.87 fof(f1443,plain,(
% 0.23/0.87 p(index_123)=index_141),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1407,f1382])).
% 0.23/0.87 fof(f1445,plain,(
% 0.23/0.87 index_117=s(index_129)),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1451,f1319])).
% 0.23/0.87 fof(f1446,plain,(
% 0.23/0.87 p(index_117)=index_129),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1451,f1316])).
% 0.23/0.87 fof(f1451,plain,(
% 0.23/0.87 index_117=index_141),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1232,f1443])).
% 0.23/0.87 fof(f1452,plain,(
% 0.23/0.87 index_111=index_129),
% 0.23/0.87 inference(forward_demodulation,[status(thm)],[f1205,f1446])).
% 0.23/0.87 fof(f1457,plain,(
% 0.23/0.87 p(index_111)=index_123),
% 0.23/0.87 inference(backward_demodulation,[status(thm)],[f1452,f1280])).
% 0.23/0.88 fof(f1462,plain,(
% 0.23/0.88 index_105=index_123),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1189,f1457])).
% 0.23/0.88 fof(f1467,plain,(
% 0.23/0.88 p(index_105)=index_117),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1462,f1232])).
% 0.23/0.88 fof(f1472,plain,(
% 0.23/0.88 index_99=index_117),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1150,f1467])).
% 0.23/0.88 fof(f1477,plain,(
% 0.23/0.88 p(index_99)=index_111),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1472,f1205])).
% 0.23/0.88 fof(f1482,plain,(
% 0.23/0.88 q32=rstore_tail(queue_155,index_156)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f676,f579])).
% 0.23/0.88 fof(f1483,plain,(
% 0.23/0.88 rselect_tail(q32)=index_156),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1482,f354])).
% 0.23/0.88 fof(f1484,plain,(
% 0.23/0.88 rselect_head(q32)=rselect_head(queue_155)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1482,f357])).
% 0.23/0.88 fof(f1486,plain,(
% 0.23/0.88 index_159=index_156),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f483,f1483])).
% 0.23/0.88 fof(f1489,plain,(
% 0.23/0.88 rselect_head(queue_161)=rselect_head(q32)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f580,f358])).
% 0.23/0.88 fof(f1492,plain,(
% 0.23/0.88 q33=rstore_tail(queue_161,index_162)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f677,f581])).
% 0.23/0.88 fof(f1493,plain,(
% 0.23/0.88 rselect_tail(q33)=index_162),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1492,f354])).
% 0.23/0.88 fof(f1494,plain,(
% 0.23/0.88 rselect_head(q33)=rselect_head(queue_161)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1492,f357])).
% 0.23/0.88 fof(f1496,plain,(
% 0.23/0.88 index_165=index_162),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f485,f1493])).
% 0.23/0.88 fof(f1499,plain,(
% 0.23/0.88 p(index_159)=index_153),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1486,f792])).
% 0.23/0.88 fof(f1505,plain,(
% 0.23/0.88 p(index_165)=index_159),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1496,f802])).
% 0.23/0.88 fof(f1511,plain,(
% 0.23/0.88 rselect_head(queue_167)=rselect_head(q33)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f582,f358])).
% 0.23/0.88 fof(f1524,plain,(
% 0.23/0.88 index_153=index_111),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1525,f481])).
% 0.23/0.88 fof(f1525,plain,(
% 0.23/0.88 rselect_tail(q31)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1452,f1417])).
% 0.23/0.88 fof(f1529,plain,(
% 0.23/0.88 q34=rstore_tail(queue_167,index_168)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f678,f583])).
% 0.23/0.88 fof(f1530,plain,(
% 0.23/0.88 rselect_tail(q34)=index_168),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1529,f354])).
% 0.23/0.88 fof(f1531,plain,(
% 0.23/0.88 rselect_head(q34)=rselect_head(queue_167)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1529,f357])).
% 0.23/0.88 fof(f1533,plain,(
% 0.23/0.88 index_171=index_168),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f487,f1530])).
% 0.23/0.88 fof(f1536,plain,(
% 0.23/0.88 rselect_head(queue_17)=rselect_head(q10)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f584,f358])).
% 0.23/0.88 fof(f1541,plain,(
% 0.23/0.88 p(index_171)=index_165),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1533,f806])).
% 0.23/0.88 fof(f1552,plain,(
% 0.23/0.88 p(index_135)=index_204),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1442,f361])).
% 0.23/0.88 fof(f1558,plain,(
% 0.23/0.88 index_99=s(index_129)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1472,f1445])).
% 0.23/0.88 fof(f1559,plain,(
% 0.23/0.88 index_99=s(index_111)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1452,f1558])).
% 0.23/0.88 fof(f1569,plain,(
% 0.23/0.88 rselect_head(queue_173)=rselect_head(q34)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f585,f358])).
% 0.23/0.88 fof(f1572,plain,(
% 0.23/0.88 q35=rstore_tail(queue_173,index_174)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f679,f586])).
% 0.23/0.88 fof(f1573,plain,(
% 0.23/0.88 rselect_tail(q35)=index_174),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1572,f354])).
% 0.23/0.88 fof(f1574,plain,(
% 0.23/0.88 rselect_head(q35)=rselect_head(queue_173)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1572,f357])).
% 0.23/0.88 fof(f1576,plain,(
% 0.23/0.88 index_177=index_174),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f489,f1573])).
% 0.23/0.88 fof(f1579,plain,(
% 0.23/0.88 rselect_head(queue_179)=rselect_head(q35)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f587,f358])).
% 0.23/0.88 fof(f1584,plain,(
% 0.23/0.88 p(index_177)=index_171),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1576,f812])).
% 0.23/0.88 fof(f1590,plain,(
% 0.23/0.88 q36=rstore_tail(queue_179,index_180)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f680,f588])).
% 0.23/0.88 fof(f1591,plain,(
% 0.23/0.88 rselect_tail(q36)=index_180),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1590,f354])).
% 0.23/0.88 fof(f1592,plain,(
% 0.23/0.88 rselect_head(q36)=rselect_head(queue_179)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1590,f357])).
% 0.23/0.88 fof(f1594,plain,(
% 0.23/0.88 index_183=index_180),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f492,f1591])).
% 0.23/0.88 fof(f1598,plain,(
% 0.23/0.88 p(index_183)=index_177),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1594,f820])).
% 0.23/0.88 fof(f1611,plain,(
% 0.23/0.88 rselect_head(queue_185)=rselect_head(q36)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f589,f358])).
% 0.23/0.88 fof(f1614,plain,(
% 0.23/0.88 q37=rstore_tail(queue_185,index_186)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f681,f590])).
% 0.23/0.88 fof(f1615,plain,(
% 0.23/0.88 rselect_tail(q37)=index_186),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1614,f354])).
% 0.23/0.88 fof(f1616,plain,(
% 0.23/0.88 rselect_head(q37)=rselect_head(queue_185)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1614,f357])).
% 0.23/0.88 fof(f1618,plain,(
% 0.23/0.88 index_189=index_186),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f494,f1615])).
% 0.23/0.88 fof(f1622,plain,(
% 0.23/0.88 p(index_189)=index_183),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1618,f824])).
% 0.23/0.88 fof(f1630,plain,(
% 0.23/0.88 p(index_159)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1524,f1499])).
% 0.23/0.88 fof(f1633,plain,(
% 0.23/0.88 s(index_111)=index_159),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1630,f362])).
% 0.23/0.88 fof(f1634,plain,(
% 0.23/0.88 index_99=index_159),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1559,f1633])).
% 0.23/0.88 fof(f1644,plain,(
% 0.23/0.88 p(index_165)=index_99),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1634,f1505])).
% 0.23/0.88 fof(f1647,plain,(
% 0.23/0.88 s(index_99)=index_165),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1644,f362])).
% 0.23/0.88 fof(f1648,plain,(
% 0.23/0.88 index_105=index_165),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1153,f1647])).
% 0.23/0.88 fof(f1659,plain,(
% 0.23/0.88 q11=rstore_tail(queue_17,index_18)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f653,f591])).
% 0.23/0.88 fof(f1660,plain,(
% 0.23/0.88 rselect_tail(q11)=index_18),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1659,f354])).
% 0.23/0.88 fof(f1661,plain,(
% 0.23/0.88 rselect_head(q11)=rselect_head(queue_17)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1659,f357])).
% 0.23/0.88 fof(f1663,plain,(
% 0.23/0.88 index_21=index_18),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f501,f1660])).
% 0.23/0.88 fof(f1666,plain,(
% 0.23/0.88 rselect_head(queue_191)=rselect_head(q37)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f592,f358])).
% 0.23/0.88 fof(f1669,plain,(
% 0.23/0.88 q38=rstore_tail(queue_191,index_192)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f682,f593])).
% 0.23/0.88 fof(f1670,plain,(
% 0.23/0.88 rselect_tail(q38)=index_192),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1669,f354])).
% 0.23/0.88 fof(f1671,plain,(
% 0.23/0.88 rselect_head(q38)=rselect_head(queue_191)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1669,f357])).
% 0.23/0.88 fof(f1673,plain,(
% 0.23/0.88 index_195=index_192),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f496,f1670])).
% 0.23/0.88 fof(f1676,plain,(
% 0.23/0.88 p(index_9)=index_21),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1663,f1395])).
% 0.23/0.88 fof(f1677,plain,(
% 0.23/0.88 s(index_21)=index_9),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1663,f1340])).
% 0.23/0.88 fof(f1679,plain,(
% 0.23/0.88 p(index_21)=index_15),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1663,f816])).
% 0.23/0.88 fof(f1681,plain,(
% 0.23/0.88 index_21=s(index_15)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1663,f490])).
% 0.23/0.88 fof(f1684,plain,(
% 0.23/0.88 p(index_195)=index_189),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1673,f832])).
% 0.23/0.88 fof(f1690,plain,(
% 0.23/0.88 rselect_head(queue_197)=rselect_head(q38)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f594,f358])).
% 0.23/0.88 fof(f1696,plain,(
% 0.23/0.88 p(index_171)=index_105),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1648,f1541])).
% 0.23/0.88 fof(f1699,plain,(
% 0.23/0.88 s(index_105)=index_171),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1696,f362])).
% 0.23/0.88 fof(f1700,plain,(
% 0.23/0.88 index_111=index_171),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1192,f1699])).
% 0.23/0.88 fof(f1710,plain,(
% 0.23/0.88 q39=rstore_tail(queue_197,index_198)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f683,f595])).
% 0.23/0.88 fof(f1711,plain,(
% 0.23/0.88 rselect_tail(q39)=index_198),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1710,f354])).
% 0.23/0.88 fof(f1712,plain,(
% 0.23/0.88 rselect_head(q39)=rselect_head(queue_197)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1710,f357])).
% 0.23/0.88 fof(f1714,plain,(
% 0.23/0.88 index_207=index_198),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f500,f1711])).
% 0.23/0.88 fof(f1717,plain,(
% 0.23/0.88 rselect_head(queue_203)=rselect_head(q3)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f596,f358])).
% 0.23/0.88 fof(f1722,plain,(
% 0.23/0.88 p(index_207)=index_195),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1714,f836])).
% 0.23/0.88 fof(f1735,plain,(
% 0.23/0.88 p(index_177)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1700,f1584])).
% 0.23/0.88 fof(f1738,plain,(
% 0.23/0.88 s(index_111)=index_177),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1735,f362])).
% 0.23/0.88 fof(f1739,plain,(
% 0.23/0.88 index_99=index_177),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1559,f1738])).
% 0.23/0.88 fof(f1753,plain,(
% 0.23/0.88 q4=rstore_tail(queue_203,index_204)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f684,f597])).
% 0.23/0.88 fof(f1754,plain,(
% 0.23/0.88 rselect_tail(q4)=index_204),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1753,f354])).
% 0.23/0.88 fof(f1755,plain,(
% 0.23/0.88 rselect_head(q4)=rselect_head(queue_203)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1753,f357])).
% 0.23/0.88 fof(f1757,plain,(
% 0.23/0.88 index_249=index_204),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f516,f1754])).
% 0.23/0.88 fof(f1760,plain,(
% 0.23/0.88 rselect_head(queue_209)=rselect_head(q39)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f598,f358])).
% 0.23/0.88 fof(f1763,plain,(
% 0.23/0.88 q40=rstore_tail(queue_209,index_210)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f685,f599])).
% 0.23/0.88 fof(f1764,plain,(
% 0.23/0.88 rselect_tail(q40)=index_210),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1763,f354])).
% 0.23/0.88 fof(f1765,plain,(
% 0.23/0.88 rselect_head(q40)=rselect_head(queue_209)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1763,f357])).
% 0.23/0.88 fof(f1767,plain,(
% 0.23/0.88 index_213=index_210),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f503,f1764])).
% 0.23/0.88 fof(f1770,plain,(
% 0.23/0.88 p(index_135)=index_249),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1757,f1552])).
% 0.23/0.88 fof(f1771,plain,(
% 0.23/0.88 s(index_249)=index_135),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1757,f1442])).
% 0.23/0.88 fof(f1773,plain,(
% 0.23/0.88 p(index_249)=index_201),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1757,f840])).
% 0.23/0.88 fof(f1775,plain,(
% 0.23/0.88 index_249=s(index_201)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1757,f499])).
% 0.23/0.88 fof(f1778,plain,(
% 0.23/0.88 p(index_213)=index_207),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1767,f844])).
% 0.23/0.88 fof(f1784,plain,(
% 0.23/0.88 rselect_head(queue_215)=rselect_head(q40)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f600,f358])).
% 0.23/0.88 fof(f1787,plain,(
% 0.23/0.88 p(index_183)=index_99),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1739,f1598])).
% 0.23/0.88 fof(f1790,plain,(
% 0.23/0.88 s(index_99)=index_183),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1787,f362])).
% 0.23/0.88 fof(f1791,plain,(
% 0.23/0.88 index_105=index_183),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1153,f1790])).
% 0.23/0.88 fof(f1805,plain,(
% 0.23/0.88 p(index_189)=index_105),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1791,f1622])).
% 0.23/0.88 fof(f1808,plain,(
% 0.23/0.88 s(index_105)=index_189),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1805,f362])).
% 0.23/0.88 fof(f1809,plain,(
% 0.23/0.88 index_111=index_189),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1192,f1808])).
% 0.23/0.88 fof(f1810,plain,(
% 0.23/0.88 q41=rstore_tail(queue_215,index_216)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f686,f601])).
% 0.23/0.88 fof(f1811,plain,(
% 0.23/0.88 rselect_tail(q41)=index_216),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1810,f354])).
% 0.23/0.88 fof(f1812,plain,(
% 0.23/0.88 rselect_head(q41)=rselect_head(queue_215)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1810,f357])).
% 0.23/0.88 fof(f1814,plain,(
% 0.23/0.88 index_219=index_216),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f505,f1811])).
% 0.23/0.88 fof(f1817,plain,(
% 0.23/0.88 rselect_head(queue_221)=rselect_head(q41)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f602,f358])).
% 0.23/0.88 fof(f1829,plain,(
% 0.23/0.88 p(index_219)=index_213),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1814,f848])).
% 0.23/0.88 fof(f1844,plain,(
% 0.23/0.88 q42=rstore_tail(queue_221,index_222)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f687,f603])).
% 0.23/0.88 fof(f1845,plain,(
% 0.23/0.88 rselect_tail(q42)=index_222),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1844,f354])).
% 0.23/0.88 fof(f1846,plain,(
% 0.23/0.88 rselect_head(q42)=rselect_head(queue_221)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1844,f357])).
% 0.23/0.88 fof(f1848,plain,(
% 0.23/0.88 index_225=index_222),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f507,f1845])).
% 0.23/0.88 fof(f1851,plain,(
% 0.23/0.88 rselect_head(queue_227)=rselect_head(q42)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f604,f358])).
% 0.23/0.88 fof(f1854,plain,(
% 0.23/0.88 q43=rstore_tail(queue_227,index_228)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f688,f605])).
% 0.23/0.88 fof(f1855,plain,(
% 0.23/0.88 rselect_tail(q43)=index_228),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1854,f354])).
% 0.23/0.88 fof(f1856,plain,(
% 0.23/0.88 rselect_head(q43)=rselect_head(queue_227)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1854,f357])).
% 0.23/0.88 fof(f1858,plain,(
% 0.23/0.88 index_231=index_228),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f509,f1855])).
% 0.23/0.88 fof(f1862,plain,(
% 0.23/0.88 p(index_225)=index_219),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1848,f852])).
% 0.23/0.88 fof(f1868,plain,(
% 0.23/0.88 p(index_231)=index_225),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1858,f862])).
% 0.23/0.88 fof(f1875,plain,(
% 0.23/0.88 rselect_head(queue_23)=rselect_head(q11)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f606,f358])).
% 0.23/0.88 fof(f1885,plain,(
% 0.23/0.88 index_24=index_9),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1677,f512])).
% 0.23/0.88 fof(f1906,plain,(
% 0.23/0.88 p(index_195)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1809,f1684])).
% 0.23/0.88 fof(f1909,plain,(
% 0.23/0.88 s(index_111)=index_195),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1906,f362])).
% 0.23/0.88 fof(f1910,plain,(
% 0.23/0.88 index_99=index_195),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1559,f1909])).
% 0.23/0.88 fof(f1919,plain,(
% 0.23/0.88 rselect_head(queue_233)=rselect_head(q43)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f607,f358])).
% 0.23/0.88 fof(f1922,plain,(
% 0.23/0.88 q44=rstore_tail(queue_233,index_234)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f689,f608])).
% 0.23/0.88 fof(f1923,plain,(
% 0.23/0.88 rselect_tail(q44)=index_234),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1922,f354])).
% 0.23/0.88 fof(f1924,plain,(
% 0.23/0.88 rselect_head(q44)=rselect_head(queue_233)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1922,f357])).
% 0.23/0.88 fof(f1926,plain,(
% 0.23/0.88 index_237=index_234),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f511,f1923])).
% 0.23/0.88 fof(f1930,plain,(
% 0.23/0.88 p(index_237)=index_231),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1926,f866])).
% 0.23/0.88 fof(f1943,plain,(
% 0.23/0.88 p(index_207)=index_99),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1910,f1722])).
% 0.23/0.88 fof(f1946,plain,(
% 0.23/0.88 s(index_99)=index_207),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1943,f362])).
% 0.23/0.88 fof(f1947,plain,(
% 0.23/0.88 index_105=index_207),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1153,f1946])).
% 0.23/0.88 fof(f1956,plain,(
% 0.23/0.88 rselect_head(queue_239)=rselect_head(q44)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f609,f358])).
% 0.23/0.88 fof(f1959,plain,(
% 0.23/0.88 q45=rstore_tail(queue_239,index_240)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f690,f610])).
% 0.23/0.88 fof(f1960,plain,(
% 0.23/0.88 rselect_tail(q45)=index_240),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1959,f354])).
% 0.23/0.88 fof(f1961,plain,(
% 0.23/0.88 rselect_head(q45)=rselect_head(queue_239)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1959,f357])).
% 0.23/0.88 fof(f1963,plain,(
% 0.23/0.88 index_243=index_240),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f514,f1960])).
% 0.23/0.88 fof(f1966,plain,(
% 0.23/0.88 rselect_head(queue_245)=rselect_head(q45)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f611,f358])).
% 0.23/0.88 fof(f1967,plain,(
% 0.23/0.88 rselect_seq(queue_245)=earray_244),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f611,f352])).
% 0.23/0.88 fof(f1971,plain,(
% 0.23/0.88 p(index_243)=index_237),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1963,f876])).
% 0.23/0.88 fof(f1978,plain,(
% 0.23/0.88 q46=rstore_tail(queue_245,index_246)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f691,f612])).
% 0.23/0.88 fof(f1979,plain,(
% 0.23/0.88 rselect_tail(q46)=index_246),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1978,f354])).
% 0.23/0.88 fof(f1980,plain,(
% 0.23/0.88 rselect_head(q46)=rselect_head(queue_245)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1978,f357])).
% 0.23/0.88 fof(f1981,plain,(
% 0.23/0.88 rselect_seq(q46)=rselect_seq(queue_245)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f1978,f356])).
% 0.23/0.88 fof(f1982,plain,(
% 0.23/0.88 index_279=rselect_head(queue_245)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f527,f1980])).
% 0.23/0.88 fof(f1983,plain,(
% 0.23/0.88 earray_278=rselect_seq(queue_245)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f432,f1981])).
% 0.23/0.88 fof(f1997,plain,(
% 0.23/0.88 index_252=index_135),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1771,f517])).
% 0.23/0.88 fof(f2004,plain,(
% 0.23/0.88 q12=rstore_tail(queue_23,index_24)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f654,f613])).
% 0.23/0.88 fof(f2005,plain,(
% 0.23/0.88 q12=rstore_tail(queue_23,index_9)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1885,f2004])).
% 0.23/0.88 fof(f2006,plain,(
% 0.23/0.88 rselect_tail(q12)=index_9),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2005,f354])).
% 0.23/0.88 fof(f2007,plain,(
% 0.23/0.88 rselect_head(q12)=rselect_head(queue_23)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2005,f357])).
% 0.23/0.88 fof(f2011,plain,(
% 0.23/0.88 rselect_head(queue_251)=rselect_head(q4)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f614,f358])).
% 0.23/0.88 fof(f2028,plain,(
% 0.23/0.88 p(index_213)=index_105),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1947,f1778])).
% 0.23/0.88 fof(f2031,plain,(
% 0.23/0.88 s(index_105)=index_213),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2028,f362])).
% 0.23/0.88 fof(f2032,plain,(
% 0.23/0.88 index_111=index_213),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1192,f2031])).
% 0.23/0.88 fof(f2050,plain,(
% 0.23/0.88 q5=rstore_tail(queue_251,index_252)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f692,f615])).
% 0.23/0.88 fof(f2051,plain,(
% 0.23/0.88 q5=rstore_tail(queue_251,index_135)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1997,f2050])).
% 0.23/0.88 fof(f2052,plain,(
% 0.23/0.88 rselect_tail(q5)=index_135),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2051,f354])).
% 0.23/0.88 fof(f2053,plain,(
% 0.23/0.88 rselect_head(q5)=rselect_head(queue_251)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2051,f357])).
% 0.23/0.88 fof(f2057,plain,(
% 0.23/0.88 rselect_head(queue_257)=rselect_head(q5)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f616,f358])).
% 0.23/0.88 fof(f2060,plain,(
% 0.23/0.88 q6=rstore_tail(queue_257,index_258)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f693,f617])).
% 0.23/0.88 fof(f2061,plain,(
% 0.23/0.88 rselect_tail(q6)=index_258),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2060,f354])).
% 0.23/0.88 fof(f2062,plain,(
% 0.23/0.88 rselect_head(q6)=rselect_head(queue_257)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2060,f357])).
% 0.23/0.88 fof(f2064,plain,(
% 0.23/0.88 index_261=index_258),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f520,f2061])).
% 0.23/0.88 fof(f2067,plain,(
% 0.23/0.88 p(index_261)=index_255),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2064,f892])).
% 0.23/0.88 fof(f2072,plain,(
% 0.23/0.88 p(index_219)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2032,f1829])).
% 0.23/0.88 fof(f2075,plain,(
% 0.23/0.88 s(index_111)=index_219),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2072,f362])).
% 0.23/0.88 fof(f2076,plain,(
% 0.23/0.88 index_99=index_219),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1559,f2075])).
% 0.23/0.88 fof(f2086,plain,(
% 0.23/0.88 rselect_head(queue_263)=rselect_head(q6)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f618,f358])).
% 0.23/0.88 fof(f2097,plain,(
% 0.23/0.88 p(index_225)=index_99),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2076,f1862])).
% 0.23/0.88 fof(f2100,plain,(
% 0.23/0.88 s(index_99)=index_225),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2097,f362])).
% 0.23/0.88 fof(f2101,plain,(
% 0.23/0.88 index_105=index_225),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1153,f2100])).
% 0.23/0.88 fof(f2110,plain,(
% 0.23/0.88 q7=rstore_tail(queue_263,index_264)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f694,f619])).
% 0.23/0.88 fof(f2111,plain,(
% 0.23/0.88 rselect_tail(q7)=index_264),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2110,f354])).
% 0.23/0.88 fof(f2112,plain,(
% 0.23/0.88 rselect_head(q7)=rselect_head(queue_263)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2110,f357])).
% 0.23/0.88 fof(f2114,plain,(
% 0.23/0.88 index_267=index_264),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f522,f2111])).
% 0.23/0.88 fof(f2117,plain,(
% 0.23/0.88 rselect_head(queue_269)=rselect_head(q7)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f620,f358])).
% 0.23/0.88 fof(f2122,plain,(
% 0.23/0.88 p(index_267)=index_261),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2114,f896])).
% 0.23/0.88 fof(f2129,plain,(
% 0.23/0.88 p(index_231)=index_105),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2101,f1868])).
% 0.23/0.88 fof(f2132,plain,(
% 0.23/0.88 s(index_105)=index_231),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2129,f362])).
% 0.23/0.88 fof(f2133,plain,(
% 0.23/0.88 index_111=index_231),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1192,f2132])).
% 0.23/0.88 fof(f2143,plain,(
% 0.23/0.88 q8=rstore_tail(queue_269,index_270)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f695,f621])).
% 0.23/0.88 fof(f2144,plain,(
% 0.23/0.88 rselect_tail(q8)=index_270),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2143,f354])).
% 0.23/0.88 fof(f2145,plain,(
% 0.23/0.88 rselect_head(q8)=rselect_head(queue_269)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2143,f357])).
% 0.23/0.88 fof(f2147,plain,(
% 0.23/0.88 index_273=index_270),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f525,f2144])).
% 0.23/0.88 fof(f2150,plain,(
% 0.23/0.88 rselect_head(queue_275)=rselect_head(q8)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f622,f358])).
% 0.23/0.88 fof(f2153,plain,(
% 0.23/0.88 q9=rstore_tail(queue_275,index_276)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f696,f623])).
% 0.23/0.88 fof(f2154,plain,(
% 0.23/0.88 rselect_tail(q9)=index_276),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2153,f354])).
% 0.23/0.88 fof(f2155,plain,(
% 0.23/0.88 rselect_head(q9)=rselect_head(queue_275)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2153,f357])).
% 0.23/0.88 fof(f2157,plain,(
% 0.23/0.88 index_9=index_276),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f552,f2154])).
% 0.23/0.88 fof(f2161,plain,(
% 0.23/0.88 p(index_273)=index_267),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2147,f900])).
% 0.23/0.88 fof(f2167,plain,(
% 0.23/0.88 p(index_9)=index_273),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2157,f904])).
% 0.23/0.88 fof(f2171,plain,(
% 0.23/0.88 index_21=index_273),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1676,f2167])).
% 0.23/0.88 fof(f2180,plain,(
% 0.23/0.88 rselect_head(queue_29)=rselect_head(q12)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f624,f358])).
% 0.23/0.88 fof(f2191,plain,(
% 0.23/0.88 p(index_237)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2133,f1930])).
% 0.23/0.88 fof(f2194,plain,(
% 0.23/0.88 s(index_111)=index_237),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2191,f362])).
% 0.23/0.88 fof(f2195,plain,(
% 0.23/0.88 index_99=index_237),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1559,f2194])).
% 0.23/0.88 fof(f2196,plain,(
% 0.23/0.88 q13=rstore_tail(queue_29,index_30)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f655,f625])).
% 0.23/0.88 fof(f2197,plain,(
% 0.23/0.88 rselect_tail(q13)=index_30),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2196,f354])).
% 0.23/0.88 fof(f2198,plain,(
% 0.23/0.88 rselect_head(q13)=rselect_head(queue_29)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2196,f357])).
% 0.23/0.88 fof(f2200,plain,(
% 0.23/0.88 index_33=index_30),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f532,f2197])).
% 0.23/0.88 fof(f2203,plain,(
% 0.23/0.88 rselect_head(queue_35)=rselect_head(q13)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f626,f358])).
% 0.23/0.88 fof(f2214,plain,(
% 0.23/0.88 p(index_33)=index_27),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2200,f908])).
% 0.23/0.88 fof(f2227,plain,(
% 0.23/0.88 earray_278=earray_244),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f1967,f1983])).
% 0.23/0.88 fof(f2229,plain,(
% 0.23/0.88 elem_283=select(earray_244,index_282)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2227,f460])).
% 0.23/0.88 fof(f2230,plain,(
% 0.23/0.88 elem_280=select(earray_244,index_279)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2227,f459])).
% 0.23/0.88 fof(f2231,plain,(
% 0.23/0.88 q14=rstore_tail(queue_35,index_36)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f656,f627])).
% 0.23/0.88 fof(f2232,plain,(
% 0.23/0.88 rselect_tail(q14)=index_36),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2231,f354])).
% 0.23/0.88 fof(f2233,plain,(
% 0.23/0.88 rselect_head(q14)=rselect_head(queue_35)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2231,f357])).
% 0.23/0.88 fof(f2235,plain,(
% 0.23/0.88 index_39=index_36),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f534,f2232])).
% 0.23/0.88 fof(f2238,plain,(
% 0.23/0.88 rselect_head(queue_41)=rselect_head(q14)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f628,f358])).
% 0.23/0.88 fof(f2241,plain,(
% 0.23/0.88 q15=rstore_tail(queue_41,index_42)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f657,f629])).
% 0.23/0.88 fof(f2242,plain,(
% 0.23/0.88 rselect_tail(q15)=index_42),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2241,f354])).
% 0.23/0.88 fof(f2243,plain,(
% 0.23/0.88 rselect_head(q15)=rselect_head(queue_41)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2241,f357])).
% 0.23/0.88 fof(f2245,plain,(
% 0.23/0.88 index_45=index_42),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f536,f2242])).
% 0.23/0.88 fof(f2249,plain,(
% 0.23/0.88 p(index_39)=index_33),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2235,f918])).
% 0.23/0.88 fof(f2255,plain,(
% 0.23/0.88 p(index_45)=index_39),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2245,f922])).
% 0.23/0.88 fof(f2262,plain,(
% 0.23/0.88 rselect_head(queue_47)=rselect_head(q15)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f630,f358])).
% 0.23/0.88 fof(f2265,plain,(
% 0.23/0.88 p(index_243)=index_99),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2195,f1971])).
% 0.23/0.88 fof(f2268,plain,(
% 0.23/0.88 s(index_99)=index_243),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2265,f362])).
% 0.23/0.88 fof(f2270,plain,(
% 0.23/0.88 index_105=index_243),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1153,f2268])).
% 0.23/0.88 fof(f2279,plain,(
% 0.23/0.88 index_246=s(index_105)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2270,f515])).
% 0.23/0.88 fof(f2281,plain,(
% 0.23/0.88 index_246=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1192,f2279])).
% 0.23/0.88 fof(f2287,plain,(
% 0.23/0.88 index_281=index_111),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2288,f528])).
% 0.23/0.88 fof(f2288,plain,(
% 0.23/0.88 rselect_tail(q46)=index_111),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2281,f1979])).
% 0.23/0.88 fof(f2289,plain,(
% 0.23/0.88 p(index_111)=index_282),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2287,f712])).
% 0.23/0.88 fof(f2294,plain,(
% 0.23/0.88 index_105=index_282),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1189,f2289])).
% 0.23/0.88 fof(f2298,plain,(
% 0.23/0.88 elem_283=select(earray_244,index_105)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2294,f2229])).
% 0.23/0.88 fof(f2299,plain,(
% 0.23/0.88 q16=rstore_tail(queue_47,index_48)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f658,f631])).
% 0.23/0.88 fof(f2300,plain,(
% 0.23/0.88 rselect_tail(q16)=index_48),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2299,f354])).
% 0.23/0.88 fof(f2301,plain,(
% 0.23/0.88 rselect_head(q16)=rselect_head(queue_47)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2299,f357])).
% 0.23/0.88 fof(f2303,plain,(
% 0.23/0.88 index_51=index_48),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f538,f2300])).
% 0.23/0.88 fof(f2309,plain,(
% 0.23/0.88 p(index_51)=index_45),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2303,f928])).
% 0.23/0.88 fof(f2314,plain,(
% 0.23/0.88 index_27=index_9),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2006,f523])).
% 0.23/0.88 fof(f2321,plain,(
% 0.23/0.88 rselect_head(queue_5)=rselect_head(q0)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f632,f358])).
% 0.23/0.88 fof(f2324,plain,(
% 0.23/0.88 rselect_head(queue_5)=index_3),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1169,f2321])).
% 0.23/0.88 fof(f2326,plain,(
% 0.23/0.88 rselect_head(queue_53)=rselect_head(q16)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f633,f358])).
% 0.23/0.88 fof(f2329,plain,(
% 0.23/0.88 q17=rstore_tail(queue_53,index_54)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f659,f634])).
% 0.23/0.88 fof(f2330,plain,(
% 0.23/0.88 rselect_tail(q17)=index_54),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2329,f354])).
% 0.23/0.88 fof(f2331,plain,(
% 0.23/0.88 rselect_head(q17)=rselect_head(queue_53)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2329,f357])).
% 0.23/0.88 fof(f2333,plain,(
% 0.23/0.88 index_57=index_54),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f540,f2330])).
% 0.23/0.88 fof(f2337,plain,(
% 0.23/0.88 p(index_57)=index_51),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2333,f932])).
% 0.23/0.88 fof(f2345,plain,(
% 0.23/0.88 rselect_head(queue_59)=rselect_head(q17)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f635,f358])).
% 0.23/0.88 fof(f2348,plain,(
% 0.23/0.88 index_255=index_135),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2052,f518])).
% 0.23/0.88 fof(f2358,plain,(
% 0.23/0.88 p(index_261)=index_135),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f2348,f2067])).
% 0.23/0.88 fof(f2361,plain,(
% 0.23/0.88 s(index_135)=index_261),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2358,f362])).
% 0.23/0.88 fof(f2362,plain,(
% 0.23/0.88 index_201=index_261),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f1376,f2361])).
% 0.23/0.88 fof(f2369,plain,(
% 0.23/0.88 q18=rstore_tail(queue_59,index_60)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f660,f636])).
% 0.23/0.88 fof(f2370,plain,(
% 0.23/0.88 rselect_tail(q18)=index_60),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2369,f354])).
% 0.23/0.88 fof(f2371,plain,(
% 0.23/0.88 rselect_head(q18)=rselect_head(queue_59)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2369,f357])).
% 0.23/0.88 fof(f2373,plain,(
% 0.23/0.88 index_63=index_60),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f543,f2370])).
% 0.23/0.88 fof(f2376,plain,(
% 0.23/0.88 rselect_head(queue_65)=rselect_head(q18)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f637,f358])).
% 0.23/0.88 fof(f2381,plain,(
% 0.23/0.88 p(index_63)=index_57),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2373,f940])).
% 0.23/0.88 fof(f2393,plain,(
% 0.23/0.88 q19=rstore_tail(queue_65,index_66)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f661,f638])).
% 0.23/0.88 fof(f2394,plain,(
% 0.23/0.88 rselect_tail(q19)=index_66),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2393,f354])).
% 0.23/0.88 fof(f2395,plain,(
% 0.23/0.88 rselect_head(q19)=rselect_head(queue_65)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2393,f357])).
% 0.23/0.88 fof(f2397,plain,(
% 0.23/0.88 index_75=index_66),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f547,f2394])).
% 0.23/0.88 fof(f2399,plain,(
% 0.23/0.88 q1=rstore_tail(queue_5,index_6)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f651,f639])).
% 0.23/0.88 fof(f2400,plain,(
% 0.23/0.88 rselect_tail(q1)=index_6),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2399,f354])).
% 0.23/0.88 fof(f2403,plain,(
% 0.23/0.88 index_69=index_6),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f545,f2400])).
% 0.23/0.88 fof(f2406,plain,(
% 0.23/0.88 rselect_head(queue_71)=rselect_head(q1)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f640,f358])).
% 0.23/0.88 fof(f2411,plain,(
% 0.23/0.88 p(index_75)=index_63),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2397,f944])).
% 0.23/0.88 fof(f2416,plain,(
% 0.23/0.88 q1=rstore_tail(queue_5,index_69)),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2403,f2399])).
% 0.23/0.88 fof(f2417,plain,(
% 0.23/0.88 p(index_69)=index_3),
% 0.23/0.88 inference(backward_demodulation,[status(thm)],[f2403,f936])).
% 0.23/0.88 fof(f2422,plain,(
% 0.23/0.88 q2=rstore_tail(queue_71,index_72)),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f662,f641])).
% 0.23/0.88 fof(f2423,plain,(
% 0.23/0.88 rselect_tail(q2)=index_72),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2422,f354])).
% 0.23/0.88 fof(f2424,plain,(
% 0.23/0.88 rselect_head(q2)=rselect_head(queue_71)),
% 0.23/0.88 inference(paramodulation,[status(thm)],[f2422,f357])).
% 0.23/0.88 fof(f2426,plain,(
% 0.23/0.88 index_135=index_72),
% 0.23/0.88 inference(forward_demodulation,[status(thm)],[f474,f2423])).
% 0.23/0.89 fof(f2430,plain,(
% 0.23/0.89 p(index_135)=index_69),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2426,f952])).
% 0.23/0.89 fof(f2433,plain,(
% 0.23/0.89 index_135=s(index_69)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2426,f546])).
% 0.23/0.89 fof(f2434,plain,(
% 0.23/0.89 index_249=index_69),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1770,f2430])).
% 0.23/0.89 fof(f2445,plain,(
% 0.23/0.89 p(index_267)=index_201),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2362,f2122])).
% 0.23/0.89 fof(f2448,plain,(
% 0.23/0.89 s(index_201)=index_267),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2445,f362])).
% 0.23/0.89 fof(f2449,plain,(
% 0.23/0.89 index_249=index_267),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1775,f2448])).
% 0.23/0.89 fof(f2451,plain,(
% 0.23/0.89 rselect_head(queue_77)=rselect_head(q19)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f642,f358])).
% 0.23/0.89 fof(f2454,plain,(
% 0.23/0.89 q20=rstore_tail(queue_77,index_78)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f663,f643])).
% 0.23/0.89 fof(f2455,plain,(
% 0.23/0.89 rselect_tail(q20)=index_78),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2454,f354])).
% 0.23/0.89 fof(f2456,plain,(
% 0.23/0.89 rselect_head(q20)=rselect_head(queue_77)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2454,f357])).
% 0.23/0.89 fof(f2458,plain,(
% 0.23/0.89 index_81=index_78),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f549,f2455])).
% 0.23/0.89 fof(f2470,plain,(
% 0.23/0.89 p(index_81)=index_75),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2458,f956])).
% 0.23/0.89 fof(f2484,plain,(
% 0.23/0.89 p(index_21)=index_267),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2171,f2161])).
% 0.23/0.89 fof(f2485,plain,(
% 0.23/0.89 index_249=index_15),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2486,f2449])).
% 0.23/0.89 fof(f2486,plain,(
% 0.23/0.89 index_15=index_267),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1679,f2484])).
% 0.23/0.89 fof(f2492,plain,(
% 0.23/0.89 index_15=index_69),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2485,f2434])).
% 0.23/0.89 fof(f2495,plain,(
% 0.23/0.89 p(index_15)=index_201),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2485,f1773])).
% 0.23/0.89 fof(f2502,plain,(
% 0.23/0.89 index_9=index_201),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1286,f2495])).
% 0.23/0.89 fof(f2504,plain,(
% 0.23/0.89 rselect_head(queue_83)=rselect_head(q20)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f644,f358])).
% 0.23/0.89 fof(f2507,plain,(
% 0.23/0.89 q21=rstore_tail(queue_83,index_84)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f664,f645])).
% 0.23/0.89 fof(f2508,plain,(
% 0.23/0.89 rselect_tail(q21)=index_84),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2507,f354])).
% 0.23/0.89 fof(f2509,plain,(
% 0.23/0.89 rselect_head(q21)=rselect_head(queue_83)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2507,f357])).
% 0.23/0.89 fof(f2511,plain,(
% 0.23/0.89 index_87=index_84),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f551,f2508])).
% 0.23/0.89 fof(f2514,plain,(
% 0.23/0.89 rselect_head(queue_89)=rselect_head(q21)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f646,f358])).
% 0.23/0.89 fof(f2522,plain,(
% 0.23/0.89 index_9=s(index_135)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2502,f1376])).
% 0.23/0.89 fof(f2528,plain,(
% 0.23/0.89 q22=rstore_tail(queue_89,index_90)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f665,f647])).
% 0.23/0.89 fof(f2529,plain,(
% 0.23/0.89 rselect_tail(q22)=index_90),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2528,f354])).
% 0.23/0.89 fof(f2530,plain,(
% 0.23/0.89 rselect_head(q22)=rselect_head(queue_89)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2528,f357])).
% 0.23/0.89 fof(f2532,plain,(
% 0.23/0.89 index_93=index_90),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f554,f2529])).
% 0.23/0.89 fof(f2536,plain,(
% 0.23/0.89 p(index_87)=index_81),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2511,f960])).
% 0.23/0.89 fof(f2542,plain,(
% 0.23/0.89 p(index_93)=index_87),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2532,f964])).
% 0.23/0.89 fof(f2545,plain,(
% 0.23/0.89 index_93=s(index_87)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2532,f553])).
% 0.23/0.89 fof(f2549,plain,(
% 0.23/0.89 rselect_head(queue_95)=rselect_head(q22)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f648,f358])).
% 0.23/0.89 fof(f2552,plain,(
% 0.23/0.89 q23=rstore_tail(queue_95,index_96)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f666,f649])).
% 0.23/0.89 fof(f2553,plain,(
% 0.23/0.89 rselect_tail(q23)=index_96),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2552,f354])).
% 0.23/0.89 fof(f2554,plain,(
% 0.23/0.89 rselect_head(q23)=rselect_head(queue_95)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2552,f357])).
% 0.23/0.89 fof(f2556,plain,(
% 0.23/0.89 index_99=index_96),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f556,f2553])).
% 0.23/0.89 fof(f2560,plain,(
% 0.23/0.89 p(index_99)=index_93),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2556,f968])).
% 0.23/0.89 fof(f2564,plain,(
% 0.23/0.89 index_111=index_93),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1477,f2560])).
% 0.23/0.89 fof(f2593,plain,(
% 0.23/0.89 p(index_33)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2314,f2214])).
% 0.23/0.89 fof(f2596,plain,(
% 0.23/0.89 s(index_9)=index_33),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2593,f362])).
% 0.23/0.89 fof(f2597,plain,(
% 0.23/0.89 index_15=index_33),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1289,f2596])).
% 0.23/0.89 fof(f2617,plain,(
% 0.23/0.89 p(index_39)=index_15),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2597,f2249])).
% 0.23/0.89 fof(f2620,plain,(
% 0.23/0.89 s(index_15)=index_39),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2617,f362])).
% 0.23/0.89 fof(f2621,plain,(
% 0.23/0.89 index_21=index_39),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1681,f2620])).
% 0.23/0.89 fof(f2639,plain,(
% 0.23/0.89 p(index_45)=index_21),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2621,f2255])).
% 0.23/0.89 fof(f2642,plain,(
% 0.23/0.89 s(index_21)=index_45),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2639,f362])).
% 0.23/0.89 fof(f2643,plain,(
% 0.23/0.89 index_9=index_45),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1677,f2642])).
% 0.23/0.89 fof(f2661,plain,(
% 0.23/0.89 p(index_51)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2643,f2309])).
% 0.23/0.89 fof(f2664,plain,(
% 0.23/0.89 s(index_9)=index_51),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2661,f362])).
% 0.23/0.89 fof(f2665,plain,(
% 0.23/0.89 index_15=index_51),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1289,f2664])).
% 0.23/0.89 fof(f2695,plain,(
% 0.23/0.89 p(index_57)=index_15),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2665,f2337])).
% 0.23/0.89 fof(f2698,plain,(
% 0.23/0.89 s(index_15)=index_57),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2695,f362])).
% 0.23/0.89 fof(f2699,plain,(
% 0.23/0.89 index_21=index_57),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1681,f2698])).
% 0.23/0.89 fof(f2722,plain,(
% 0.23/0.89 p(index_63)=index_21),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2699,f2381])).
% 0.23/0.89 fof(f2725,plain,(
% 0.23/0.89 s(index_21)=index_63),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2722,f362])).
% 0.23/0.89 fof(f2726,plain,(
% 0.23/0.89 index_9=index_63),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1677,f2725])).
% 0.23/0.89 fof(f2743,plain,(
% 0.23/0.89 p(index_75)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2726,f2411])).
% 0.23/0.89 fof(f2746,plain,(
% 0.23/0.89 s(index_9)=index_75),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2743,f362])).
% 0.23/0.89 fof(f2747,plain,(
% 0.23/0.89 index_15=index_75),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1289,f2746])).
% 0.23/0.89 fof(f2768,plain,(
% 0.23/0.89 p(index_15)=index_3),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2492,f2417])).
% 0.23/0.89 fof(f2769,plain,(
% 0.23/0.89 rselect_head(queue_5)=index_9),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2779,f2324])).
% 0.23/0.89 fof(f2779,plain,(
% 0.23/0.89 index_9=index_3),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1286,f2768])).
% 0.23/0.89 fof(f2790,plain,(
% 0.23/0.89 index_135=s(index_15)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2492,f2433])).
% 0.23/0.89 fof(f2830,plain,(
% 0.23/0.89 p(index_81)=index_15),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2747,f2470])).
% 0.23/0.89 fof(f2833,plain,(
% 0.23/0.89 s(index_15)=index_81),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2830,f362])).
% 0.23/0.89 fof(f2834,plain,(
% 0.23/0.89 index_135=index_81),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2790,f2833])).
% 0.23/0.89 fof(f2882,plain,(
% 0.23/0.89 p(index_87)=index_135),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2834,f2536])).
% 0.23/0.89 fof(f2885,plain,(
% 0.23/0.89 s(index_135)=index_87),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f2882,f362])).
% 0.23/0.89 fof(f2886,plain,(
% 0.23/0.89 index_9=index_87),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2522,f2885])).
% 0.23/0.89 fof(f2905,plain,(
% 0.23/0.89 p(index_111)=index_87),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2564,f2542])).
% 0.23/0.89 fof(f2906,plain,(
% 0.23/0.89 index_105=index_87),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1189,f2905])).
% 0.23/0.89 fof(f2918,plain,(
% 0.23/0.89 elem_283=select(earray_244,index_9)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2953,f2298])).
% 0.23/0.89 fof(f2921,plain,(
% 0.23/0.89 index_9=index_243),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2953,f2270])).
% 0.23/0.89 fof(f2953,plain,(
% 0.23/0.89 index_105=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2886,f2906])).
% 0.23/0.89 fof(f2967,plain,(
% 0.23/0.89 index_111=s(index_87)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2564,f2545])).
% 0.23/0.89 fof(f2968,plain,(
% 0.23/0.89 index_15=index_111),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2969,f1289])).
% 0.23/0.89 fof(f2969,plain,(
% 0.23/0.89 index_111=s(index_9)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2886,f2967])).
% 0.23/0.89 fof(f2996,plain,(
% 0.23/0.89 index_111=index_69),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f2968,f2492])).
% 0.23/0.89 fof(f3374,plain,(
% 0.23/0.89 elem_283=e45),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f3375,f2918])).
% 0.23/0.89 fof(f3375,plain,(
% 0.23/0.89 select(earray_244,index_9)=e45),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2921,f914])).
% 0.23/0.89 fof(f3376,plain,(
% 0.23/0.89 ~elem_280=e45),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f3374,f697])).
% 0.23/0.89 fof(f3461,plain,(
% 0.23/0.89 rselect_head(q24)=rselect_head(q23)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f1141,f1118])).
% 0.23/0.89 fof(f3462,plain,(
% 0.23/0.89 rselect_head(q25)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1146,f1175])).
% 0.23/0.89 fof(f3463,plain,(
% 0.23/0.89 rselect_head(queue_113)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3462,f1184])).
% 0.23/0.89 fof(f3464,plain,(
% 0.23/0.89 rselect_head(q26)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3463,f1199])).
% 0.23/0.89 fof(f3467,plain,(
% 0.23/0.89 rselect_head(queue_119)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3464,f1221])).
% 0.23/0.89 fof(f3468,plain,(
% 0.23/0.89 rselect_head(q27)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3467,f1226])).
% 0.23/0.89 fof(f3473,plain,(
% 0.23/0.89 rselect_head(queue_125)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3468,f1262])).
% 0.23/0.89 fof(f3474,plain,(
% 0.23/0.89 rselect_head(q28)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3473,f1267])).
% 0.23/0.89 fof(f3475,plain,(
% 0.23/0.89 rselect_head(q10)=rselect_head(q9)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f1273,f1180])).
% 0.23/0.89 fof(f3476,plain,(
% 0.23/0.89 rselect_head(queue_131)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3474,f1294])).
% 0.23/0.89 fof(f3480,plain,(
% 0.23/0.89 rselect_head(q29)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3476,f1306])).
% 0.23/0.89 fof(f3497,plain,(
% 0.23/0.89 rselect_head(q3)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1311,f1357])).
% 0.23/0.89 fof(f3498,plain,(
% 0.23/0.89 rselect_head(queue_143)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3480,f1363])).
% 0.23/0.89 fof(f3499,plain,(
% 0.23/0.89 rselect_head(q30)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3498,f1368])).
% 0.23/0.89 fof(f3500,plain,(
% 0.23/0.89 rselect_head(queue_149)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3499,f1388])).
% 0.23/0.89 fof(f3501,plain,(
% 0.23/0.89 rselect_head(q31)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3500,f1418])).
% 0.23/0.89 fof(f3502,plain,(
% 0.23/0.89 q1=rstore_tail(queue_5,index_111)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2996,f2416])).
% 0.23/0.89 fof(f3504,plain,(
% 0.23/0.89 rselect_head(q1)=rselect_head(queue_5)),
% 0.23/0.89 inference(paramodulation,[status(thm)],[f3502,f357])).
% 0.23/0.89 fof(f3506,plain,(
% 0.23/0.89 rselect_head(q1)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f2769,f3504])).
% 0.23/0.89 fof(f3508,plain,(
% 0.23/0.89 rselect_head(queue_155)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3501,f1422])).
% 0.23/0.89 fof(f3509,plain,(
% 0.23/0.89 rselect_head(q32)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3508,f1484])).
% 0.23/0.89 fof(f3510,plain,(
% 0.23/0.89 rselect_head(queue_161)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3509,f1489])).
% 0.23/0.89 fof(f3511,plain,(
% 0.23/0.89 rselect_head(q33)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3510,f1494])).
% 0.23/0.89 fof(f3512,plain,(
% 0.23/0.89 rselect_head(queue_167)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3511,f1511])).
% 0.23/0.89 fof(f3513,plain,(
% 0.23/0.89 rselect_head(q34)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3512,f1531])).
% 0.23/0.89 fof(f3514,plain,(
% 0.23/0.89 rselect_head(queue_173)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3513,f1569])).
% 0.23/0.89 fof(f3515,plain,(
% 0.23/0.89 rselect_head(q35)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3514,f1574])).
% 0.23/0.89 fof(f3516,plain,(
% 0.23/0.89 rselect_head(queue_179)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3515,f1579])).
% 0.23/0.89 fof(f3517,plain,(
% 0.23/0.89 rselect_head(q36)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3516,f1592])).
% 0.23/0.89 fof(f3528,plain,(
% 0.23/0.89 rselect_head(queue_185)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3517,f1611])).
% 0.23/0.89 fof(f3529,plain,(
% 0.23/0.89 rselect_head(q37)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3528,f1616])).
% 0.23/0.89 fof(f3530,plain,(
% 0.23/0.89 rselect_head(q11)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1536,f1661])).
% 0.23/0.89 fof(f3531,plain,(
% 0.23/0.89 rselect_head(queue_191)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3529,f1666])).
% 0.23/0.89 fof(f3532,plain,(
% 0.23/0.89 rselect_head(q38)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3531,f1671])).
% 0.23/0.89 fof(f3533,plain,(
% 0.23/0.89 rselect_head(queue_197)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3532,f1690])).
% 0.23/0.89 fof(f3534,plain,(
% 0.23/0.89 rselect_head(q39)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3533,f1712])).
% 0.23/0.89 fof(f3535,plain,(
% 0.23/0.89 rselect_head(queue_203)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3497,f1717])).
% 0.23/0.89 fof(f3536,plain,(
% 0.23/0.89 rselect_head(q4)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3535,f1755])).
% 0.23/0.89 fof(f3537,plain,(
% 0.23/0.89 rselect_head(queue_209)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3534,f1760])).
% 0.23/0.89 fof(f3538,plain,(
% 0.23/0.89 rselect_head(q40)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3537,f1765])).
% 0.23/0.89 fof(f3539,plain,(
% 0.23/0.89 rselect_head(queue_215)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3538,f1784])).
% 0.23/0.89 fof(f3540,plain,(
% 0.23/0.89 rselect_head(q41)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3539,f1812])).
% 0.23/0.89 fof(f3541,plain,(
% 0.23/0.89 rselect_head(queue_221)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3540,f1817])).
% 0.23/0.89 fof(f3542,plain,(
% 0.23/0.89 rselect_head(q42)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3541,f1846])).
% 0.23/0.89 fof(f3543,plain,(
% 0.23/0.89 rselect_head(queue_227)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3542,f1851])).
% 0.23/0.89 fof(f3544,plain,(
% 0.23/0.89 rselect_head(q43)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3543,f1856])).
% 0.23/0.89 fof(f3545,plain,(
% 0.23/0.89 rselect_head(queue_23)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3530,f1875])).
% 0.23/0.89 fof(f3558,plain,(
% 0.23/0.89 rselect_head(queue_233)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3544,f1919])).
% 0.23/0.89 fof(f3559,plain,(
% 0.23/0.89 rselect_head(q44)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3558,f1924])).
% 0.23/0.89 fof(f3560,plain,(
% 0.23/0.89 rselect_head(queue_239)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3559,f1956])).
% 0.23/0.89 fof(f3561,plain,(
% 0.23/0.89 rselect_head(q45)=rselect_head(q24)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3560,f1961])).
% 0.23/0.89 fof(f3562,plain,(
% 0.23/0.89 index_279=rselect_head(q24)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f3563,f3561])).
% 0.23/0.89 fof(f3563,plain,(
% 0.23/0.89 index_279=rselect_head(q45)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f1982,f1966])).
% 0.23/0.89 fof(f3633,plain,(
% 0.23/0.89 rselect_head(q12)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3545,f2007])).
% 0.23/0.89 fof(f3634,plain,(
% 0.23/0.89 rselect_head(queue_251)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3536,f2011])).
% 0.23/0.89 fof(f3635,plain,(
% 0.23/0.89 rselect_head(q5)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3634,f2053])).
% 0.23/0.89 fof(f3636,plain,(
% 0.23/0.89 rselect_head(queue_257)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3635,f2057])).
% 0.23/0.89 fof(f3637,plain,(
% 0.23/0.89 rselect_head(q6)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3636,f2062])).
% 0.23/0.89 fof(f3638,plain,(
% 0.23/0.89 rselect_head(queue_263)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3637,f2086])).
% 0.23/0.89 fof(f3645,plain,(
% 0.23/0.89 rselect_head(q7)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3638,f2112])).
% 0.23/0.89 fof(f3646,plain,(
% 0.23/0.89 rselect_head(queue_269)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3645,f2117])).
% 0.23/0.89 fof(f3647,plain,(
% 0.23/0.89 rselect_head(q8)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3646,f2145])).
% 0.23/0.89 fof(f3648,plain,(
% 0.23/0.89 rselect_head(queue_275)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3647,f2150])).
% 0.23/0.89 fof(f3649,plain,(
% 0.23/0.89 rselect_head(q9)=rselect_head(q2)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3648,f2155])).
% 0.23/0.89 fof(f3650,plain,(
% 0.23/0.89 rselect_head(queue_29)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3633,f2180])).
% 0.23/0.89 fof(f3651,plain,(
% 0.23/0.89 rselect_head(q13)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3650,f2198])).
% 0.23/0.89 fof(f3652,plain,(
% 0.23/0.89 rselect_head(queue_35)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3651,f2203])).
% 0.23/0.89 fof(f3653,plain,(
% 0.23/0.89 rselect_head(q14)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3652,f2233])).
% 0.23/0.89 fof(f3654,plain,(
% 0.23/0.89 rselect_head(queue_41)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3653,f2238])).
% 0.23/0.89 fof(f3655,plain,(
% 0.23/0.89 rselect_head(q15)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3654,f2243])).
% 0.23/0.89 fof(f3656,plain,(
% 0.23/0.89 rselect_head(queue_47)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3655,f2262])).
% 0.23/0.89 fof(f3657,plain,(
% 0.23/0.89 rselect_head(q16)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3656,f2301])).
% 0.23/0.89 fof(f3658,plain,(
% 0.23/0.89 rselect_head(queue_53)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3657,f2326])).
% 0.23/0.89 fof(f3659,plain,(
% 0.23/0.89 rselect_head(q17)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3658,f2331])).
% 0.23/0.89 fof(f3660,plain,(
% 0.23/0.89 rselect_head(queue_59)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3659,f2345])).
% 0.23/0.89 fof(f3661,plain,(
% 0.23/0.89 rselect_head(q18)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3660,f2371])).
% 0.23/0.89 fof(f3662,plain,(
% 0.23/0.89 rselect_head(queue_65)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3661,f2376])).
% 0.23/0.89 fof(f3674,plain,(
% 0.23/0.89 rselect_head(q19)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3662,f2395])).
% 0.23/0.89 fof(f3676,plain,(
% 0.23/0.89 rselect_head(queue_71)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3506,f2406])).
% 0.23/0.89 fof(f3677,plain,(
% 0.23/0.89 rselect_head(q9)=index_9),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f3691,f3649])).
% 0.23/0.89 fof(f3691,plain,(
% 0.23/0.89 rselect_head(q2)=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3676,f2424])).
% 0.23/0.89 fof(f3702,plain,(
% 0.23/0.89 rselect_head(queue_77)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3674,f2451])).
% 0.23/0.89 fof(f3703,plain,(
% 0.23/0.89 rselect_head(q20)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3702,f2456])).
% 0.23/0.89 fof(f3704,plain,(
% 0.23/0.89 rselect_head(queue_83)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3703,f2504])).
% 0.23/0.89 fof(f3705,plain,(
% 0.23/0.89 rselect_head(q21)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3704,f2509])).
% 0.23/0.89 fof(f3706,plain,(
% 0.23/0.89 rselect_head(queue_89)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3705,f2514])).
% 0.23/0.89 fof(f3707,plain,(
% 0.23/0.89 rselect_head(q22)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3706,f2530])).
% 0.23/0.89 fof(f3708,plain,(
% 0.23/0.89 rselect_head(queue_95)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3707,f2549])).
% 0.23/0.89 fof(f3709,plain,(
% 0.23/0.89 rselect_head(q23)=rselect_head(q10)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3708,f2554])).
% 0.23/0.89 fof(f3863,plain,(
% 0.23/0.89 index_279=rselect_head(q10)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f3864,f3709])).
% 0.23/0.89 fof(f3864,plain,(
% 0.23/0.89 index_279=rselect_head(q23)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3562,f3461])).
% 0.23/0.89 fof(f3929,plain,(
% 0.23/0.89 index_279=rselect_head(q9)),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3863,f3475])).
% 0.23/0.89 fof(f4002,plain,(
% 0.23/0.89 elem_280=select(earray_244,index_9)),
% 0.23/0.89 inference(backward_demodulation,[status(thm)],[f4005,f2230])).
% 0.23/0.89 fof(f4005,plain,(
% 0.23/0.89 index_279=index_9),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3677,f3929])).
% 0.23/0.89 fof(f4006,plain,(
% 0.23/0.89 elem_280=e45),
% 0.23/0.89 inference(forward_demodulation,[status(thm)],[f3375,f4002])).
% 0.23/0.89 fof(f4007,plain,(
% 0.23/0.89 $false),
% 0.23/0.89 inference(forward_subsumption_resolution,[status(thm)],[f4006,f3376])).
% 0.23/0.89 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.92 % Elapsed time: 0.389856 seconds
% 0.23/0.92 % CPU time: 2.467427 seconds
% 0.23/0.92 % Total memory used: 140.147 MB
% 0.23/0.92 % Net memory used: 139.411 MB
%------------------------------------------------------------------------------